(benchmark tgc_io_nosafe_7.smt :source { SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria Sorea, and Leonardo de Moura. Contact demoura@csl.sri.com for more information. This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite } :status unknown :logic QF_LRA :extrasorts (ANY) :extrapreds ((x_0)) :extrapreds ((x_1)) :extrapreds ((x_2)) :extrapreds ((x_3)) :extrapreds ((x_4)) :extrapreds ((x_5)) :extrafuns ((x_6 Real)) :extrafuns ((x_7 Real)) :extrafuns ((x_8 Real)) :extrafuns ((x_9 Real)) :extrafuns ((x_10 Real)) :extrafuns ((x_11 Real)) :extrafuns ((x_12 Real)) :extrafuns ((x_13 Real)) :extrapreds ((x_14)) :extrapreds ((x_15)) :extrapreds ((x_16)) :extrapreds ((x_17)) :extrapreds ((x_18)) :extrapreds ((x_19)) :extrapreds ((x_20)) :extrafuns ((x_21 Real)) :extrapreds ((x_22)) :extrapreds ((x_23)) :extrafuns ((x_24 Real)) :extrafuns ((x_25 Real)) :extrafuns ((x_26 Real)) :extrafuns ((x_27 Real)) :extrapreds ((x_28)) :extrapreds ((x_29)) :extrafuns ((x_30 Real)) :extrafuns ((x_31 Real)) :extrapreds ((x_32)) :extrapreds ((x_33)) :extrafuns ((x_34 Real)) :extrapreds ((x_35)) :extrapreds ((x_36)) :extrafuns ((x_37 Real)) :extrapreds ((x_38)) :extrapreds ((x_39)) :extrapreds ((x_40)) :extrapreds ((x_41)) :extrapreds ((x_42)) :extrapreds ((x_43)) :extrafuns ((x_44 Real)) :extrapreds ((x_45)) :extrapreds ((x_46)) :extrafuns ((x_47 Real)) :extrafuns ((x_48 Real)) :extrafuns ((x_49 Real)) :extrapreds ((x_50)) :extrapreds ((x_51)) :extrafuns ((x_52 Real)) :extrafuns ((x_53 Real)) :extrafuns ((x_54 Real)) :extrafuns ((x_55 Real)) :extrapreds ((x_56)) :extrapreds ((x_57)) :extrapreds ((x_58)) :extrapreds ((x_59)) :extrapreds ((x_60)) :extrapreds ((x_61)) :extrafuns ((x_62 Real)) :extrapreds ((x_63)) :extrapreds ((x_64)) :extrafuns ((x_65 Real)) :extrafuns ((x_66 Real)) :extrafuns ((x_67 Real)) :extrapreds ((x_68)) :extrapreds ((x_69)) :extrafuns ((x_70 Real)) :extrafuns ((x_71 Real)) :extrafuns ((x_72 Real)) :extrafuns ((x_73 Real)) :extrapreds ((x_74)) :extrapreds ((x_75)) :extrapreds ((x_76)) :extrapreds ((x_77)) :extrapreds ((x_78)) :extrapreds ((x_79)) :extrafuns ((x_80 Real)) :extrapreds ((x_81)) :extrapreds ((x_82)) :extrafuns ((x_83 Real)) :extrafuns ((x_84 Real)) :extrafuns ((x_85 Real)) :extrapreds ((x_86)) :extrapreds ((x_87)) :extrafuns ((x_88 Real)) :extrafuns ((x_89 Real)) :extrafuns ((x_90 Real)) :extrafuns ((x_91 Real)) :extrapreds ((x_92)) :extrapreds ((x_93)) :extrapreds ((x_94)) :extrapreds ((x_95)) :extrapreds ((x_96)) :extrapreds ((x_97)) :extrafuns ((x_98 Real)) :extrapreds ((x_99)) :extrapreds ((x_100)) :extrafuns ((x_101 Real)) :extrafuns ((x_102 Real)) :extrafuns ((x_103 Real)) :extrapreds ((x_104)) :extrapreds ((x_105)) :extrafuns ((x_106 Real)) :extrafuns ((x_107 Real)) :extrafuns ((x_108 Real)) :extrafuns ((x_109 Real)) :extrapreds ((x_110)) :extrapreds ((x_111)) :extrapreds ((x_112)) :extrapreds ((x_113)) :extrapreds ((x_114)) :extrapreds ((x_115)) :extrafuns ((x_116 Real)) :extrapreds ((x_117)) :extrapreds ((x_118)) :extrafuns ((x_119 Real)) :extrafuns ((x_120 Real)) :extrafuns ((x_121 Real)) :extrapreds ((x_122)) :extrapreds ((x_123)) :extrafuns ((x_124 Real)) :extrafuns ((x_125 Real)) :extrafuns ((x_126 Real)) :extrafuns ((x_127 Real)) :extrapreds ((x_128)) :extrapreds ((x_129)) :extrapreds ((x_130)) :extrapreds ((x_131)) :extrapreds ((x_132)) :extrapreds ((x_133)) :extrafuns ((x_134 Real)) :extrapreds ((x_135)) :extrapreds ((x_136)) :extrafuns ((x_137 Real)) :extrafuns ((x_138 Real)) :extrafuns ((x_139 Real)) :extrapreds ((x_140)) :extrapreds ((x_141)) :extrafuns ((x_142 Real)) :extrafuns ((x_143 Real)) :extrafuns ((x_144 Real)) :extrafuns ((x_145 Real)) :formula (flet ($cvcl_22 (and (iff x_128 x_110) (iff x_129 x_111))) (flet ($cvcl_13 (not x_130)) (flet ($cvcl_15 (and $cvcl_13 x_131)) (flet ($cvcl_30 (and (iff x_132 x_114) (iff x_133 x_115))) (flet ($cvcl_9 (= x_124 1)) (flet ($cvcl_29 (= x_134 x_116)) (flet ($cvcl_11 (and (iff x_135 x_117) (iff x_136 x_118))) (flet ($cvcl_5 (= x_137 x_119)) (flet ($cvcl_26 (= x_134 0)) (flet ($cvcl_0 (= x_124 0)) (flet ($cvcl_20 (= x_138 x_120)) (flet ($cvcl_16 (= x_138 0)) (flet ($cvcl_24 (= x_139 x_121)) (flet ($cvcl_2 (not x_140)) (flet ($cvcl_4 (and $cvcl_2 x_141)) (flet ($cvcl_49 (and (iff x_110 x_92) (iff x_111 x_93))) (flet ($cvcl_42 (not x_112)) (flet ($cvcl_44 (and $cvcl_42 x_113)) (flet ($cvcl_55 (and (iff x_114 x_96) (iff x_115 x_97))) (flet ($cvcl_38 (= x_106 1)) (flet ($cvcl_54 (= x_116 x_98)) (flet ($cvcl_40 (and (iff x_117 x_99) (iff x_118 x_100))) (flet ($cvcl_36 (= x_119 x_101)) (flet ($cvcl_53 (= x_116 0)) (flet ($cvcl_31 (= x_106 0)) (flet ($cvcl_47 (= x_120 x_102)) (flet ($cvcl_45 (= x_120 0)) (flet ($cvcl_51 (= x_121 x_103)) (flet ($cvcl_33 (not x_122)) (flet ($cvcl_35 (and $cvcl_33 x_123)) (flet ($cvcl_74 (and (iff x_92 x_74) (iff x_93 x_75))) (flet ($cvcl_67 (not x_94)) (flet ($cvcl_69 (and $cvcl_67 x_95)) (flet ($cvcl_80 (and (iff x_96 x_78) (iff x_97 x_79))) (flet ($cvcl_63 (= x_88 1)) (flet ($cvcl_79 (= x_98 x_80)) (flet ($cvcl_65 (and (iff x_99 x_81) (iff x_100 x_82))) (flet ($cvcl_61 (= x_101 x_83)) (flet ($cvcl_78 (= x_98 0)) (flet ($cvcl_56 (= x_88 0)) (flet ($cvcl_72 (= x_102 x_84)) (flet ($cvcl_70 (= x_102 0)) (flet ($cvcl_76 (= x_103 x_85)) (flet ($cvcl_58 (not x_104)) (flet ($cvcl_60 (and $cvcl_58 x_105)) (flet ($cvcl_99 (and (iff x_74 x_56) (iff x_75 x_57))) (flet ($cvcl_92 (not x_76)) (flet ($cvcl_94 (and $cvcl_92 x_77)) (flet ($cvcl_105 (and (iff x_78 x_60) (iff x_79 x_61))) (flet ($cvcl_88 (= x_70 1)) (flet ($cvcl_104 (= x_80 x_62)) (flet ($cvcl_90 (and (iff x_81 x_63) (iff x_82 x_64))) (flet ($cvcl_86 (= x_83 x_65)) (flet ($cvcl_103 (= x_80 0)) (flet ($cvcl_81 (= x_70 0)) (flet ($cvcl_97 (= x_84 x_66)) (flet ($cvcl_95 (= x_84 0)) (flet ($cvcl_101 (= x_85 x_67)) (flet ($cvcl_83 (not x_86)) (flet ($cvcl_85 (and $cvcl_83 x_87)) (flet ($cvcl_124 (and (iff x_56 x_38) (iff x_57 x_39))) (flet ($cvcl_117 (not x_58)) (flet ($cvcl_119 (and $cvcl_117 x_59)) (flet ($cvcl_130 (and (iff x_60 x_42) (iff x_61 x_43))) (flet ($cvcl_113 (= x_52 1)) (flet ($cvcl_129 (= x_62 x_44)) (flet ($cvcl_115 (and (iff x_63 x_45) (iff x_64 x_46))) (flet ($cvcl_111 (= x_65 x_47)) (flet ($cvcl_128 (= x_62 0)) (flet ($cvcl_106 (= x_52 0)) (flet ($cvcl_122 (= x_66 x_48)) (flet ($cvcl_120 (= x_66 0)) (flet ($cvcl_126 (= x_67 x_49)) (flet ($cvcl_108 (not x_68)) (flet ($cvcl_110 (and $cvcl_108 x_69)) (flet ($cvcl_149 (and (iff x_38 x_14) (iff x_39 x_15))) (flet ($cvcl_142 (not x_40)) (flet ($cvcl_144 (and $cvcl_142 x_41)) (flet ($cvcl_155 (and (iff x_42 x_18) (iff x_43 x_19))) (flet ($cvcl_138 (= x_30 1)) (flet ($cvcl_154 (= x_44 x_21)) (flet ($cvcl_140 (and (iff x_45 x_22) (iff x_46 x_23))) (flet ($cvcl_136 (= x_47 x_24)) (flet ($cvcl_153 (= x_44 0)) (flet ($cvcl_131 (= x_30 0)) (flet ($cvcl_147 (= x_48 x_25)) (flet ($cvcl_145 (= x_48 0)) (flet ($cvcl_151 (= x_49 x_26)) (flet ($cvcl_133 (not x_50)) (flet ($cvcl_135 (and $cvcl_133 x_51)) (flet ($cvcl_172 (and (iff x_14 x_2) (iff x_15 x_3))) (flet ($cvcl_167 (not x_16)) (flet ($cvcl_169 (and $cvcl_167 x_17)) (flet ($cvcl_177 (and (iff x_18 x_4) (iff x_19 x_5))) (flet ($cvcl_164 (and (iff x_22 x_0) (iff x_23 x_1))) (flet ($cvcl_176 (= x_21 0)) (flet ($cvcl_158 (not x_20)) (flet ($cvcl_168 (= x_25 0)) (flet ($cvcl_175 (= x_26 x_27)) (flet ($cvcl_159 (not x_28)) (flet ($cvcl_161 (and $cvcl_159 x_29)) (flet ($cvcl_156 (not x_0)) (flet ($cvcl_157 (not x_1)) (flet ($cvcl_165 (not x_2)) (flet ($cvcl_166 (not x_3)) (flet ($cvcl_173 (not x_4)) (flet ($cvcl_174 (not x_5)) (flet ($cvcl_3 (not x_117)) (flet ($cvcl_1 (not x_118)) (flet ($cvcl_6 (not x_141)) (flet ($cvcl_8 (not x_136)) (flet ($cvcl_7 (not x_135)) (flet ($cvcl_14 (not x_110)) (flet ($cvcl_12 (not x_111)) (flet ($cvcl_19 (not x_129)) (flet ($cvcl_17 (not x_131)) (flet ($cvcl_18 (not x_128)) (flet ($cvcl_25 (not x_114)) (flet ($cvcl_23 (not x_115)) (flet ($cvcl_28 (not x_133)) (flet ($cvcl_27 (not x_132)) (flet ($cvcl_178 (or $cvcl_25 $cvcl_23 )) (flet ($cvcl_34 (not x_99)) (flet ($cvcl_32 (not x_100)) (flet ($cvcl_37 (not x_123)) (flet ($cvcl_43 (not x_92)) (flet ($cvcl_41 (not x_93)) (flet ($cvcl_46 (not x_113)) (flet ($cvcl_52 (not x_96)) (flet ($cvcl_50 (not x_97)) (flet ($cvcl_179 (or $cvcl_52 $cvcl_50 )) (flet ($cvcl_59 (not x_81)) (flet ($cvcl_57 (not x_82)) (flet ($cvcl_62 (not x_105)) (flet ($cvcl_68 (not x_74)) (flet ($cvcl_66 (not x_75)) (flet ($cvcl_71 (not x_95)) (flet ($cvcl_77 (not x_78)) (flet ($cvcl_75 (not x_79)) (flet ($cvcl_180 (or $cvcl_77 $cvcl_75 )) (flet ($cvcl_84 (not x_63)) (flet ($cvcl_82 (not x_64)) (flet ($cvcl_87 (not x_87)) (flet ($cvcl_93 (not x_56)) (flet ($cvcl_91 (not x_57)) (flet ($cvcl_96 (not x_77)) (flet ($cvcl_102 (not x_60)) (flet ($cvcl_100 (not x_61)) (flet ($cvcl_181 (or $cvcl_102 $cvcl_100 )) (flet ($cvcl_109 (not x_45)) (flet ($cvcl_107 (not x_46)) (flet ($cvcl_112 (not x_69)) (flet ($cvcl_118 (not x_38)) (flet ($cvcl_116 (not x_39)) (flet ($cvcl_121 (not x_59)) (flet ($cvcl_127 (not x_42)) (flet ($cvcl_125 (not x_43)) (flet ($cvcl_182 (or $cvcl_127 $cvcl_125 )) (flet ($cvcl_134 (not x_22)) (flet ($cvcl_132 (not x_23)) (flet ($cvcl_137 (not x_51)) (flet ($cvcl_143 (not x_14)) (flet ($cvcl_141 (not x_15)) (flet ($cvcl_146 (not x_41)) (flet ($cvcl_152 (not x_18)) (flet ($cvcl_150 (not x_19)) (flet ($cvcl_183 (or $cvcl_152 $cvcl_150 )) (flet ($cvcl_162 (not x_29)) (flet ($cvcl_160 (= x_24 0)) (flet ($cvcl_170 (not x_17)) (flet ($cvcl_184 (or $cvcl_173 $cvcl_174 )) (flet ($cvcl_10 (<= (+ x_119 x_12) 5)) (flet ($cvcl_21 (<= (+ x_120 x_12) 1)) (flet ($cvcl_39 (<= (+ x_101 x_11) 5)) (flet ($cvcl_48 (<= (+ x_102 x_11) 1)) (flet ($cvcl_64 (<= (+ x_83 x_10) 5)) (flet ($cvcl_73 (<= (+ x_84 x_10) 1)) (flet ($cvcl_89 (<= (+ x_65 x_9) 5)) (flet ($cvcl_98 (<= (+ x_66 x_9) 1)) (flet ($cvcl_114 (<= (+ x_47 x_8) 5)) (flet ($cvcl_123 (<= (+ x_48 x_8) 1)) (flet ($cvcl_139 (<= (+ x_24 x_7) 5)) (flet ($cvcl_148 (<= (+ x_25 x_7) 1)) (flet ($cvcl_163 (<= (+ 0 x_6) 5)) (flet ($cvcl_171 (<= (+ 0 x_6) 1)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_142 1) (>= x_142 0)) (<= x_124 1)) (>= x_124 0)) (<= x_106 1)) (>= x_106 0)) (<= x_88 1)) (>= x_88 0)) (<= x_70 1)) (>= x_70 0)) (<= x_52 1)) (>= x_52 0)) (<= x_30 1)) (>= x_30 0)) (and $cvcl_156 $cvcl_157)) (and $cvcl_165 $cvcl_166)) (and $cvcl_173 $cvcl_174)) (not (< x_13 0))) (not (< x_12 0))) (not (< x_11 0))) (not (< x_10 0))) (not (< x_9 0))) (not (< x_8 0))) (not (< x_7 0))) (not (< x_6 0))) (= x_142 (ite $cvcl_9 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_143 0) $cvcl_0) $cvcl_3) $cvcl_1) $cvcl_2) $cvcl_6) x_135) $cvcl_8) (= x_137 0)) (and (and (and (and (and (and (and (and (= x_143 1) $cvcl_0) x_117) $cvcl_1) (not (<= x_119 2))) $cvcl_4) $cvcl_7) x_136) $cvcl_5) ) (and (and (and (and (and (and (and (= x_143 2) $cvcl_0) $cvcl_3) x_118) $cvcl_4) x_135) x_136) $cvcl_5) ) (and (and (and (and (and (and (and (and (= x_143 3) $cvcl_0) x_117) x_118) x_140) $cvcl_6) $cvcl_7) $cvcl_8) $cvcl_5) ) (and (and (and (and (and (and (and (and (= x_143 4) $cvcl_9) (or (or $cvcl_3 x_118 ) $cvcl_10 )) (or (or x_117 $cvcl_1 ) $cvcl_10 )) (or (or $cvcl_3 $cvcl_1 ) $cvcl_10 )) (= x_137 (+ x_119 x_12))) (iff x_140 x_122)) (iff x_141 x_123)) $cvcl_11) ) (and (and (and (and (= x_143 5) $cvcl_0) $cvcl_5) $cvcl_4) $cvcl_11) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_144 0) $cvcl_0) $cvcl_14) $cvcl_12) $cvcl_2) $cvcl_6) $cvcl_15) x_128) $cvcl_19) $cvcl_16) (and (and (and (and (and (and (and (and (and (= x_144 1) $cvcl_0) x_110) $cvcl_12) (= x_120 1)) $cvcl_13) $cvcl_17) $cvcl_18) x_129) $cvcl_20) ) (and (and (and (and (and (and (and (and (and (= x_144 2) $cvcl_0) $cvcl_14) x_111) x_140) $cvcl_6) $cvcl_15) x_128) x_129) $cvcl_16) ) (and (and (and (and (and (and (and (and (= x_144 3) $cvcl_0) x_110) x_111) x_130) $cvcl_17) $cvcl_18) $cvcl_19) $cvcl_20) ) (and (and (and (and (and (and (and (= x_144 4) $cvcl_9) (or (or $cvcl_14 x_111 ) $cvcl_21 )) (or (or $cvcl_14 $cvcl_12 ) $cvcl_21 )) (= x_138 (+ x_120 x_12))) (iff x_130 x_112)) (iff x_131 x_113)) $cvcl_22) ) (and (and (and (and (and (and (= x_144 5) $cvcl_0) $cvcl_2) x_141) $cvcl_20) $cvcl_15) $cvcl_22) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_145 0) $cvcl_0) $cvcl_25) $cvcl_23) $cvcl_13) $cvcl_17) x_132) $cvcl_28) $cvcl_26) $cvcl_24) (and (and (and (and (and (and (and (= x_145 1) $cvcl_0) x_114) $cvcl_23) $cvcl_27) x_133) $cvcl_24) $cvcl_29) ) (and (and (and (and (and (and (and (and (and (= x_145 2) $cvcl_0) $cvcl_25) x_115) x_130) $cvcl_17) x_132) x_133) $cvcl_26) $cvcl_24) ) (and (and (and (and (and (and (and (and (= x_145 3) $cvcl_0) x_114) x_115) (not (< x_116 1))) $cvcl_27) $cvcl_28) $cvcl_24) $cvcl_29) ) (and (and (and (and (and (and (= x_145 4) $cvcl_9) (or (or $cvcl_25 x_115 ) (<= (+ x_116 x_12) 1) )) (or $cvcl_178 (<= (+ x_116 x_12) 2) )) (= x_134 (+ x_116 x_12))) $cvcl_30) $cvcl_24) ) (and (and (and (and (and (and (= x_145 5) $cvcl_0) $cvcl_13) x_131) $cvcl_29) $cvcl_30) $cvcl_24) )) (= x_124 (ite $cvcl_38 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_125 0) $cvcl_31) $cvcl_34) $cvcl_32) $cvcl_33) $cvcl_37) x_117) $cvcl_1) (= x_119 0)) (and (and (and (and (and (and (and (and (= x_125 1) $cvcl_31) x_99) $cvcl_32) (not (<= x_101 2))) $cvcl_35) $cvcl_3) x_118) $cvcl_36) ) (and (and (and (and (and (and (and (= x_125 2) $cvcl_31) $cvcl_34) x_100) $cvcl_35) x_117) x_118) $cvcl_36) ) (and (and (and (and (and (and (and (and (= x_125 3) $cvcl_31) x_99) x_100) x_122) $cvcl_37) $cvcl_3) $cvcl_1) $cvcl_36) ) (and (and (and (and (and (and (and (and (= x_125 4) $cvcl_38) (or (or $cvcl_34 x_100 ) $cvcl_39 )) (or (or x_99 $cvcl_32 ) $cvcl_39 )) (or (or $cvcl_34 $cvcl_32 ) $cvcl_39 )) (= x_119 (+ x_101 x_11))) (iff x_122 x_104)) (iff x_123 x_105)) $cvcl_40) ) (and (and (and (and (= x_125 5) $cvcl_31) $cvcl_36) $cvcl_35) $cvcl_40) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_126 0) $cvcl_31) $cvcl_43) $cvcl_41) $cvcl_33) $cvcl_37) $cvcl_44) x_110) $cvcl_12) $cvcl_45) (and (and (and (and (and (and (and (and (and (= x_126 1) $cvcl_31) x_92) $cvcl_41) (= x_102 1)) $cvcl_42) $cvcl_46) $cvcl_14) x_111) $cvcl_47) ) (and (and (and (and (and (and (and (and (and (= x_126 2) $cvcl_31) $cvcl_43) x_93) x_122) $cvcl_37) $cvcl_44) x_110) x_111) $cvcl_45) ) (and (and (and (and (and (and (and (and (= x_126 3) $cvcl_31) x_92) x_93) x_112) $cvcl_46) $cvcl_14) $cvcl_12) $cvcl_47) ) (and (and (and (and (and (and (and (= x_126 4) $cvcl_38) (or (or $cvcl_43 x_93 ) $cvcl_48 )) (or (or $cvcl_43 $cvcl_41 ) $cvcl_48 )) (= x_120 (+ x_102 x_11))) (iff x_112 x_94)) (iff x_113 x_95)) $cvcl_49) ) (and (and (and (and (and (and (= x_126 5) $cvcl_31) $cvcl_33) x_123) $cvcl_47) $cvcl_44) $cvcl_49) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_127 0) $cvcl_31) $cvcl_52) $cvcl_50) $cvcl_42) $cvcl_46) x_114) $cvcl_23) $cvcl_53) $cvcl_51) (and (and (and (and (and (and (and (= x_127 1) $cvcl_31) x_96) $cvcl_50) $cvcl_25) x_115) $cvcl_51) $cvcl_54) ) (and (and (and (and (and (and (and (and (and (= x_127 2) $cvcl_31) $cvcl_52) x_97) x_112) $cvcl_46) x_114) x_115) $cvcl_53) $cvcl_51) ) (and (and (and (and (and (and (and (and (= x_127 3) $cvcl_31) x_96) x_97) (not (< x_98 1))) $cvcl_25) $cvcl_23) $cvcl_51) $cvcl_54) ) (and (and (and (and (and (and (= x_127 4) $cvcl_38) (or (or $cvcl_52 x_97 ) (<= (+ x_98 x_11) 1) )) (or $cvcl_179 (<= (+ x_98 x_11) 2) )) (= x_116 (+ x_98 x_11))) $cvcl_55) $cvcl_51) ) (and (and (and (and (and (and (= x_127 5) $cvcl_31) $cvcl_42) x_113) $cvcl_54) $cvcl_55) $cvcl_51) )) (= x_106 (ite $cvcl_63 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_107 0) $cvcl_56) $cvcl_59) $cvcl_57) $cvcl_58) $cvcl_62) x_99) $cvcl_32) (= x_101 0)) (and (and (and (and (and (and (and (and (= x_107 1) $cvcl_56) x_81) $cvcl_57) (not (<= x_83 2))) $cvcl_60) $cvcl_34) x_100) $cvcl_61) ) (and (and (and (and (and (and (and (= x_107 2) $cvcl_56) $cvcl_59) x_82) $cvcl_60) x_99) x_100) $cvcl_61) ) (and (and (and (and (and (and (and (and (= x_107 3) $cvcl_56) x_81) x_82) x_104) $cvcl_62) $cvcl_34) $cvcl_32) $cvcl_61) ) (and (and (and (and (and (and (and (and (= x_107 4) $cvcl_63) (or (or $cvcl_59 x_82 ) $cvcl_64 )) (or (or x_81 $cvcl_57 ) $cvcl_64 )) (or (or $cvcl_59 $cvcl_57 ) $cvcl_64 )) (= x_101 (+ x_83 x_10))) (iff x_104 x_86)) (iff x_105 x_87)) $cvcl_65) ) (and (and (and (and (= x_107 5) $cvcl_56) $cvcl_61) $cvcl_60) $cvcl_65) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_108 0) $cvcl_56) $cvcl_68) $cvcl_66) $cvcl_58) $cvcl_62) $cvcl_69) x_92) $cvcl_41) $cvcl_70) (and (and (and (and (and (and (and (and (and (= x_108 1) $cvcl_56) x_74) $cvcl_66) (= x_84 1)) $cvcl_67) $cvcl_71) $cvcl_43) x_93) $cvcl_72) ) (and (and (and (and (and (and (and (and (and (= x_108 2) $cvcl_56) $cvcl_68) x_75) x_104) $cvcl_62) $cvcl_69) x_92) x_93) $cvcl_70) ) (and (and (and (and (and (and (and (and (= x_108 3) $cvcl_56) x_74) x_75) x_94) $cvcl_71) $cvcl_43) $cvcl_41) $cvcl_72) ) (and (and (and (and (and (and (and (= x_108 4) $cvcl_63) (or (or $cvcl_68 x_75 ) $cvcl_73 )) (or (or $cvcl_68 $cvcl_66 ) $cvcl_73 )) (= x_102 (+ x_84 x_10))) (iff x_94 x_76)) (iff x_95 x_77)) $cvcl_74) ) (and (and (and (and (and (and (= x_108 5) $cvcl_56) $cvcl_58) x_105) $cvcl_72) $cvcl_69) $cvcl_74) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_109 0) $cvcl_56) $cvcl_77) $cvcl_75) $cvcl_67) $cvcl_71) x_96) $cvcl_50) $cvcl_78) $cvcl_76) (and (and (and (and (and (and (and (= x_109 1) $cvcl_56) x_78) $cvcl_75) $cvcl_52) x_97) $cvcl_76) $cvcl_79) ) (and (and (and (and (and (and (and (and (and (= x_109 2) $cvcl_56) $cvcl_77) x_79) x_94) $cvcl_71) x_96) x_97) $cvcl_78) $cvcl_76) ) (and (and (and (and (and (and (and (and (= x_109 3) $cvcl_56) x_78) x_79) (not (< x_80 1))) $cvcl_52) $cvcl_50) $cvcl_76) $cvcl_79) ) (and (and (and (and (and (and (= x_109 4) $cvcl_63) (or (or $cvcl_77 x_79 ) (<= (+ x_80 x_10) 1) )) (or $cvcl_180 (<= (+ x_80 x_10) 2) )) (= x_98 (+ x_80 x_10))) $cvcl_80) $cvcl_76) ) (and (and (and (and (and (and (= x_109 5) $cvcl_56) $cvcl_67) x_95) $cvcl_79) $cvcl_80) $cvcl_76) )) (= x_88 (ite $cvcl_88 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_89 0) $cvcl_81) $cvcl_84) $cvcl_82) $cvcl_83) $cvcl_87) x_81) $cvcl_57) (= x_83 0)) (and (and (and (and (and (and (and (and (= x_89 1) $cvcl_81) x_63) $cvcl_82) (not (<= x_65 2))) $cvcl_85) $cvcl_59) x_82) $cvcl_86) ) (and (and (and (and (and (and (and (= x_89 2) $cvcl_81) $cvcl_84) x_64) $cvcl_85) x_81) x_82) $cvcl_86) ) (and (and (and (and (and (and (and (and (= x_89 3) $cvcl_81) x_63) x_64) x_86) $cvcl_87) $cvcl_59) $cvcl_57) $cvcl_86) ) (and (and (and (and (and (and (and (and (= x_89 4) $cvcl_88) (or (or $cvcl_84 x_64 ) $cvcl_89 )) (or (or x_63 $cvcl_82 ) $cvcl_89 )) (or (or $cvcl_84 $cvcl_82 ) $cvcl_89 )) (= x_83 (+ x_65 x_9))) (iff x_86 x_68)) (iff x_87 x_69)) $cvcl_90) ) (and (and (and (and (= x_89 5) $cvcl_81) $cvcl_86) $cvcl_85) $cvcl_90) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_90 0) $cvcl_81) $cvcl_93) $cvcl_91) $cvcl_83) $cvcl_87) $cvcl_94) x_74) $cvcl_66) $cvcl_95) (and (and (and (and (and (and (and (and (and (= x_90 1) $cvcl_81) x_56) $cvcl_91) (= x_66 1)) $cvcl_92) $cvcl_96) $cvcl_68) x_75) $cvcl_97) ) (and (and (and (and (and (and (and (and (and (= x_90 2) $cvcl_81) $cvcl_93) x_57) x_86) $cvcl_87) $cvcl_94) x_74) x_75) $cvcl_95) ) (and (and (and (and (and (and (and (and (= x_90 3) $cvcl_81) x_56) x_57) x_76) $cvcl_96) $cvcl_68) $cvcl_66) $cvcl_97) ) (and (and (and (and (and (and (and (= x_90 4) $cvcl_88) (or (or $cvcl_93 x_57 ) $cvcl_98 )) (or (or $cvcl_93 $cvcl_91 ) $cvcl_98 )) (= x_84 (+ x_66 x_9))) (iff x_76 x_58)) (iff x_77 x_59)) $cvcl_99) ) (and (and (and (and (and (and (= x_90 5) $cvcl_81) $cvcl_83) x_87) $cvcl_97) $cvcl_94) $cvcl_99) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_91 0) $cvcl_81) $cvcl_102) $cvcl_100) $cvcl_92) $cvcl_96) x_78) $cvcl_75) $cvcl_103) $cvcl_101) (and (and (and (and (and (and (and (= x_91 1) $cvcl_81) x_60) $cvcl_100) $cvcl_77) x_79) $cvcl_101) $cvcl_104) ) (and (and (and (and (and (and (and (and (and (= x_91 2) $cvcl_81) $cvcl_102) x_61) x_76) $cvcl_96) x_78) x_79) $cvcl_103) $cvcl_101) ) (and (and (and (and (and (and (and (and (= x_91 3) $cvcl_81) x_60) x_61) (not (< x_62 1))) $cvcl_77) $cvcl_75) $cvcl_101) $cvcl_104) ) (and (and (and (and (and (and (= x_91 4) $cvcl_88) (or (or $cvcl_102 x_61 ) (<= (+ x_62 x_9) 1) )) (or $cvcl_181 (<= (+ x_62 x_9) 2) )) (= x_80 (+ x_62 x_9))) $cvcl_105) $cvcl_101) ) (and (and (and (and (and (and (= x_91 5) $cvcl_81) $cvcl_92) x_77) $cvcl_104) $cvcl_105) $cvcl_101) )) (= x_70 (ite $cvcl_113 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_71 0) $cvcl_106) $cvcl_109) $cvcl_107) $cvcl_108) $cvcl_112) x_63) $cvcl_82) (= x_65 0)) (and (and (and (and (and (and (and (and (= x_71 1) $cvcl_106) x_45) $cvcl_107) (not (<= x_47 2))) $cvcl_110) $cvcl_84) x_64) $cvcl_111) ) (and (and (and (and (and (and (and (= x_71 2) $cvcl_106) $cvcl_109) x_46) $cvcl_110) x_63) x_64) $cvcl_111) ) (and (and (and (and (and (and (and (and (= x_71 3) $cvcl_106) x_45) x_46) x_68) $cvcl_112) $cvcl_84) $cvcl_82) $cvcl_111) ) (and (and (and (and (and (and (and (and (= x_71 4) $cvcl_113) (or (or $cvcl_109 x_46 ) $cvcl_114 )) (or (or x_45 $cvcl_107 ) $cvcl_114 )) (or (or $cvcl_109 $cvcl_107 ) $cvcl_114 )) (= x_65 (+ x_47 x_8))) (iff x_68 x_50)) (iff x_69 x_51)) $cvcl_115) ) (and (and (and (and (= x_71 5) $cvcl_106) $cvcl_111) $cvcl_110) $cvcl_115) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_72 0) $cvcl_106) $cvcl_118) $cvcl_116) $cvcl_108) $cvcl_112) $cvcl_119) x_56) $cvcl_91) $cvcl_120) (and (and (and (and (and (and (and (and (and (= x_72 1) $cvcl_106) x_38) $cvcl_116) (= x_48 1)) $cvcl_117) $cvcl_121) $cvcl_93) x_57) $cvcl_122) ) (and (and (and (and (and (and (and (and (and (= x_72 2) $cvcl_106) $cvcl_118) x_39) x_68) $cvcl_112) $cvcl_119) x_56) x_57) $cvcl_120) ) (and (and (and (and (and (and (and (and (= x_72 3) $cvcl_106) x_38) x_39) x_58) $cvcl_121) $cvcl_93) $cvcl_91) $cvcl_122) ) (and (and (and (and (and (and (and (= x_72 4) $cvcl_113) (or (or $cvcl_118 x_39 ) $cvcl_123 )) (or (or $cvcl_118 $cvcl_116 ) $cvcl_123 )) (= x_66 (+ x_48 x_8))) (iff x_58 x_40)) (iff x_59 x_41)) $cvcl_124) ) (and (and (and (and (and (and (= x_72 5) $cvcl_106) $cvcl_108) x_69) $cvcl_122) $cvcl_119) $cvcl_124) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_73 0) $cvcl_106) $cvcl_127) $cvcl_125) $cvcl_117) $cvcl_121) x_60) $cvcl_100) $cvcl_128) $cvcl_126) (and (and (and (and (and (and (and (= x_73 1) $cvcl_106) x_42) $cvcl_125) $cvcl_102) x_61) $cvcl_126) $cvcl_129) ) (and (and (and (and (and (and (and (and (and (= x_73 2) $cvcl_106) $cvcl_127) x_43) x_58) $cvcl_121) x_60) x_61) $cvcl_128) $cvcl_126) ) (and (and (and (and (and (and (and (and (= x_73 3) $cvcl_106) x_42) x_43) (not (< x_44 1))) $cvcl_102) $cvcl_100) $cvcl_126) $cvcl_129) ) (and (and (and (and (and (and (= x_73 4) $cvcl_113) (or (or $cvcl_127 x_43 ) (<= (+ x_44 x_8) 1) )) (or $cvcl_182 (<= (+ x_44 x_8) 2) )) (= x_62 (+ x_44 x_8))) $cvcl_130) $cvcl_126) ) (and (and (and (and (and (and (= x_73 5) $cvcl_106) $cvcl_117) x_59) $cvcl_129) $cvcl_130) $cvcl_126) )) (= x_52 (ite $cvcl_138 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_53 0) $cvcl_131) $cvcl_134) $cvcl_132) $cvcl_133) $cvcl_137) x_45) $cvcl_107) (= x_47 0)) (and (and (and (and (and (and (and (and (= x_53 1) $cvcl_131) x_22) $cvcl_132) (not (<= x_24 2))) $cvcl_135) $cvcl_109) x_46) $cvcl_136) ) (and (and (and (and (and (and (and (= x_53 2) $cvcl_131) $cvcl_134) x_23) $cvcl_135) x_45) x_46) $cvcl_136) ) (and (and (and (and (and (and (and (and (= x_53 3) $cvcl_131) x_22) x_23) x_50) $cvcl_137) $cvcl_109) $cvcl_107) $cvcl_136) ) (and (and (and (and (and (and (and (and (= x_53 4) $cvcl_138) (or (or $cvcl_134 x_23 ) $cvcl_139 )) (or (or x_22 $cvcl_132 ) $cvcl_139 )) (or (or $cvcl_134 $cvcl_132 ) $cvcl_139 )) (= x_47 (+ x_24 x_7))) (iff x_50 x_28)) (iff x_51 x_29)) $cvcl_140) ) (and (and (and (and (= x_53 5) $cvcl_131) $cvcl_136) $cvcl_135) $cvcl_140) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_54 0) $cvcl_131) $cvcl_143) $cvcl_141) $cvcl_133) $cvcl_137) $cvcl_144) x_38) $cvcl_116) $cvcl_145) (and (and (and (and (and (and (and (and (and (= x_54 1) $cvcl_131) x_14) $cvcl_141) (= x_25 1)) $cvcl_142) $cvcl_146) $cvcl_118) x_39) $cvcl_147) ) (and (and (and (and (and (and (and (and (and (= x_54 2) $cvcl_131) $cvcl_143) x_15) x_50) $cvcl_137) $cvcl_144) x_38) x_39) $cvcl_145) ) (and (and (and (and (and (and (and (and (= x_54 3) $cvcl_131) x_14) x_15) x_40) $cvcl_146) $cvcl_118) $cvcl_116) $cvcl_147) ) (and (and (and (and (and (and (and (= x_54 4) $cvcl_138) (or (or $cvcl_143 x_15 ) $cvcl_148 )) (or (or $cvcl_143 $cvcl_141 ) $cvcl_148 )) (= x_48 (+ x_25 x_7))) (iff x_40 x_16)) (iff x_41 x_17)) $cvcl_149) ) (and (and (and (and (and (and (= x_54 5) $cvcl_131) $cvcl_133) x_51) $cvcl_147) $cvcl_144) $cvcl_149) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_55 0) $cvcl_131) $cvcl_152) $cvcl_150) $cvcl_142) $cvcl_146) x_42) $cvcl_125) $cvcl_153) $cvcl_151) (and (and (and (and (and (and (and (= x_55 1) $cvcl_131) x_18) $cvcl_150) $cvcl_127) x_43) $cvcl_151) $cvcl_154) ) (and (and (and (and (and (and (and (and (and (= x_55 2) $cvcl_131) $cvcl_152) x_19) x_40) $cvcl_146) x_42) x_43) $cvcl_153) $cvcl_151) ) (and (and (and (and (and (and (and (and (= x_55 3) $cvcl_131) x_18) x_19) (not (< x_21 1))) $cvcl_127) $cvcl_125) $cvcl_151) $cvcl_154) ) (and (and (and (and (and (and (= x_55 4) $cvcl_138) (or (or $cvcl_152 x_19 ) (<= (+ x_21 x_7) 1) )) (or $cvcl_183 (<= (+ x_21 x_7) 2) )) (= x_44 (+ x_21 x_7))) $cvcl_155) $cvcl_151) ) (and (and (and (and (and (and (= x_55 5) $cvcl_131) $cvcl_142) x_41) $cvcl_154) $cvcl_155) $cvcl_151) )) (= x_30 (ite x_20 0 1))) (or (or (or (or (or (and (and (and (and (and (and (and (and (= x_31 0) $cvcl_158) $cvcl_156) $cvcl_157) $cvcl_159) $cvcl_162) x_22) $cvcl_132) $cvcl_160) (and (and (and (and (and (and (and (and (= x_31 1) $cvcl_158) x_0) $cvcl_157) (not (>= 2 0))) $cvcl_161) $cvcl_134) x_23) $cvcl_160) ) (and (and (and (and (and (and (and (= x_31 2) $cvcl_158) $cvcl_156) x_1) $cvcl_161) x_22) x_23) $cvcl_160) ) (and (and (and (and (and (and (and (and (= x_31 3) $cvcl_158) x_0) x_1) x_28) $cvcl_162) $cvcl_134) $cvcl_132) $cvcl_160) ) (and (and (and (and (and (and (and (and (= x_31 4) x_20) (or (or $cvcl_156 x_1 ) $cvcl_163 )) (or (or x_0 $cvcl_157 ) $cvcl_163 )) (or (or $cvcl_156 $cvcl_157 ) $cvcl_163 )) (= x_24 (+ 0 x_6))) (iff x_28 x_32)) (iff x_29 x_33)) $cvcl_164) ) (and (and (and (and (= x_31 5) $cvcl_158) $cvcl_160) $cvcl_161) $cvcl_164) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_34 0) $cvcl_158) $cvcl_165) $cvcl_166) $cvcl_159) $cvcl_162) $cvcl_169) x_14) $cvcl_141) $cvcl_168) (and (and (and (and (and (and (and (and (and (= x_34 1) $cvcl_158) x_2) $cvcl_166) (= 0 1)) $cvcl_167) $cvcl_170) $cvcl_143) x_15) $cvcl_168) ) (and (and (and (and (and (and (and (and (and (= x_34 2) $cvcl_158) $cvcl_165) x_3) x_28) $cvcl_162) $cvcl_169) x_14) x_15) $cvcl_168) ) (and (and (and (and (and (and (and (and (= x_34 3) $cvcl_158) x_2) x_3) x_16) $cvcl_170) $cvcl_143) $cvcl_141) $cvcl_168) ) (and (and (and (and (and (and (and (= x_34 4) x_20) (or (or $cvcl_165 x_3 ) $cvcl_171 )) (or (or $cvcl_165 $cvcl_166 ) $cvcl_171 )) (= x_25 (+ 0 x_6))) (iff x_16 x_35)) (iff x_17 x_36)) $cvcl_172) ) (and (and (and (and (and (and (= x_34 5) $cvcl_158) $cvcl_159) x_29) $cvcl_168) $cvcl_169) $cvcl_172) )) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_37 0) $cvcl_158) $cvcl_173) $cvcl_174) $cvcl_167) $cvcl_170) x_18) $cvcl_150) $cvcl_176) $cvcl_175) (and (and (and (and (and (and (and (= x_37 1) $cvcl_158) x_4) $cvcl_174) $cvcl_152) x_19) $cvcl_175) $cvcl_176) ) (and (and (and (and (and (and (and (and (and (= x_37 2) $cvcl_158) $cvcl_173) x_5) x_16) $cvcl_170) x_18) x_19) $cvcl_176) $cvcl_175) ) (and (and (and (and (and (and (and (and (= x_37 3) $cvcl_158) x_4) x_5) (not (> 1 0))) $cvcl_152) $cvcl_150) $cvcl_175) $cvcl_176) ) (and (and (and (and (and (and (= x_37 4) x_20) (or (or $cvcl_173 x_5 ) $cvcl_171 )) (or $cvcl_184 (<= (+ 0 x_6) 2) )) (= x_21 (+ 0 x_6))) $cvcl_177) $cvcl_175) ) (and (and (and (and (and (and (= x_37 5) $cvcl_158) $cvcl_167) x_17) $cvcl_176) $cvcl_177) $cvcl_175) )) (or (or (or (or (or (or (or (and (and $cvcl_7 x_136) (or $cvcl_27 $cvcl_28 )) (and (and $cvcl_3 x_118) $cvcl_178) ) (and (and $cvcl_34 x_100) $cvcl_179) ) (and (and $cvcl_59 x_82) $cvcl_180) ) (and (and $cvcl_84 x_64) $cvcl_181) ) (and (and $cvcl_109 x_46) $cvcl_182) ) (and (and $cvcl_134 x_23) $cvcl_183) ) (and (and $cvcl_156 x_1) $cvcl_184) )) (or $cvcl_170 $cvcl_167 )) (or $cvcl_162 $cvcl_159 )) (or (not x_33) (not x_32) )) (or (not x_36) (not x_35) )) (or $cvcl_146 $cvcl_142 )) (or $cvcl_137 $cvcl_133 )) (or $cvcl_121 $cvcl_117 )) (or $cvcl_112 $cvcl_108 )) (or $cvcl_96 $cvcl_92 )) (or $cvcl_87 $cvcl_83 )) (or $cvcl_71 $cvcl_67 )) (or $cvcl_62 $cvcl_58 )) (or $cvcl_46 $cvcl_42 )) (or $cvcl_37 $cvcl_33 )) (or $cvcl_17 $cvcl_13 )) (or $cvcl_6 $cvcl_2 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )