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