(benchmark Rod_2_8_1.smt
	:status unknown
	:difficulty {unknown}
	:category {unknown}
	:logic QF_LRA
	:extrapreds ((jump_0))
	:extrapreds ((jump_1))
	:extrapreds ((jump_2))
	:extrapreds ((jump_3))
	:extrapreds ((jump_4))
	:extrapreds ((jump_5))
	:extrapreds ((jump_6))
	:extrapreds ((jump_7))
	:extrapreds ((out_1_0))
	:extrapreds ((in_1_0))
	:extrapreds ((recover_1_0))
	:extrapreds ((add_1_0))
	:extrapreds ((remove_1_0))
	:extrapreds ((out_2_0))
	:extrapreds ((in_2_0))
	:extrapreds ((recover_2_0))
	:extrapreds ((add_2_0))
	:extrapreds ((remove_2_0))
	:extrapreds ((rod_0_0))
	:extrapreds ((rod_1_0))
	:extrapreds ((rod_2_0))
	:extrafuns ((dt_0 Real))
	:extrafuns ((x_1_0 Real))
	:extrafuns ((x_2_0 Real))
	:extrafuns ((x_3_0 Real))
	:extrapreds ((out_1_1))
	:extrapreds ((in_1_1))
	:extrapreds ((recover_1_1))
	:extrapreds ((add_1_1))
	:extrapreds ((remove_1_1))
	:extrapreds ((out_2_1))
	:extrapreds ((in_2_1))
	:extrapreds ((recover_2_1))
	:extrapreds ((add_2_1))
	:extrapreds ((remove_2_1))
	:extrapreds ((rod_0_1))
	:extrapreds ((rod_1_1))
	:extrapreds ((rod_2_1))
	:extrafuns ((dt_1 Real))
	:extrafuns ((x_1_1 Real))
	:extrafuns ((x_2_1 Real))
	:extrafuns ((x_3_1 Real))
	:extrapreds ((out_1_2))
	:extrapreds ((in_1_2))
	:extrapreds ((recover_1_2))
	:extrapreds ((add_1_2))
	:extrapreds ((remove_1_2))
	:extrapreds ((out_2_2))
	:extrapreds ((in_2_2))
	:extrapreds ((recover_2_2))
	:extrapreds ((add_2_2))
	:extrapreds ((remove_2_2))
	:extrapreds ((rod_0_2))
	:extrapreds ((rod_1_2))
	:extrapreds ((rod_2_2))
	:extrafuns ((dt_2 Real))
	:extrafuns ((x_1_2 Real))
	:extrafuns ((x_2_2 Real))
	:extrafuns ((x_3_2 Real))
	:extrapreds ((out_1_3))
	:extrapreds ((in_1_3))
	:extrapreds ((recover_1_3))
	:extrapreds ((add_1_3))
	:extrapreds ((remove_1_3))
	:extrapreds ((out_2_3))
	:extrapreds ((in_2_3))
	:extrapreds ((recover_2_3))
	:extrapreds ((add_2_3))
	:extrapreds ((remove_2_3))
	:extrapreds ((rod_0_3))
	:extrapreds ((rod_1_3))
	:extrapreds ((rod_2_3))
	:extrafuns ((dt_3 Real))
	:extrafuns ((x_1_3 Real))
	:extrafuns ((x_2_3 Real))
	:extrafuns ((x_3_3 Real))
	:extrapreds ((out_1_4))
	:extrapreds ((in_1_4))
	:extrapreds ((recover_1_4))
	:extrapreds ((add_1_4))
	:extrapreds ((remove_1_4))
	:extrapreds ((out_2_4))
	:extrapreds ((in_2_4))
	:extrapreds ((recover_2_4))
	:extrapreds ((add_2_4))
	:extrapreds ((remove_2_4))
	:extrapreds ((rod_0_4))
	:extrapreds ((rod_1_4))
	:extrapreds ((rod_2_4))
	:extrafuns ((dt_4 Real))
	:extrafuns ((x_1_4 Real))
	:extrafuns ((x_2_4 Real))
	:extrafuns ((x_3_4 Real))
	:extrapreds ((out_1_5))
	:extrapreds ((in_1_5))
	:extrapreds ((recover_1_5))
	:extrapreds ((add_1_5))
	:extrapreds ((remove_1_5))
	:extrapreds ((out_2_5))
	:extrapreds ((in_2_5))
	:extrapreds ((recover_2_5))
	:extrapreds ((add_2_5))
	:extrapreds ((remove_2_5))
	:extrapreds ((rod_0_5))
	:extrapreds ((rod_1_5))
	:extrapreds ((rod_2_5))
	:extrafuns ((dt_5 Real))
	:extrafuns ((x_1_5 Real))
	:extrafuns ((x_2_5 Real))
	:extrafuns ((x_3_5 Real))
	:extrapreds ((out_1_6))
	:extrapreds ((in_1_6))
	:extrapreds ((recover_1_6))
	:extrapreds ((add_1_6))
	:extrapreds ((remove_1_6))
	:extrapreds ((out_2_6))
	:extrapreds ((in_2_6))
	:extrapreds ((recover_2_6))
	:extrapreds ((add_2_6))
	:extrapreds ((remove_2_6))
	:extrapreds ((rod_0_6))
	:extrapreds ((rod_1_6))
	:extrapreds ((rod_2_6))
	:extrafuns ((dt_6 Real))
	:extrafuns ((x_1_6 Real))
	:extrafuns ((x_2_6 Real))
	:extrafuns ((x_3_6 Real))
	:extrapreds ((out_1_7))
	:extrapreds ((in_1_7))
	:extrapreds ((recover_1_7))
	:extrapreds ((add_1_7))
	:extrapreds ((remove_1_7))
	:extrapreds ((out_2_7))
	:extrapreds ((in_2_7))
	:extrapreds ((recover_2_7))
	:extrapreds ((add_2_7))
	:extrapreds ((remove_2_7))
	:extrapreds ((rod_0_7))
	:extrapreds ((rod_1_7))
	:extrapreds ((rod_2_7))
	:extrafuns ((dt_7 Real))
	:extrafuns ((x_1_7 Real))
	:extrafuns ((x_2_7 Real))
	:extrafuns ((x_3_7 Real))
	:assumption
	(not jump_0)
	:assumption
	(and true out_1_0)
 	:assumption
	(not in_1_0)
 	:assumption
	(not recover_1_0)
	:assumption
	(= x_1_0 0)
	:assumption
	(and true out_2_0)
 	:assumption
	(not in_2_0)
 	:assumption
	(not recover_2_0)
	:assumption
	(= x_2_0 0)
	:assumption
	(and true rod_0_0)
 	:assumption
	(not rod_1_0)
 	:assumption
 (not rod_2_0)
	:assumption
	(= x_3_0 0)
	:assumption
	(or jump_0 jump_1)
	:assumption
	(or ( not jump_0) (not jump_1))

	:assumption
	(or jump_1 jump_2)
	:assumption
	(or ( not jump_1) (not jump_2))

	:assumption
	(or jump_2 jump_3)
	:assumption
	(or ( not jump_2) (not jump_3))

	:assumption
	(or jump_3 jump_4)
	:assumption
	(or ( not jump_3) (not jump_4))

	:assumption
	(or jump_4 jump_5)
	:assumption
	(or ( not jump_4) (not jump_5))

	:assumption
	(or jump_5 jump_6)
	:assumption
	(or ( not jump_5) (not jump_6))

	:assumption
	(or jump_6 jump_7)
	:assumption
	(or ( not jump_6) (not jump_7))

	:assumption
	(or ( not jump_0 ) (= dt_0 0))
	:assumption
	(or jump_0 (> dt_0 0))

	:assumption
	(or ( not jump_1 ) (= dt_1 0))
	:assumption
	(or jump_1 (> dt_1 0))

	:assumption
	(or ( not jump_2 ) (= dt_2 0))
	:assumption
	(or jump_2 (> dt_2 0))

	:assumption
	(or ( not jump_3 ) (= dt_3 0))
	:assumption
	(or jump_3 (> dt_3 0))

	:assumption
	(or ( not jump_4 ) (= dt_4 0))
	:assumption
	(or jump_4 (> dt_4 0))

	:assumption
	(or ( not jump_5 ) (= dt_5 0))
	:assumption
	(or jump_5 (> dt_5 0))

	:assumption
	(or ( not jump_6 ) (= dt_6 0))
	:assumption
	(or jump_6 (> dt_6 0))

	:assumption
	(or ( not jump_7 ) (= dt_7 0))
	:assumption
	(or jump_7 (> dt_7 0))

	:assumption
	(or(not (and (and jump_0 out_1_0) add_1_0) ) in_1_1 )
	:assumption
	(or (not (and (and jump_0 out_1_0) in_1_1)) (and (and ( and  add_1_0 (not remove_1_0)) (> x_1_0 1)) (= x_1_1 0)))

	:assumption
	(or(not (and (and jump_0 in_1_0) remove_1_0) ) recover_1_1 )
	:assumption
	(or (not (and (and jump_0 in_1_0) recover_1_1)) (and ( and remove_1_0 (not add_1_0)) (= x_1_1 0)))

	:assumption
	(or(not (and jump_0 recover_1_0)  ) (or out_1_1 recover_1_1 ))
	:assumption
	(or (not (and (and jump_0 recover_1_0) out_1_1)) (and (and ( and (not add_1_0) (not remove_1_0)) (< x_1_0 10000)) (= x_1_1 x_1_0)))

	:assumption
	(or(not (and (and jump_0 out_1_0) out_1_1)) ( and (and (not add_1_0) (not remove_1_0) )  (= x_1_1 x_1_0)))

	:assumption
	(or(not (and (and jump_0 in_1_0) in_1_1)) ( and (and (not add_1_0) (not remove_1_0) )  (= x_1_1 x_1_0)))

	:assumption
	(or(not (and (and jump_0 recover_1_0) recover_1_1)) ( and (and (not add_1_0) (not remove_1_0) )  (= x_1_1 x_1_0)))

	:assumption
	(or (not (and (not jump_0) out_1_0)) (and ( and (and (and out_1_1 (<= (+ x_1_0 (* 0.9 dt_0)) x_1_1)) (<= x_1_1 (+ x_1_0 (* 1.1 dt_0))))  (< x_1_0 10000)) (< x_1_1 10000)))

	:assumption
	(or (not (and (not jump_0) in_1_0)) (and ( and (and (and in_1_1 (<= (+ x_1_0 (* 0.9 dt_0)) x_1_1)) (<= x_1_1 (+ x_1_0 (* 1.1 dt_0)))) (< x_1_0 10000)) (< x_1_1 10000)))

	:assumption
	(or (not (and (not jump_0) recover_1_0)) (and ( and (and (and recover_1_1 (<= (+ x_1_0 (* 0.9 dt_0)) x_1_1)) (<= x_1_1 (+ x_1_0 (* 1.1 dt_0)))) (< x_1_0 10000)) (< x_1_1 10000)))


	:assumption
	(or  (not out_1_0) (or out_1_1 in_1_1)) 
	:assumption
	(or  (not in_1_0) (or in_1_1 recover_1_1)) 
	:assumption
	(or  (not recover_1_0) (or out_1_1 recover_1_1)) 

	:assumption
( and ( and ( and ( or (not out_1_1) (not in_1_1))( or (not out_1_1) (not recover_1_1)))( or (not in_1_1) (not recover_1_1)))true ) 

	:assumption
	(or(not (and (and jump_0 out_2_0) add_2_0) ) in_2_1 )
	:assumption
	(or (not (and (and jump_0 out_2_0) in_2_1)) (and (and ( and  add_2_0 (not remove_2_0)) (> x_2_0 1)) (= x_2_1 0)))

	:assumption
	(or(not (and (and jump_0 in_2_0) remove_2_0) ) recover_2_1 )
	:assumption
	(or (not (and (and jump_0 in_2_0) recover_2_1)) (and ( and remove_2_0 (not add_2_0)) (= x_2_1 0)))

	:assumption
	(or(not (and jump_0 recover_2_0)  ) (or out_2_1 recover_2_1 ))
	:assumption
	(or (not (and (and jump_0 recover_2_0) out_2_1)) (and (and ( and (not add_2_0) (not remove_2_0)) (< x_2_0 10000)) (= x_2_1 x_2_0)))

	:assumption
	(or(not (and (and jump_0 out_2_0) out_2_1)) ( and (and (not add_2_0) (not remove_2_0) )  (= x_2_1 x_2_0)))

	:assumption
	(or(not (and (and jump_0 in_2_0) in_2_1)) ( and (and (not add_2_0) (not remove_2_0) )  (= x_2_1 x_2_0)))

	:assumption
	(or(not (and (and jump_0 recover_2_0) recover_2_1)) ( and (and (not add_2_0) (not remove_2_0) )  (= x_2_1 x_2_0)))

	:assumption
	(or (not (and (not jump_0) out_2_0)) (and ( and (and (and out_2_1 (<= (+ x_2_0 (* 0.9 dt_0)) x_2_1)) (<= x_2_1 (+ x_2_0 (* 1.1 dt_0))))  (< x_2_0 10000)) (< x_2_1 10000)))

	:assumption
	(or (not (and (not jump_0) in_2_0)) (and ( and (and (and in_2_1 (<= (+ x_2_0 (* 0.9 dt_0)) x_2_1)) (<= x_2_1 (+ x_2_0 (* 1.1 dt_0)))) (< x_2_0 10000)) (< x_2_1 10000)))

	:assumption
	(or (not (and (not jump_0) recover_2_0)) (and ( and (and (and recover_2_1 (<= (+ x_2_0 (* 0.9 dt_0)) x_2_1)) (<= x_2_1 (+ x_2_0 (* 1.1 dt_0)))) (< x_2_0 10000)) (< x_2_1 10000)))


	:assumption
	(or  (not out_2_0) (or out_2_1 in_2_1)) 
	:assumption
	(or  (not in_2_0) (or in_2_1 recover_2_1)) 
	:assumption
	(or  (not recover_2_0) (or out_2_1 recover_2_1)) 

	:assumption
( and ( and ( and ( or (not out_2_1) (not in_2_1))( or (not out_2_1) (not recover_2_1)))( or (not in_2_1) (not recover_2_1)))true ) 

	:assumption
	(or(not (and (and jump_1 out_1_1) add_1_1) ) in_1_2 )
	:assumption
	(or (not (and (and jump_1 out_1_1) in_1_2)) (and (and ( and  add_1_1 (not remove_1_1)) (> x_1_1 1)) (= x_1_2 0)))

	:assumption
	(or(not (and (and jump_1 in_1_1) remove_1_1) ) recover_1_2 )
	:assumption
	(or (not (and (and jump_1 in_1_1) recover_1_2)) (and ( and remove_1_1 (not add_1_1)) (= x_1_2 0)))

	:assumption
	(or(not (and jump_1 recover_1_1)  ) (or out_1_2 recover_1_2 ))
	:assumption
	(or (not (and (and jump_1 recover_1_1) out_1_2)) (and (and ( and (not add_1_1) (not remove_1_1)) (< x_1_1 10000)) (= x_1_2 x_1_1)))

	:assumption
	(or(not (and (and jump_1 out_1_1) out_1_2)) ( and (and (not add_1_1) (not remove_1_1) )  (= x_1_2 x_1_1)))

	:assumption
	(or(not (and (and jump_1 in_1_1) in_1_2)) ( and (and (not add_1_1) (not remove_1_1) )  (= x_1_2 x_1_1)))

	:assumption
	(or(not (and (and jump_1 recover_1_1) recover_1_2)) ( and (and (not add_1_1) (not remove_1_1) )  (= x_1_2 x_1_1)))

	:assumption
	(or (not (and (not jump_1) out_1_1)) (and ( and (and (and out_1_2 (<= (+ x_1_1 (* 0.9 dt_1)) x_1_2)) (<= x_1_2 (+ x_1_1 (* 1.1 dt_1))))  (< x_1_1 10000)) (< x_1_2 10000)))

	:assumption
	(or (not (and (not jump_1) in_1_1)) (and ( and (and (and in_1_2 (<= (+ x_1_1 (* 0.9 dt_1)) x_1_2)) (<= x_1_2 (+ x_1_1 (* 1.1 dt_1)))) (< x_1_1 10000)) (< x_1_2 10000)))

	:assumption
	(or (not (and (not jump_1) recover_1_1)) (and ( and (and (and recover_1_2 (<= (+ x_1_1 (* 0.9 dt_1)) x_1_2)) (<= x_1_2 (+ x_1_1 (* 1.1 dt_1)))) (< x_1_1 10000)) (< x_1_2 10000)))


	:assumption
	(or  (not out_1_1) (or out_1_2 in_1_2)) 
	:assumption
	(or  (not in_1_1) (or in_1_2 recover_1_2)) 
	:assumption
	(or  (not recover_1_1) (or out_1_2 recover_1_2)) 

	:assumption
( and ( and ( and ( or (not out_1_2) (not in_1_2))( or (not out_1_2) (not recover_1_2)))( or (not in_1_2) (not recover_1_2)))true ) 

	:assumption
	(or(not (and (and jump_1 out_2_1) add_2_1) ) in_2_2 )
	:assumption
	(or (not (and (and jump_1 out_2_1) in_2_2)) (and (and ( and  add_2_1 (not remove_2_1)) (> x_2_1 1)) (= x_2_2 0)))

	:assumption
	(or(not (and (and jump_1 in_2_1) remove_2_1) ) recover_2_2 )
	:assumption
	(or (not (and (and jump_1 in_2_1) recover_2_2)) (and ( and remove_2_1 (not add_2_1)) (= x_2_2 0)))

	:assumption
	(or(not (and jump_1 recover_2_1)  ) (or out_2_2 recover_2_2 ))
	:assumption
	(or (not (and (and jump_1 recover_2_1) out_2_2)) (and (and ( and (not add_2_1) (not remove_2_1)) (< x_2_1 10000)) (= x_2_2 x_2_1)))

	:assumption
	(or(not (and (and jump_1 out_2_1) out_2_2)) ( and (and (not add_2_1) (not remove_2_1) )  (= x_2_2 x_2_1)))

	:assumption
	(or(not (and (and jump_1 in_2_1) in_2_2)) ( and (and (not add_2_1) (not remove_2_1) )  (= x_2_2 x_2_1)))

	:assumption
	(or(not (and (and jump_1 recover_2_1) recover_2_2)) ( and (and (not add_2_1) (not remove_2_1) )  (= x_2_2 x_2_1)))

	:assumption
	(or (not (and (not jump_1) out_2_1)) (and ( and (and (and out_2_2 (<= (+ x_2_1 (* 0.9 dt_1)) x_2_2)) (<= x_2_2 (+ x_2_1 (* 1.1 dt_1))))  (< x_2_1 10000)) (< x_2_2 10000)))

	:assumption
	(or (not (and (not jump_1) in_2_1)) (and ( and (and (and in_2_2 (<= (+ x_2_1 (* 0.9 dt_1)) x_2_2)) (<= x_2_2 (+ x_2_1 (* 1.1 dt_1)))) (< x_2_1 10000)) (< x_2_2 10000)))

	:assumption
	(or (not (and (not jump_1) recover_2_1)) (and ( and (and (and recover_2_2 (<= (+ x_2_1 (* 0.9 dt_1)) x_2_2)) (<= x_2_2 (+ x_2_1 (* 1.1 dt_1)))) (< x_2_1 10000)) (< x_2_2 10000)))


	:assumption
	(or  (not out_2_1) (or out_2_2 in_2_2)) 
	:assumption
	(or  (not in_2_1) (or in_2_2 recover_2_2)) 
	:assumption
	(or  (not recover_2_1) (or out_2_2 recover_2_2)) 

	:assumption
( and ( and ( and ( or (not out_2_2) (not in_2_2))( or (not out_2_2) (not recover_2_2)))( or (not in_2_2) (not recover_2_2)))true ) 

	:assumption
	(or(not (and (and jump_2 out_1_2) add_1_2) ) in_1_3 )
	:assumption
	(or (not (and (and jump_2 out_1_2) in_1_3)) (and (and ( and  add_1_2 (not remove_1_2)) (> x_1_2 1)) (= x_1_3 0)))

	:assumption
	(or(not (and (and jump_2 in_1_2) remove_1_2) ) recover_1_3 )
	:assumption
	(or (not (and (and jump_2 in_1_2) recover_1_3)) (and ( and remove_1_2 (not add_1_2)) (= x_1_3 0)))

	:assumption
	(or(not (and jump_2 recover_1_2)  ) (or out_1_3 recover_1_3 ))
	:assumption
	(or (not (and (and jump_2 recover_1_2) out_1_3)) (and (and ( and (not add_1_2) (not remove_1_2)) (< x_1_2 10000)) (= x_1_3 x_1_2)))

	:assumption
	(or(not (and (and jump_2 out_1_2) out_1_3)) ( and (and (not add_1_2) (not remove_1_2) )  (= x_1_3 x_1_2)))

	:assumption
	(or(not (and (and jump_2 in_1_2) in_1_3)) ( and (and (not add_1_2) (not remove_1_2) )  (= x_1_3 x_1_2)))

	:assumption
	(or(not (and (and jump_2 recover_1_2) recover_1_3)) ( and (and (not add_1_2) (not remove_1_2) )  (= x_1_3 x_1_2)))

	:assumption
	(or (not (and (not jump_2) out_1_2)) (and ( and (and (and out_1_3 (<= (+ x_1_2 (* 0.9 dt_2)) x_1_3)) (<= x_1_3 (+ x_1_2 (* 1.1 dt_2))))  (< x_1_2 10000)) (< x_1_3 10000)))

	:assumption
	(or (not (and (not jump_2) in_1_2)) (and ( and (and (and in_1_3 (<= (+ x_1_2 (* 0.9 dt_2)) x_1_3)) (<= x_1_3 (+ x_1_2 (* 1.1 dt_2)))) (< x_1_2 10000)) (< x_1_3 10000)))

	:assumption
	(or (not (and (not jump_2) recover_1_2)) (and ( and (and (and recover_1_3 (<= (+ x_1_2 (* 0.9 dt_2)) x_1_3)) (<= x_1_3 (+ x_1_2 (* 1.1 dt_2)))) (< x_1_2 10000)) (< x_1_3 10000)))


	:assumption
	(or  (not out_1_2) (or out_1_3 in_1_3)) 
	:assumption
	(or  (not in_1_2) (or in_1_3 recover_1_3)) 
	:assumption
	(or  (not recover_1_2) (or out_1_3 recover_1_3)) 

	:assumption
( and ( and ( and ( or (not out_1_3) (not in_1_3))( or (not out_1_3) (not recover_1_3)))( or (not in_1_3) (not recover_1_3)))true ) 

	:assumption
	(or(not (and (and jump_2 out_2_2) add_2_2) ) in_2_3 )
	:assumption
	(or (not (and (and jump_2 out_2_2) in_2_3)) (and (and ( and  add_2_2 (not remove_2_2)) (> x_2_2 1)) (= x_2_3 0)))

	:assumption
	(or(not (and (and jump_2 in_2_2) remove_2_2) ) recover_2_3 )
	:assumption
	(or (not (and (and jump_2 in_2_2) recover_2_3)) (and ( and remove_2_2 (not add_2_2)) (= x_2_3 0)))

	:assumption
	(or(not (and jump_2 recover_2_2)  ) (or out_2_3 recover_2_3 ))
	:assumption
	(or (not (and (and jump_2 recover_2_2) out_2_3)) (and (and ( and (not add_2_2) (not remove_2_2)) (< x_2_2 10000)) (= x_2_3 x_2_2)))

	:assumption
	(or(not (and (and jump_2 out_2_2) out_2_3)) ( and (and (not add_2_2) (not remove_2_2) )  (= x_2_3 x_2_2)))

	:assumption
	(or(not (and (and jump_2 in_2_2) in_2_3)) ( and (and (not add_2_2) (not remove_2_2) )  (= x_2_3 x_2_2)))

	:assumption
	(or(not (and (and jump_2 recover_2_2) recover_2_3)) ( and (and (not add_2_2) (not remove_2_2) )  (= x_2_3 x_2_2)))

	:assumption
	(or (not (and (not jump_2) out_2_2)) (and ( and (and (and out_2_3 (<= (+ x_2_2 (* 0.9 dt_2)) x_2_3)) (<= x_2_3 (+ x_2_2 (* 1.1 dt_2))))  (< x_2_2 10000)) (< x_2_3 10000)))

	:assumption
	(or (not (and (not jump_2) in_2_2)) (and ( and (and (and in_2_3 (<= (+ x_2_2 (* 0.9 dt_2)) x_2_3)) (<= x_2_3 (+ x_2_2 (* 1.1 dt_2)))) (< x_2_2 10000)) (< x_2_3 10000)))

	:assumption
	(or (not (and (not jump_2) recover_2_2)) (and ( and (and (and recover_2_3 (<= (+ x_2_2 (* 0.9 dt_2)) x_2_3)) (<= x_2_3 (+ x_2_2 (* 1.1 dt_2)))) (< x_2_2 10000)) (< x_2_3 10000)))


	:assumption
	(or  (not out_2_2) (or out_2_3 in_2_3)) 
	:assumption
	(or  (not in_2_2) (or in_2_3 recover_2_3)) 
	:assumption
	(or  (not recover_2_2) (or out_2_3 recover_2_3)) 

	:assumption
( and ( and ( and ( or (not out_2_3) (not in_2_3))( or (not out_2_3) (not recover_2_3)))( or (not in_2_3) (not recover_2_3)))true ) 

	:assumption
	(or(not (and (and jump_3 out_1_3) add_1_3) ) in_1_4 )
	:assumption
	(or (not (and (and jump_3 out_1_3) in_1_4)) (and (and ( and  add_1_3 (not remove_1_3)) (> x_1_3 1)) (= x_1_4 0)))

	:assumption
	(or(not (and (and jump_3 in_1_3) remove_1_3) ) recover_1_4 )
	:assumption
	(or (not (and (and jump_3 in_1_3) recover_1_4)) (and ( and remove_1_3 (not add_1_3)) (= x_1_4 0)))

	:assumption
	(or(not (and jump_3 recover_1_3)  ) (or out_1_4 recover_1_4 ))
	:assumption
	(or (not (and (and jump_3 recover_1_3) out_1_4)) (and (and ( and (not add_1_3) (not remove_1_3)) (< x_1_3 10000)) (= x_1_4 x_1_3)))

	:assumption
	(or(not (and (and jump_3 out_1_3) out_1_4)) ( and (and (not add_1_3) (not remove_1_3) )  (= x_1_4 x_1_3)))

	:assumption
	(or(not (and (and jump_3 in_1_3) in_1_4)) ( and (and (not add_1_3) (not remove_1_3) )  (= x_1_4 x_1_3)))

	:assumption
	(or(not (and (and jump_3 recover_1_3) recover_1_4)) ( and (and (not add_1_3) (not remove_1_3) )  (= x_1_4 x_1_3)))

	:assumption
	(or (not (and (not jump_3) out_1_3)) (and ( and (and (and out_1_4 (<= (+ x_1_3 (* 0.9 dt_3)) x_1_4)) (<= x_1_4 (+ x_1_3 (* 1.1 dt_3))))  (< x_1_3 10000)) (< x_1_4 10000)))

	:assumption
	(or (not (and (not jump_3) in_1_3)) (and ( and (and (and in_1_4 (<= (+ x_1_3 (* 0.9 dt_3)) x_1_4)) (<= x_1_4 (+ x_1_3 (* 1.1 dt_3)))) (< x_1_3 10000)) (< x_1_4 10000)))

	:assumption
	(or (not (and (not jump_3) recover_1_3)) (and ( and (and (and recover_1_4 (<= (+ x_1_3 (* 0.9 dt_3)) x_1_4)) (<= x_1_4 (+ x_1_3 (* 1.1 dt_3)))) (< x_1_3 10000)) (< x_1_4 10000)))


	:assumption
	(or  (not out_1_3) (or out_1_4 in_1_4)) 
	:assumption
	(or  (not in_1_3) (or in_1_4 recover_1_4)) 
	:assumption
	(or  (not recover_1_3) (or out_1_4 recover_1_4)) 

	:assumption
( and ( and ( and ( or (not out_1_4) (not in_1_4))( or (not out_1_4) (not recover_1_4)))( or (not in_1_4) (not recover_1_4)))true ) 

	:assumption
	(or(not (and (and jump_3 out_2_3) add_2_3) ) in_2_4 )
	:assumption
	(or (not (and (and jump_3 out_2_3) in_2_4)) (and (and ( and  add_2_3 (not remove_2_3)) (> x_2_3 1)) (= x_2_4 0)))

	:assumption
	(or(not (and (and jump_3 in_2_3) remove_2_3) ) recover_2_4 )
	:assumption
	(or (not (and (and jump_3 in_2_3) recover_2_4)) (and ( and remove_2_3 (not add_2_3)) (= x_2_4 0)))

	:assumption
	(or(not (and jump_3 recover_2_3)  ) (or out_2_4 recover_2_4 ))
	:assumption
	(or (not (and (and jump_3 recover_2_3) out_2_4)) (and (and ( and (not add_2_3) (not remove_2_3)) (< x_2_3 10000)) (= x_2_4 x_2_3)))

	:assumption
	(or(not (and (and jump_3 out_2_3) out_2_4)) ( and (and (not add_2_3) (not remove_2_3) )  (= x_2_4 x_2_3)))

	:assumption
	(or(not (and (and jump_3 in_2_3) in_2_4)) ( and (and (not add_2_3) (not remove_2_3) )  (= x_2_4 x_2_3)))

	:assumption
	(or(not (and (and jump_3 recover_2_3) recover_2_4)) ( and (and (not add_2_3) (not remove_2_3) )  (= x_2_4 x_2_3)))

	:assumption
	(or (not (and (not jump_3) out_2_3)) (and ( and (and (and out_2_4 (<= (+ x_2_3 (* 0.9 dt_3)) x_2_4)) (<= x_2_4 (+ x_2_3 (* 1.1 dt_3))))  (< x_2_3 10000)) (< x_2_4 10000)))

	:assumption
	(or (not (and (not jump_3) in_2_3)) (and ( and (and (and in_2_4 (<= (+ x_2_3 (* 0.9 dt_3)) x_2_4)) (<= x_2_4 (+ x_2_3 (* 1.1 dt_3)))) (< x_2_3 10000)) (< x_2_4 10000)))

	:assumption
	(or (not (and (not jump_3) recover_2_3)) (and ( and (and (and recover_2_4 (<= (+ x_2_3 (* 0.9 dt_3)) x_2_4)) (<= x_2_4 (+ x_2_3 (* 1.1 dt_3)))) (< x_2_3 10000)) (< x_2_4 10000)))


	:assumption
	(or  (not out_2_3) (or out_2_4 in_2_4)) 
	:assumption
	(or  (not in_2_3) (or in_2_4 recover_2_4)) 
	:assumption
	(or  (not recover_2_3) (or out_2_4 recover_2_4)) 

	:assumption
( and ( and ( and ( or (not out_2_4) (not in_2_4))( or (not out_2_4) (not recover_2_4)))( or (not in_2_4) (not recover_2_4)))true ) 

	:assumption
	(or(not (and (and jump_4 out_1_4) add_1_4) ) in_1_5 )
	:assumption
	(or (not (and (and jump_4 out_1_4) in_1_5)) (and (and ( and  add_1_4 (not remove_1_4)) (> x_1_4 1)) (= x_1_5 0)))

	:assumption
	(or(not (and (and jump_4 in_1_4) remove_1_4) ) recover_1_5 )
	:assumption
	(or (not (and (and jump_4 in_1_4) recover_1_5)) (and ( and remove_1_4 (not add_1_4)) (= x_1_5 0)))

	:assumption
	(or(not (and jump_4 recover_1_4)  ) (or out_1_5 recover_1_5 ))
	:assumption
	(or (not (and (and jump_4 recover_1_4) out_1_5)) (and (and ( and (not add_1_4) (not remove_1_4)) (< x_1_4 10000)) (= x_1_5 x_1_4)))

	:assumption
	(or(not (and (and jump_4 out_1_4) out_1_5)) ( and (and (not add_1_4) (not remove_1_4) )  (= x_1_5 x_1_4)))

	:assumption
	(or(not (and (and jump_4 in_1_4) in_1_5)) ( and (and (not add_1_4) (not remove_1_4) )  (= x_1_5 x_1_4)))

	:assumption
	(or(not (and (and jump_4 recover_1_4) recover_1_5)) ( and (and (not add_1_4) (not remove_1_4) )  (= x_1_5 x_1_4)))

	:assumption
	(or (not (and (not jump_4) out_1_4)) (and ( and (and (and out_1_5 (<= (+ x_1_4 (* 0.9 dt_4)) x_1_5)) (<= x_1_5 (+ x_1_4 (* 1.1 dt_4))))  (< x_1_4 10000)) (< x_1_5 10000)))

	:assumption
	(or (not (and (not jump_4) in_1_4)) (and ( and (and (and in_1_5 (<= (+ x_1_4 (* 0.9 dt_4)) x_1_5)) (<= x_1_5 (+ x_1_4 (* 1.1 dt_4)))) (< x_1_4 10000)) (< x_1_5 10000)))

	:assumption
	(or (not (and (not jump_4) recover_1_4)) (and ( and (and (and recover_1_5 (<= (+ x_1_4 (* 0.9 dt_4)) x_1_5)) (<= x_1_5 (+ x_1_4 (* 1.1 dt_4)))) (< x_1_4 10000)) (< x_1_5 10000)))


	:assumption
	(or  (not out_1_4) (or out_1_5 in_1_5)) 
	:assumption
	(or  (not in_1_4) (or in_1_5 recover_1_5)) 
	:assumption
	(or  (not recover_1_4) (or out_1_5 recover_1_5)) 

	:assumption
( and ( and ( and ( or (not out_1_5) (not in_1_5))( or (not out_1_5) (not recover_1_5)))( or (not in_1_5) (not recover_1_5)))true ) 

	:assumption
	(or(not (and (and jump_4 out_2_4) add_2_4) ) in_2_5 )
	:assumption
	(or (not (and (and jump_4 out_2_4) in_2_5)) (and (and ( and  add_2_4 (not remove_2_4)) (> x_2_4 1)) (= x_2_5 0)))

	:assumption
	(or(not (and (and jump_4 in_2_4) remove_2_4) ) recover_2_5 )
	:assumption
	(or (not (and (and jump_4 in_2_4) recover_2_5)) (and ( and remove_2_4 (not add_2_4)) (= x_2_5 0)))

	:assumption
	(or(not (and jump_4 recover_2_4)  ) (or out_2_5 recover_2_5 ))
	:assumption
	(or (not (and (and jump_4 recover_2_4) out_2_5)) (and (and ( and (not add_2_4) (not remove_2_4)) (< x_2_4 10000)) (= x_2_5 x_2_4)))

	:assumption
	(or(not (and (and jump_4 out_2_4) out_2_5)) ( and (and (not add_2_4) (not remove_2_4) )  (= x_2_5 x_2_4)))

	:assumption
	(or(not (and (and jump_4 in_2_4) in_2_5)) ( and (and (not add_2_4) (not remove_2_4) )  (= x_2_5 x_2_4)))

	:assumption
	(or(not (and (and jump_4 recover_2_4) recover_2_5)) ( and (and (not add_2_4) (not remove_2_4) )  (= x_2_5 x_2_4)))

	:assumption
	(or (not (and (not jump_4) out_2_4)) (and ( and (and (and out_2_5 (<= (+ x_2_4 (* 0.9 dt_4)) x_2_5)) (<= x_2_5 (+ x_2_4 (* 1.1 dt_4))))  (< x_2_4 10000)) (< x_2_5 10000)))

	:assumption
	(or (not (and (not jump_4) in_2_4)) (and ( and (and (and in_2_5 (<= (+ x_2_4 (* 0.9 dt_4)) x_2_5)) (<= x_2_5 (+ x_2_4 (* 1.1 dt_4)))) (< x_2_4 10000)) (< x_2_5 10000)))

	:assumption
	(or (not (and (not jump_4) recover_2_4)) (and ( and (and (and recover_2_5 (<= (+ x_2_4 (* 0.9 dt_4)) x_2_5)) (<= x_2_5 (+ x_2_4 (* 1.1 dt_4)))) (< x_2_4 10000)) (< x_2_5 10000)))


	:assumption
	(or  (not out_2_4) (or out_2_5 in_2_5)) 
	:assumption
	(or  (not in_2_4) (or in_2_5 recover_2_5)) 
	:assumption
	(or  (not recover_2_4) (or out_2_5 recover_2_5)) 

	:assumption
( and ( and ( and ( or (not out_2_5) (not in_2_5))( or (not out_2_5) (not recover_2_5)))( or (not in_2_5) (not recover_2_5)))true ) 

	:assumption
	(or(not (and (and jump_5 out_1_5) add_1_5) ) in_1_6 )
	:assumption
	(or (not (and (and jump_5 out_1_5) in_1_6)) (and (and ( and  add_1_5 (not remove_1_5)) (> x_1_5 1)) (= x_1_6 0)))

	:assumption
	(or(not (and (and jump_5 in_1_5) remove_1_5) ) recover_1_6 )
	:assumption
	(or (not (and (and jump_5 in_1_5) recover_1_6)) (and ( and remove_1_5 (not add_1_5)) (= x_1_6 0)))

	:assumption
	(or(not (and jump_5 recover_1_5)  ) (or out_1_6 recover_1_6 ))
	:assumption
	(or (not (and (and jump_5 recover_1_5) out_1_6)) (and (and ( and (not add_1_5) (not remove_1_5)) (< x_1_5 10000)) (= x_1_6 x_1_5)))

	:assumption
	(or(not (and (and jump_5 out_1_5) out_1_6)) ( and (and (not add_1_5) (not remove_1_5) )  (= x_1_6 x_1_5)))

	:assumption
	(or(not (and (and jump_5 in_1_5) in_1_6)) ( and (and (not add_1_5) (not remove_1_5) )  (= x_1_6 x_1_5)))

	:assumption
	(or(not (and (and jump_5 recover_1_5) recover_1_6)) ( and (and (not add_1_5) (not remove_1_5) )  (= x_1_6 x_1_5)))

	:assumption
	(or (not (and (not jump_5) out_1_5)) (and ( and (and (and out_1_6 (<= (+ x_1_5 (* 0.9 dt_5)) x_1_6)) (<= x_1_6 (+ x_1_5 (* 1.1 dt_5))))  (< x_1_5 10000)) (< x_1_6 10000)))

	:assumption
	(or (not (and (not jump_5) in_1_5)) (and ( and (and (and in_1_6 (<= (+ x_1_5 (* 0.9 dt_5)) x_1_6)) (<= x_1_6 (+ x_1_5 (* 1.1 dt_5)))) (< x_1_5 10000)) (< x_1_6 10000)))

	:assumption
	(or (not (and (not jump_5) recover_1_5)) (and ( and (and (and recover_1_6 (<= (+ x_1_5 (* 0.9 dt_5)) x_1_6)) (<= x_1_6 (+ x_1_5 (* 1.1 dt_5)))) (< x_1_5 10000)) (< x_1_6 10000)))


	:assumption
	(or  (not out_1_5) (or out_1_6 in_1_6)) 
	:assumption
	(or  (not in_1_5) (or in_1_6 recover_1_6)) 
	:assumption
	(or  (not recover_1_5) (or out_1_6 recover_1_6)) 

	:assumption
( and ( and ( and ( or (not out_1_6) (not in_1_6))( or (not out_1_6) (not recover_1_6)))( or (not in_1_6) (not recover_1_6)))true ) 

	:assumption
	(or(not (and (and jump_5 out_2_5) add_2_5) ) in_2_6 )
	:assumption
	(or (not (and (and jump_5 out_2_5) in_2_6)) (and (and ( and  add_2_5 (not remove_2_5)) (> x_2_5 1)) (= x_2_6 0)))

	:assumption
	(or(not (and (and jump_5 in_2_5) remove_2_5) ) recover_2_6 )
	:assumption
	(or (not (and (and jump_5 in_2_5) recover_2_6)) (and ( and remove_2_5 (not add_2_5)) (= x_2_6 0)))

	:assumption
	(or(not (and jump_5 recover_2_5)  ) (or out_2_6 recover_2_6 ))
	:assumption
	(or (not (and (and jump_5 recover_2_5) out_2_6)) (and (and ( and (not add_2_5) (not remove_2_5)) (< x_2_5 10000)) (= x_2_6 x_2_5)))

	:assumption
	(or(not (and (and jump_5 out_2_5) out_2_6)) ( and (and (not add_2_5) (not remove_2_5) )  (= x_2_6 x_2_5)))

	:assumption
	(or(not (and (and jump_5 in_2_5) in_2_6)) ( and (and (not add_2_5) (not remove_2_5) )  (= x_2_6 x_2_5)))

	:assumption
	(or(not (and (and jump_5 recover_2_5) recover_2_6)) ( and (and (not add_2_5) (not remove_2_5) )  (= x_2_6 x_2_5)))

	:assumption
	(or (not (and (not jump_5) out_2_5)) (and ( and (and (and out_2_6 (<= (+ x_2_5 (* 0.9 dt_5)) x_2_6)) (<= x_2_6 (+ x_2_5 (* 1.1 dt_5))))  (< x_2_5 10000)) (< x_2_6 10000)))

	:assumption
	(or (not (and (not jump_5) in_2_5)) (and ( and (and (and in_2_6 (<= (+ x_2_5 (* 0.9 dt_5)) x_2_6)) (<= x_2_6 (+ x_2_5 (* 1.1 dt_5)))) (< x_2_5 10000)) (< x_2_6 10000)))

	:assumption
	(or (not (and (not jump_5) recover_2_5)) (and ( and (and (and recover_2_6 (<= (+ x_2_5 (* 0.9 dt_5)) x_2_6)) (<= x_2_6 (+ x_2_5 (* 1.1 dt_5)))) (< x_2_5 10000)) (< x_2_6 10000)))


	:assumption
	(or  (not out_2_5) (or out_2_6 in_2_6)) 
	:assumption
	(or  (not in_2_5) (or in_2_6 recover_2_6)) 
	:assumption
	(or  (not recover_2_5) (or out_2_6 recover_2_6)) 

	:assumption
( and ( and ( and ( or (not out_2_6) (not in_2_6))( or (not out_2_6) (not recover_2_6)))( or (not in_2_6) (not recover_2_6)))true ) 

	:assumption
	(or(not (and (and jump_6 out_1_6) add_1_6) ) in_1_7 )
	:assumption
	(or (not (and (and jump_6 out_1_6) in_1_7)) (and (and ( and  add_1_6 (not remove_1_6)) (> x_1_6 1)) (= x_1_7 0)))

	:assumption
	(or(not (and (and jump_6 in_1_6) remove_1_6) ) recover_1_7 )
	:assumption
	(or (not (and (and jump_6 in_1_6) recover_1_7)) (and ( and remove_1_6 (not add_1_6)) (= x_1_7 0)))

	:assumption
	(or(not (and jump_6 recover_1_6)  ) (or out_1_7 recover_1_7 ))
	:assumption
	(or (not (and (and jump_6 recover_1_6) out_1_7)) (and (and ( and (not add_1_6) (not remove_1_6)) (< x_1_6 10000)) (= x_1_7 x_1_6)))

	:assumption
	(or(not (and (and jump_6 out_1_6) out_1_7)) ( and (and (not add_1_6) (not remove_1_6) )  (= x_1_7 x_1_6)))

	:assumption
	(or(not (and (and jump_6 in_1_6) in_1_7)) ( and (and (not add_1_6) (not remove_1_6) )  (= x_1_7 x_1_6)))

	:assumption
	(or(not (and (and jump_6 recover_1_6) recover_1_7)) ( and (and (not add_1_6) (not remove_1_6) )  (= x_1_7 x_1_6)))

	:assumption
	(or (not (and (not jump_6) out_1_6)) (and ( and (and (and out_1_7 (<= (+ x_1_6 (* 0.9 dt_6)) x_1_7)) (<= x_1_7 (+ x_1_6 (* 1.1 dt_6))))  (< x_1_6 10000)) (< x_1_7 10000)))

	:assumption
	(or (not (and (not jump_6) in_1_6)) (and ( and (and (and in_1_7 (<= (+ x_1_6 (* 0.9 dt_6)) x_1_7)) (<= x_1_7 (+ x_1_6 (* 1.1 dt_6)))) (< x_1_6 10000)) (< x_1_7 10000)))

	:assumption
	(or (not (and (not jump_6) recover_1_6)) (and ( and (and (and recover_1_7 (<= (+ x_1_6 (* 0.9 dt_6)) x_1_7)) (<= x_1_7 (+ x_1_6 (* 1.1 dt_6)))) (< x_1_6 10000)) (< x_1_7 10000)))


	:assumption
	(or  (not out_1_6) (or out_1_7 in_1_7)) 
	:assumption
	(or  (not in_1_6) (or in_1_7 recover_1_7)) 
	:assumption
	(or  (not recover_1_6) (or out_1_7 recover_1_7)) 

	:assumption
( and ( and ( and ( or (not out_1_7) (not in_1_7))( or (not out_1_7) (not recover_1_7)))( or (not in_1_7) (not recover_1_7)))true ) 

	:assumption
	(or(not (and (and jump_6 out_2_6) add_2_6) ) in_2_7 )
	:assumption
	(or (not (and (and jump_6 out_2_6) in_2_7)) (and (and ( and  add_2_6 (not remove_2_6)) (> x_2_6 1)) (= x_2_7 0)))

	:assumption
	(or(not (and (and jump_6 in_2_6) remove_2_6) ) recover_2_7 )
	:assumption
	(or (not (and (and jump_6 in_2_6) recover_2_7)) (and ( and remove_2_6 (not add_2_6)) (= x_2_7 0)))

	:assumption
	(or(not (and jump_6 recover_2_6)  ) (or out_2_7 recover_2_7 ))
	:assumption
	(or (not (and (and jump_6 recover_2_6) out_2_7)) (and (and ( and (not add_2_6) (not remove_2_6)) (< x_2_6 10000)) (= x_2_7 x_2_6)))

	:assumption
	(or(not (and (and jump_6 out_2_6) out_2_7)) ( and (and (not add_2_6) (not remove_2_6) )  (= x_2_7 x_2_6)))

	:assumption
	(or(not (and (and jump_6 in_2_6) in_2_7)) ( and (and (not add_2_6) (not remove_2_6) )  (= x_2_7 x_2_6)))

	:assumption
	(or(not (and (and jump_6 recover_2_6) recover_2_7)) ( and (and (not add_2_6) (not remove_2_6) )  (= x_2_7 x_2_6)))

	:assumption
	(or (not (and (not jump_6) out_2_6)) (and ( and (and (and out_2_7 (<= (+ x_2_6 (* 0.9 dt_6)) x_2_7)) (<= x_2_7 (+ x_2_6 (* 1.1 dt_6))))  (< x_2_6 10000)) (< x_2_7 10000)))

	:assumption
	(or (not (and (not jump_6) in_2_6)) (and ( and (and (and in_2_7 (<= (+ x_2_6 (* 0.9 dt_6)) x_2_7)) (<= x_2_7 (+ x_2_6 (* 1.1 dt_6)))) (< x_2_6 10000)) (< x_2_7 10000)))

	:assumption
	(or (not (and (not jump_6) recover_2_6)) (and ( and (and (and recover_2_7 (<= (+ x_2_6 (* 0.9 dt_6)) x_2_7)) (<= x_2_7 (+ x_2_6 (* 1.1 dt_6)))) (< x_2_6 10000)) (< x_2_7 10000)))


	:assumption
	(or  (not out_2_6) (or out_2_7 in_2_7)) 
	:assumption
	(or  (not in_2_6) (or in_2_7 recover_2_7)) 
	:assumption
	(or  (not recover_2_6) (or out_2_7 recover_2_7)) 

	:assumption
( and ( and ( and ( or (not out_2_7) (not in_2_7))( or (not out_2_7) (not recover_2_7)))( or (not in_2_7) (not recover_2_7)))true ) 

	:assumption
	(or(not (and (and jump_0 rod_0_0) add_1_0) ) rod_1_1 )  
	:assumption
	(or (not (and (and jump_0 rod_0_0) rod_1_1))( and ( and ( and ( and ( and ( and  ( and true add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  (>= x_3_0 16.0 ) )  (<= x_3_0 16.1 ) )  (= x_3_1 0 ) )  )
 	:assumption
	(or(not (and (and jump_0 rod_1_0) remove_1_0) ) rod_0_1 )  
	:assumption
	(or (not (and (and jump_0 rod_1_0) rod_0_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( and true remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  (>= x_3_0 5.0 ) )  (<= x_3_0 5.9 ) )  (= x_3_1 0 ) )  )
 	:assumption
	(or(not (and (and jump_0 rod_0_0) add_2_0) ) rod_2_1 )  
	:assumption
	(or (not (and (and jump_0 rod_0_0) rod_2_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( and true add_2_0) )  ( not remove_2_0) )  (>= x_3_0 16.0 ) )  (<= x_3_0 16.1 ) )  (= x_3_1 0 ) )  )
 	:assumption
	(or(not (and (and jump_0 rod_2_0) remove_2_0) ) rod_0_1 )  
	:assumption
	(or (not (and (and jump_0 rod_2_0) rod_0_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( and true remove_2_0) )  (>= x_3_0 5.0 ) )  (<= x_3_0 5.9 ) )  (= x_3_1 0 ) )  )
 	:assumption
	(or (not (and (and jump_0 rod_0_0) rod_0_1))( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  (= x_3_0 x_3_1) )  )
 	:assumption
	(or (not (and (and jump_0 rod_1_0) rod_1_1))( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  (= x_3_0 x_3_1) )  )
 	:assumption
	(or (not (and (and jump_0 rod_2_0) rod_2_1))( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  (= x_3_0 x_3_1) )  )
 
	:assumption
	(or (not (and (not jump_0) rod_0_0)) (and ( and (and (and rod_0_1 (<= (+ x_3_0 (* 0.9 dt_0)) x_3_1)) (<= x_3_1 (+ x_3_0 (* 1.1 dt_0)))) (<= x_3_0 16.1)) (<= x_3_1 16.1)))

	:assumption
	(or (not (and (not jump_0) rod_1_0)) (and ( and (and (and rod_1_1 (<= (+ x_3_0 (* 0.9 dt_0)) x_3_1)) (<= x_3_1 (+ x_3_0 (* 1.1 dt_0)))) (<= x_3_0 5.9)) (<= x_3_1 5.9)))

	:assumption
	(or (not (and (not jump_0) rod_2_0)) (and ( and (and (and rod_2_1 (<= (+ x_3_0 (* 0.9 dt_0)) x_3_1)) (<= x_3_1 (+ x_3_0 (* 1.1 dt_0)))) (<= x_3_0 5.9)) (<= x_3_1 5.9)))

	:assumption
	(or  (not rod_0_0) ( or ( or  rod_0_1   rod_1_1  )  rod_2_1  ) ) 
	:assumption
	(or  (not rod_1_0) (or rod_0_1 rod_1_1)) 
	:assumption
	(or  (not rod_2_0) (or rod_0_1 rod_2_1)) 


	:assumption
( and ( and ( and ( or (not rod_0_1) (not rod_1_1))( or (not rod_0_1) (not rod_2_1)))( or (not rod_1_1) (not rod_2_1)))true ) 


	:assumption
	(or(not (and (and jump_1 rod_0_1) add_1_1) ) rod_1_2 )  
	:assumption
	(or (not (and (and jump_1 rod_0_1) rod_1_2))( and ( and ( and ( and ( and ( and  ( and true add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  (>= x_3_1 16.0 ) )  (<= x_3_1 16.1 ) )  (= x_3_2 0 ) )  )
 	:assumption
	(or(not (and (and jump_1 rod_1_1) remove_1_1) ) rod_0_2 )  
	:assumption
	(or (not (and (and jump_1 rod_1_1) rod_0_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( and true remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  (>= x_3_1 5.0 ) )  (<= x_3_1 5.9 ) )  (= x_3_2 0 ) )  )
 	:assumption
	(or(not (and (and jump_1 rod_0_1) add_2_1) ) rod_2_2 )  
	:assumption
	(or (not (and (and jump_1 rod_0_1) rod_2_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( and true add_2_1) )  ( not remove_2_1) )  (>= x_3_1 16.0 ) )  (<= x_3_1 16.1 ) )  (= x_3_2 0 ) )  )
 	:assumption
	(or(not (and (and jump_1 rod_2_1) remove_2_1) ) rod_0_2 )  
	:assumption
	(or (not (and (and jump_1 rod_2_1) rod_0_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( and true remove_2_1) )  (>= x_3_1 5.0 ) )  (<= x_3_1 5.9 ) )  (= x_3_2 0 ) )  )
 	:assumption
	(or (not (and (and jump_1 rod_0_1) rod_0_2))( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  (= x_3_1 x_3_2) )  )
 	:assumption
	(or (not (and (and jump_1 rod_1_1) rod_1_2))( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  (= x_3_1 x_3_2) )  )
 	:assumption
	(or (not (and (and jump_1 rod_2_1) rod_2_2))( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  (= x_3_1 x_3_2) )  )
 
	:assumption
	(or (not (and (not jump_1) rod_0_1)) (and ( and (and (and rod_0_2 (<= (+ x_3_1 (* 0.9 dt_1)) x_3_2)) (<= x_3_2 (+ x_3_1 (* 1.1 dt_1)))) (<= x_3_1 16.1)) (<= x_3_2 16.1)))

	:assumption
	(or (not (and (not jump_1) rod_1_1)) (and ( and (and (and rod_1_2 (<= (+ x_3_1 (* 0.9 dt_1)) x_3_2)) (<= x_3_2 (+ x_3_1 (* 1.1 dt_1)))) (<= x_3_1 5.9)) (<= x_3_2 5.9)))

	:assumption
	(or (not (and (not jump_1) rod_2_1)) (and ( and (and (and rod_2_2 (<= (+ x_3_1 (* 0.9 dt_1)) x_3_2)) (<= x_3_2 (+ x_3_1 (* 1.1 dt_1)))) (<= x_3_1 5.9)) (<= x_3_2 5.9)))

	:assumption
	(or  (not rod_0_1) ( or ( or  rod_0_2   rod_1_2  )  rod_2_2  ) ) 
	:assumption
	(or  (not rod_1_1) (or rod_0_2 rod_1_2)) 
	:assumption
	(or  (not rod_2_1) (or rod_0_2 rod_2_2)) 


	:assumption
( and ( and ( and ( or (not rod_0_2) (not rod_1_2))( or (not rod_0_2) (not rod_2_2)))( or (not rod_1_2) (not rod_2_2)))true ) 


	:assumption
	(or(not (and (and jump_2 rod_0_2) add_1_2) ) rod_1_3 )  
	:assumption
	(or (not (and (and jump_2 rod_0_2) rod_1_3))( and ( and ( and ( and ( and ( and  ( and true add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  (>= x_3_2 16.0 ) )  (<= x_3_2 16.1 ) )  (= x_3_3 0 ) )  )
 	:assumption
	(or(not (and (and jump_2 rod_1_2) remove_1_2) ) rod_0_3 )  
	:assumption
	(or (not (and (and jump_2 rod_1_2) rod_0_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( and true remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  (>= x_3_2 5.0 ) )  (<= x_3_2 5.9 ) )  (= x_3_3 0 ) )  )
 	:assumption
	(or(not (and (and jump_2 rod_0_2) add_2_2) ) rod_2_3 )  
	:assumption
	(or (not (and (and jump_2 rod_0_2) rod_2_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( and true add_2_2) )  ( not remove_2_2) )  (>= x_3_2 16.0 ) )  (<= x_3_2 16.1 ) )  (= x_3_3 0 ) )  )
 	:assumption
	(or(not (and (and jump_2 rod_2_2) remove_2_2) ) rod_0_3 )  
	:assumption
	(or (not (and (and jump_2 rod_2_2) rod_0_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( and true remove_2_2) )  (>= x_3_2 5.0 ) )  (<= x_3_2 5.9 ) )  (= x_3_3 0 ) )  )
 	:assumption
	(or (not (and (and jump_2 rod_0_2) rod_0_3))( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  (= x_3_2 x_3_3) )  )
 	:assumption
	(or (not (and (and jump_2 rod_1_2) rod_1_3))( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  (= x_3_2 x_3_3) )  )
 	:assumption
	(or (not (and (and jump_2 rod_2_2) rod_2_3))( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  (= x_3_2 x_3_3) )  )
 
	:assumption
	(or (not (and (not jump_2) rod_0_2)) (and ( and (and (and rod_0_3 (<= (+ x_3_2 (* 0.9 dt_2)) x_3_3)) (<= x_3_3 (+ x_3_2 (* 1.1 dt_2)))) (<= x_3_2 16.1)) (<= x_3_3 16.1)))

	:assumption
	(or (not (and (not jump_2) rod_1_2)) (and ( and (and (and rod_1_3 (<= (+ x_3_2 (* 0.9 dt_2)) x_3_3)) (<= x_3_3 (+ x_3_2 (* 1.1 dt_2)))) (<= x_3_2 5.9)) (<= x_3_3 5.9)))

	:assumption
	(or (not (and (not jump_2) rod_2_2)) (and ( and (and (and rod_2_3 (<= (+ x_3_2 (* 0.9 dt_2)) x_3_3)) (<= x_3_3 (+ x_3_2 (* 1.1 dt_2)))) (<= x_3_2 5.9)) (<= x_3_3 5.9)))

	:assumption
	(or  (not rod_0_2) ( or ( or  rod_0_3   rod_1_3  )  rod_2_3  ) ) 
	:assumption
	(or  (not rod_1_2) (or rod_0_3 rod_1_3)) 
	:assumption
	(or  (not rod_2_2) (or rod_0_3 rod_2_3)) 


	:assumption
( and ( and ( and ( or (not rod_0_3) (not rod_1_3))( or (not rod_0_3) (not rod_2_3)))( or (not rod_1_3) (not rod_2_3)))true ) 


	:assumption
	(or(not (and (and jump_3 rod_0_3) add_1_3) ) rod_1_4 )  
	:assumption
	(or (not (and (and jump_3 rod_0_3) rod_1_4))( and ( and ( and ( and ( and ( and  ( and true add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  (>= x_3_3 16.0 ) )  (<= x_3_3 16.1 ) )  (= x_3_4 0 ) )  )
 	:assumption
	(or(not (and (and jump_3 rod_1_3) remove_1_3) ) rod_0_4 )  
	:assumption
	(or (not (and (and jump_3 rod_1_3) rod_0_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( and true remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  (>= x_3_3 5.0 ) )  (<= x_3_3 5.9 ) )  (= x_3_4 0 ) )  )
 	:assumption
	(or(not (and (and jump_3 rod_0_3) add_2_3) ) rod_2_4 )  
	:assumption
	(or (not (and (and jump_3 rod_0_3) rod_2_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( and true add_2_3) )  ( not remove_2_3) )  (>= x_3_3 16.0 ) )  (<= x_3_3 16.1 ) )  (= x_3_4 0 ) )  )
 	:assumption
	(or(not (and (and jump_3 rod_2_3) remove_2_3) ) rod_0_4 )  
	:assumption
	(or (not (and (and jump_3 rod_2_3) rod_0_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( and true remove_2_3) )  (>= x_3_3 5.0 ) )  (<= x_3_3 5.9 ) )  (= x_3_4 0 ) )  )
 	:assumption
	(or (not (and (and jump_3 rod_0_3) rod_0_4))( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  (= x_3_3 x_3_4) )  )
 	:assumption
	(or (not (and (and jump_3 rod_1_3) rod_1_4))( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  (= x_3_3 x_3_4) )  )
 	:assumption
	(or (not (and (and jump_3 rod_2_3) rod_2_4))( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  (= x_3_3 x_3_4) )  )
 
	:assumption
	(or (not (and (not jump_3) rod_0_3)) (and ( and (and (and rod_0_4 (<= (+ x_3_3 (* 0.9 dt_3)) x_3_4)) (<= x_3_4 (+ x_3_3 (* 1.1 dt_3)))) (<= x_3_3 16.1)) (<= x_3_4 16.1)))

	:assumption
	(or (not (and (not jump_3) rod_1_3)) (and ( and (and (and rod_1_4 (<= (+ x_3_3 (* 0.9 dt_3)) x_3_4)) (<= x_3_4 (+ x_3_3 (* 1.1 dt_3)))) (<= x_3_3 5.9)) (<= x_3_4 5.9)))

	:assumption
	(or (not (and (not jump_3) rod_2_3)) (and ( and (and (and rod_2_4 (<= (+ x_3_3 (* 0.9 dt_3)) x_3_4)) (<= x_3_4 (+ x_3_3 (* 1.1 dt_3)))) (<= x_3_3 5.9)) (<= x_3_4 5.9)))

	:assumption
	(or  (not rod_0_3) ( or ( or  rod_0_4   rod_1_4  )  rod_2_4  ) ) 
	:assumption
	(or  (not rod_1_3) (or rod_0_4 rod_1_4)) 
	:assumption
	(or  (not rod_2_3) (or rod_0_4 rod_2_4)) 


	:assumption
( and ( and ( and ( or (not rod_0_4) (not rod_1_4))( or (not rod_0_4) (not rod_2_4)))( or (not rod_1_4) (not rod_2_4)))true ) 


	:assumption
	(or(not (and (and jump_4 rod_0_4) add_1_4) ) rod_1_5 )  
	:assumption
	(or (not (and (and jump_4 rod_0_4) rod_1_5))( and ( and ( and ( and ( and ( and  ( and true add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  (>= x_3_4 16.0 ) )  (<= x_3_4 16.1 ) )  (= x_3_5 0 ) )  )
 	:assumption
	(or(not (and (and jump_4 rod_1_4) remove_1_4) ) rod_0_5 )  
	:assumption
	(or (not (and (and jump_4 rod_1_4) rod_0_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( and true remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  (>= x_3_4 5.0 ) )  (<= x_3_4 5.9 ) )  (= x_3_5 0 ) )  )
 	:assumption
	(or(not (and (and jump_4 rod_0_4) add_2_4) ) rod_2_5 )  
	:assumption
	(or (not (and (and jump_4 rod_0_4) rod_2_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( and true add_2_4) )  ( not remove_2_4) )  (>= x_3_4 16.0 ) )  (<= x_3_4 16.1 ) )  (= x_3_5 0 ) )  )
 	:assumption
	(or(not (and (and jump_4 rod_2_4) remove_2_4) ) rod_0_5 )  
	:assumption
	(or (not (and (and jump_4 rod_2_4) rod_0_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( and true remove_2_4) )  (>= x_3_4 5.0 ) )  (<= x_3_4 5.9 ) )  (= x_3_5 0 ) )  )
 	:assumption
	(or (not (and (and jump_4 rod_0_4) rod_0_5))( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  (= x_3_4 x_3_5) )  )
 	:assumption
	(or (not (and (and jump_4 rod_1_4) rod_1_5))( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  (= x_3_4 x_3_5) )  )
 	:assumption
	(or (not (and (and jump_4 rod_2_4) rod_2_5))( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  (= x_3_4 x_3_5) )  )
 
	:assumption
	(or (not (and (not jump_4) rod_0_4)) (and ( and (and (and rod_0_5 (<= (+ x_3_4 (* 0.9 dt_4)) x_3_5)) (<= x_3_5 (+ x_3_4 (* 1.1 dt_4)))) (<= x_3_4 16.1)) (<= x_3_5 16.1)))

	:assumption
	(or (not (and (not jump_4) rod_1_4)) (and ( and (and (and rod_1_5 (<= (+ x_3_4 (* 0.9 dt_4)) x_3_5)) (<= x_3_5 (+ x_3_4 (* 1.1 dt_4)))) (<= x_3_4 5.9)) (<= x_3_5 5.9)))

	:assumption
	(or (not (and (not jump_4) rod_2_4)) (and ( and (and (and rod_2_5 (<= (+ x_3_4 (* 0.9 dt_4)) x_3_5)) (<= x_3_5 (+ x_3_4 (* 1.1 dt_4)))) (<= x_3_4 5.9)) (<= x_3_5 5.9)))

	:assumption
	(or  (not rod_0_4) ( or ( or  rod_0_5   rod_1_5  )  rod_2_5  ) ) 
	:assumption
	(or  (not rod_1_4) (or rod_0_5 rod_1_5)) 
	:assumption
	(or  (not rod_2_4) (or rod_0_5 rod_2_5)) 


	:assumption
( and ( and ( and ( or (not rod_0_5) (not rod_1_5))( or (not rod_0_5) (not rod_2_5)))( or (not rod_1_5) (not rod_2_5)))true ) 


	:assumption
	(or(not (and (and jump_5 rod_0_5) add_1_5) ) rod_1_6 )  
	:assumption
	(or (not (and (and jump_5 rod_0_5) rod_1_6))( and ( and ( and ( and ( and ( and  ( and true add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  (>= x_3_5 16.0 ) )  (<= x_3_5 16.1 ) )  (= x_3_6 0 ) )  )
 	:assumption
	(or(not (and (and jump_5 rod_1_5) remove_1_5) ) rod_0_6 )  
	:assumption
	(or (not (and (and jump_5 rod_1_5) rod_0_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( and true remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  (>= x_3_5 5.0 ) )  (<= x_3_5 5.9 ) )  (= x_3_6 0 ) )  )
 	:assumption
	(or(not (and (and jump_5 rod_0_5) add_2_5) ) rod_2_6 )  
	:assumption
	(or (not (and (and jump_5 rod_0_5) rod_2_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( and true add_2_5) )  ( not remove_2_5) )  (>= x_3_5 16.0 ) )  (<= x_3_5 16.1 ) )  (= x_3_6 0 ) )  )
 	:assumption
	(or(not (and (and jump_5 rod_2_5) remove_2_5) ) rod_0_6 )  
	:assumption
	(or (not (and (and jump_5 rod_2_5) rod_0_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( and true remove_2_5) )  (>= x_3_5 5.0 ) )  (<= x_3_5 5.9 ) )  (= x_3_6 0 ) )  )
 	:assumption
	(or (not (and (and jump_5 rod_0_5) rod_0_6))( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  (= x_3_5 x_3_6) )  )
 	:assumption
	(or (not (and (and jump_5 rod_1_5) rod_1_6))( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  (= x_3_5 x_3_6) )  )
 	:assumption
	(or (not (and (and jump_5 rod_2_5) rod_2_6))( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  (= x_3_5 x_3_6) )  )
 
	:assumption
	(or (not (and (not jump_5) rod_0_5)) (and ( and (and (and rod_0_6 (<= (+ x_3_5 (* 0.9 dt_5)) x_3_6)) (<= x_3_6 (+ x_3_5 (* 1.1 dt_5)))) (<= x_3_5 16.1)) (<= x_3_6 16.1)))

	:assumption
	(or (not (and (not jump_5) rod_1_5)) (and ( and (and (and rod_1_6 (<= (+ x_3_5 (* 0.9 dt_5)) x_3_6)) (<= x_3_6 (+ x_3_5 (* 1.1 dt_5)))) (<= x_3_5 5.9)) (<= x_3_6 5.9)))

	:assumption
	(or (not (and (not jump_5) rod_2_5)) (and ( and (and (and rod_2_6 (<= (+ x_3_5 (* 0.9 dt_5)) x_3_6)) (<= x_3_6 (+ x_3_5 (* 1.1 dt_5)))) (<= x_3_5 5.9)) (<= x_3_6 5.9)))

	:assumption
	(or  (not rod_0_5) ( or ( or  rod_0_6   rod_1_6  )  rod_2_6  ) ) 
	:assumption
	(or  (not rod_1_5) (or rod_0_6 rod_1_6)) 
	:assumption
	(or  (not rod_2_5) (or rod_0_6 rod_2_6)) 


	:assumption
( and ( and ( and ( or (not rod_0_6) (not rod_1_6))( or (not rod_0_6) (not rod_2_6)))( or (not rod_1_6) (not rod_2_6)))true ) 


	:assumption
	(or(not (and (and jump_6 rod_0_6) add_1_6) ) rod_1_7 )  
	:assumption
	(or (not (and (and jump_6 rod_0_6) rod_1_7))( and ( and ( and ( and ( and ( and  ( and true add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  (>= x_3_6 16.0 ) )  (<= x_3_6 16.1 ) )  (= x_3_7 0 ) )  )
 	:assumption
	(or(not (and (and jump_6 rod_1_6) remove_1_6) ) rod_0_7 )  
	:assumption
	(or (not (and (and jump_6 rod_1_6) rod_0_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( and true remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  (>= x_3_6 5.0 ) )  (<= x_3_6 5.9 ) )  (= x_3_7 0 ) )  )
 	:assumption
	(or(not (and (and jump_6 rod_0_6) add_2_6) ) rod_2_7 )  
	:assumption
	(or (not (and (and jump_6 rod_0_6) rod_2_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( and true add_2_6) )  ( not remove_2_6) )  (>= x_3_6 16.0 ) )  (<= x_3_6 16.1 ) )  (= x_3_7 0 ) )  )
 	:assumption
	(or(not (and (and jump_6 rod_2_6) remove_2_6) ) rod_0_7 )  
	:assumption
	(or (not (and (and jump_6 rod_2_6) rod_0_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( and true remove_2_6) )  (>= x_3_6 5.0 ) )  (<= x_3_6 5.9 ) )  (= x_3_7 0 ) )  )
 	:assumption
	(or (not (and (and jump_6 rod_0_6) rod_0_7))( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  (= x_3_6 x_3_7) )  )
 	:assumption
	(or (not (and (and jump_6 rod_1_6) rod_1_7))( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  (= x_3_6 x_3_7) )  )
 	:assumption
	(or (not (and (and jump_6 rod_2_6) rod_2_7))( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  (= x_3_6 x_3_7) )  )
 
	:assumption
	(or (not (and (not jump_6) rod_0_6)) (and ( and (and (and rod_0_7 (<= (+ x_3_6 (* 0.9 dt_6)) x_3_7)) (<= x_3_7 (+ x_3_6 (* 1.1 dt_6)))) (<= x_3_6 16.1)) (<= x_3_7 16.1)))

	:assumption
	(or (not (and (not jump_6) rod_1_6)) (and ( and (and (and rod_1_7 (<= (+ x_3_6 (* 0.9 dt_6)) x_3_7)) (<= x_3_7 (+ x_3_6 (* 1.1 dt_6)))) (<= x_3_6 5.9)) (<= x_3_7 5.9)))

	:assumption
	(or (not (and (not jump_6) rod_2_6)) (and ( and (and (and rod_2_7 (<= (+ x_3_6 (* 0.9 dt_6)) x_3_7)) (<= x_3_7 (+ x_3_6 (* 1.1 dt_6)))) (<= x_3_6 5.9)) (<= x_3_7 5.9)))

	:assumption
	(or  (not rod_0_6) ( or ( or  rod_0_7   rod_1_7  )  rod_2_7  ) ) 
	:assumption
	(or  (not rod_1_6) (or rod_0_7 rod_1_7)) 
	:assumption
	(or  (not rod_2_6) (or rod_0_7 rod_2_7)) 


	:assumption
( and ( and ( and ( or (not rod_0_7) (not rod_1_7))( or (not rod_0_7) (not rod_2_7)))( or (not rod_1_7) (not rod_2_7)))true ) 


	:formula
	( or ( or ( or ( or ( or ( or ( or ( and ( and  recover_1_0   recover_2_0 )  rod_0_0 )  ( and ( and  recover_1_1   recover_2_1 )  rod_0_1 ) ) ( and ( and  recover_1_2   recover_2_2 )  rod_0_2 ) ) ( and ( and  recover_1_3   recover_2_3 )  rod_0_3 ) ) ( and ( and  recover_1_4   recover_2_4 )  rod_0_4 ) ) ( and ( and  recover_1_5   recover_2_5 )  rod_0_5 ) ) ( and ( and  recover_1_6   recover_2_6 )  rod_0_6 ) ) ( and ( and  recover_1_7   recover_2_7 )  rod_0_7 ) ) )
