(set-logic QF_S)
(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () String)
(declare-fun var4 () String)
(declare-fun var5 () String)
(declare-fun var6 () String)
(declare-fun var7 () String)
(declare-fun var8 () String)
(declare-fun var9 () String)
(assert (= 33 (Length var0)))
(assert (= 1 (Length var1)))
(assert (= 49 (Length var2)))
(assert (= 50 (Length var3)))
(assert (= 25 (Length var4)))
(assert (= 3 (Length var5)))
(assert (= 77 (Length var6)))
(assert (= 20 (Length var7)))
(assert (= 100 (Length var8)))
(assert (= 7 (Length var9)))
(assert (= 84 (Length (Concat var6 var9))))
(check-sat)