(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 (= 2640 (str.len var0)))
(assert (= 2621 (str.len var1)))
(assert (= 1701 (str.len var2)))
(assert (= 782 (str.len var3)))
(assert (= 2484 (str.len var4)))
(assert (= 2451 (str.len var5)))
(assert (= 1598 (str.len var6)))
(assert (= 832 (str.len var7)))
(assert (= 1986 (str.len var8)))
(assert (= 3347 (str.len var9)))
(assert (= 4373 (str.len var10)))
(assert (= 1342 (str.len var11)))
(assert (= 2586 (str.len var12)))
(assert (= 1743 (str.len var13)))
(assert (= 3427 (str.len var14)))
(assert (= 3807 (str.len var15)))
(assert (= 2005 (str.len var16)))
(assert (= 2249 (str.len var17)))
(assert (= 4282 (str.len var18)))
(assert (= 2986 (str.len var19)))
(assert (= 3215 (str.len var20)))
(assert (= 542 (str.len var21)))
(assert (= 4794 (str.len var22)))
(assert (= 3903 (str.len var23)))
(assert (= 3604 (str.len var24)))
(assert (= 792 (str.len var25)))
(assert (= 1365 (str.len var26)))
(assert (= 987 (str.len var27)))
(assert (= 4293 (str.len var28)))
(assert (= 2184 (str.len var29)))
(check-sat)