(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 (= (Concat "Fi^" (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 (Concat var29 (Concat var30 (Concat var31 (Concat var32 (Concat var33 (Concat var34 (Concat var35 (Concat var36 (Concat var37 (Concat var38 (Concat var39 (Concat var40 (Concat var41 (Concat var42 (Concat var43 (Concat var44 (Concat var45 (Concat var46 (Concat var47 (Concat var48 (Concat var49 (Concat var50 (Concat var51 (Concat var52 (Concat var53 (Concat var54 (Concat var55 (Concat var56 (Concat var57 (Concat var58 (Concat var59 (Concat var60 (Concat var61 (Concat var62 (Concat var63 (Concat var64 (Concat var65 (Concat var66 (Concat var67 (Concat var68 (Concat var69 (Concat var70 (Concat var71 (Concat var72 (Concat var73 (Concat var74 (Concat var75 (Concat var76 (Concat var77 (Concat var78 (Concat var79 (Concat var80 (Concat var81 (Concat var82 (Concat var83 (Concat var84 (Concat var85 (Concat var86 (Concat var87 (Concat var88 (Concat var89 (Concat var90 (Concat var91 (Concat var92 (Concat var93 (Concat var94 (Concat var95 (Concat var96 (Concat var97 (Concat var98 (Concat var99 (Concat var100 (Concat var101 (Concat var102 (Concat var103 (Concat var104 (Concat var105 (Concat var106 (Concat var107 (Concat var108 (Concat var109 (Concat var110 (Concat var111 (Concat var112 (Concat var113 (Concat var114 (Concat var115 (Concat var116 (Concat var117 (Concat var118 (Concat var119 (Concat var120 (Concat var121 (Concat var122 (Concat var123 (Concat var124 (Concat var125 (Concat var126 (Concat var127 (Concat var128 (Concat var129 (Concat var130 (Concat var131 (Concat var132 (Concat var133 (Concat var134 var135)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (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 (Concat var29 (Concat var30 (Concat var31 (Concat var32 (Concat var33 (Concat var34 (Concat var35 (Concat var36 (Concat var37 (Concat var38 (Concat var39 (Concat var40 (Concat var41 (Concat var42 (Concat var43 (Concat var44 (Concat var45 (Concat var46 (Concat var47 (Concat var48 (Concat var49 (Concat var50 (Concat var51 (Concat var52 (Concat var53 (Concat var54 (Concat var55 (Concat var56 (Concat var57 (Concat var58 (Concat var59 (Concat var60 (Concat var61 (Concat var62 (Concat var63 (Concat var64 (Concat var65 (Concat var66 (Concat var67 (Concat var68 (Concat var69 (Concat var70 (Concat var71 (Concat var72 (Concat var73 (Concat var74 (Concat var75 (Concat var76 (Concat var77 (Concat var78 (Concat var79 (Concat var80 (Concat var81 (Concat var82 (Concat var83 (Concat var84 (Concat var85 (Concat var86 (Concat var87 (Concat var88 (Concat var89 (Concat var90 (Concat var91 (Concat var92 (Concat var93 (Concat var94 (Concat var95 (Concat var96 (Concat var97 (Concat var98 (Concat var99 (Concat var100 (Concat var101 (Concat var102 (Concat var103 (Concat var104 (Concat var105 (Concat var106 (Concat var107 (Concat var108 (Concat var109 (Concat var110 (Concat var111 (Concat var112 (Concat var113 (Concat var114 (Concat var115 (Concat var116 (Concat var117 (Concat var118 (Concat var119 (Concat var120 (Concat var121 (Concat var122 (Concat var123 (Concat var124 (Concat var125 (Concat var126 (Concat var127 (Concat var128 (Concat var129 (Concat var130 (Concat var131 (Concat var132 (Concat var133 (Concat var134 var135))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) "Jdf")))
(check-sat)