source: vis_dev/cusp-1.1/examples/plan-5.cvc/plan-5.cvc.smt @ 89

(benchmark plan
  :source {
Planning problem.
Rick Butler (R.W.Butler@larc.nasa.gov)

Translated into CVC format by Leonardo de Moura.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite

}
  :status unsat
:category { industrial }
:difficulty { 0 }
  :logic QF_IDL
  :extrafuns ((cvclZero Int))
  
  :extrafuns ((x_0 Int))
  :extrapreds ((x_1))
  :extrapreds ((x_2))
  :extrapreds ((x_3))
  :extrapreds ((x_4))
  :extrafuns ((x_5 Int))
  :extrapreds ((x_6))
  :extrapreds ((x_7))
  :extrapreds ((x_8))
  :extrafuns ((x_9 Int))
  :extrapreds ((x_10))
  :extrapreds ((x_11))
  :extrapreds ((x_12))
  :extrafuns ((x_13 Int))
  :extrafuns ((x_14 Int))
  :extrafuns ((x_15 Int))
  :extrapreds ((x_16))
  :extrapreds ((x_17))
  :extrapreds ((x_18))
  :extrapreds ((x_19))
  :extrafuns ((x_20 Int))
  :extrafuns ((x_21 Int))
  :extrapreds ((x_22))
  :extrapreds ((x_23))
  :extrapreds ((x_24))
  :extrapreds ((x_25))
  :extrafuns ((x_26 Int))
  :extrapreds ((x_27))
  :extrapreds ((x_28))
  :extrapreds ((x_29))
  :extrapreds ((x_30))
  :extrafuns ((x_31 Int))
  :extrafuns ((x_32 Int))
  :extrafuns ((x_33 Int))
  :extrapreds ((x_34))
  :extrapreds ((x_35))
  :extrapreds ((x_36))
  :extrapreds ((x_37))
  :extrapreds ((x_38))
  :extrafuns ((x_39 Int))
  :extrapreds ((x_40))
  :extrapreds ((x_41))
  :extrapreds ((x_42))
  :extrafuns ((x_43 Int))
  :extrafuns ((x_44 Int))
  :extrafuns ((x_45 Int))
  :extrapreds ((x_46))
  :extrapreds ((x_47))
  :extrapreds ((x_48))
  :extrapreds ((x_49))
  :extrafuns ((x_50 Int))
  :extrapreds ((x_51))
  :extrapreds ((x_52))
  :extrapreds ((x_53))
  :extrapreds ((x_54))
  :extrafuns ((x_55 Int))
  :extrapreds ((x_56))
  :extrapreds ((x_57))
  :extrapreds ((x_58))
  :extrapreds ((x_59))
  :extrafuns ((x_60 Int))
  :extrafuns ((x_61 Int))
  :extrafuns ((x_62 Int))
  :extrapreds ((x_63))
  :extrapreds ((x_64))
  :extrapreds ((x_65))
  :extrapreds ((x_66))
  :extrapreds ((x_67))
  :extrafuns ((x_68 Int))
  :extrapreds ((x_69))
  :extrapreds ((x_70))
  :extrapreds ((x_71))
  :extrafuns ((x_72 Int))
  :extrafuns ((x_73 Int))
  :extrafuns ((x_74 Int))
  :extrapreds ((x_75))
  :extrapreds ((x_76))
  :extrapreds ((x_77))
  :extrapreds ((x_78))
  :extrafuns ((x_79 Int))
  :extrapreds ((x_80))
  :extrapreds ((x_81))
  :extrapreds ((x_82))
  :extrapreds ((x_83))
  :extrafuns ((x_84 Int))
  :extrapreds ((x_85))
  :extrapreds ((x_86))
  :extrapreds ((x_87))
  :extrapreds ((x_88))
  :extrafuns ((x_89 Int))
  :extrafuns ((x_90 Int))
  :extrafuns ((x_91 Int))
  :extrapreds ((x_92))
  :extrapreds ((x_93))
  :extrapreds ((x_94))
  :extrapreds ((x_95))
  :extrapreds ((x_96))
  :extrafuns ((x_97 Int))
  :extrapreds ((x_98))
  :extrapreds ((x_99))
  :extrapreds ((x_100))
  :extrafuns ((x_101 Int))
  :extrafuns ((x_102 Int))
  :extrafuns ((x_103 Int))
  :extrapreds ((x_104))
  :extrapreds ((x_105))
  :extrapreds ((x_106))
  :extrapreds ((x_107))
  :extrafuns ((x_108 Int))
  :extrapreds ((x_109))
  :extrapreds ((x_110))
  :extrapreds ((x_111))
  :extrapreds ((x_112))
  :extrafuns ((x_113 Int))
  :extrapreds ((x_114))
  :extrapreds ((x_115))
  :extrapreds ((x_116))
  :extrapreds ((x_117))
  :extrafuns ((x_118 Int))
  :extrafuns ((x_119 Int))
  :extrafuns ((x_120 Int))
  :extrapreds ((x_121))
  :extrapreds ((x_122))
  :extrapreds ((x_123))
  :extrapreds ((x_124))
  :extrapreds ((x_125))
  :extrafuns ((x_126 Int))
  :extrapreds ((x_127))
  :extrapreds ((x_128))
  :extrapreds ((x_129))
  :extrafuns ((x_130 Int))
  :formula
(flet ($cvcl_129 (and (and (iff x_16 x_1) (iff x_17 x_2)) (iff x_18 x_3))) (flet ($cvcl_132 (iff x_19 x_4)) (flet ($cvcl_139 (not x_7)) (flet ($cvcl_135 (not x_8)) (flet ($cvcl_124 (and (and x_6 $cvcl_139) $cvcl_135)) (flet ($cvcl_123 (not x_4)) (flet ($cvcl_145 (and (iff x_22 x_10) (iff x_23 x_11))) (flet ($cvcl_138 (not x_6)) (flet ($cvcl_147 (and (and $cvcl_138 $cvcl_139) x_8)) (flet ($cvcl_149 (not x_25)) (flet ($cvcl_153 (and x_24 $cvcl_149)) (flet ($cvcl_150 (not x_11)) (flet ($cvcl_154 (and x_10 $cvcl_150)) (flet ($cvcl_155 (not $cvcl_147)) (flet ($cvcl_146 (iff x_27 x_12)) (flet ($cvcl_158 (not x_24)) (flet ($cvcl_160 (and $cvcl_158 x_25)) (flet ($cvcl_151 (not x_22)) (flet ($cvcl_148 (not x_23)) (flet ($cvcl_163 (and $cvcl_151 $cvcl_148)) (flet ($cvcl_164 (iff x_27 true)) (flet ($cvcl_126 (and (and (iff x_28 x_6) (iff x_29 x_7)) (iff x_30 x_8))) (flet ($cvcl_87 (and (and (iff x_46 x_16) (iff x_47 x_17)) (iff x_48 x_18))) (flet ($cvcl_92 (iff x_49 x_19)) (flet ($cvcl_99 (not x_29)) (flet ($cvcl_95 (not x_30)) (flet ($cvcl_90 (and (and x_28 $cvcl_99) $cvcl_95)) (flet ($cvcl_91 (not x_19)) (flet ($cvcl_105 (and (iff x_51 x_22) (iff x_52 x_23))) (flet ($cvcl_98 (not x_28)) (flet ($cvcl_107 (and (and $cvcl_98 $cvcl_99) x_30)) (flet ($cvcl_109 (not x_54)) (flet ($cvcl_112 (and x_53 $cvcl_109)) (flet ($cvcl_113 (and x_22 $cvcl_148)) (flet ($cvcl_114 (not $cvcl_107)) (flet ($cvcl_106 (iff x_56 x_27)) (flet ($cvcl_117 (not x_53)) (flet ($cvcl_118 (and $cvcl_117 x_54)) (flet ($cvcl_110 (not x_51)) (flet ($cvcl_108 (not x_52)) (flet ($cvcl_121 (and $cvcl_110 $cvcl_108)) (flet ($cvcl_122 (iff x_56 true)) (flet ($cvcl_84 (and (and (iff x_57 x_28) (iff x_58 x_29)) (iff x_59 x_30))) (flet ($cvcl_47 (and (and (iff x_75 x_46) (iff x_76 x_47)) (iff x_77 x_48))) (flet ($cvcl_52 (iff x_78 x_49)) (flet ($cvcl_59 (not x_58)) (flet ($cvcl_55 (not x_59)) (flet ($cvcl_50 (and (and x_57 $cvcl_59) $cvcl_55)) (flet ($cvcl_51 (not x_49)) (flet ($cvcl_65 (and (iff x_80 x_51) (iff x_81 x_52))) (flet ($cvcl_58 (not x_57)) (flet ($cvcl_67 (and (and $cvcl_58 $cvcl_59) x_59)) (flet ($cvcl_69 (not x_83)) (flet ($cvcl_72 (and x_82 $cvcl_69)) (flet ($cvcl_73 (and x_51 $cvcl_108)) (flet ($cvcl_74 (not $cvcl_67)) (flet ($cvcl_66 (iff x_85 x_56)) (flet ($cvcl_77 (not x_82)) (flet ($cvcl_78 (and $cvcl_77 x_83)) (flet ($cvcl_70 (not x_80)) (flet ($cvcl_68 (not x_81)) (flet ($cvcl_81 (and $cvcl_70 $cvcl_68)) (flet ($cvcl_82 (iff x_85 true)) (flet ($cvcl_44 (and (and (iff x_86 x_57) (iff x_87 x_58)) (iff x_88 x_59))) (flet ($cvcl_4 (and (and (iff x_104 x_75) (iff x_105 x_76)) (iff x_106 x_77))) (flet ($cvcl_9 (iff x_107 x_78)) (flet ($cvcl_18 (not x_87)) (flet ($cvcl_12 (not x_88)) (flet ($cvcl_7 (and (and x_86 $cvcl_18) $cvcl_12)) (flet ($cvcl_8 (not x_78)) (flet ($cvcl_25 (and (iff x_109 x_80) (iff x_110 x_81))) (flet ($cvcl_17 (not x_86)) (flet ($cvcl_27 (and (and $cvcl_17 $cvcl_18) x_88)) (flet ($cvcl_28 (not x_112)) (flet ($cvcl_30 (and x_111 $cvcl_28)) (flet ($cvcl_31 (and x_80 $cvcl_68)) (flet ($cvcl_32 (not $cvcl_27)) (flet ($cvcl_26 (iff x_114 x_85)) (flet ($cvcl_35 (not x_111)) (flet ($cvcl_38 (and $cvcl_35 x_112)) (flet ($cvcl_36 (not x_109)) (flet ($cvcl_37 (not x_110)) (flet ($cvcl_41 (and $cvcl_36 $cvcl_37)) (flet ($cvcl_42 (iff x_114 true)) (flet ($cvcl_1 (and (and (iff x_115 x_86) (iff x_116 x_87)) (iff x_117 x_88))) (flet ($cvcl_167 (not x_1)) (flet ($cvcl_166 (not x_2)) (flet ($cvcl_159 (not x_10)) (flet ($cvcl_3 (not x_121)) (flet ($cvcl_0 (not x_122)) (flet ($cvcl_15 (not x_127)) (flet ($cvcl_10 (not x_128)) (flet ($cvcl_11 (not x_129)) (flet ($cvcl_16 (not x_115)) (flet ($cvcl_14 (not x_117)) (flet ($cvcl_170 (not x_77)) (flet ($cvcl_19 (not x_116)) (flet ($cvcl_46 (not x_92)) (flet ($cvcl_43 (not x_93)) (flet ($cvcl_57 (not x_98)) (flet ($cvcl_53 (not x_99)) (flet ($cvcl_54 (not x_100)) (flet ($cvcl_169 (not x_48)) (flet ($cvcl_86 (not x_63)) (flet ($cvcl_83 (not x_64)) (flet ($cvcl_97 (not x_69)) (flet ($cvcl_93 (not x_70)) (flet ($cvcl_94 (not x_71)) (flet ($cvcl_168 (not x_18)) (flet ($cvcl_128 (not x_34)) (flet ($cvcl_125 (not x_35)) (flet ($cvcl_137 (not x_40)) (flet ($cvcl_133 (not x_41)) (flet ($cvcl_134 (not x_42)) (flet ($cvcl_165 (not x_3)) (flet ($cvcl_171 (not x_106)) (flet ($cvcl_5 (= (- x_113 x_84) 0)) (flet ($cvcl_2 (= (- x_118 x_89) 0)) (flet ($cvcl_6 (= (- x_102 x_73) 0)) (flet ($cvcl_23 (= (- x_103 x_74) 0)) (flet ($cvcl_24 (= (- x_108 x_79) 0)) (flet ($cvcl_13 (= (- x_103 x_89) 0)) (flet ($cvcl_20 (not (< (- x_89 x_74) 2))) (flet ($cvcl_21 (<= (- x_89 x_74) 6)) (flet ($cvcl_22 (= (- x_113 x_84) (~ 20))) (flet ($cvcl_29 (= (- x_108 x_89) 0)) (flet ($cvcl_33 (not (< (- x_89 x_79) 20))) (flet ($cvcl_34 (<= (- x_89 x_79) 25)) (flet ($cvcl_39 (not (< (- x_89 x_79) 2))) (flet ($cvcl_40 (<= (- x_89 x_79) 5)) (flet ($cvcl_48 (= (- x_84 x_55) 0)) (flet ($cvcl_45 (= (- x_89 x_60) 0)) (flet ($cvcl_49 (= (- x_73 x_44) 0)) (flet ($cvcl_63 (= (- x_74 x_45) 0)) (flet ($cvcl_64 (= (- x_79 x_50) 0)) (flet ($cvcl_56 (= (- x_74 x_60) 0)) (flet ($cvcl_60 (not (< (- x_60 x_45) 2))) (flet ($cvcl_61 (<= (- x_60 x_45) 6)) (flet ($cvcl_62 (= (- x_84 x_55) (~ 20))) (flet ($cvcl_71 (= (- x_79 x_60) 0)) (flet ($cvcl_75 (not (< (- x_60 x_50) 20))) (flet ($cvcl_76 (<= (- x_60 x_50) 25)) (flet ($cvcl_79 (not (< (- x_60 x_50) 2))) (flet ($cvcl_80 (<= (- x_60 x_50) 5)) (flet ($cvcl_88 (= (- x_55 x_26) 0)) (flet ($cvcl_85 (= (- x_60 x_31) 0)) (flet ($cvcl_89 (= (- x_44 x_13) 0)) (flet ($cvcl_103 (= (- x_45 x_15) 0)) (flet ($cvcl_104 (= (- x_50 x_20) 0)) (flet ($cvcl_96 (= (- x_45 x_31) 0)) (flet ($cvcl_100 (not (< (- x_31 x_15) 2))) (flet ($cvcl_101 (<= (- x_31 x_15) 6)) (flet ($cvcl_102 (= (- x_55 x_26) (~ 20))) (flet ($cvcl_111 (= (- x_50 x_31) 0)) (flet ($cvcl_115 (not (< (- x_31 x_20) 20))) (flet ($cvcl_116 (<= (- x_31 x_20) 25)) (flet ($cvcl_119 (not (< (- x_31 x_20) 2))) (flet ($cvcl_120 (<= (- x_31 x_20) 5)) (flet ($cvcl_130 (= (- x_26 x_5) 0)) (flet ($cvcl_127 (= (- x_31 x_0) 0)) (flet ($cvcl_131 (= (- x_13 x_14) 0)) (flet ($cvcl_143 (= (- x_15 x_9) 0)) (flet ($cvcl_144 (= (- x_20 x_21) 0)) (flet ($cvcl_136 (= (- x_15 x_0) 0)) (flet ($cvcl_140 (not (< (- x_0 x_9) 2))) (flet ($cvcl_141 (<= (- x_0 x_9) 6)) (flet ($cvcl_142 (= (- x_26 x_5) (~ 20))) (flet ($cvcl_152 (= (- x_20 x_0) 0)) (flet ($cvcl_156 (not (< (- x_0 x_21) 20))) (flet ($cvcl_157 (<= (- x_0 x_21) 25)) (flet ($cvcl_161 (not (< (- x_0 x_21) 2))) (flet ($cvcl_162 (<= (- x_0 x_21) 5)) (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 (not (< (- x_0 cvclZero) 0)) (not (< (- x_5 cvclZero) 0))) (not (< (- x_9 cvclZero) 0))) (not (< (- x_13 cvclZero) 0))) (not (< (- x_14 cvclZero) 0))) (not (< (- x_15 cvclZero) 0))) (not (< (- x_20 cvclZero) 0))) (not (< (- x_21 cvclZero) 0))) (not (< (- x_26 cvclZero) 0))) (not (< (- x_31 cvclZero) 0))) (not (< (- x_44 cvclZero) 0))) (not (< (- x_45 cvclZero) 0))) (not (< (- x_50 cvclZero) 0))) (not (< (- x_55 cvclZero) 0))) (not (< (- x_60 cvclZero) 0))) (not (< (- x_73 cvclZero) 0))) (not (< (- x_74 cvclZero) 0))) (not (< (- x_79 cvclZero) 0))) (not (< (- x_84 cvclZero) 0))) (not (< (- x_89 cvclZero) 0))) (not (< (- x_102 cvclZero) 0))) (not (< (- x_103 cvclZero) 0))) (not (< (- x_108 cvclZero) 0))) (not (< (- x_113 cvclZero) 0))) (not (< (- x_118 cvclZero) 0))) (= (- x_0 cvclZero) 0)) (and (and $cvcl_167 $cvcl_166) x_3)) $cvcl_123) (= (- x_5 cvclZero) 1000)) $cvcl_124) (= (- x_9 cvclZero) 0)) (and $cvcl_159 $cvcl_150)) (not x_12)) (or (or (and (and (and (and (and (= (- x_119 cvclZero) 0) (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_120 cvclZero) 0) $cvcl_3) $cvcl_0) $cvcl_8) $cvcl_7) (= (- x_102 x_89) 0)) x_107) $cvcl_4) $cvcl_5) $cvcl_1) $cvcl_2)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_120 cvclZero) 1) x_121) $cvcl_0) x_78) (not (<= (- x_89 x_73) 10))) (iff x_104 x_123)) (iff x_105 x_124)) (iff x_106 x_125)) (not x_107)) (= (- x_113 x_84) (~ 400))) $cvcl_1) $cvcl_6) $cvcl_2) )  (and (and (and (and (and (and (and (and (= (- x_120 cvclZero) 2) $cvcl_3) x_122) (= (- x_118 x_89) 1)) $cvcl_4) $cvcl_5) $cvcl_1) $cvcl_9) $cvcl_6) )) $cvcl_23) $cvcl_24) $cvcl_25) $cvcl_26)  (and (and (and (and (and (= (- x_119 cvclZero) 1) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_126 cvclZero) 0) $cvcl_15) $cvcl_10) $cvcl_11) $cvcl_7) $cvcl_8) $cvcl_13) $cvcl_16) x_116) $cvcl_14) $cvcl_4) $cvcl_5) $cvcl_9) $cvcl_2)  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_126 cvclZero) 1) x_127) $cvcl_10) $cvcl_11) $cvcl_17) x_87) $cvcl_12) $cvcl_8) $cvcl_20) $cvcl_21) $cvcl_13) x_115) x_116) $cvcl_14) $cvcl_22) $cvcl_4) $cvcl_9) $cvcl_2) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_126 cvclZero) 2) $cvcl_15) x_128) $cvcl_11) x_86) x_87) $cvcl_12) $cvcl_8) x_75) x_76) $cvcl_170) (not (< (- x_89 x_74) 3))) (<= (- x_89 x_74) 12)) $cvcl_13) $cvcl_16) $cvcl_19) x_117) $cvcl_4) $cvcl_5) $cvcl_9) $cvcl_2) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_126 cvclZero) 3) x_127) x_128) $cvcl_11) $cvcl_27) $cvcl_8) (not (< (- x_89 x_74) 20))) (<= (- x_89 x_74) 25)) $cvcl_13) $cvcl_16) $cvcl_19) $cvcl_14) (= (- x_113 x_84) (~ 120))) $cvcl_4) $cvcl_9) $cvcl_2) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_126 cvclZero) 4) $cvcl_15) $cvcl_10) x_129) $cvcl_17) $cvcl_18) $cvcl_12) $cvcl_20) $cvcl_21) x_115) $cvcl_19) $cvcl_14) $cvcl_22) $cvcl_4) $cvcl_9) $cvcl_23) $cvcl_2) )) $cvcl_6) $cvcl_24) $cvcl_25) $cvcl_26) )  (and (and (and (and (and (= (- x_119 cvclZero) 2) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_130 cvclZero) 0) $cvcl_35) $cvcl_28) $cvcl_27) x_109) $cvcl_37) $cvcl_29) $cvcl_5) $cvcl_1) $cvcl_26) $cvcl_2)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_130 cvclZero) 1) $cvcl_30) $cvcl_31) $cvcl_32) $cvcl_33) $cvcl_34) $cvcl_36) x_110) $cvcl_29) $cvcl_5) $cvcl_1) $cvcl_26) $cvcl_2) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_130 cvclZero) 2) $cvcl_30) $cvcl_31) $cvcl_32) $cvcl_33) $cvcl_34) x_109) x_110) $cvcl_29) $cvcl_5) $cvcl_1) $cvcl_26) $cvcl_2) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_130 cvclZero) 3) $cvcl_38) $cvcl_70) x_81) $cvcl_39) $cvcl_40) (not (<= (- x_84 cvclZero) 600))) $cvcl_41) $cvcl_29) (= (- x_113 x_84) (~ 600))) $cvcl_42) $cvcl_1) $cvcl_2) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_130 cvclZero) 4) $cvcl_38) x_80) x_81) $cvcl_39) $cvcl_40) (not (<= (- x_84 cvclZero) 20))) $cvcl_41) $cvcl_29) $cvcl_22) $cvcl_42) $cvcl_1) $cvcl_2) )) $cvcl_6) $cvcl_23) $cvcl_4) $cvcl_9) )) (or (or (and (and (and (and (and (= (- x_90 cvclZero) 0) (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_91 cvclZero) 0) $cvcl_46) $cvcl_43) $cvcl_51) $cvcl_50) (= (- x_73 x_60) 0)) x_78) $cvcl_47) $cvcl_48) $cvcl_44) $cvcl_45)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_91 cvclZero) 1) x_92) $cvcl_43) x_49) (not (<= (- x_60 x_44) 10))) (iff x_75 x_94)) (iff x_76 x_95)) (iff x_77 x_96)) $cvcl_8) (= (- x_84 x_55) (~ 400))) $cvcl_44) $cvcl_49) $cvcl_45) )  (and (and (and (and (and (and (and (and (= (- x_91 cvclZero) 2) $cvcl_46) x_93) (= (- x_89 x_60) 1)) $cvcl_47) $cvcl_48) $cvcl_44) $cvcl_52) $cvcl_49) )) $cvcl_63) $cvcl_64) $cvcl_65) $cvcl_66)  (and (and (and (and (and (= (- x_90 cvclZero) 1) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_97 cvclZero) 0) $cvcl_57) $cvcl_53) $cvcl_54) $cvcl_50) $cvcl_51) $cvcl_56) $cvcl_17) x_87) $cvcl_12) $cvcl_47) $cvcl_48) $cvcl_52) $cvcl_45)  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_97 cvclZero) 1) x_98) $cvcl_53) $cvcl_54) $cvcl_58) x_58) $cvcl_55) $cvcl_51) $cvcl_60) $cvcl_61) $cvcl_56) x_86) x_87) $cvcl_12) $cvcl_62) $cvcl_47) $cvcl_52) $cvcl_45) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_97 cvclZero) 2) $cvcl_57) x_99) $cvcl_54) x_57) x_58) $cvcl_55) $cvcl_51) x_46) x_47) $cvcl_169) (not (< (- x_60 x_45) 3))) (<= (- x_60 x_45) 12)) $cvcl_56) $cvcl_17) $cvcl_18) x_88) $cvcl_47) $cvcl_48) $cvcl_52) $cvcl_45) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_97 cvclZero) 3) x_98) x_99) $cvcl_54) $cvcl_67) $cvcl_51) (not (< (- x_60 x_45) 20))) (<= (- x_60 x_45) 25)) $cvcl_56) $cvcl_17) $cvcl_18) $cvcl_12) (= (- x_84 x_55) (~ 120))) $cvcl_47) $cvcl_52) $cvcl_45) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_97 cvclZero) 4) $cvcl_57) $cvcl_53) x_100) $cvcl_58) $cvcl_59) $cvcl_55) $cvcl_60) $cvcl_61) x_86) $cvcl_18) $cvcl_12) $cvcl_62) $cvcl_47) $cvcl_52) $cvcl_63) $cvcl_45) )) $cvcl_49) $cvcl_64) $cvcl_65) $cvcl_66) )  (and (and (and (and (and (= (- x_90 cvclZero) 2) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_101 cvclZero) 0) $cvcl_77) $cvcl_69) $cvcl_67) x_80) $cvcl_68) $cvcl_71) $cvcl_48) $cvcl_44) $cvcl_66) $cvcl_45)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_101 cvclZero) 1) $cvcl_72) $cvcl_73) $cvcl_74) $cvcl_75) $cvcl_76) $cvcl_70) x_81) $cvcl_71) $cvcl_48) $cvcl_44) $cvcl_66) $cvcl_45) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_101 cvclZero) 2) $cvcl_72) $cvcl_73) $cvcl_74) $cvcl_75) $cvcl_76) x_80) x_81) $cvcl_71) $cvcl_48) $cvcl_44) $cvcl_66) $cvcl_45) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_101 cvclZero) 3) $cvcl_78) $cvcl_110) x_52) $cvcl_79) $cvcl_80) (not (<= (- x_55 cvclZero) 600))) $cvcl_81) $cvcl_71) (= (- x_84 x_55) (~ 600))) $cvcl_82) $cvcl_44) $cvcl_45) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_101 cvclZero) 4) $cvcl_78) x_51) x_52) $cvcl_79) $cvcl_80) (not (<= (- x_55 cvclZero) 20))) $cvcl_81) $cvcl_71) $cvcl_62) $cvcl_82) $cvcl_44) $cvcl_45) )) $cvcl_49) $cvcl_63) $cvcl_47) $cvcl_52) )) (or (or (and (and (and (and (and (= (- x_61 cvclZero) 0) (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_62 cvclZero) 0) $cvcl_86) $cvcl_83) $cvcl_91) $cvcl_90) (= (- x_44 x_31) 0)) x_49) $cvcl_87) $cvcl_88) $cvcl_84) $cvcl_85)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_62 cvclZero) 1) x_63) $cvcl_83) x_19) (not (<= (- x_31 x_13) 10))) (iff x_46 x_65)) (iff x_47 x_66)) (iff x_48 x_67)) $cvcl_51) (= (- x_55 x_26) (~ 400))) $cvcl_84) $cvcl_89) $cvcl_85) )  (and (and (and (and (and (and (and (and (= (- x_62 cvclZero) 2) $cvcl_86) x_64) (= (- x_60 x_31) 1)) $cvcl_87) $cvcl_88) $cvcl_84) $cvcl_92) $cvcl_89) )) $cvcl_103) $cvcl_104) $cvcl_105) $cvcl_106)  (and (and (and (and (and (= (- x_61 cvclZero) 1) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_68 cvclZero) 0) $cvcl_97) $cvcl_93) $cvcl_94) $cvcl_90) $cvcl_91) $cvcl_96) $cvcl_58) x_58) $cvcl_55) $cvcl_87) $cvcl_88) $cvcl_92) $cvcl_85)  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_68 cvclZero) 1) x_69) $cvcl_93) $cvcl_94) $cvcl_98) x_29) $cvcl_95) $cvcl_91) $cvcl_100) $cvcl_101) $cvcl_96) x_57) x_58) $cvcl_55) $cvcl_102) $cvcl_87) $cvcl_92) $cvcl_85) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_68 cvclZero) 2) $cvcl_97) x_70) $cvcl_94) x_28) x_29) $cvcl_95) $cvcl_91) x_16) x_17) $cvcl_168) (not (< (- x_31 x_15) 3))) (<= (- x_31 x_15) 12)) $cvcl_96) $cvcl_58) $cvcl_59) x_59) $cvcl_87) $cvcl_88) $cvcl_92) $cvcl_85) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_68 cvclZero) 3) x_69) x_70) $cvcl_94) $cvcl_107) $cvcl_91) (not (< (- x_31 x_15) 20))) (<= (- x_31 x_15) 25)) $cvcl_96) $cvcl_58) $cvcl_59) $cvcl_55) (= (- x_55 x_26) (~ 120))) $cvcl_87) $cvcl_92) $cvcl_85) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_68 cvclZero) 4) $cvcl_97) $cvcl_93) x_71) $cvcl_98) $cvcl_99) $cvcl_95) $cvcl_100) $cvcl_101) x_57) $cvcl_59) $cvcl_55) $cvcl_102) $cvcl_87) $cvcl_92) $cvcl_103) $cvcl_85) )) $cvcl_89) $cvcl_104) $cvcl_105) $cvcl_106) )  (and (and (and (and (and (= (- x_61 cvclZero) 2) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_72 cvclZero) 0) $cvcl_117) $cvcl_109) $cvcl_107) x_51) $cvcl_108) $cvcl_111) $cvcl_88) $cvcl_84) $cvcl_106) $cvcl_85)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_72 cvclZero) 1) $cvcl_112) $cvcl_113) $cvcl_114) $cvcl_115) $cvcl_116) $cvcl_110) x_52) $cvcl_111) $cvcl_88) $cvcl_84) $cvcl_106) $cvcl_85) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_72 cvclZero) 2) $cvcl_112) $cvcl_113) $cvcl_114) $cvcl_115) $cvcl_116) x_51) x_52) $cvcl_111) $cvcl_88) $cvcl_84) $cvcl_106) $cvcl_85) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_72 cvclZero) 3) $cvcl_118) $cvcl_151) x_23) $cvcl_119) $cvcl_120) (not (<= (- x_26 cvclZero) 600))) $cvcl_121) $cvcl_111) (= (- x_55 x_26) (~ 600))) $cvcl_122) $cvcl_84) $cvcl_85) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_72 cvclZero) 4) $cvcl_118) x_22) x_23) $cvcl_119) $cvcl_120) (not (<= (- x_26 cvclZero) 20))) $cvcl_121) $cvcl_111) $cvcl_102) $cvcl_122) $cvcl_84) $cvcl_85) )) $cvcl_89) $cvcl_103) $cvcl_87) $cvcl_92) )) (or (or (and (and (and (and (and (= (- x_32 cvclZero) 0) (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_33 cvclZero) 0) $cvcl_128) $cvcl_125) $cvcl_123) $cvcl_124) (= (- x_13 x_0) 0)) x_19) $cvcl_129) $cvcl_130) $cvcl_126) $cvcl_127)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_33 cvclZero) 1) x_34) $cvcl_125) x_4) (not (<= (- x_0 x_14) 10))) (iff x_16 x_36)) (iff x_17 x_37)) (iff x_18 x_38)) $cvcl_91) (= (- x_26 x_5) (~ 400))) $cvcl_126) $cvcl_131) $cvcl_127) )  (and (and (and (and (and (and (and (and (= (- x_33 cvclZero) 2) $cvcl_128) x_35) (= (- x_31 x_0) 1)) $cvcl_129) $cvcl_130) $cvcl_126) $cvcl_132) $cvcl_131) )) $cvcl_143) $cvcl_144) $cvcl_145) $cvcl_146)  (and (and (and (and (and (= (- x_32 cvclZero) 1) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_39 cvclZero) 0) $cvcl_137) $cvcl_133) $cvcl_134) $cvcl_124) $cvcl_123) $cvcl_136) $cvcl_98) x_29) $cvcl_95) $cvcl_129) $cvcl_130) $cvcl_132) $cvcl_127)  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_39 cvclZero) 1) x_40) $cvcl_133) $cvcl_134) $cvcl_138) x_7) $cvcl_135) $cvcl_123) $cvcl_140) $cvcl_141) $cvcl_136) x_28) x_29) $cvcl_95) $cvcl_142) $cvcl_129) $cvcl_132) $cvcl_127) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_39 cvclZero) 2) $cvcl_137) x_41) $cvcl_134) x_6) x_7) $cvcl_135) $cvcl_123) x_1) x_2) $cvcl_165) (not (< (- x_0 x_9) 3))) (<= (- x_0 x_9) 12)) $cvcl_136) $cvcl_98) $cvcl_99) x_30) $cvcl_129) $cvcl_130) $cvcl_132) $cvcl_127) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_39 cvclZero) 3) x_40) x_41) $cvcl_134) $cvcl_147) $cvcl_123) (not (< (- x_0 x_9) 20))) (<= (- x_0 x_9) 25)) $cvcl_136) $cvcl_98) $cvcl_99) $cvcl_95) (= (- x_26 x_5) (~ 120))) $cvcl_129) $cvcl_132) $cvcl_127) )  (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_39 cvclZero) 4) $cvcl_137) $cvcl_133) x_42) $cvcl_138) $cvcl_139) $cvcl_135) $cvcl_140) $cvcl_141) x_28) $cvcl_99) $cvcl_95) $cvcl_142) $cvcl_129) $cvcl_132) $cvcl_143) $cvcl_127) )) $cvcl_131) $cvcl_144) $cvcl_145) $cvcl_146) )  (and (and (and (and (and (= (- x_32 cvclZero) 2) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= (- x_43 cvclZero) 0) $cvcl_158) $cvcl_149) $cvcl_147) x_22) $cvcl_148) $cvcl_152) $cvcl_130) $cvcl_126) $cvcl_146) $cvcl_127)  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_43 cvclZero) 1) $cvcl_153) $cvcl_154) $cvcl_155) $cvcl_156) $cvcl_157) $cvcl_151) x_23) $cvcl_152) $cvcl_130) $cvcl_126) $cvcl_146) $cvcl_127) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_43 cvclZero) 2) $cvcl_153) $cvcl_154) $cvcl_155) $cvcl_156) $cvcl_157) x_22) x_23) $cvcl_152) $cvcl_130) $cvcl_126) $cvcl_146) $cvcl_127) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_43 cvclZero) 3) $cvcl_160) $cvcl_159) x_11) $cvcl_161) $cvcl_162) (not (<= (- x_5 cvclZero) 600))) $cvcl_163) $cvcl_152) (= (- x_26 x_5) (~ 600))) $cvcl_164) $cvcl_126) $cvcl_127) )  (and (and (and (and (and (and (and (and (and (and (and (and (= (- x_43 cvclZero) 4) $cvcl_160) x_10) x_11) $cvcl_161) $cvcl_162) (not (<= (- x_5 cvclZero) 20))) $cvcl_163) $cvcl_152) $cvcl_142) $cvcl_164) $cvcl_126) $cvcl_127) )) $cvcl_131) $cvcl_143) $cvcl_129) $cvcl_132) )) (and (and x_104 x_105) $cvcl_171)) x_114) (not (<= (- x_113 cvclZero) 0))) (or $cvcl_165  (and $cvcl_166 $cvcl_167) )) (or $cvcl_135  (and $cvcl_139 $cvcl_138) )) (or $cvcl_168  (and (not x_17) (not x_16)) )) (or $cvcl_149  $cvcl_158 )) (or $cvcl_95  (and $cvcl_99 $cvcl_98) )) (or $cvcl_125  $cvcl_128 )) (or (not x_38)  (and (not x_37) (not x_36)) )) (or $cvcl_134  (and $cvcl_133 $cvcl_137) )) (or $cvcl_169  (and (not x_47) (not x_46)) )) (or $cvcl_109  $cvcl_117 )) (or $cvcl_55  (and $cvcl_59 $cvcl_58) )) (or $cvcl_83  $cvcl_86 )) (or (not x_67)  (and (not x_66) (not x_65)) )) (or $cvcl_94  (and $cvcl_93 $cvcl_97) )) (or $cvcl_170  (and (not x_76) (not x_75)) )) (or $cvcl_69  $cvcl_77 )) (or $cvcl_12  (and $cvcl_18 $cvcl_17) )) (or $cvcl_43  $cvcl_46 )) (or (not x_96)  (and (not x_95) (not x_94)) )) (or $cvcl_54  (and $cvcl_53 $cvcl_57) )) (or $cvcl_171  (and (not x_105) (not x_104)) )) (or $cvcl_28  $cvcl_35 )) (or $cvcl_14  (and $cvcl_19 $cvcl_16) )) (or $cvcl_0  $cvcl_3 )) (or (not x_125)  (and (not x_124) (not x_123)) )) (or $cvcl_11  (and $cvcl_10 $cvcl_15) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)