% Unsatisfiable
reset.
prop a_0 := [[~ x_0]] & [[~ x_1]] .
prop a_1 := x_2 = 0 .
prop a_2 := x_3 = 1 .
prop a_3 := x_4 = (x_5 + x_6) .
prop x_7 := [~ x_8] .
prop x_9 := x_10 = x_11 .
prop a_4 := x_12 = (x_11 + x_6) .
prop x_13 := x_5 = 2 .
prop x_14 := [[~ x_15]] & [[~ x_16]] .
prop x_17 := x_18 = 0 .
prop x_19 := x_18 = x_5 .
prop x_20 := x_15 & [[~ x_16]] .
prop x_21 := x_4 <= 2 .
prop a_5 := x_22 = (x_23 + x_24) .
prop x_25 := [~ x_26] .
prop x_27 := x_11 = x_28 .
prop a_6 := x_29 = (x_28 + x_24) .
prop x_30 := x_23 = 2 .
prop x_31 := [[~ x_32]] & [[~ x_33]] .
prop x_34 := x_5 = 0 .
prop x_35 := x_5 = x_23 .
prop x_36 := x_32 & [[~ x_33]] .
prop x_37 := x_22 <= 2 .
prop a_7 := x_38 = (x_39 + x_40) .
prop x_41 := [~ x_42] .
prop x_43 := x_28 = x_44 .
prop a_8 := x_45 = (x_44 + x_40) .
prop x_46 := x_39 = 2 .
prop x_47 := [[~ x_48]] & [[~ x_49]] .
prop x_50 := x_23 = 0 .
prop x_51 := x_23 = x_39 .
prop x_52 := x_48 & [[~ x_49]] .
prop x_53 := x_38 <= 2 .
prop a_9 := x_54 = (x_55 + x_56) .
prop x_57 := [~ x_58] .
prop x_59 := x_44 = x_60 .
prop a_10 := x_61 = (x_60 + x_56) .
prop x_62 := x_55 = 2 .
prop x_63 := [[~ x_64]] & [[~ x_65]] .
prop x_66 := x_39 = 0 .
prop x_67 := x_39 = x_55 .
prop x_68 := x_64 & [[~ x_65]] .
prop x_69 := x_54 <= 2 .
prop a_11 := x_70 = (x_71 + x_72) .
prop x_73 := [~ x_74] .
prop x_75 := x_60 = x_76 .
prop a_12 := x_77 = (x_76 + x_72) .
prop x_78 := x_71 = 2 .
prop x_79 := [[~ x_80]] & [[~ x_81]] .
prop x_82 := x_55 = 0 .
prop x_83 := x_55 = x_71 .
prop x_84 := x_80 & [[~ x_81]] .
prop x_85 := x_70 <= 2 .
prop a_13 := x_86 = (x_87 + x_88) .
prop x_89 := [~ x_90] .
prop x_91 := x_76 = x_92 .
prop a_14 := x_93 = (x_92 + x_88) .
prop x_94 := x_87 = 2 .
prop x_95 := [[~ x_96]] & [[~ x_97]] .
prop x_98 := x_71 = 0 .
prop x_99 := x_71 = x_87 .
prop x_100 := x_96 & [[~ x_97]] .
prop x_101 := x_86 <= 2 .
prop a_15 := x_102 = (x_103 + x_104) .
prop x_105 := [~ x_106] .
prop x_107 := x_92 = x_108 .
prop a_16 := x_109 = (x_108 + x_104) .
prop x_110 := x_103 = 2 .
prop x_111 := [[~ x_112]] & [[~ x_113]] .
prop x_114 := x_87 = 0 .
prop x_115 := x_87 = x_103 .
prop x_116 := x_112 & [[~ x_113]] .
prop x_117 := x_102 <= 2 .
prop a_17 := x_118 = (x_119 + x_120) .
prop x_121 := [~ x_122] .
prop x_123 := x_108 = x_124 .
prop a_18 := x_125 = (x_124 + x_120) .
prop x_126 := x_119 = 2 .
prop x_127 := [[~ x_128]] & [[~ x_129]] .
prop x_130 := x_103 = 0 .
prop x_131 := x_103 = x_119 .
prop x_132 := x_128 & [[~ x_129]] .
prop x_133 := x_118 <= 2 .
prop a_19 := x_134 = (x_135 + x_136) .
prop x_137 := [~ x_138] .
prop x_139 := x_124 = x_140 .
prop a_20 := x_141 = (x_140 + x_136) .
prop x_142 := x_135 = 2 .
prop x_143 := [[~ x_144]] & [[~ x_145]] .
prop x_146 := x_119 = 0 .
prop x_147 := x_119 = x_135 .
prop x_148 := x_144 & [[~ x_145]] .
prop x_149 := x_134 <= 2 .
prop a_21 := x_150 = (x_2 + x_151) .
prop x_152 := [~ x_153] .
prop x_154 := x_140 = x_3 .
prop a_22 := x_155 = (x_3 + x_151) .
prop x_156 := x_2 = 2 .
prop x_157 := [[~ x_0]] & [[~ x_1]] .
prop x_158 := x_135 = 0 .
prop x_159 := x_135 = x_2 .
prop x_160 := x_0 & [[~ x_1]] .
prop x_161 := x_150 <= 2 .
prop a_23 := [~ [x_162 < 0]] .
prop a_24 := if [x_8] then [[~ x_163]] else [x_163] end .
prop a_25 := x_164 <=> x_163 .
prop a_26 := if [x_14 | x_20] then [x_165 = x_12] else [x_165 = (x_11 - (x_6 * 2))] end .
prop a_27 := [[x_166 = 0] & x_7 & x_14 & [x_11 = 10] & x_167 & [[~ x_168]] & x_17 & x_9] | [[x_166 = 1] & x_7 & x_20 & x_13 & [[~ [x_11 < 5]]] & [[~ x_167]] & x_168 & x_19 & x_9] | [[x_166 = 2] & x_7 & [[~ x_15]] & x_16 & [x_11 = 5] & x_167 & x_168 & x_17 & x_9] | [[x_166 = 3] & x_7 & x_15 & x_16 & x_13 & [x_11 <= 10] & [[~ x_167]] & [[~ x_168]] & x_19 & x_9] | [[x_166 = 4] & x_8 & [[~ [x_6 < 0]]] & [x_15 | x_16 | [x_12 <= 10]] & [[[~ x_15]] | x_16 | x_21] & [x_15 | [[~ x_16]] | [[~ [x_12 < 5]]]] & [[[~ x_15]] | [[~ x_16]] | x_21] & [x_18 = x_4] & [x_10 = x_165] & [x_167 <=> x_15] & [x_168 <=> x_16]] .
prop a_28 := [~ [x_6 < 0]] .
prop a_29 := if [x_26] then [[~ x_169]] else [x_169] end .
prop a_30 := x_8 <=> x_169 .
prop a_31 := if [x_31 | x_36] then [x_170 = x_29] else [x_170 = (x_28 - (x_24 * 2))] end .
prop a_32 := [[x_171 = 0] & x_25 & x_31 & [x_28 = 10] & x_15 & [[~ x_16]] & x_34 & x_27] | [[x_171 = 1] & x_25 & x_36 & x_30 & [[~ [x_28 < 5]]] & [[~ x_15]] & x_16 & x_35 & x_27] | [[x_171 = 2] & x_25 & [[~ x_32]] & x_33 & [x_28 = 5] & x_15 & x_16 & x_34 & x_27] | [[x_171 = 3] & x_25 & x_32 & x_33 & x_30 & [x_28 <= 10] & [[~ x_15]] & [[~ x_16]] & x_35 & x_27] | [[x_171 = 4] & x_26 & [[~ [x_24 < 0]]] & [x_32 | x_33 | [x_29 <= 10]] & [[[~ x_32]] | x_33 | x_37] & [x_32 | [[~ x_33]] | [[~ [x_29 < 5]]]] & [[[~ x_32]] | [[~ x_33]] | x_37] & [x_5 = x_22] & [x_11 = x_170] & [x_15 <=> x_32] & [x_16 <=> x_33]] .
prop a_33 := [~ [x_24 < 0]] .
prop a_34 := if [x_42] then [[~ x_172]] else [x_172] end .
prop a_35 := x_26 <=> x_172 .
prop a_36 := if [x_47 | x_52] then [x_173 = x_45] else [x_173 = (x_44 - (x_40 * 2))] end .
prop a_37 := [[x_174 = 0] & x_41 & x_47 & [x_44 = 10] & x_32 & [[~ x_33]] & x_50 & x_43] | [[x_174 = 1] & x_41 & x_52 & x_46 & [[~ [x_44 < 5]]] & [[~ x_32]] & x_33 & x_51 & x_43] | [[x_174 = 2] & x_41 & [[~ x_48]] & x_49 & [x_44 = 5] & x_32 & x_33 & x_50 & x_43] | [[x_174 = 3] & x_41 & x_48 & x_49 & x_46 & [x_44 <= 10] & [[~ x_32]] & [[~ x_33]] & x_51 & x_43] | [[x_174 = 4] & x_42 & [[~ [x_40 < 0]]] & [x_48 | x_49 | [x_45 <= 10]] & [[[~ x_48]] | x_49 | x_53] & [x_48 | [[~ x_49]] | [[~ [x_45 < 5]]]] & [[[~ x_48]] | [[~ x_49]] | x_53] & [x_23 = x_38] & [x_28 = x_173] & [x_32 <=> x_48] & [x_33 <=> x_49]] .
prop a_38 := [~ [x_40 < 0]] .
prop a_39 := if [x_58] then [[~ x_175]] else [x_175] end .
prop a_40 := x_42 <=> x_175 .
prop a_41 := if [x_63 | x_68] then [x_176 = x_61] else [x_176 = (x_60 - (x_56 * 2))] end .
prop a_42 := [[x_177 = 0] & x_57 & x_63 & [x_60 = 10] & x_48 & [[~ x_49]] & x_66 & x_59] | [[x_177 = 1] & x_57 & x_68 & x_62 & [[~ [x_60 < 5]]] & [[~ x_48]] & x_49 & x_67 & x_59] | [[x_177 = 2] & x_57 & [[~ x_64]] & x_65 & [x_60 = 5] & x_48 & x_49 & x_66 & x_59] | [[x_177 = 3] & x_57 & x_64 & x_65 & x_62 & [x_60 <= 10] & [[~ x_48]] & [[~ x_49]] & x_67 & x_59] | [[x_177 = 4] & x_58 & [[~ [x_56 < 0]]] & [x_64 | x_65 | [x_61 <= 10]] & [[[~ x_64]] | x_65 | x_69] & [x_64 | [[~ x_65]] | [[~ [x_61 < 5]]]] & [[[~ x_64]] | [[~ x_65]] | x_69] & [x_39 = x_54] & [x_44 = x_176] & [x_48 <=> x_64] & [x_49 <=> x_65]] .
prop a_43 := [~ [x_56 < 0]] .
prop a_44 := if [x_74] then [[~ x_178]] else [x_178] end .
prop a_45 := x_58 <=> x_178 .
prop a_46 := if [x_79 | x_84] then [x_179 = x_77] else [x_179 = (x_76 - (x_72 * 2))] end .
prop a_47 := [[x_180 = 0] & x_73 & x_79 & [x_76 = 10] & x_64 & [[~ x_65]] & x_82 & x_75] | [[x_180 = 1] & x_73 & x_84 & x_78 & [[~ [x_76 < 5]]] & [[~ x_64]] & x_65 & x_83 & x_75] | [[x_180 = 2] & x_73 & [[~ x_80]] & x_81 & [x_76 = 5] & x_64 & x_65 & x_82 & x_75] | [[x_180 = 3] & x_73 & x_80 & x_81 & x_78 & [x_76 <= 10] & [[~ x_64]] & [[~ x_65]] & x_83 & x_75] | [[x_180 = 4] & x_74 & [[~ [x_72 < 0]]] & [x_80 | x_81 | [x_77 <= 10]] & [[[~ x_80]] | x_81 | x_85] & [x_80 | [[~ x_81]] | [[~ [x_77 < 5]]]] & [[[~ x_80]] | [[~ x_81]] | x_85] & [x_55 = x_70] & [x_60 = x_179] & [x_64 <=> x_80] & [x_65 <=> x_81]] .
prop a_48 := [~ [x_72 < 0]] .
prop a_49 := if [x_90] then [[~ x_181]] else [x_181] end .
prop a_50 := x_74 <=> x_181 .
prop a_51 := if [x_95 | x_100] then [x_182 = x_93] else [x_182 = (x_92 - (x_88 * 2))] end .
prop a_52 := [[x_183 = 0] & x_89 & x_95 & [x_92 = 10] & x_80 & [[~ x_81]] & x_98 & x_91] | [[x_183 = 1] & x_89 & x_100 & x_94 & [[~ [x_92 < 5]]] & [[~ x_80]] & x_81 & x_99 & x_91] | [[x_183 = 2] & x_89 & [[~ x_96]] & x_97 & [x_92 = 5] & x_80 & x_81 & x_98 & x_91] | [[x_183 = 3] & x_89 & x_96 & x_97 & x_94 & [x_92 <= 10] & [[~ x_80]] & [[~ x_81]] & x_99 & x_91] | [[x_183 = 4] & x_90 & [[~ [x_88 < 0]]] & [x_96 | x_97 | [x_93 <= 10]] & [[[~ x_96]] | x_97 | x_101] & [x_96 | [[~ x_97]] | [[~ [x_93 < 5]]]] & [[[~ x_96]] | [[~ x_97]] | x_101] & [x_71 = x_86] & [x_76 = x_182] & [x_80 <=> x_96] & [x_81 <=> x_97]] .
prop a_53 := [~ [x_88 < 0]] .
prop a_54 := if [x_106] then [[~ x_184]] else [x_184] end .
prop a_55 := x_90 <=> x_184 .
prop a_56 := if [x_111 | x_116] then [x_185 = x_109] else [x_185 = (x_108 - (x_104 * 2))] end .
prop a_57 := [[x_186 = 0] & x_105 & x_111 & [x_108 = 10] & x_96 & [[~ x_97]] & x_114 & x_107] | [[x_186 = 1] & x_105 & x_116 & x_110 & [[~ [x_108 < 5]]] & [[~ x_96]] & x_97 & x_115 & x_107] | [[x_186 = 2] & x_105 & [[~ x_112]] & x_113 & [x_108 = 5] & x_96 & x_97 & x_114 & x_107] | [[x_186 = 3] & x_105 & x_112 & x_113 & x_110 & [x_108 <= 10] & [[~ x_96]] & [[~ x_97]] & x_115 & x_107] | [[x_186 = 4] & x_106 & [[~ [x_104 < 0]]] & [x_112 | x_113 | [x_109 <= 10]] & [[[~ x_112]] | x_113 | x_117] & [x_112 | [[~ x_113]] | [[~ [x_109 < 5]]]] & [[[~ x_112]] | [[~ x_113]] | x_117] & [x_87 = x_102] & [x_92 = x_185] & [x_96 <=> x_112] & [x_97 <=> x_113]] .
prop a_58 := [~ [x_104 < 0]] .
prop a_59 := if [x_122] then [[~ x_187]] else [x_187] end .
prop a_60 := x_106 <=> x_187 .
prop a_61 := if [x_127 | x_132] then [x_188 = x_125] else [x_188 = (x_124 - (x_120 * 2))] end .
prop a_62 := [[x_189 = 0] & x_121 & x_127 & [x_124 = 10] & x_112 & [[~ x_113]] & x_130 & x_123] | [[x_189 = 1] & x_121 & x_132 & x_126 & [[~ [x_124 < 5]]] & [[~ x_112]] & x_113 & x_131 & x_123] | [[x_189 = 2] & x_121 & [[~ x_128]] & x_129 & [x_124 = 5] & x_112 & x_113 & x_130 & x_123] | [[x_189 = 3] & x_121 & x_128 & x_129 & x_126 & [x_124 <= 10] & [[~ x_112]] & [[~ x_113]] & x_131 & x_123] | [[x_189 = 4] & x_122 & [[~ [x_120 < 0]]] & [x_128 | x_129 | [x_125 <= 10]] & [[[~ x_128]] | x_129 | x_133] & [x_128 | [[~ x_129]] | [[~ [x_125 < 5]]]] & [[[~ x_128]] | [[~ x_129]] | x_133] & [x_103 = x_118] & [x_108 = x_188] & [x_112 <=> x_128] & [x_113 <=> x_129]] .
prop a_63 := [~ [x_120 < 0]] .
prop a_64 := if [x_138] then [[~ x_190]] else [x_190] end .
prop a_65 := x_122 <=> x_190 .
prop a_66 := if [x_143 | x_148] then [x_191 = x_141] else [x_191 = (x_140 - (x_136 * 2))] end .
prop a_67 := [[x_192 = 0] & x_137 & x_143 & [x_140 = 10] & x_128 & [[~ x_129]] & x_146 & x_139] | [[x_192 = 1] & x_137 & x_148 & x_142 & [[~ [x_140 < 5]]] & [[~ x_128]] & x_129 & x_147 & x_139] | [[x_192 = 2] & x_137 & [[~ x_144]] & x_145 & [x_140 = 5] & x_128 & x_129 & x_146 & x_139] | [[x_192 = 3] & x_137 & x_144 & x_145 & x_142 & [x_140 <= 10] & [[~ x_128]] & [[~ x_129]] & x_147 & x_139] | [[x_192 = 4] & x_138 & [[~ [x_136 < 0]]] & [x_144 | x_145 | [x_141 <= 10]] & [[[~ x_144]] | x_145 | x_149] & [x_144 | [[~ x_145]] | [[~ [x_141 < 5]]]] & [[[~ x_144]] | [[~ x_145]] | x_149] & [x_119 = x_134] & [x_124 = x_191] & [x_128 <=> x_144] & [x_129 <=> x_145]] .
prop a_68 := [~ [x_136 < 0]] .
prop a_69 := if [x_153] then [[~ x_193]] else [x_193] end .
prop a_70 := x_138 <=> x_193 .
prop a_71 := if [x_157 | x_160] then [x_194 = x_155] else [x_194 = (x_3 - (x_151 * 2))] end .
prop a_72 := [[x_195 = 0] & x_152 & x_157 & [x_3 = 10] & x_144 & [[~ x_145]] & x_158 & x_154] | [[x_195 = 1] & x_152 & x_160 & x_156 & [[~ [x_3 < 5]]] & [[~ x_144]] & x_145 & x_159 & x_154] | [[x_195 = 2] & x_152 & [[~ x_0]] & x_1 & [x_3 = 5] & x_144 & x_145 & x_158 & x_154] | [[x_195 = 3] & x_152 & x_0 & x_1 & x_156 & [x_3 <= 10] & [[~ x_144]] & [[~ x_145]] & x_159 & x_154] | [[x_195 = 4] & x_153 & [[~ [x_151 < 0]]] & [x_0 | x_1 | [x_155 <= 10]] & [[[~ x_0]] | x_1 | x_161] & [x_0 | [[~ x_1]] | [[~ [x_155 < 5]]]] & [[[~ x_0]] | [[~ x_1]] | x_161] & [x_135 = x_150] & [x_140 = x_194] & [x_144 <=> x_0] & [x_145 <=> x_1]] .
prop a_73 := [x_10 < 1] | [[~ [x_10 <= 12]]] | [x_11 < 1] | [[~ [x_11 <= 12]]] | [x_28 < 1] | [[~ [x_28 <= 12]]] | [x_44 < 1] | [[~ [x_44 <= 12]]] | [x_60 < 1] | [[~ [x_60 <= 12]]] | [x_76 < 1] | [[~ [x_76 <= 12]]] | [x_92 < 1] | [[~ [x_92 <= 12]]] | [x_108 < 1] | [[~ [x_108 <= 12]]] | [x_124 < 1] | [[~ [x_124 <= 12]]] | [x_140 < 1] | [[~ [x_140 <= 12]]] | [x_3 < 1] | [[~ [x_3 <= 12]]] .
prop bb := tt.
sat bb & a_0 & a_1 & a_2 & a_3 & a_4 & a_5 & a_6 & a_7 & a_8 & a_9 & a_10 & 
     a_11 & a_12 & a_13 & a_14 & a_15 & a_16 & a_17 & a_18 & a_19 & a_20 & a_21 & a_22 & 
     a_23 & a_24 & a_25 & a_26 & a_27 & a_28 & a_29 & a_30 & a_31 & a_32 & a_33 & 
     a_34 & a_35 & a_36 & a_37 & a_38 & a_39 & a_40 & a_41 & a_42 & a_43 & a_44 & 
     a_45 & a_46 & a_47 & a_48 & a_49 & a_50 & a_51 & a_52 & a_53 & a_54 & a_55 & 
     a_56 & a_57 & a_58 & a_59 & a_60 & a_61 & a_62 & a_63 & a_64 & a_65 & a_66 & 
     a_67 & a_68 & a_69 & a_70 & a_71 & a_72 & a_73.