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