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