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