(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) (declare-fun var136 () String) (declare-fun var137 () String) (declare-fun var138 () String) (declare-fun var139 () String) (declare-fun var140 () String) (declare-fun var141 () String) (declare-fun var142 () String) (declare-fun var143 () String) (declare-fun var144 () String) (declare-fun var145 () String) (declare-fun var146 () String) (declare-fun var147 () String) (declare-fun var148 () String) (declare-fun var149 () String) (declare-fun var150 () String) (declare-fun var151 () String) (declare-fun var152 () String) (declare-fun var153 () String) (declare-fun var154 () String) (declare-fun var155 () String) (declare-fun var156 () String) (declare-fun var157 () String) (declare-fun var158 () String) (declare-fun var159 () String) (declare-fun var160 () String) (declare-fun var161 () String) (declare-fun var162 () String) (declare-fun var163 () String) (declare-fun var164 () String) (declare-fun var165 () String) (declare-fun var166 () String) (declare-fun var167 () String) (declare-fun var168 () String) (declare-fun var169 () String) (declare-fun var170 () String) (declare-fun var171 () String) (declare-fun var172 () String) (declare-fun var173 () String) (declare-fun var174 () String) (declare-fun var175 () String) (declare-fun var176 () String) (assert (= var0 (Concat var1 var2))) (assert (= var2 (Concat var3 var4))) (assert (= var4 (Concat var5 var6))) (assert (= var6 (Concat var7 var8))) (assert (= var8 (Concat var9 var10))) (assert (= var10 (Concat var11 var12))) (assert (= var12 (Concat var13 var14))) (assert (= var14 (Concat var15 var16))) (assert (= var16 (Concat var17 var18))) (assert (= var18 (Concat var19 var20))) (assert (= var20 (Concat var21 var22))) (assert (= var22 (Concat var23 var24))) (assert (= var24 (Concat var25 var26))) (assert (= var26 (Concat var27 var28))) (assert (= var28 (Concat var29 var30))) (assert (= var30 (Concat var31 var32))) (assert (= var32 (Concat var33 var34))) (assert (= var34 (Concat var35 var36))) (assert (= var36 (Concat var37 var38))) (assert (= var38 (Concat var39 var40))) (assert (= var40 (Concat var41 var42))) (assert (= var42 (Concat var43 var44))) (assert (= var44 (Concat var45 var46))) (assert (= var46 (Concat var47 var48))) (assert (= var48 (Concat var49 var50))) (assert (= var50 (Concat var51 var52))) (assert (= var52 (Concat var53 var54))) (assert (= var54 (Concat var55 var56))) (assert (= var56 (Concat var57 var58))) (assert (= var58 (Concat var59 var60))) (assert (= var60 (Concat var61 var62))) (assert (= var62 (Concat var63 var64))) (assert (= var64 (Concat var65 var66))) (assert (= var66 (Concat var67 var68))) (assert (= var68 (Concat var69 var70))) (assert (= var70 (Concat var71 var72))) (assert (= var72 (Concat var73 var74))) (assert (= var74 (Concat var75 var76))) (assert (= var76 (Concat var77 var78))) (assert (= var78 (Concat var79 var80))) (assert (= var80 (Concat var81 var82))) (assert (= var82 (Concat var83 var84))) (assert (= var84 (Concat var85 var86))) (assert (= var86 (Concat var87 var88))) (assert (= var88 (Concat var89 var90))) (assert (= var90 (Concat var91 var92))) (assert (= var92 (Concat var93 var94))) (assert (= var94 (Concat var95 var96))) (assert (= var96 (Concat var97 var98))) (assert (= var98 (Concat var99 var100))) (assert (= var100 (Concat var101 var102))) (assert (= var102 (Concat var103 var104))) (assert (= var104 (Concat var105 var106))) (assert (= var106 (Concat var107 var108))) (assert (= var108 (Concat var109 var110))) (assert (= var110 (Concat var111 var112))) (assert (= var112 (Concat var113 var114))) (assert (= var114 (Concat var115 var116))) (assert (= var116 (Concat var117 var118))) (assert (= var118 (Concat var119 var120))) (assert (= var120 (Concat var121 var122))) (assert (= var122 (Concat var123 var124))) (assert (= var124 (Concat var125 var126))) (assert (= var126 (Concat var127 var128))) (assert (= var128 (Concat var129 var130))) (assert (= var130 (Concat var131 var132))) (assert (= var132 (Concat var133 var134))) (assert (= var134 (Concat var135 var136))) (assert (= var136 (Concat var137 var138))) (assert (= var138 (Concat var139 var140))) (assert (= var140 (Concat var141 var142))) (assert (= var142 (Concat var143 var144))) (assert (= var144 (Concat var145 var146))) (assert (= var146 (Concat var147 var148))) (assert (= var148 (Concat var149 var150))) (assert (= var150 (Concat var151 var152))) (assert (= var152 (Concat var153 var154))) (assert (= var154 (Concat var155 var156))) (assert (= var156 (Concat var157 var158))) (assert (= var158 (Concat var159 var160))) (assert (= var160 (Concat var161 var162))) (assert (= var162 (Concat var163 var164))) (assert (= var164 (Concat var165 var166))) (assert (= var166 (Concat var167 var168))) (assert (= var168 (Concat var169 var170))) (assert (= var170 (Concat var171 var172))) (assert (= var172 (Concat var173 var174))) (assert (= var174 (Concat var175 var176))) (assert (= var0 "solution")) (check-sat)