(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)