(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)
(declare-fun var61 () String)
(declare-fun var62 () String)
(declare-fun var63 () String)
(declare-fun var64 () String)
(declare-fun var65 () String)
(declare-fun var66 () String)
(declare-fun var67 () String)
(declare-fun var68 () String)
(declare-fun var69 () String)
(declare-fun var70 () String)
(declare-fun var71 () String)
(declare-fun var72 () String)
(declare-fun var73 () String)
(declare-fun var74 () String)
(declare-fun var75 () String)
(declare-fun var76 () String)
(declare-fun var77 () String)
(declare-fun var78 () String)
(declare-fun var79 () String)
(declare-fun var80 () String)
(declare-fun var81 () String)
(declare-fun var82 () String)
(declare-fun var83 () String)
(declare-fun var84 () String)
(declare-fun var85 () String)
(declare-fun var86 () String)
(declare-fun var87 () String)
(declare-fun var88 () String)
(declare-fun var89 () String)
(declare-fun var90 () String)
(declare-fun var91 () String)
(declare-fun var92 () String)
(declare-fun var93 () String)
(declare-fun var94 () String)
(declare-fun var95 () String)
(declare-fun var96 () String)
(declare-fun var97 () String)
(declare-fun var98 () String)
(declare-fun var99 () String)
(declare-fun var100 () String)
(declare-fun var101 () String)
(declare-fun var102 () String)
(declare-fun var103 () String)
(declare-fun var104 () String)
(declare-fun var105 () String)
(declare-fun var106 () String)
(declare-fun var107 () String)
(declare-fun var108 () String)
(declare-fun var109 () String)
(declare-fun var110 () String)
(declare-fun var111 () String)
(declare-fun var112 () String)
(declare-fun var113 () String)
(declare-fun var114 () String)
(declare-fun var115 () String)
(declare-fun var116 () String)
(declare-fun var117 () String)
(declare-fun var118 () String)
(declare-fun var119 () String)
(declare-fun var120 () String)
(declare-fun var121 () String)
(declare-fun var122 () String)
(declare-fun var123 () String)
(declare-fun var124 () String)
(declare-fun var125 () String)
(declare-fun var126 () String)
(declare-fun var127 () String)
(declare-fun var128 () String)
(declare-fun var129 () String)
(declare-fun var130 () String)
(declare-fun var131 () String)
(declare-fun var132 () String)
(declare-fun var133 () String)
(declare-fun var134 () String)
(declare-fun var135 () String)
(assert (= (str.++ "Fi^" (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 (str.++ var29 (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 (str.++ var59 (str.++ var60 (str.++ var61 (str.++ var62 (str.++ var63 (str.++ var64 (str.++ var65 (str.++ var66 (str.++ var67 (str.++ var68 (str.++ var69 (str.++ var70 (str.++ var71 (str.++ var72 (str.++ var73 (str.++ var74 (str.++ var75 (str.++ var76 (str.++ var77 (str.++ var78 (str.++ var79 (str.++ var80 (str.++ var81 (str.++ var82 (str.++ var83 (str.++ var84 (str.++ var85 (str.++ var86 (str.++ var87 (str.++ var88 (str.++ var89 (str.++ var90 (str.++ var91 (str.++ var92 (str.++ var93 (str.++ var94 (str.++ var95 (str.++ var96 (str.++ var97 (str.++ var98 (str.++ var99 (str.++ var100 (str.++ var101 (str.++ var102 (str.++ var103 (str.++ var104 (str.++ var105 (str.++ var106 (str.++ var107 (str.++ var108 (str.++ var109 (str.++ var110 (str.++ var111 (str.++ var112 (str.++ var113 (str.++ var114 (str.++ var115 (str.++ var116 (str.++ var117 (str.++ var118 (str.++ var119 (str.++ var120 (str.++ var121 (str.++ var122 (str.++ var123 (str.++ var124 (str.++ var125 (str.++ var126 (str.++ var127 (str.++ var128 (str.++ var129 (str.++ var130 (str.++ var131 (str.++ var132 (str.++ var133 (str.++ var134 var135)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (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 (str.++ var29 (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 (str.++ var59 (str.++ var60 (str.++ var61 (str.++ var62 (str.++ var63 (str.++ var64 (str.++ var65 (str.++ var66 (str.++ var67 (str.++ var68 (str.++ var69 (str.++ var70 (str.++ var71 (str.++ var72 (str.++ var73 (str.++ var74 (str.++ var75 (str.++ var76 (str.++ var77 (str.++ var78 (str.++ var79 (str.++ var80 (str.++ var81 (str.++ var82 (str.++ var83 (str.++ var84 (str.++ var85 (str.++ var86 (str.++ var87 (str.++ var88 (str.++ var89 (str.++ var90 (str.++ var91 (str.++ var92 (str.++ var93 (str.++ var94 (str.++ var95 (str.++ var96 (str.++ var97 (str.++ var98 (str.++ var99 (str.++ var100 (str.++ var101 (str.++ var102 (str.++ var103 (str.++ var104 (str.++ var105 (str.++ var106 (str.++ var107 (str.++ var108 (str.++ var109 (str.++ var110 (str.++ var111 (str.++ var112 (str.++ var113 (str.++ var114 (str.++ var115 (str.++ var116 (str.++ var117 (str.++ var118 (str.++ var119 (str.++ var120 (str.++ var121 (str.++ var122 (str.++ var123 (str.++ var124 (str.++ var125 (str.++ var126 (str.++ var127 (str.++ var128 (str.++ var129 (str.++ var130 (str.++ var131 (str.++ var132 (str.++ var133 (str.++ var134 var135))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) "Jdf")))
(check-sat)