(benchmark reint_to_least.induction.smt
  :source {
The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unsat
:category { industrial }
:difficulty { 0 }
  :logic QF_LRA
  
  :extrafuns ((x_0 Real))
  :extrafuns ((x_1 Real))
  :extrafuns ((x_2 Real))
  :extrafuns ((x_3 Real))
  :extrafuns ((x_4 Real))
  :extrafuns ((x_5 Real))
  :extrafuns ((x_6 Real))
  :extrafuns ((x_7 Real))
  :extrafuns ((x_8 Real))
  :extrafuns ((x_9 Real))
  :extrapreds ((x_10))
  :extrapreds ((x_11))
  :extrapreds ((x_12))
  :extrafuns ((x_13 Real))
  :extrapreds ((x_14))
  :extrafuns ((x_15 Real))
  :extrapreds ((x_16))
  :extrafuns ((x_17 Real))
  :extrafuns ((x_18 Real))
  :extrapreds ((x_19))
  :extrapreds ((x_20))
  :extrapreds ((x_21))
  :extrafuns ((x_22 Real))
  :extrapreds ((x_23))
  :extrafuns ((x_24 Real))
  :extrapreds ((x_25))
  :extrafuns ((x_26 Real))
  :extrapreds ((x_27))
  :extrapreds ((x_28))
  :extrapreds ((x_29))
  :extrafuns ((x_30 Real))
  :extrapreds ((x_31))
  :extrafuns ((x_32 Real))
  :extrafuns ((x_33 Real))
  :extrapreds ((x_34))
  :extrafuns ((x_35 Real))
  :extrafuns ((x_36 Real))
  :extrafuns ((x_37 Real))
  :extrafuns ((x_38 Real))
  :extrafuns ((x_39 Real))
  :extrafuns ((x_40 Real))
  :extrapreds ((x_41))
  :extrapreds ((x_42))
  :extrapreds ((x_43))
  :extrapreds ((x_44))
  :extrapreds ((x_45))
  :extrapreds ((x_46))
  :extrapreds ((x_47))
  :extrapreds ((x_48))
  :extrafuns ((x_49 Real))
  :extrafuns ((x_50 Real))
  :extrafuns ((x_51 Real))
  :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))
  :extrafuns ((x_63 Real))
  :extrafuns ((x_64 Real))
  :extrafuns ((x_65 Real))
  :extrafuns ((x_66 Real))
  :extrafuns ((x_67 Real))
  :extrafuns ((x_68 Real))
  :extrapreds ((x_69))
  :extrapreds ((x_70))
  :extrapreds ((x_71))
  :extrapreds ((x_72))
  :extrapreds ((x_73))
  :extrafuns ((x_74 Real))
  :extrafuns ((x_75 Real))
  :extrafuns ((x_76 Real))
  :extrafuns ((x_77 Real))
  :extrapreds ((x_78))
  :extrapreds ((x_79))
  :extrapreds ((x_80))
  :extrafuns ((x_81 Real))
  :extrafuns ((x_82 Real))
  :extrafuns ((x_83 Real))
  :extrafuns ((x_84 Real))
  :extrafuns ((x_85 Real))
  :extrafuns ((x_86 Real))
  :extrapreds ((x_87))
  :formula
(flet ($cvcl_14 x_10) (flet ($cvcl_15 x_11) (flet ($cvcl_16 x_12) (flet ($cvcl_7 x_19) (flet ($cvcl_8 x_20) (flet ($cvcl_9 x_21) (flet ($cvcl_0 x_27) (flet ($cvcl_1 x_28) (flet ($cvcl_2 x_29) (let (?cvcl_132 (+ x_18 x_0)) (flet ($cvcl_181 (<= x_1 x_5)) (flet ($cvcl_160 (iff x_19 x_10)) (flet ($cvcl_101 (= x_22 0)) (flet ($cvcl_116 $cvcl_101) (flet ($cvcl_117 (< x_1 x_40)) (flet ($cvcl_144 (= x_5 x_1)) (flet ($cvcl_168 $cvcl_144) (flet ($cvcl_161 (= x_22 2)) (flet ($cvcl_169 $cvcl_161) (flet ($cvcl_171 (iff x_41 x_42)) (flet ($cvcl_172 (and (iff x_43 x_44) (iff x_45 x_46))) (flet ($cvcl_158 (iff x_47 x_48)) (flet ($cvcl_159 (and (iff x_23 x_14) (iff x_25 x_16))) (flet ($cvcl_173 (= x_49 x_50)) (flet ($cvcl_174 (and (= x_51 x_52) (= x_53 x_54))) (flet ($cvcl_127 (= x_55 x_40)) (flet ($cvcl_157 (iff x_20 x_11)) (flet ($cvcl_155 (iff x_56 x_57)) (flet ($cvcl_156 (and (iff x_58 x_59) (iff x_60 x_61))) (flet ($cvcl_175 (iff x_21 x_12)) (let (?cvcl_183 (- x_6 x_18)) (flet ($cvcl_102 (= x_22 1)) (flet ($cvcl_148 $cvcl_102) (let (?cvcl_152 (+ x_0 x_18)) (flet ($cvcl_147 (<= x_2 x_5)) (flet ($cvcl_154 (iff x_41 (or x_42  (and $cvcl_147 x_57) ))) (flet ($cvcl_134 (<= x_15 ?cvcl_132)) (flet ($cvcl_136 (<= x_17 ?cvcl_132)) (flet ($cvcl_128 (<= x_15 x_0)) (flet ($cvcl_133 $cvcl_128) (flet ($cvcl_130 (<= x_17 x_0)) (flet ($cvcl_135 $cvcl_130) (flet ($cvcl_129 (not x_44)) (flet ($cvcl_139 $cvcl_129) (flet ($cvcl_162 (< x_15 x_1)) (flet ($cvcl_163 (= x_5 x_15)) (flet ($cvcl_131 (not x_46)) (flet ($cvcl_141 $cvcl_131) (flet ($cvcl_164 (< x_17 x_1)) (flet ($cvcl_165 (= x_5 x_17)) (flet ($cvcl_120 (not x_42)) (flet ($cvcl_143 $cvcl_120) (flet ($cvcl_184 (not $cvcl_181)) (flet ($cvcl_138 (not x_59)) (flet ($cvcl_140 (not x_61)) (flet ($cvcl_142 (not x_57)) (flet ($cvcl_145 (and (not $cvcl_128) (<= x_15 x_5))) (flet ($cvcl_146 (and (not $cvcl_130) (<= x_17 x_5))) (flet ($cvcl_153 (and (iff x_43 (or x_44  (and $cvcl_145 x_59) )) (iff x_45 (or x_46  (and $cvcl_146 x_61) )))) (flet ($cvcl_137 (<= x_2 ?cvcl_132)) (flet ($cvcl_166 (< x_2 x_1)) (flet ($cvcl_167 (= x_5 x_2)) (flet ($cvcl_170 (<= (ite x_48 (ite x_16 (ite x_14 3 2) x_62) (ite x_16 x_62 (ite x_14 1 0))) (* (* (ite x_42 (ite x_46 (ite x_44 0 1) x_63) (ite x_46 x_63 (ite x_44 2 3))) 1) (/ 1 2)))) (flet ($cvcl_189 $cvcl_147) (flet ($cvcl_149 (not $cvcl_134)) (flet ($cvcl_150 (not $cvcl_136)) (flet ($cvcl_21 (and (not (<= x_2 x_0)) $cvcl_147)) (flet ($cvcl_22 $cvcl_21) (flet ($cvcl_25 (and (not (<= x_3 x_0)) (<= x_3 x_5))) (flet ($cvcl_23 $cvcl_25) (flet ($cvcl_26 $cvcl_21) (flet ($cvcl_27 $cvcl_25) (flet ($cvcl_151 (not $cvcl_137)) (let (?cvcl_56 (+ x_18 x_5)) (flet ($cvcl_106 (<= x_6 x_32)) (flet ($cvcl_85 (iff x_27 x_19)) (flet ($cvcl_35 (= x_30 0)) (flet ($cvcl_39 $cvcl_35) (flet ($cvcl_40 (< x_6 x_55)) (flet ($cvcl_69 (= x_32 x_6)) (flet ($cvcl_93 $cvcl_69) (flet ($cvcl_86 (= x_30 2)) (flet ($cvcl_94 $cvcl_86) (flet ($cvcl_96 (iff x_70 x_41)) (flet ($cvcl_97 (and (iff x_71 x_43) (iff x_72 x_45))) (flet ($cvcl_83 (iff x_73 x_47)) (flet ($cvcl_84 (and (iff x_31 x_23) (iff x_34 x_25))) (flet ($cvcl_98 (= x_74 x_49)) (flet ($cvcl_99 (and (= x_75 x_51) (= x_76 x_53))) (flet ($cvcl_50 (= x_77 x_55)) (flet ($cvcl_82 (iff x_28 x_20)) (flet ($cvcl_80 (iff x_78 x_56)) (flet ($cvcl_81 (and (iff x_79 x_58) (iff x_80 x_60))) (flet ($cvcl_100 (iff x_29 x_21)) (let (?cvcl_108 (- x_36 x_18)) (flet ($cvcl_51 (= x_30 1)) (flet ($cvcl_73 $cvcl_51) (let (?cvcl_77 (+ x_5 x_18)) (flet ($cvcl_72 (<= x_7 x_32)) (flet ($cvcl_79 (iff x_70 (or x_41  (and $cvcl_72 x_56) ))) (flet ($cvcl_59 (<= x_24 ?cvcl_56)) (flet ($cvcl_61 (<= x_26 ?cvcl_56)) (flet ($cvcl_52 (<= x_24 x_5)) (flet ($cvcl_58 $cvcl_52) (flet ($cvcl_54 (<= x_26 x_5)) (flet ($cvcl_60 $cvcl_54) (flet ($cvcl_53 (not x_43)) (flet ($cvcl_64 $cvcl_53) (flet ($cvcl_87 (< x_24 x_6)) (flet ($cvcl_88 (= x_32 x_24)) (flet ($cvcl_55 (not x_45)) (flet ($cvcl_66 $cvcl_55) (flet ($cvcl_89 (< x_26 x_6)) (flet ($cvcl_90 (= x_32 x_26)) (flet ($cvcl_43 (not x_41)) (flet ($cvcl_68 $cvcl_43) (flet ($cvcl_109 (not $cvcl_106)) (flet ($cvcl_63 (not x_58)) (flet ($cvcl_65 (not x_60)) (flet ($cvcl_67 (not x_56)) (flet ($cvcl_70 (and (not $cvcl_52) (<= x_24 x_32))) (flet ($cvcl_71 (and (not $cvcl_54) (<= x_26 x_32))) (flet ($cvcl_78 (and (iff x_71 (or x_43  (and $cvcl_70 x_58) )) (iff x_72 (or x_45  (and $cvcl_71 x_60) )))) (flet ($cvcl_62 (<= x_7 ?cvcl_56)) (flet ($cvcl_91 (< x_7 x_6)) (flet ($cvcl_92 (= x_32 x_7)) (flet ($cvcl_95 (<= (ite x_47 (ite x_25 (ite x_23 3 2) x_81) (ite x_25 x_81 (ite x_23 1 0))) (* (* (ite x_41 (ite x_45 (ite x_43 0 1) x_82) (ite x_45 x_82 (ite x_43 2 3))) 1) (/ 1 2)))) (flet ($cvcl_112 $cvcl_72) (flet ($cvcl_74 (not $cvcl_59)) (flet ($cvcl_75 (not $cvcl_61)) (flet ($cvcl_185 (not (<= x_7 x_5))) (flet ($cvcl_28 (and $cvcl_185 $cvcl_72)) (flet ($cvcl_29 $cvcl_28) (flet ($cvcl_186 (not (<= x_8 x_5))) (flet ($cvcl_32 (and $cvcl_186 (<= x_8 x_32))) (flet ($cvcl_30 $cvcl_32) (flet ($cvcl_33 $cvcl_28) (flet ($cvcl_34 $cvcl_32) (flet ($cvcl_76 (not $cvcl_62)) (flet ($cvcl_126 (= x_49 0)) (flet ($cvcl_115 (= x_49 3)) (flet ($cvcl_122 (= x_51 0)) (flet ($cvcl_113 (= x_51 3)) (flet ($cvcl_124 (= x_53 0)) (flet ($cvcl_114 (= x_53 3)) (flet ($cvcl_49 (= x_74 0)) (flet ($cvcl_38 (= x_74 3)) (flet ($cvcl_45 (= x_75 0)) (flet ($cvcl_36 (= x_75 3)) (flet ($cvcl_47 (= x_76 0)) (flet ($cvcl_37 (= x_76 3)) (flet ($cvcl_4 (not $cvcl_51)) (flet ($cvcl_3 (not $cvcl_86)) (flet ($cvcl_5 (< x_32 x_33)) (flet ($cvcl_6 (< x_32 x_35)) (flet ($cvcl_57 (not x_29)) (flet ($cvcl_105 (not (<= x_36 x_33))) (flet ($cvcl_107 (not (<= x_36 x_35))) (flet ($cvcl_110 (< x_37 x_38)) (flet ($cvcl_111 (< x_38 x_39)) (flet ($cvcl_104 (not $cvcl_101)) (flet ($cvcl_11 (not $cvcl_102)) (flet ($cvcl_10 (not $cvcl_161)) (flet ($cvcl_12 (< x_5 x_24)) (flet ($cvcl_13 (< x_5 x_26)) (flet ($cvcl_103 (not x_21)) (flet ($cvcl_180 (not (<= x_6 x_24))) (flet ($cvcl_182 (not (<= x_6 x_26))) (flet ($cvcl_187 (< x_7 x_8)) (flet ($cvcl_188 (< x_8 x_9)) (flet ($cvcl_176 (= x_13 0)) (flet ($cvcl_179 (not $cvcl_176)) (flet ($cvcl_177 (= x_13 1)) (flet ($cvcl_18 (not $cvcl_177)) (flet ($cvcl_17 (not (= x_13 2))) (flet ($cvcl_19 (< x_0 x_15)) (flet ($cvcl_20 (< x_0 x_17)) (flet ($cvcl_178 (not x_12)) (flet ($cvcl_24 (and (not (<= x_4 x_0)) (<= x_4 x_5))) (flet ($cvcl_31 (and (not (<= x_9 x_5)) (<= x_9 x_32))) (flet ($cvcl_41 (= x_75 (ite $cvcl_53 (ite (and $cvcl_70 (< x_51 3)) (+ x_51 1) x_51) x_51))) (flet ($cvcl_42 (= x_76 (ite $cvcl_55 (ite (and $cvcl_71 (< x_53 3)) (+ x_53 1) x_53) x_53))) (flet ($cvcl_44 (or x_43  $cvcl_36 )) (flet ($cvcl_46 (or x_45  $cvcl_37 )) (flet ($cvcl_48 (or x_41  $cvcl_38 )) (flet ($cvcl_118 (= x_51 (ite $cvcl_129 (ite (and $cvcl_145 (< x_52 3)) (+ x_52 1) x_52) x_52))) (flet ($cvcl_119 (= x_53 (ite $cvcl_131 (ite (and $cvcl_146 (< x_54 3)) (+ x_54 1) x_54) x_54))) (flet ($cvcl_121 (or x_44  $cvcl_113 )) (flet ($cvcl_123 (or x_46  $cvcl_114 )) (flet ($cvcl_125 (or x_42  $cvcl_115 )) (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 (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_30 2) (>= x_30 0)) (<= x_22 2)) (>= x_22 0)) (<= x_13 2)) (>= x_13 0)) (>= x_0 0)) (>= x_1 0)) (>= x_2 0)) (>= x_3 0)) (>= x_4 0)) (>= x_5 0)) (>= x_6 0)) (>= x_7 0)) (>= x_8 0)) (>= x_9 0)) (>= x_15 0)) (>= x_17 0)) (> x_18 0)) (>= x_18 0)) (>= x_24 0)) (>= x_26 0)) (>= x_32 0)) (>= x_33 0)) (>= x_35 0)) (>= x_36 0)) (>= x_37 0)) (>= x_38 0)) (>= x_39 0)) (>= x_40 0)) (or (or (or $cvcl_126  (= x_49 1) )  (= x_49 2) )  $cvcl_115 )) (not (< x_49 0))) (<= x_49 3)) (or (or (or (= x_50 0)  (= x_50 1) )  (= x_50 2) )  (= x_50 3) )) (not (< x_50 0))) (<= x_50 3)) (or (or (or $cvcl_122  (= x_51 1) )  (= x_51 2) )  $cvcl_113 )) (not (< x_51 0))) (<= x_51 3)) (or (or (or (= x_52 0)  (= x_52 1) )  (= x_52 2) )  (= x_52 3) )) (not (< x_52 0))) (<= x_52 3)) (or (or (or $cvcl_124  (= x_53 1) )  (= x_53 2) )  $cvcl_114 )) (not (< x_53 0))) (<= x_53 3)) (or (or (or (= x_54 0)  (= x_54 1) )  (= x_54 2) )  (= x_54 3) )) (not (< x_54 0))) (<= x_54 3)) (>= x_55 0)) (not (<= x_68 (* x_18 3)))) (>= x_68 0)) (or (or (or $cvcl_49  (= x_74 1) )  (= x_74 2) )  $cvcl_38 )) (not (< x_74 0))) (<= x_74 3)) (or (or (or $cvcl_45  (= x_75 1) )  (= x_75 2) )  $cvcl_36 )) (not (< x_75 0))) (<= x_75 3)) (or (or (or $cvcl_47  (= x_76 1) )  (= x_76 2) )  $cvcl_37 )) (not (< x_76 0))) (<= x_76 3)) (>= x_77 0)) (< x_5 x_6)) (< x_5 x_7)) (< x_5 x_8)) (< x_5 x_9)) (< x_0 x_1)) (< x_0 x_2)) (< x_0 x_3)) (< x_0 x_4)) (or (not $cvcl_35)  (and $cvcl_2 $cvcl_0) )) (or $cvcl_4  (and $cvcl_1 $cvcl_0) )) (or $cvcl_3  (and $cvcl_1 $cvcl_2) )) (or $cvcl_3  (and (or x_31  $cvcl_5 ) (or x_34  $cvcl_6 )) )) (or (or $cvcl_4  $cvcl_57 )  (and $cvcl_5 $cvcl_6) )) $cvcl_105) $cvcl_107) (< (- x_36 x_33) x_18)) (< (- x_36 x_35) x_18)) $cvcl_110) $cvcl_111) (or $cvcl_104  (and $cvcl_9 $cvcl_7) )) (or $cvcl_11  (and $cvcl_8 $cvcl_7) )) (or $cvcl_10  (and $cvcl_8 $cvcl_9) )) (or $cvcl_10  (and (or x_23  $cvcl_12 ) (or x_25  $cvcl_13 )) )) (or (or $cvcl_11  $cvcl_103 )  (and $cvcl_12 $cvcl_13) )) $cvcl_180) $cvcl_182) (< (- x_6 x_24) x_18)) (< (- x_6 x_26) x_18)) $cvcl_187) $cvcl_188) (or $cvcl_179  (and $cvcl_16 $cvcl_14) )) (or $cvcl_18  (and $cvcl_15 $cvcl_14) )) (or $cvcl_17  (and $cvcl_15 $cvcl_16) )) (or $cvcl_17  (and (or x_14  $cvcl_19 ) (or x_16  $cvcl_20 )) )) (or (or $cvcl_18  $cvcl_178 )  (and $cvcl_19 $cvcl_20) )) (not (<= x_1 x_15))) (not (<= x_1 x_17))) (< (- x_1 x_15) x_18)) (< (- x_1 x_17) x_18)) (< x_2 x_3)) (< x_3 x_4)) (= x_62 (ite x_14 2 1))) (= x_63 (ite x_44 1 2))) (= x_64 (ite $cvcl_22 2 1))) (= x_65 (ite $cvcl_26 2 1))) (= x_66 (+ (ite $cvcl_24 (ite $cvcl_23 (ite $cvcl_22 3 2) x_64) (ite $cvcl_23 x_64 (ite $cvcl_22 1 0))) x_50))) (= x_67 (+ (ite $cvcl_24 (ite $cvcl_27 (ite $cvcl_26 3 2) x_65) (ite $cvcl_27 x_65 (ite $cvcl_26 1 0))) x_50))) (= x_81 (ite x_23 2 1))) (= x_82 (ite x_43 1 2))) (= x_83 (ite $cvcl_29 2 1))) (= x_84 (ite $cvcl_33 2 1))) (= x_85 (+ (ite $cvcl_31 (ite $cvcl_30 (ite $cvcl_29 3 2) x_83) (ite $cvcl_30 x_83 (ite $cvcl_29 1 0))) x_49))) (= x_86 (+ (ite $cvcl_31 (ite $cvcl_34 (ite $cvcl_33 3 2) x_84) (ite $cvcl_34 x_84 (ite $cvcl_33 1 0))) x_49))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_39 $cvcl_40) $cvcl_69) $cvcl_41) $cvcl_42) (= x_74 (ite $cvcl_43 (ite (not (< x_85 3)) 3 x_85) x_49))) (iff x_71 $cvcl_44)) (iff x_72 $cvcl_46)) (iff x_70 $cvcl_48)) $cvcl_82) $cvcl_50)  (and (and (and (and (and (and (and (and (and (and $cvcl_39 (not $cvcl_40)) x_28) (= x_32 x_55)) $cvcl_41) $cvcl_42) (= x_74 (ite $cvcl_43 (ite (not (< x_86 3)) 3 x_86) x_49))) (iff x_71 (or $cvcl_44  $cvcl_45 ))) (iff x_72 (or $cvcl_46  $cvcl_47 ))) (iff x_70 (or $cvcl_48  $cvcl_49 ))) $cvcl_50) ) $cvcl_80) $cvcl_81) $cvcl_100) $cvcl_83) $cvcl_84) $cvcl_85)  (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_73 (or (or (and (and (and (not $cvcl_58) $cvcl_64) $cvcl_63) $cvcl_59)  (and (and (and (not $cvcl_60) $cvcl_66) $cvcl_65) $cvcl_61) )  (and (and $cvcl_68 $cvcl_67) $cvcl_62) )) $cvcl_57) (or (or (or (or $cvcl_58  $cvcl_74 )  x_58 )  x_43 )  (not (< x_32 x_24)) )) (or (or (or (or $cvcl_60  $cvcl_75 )  x_60 )  x_45 )  (not (< x_32 x_26)) )) (or (or (or $cvcl_76  x_56 )  x_41 )  (not (< x_32 x_7)) )) (or (or (or (and (and (and (and $cvcl_63 $cvcl_64) $cvcl_59) $cvcl_87) $cvcl_88)  (and (and (and (and $cvcl_65 $cvcl_66) $cvcl_61) $cvcl_89) $cvcl_90) )  (and (and (and (and $cvcl_67 $cvcl_68) $cvcl_62) $cvcl_91) $cvcl_92) )  (and (< x_6 ?cvcl_77) $cvcl_93) )) (iff x_79 (or x_58  $cvcl_70 ))) (iff x_80 (or x_60  $cvcl_71 ))) (iff x_78 (or x_56  $cvcl_72 ))) $cvcl_78) $cvcl_79)  (and (and (and (and (and (and (and (and (and $cvcl_73 (or (or (or $cvcl_58  x_58 )  x_43 )  $cvcl_74 )) (or (or (or $cvcl_60  x_60 )  x_45 )  $cvcl_75 )) (or (or x_56  x_41 )  $cvcl_76 )) x_29) (= x_32 ?cvcl_77)) $cvcl_78) $cvcl_79) $cvcl_80) $cvcl_81) ) $cvcl_98) $cvcl_99) $cvcl_50) $cvcl_82) $cvcl_83) $cvcl_84) $cvcl_85) )  (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_94 $cvcl_95) (not x_27)) (or (or (or $cvcl_58  x_23 )  x_43 )  (<= x_32 x_24) )) (or (or (or $cvcl_60  x_25 )  x_45 )  (<= x_32 x_26) )) (or (or x_47  x_41 )  (<= x_32 x_7) )) (or (or (or (and (and (and (and (not x_23) $cvcl_64) $cvcl_12) $cvcl_87) $cvcl_88)  (and (and (and (and (not x_25) $cvcl_66) $cvcl_13) $cvcl_89) $cvcl_90) )  (and (and (and (not x_47) $cvcl_68) $cvcl_91) $cvcl_92) )  $cvcl_93 )) (iff x_31 (or x_23  (= x_24 x_32) ))) (iff x_34 (or x_25  (= x_26 x_32) ))) (iff x_73 (or x_47  (= x_7 x_32) ))) $cvcl_96) $cvcl_97)  (and (and (and (and (and (and (and $cvcl_94 (not $cvcl_95)) x_27) $cvcl_96) $cvcl_97) (= x_32 x_5)) $cvcl_83) $cvcl_84) ) $cvcl_98) $cvcl_99) $cvcl_50) $cvcl_82) $cvcl_80) $cvcl_81) $cvcl_100) )) (or (or (and $cvcl_101 (= x_30 (ite (not x_20) x_22 1)))  (and $cvcl_102 (= x_30 (ite $cvcl_103 x_22 2))) )  (and (and $cvcl_104 $cvcl_11) (= x_30 x_22)) )) (or (and (and $cvcl_106 $cvcl_105) (not (<= x_33 ?cvcl_108)))  (and $cvcl_109 (= x_33 x_24)) )) (or (and (and $cvcl_106 $cvcl_107) (not (<= x_35 ?cvcl_108)))  (and $cvcl_109 (= x_35 x_26)) )) (or (and (and $cvcl_106 (= x_36 (+ x_6 x_68))) x_87)  (and (and $cvcl_109 (not x_87)) (= x_36 x_6)) )) (or (and (and (and (and $cvcl_112 (not (<= x_37 x_32))) (not (<= x_38 x_32))) $cvcl_110) $cvcl_111)  (and (and (and (not $cvcl_112) (= x_37 x_7)) (= x_38 x_8)) (= x_39 x_9)) )) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_116 $cvcl_117) $cvcl_144) $cvcl_118) $cvcl_119) (= x_49 (ite $cvcl_120 (ite (not (< x_66 3)) 3 x_66) x_50))) (iff x_43 $cvcl_121)) (iff x_45 $cvcl_123)) (iff x_41 $cvcl_125)) $cvcl_157) $cvcl_127)  (and (and (and (and (and (and (and (and (and (and $cvcl_116 (not $cvcl_117)) x_20) (= x_5 x_40)) $cvcl_118) $cvcl_119) (= x_49 (ite $cvcl_120 (ite (not (< x_67 3)) 3 x_67) x_50))) (iff x_43 (or $cvcl_121  $cvcl_122 ))) (iff x_45 (or $cvcl_123  $cvcl_124 ))) (iff x_41 (or $cvcl_125  $cvcl_126 ))) $cvcl_127) ) $cvcl_155) $cvcl_156) $cvcl_175) $cvcl_158) $cvcl_159) $cvcl_160)  (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_148 (or (or (and (and (and (not $cvcl_133) $cvcl_139) $cvcl_138) $cvcl_134)  (and (and (and (not $cvcl_135) $cvcl_141) $cvcl_140) $cvcl_136) )  (and (and $cvcl_143 $cvcl_142) $cvcl_137) )) $cvcl_103) (or (or (or (or $cvcl_133  $cvcl_149 )  x_59 )  x_44 )  (not (< x_5 x_15)) )) (or (or (or (or $cvcl_135  $cvcl_150 )  x_61 )  x_46 )  (not (< x_5 x_17)) )) (or (or (or $cvcl_151  x_57 )  x_42 )  (not (< x_5 x_2)) )) (or (or (or (and (and (and (and $cvcl_138 $cvcl_139) $cvcl_134) $cvcl_162) $cvcl_163)  (and (and (and (and $cvcl_140 $cvcl_141) $cvcl_136) $cvcl_164) $cvcl_165) )  (and (and (and (and $cvcl_142 $cvcl_143) $cvcl_137) $cvcl_166) $cvcl_167) )  (and (< x_1 ?cvcl_152) $cvcl_168) )) (iff x_58 (or x_59  $cvcl_145 ))) (iff x_60 (or x_61  $cvcl_146 ))) (iff x_56 (or x_57  $cvcl_147 ))) $cvcl_153) $cvcl_154)  (and (and (and (and (and (and (and (and (and $cvcl_148 (or (or (or $cvcl_133  x_59 )  x_44 )  $cvcl_149 )) (or (or (or $cvcl_135  x_61 )  x_46 )  $cvcl_150 )) (or (or x_57  x_42 )  $cvcl_151 )) x_21) (= x_5 ?cvcl_152)) $cvcl_153) $cvcl_154) $cvcl_155) $cvcl_156) ) $cvcl_173) $cvcl_174) $cvcl_127) $cvcl_157) $cvcl_158) $cvcl_159) $cvcl_160) )  (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_169 $cvcl_170) (not x_19)) (or (or (or $cvcl_133  x_14 )  x_44 )  (<= x_5 x_15) )) (or (or (or $cvcl_135  x_16 )  x_46 )  (<= x_5 x_17) )) (or (or x_48  x_42 )  (<= x_5 x_2) )) (or (or (or (and (and (and (and (not x_14) $cvcl_139) $cvcl_19) $cvcl_162) $cvcl_163)  (and (and (and (and (not x_16) $cvcl_141) $cvcl_20) $cvcl_164) $cvcl_165) )  (and (and (and (not x_48) $cvcl_143) $cvcl_166) $cvcl_167) )  $cvcl_168 )) (iff x_23 (or x_14  (= x_15 x_5) ))) (iff x_25 (or x_16  (= x_17 x_5) ))) (iff x_47 (or x_48  (= x_2 x_5) ))) $cvcl_171) $cvcl_172)  (and (and (and (and (and (and (and $cvcl_169 (not $cvcl_170)) x_19) $cvcl_171) $cvcl_172) (= x_5 x_0)) $cvcl_158) $cvcl_159) ) $cvcl_173) $cvcl_174) $cvcl_127) $cvcl_157) $cvcl_155) $cvcl_156) $cvcl_175) )) (or (or (and $cvcl_176 (= x_22 (ite (not x_11) x_13 1)))  (and $cvcl_177 (= x_22 (ite $cvcl_178 x_13 2))) )  (and (and $cvcl_179 $cvcl_18) (= x_22 x_13)) )) (or (and (and $cvcl_181 $cvcl_180) (not (<= x_24 ?cvcl_183)))  (and $cvcl_184 (= x_24 x_15)) )) (or (and (and $cvcl_181 $cvcl_182) (not (<= x_26 ?cvcl_183)))  (and $cvcl_184 (= x_26 x_17)) )) (or (and (and $cvcl_181 (= x_6 (+ x_1 x_68))) x_69)  (and (and $cvcl_184 (not x_69)) (= x_6 x_1)) )) (or (and (and (and (and $cvcl_189 $cvcl_185) $cvcl_186) $cvcl_187) $cvcl_188)  (and (and (and (not $cvcl_189) (= x_7 x_2)) (= x_8 x_3)) (= x_9 x_4)) )) (or (or (or (not (< x_32 x_36))  (not (< x_32 x_37)) )  (not (< x_32 x_38)) )  (not (< x_32 x_39)) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)