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