(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 (= (str.++ "0>|" (str.++ var0 (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 var29)))))))))))))))))))))))))))))) (str.++ (str.++ var0 (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 var29))))))))))))))))))))))))))))) "H-A")))
(check-sat)