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