(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) (declare-fun var30 () String) (declare-fun var31 () String) (declare-fun var32 () String) (declare-fun var33 () String) (declare-fun var34 () String) (declare-fun var35 () String) (declare-fun var36 () String) (declare-fun var37 () String) (declare-fun var38 () String) (declare-fun var39 () String) (declare-fun var40 () String) (declare-fun var41 () String) (declare-fun var42 () String) (declare-fun var43 () String) (declare-fun var44 () String) (declare-fun var45 () String) (declare-fun var46 () String) (declare-fun var47 () String) (declare-fun var48 () String) (declare-fun var49 () String) (declare-fun var50 () String) (declare-fun var51 () String) (declare-fun var52 () String) (declare-fun var53 () String) (declare-fun var54 () String) (declare-fun var55 () String) (declare-fun var56 () String) (declare-fun var57 () String) (declare-fun var58 () String) (declare-fun var59 () String) (declare-fun var60 () String) (assert (= var0 (Concat var1 var2))) (assert (= var2 (Concat var3 var4))) (assert (= var4 (Concat var5 var6))) (assert (= var6 (Concat var7 var8))) (assert (= var8 (Concat var9 var10))) (assert (= var10 (Concat var11 var12))) (assert (= var12 (Concat var13 var14))) (assert (= var14 (Concat var15 var16))) (assert (= var16 (Concat var17 var18))) (assert (= var18 (Concat var19 var20))) (assert (= var20 (Concat var21 var22))) (assert (= var22 (Concat var23 var24))) (assert (= var24 (Concat var25 var26))) (assert (= var26 (Concat var27 var28))) (assert (= var28 (Concat var29 var30))) (assert (= var30 (Concat var31 var32))) (assert (= var32 (Concat var33 var34))) (assert (= var34 (Concat var35 var36))) (assert (= var36 (Concat var37 var38))) (assert (= var38 (Concat var39 var40))) (assert (= var40 (Concat var41 var42))) (assert (= var42 (Concat var43 var44))) (assert (= var44 (Concat var45 var46))) (assert (= var46 (Concat var47 var48))) (assert (= var48 (Concat var49 var50))) (assert (= var50 (Concat var51 var52))) (assert (= var52 (Concat var53 var54))) (assert (= var54 (Concat var55 var56))) (assert (= var56 (Concat var57 var58))) (assert (= var58 (Concat var59 var60))) (assert (= var0 "solution")) (assert (= "9" (CharAt var41 592))) (check-sat)