(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 (= 1 (str.len var0))) (assert (= 1 (str.len var1))) (assert (= 1 (str.len var2))) (assert (= 1 (str.len var3))) (assert (= 1 (str.len var4))) (assert (= 0 (str.len var5))) (assert (= 0 (str.len var6))) (assert (= 1 (str.len var7))) (assert (= 1 (str.len var8))) (assert (= 1 (str.len var9))) (assert (= 1 (str.len var10))) (assert (= 1 (str.len var11))) (assert (= 1 (str.len var12))) (assert (= 0 (str.len var13))) (assert (= 0 (str.len var14))) (assert (= 0 (str.len var15))) (assert (= 1 (str.len var16))) (assert (= 1 (str.len var17))) (assert (= 0 (str.len var18))) (assert (= 0 (str.len var19))) (assert (= 0 (str.len var20))) (assert (= 0 (str.len var21))) (assert (= 0 (str.len var22))) (assert (= 1 (str.len var23))) (assert (= 0 (str.len var24))) (assert (= 0 (str.len var25))) (assert (= 1 (str.len var26))) (assert (= 1 (str.len var27))) (assert (= 1 (str.len var28))) (assert (= 1 (str.len var29))) (check-sat)