(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)
(declare-fun var10 () String)
(declare-fun var11 () String)
(declare-fun var12 () String)
(declare-fun var13 () String)
(declare-fun var14 () String)
(declare-fun var15 () String)
(declare-fun var16 () String)
(declare-fun var17 () String)
(declare-fun var18 () String)
(declare-fun var19 () String)
(declare-fun var20 () String)
(declare-fun var21 () String)
(declare-fun var22 () String)
(declare-fun var23 () String)
(declare-fun var24 () String)
(declare-fun var25 () String)
(declare-fun var26 () String)
(declare-fun var27 () String)
(declare-fun var28 () String)
(declare-fun var29 () String)
(assert (= 199 (Length var0)))
(assert (= 17 (Length var1)))
(assert (= 224 (Length var2)))
(assert (= 2 (Length var3)))
(assert (= 163 (Length var4)))
(assert (= 72 (Length var5)))
(assert (= 39 (Length var6)))
(assert (= 197 (Length var7)))
(assert (= 36 (Length var8)))
(assert (= 213 (Length var9)))
(assert (= 194 (Length var10)))
(assert (= 129 (Length var11)))
(assert (= 34 (Length var12)))
(assert (= 240 (Length var13)))
(assert (= 29 (Length var14)))
(assert (= 244 (Length var15)))
(assert (= 85 (Length var16)))
(assert (= 1 (Length var17)))
(assert (= 189 (Length var18)))
(assert (= 210 (Length var19)))
(assert (= 82 (Length var20)))
(assert (= 214 (Length var21)))
(assert (= 37 (Length var22)))
(assert (= 84 (Length var23)))
(assert (= 148 (Length var24)))
(assert (= 192 (Length var25)))
(assert (= 16 (Length var26)))
(assert (= 22 (Length var27)))
(assert (= 95 (Length var28)))
(assert (= 53 (Length var29)))
(check-sat)