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