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