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