(benchmark Rod_3_13_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 ((jump_8))
	:extrapreds ((jump_9))
	:extrapreds ((jump_10))
	:extrapreds ((jump_11))
	:extrapreds ((jump_12))
	: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 ((out_3_0))
	:extrapreds ((in_3_0))
	:extrapreds ((recover_3_0))
	:extrapreds ((add_3_0))
	:extrapreds ((remove_3_0))
	:extrapreds ((rod_0_0))
	:extrapreds ((rod_1_0))
	:extrapreds ((rod_2_0))
	:extrapreds ((rod_3_0))
	:extrafuns ((dt_0 Real))
	:extrafuns ((x_1_0 Real))
	:extrafuns ((x_2_0 Real))
	:extrafuns ((x_3_0 Real))
	:extrafuns ((x_4_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 ((out_3_1))
	:extrapreds ((in_3_1))
	:extrapreds ((recover_3_1))
	:extrapreds ((add_3_1))
	:extrapreds ((remove_3_1))
	:extrapreds ((rod_0_1))
	:extrapreds ((rod_1_1))
	:extrapreds ((rod_2_1))
	:extrapreds ((rod_3_1))
	:extrafuns ((dt_1 Real))
	:extrafuns ((x_1_1 Real))
	:extrafuns ((x_2_1 Real))
	:extrafuns ((x_3_1 Real))
	:extrafuns ((x_4_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 ((out_3_2))
	:extrapreds ((in_3_2))
	:extrapreds ((recover_3_2))
	:extrapreds ((add_3_2))
	:extrapreds ((remove_3_2))
	:extrapreds ((rod_0_2))
	:extrapreds ((rod_1_2))
	:extrapreds ((rod_2_2))
	:extrapreds ((rod_3_2))
	:extrafuns ((dt_2 Real))
	:extrafuns ((x_1_2 Real))
	:extrafuns ((x_2_2 Real))
	:extrafuns ((x_3_2 Real))
	:extrafuns ((x_4_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 ((out_3_3))
	:extrapreds ((in_3_3))
	:extrapreds ((recover_3_3))
	:extrapreds ((add_3_3))
	:extrapreds ((remove_3_3))
	:extrapreds ((rod_0_3))
	:extrapreds ((rod_1_3))
	:extrapreds ((rod_2_3))
	:extrapreds ((rod_3_3))
	:extrafuns ((dt_3 Real))
	:extrafuns ((x_1_3 Real))
	:extrafuns ((x_2_3 Real))
	:extrafuns ((x_3_3 Real))
	:extrafuns ((x_4_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 ((out_3_4))
	:extrapreds ((in_3_4))
	:extrapreds ((recover_3_4))
	:extrapreds ((add_3_4))
	:extrapreds ((remove_3_4))
	:extrapreds ((rod_0_4))
	:extrapreds ((rod_1_4))
	:extrapreds ((rod_2_4))
	:extrapreds ((rod_3_4))
	:extrafuns ((dt_4 Real))
	:extrafuns ((x_1_4 Real))
	:extrafuns ((x_2_4 Real))
	:extrafuns ((x_3_4 Real))
	:extrafuns ((x_4_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 ((out_3_5))
	:extrapreds ((in_3_5))
	:extrapreds ((recover_3_5))
	:extrapreds ((add_3_5))
	:extrapreds ((remove_3_5))
	:extrapreds ((rod_0_5))
	:extrapreds ((rod_1_5))
	:extrapreds ((rod_2_5))
	:extrapreds ((rod_3_5))
	:extrafuns ((dt_5 Real))
	:extrafuns ((x_1_5 Real))
	:extrafuns ((x_2_5 Real))
	:extrafuns ((x_3_5 Real))
	:extrafuns ((x_4_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 ((out_3_6))
	:extrapreds ((in_3_6))
	:extrapreds ((recover_3_6))
	:extrapreds ((add_3_6))
	:extrapreds ((remove_3_6))
	:extrapreds ((rod_0_6))
	:extrapreds ((rod_1_6))
	:extrapreds ((rod_2_6))
	:extrapreds ((rod_3_6))
	:extrafuns ((dt_6 Real))
	:extrafuns ((x_1_6 Real))
	:extrafuns ((x_2_6 Real))
	:extrafuns ((x_3_6 Real))
	:extrafuns ((x_4_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 ((out_3_7))
	:extrapreds ((in_3_7))
	:extrapreds ((recover_3_7))
	:extrapreds ((add_3_7))
	:extrapreds ((remove_3_7))
	:extrapreds ((rod_0_7))
	:extrapreds ((rod_1_7))
	:extrapreds ((rod_2_7))
	:extrapreds ((rod_3_7))
	:extrafuns ((dt_7 Real))
	:extrafuns ((x_1_7 Real))
	:extrafuns ((x_2_7 Real))
	:extrafuns ((x_3_7 Real))
	:extrafuns ((x_4_7 Real))
	:extrapreds ((out_1_8))
	:extrapreds ((in_1_8))
	:extrapreds ((recover_1_8))
	:extrapreds ((add_1_8))
	:extrapreds ((remove_1_8))
	:extrapreds ((out_2_8))
	:extrapreds ((in_2_8))
	:extrapreds ((recover_2_8))
	:extrapreds ((add_2_8))
	:extrapreds ((remove_2_8))
	:extrapreds ((out_3_8))
	:extrapreds ((in_3_8))
	:extrapreds ((recover_3_8))
	:extrapreds ((add_3_8))
	:extrapreds ((remove_3_8))
	:extrapreds ((rod_0_8))
	:extrapreds ((rod_1_8))
	:extrapreds ((rod_2_8))
	:extrapreds ((rod_3_8))
	:extrafuns ((dt_8 Real))
	:extrafuns ((x_1_8 Real))
	:extrafuns ((x_2_8 Real))
	:extrafuns ((x_3_8 Real))
	:extrafuns ((x_4_8 Real))
	:extrapreds ((out_1_9))
	:extrapreds ((in_1_9))
	:extrapreds ((recover_1_9))
	:extrapreds ((add_1_9))
	:extrapreds ((remove_1_9))
	:extrapreds ((out_2_9))
	:extrapreds ((in_2_9))
	:extrapreds ((recover_2_9))
	:extrapreds ((add_2_9))
	:extrapreds ((remove_2_9))
	:extrapreds ((out_3_9))
	:extrapreds ((in_3_9))
	:extrapreds ((recover_3_9))
	:extrapreds ((add_3_9))
	:extrapreds ((remove_3_9))
	:extrapreds ((rod_0_9))
	:extrapreds ((rod_1_9))
	:extrapreds ((rod_2_9))
	:extrapreds ((rod_3_9))
	:extrafuns ((dt_9 Real))
	:extrafuns ((x_1_9 Real))
	:extrafuns ((x_2_9 Real))
	:extrafuns ((x_3_9 Real))
	:extrafuns ((x_4_9 Real))
	:extrapreds ((out_1_10))
	:extrapreds ((in_1_10))
	:extrapreds ((recover_1_10))
	:extrapreds ((add_1_10))
	:extrapreds ((remove_1_10))
	:extrapreds ((out_2_10))
	:extrapreds ((in_2_10))
	:extrapreds ((recover_2_10))
	:extrapreds ((add_2_10))
	:extrapreds ((remove_2_10))
	:extrapreds ((out_3_10))
	:extrapreds ((in_3_10))
	:extrapreds ((recover_3_10))
	:extrapreds ((add_3_10))
	:extrapreds ((remove_3_10))
	:extrapreds ((rod_0_10))
	:extrapreds ((rod_1_10))
	:extrapreds ((rod_2_10))
	:extrapreds ((rod_3_10))
	:extrafuns ((dt_10 Real))
	:extrafuns ((x_1_10 Real))
	:extrafuns ((x_2_10 Real))
	:extrafuns ((x_3_10 Real))
	:extrafuns ((x_4_10 Real))
	:extrapreds ((out_1_11))
	:extrapreds ((in_1_11))
	:extrapreds ((recover_1_11))
	:extrapreds ((add_1_11))
	:extrapreds ((remove_1_11))
	:extrapreds ((out_2_11))
	:extrapreds ((in_2_11))
	:extrapreds ((recover_2_11))
	:extrapreds ((add_2_11))
	:extrapreds ((remove_2_11))
	:extrapreds ((out_3_11))
	:extrapreds ((in_3_11))
	:extrapreds ((recover_3_11))
	:extrapreds ((add_3_11))
	:extrapreds ((remove_3_11))
	:extrapreds ((rod_0_11))
	:extrapreds ((rod_1_11))
	:extrapreds ((rod_2_11))
	:extrapreds ((rod_3_11))
	:extrafuns ((dt_11 Real))
	:extrafuns ((x_1_11 Real))
	:extrafuns ((x_2_11 Real))
	:extrafuns ((x_3_11 Real))
	:extrafuns ((x_4_11 Real))
	:extrapreds ((out_1_12))
	:extrapreds ((in_1_12))
	:extrapreds ((recover_1_12))
	:extrapreds ((add_1_12))
	:extrapreds ((remove_1_12))
	:extrapreds ((out_2_12))
	:extrapreds ((in_2_12))
	:extrapreds ((recover_2_12))
	:extrapreds ((add_2_12))
	:extrapreds ((remove_2_12))
	:extrapreds ((out_3_12))
	:extrapreds ((in_3_12))
	:extrapreds ((recover_3_12))
	:extrapreds ((add_3_12))
	:extrapreds ((remove_3_12))
	:extrapreds ((rod_0_12))
	:extrapreds ((rod_1_12))
	:extrapreds ((rod_2_12))
	:extrapreds ((rod_3_12))
	:extrafuns ((dt_12 Real))
	:extrafuns ((x_1_12 Real))
	:extrafuns ((x_2_12 Real))
	:extrafuns ((x_3_12 Real))
	:extrafuns ((x_4_12 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 out_3_0)
 	:assumption
	(not in_3_0)
 	:assumption
	(not recover_3_0)
	:assumption
	(= x_3_0 0)
	:assumption
	(and true rod_0_0)
 	:assumption
	(not rod_1_0)
 	:assumption
	(not rod_2_0)
 	:assumption
 (not rod_3_0)
	:assumption
	(= x_4_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 jump_7 jump_8)
	:assumption
	(or ( not jump_7) (not jump_8))

	:assumption
	(or jump_8 jump_9)
	:assumption
	(or ( not jump_8) (not jump_9))

	:assumption
	(or jump_9 jump_10)
	:assumption
	(or ( not jump_9) (not jump_10))

	:assumption
	(or jump_10 jump_11)
	:assumption
	(or ( not jump_10) (not jump_11))

	:assumption
	(or jump_11 jump_12)
	:assumption
	(or ( not jump_11) (not jump_12))

	: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 jump_8 ) (= dt_8 0))
	:assumption
	(or jump_8 (> dt_8 0))

	:assumption
	(or ( not jump_9 ) (= dt_9 0))
	:assumption
	(or jump_9 (> dt_9 0))

	:assumption
	(or ( not jump_10 ) (= dt_10 0))
	:assumption
	(or jump_10 (> dt_10 0))

	:assumption
	(or ( not jump_11 ) (= dt_11 0))
	:assumption
	(or jump_11 (> dt_11 0))

	:assumption
	(or ( not jump_12 ) (= dt_12 0))
	:assumption
	(or jump_12 (> dt_12 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_0 out_3_0) add_3_0) ) in_3_1 )
	:assumption
	(or (not (and (and jump_0 out_3_0) in_3_1)) (and (and ( and  add_3_0 (not remove_3_0)) (> x_3_0 1)) (= x_3_1 0)))

	:assumption
	(or(not (and (and jump_0 in_3_0) remove_3_0) ) recover_3_1 )
	:assumption
	(or (not (and (and jump_0 in_3_0) recover_3_1)) (and ( and remove_3_0 (not add_3_0)) (= x_3_1 0)))

	:assumption
	(or(not (and jump_0 recover_3_0)  ) (or out_3_1 recover_3_1 ))
	:assumption
	(or (not (and (and jump_0 recover_3_0) out_3_1)) (and (and ( and (not add_3_0) (not remove_3_0)) (< x_3_0 10000)) (= x_3_1 x_3_0)))

	:assumption
	(or(not (and (and jump_0 out_3_0) out_3_1)) ( and (and (not add_3_0) (not remove_3_0) )  (= x_3_1 x_3_0)))

	:assumption
	(or(not (and (and jump_0 in_3_0) in_3_1)) ( and (and (not add_3_0) (not remove_3_0) )  (= x_3_1 x_3_0)))

	:assumption
	(or(not (and (and jump_0 recover_3_0) recover_3_1)) ( and (and (not add_3_0) (not remove_3_0) )  (= x_3_1 x_3_0)))

	:assumption
	(or (not (and (not jump_0) out_3_0)) (and ( and (and (and out_3_1 (<= (+ x_3_0 (* 0.9 dt_0)) x_3_1)) (<= x_3_1 (+ x_3_0 (* 1.1 dt_0))))  (< x_3_0 10000)) (< x_3_1 10000)))

	:assumption
	(or (not (and (not jump_0) in_3_0)) (and ( and (and (and in_3_1 (<= (+ x_3_0 (* 0.9 dt_0)) x_3_1)) (<= x_3_1 (+ x_3_0 (* 1.1 dt_0)))) (< x_3_0 10000)) (< x_3_1 10000)))

	:assumption
	(or (not (and (not jump_0) recover_3_0)) (and ( and (and (and recover_3_1 (<= (+ x_3_0 (* 0.9 dt_0)) x_3_1)) (<= x_3_1 (+ x_3_0 (* 1.1 dt_0)))) (< x_3_0 10000)) (< x_3_1 10000)))


	:assumption
	(or  (not out_3_0) (or out_3_1 in_3_1)) 
	:assumption
	(or  (not in_3_0) (or in_3_1 recover_3_1)) 
	:assumption
	(or  (not recover_3_0) (or out_3_1 recover_3_1)) 

	:assumption
( and ( and ( and ( or (not out_3_1) (not in_3_1))( or (not out_3_1) (not recover_3_1)))( or (not in_3_1) (not recover_3_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_1 out_3_1) add_3_1) ) in_3_2 )
	:assumption
	(or (not (and (and jump_1 out_3_1) in_3_2)) (and (and ( and  add_3_1 (not remove_3_1)) (> x_3_1 1)) (= x_3_2 0)))

	:assumption
	(or(not (and (and jump_1 in_3_1) remove_3_1) ) recover_3_2 )
	:assumption
	(or (not (and (and jump_1 in_3_1) recover_3_2)) (and ( and remove_3_1 (not add_3_1)) (= x_3_2 0)))

	:assumption
	(or(not (and jump_1 recover_3_1)  ) (or out_3_2 recover_3_2 ))
	:assumption
	(or (not (and (and jump_1 recover_3_1) out_3_2)) (and (and ( and (not add_3_1) (not remove_3_1)) (< x_3_1 10000)) (= x_3_2 x_3_1)))

	:assumption
	(or(not (and (and jump_1 out_3_1) out_3_2)) ( and (and (not add_3_1) (not remove_3_1) )  (= x_3_2 x_3_1)))

	:assumption
	(or(not (and (and jump_1 in_3_1) in_3_2)) ( and (and (not add_3_1) (not remove_3_1) )  (= x_3_2 x_3_1)))

	:assumption
	(or(not (and (and jump_1 recover_3_1) recover_3_2)) ( and (and (not add_3_1) (not remove_3_1) )  (= x_3_2 x_3_1)))

	:assumption
	(or (not (and (not jump_1) out_3_1)) (and ( and (and (and out_3_2 (<= (+ x_3_1 (* 0.9 dt_1)) x_3_2)) (<= x_3_2 (+ x_3_1 (* 1.1 dt_1))))  (< x_3_1 10000)) (< x_3_2 10000)))

	:assumption
	(or (not (and (not jump_1) in_3_1)) (and ( and (and (and in_3_2 (<= (+ x_3_1 (* 0.9 dt_1)) x_3_2)) (<= x_3_2 (+ x_3_1 (* 1.1 dt_1)))) (< x_3_1 10000)) (< x_3_2 10000)))

	:assumption
	(or (not (and (not jump_1) recover_3_1)) (and ( and (and (and recover_3_2 (<= (+ x_3_1 (* 0.9 dt_1)) x_3_2)) (<= x_3_2 (+ x_3_1 (* 1.1 dt_1)))) (< x_3_1 10000)) (< x_3_2 10000)))


	:assumption
	(or  (not out_3_1) (or out_3_2 in_3_2)) 
	:assumption
	(or  (not in_3_1) (or in_3_2 recover_3_2)) 
	:assumption
	(or  (not recover_3_1) (or out_3_2 recover_3_2)) 

	:assumption
( and ( and ( and ( or (not out_3_2) (not in_3_2))( or (not out_3_2) (not recover_3_2)))( or (not in_3_2) (not recover_3_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_2 out_3_2) add_3_2) ) in_3_3 )
	:assumption
	(or (not (and (and jump_2 out_3_2) in_3_3)) (and (and ( and  add_3_2 (not remove_3_2)) (> x_3_2 1)) (= x_3_3 0)))

	:assumption
	(or(not (and (and jump_2 in_3_2) remove_3_2) ) recover_3_3 )
	:assumption
	(or (not (and (and jump_2 in_3_2) recover_3_3)) (and ( and remove_3_2 (not add_3_2)) (= x_3_3 0)))

	:assumption
	(or(not (and jump_2 recover_3_2)  ) (or out_3_3 recover_3_3 ))
	:assumption
	(or (not (and (and jump_2 recover_3_2) out_3_3)) (and (and ( and (not add_3_2) (not remove_3_2)) (< x_3_2 10000)) (= x_3_3 x_3_2)))

	:assumption
	(or(not (and (and jump_2 out_3_2) out_3_3)) ( and (and (not add_3_2) (not remove_3_2) )  (= x_3_3 x_3_2)))

	:assumption
	(or(not (and (and jump_2 in_3_2) in_3_3)) ( and (and (not add_3_2) (not remove_3_2) )  (= x_3_3 x_3_2)))

	:assumption
	(or(not (and (and jump_2 recover_3_2) recover_3_3)) ( and (and (not add_3_2) (not remove_3_2) )  (= x_3_3 x_3_2)))

	:assumption
	(or (not (and (not jump_2) out_3_2)) (and ( and (and (and out_3_3 (<= (+ x_3_2 (* 0.9 dt_2)) x_3_3)) (<= x_3_3 (+ x_3_2 (* 1.1 dt_2))))  (< x_3_2 10000)) (< x_3_3 10000)))

	:assumption
	(or (not (and (not jump_2) in_3_2)) (and ( and (and (and in_3_3 (<= (+ x_3_2 (* 0.9 dt_2)) x_3_3)) (<= x_3_3 (+ x_3_2 (* 1.1 dt_2)))) (< x_3_2 10000)) (< x_3_3 10000)))

	:assumption
	(or (not (and (not jump_2) recover_3_2)) (and ( and (and (and recover_3_3 (<= (+ x_3_2 (* 0.9 dt_2)) x_3_3)) (<= x_3_3 (+ x_3_2 (* 1.1 dt_2)))) (< x_3_2 10000)) (< x_3_3 10000)))


	:assumption
	(or  (not out_3_2) (or out_3_3 in_3_3)) 
	:assumption
	(or  (not in_3_2) (or in_3_3 recover_3_3)) 
	:assumption
	(or  (not recover_3_2) (or out_3_3 recover_3_3)) 

	:assumption
( and ( and ( and ( or (not out_3_3) (not in_3_3))( or (not out_3_3) (not recover_3_3)))( or (not in_3_3) (not recover_3_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_3 out_3_3) add_3_3) ) in_3_4 )
	:assumption
	(or (not (and (and jump_3 out_3_3) in_3_4)) (and (and ( and  add_3_3 (not remove_3_3)) (> x_3_3 1)) (= x_3_4 0)))

	:assumption
	(or(not (and (and jump_3 in_3_3) remove_3_3) ) recover_3_4 )
	:assumption
	(or (not (and (and jump_3 in_3_3) recover_3_4)) (and ( and remove_3_3 (not add_3_3)) (= x_3_4 0)))

	:assumption
	(or(not (and jump_3 recover_3_3)  ) (or out_3_4 recover_3_4 ))
	:assumption
	(or (not (and (and jump_3 recover_3_3) out_3_4)) (and (and ( and (not add_3_3) (not remove_3_3)) (< x_3_3 10000)) (= x_3_4 x_3_3)))

	:assumption
	(or(not (and (and jump_3 out_3_3) out_3_4)) ( and (and (not add_3_3) (not remove_3_3) )  (= x_3_4 x_3_3)))

	:assumption
	(or(not (and (and jump_3 in_3_3) in_3_4)) ( and (and (not add_3_3) (not remove_3_3) )  (= x_3_4 x_3_3)))

	:assumption
	(or(not (and (and jump_3 recover_3_3) recover_3_4)) ( and (and (not add_3_3) (not remove_3_3) )  (= x_3_4 x_3_3)))

	:assumption
	(or (not (and (not jump_3) out_3_3)) (and ( and (and (and out_3_4 (<= (+ x_3_3 (* 0.9 dt_3)) x_3_4)) (<= x_3_4 (+ x_3_3 (* 1.1 dt_3))))  (< x_3_3 10000)) (< x_3_4 10000)))

	:assumption
	(or (not (and (not jump_3) in_3_3)) (and ( and (and (and in_3_4 (<= (+ x_3_3 (* 0.9 dt_3)) x_3_4)) (<= x_3_4 (+ x_3_3 (* 1.1 dt_3)))) (< x_3_3 10000)) (< x_3_4 10000)))

	:assumption
	(or (not (and (not jump_3) recover_3_3)) (and ( and (and (and recover_3_4 (<= (+ x_3_3 (* 0.9 dt_3)) x_3_4)) (<= x_3_4 (+ x_3_3 (* 1.1 dt_3)))) (< x_3_3 10000)) (< x_3_4 10000)))


	:assumption
	(or  (not out_3_3) (or out_3_4 in_3_4)) 
	:assumption
	(or  (not in_3_3) (or in_3_4 recover_3_4)) 
	:assumption
	(or  (not recover_3_3) (or out_3_4 recover_3_4)) 

	:assumption
( and ( and ( and ( or (not out_3_4) (not in_3_4))( or (not out_3_4) (not recover_3_4)))( or (not in_3_4) (not recover_3_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_4 out_3_4) add_3_4) ) in_3_5 )
	:assumption
	(or (not (and (and jump_4 out_3_4) in_3_5)) (and (and ( and  add_3_4 (not remove_3_4)) (> x_3_4 1)) (= x_3_5 0)))

	:assumption
	(or(not (and (and jump_4 in_3_4) remove_3_4) ) recover_3_5 )
	:assumption
	(or (not (and (and jump_4 in_3_4) recover_3_5)) (and ( and remove_3_4 (not add_3_4)) (= x_3_5 0)))

	:assumption
	(or(not (and jump_4 recover_3_4)  ) (or out_3_5 recover_3_5 ))
	:assumption
	(or (not (and (and jump_4 recover_3_4) out_3_5)) (and (and ( and (not add_3_4) (not remove_3_4)) (< x_3_4 10000)) (= x_3_5 x_3_4)))

	:assumption
	(or(not (and (and jump_4 out_3_4) out_3_5)) ( and (and (not add_3_4) (not remove_3_4) )  (= x_3_5 x_3_4)))

	:assumption
	(or(not (and (and jump_4 in_3_4) in_3_5)) ( and (and (not add_3_4) (not remove_3_4) )  (= x_3_5 x_3_4)))

	:assumption
	(or(not (and (and jump_4 recover_3_4) recover_3_5)) ( and (and (not add_3_4) (not remove_3_4) )  (= x_3_5 x_3_4)))

	:assumption
	(or (not (and (not jump_4) out_3_4)) (and ( and (and (and out_3_5 (<= (+ x_3_4 (* 0.9 dt_4)) x_3_5)) (<= x_3_5 (+ x_3_4 (* 1.1 dt_4))))  (< x_3_4 10000)) (< x_3_5 10000)))

	:assumption
	(or (not (and (not jump_4) in_3_4)) (and ( and (and (and in_3_5 (<= (+ x_3_4 (* 0.9 dt_4)) x_3_5)) (<= x_3_5 (+ x_3_4 (* 1.1 dt_4)))) (< x_3_4 10000)) (< x_3_5 10000)))

	:assumption
	(or (not (and (not jump_4) recover_3_4)) (and ( and (and (and recover_3_5 (<= (+ x_3_4 (* 0.9 dt_4)) x_3_5)) (<= x_3_5 (+ x_3_4 (* 1.1 dt_4)))) (< x_3_4 10000)) (< x_3_5 10000)))


	:assumption
	(or  (not out_3_4) (or out_3_5 in_3_5)) 
	:assumption
	(or  (not in_3_4) (or in_3_5 recover_3_5)) 
	:assumption
	(or  (not recover_3_4) (or out_3_5 recover_3_5)) 

	:assumption
( and ( and ( and ( or (not out_3_5) (not in_3_5))( or (not out_3_5) (not recover_3_5)))( or (not in_3_5) (not recover_3_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_5 out_3_5) add_3_5) ) in_3_6 )
	:assumption
	(or (not (and (and jump_5 out_3_5) in_3_6)) (and (and ( and  add_3_5 (not remove_3_5)) (> x_3_5 1)) (= x_3_6 0)))

	:assumption
	(or(not (and (and jump_5 in_3_5) remove_3_5) ) recover_3_6 )
	:assumption
	(or (not (and (and jump_5 in_3_5) recover_3_6)) (and ( and remove_3_5 (not add_3_5)) (= x_3_6 0)))

	:assumption
	(or(not (and jump_5 recover_3_5)  ) (or out_3_6 recover_3_6 ))
	:assumption
	(or (not (and (and jump_5 recover_3_5) out_3_6)) (and (and ( and (not add_3_5) (not remove_3_5)) (< x_3_5 10000)) (= x_3_6 x_3_5)))

	:assumption
	(or(not (and (and jump_5 out_3_5) out_3_6)) ( and (and (not add_3_5) (not remove_3_5) )  (= x_3_6 x_3_5)))

	:assumption
	(or(not (and (and jump_5 in_3_5) in_3_6)) ( and (and (not add_3_5) (not remove_3_5) )  (= x_3_6 x_3_5)))

	:assumption
	(or(not (and (and jump_5 recover_3_5) recover_3_6)) ( and (and (not add_3_5) (not remove_3_5) )  (= x_3_6 x_3_5)))

	:assumption
	(or (not (and (not jump_5) out_3_5)) (and ( and (and (and out_3_6 (<= (+ x_3_5 (* 0.9 dt_5)) x_3_6)) (<= x_3_6 (+ x_3_5 (* 1.1 dt_5))))  (< x_3_5 10000)) (< x_3_6 10000)))

	:assumption
	(or (not (and (not jump_5) in_3_5)) (and ( and (and (and in_3_6 (<= (+ x_3_5 (* 0.9 dt_5)) x_3_6)) (<= x_3_6 (+ x_3_5 (* 1.1 dt_5)))) (< x_3_5 10000)) (< x_3_6 10000)))

	:assumption
	(or (not (and (not jump_5) recover_3_5)) (and ( and (and (and recover_3_6 (<= (+ x_3_5 (* 0.9 dt_5)) x_3_6)) (<= x_3_6 (+ x_3_5 (* 1.1 dt_5)))) (< x_3_5 10000)) (< x_3_6 10000)))


	:assumption
	(or  (not out_3_5) (or out_3_6 in_3_6)) 
	:assumption
	(or  (not in_3_5) (or in_3_6 recover_3_6)) 
	:assumption
	(or  (not recover_3_5) (or out_3_6 recover_3_6)) 

	:assumption
( and ( and ( and ( or (not out_3_6) (not in_3_6))( or (not out_3_6) (not recover_3_6)))( or (not in_3_6) (not recover_3_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_6 out_3_6) add_3_6) ) in_3_7 )
	:assumption
	(or (not (and (and jump_6 out_3_6) in_3_7)) (and (and ( and  add_3_6 (not remove_3_6)) (> x_3_6 1)) (= x_3_7 0)))

	:assumption
	(or(not (and (and jump_6 in_3_6) remove_3_6) ) recover_3_7 )
	:assumption
	(or (not (and (and jump_6 in_3_6) recover_3_7)) (and ( and remove_3_6 (not add_3_6)) (= x_3_7 0)))

	:assumption
	(or(not (and jump_6 recover_3_6)  ) (or out_3_7 recover_3_7 ))
	:assumption
	(or (not (and (and jump_6 recover_3_6) out_3_7)) (and (and ( and (not add_3_6) (not remove_3_6)) (< x_3_6 10000)) (= x_3_7 x_3_6)))

	:assumption
	(or(not (and (and jump_6 out_3_6) out_3_7)) ( and (and (not add_3_6) (not remove_3_6) )  (= x_3_7 x_3_6)))

	:assumption
	(or(not (and (and jump_6 in_3_6) in_3_7)) ( and (and (not add_3_6) (not remove_3_6) )  (= x_3_7 x_3_6)))

	:assumption
	(or(not (and (and jump_6 recover_3_6) recover_3_7)) ( and (and (not add_3_6) (not remove_3_6) )  (= x_3_7 x_3_6)))

	:assumption
	(or (not (and (not jump_6) out_3_6)) (and ( and (and (and out_3_7 (<= (+ x_3_6 (* 0.9 dt_6)) x_3_7)) (<= x_3_7 (+ x_3_6 (* 1.1 dt_6))))  (< x_3_6 10000)) (< x_3_7 10000)))

	:assumption
	(or (not (and (not jump_6) in_3_6)) (and ( and (and (and in_3_7 (<= (+ x_3_6 (* 0.9 dt_6)) x_3_7)) (<= x_3_7 (+ x_3_6 (* 1.1 dt_6)))) (< x_3_6 10000)) (< x_3_7 10000)))

	:assumption
	(or (not (and (not jump_6) recover_3_6)) (and ( and (and (and recover_3_7 (<= (+ x_3_6 (* 0.9 dt_6)) x_3_7)) (<= x_3_7 (+ x_3_6 (* 1.1 dt_6)))) (< x_3_6 10000)) (< x_3_7 10000)))


	:assumption
	(or  (not out_3_6) (or out_3_7 in_3_7)) 
	:assumption
	(or  (not in_3_6) (or in_3_7 recover_3_7)) 
	:assumption
	(or  (not recover_3_6) (or out_3_7 recover_3_7)) 

	:assumption
( and ( and ( and ( or (not out_3_7) (not in_3_7))( or (not out_3_7) (not recover_3_7)))( or (not in_3_7) (not recover_3_7)))true ) 

	:assumption
	(or(not (and (and jump_7 out_1_7) add_1_7) ) in_1_8 )
	:assumption
	(or (not (and (and jump_7 out_1_7) in_1_8)) (and (and ( and  add_1_7 (not remove_1_7)) (> x_1_7 1)) (= x_1_8 0)))

	:assumption
	(or(not (and (and jump_7 in_1_7) remove_1_7) ) recover_1_8 )
	:assumption
	(or (not (and (and jump_7 in_1_7) recover_1_8)) (and ( and remove_1_7 (not add_1_7)) (= x_1_8 0)))

	:assumption
	(or(not (and jump_7 recover_1_7)  ) (or out_1_8 recover_1_8 ))
	:assumption
	(or (not (and (and jump_7 recover_1_7) out_1_8)) (and (and ( and (not add_1_7) (not remove_1_7)) (< x_1_7 10000)) (= x_1_8 x_1_7)))

	:assumption
	(or(not (and (and jump_7 out_1_7) out_1_8)) ( and (and (not add_1_7) (not remove_1_7) )  (= x_1_8 x_1_7)))

	:assumption
	(or(not (and (and jump_7 in_1_7) in_1_8)) ( and (and (not add_1_7) (not remove_1_7) )  (= x_1_8 x_1_7)))

	:assumption
	(or(not (and (and jump_7 recover_1_7) recover_1_8)) ( and (and (not add_1_7) (not remove_1_7) )  (= x_1_8 x_1_7)))

	:assumption
	(or (not (and (not jump_7) out_1_7)) (and ( and (and (and out_1_8 (<= (+ x_1_7 (* 0.9 dt_7)) x_1_8)) (<= x_1_8 (+ x_1_7 (* 1.1 dt_7))))  (< x_1_7 10000)) (< x_1_8 10000)))

	:assumption
	(or (not (and (not jump_7) in_1_7)) (and ( and (and (and in_1_8 (<= (+ x_1_7 (* 0.9 dt_7)) x_1_8)) (<= x_1_8 (+ x_1_7 (* 1.1 dt_7)))) (< x_1_7 10000)) (< x_1_8 10000)))

	:assumption
	(or (not (and (not jump_7) recover_1_7)) (and ( and (and (and recover_1_8 (<= (+ x_1_7 (* 0.9 dt_7)) x_1_8)) (<= x_1_8 (+ x_1_7 (* 1.1 dt_7)))) (< x_1_7 10000)) (< x_1_8 10000)))


	:assumption
	(or  (not out_1_7) (or out_1_8 in_1_8)) 
	:assumption
	(or  (not in_1_7) (or in_1_8 recover_1_8)) 
	:assumption
	(or  (not recover_1_7) (or out_1_8 recover_1_8)) 

	:assumption
( and ( and ( and ( or (not out_1_8) (not in_1_8))( or (not out_1_8) (not recover_1_8)))( or (not in_1_8) (not recover_1_8)))true ) 

	:assumption
	(or(not (and (and jump_7 out_2_7) add_2_7) ) in_2_8 )
	:assumption
	(or (not (and (and jump_7 out_2_7) in_2_8)) (and (and ( and  add_2_7 (not remove_2_7)) (> x_2_7 1)) (= x_2_8 0)))

	:assumption
	(or(not (and (and jump_7 in_2_7) remove_2_7) ) recover_2_8 )
	:assumption
	(or (not (and (and jump_7 in_2_7) recover_2_8)) (and ( and remove_2_7 (not add_2_7)) (= x_2_8 0)))

	:assumption
	(or(not (and jump_7 recover_2_7)  ) (or out_2_8 recover_2_8 ))
	:assumption
	(or (not (and (and jump_7 recover_2_7) out_2_8)) (and (and ( and (not add_2_7) (not remove_2_7)) (< x_2_7 10000)) (= x_2_8 x_2_7)))

	:assumption
	(or(not (and (and jump_7 out_2_7) out_2_8)) ( and (and (not add_2_7) (not remove_2_7) )  (= x_2_8 x_2_7)))

	:assumption
	(or(not (and (and jump_7 in_2_7) in_2_8)) ( and (and (not add_2_7) (not remove_2_7) )  (= x_2_8 x_2_7)))

	:assumption
	(or(not (and (and jump_7 recover_2_7) recover_2_8)) ( and (and (not add_2_7) (not remove_2_7) )  (= x_2_8 x_2_7)))

	:assumption
	(or (not (and (not jump_7) out_2_7)) (and ( and (and (and out_2_8 (<= (+ x_2_7 (* 0.9 dt_7)) x_2_8)) (<= x_2_8 (+ x_2_7 (* 1.1 dt_7))))  (< x_2_7 10000)) (< x_2_8 10000)))

	:assumption
	(or (not (and (not jump_7) in_2_7)) (and ( and (and (and in_2_8 (<= (+ x_2_7 (* 0.9 dt_7)) x_2_8)) (<= x_2_8 (+ x_2_7 (* 1.1 dt_7)))) (< x_2_7 10000)) (< x_2_8 10000)))

	:assumption
	(or (not (and (not jump_7) recover_2_7)) (and ( and (and (and recover_2_8 (<= (+ x_2_7 (* 0.9 dt_7)) x_2_8)) (<= x_2_8 (+ x_2_7 (* 1.1 dt_7)))) (< x_2_7 10000)) (< x_2_8 10000)))


	:assumption
	(or  (not out_2_7) (or out_2_8 in_2_8)) 
	:assumption
	(or  (not in_2_7) (or in_2_8 recover_2_8)) 
	:assumption
	(or  (not recover_2_7) (or out_2_8 recover_2_8)) 

	:assumption
( and ( and ( and ( or (not out_2_8) (not in_2_8))( or (not out_2_8) (not recover_2_8)))( or (not in_2_8) (not recover_2_8)))true ) 

	:assumption
	(or(not (and (and jump_7 out_3_7) add_3_7) ) in_3_8 )
	:assumption
	(or (not (and (and jump_7 out_3_7) in_3_8)) (and (and ( and  add_3_7 (not remove_3_7)) (> x_3_7 1)) (= x_3_8 0)))

	:assumption
	(or(not (and (and jump_7 in_3_7) remove_3_7) ) recover_3_8 )
	:assumption
	(or (not (and (and jump_7 in_3_7) recover_3_8)) (and ( and remove_3_7 (not add_3_7)) (= x_3_8 0)))

	:assumption
	(or(not (and jump_7 recover_3_7)  ) (or out_3_8 recover_3_8 ))
	:assumption
	(or (not (and (and jump_7 recover_3_7) out_3_8)) (and (and ( and (not add_3_7) (not remove_3_7)) (< x_3_7 10000)) (= x_3_8 x_3_7)))

	:assumption
	(or(not (and (and jump_7 out_3_7) out_3_8)) ( and (and (not add_3_7) (not remove_3_7) )  (= x_3_8 x_3_7)))

	:assumption
	(or(not (and (and jump_7 in_3_7) in_3_8)) ( and (and (not add_3_7) (not remove_3_7) )  (= x_3_8 x_3_7)))

	:assumption
	(or(not (and (and jump_7 recover_3_7) recover_3_8)) ( and (and (not add_3_7) (not remove_3_7) )  (= x_3_8 x_3_7)))

	:assumption
	(or (not (and (not jump_7) out_3_7)) (and ( and (and (and out_3_8 (<= (+ x_3_7 (* 0.9 dt_7)) x_3_8)) (<= x_3_8 (+ x_3_7 (* 1.1 dt_7))))  (< x_3_7 10000)) (< x_3_8 10000)))

	:assumption
	(or (not (and (not jump_7) in_3_7)) (and ( and (and (and in_3_8 (<= (+ x_3_7 (* 0.9 dt_7)) x_3_8)) (<= x_3_8 (+ x_3_7 (* 1.1 dt_7)))) (< x_3_7 10000)) (< x_3_8 10000)))

	:assumption
	(or (not (and (not jump_7) recover_3_7)) (and ( and (and (and recover_3_8 (<= (+ x_3_7 (* 0.9 dt_7)) x_3_8)) (<= x_3_8 (+ x_3_7 (* 1.1 dt_7)))) (< x_3_7 10000)) (< x_3_8 10000)))


	:assumption
	(or  (not out_3_7) (or out_3_8 in_3_8)) 
	:assumption
	(or  (not in_3_7) (or in_3_8 recover_3_8)) 
	:assumption
	(or  (not recover_3_7) (or out_3_8 recover_3_8)) 

	:assumption
( and ( and ( and ( or (not out_3_8) (not in_3_8))( or (not out_3_8) (not recover_3_8)))( or (not in_3_8) (not recover_3_8)))true ) 

	:assumption
	(or(not (and (and jump_8 out_1_8) add_1_8) ) in_1_9 )
	:assumption
	(or (not (and (and jump_8 out_1_8) in_1_9)) (and (and ( and  add_1_8 (not remove_1_8)) (> x_1_8 1)) (= x_1_9 0)))

	:assumption
	(or(not (and (and jump_8 in_1_8) remove_1_8) ) recover_1_9 )
	:assumption
	(or (not (and (and jump_8 in_1_8) recover_1_9)) (and ( and remove_1_8 (not add_1_8)) (= x_1_9 0)))

	:assumption
	(or(not (and jump_8 recover_1_8)  ) (or out_1_9 recover_1_9 ))
	:assumption
	(or (not (and (and jump_8 recover_1_8) out_1_9)) (and (and ( and (not add_1_8) (not remove_1_8)) (< x_1_8 10000)) (= x_1_9 x_1_8)))

	:assumption
	(or(not (and (and jump_8 out_1_8) out_1_9)) ( and (and (not add_1_8) (not remove_1_8) )  (= x_1_9 x_1_8)))

	:assumption
	(or(not (and (and jump_8 in_1_8) in_1_9)) ( and (and (not add_1_8) (not remove_1_8) )  (= x_1_9 x_1_8)))

	:assumption
	(or(not (and (and jump_8 recover_1_8) recover_1_9)) ( and (and (not add_1_8) (not remove_1_8) )  (= x_1_9 x_1_8)))

	:assumption
	(or (not (and (not jump_8) out_1_8)) (and ( and (and (and out_1_9 (<= (+ x_1_8 (* 0.9 dt_8)) x_1_9)) (<= x_1_9 (+ x_1_8 (* 1.1 dt_8))))  (< x_1_8 10000)) (< x_1_9 10000)))

	:assumption
	(or (not (and (not jump_8) in_1_8)) (and ( and (and (and in_1_9 (<= (+ x_1_8 (* 0.9 dt_8)) x_1_9)) (<= x_1_9 (+ x_1_8 (* 1.1 dt_8)))) (< x_1_8 10000)) (< x_1_9 10000)))

	:assumption
	(or (not (and (not jump_8) recover_1_8)) (and ( and (and (and recover_1_9 (<= (+ x_1_8 (* 0.9 dt_8)) x_1_9)) (<= x_1_9 (+ x_1_8 (* 1.1 dt_8)))) (< x_1_8 10000)) (< x_1_9 10000)))


	:assumption
	(or  (not out_1_8) (or out_1_9 in_1_9)) 
	:assumption
	(or  (not in_1_8) (or in_1_9 recover_1_9)) 
	:assumption
	(or  (not recover_1_8) (or out_1_9 recover_1_9)) 

	:assumption
( and ( and ( and ( or (not out_1_9) (not in_1_9))( or (not out_1_9) (not recover_1_9)))( or (not in_1_9) (not recover_1_9)))true ) 

	:assumption
	(or(not (and (and jump_8 out_2_8) add_2_8) ) in_2_9 )
	:assumption
	(or (not (and (and jump_8 out_2_8) in_2_9)) (and (and ( and  add_2_8 (not remove_2_8)) (> x_2_8 1)) (= x_2_9 0)))

	:assumption
	(or(not (and (and jump_8 in_2_8) remove_2_8) ) recover_2_9 )
	:assumption
	(or (not (and (and jump_8 in_2_8) recover_2_9)) (and ( and remove_2_8 (not add_2_8)) (= x_2_9 0)))

	:assumption
	(or(not (and jump_8 recover_2_8)  ) (or out_2_9 recover_2_9 ))
	:assumption
	(or (not (and (and jump_8 recover_2_8) out_2_9)) (and (and ( and (not add_2_8) (not remove_2_8)) (< x_2_8 10000)) (= x_2_9 x_2_8)))

	:assumption
	(or(not (and (and jump_8 out_2_8) out_2_9)) ( and (and (not add_2_8) (not remove_2_8) )  (= x_2_9 x_2_8)))

	:assumption
	(or(not (and (and jump_8 in_2_8) in_2_9)) ( and (and (not add_2_8) (not remove_2_8) )  (= x_2_9 x_2_8)))

	:assumption
	(or(not (and (and jump_8 recover_2_8) recover_2_9)) ( and (and (not add_2_8) (not remove_2_8) )  (= x_2_9 x_2_8)))

	:assumption
	(or (not (and (not jump_8) out_2_8)) (and ( and (and (and out_2_9 (<= (+ x_2_8 (* 0.9 dt_8)) x_2_9)) (<= x_2_9 (+ x_2_8 (* 1.1 dt_8))))  (< x_2_8 10000)) (< x_2_9 10000)))

	:assumption
	(or (not (and (not jump_8) in_2_8)) (and ( and (and (and in_2_9 (<= (+ x_2_8 (* 0.9 dt_8)) x_2_9)) (<= x_2_9 (+ x_2_8 (* 1.1 dt_8)))) (< x_2_8 10000)) (< x_2_9 10000)))

	:assumption
	(or (not (and (not jump_8) recover_2_8)) (and ( and (and (and recover_2_9 (<= (+ x_2_8 (* 0.9 dt_8)) x_2_9)) (<= x_2_9 (+ x_2_8 (* 1.1 dt_8)))) (< x_2_8 10000)) (< x_2_9 10000)))


	:assumption
	(or  (not out_2_8) (or out_2_9 in_2_9)) 
	:assumption
	(or  (not in_2_8) (or in_2_9 recover_2_9)) 
	:assumption
	(or  (not recover_2_8) (or out_2_9 recover_2_9)) 

	:assumption
( and ( and ( and ( or (not out_2_9) (not in_2_9))( or (not out_2_9) (not recover_2_9)))( or (not in_2_9) (not recover_2_9)))true ) 

	:assumption
	(or(not (and (and jump_8 out_3_8) add_3_8) ) in_3_9 )
	:assumption
	(or (not (and (and jump_8 out_3_8) in_3_9)) (and (and ( and  add_3_8 (not remove_3_8)) (> x_3_8 1)) (= x_3_9 0)))

	:assumption
	(or(not (and (and jump_8 in_3_8) remove_3_8) ) recover_3_9 )
	:assumption
	(or (not (and (and jump_8 in_3_8) recover_3_9)) (and ( and remove_3_8 (not add_3_8)) (= x_3_9 0)))

	:assumption
	(or(not (and jump_8 recover_3_8)  ) (or out_3_9 recover_3_9 ))
	:assumption
	(or (not (and (and jump_8 recover_3_8) out_3_9)) (and (and ( and (not add_3_8) (not remove_3_8)) (< x_3_8 10000)) (= x_3_9 x_3_8)))

	:assumption
	(or(not (and (and jump_8 out_3_8) out_3_9)) ( and (and (not add_3_8) (not remove_3_8) )  (= x_3_9 x_3_8)))

	:assumption
	(or(not (and (and jump_8 in_3_8) in_3_9)) ( and (and (not add_3_8) (not remove_3_8) )  (= x_3_9 x_3_8)))

	:assumption
	(or(not (and (and jump_8 recover_3_8) recover_3_9)) ( and (and (not add_3_8) (not remove_3_8) )  (= x_3_9 x_3_8)))

	:assumption
	(or (not (and (not jump_8) out_3_8)) (and ( and (and (and out_3_9 (<= (+ x_3_8 (* 0.9 dt_8)) x_3_9)) (<= x_3_9 (+ x_3_8 (* 1.1 dt_8))))  (< x_3_8 10000)) (< x_3_9 10000)))

	:assumption
	(or (not (and (not jump_8) in_3_8)) (and ( and (and (and in_3_9 (<= (+ x_3_8 (* 0.9 dt_8)) x_3_9)) (<= x_3_9 (+ x_3_8 (* 1.1 dt_8)))) (< x_3_8 10000)) (< x_3_9 10000)))

	:assumption
	(or (not (and (not jump_8) recover_3_8)) (and ( and (and (and recover_3_9 (<= (+ x_3_8 (* 0.9 dt_8)) x_3_9)) (<= x_3_9 (+ x_3_8 (* 1.1 dt_8)))) (< x_3_8 10000)) (< x_3_9 10000)))


	:assumption
	(or  (not out_3_8) (or out_3_9 in_3_9)) 
	:assumption
	(or  (not in_3_8) (or in_3_9 recover_3_9)) 
	:assumption
	(or  (not recover_3_8) (or out_3_9 recover_3_9)) 

	:assumption
( and ( and ( and ( or (not out_3_9) (not in_3_9))( or (not out_3_9) (not recover_3_9)))( or (not in_3_9) (not recover_3_9)))true ) 

	:assumption
	(or(not (and (and jump_9 out_1_9) add_1_9) ) in_1_10 )
	:assumption
	(or (not (and (and jump_9 out_1_9) in_1_10)) (and (and ( and  add_1_9 (not remove_1_9)) (> x_1_9 1)) (= x_1_10 0)))

	:assumption
	(or(not (and (and jump_9 in_1_9) remove_1_9) ) recover_1_10 )
	:assumption
	(or (not (and (and jump_9 in_1_9) recover_1_10)) (and ( and remove_1_9 (not add_1_9)) (= x_1_10 0)))

	:assumption
	(or(not (and jump_9 recover_1_9)  ) (or out_1_10 recover_1_10 ))
	:assumption
	(or (not (and (and jump_9 recover_1_9) out_1_10)) (and (and ( and (not add_1_9) (not remove_1_9)) (< x_1_9 10000)) (= x_1_10 x_1_9)))

	:assumption
	(or(not (and (and jump_9 out_1_9) out_1_10)) ( and (and (not add_1_9) (not remove_1_9) )  (= x_1_10 x_1_9)))

	:assumption
	(or(not (and (and jump_9 in_1_9) in_1_10)) ( and (and (not add_1_9) (not remove_1_9) )  (= x_1_10 x_1_9)))

	:assumption
	(or(not (and (and jump_9 recover_1_9) recover_1_10)) ( and (and (not add_1_9) (not remove_1_9) )  (= x_1_10 x_1_9)))

	:assumption
	(or (not (and (not jump_9) out_1_9)) (and ( and (and (and out_1_10 (<= (+ x_1_9 (* 0.9 dt_9)) x_1_10)) (<= x_1_10 (+ x_1_9 (* 1.1 dt_9))))  (< x_1_9 10000)) (< x_1_10 10000)))

	:assumption
	(or (not (and (not jump_9) in_1_9)) (and ( and (and (and in_1_10 (<= (+ x_1_9 (* 0.9 dt_9)) x_1_10)) (<= x_1_10 (+ x_1_9 (* 1.1 dt_9)))) (< x_1_9 10000)) (< x_1_10 10000)))

	:assumption
	(or (not (and (not jump_9) recover_1_9)) (and ( and (and (and recover_1_10 (<= (+ x_1_9 (* 0.9 dt_9)) x_1_10)) (<= x_1_10 (+ x_1_9 (* 1.1 dt_9)))) (< x_1_9 10000)) (< x_1_10 10000)))


	:assumption
	(or  (not out_1_9) (or out_1_10 in_1_10)) 
	:assumption
	(or  (not in_1_9) (or in_1_10 recover_1_10)) 
	:assumption
	(or  (not recover_1_9) (or out_1_10 recover_1_10)) 

	:assumption
( and ( and ( and ( or (not out_1_10) (not in_1_10))( or (not out_1_10) (not recover_1_10)))( or (not in_1_10) (not recover_1_10)))true ) 

	:assumption
	(or(not (and (and jump_9 out_2_9) add_2_9) ) in_2_10 )
	:assumption
	(or (not (and (and jump_9 out_2_9) in_2_10)) (and (and ( and  add_2_9 (not remove_2_9)) (> x_2_9 1)) (= x_2_10 0)))

	:assumption
	(or(not (and (and jump_9 in_2_9) remove_2_9) ) recover_2_10 )
	:assumption
	(or (not (and (and jump_9 in_2_9) recover_2_10)) (and ( and remove_2_9 (not add_2_9)) (= x_2_10 0)))

	:assumption
	(or(not (and jump_9 recover_2_9)  ) (or out_2_10 recover_2_10 ))
	:assumption
	(or (not (and (and jump_9 recover_2_9) out_2_10)) (and (and ( and (not add_2_9) (not remove_2_9)) (< x_2_9 10000)) (= x_2_10 x_2_9)))

	:assumption
	(or(not (and (and jump_9 out_2_9) out_2_10)) ( and (and (not add_2_9) (not remove_2_9) )  (= x_2_10 x_2_9)))

	:assumption
	(or(not (and (and jump_9 in_2_9) in_2_10)) ( and (and (not add_2_9) (not remove_2_9) )  (= x_2_10 x_2_9)))

	:assumption
	(or(not (and (and jump_9 recover_2_9) recover_2_10)) ( and (and (not add_2_9) (not remove_2_9) )  (= x_2_10 x_2_9)))

	:assumption
	(or (not (and (not jump_9) out_2_9)) (and ( and (and (and out_2_10 (<= (+ x_2_9 (* 0.9 dt_9)) x_2_10)) (<= x_2_10 (+ x_2_9 (* 1.1 dt_9))))  (< x_2_9 10000)) (< x_2_10 10000)))

	:assumption
	(or (not (and (not jump_9) in_2_9)) (and ( and (and (and in_2_10 (<= (+ x_2_9 (* 0.9 dt_9)) x_2_10)) (<= x_2_10 (+ x_2_9 (* 1.1 dt_9)))) (< x_2_9 10000)) (< x_2_10 10000)))

	:assumption
	(or (not (and (not jump_9) recover_2_9)) (and ( and (and (and recover_2_10 (<= (+ x_2_9 (* 0.9 dt_9)) x_2_10)) (<= x_2_10 (+ x_2_9 (* 1.1 dt_9)))) (< x_2_9 10000)) (< x_2_10 10000)))


	:assumption
	(or  (not out_2_9) (or out_2_10 in_2_10)) 
	:assumption
	(or  (not in_2_9) (or in_2_10 recover_2_10)) 
	:assumption
	(or  (not recover_2_9) (or out_2_10 recover_2_10)) 

	:assumption
( and ( and ( and ( or (not out_2_10) (not in_2_10))( or (not out_2_10) (not recover_2_10)))( or (not in_2_10) (not recover_2_10)))true ) 

	:assumption
	(or(not (and (and jump_9 out_3_9) add_3_9) ) in_3_10 )
	:assumption
	(or (not (and (and jump_9 out_3_9) in_3_10)) (and (and ( and  add_3_9 (not remove_3_9)) (> x_3_9 1)) (= x_3_10 0)))

	:assumption
	(or(not (and (and jump_9 in_3_9) remove_3_9) ) recover_3_10 )
	:assumption
	(or (not (and (and jump_9 in_3_9) recover_3_10)) (and ( and remove_3_9 (not add_3_9)) (= x_3_10 0)))

	:assumption
	(or(not (and jump_9 recover_3_9)  ) (or out_3_10 recover_3_10 ))
	:assumption
	(or (not (and (and jump_9 recover_3_9) out_3_10)) (and (and ( and (not add_3_9) (not remove_3_9)) (< x_3_9 10000)) (= x_3_10 x_3_9)))

	:assumption
	(or(not (and (and jump_9 out_3_9) out_3_10)) ( and (and (not add_3_9) (not remove_3_9) )  (= x_3_10 x_3_9)))

	:assumption
	(or(not (and (and jump_9 in_3_9) in_3_10)) ( and (and (not add_3_9) (not remove_3_9) )  (= x_3_10 x_3_9)))

	:assumption
	(or(not (and (and jump_9 recover_3_9) recover_3_10)) ( and (and (not add_3_9) (not remove_3_9) )  (= x_3_10 x_3_9)))

	:assumption
	(or (not (and (not jump_9) out_3_9)) (and ( and (and (and out_3_10 (<= (+ x_3_9 (* 0.9 dt_9)) x_3_10)) (<= x_3_10 (+ x_3_9 (* 1.1 dt_9))))  (< x_3_9 10000)) (< x_3_10 10000)))

	:assumption
	(or (not (and (not jump_9) in_3_9)) (and ( and (and (and in_3_10 (<= (+ x_3_9 (* 0.9 dt_9)) x_3_10)) (<= x_3_10 (+ x_3_9 (* 1.1 dt_9)))) (< x_3_9 10000)) (< x_3_10 10000)))

	:assumption
	(or (not (and (not jump_9) recover_3_9)) (and ( and (and (and recover_3_10 (<= (+ x_3_9 (* 0.9 dt_9)) x_3_10)) (<= x_3_10 (+ x_3_9 (* 1.1 dt_9)))) (< x_3_9 10000)) (< x_3_10 10000)))


	:assumption
	(or  (not out_3_9) (or out_3_10 in_3_10)) 
	:assumption
	(or  (not in_3_9) (or in_3_10 recover_3_10)) 
	:assumption
	(or  (not recover_3_9) (or out_3_10 recover_3_10)) 

	:assumption
( and ( and ( and ( or (not out_3_10) (not in_3_10))( or (not out_3_10) (not recover_3_10)))( or (not in_3_10) (not recover_3_10)))true ) 

	:assumption
	(or(not (and (and jump_10 out_1_10) add_1_10) ) in_1_11 )
	:assumption
	(or (not (and (and jump_10 out_1_10) in_1_11)) (and (and ( and  add_1_10 (not remove_1_10)) (> x_1_10 1)) (= x_1_11 0)))

	:assumption
	(or(not (and (and jump_10 in_1_10) remove_1_10) ) recover_1_11 )
	:assumption
	(or (not (and (and jump_10 in_1_10) recover_1_11)) (and ( and remove_1_10 (not add_1_10)) (= x_1_11 0)))

	:assumption
	(or(not (and jump_10 recover_1_10)  ) (or out_1_11 recover_1_11 ))
	:assumption
	(or (not (and (and jump_10 recover_1_10) out_1_11)) (and (and ( and (not add_1_10) (not remove_1_10)) (< x_1_10 10000)) (= x_1_11 x_1_10)))

	:assumption
	(or(not (and (and jump_10 out_1_10) out_1_11)) ( and (and (not add_1_10) (not remove_1_10) )  (= x_1_11 x_1_10)))

	:assumption
	(or(not (and (and jump_10 in_1_10) in_1_11)) ( and (and (not add_1_10) (not remove_1_10) )  (= x_1_11 x_1_10)))

	:assumption
	(or(not (and (and jump_10 recover_1_10) recover_1_11)) ( and (and (not add_1_10) (not remove_1_10) )  (= x_1_11 x_1_10)))

	:assumption
	(or (not (and (not jump_10) out_1_10)) (and ( and (and (and out_1_11 (<= (+ x_1_10 (* 0.9 dt_10)) x_1_11)) (<= x_1_11 (+ x_1_10 (* 1.1 dt_10))))  (< x_1_10 10000)) (< x_1_11 10000)))

	:assumption
	(or (not (and (not jump_10) in_1_10)) (and ( and (and (and in_1_11 (<= (+ x_1_10 (* 0.9 dt_10)) x_1_11)) (<= x_1_11 (+ x_1_10 (* 1.1 dt_10)))) (< x_1_10 10000)) (< x_1_11 10000)))

	:assumption
	(or (not (and (not jump_10) recover_1_10)) (and ( and (and (and recover_1_11 (<= (+ x_1_10 (* 0.9 dt_10)) x_1_11)) (<= x_1_11 (+ x_1_10 (* 1.1 dt_10)))) (< x_1_10 10000)) (< x_1_11 10000)))


	:assumption
	(or  (not out_1_10) (or out_1_11 in_1_11)) 
	:assumption
	(or  (not in_1_10) (or in_1_11 recover_1_11)) 
	:assumption
	(or  (not recover_1_10) (or out_1_11 recover_1_11)) 

	:assumption
( and ( and ( and ( or (not out_1_11) (not in_1_11))( or (not out_1_11) (not recover_1_11)))( or (not in_1_11) (not recover_1_11)))true ) 

	:assumption
	(or(not (and (and jump_10 out_2_10) add_2_10) ) in_2_11 )
	:assumption
	(or (not (and (and jump_10 out_2_10) in_2_11)) (and (and ( and  add_2_10 (not remove_2_10)) (> x_2_10 1)) (= x_2_11 0)))

	:assumption
	(or(not (and (and jump_10 in_2_10) remove_2_10) ) recover_2_11 )
	:assumption
	(or (not (and (and jump_10 in_2_10) recover_2_11)) (and ( and remove_2_10 (not add_2_10)) (= x_2_11 0)))

	:assumption
	(or(not (and jump_10 recover_2_10)  ) (or out_2_11 recover_2_11 ))
	:assumption
	(or (not (and (and jump_10 recover_2_10) out_2_11)) (and (and ( and (not add_2_10) (not remove_2_10)) (< x_2_10 10000)) (= x_2_11 x_2_10)))

	:assumption
	(or(not (and (and jump_10 out_2_10) out_2_11)) ( and (and (not add_2_10) (not remove_2_10) )  (= x_2_11 x_2_10)))

	:assumption
	(or(not (and (and jump_10 in_2_10) in_2_11)) ( and (and (not add_2_10) (not remove_2_10) )  (= x_2_11 x_2_10)))

	:assumption
	(or(not (and (and jump_10 recover_2_10) recover_2_11)) ( and (and (not add_2_10) (not remove_2_10) )  (= x_2_11 x_2_10)))

	:assumption
	(or (not (and (not jump_10) out_2_10)) (and ( and (and (and out_2_11 (<= (+ x_2_10 (* 0.9 dt_10)) x_2_11)) (<= x_2_11 (+ x_2_10 (* 1.1 dt_10))))  (< x_2_10 10000)) (< x_2_11 10000)))

	:assumption
	(or (not (and (not jump_10) in_2_10)) (and ( and (and (and in_2_11 (<= (+ x_2_10 (* 0.9 dt_10)) x_2_11)) (<= x_2_11 (+ x_2_10 (* 1.1 dt_10)))) (< x_2_10 10000)) (< x_2_11 10000)))

	:assumption
	(or (not (and (not jump_10) recover_2_10)) (and ( and (and (and recover_2_11 (<= (+ x_2_10 (* 0.9 dt_10)) x_2_11)) (<= x_2_11 (+ x_2_10 (* 1.1 dt_10)))) (< x_2_10 10000)) (< x_2_11 10000)))


	:assumption
	(or  (not out_2_10) (or out_2_11 in_2_11)) 
	:assumption
	(or  (not in_2_10) (or in_2_11 recover_2_11)) 
	:assumption
	(or  (not recover_2_10) (or out_2_11 recover_2_11)) 

	:assumption
( and ( and ( and ( or (not out_2_11) (not in_2_11))( or (not out_2_11) (not recover_2_11)))( or (not in_2_11) (not recover_2_11)))true ) 

	:assumption
	(or(not (and (and jump_10 out_3_10) add_3_10) ) in_3_11 )
	:assumption
	(or (not (and (and jump_10 out_3_10) in_3_11)) (and (and ( and  add_3_10 (not remove_3_10)) (> x_3_10 1)) (= x_3_11 0)))

	:assumption
	(or(not (and (and jump_10 in_3_10) remove_3_10) ) recover_3_11 )
	:assumption
	(or (not (and (and jump_10 in_3_10) recover_3_11)) (and ( and remove_3_10 (not add_3_10)) (= x_3_11 0)))

	:assumption
	(or(not (and jump_10 recover_3_10)  ) (or out_3_11 recover_3_11 ))
	:assumption
	(or (not (and (and jump_10 recover_3_10) out_3_11)) (and (and ( and (not add_3_10) (not remove_3_10)) (< x_3_10 10000)) (= x_3_11 x_3_10)))

	:assumption
	(or(not (and (and jump_10 out_3_10) out_3_11)) ( and (and (not add_3_10) (not remove_3_10) )  (= x_3_11 x_3_10)))

	:assumption
	(or(not (and (and jump_10 in_3_10) in_3_11)) ( and (and (not add_3_10) (not remove_3_10) )  (= x_3_11 x_3_10)))

	:assumption
	(or(not (and (and jump_10 recover_3_10) recover_3_11)) ( and (and (not add_3_10) (not remove_3_10) )  (= x_3_11 x_3_10)))

	:assumption
	(or (not (and (not jump_10) out_3_10)) (and ( and (and (and out_3_11 (<= (+ x_3_10 (* 0.9 dt_10)) x_3_11)) (<= x_3_11 (+ x_3_10 (* 1.1 dt_10))))  (< x_3_10 10000)) (< x_3_11 10000)))

	:assumption
	(or (not (and (not jump_10) in_3_10)) (and ( and (and (and in_3_11 (<= (+ x_3_10 (* 0.9 dt_10)) x_3_11)) (<= x_3_11 (+ x_3_10 (* 1.1 dt_10)))) (< x_3_10 10000)) (< x_3_11 10000)))

	:assumption
	(or (not (and (not jump_10) recover_3_10)) (and ( and (and (and recover_3_11 (<= (+ x_3_10 (* 0.9 dt_10)) x_3_11)) (<= x_3_11 (+ x_3_10 (* 1.1 dt_10)))) (< x_3_10 10000)) (< x_3_11 10000)))


	:assumption
	(or  (not out_3_10) (or out_3_11 in_3_11)) 
	:assumption
	(or  (not in_3_10) (or in_3_11 recover_3_11)) 
	:assumption
	(or  (not recover_3_10) (or out_3_11 recover_3_11)) 

	:assumption
( and ( and ( and ( or (not out_3_11) (not in_3_11))( or (not out_3_11) (not recover_3_11)))( or (not in_3_11) (not recover_3_11)))true ) 

	:assumption
	(or(not (and (and jump_11 out_1_11) add_1_11) ) in_1_12 )
	:assumption
	(or (not (and (and jump_11 out_1_11) in_1_12)) (and (and ( and  add_1_11 (not remove_1_11)) (> x_1_11 1)) (= x_1_12 0)))

	:assumption
	(or(not (and (and jump_11 in_1_11) remove_1_11) ) recover_1_12 )
	:assumption
	(or (not (and (and jump_11 in_1_11) recover_1_12)) (and ( and remove_1_11 (not add_1_11)) (= x_1_12 0)))

	:assumption
	(or(not (and jump_11 recover_1_11)  ) (or out_1_12 recover_1_12 ))
	:assumption
	(or (not (and (and jump_11 recover_1_11) out_1_12)) (and (and ( and (not add_1_11) (not remove_1_11)) (< x_1_11 10000)) (= x_1_12 x_1_11)))

	:assumption
	(or(not (and (and jump_11 out_1_11) out_1_12)) ( and (and (not add_1_11) (not remove_1_11) )  (= x_1_12 x_1_11)))

	:assumption
	(or(not (and (and jump_11 in_1_11) in_1_12)) ( and (and (not add_1_11) (not remove_1_11) )  (= x_1_12 x_1_11)))

	:assumption
	(or(not (and (and jump_11 recover_1_11) recover_1_12)) ( and (and (not add_1_11) (not remove_1_11) )  (= x_1_12 x_1_11)))

	:assumption
	(or (not (and (not jump_11) out_1_11)) (and ( and (and (and out_1_12 (<= (+ x_1_11 (* 0.9 dt_11)) x_1_12)) (<= x_1_12 (+ x_1_11 (* 1.1 dt_11))))  (< x_1_11 10000)) (< x_1_12 10000)))

	:assumption
	(or (not (and (not jump_11) in_1_11)) (and ( and (and (and in_1_12 (<= (+ x_1_11 (* 0.9 dt_11)) x_1_12)) (<= x_1_12 (+ x_1_11 (* 1.1 dt_11)))) (< x_1_11 10000)) (< x_1_12 10000)))

	:assumption
	(or (not (and (not jump_11) recover_1_11)) (and ( and (and (and recover_1_12 (<= (+ x_1_11 (* 0.9 dt_11)) x_1_12)) (<= x_1_12 (+ x_1_11 (* 1.1 dt_11)))) (< x_1_11 10000)) (< x_1_12 10000)))


	:assumption
	(or  (not out_1_11) (or out_1_12 in_1_12)) 
	:assumption
	(or  (not in_1_11) (or in_1_12 recover_1_12)) 
	:assumption
	(or  (not recover_1_11) (or out_1_12 recover_1_12)) 

	:assumption
( and ( and ( and ( or (not out_1_12) (not in_1_12))( or (not out_1_12) (not recover_1_12)))( or (not in_1_12) (not recover_1_12)))true ) 

	:assumption
	(or(not (and (and jump_11 out_2_11) add_2_11) ) in_2_12 )
	:assumption
	(or (not (and (and jump_11 out_2_11) in_2_12)) (and (and ( and  add_2_11 (not remove_2_11)) (> x_2_11 1)) (= x_2_12 0)))

	:assumption
	(or(not (and (and jump_11 in_2_11) remove_2_11) ) recover_2_12 )
	:assumption
	(or (not (and (and jump_11 in_2_11) recover_2_12)) (and ( and remove_2_11 (not add_2_11)) (= x_2_12 0)))

	:assumption
	(or(not (and jump_11 recover_2_11)  ) (or out_2_12 recover_2_12 ))
	:assumption
	(or (not (and (and jump_11 recover_2_11) out_2_12)) (and (and ( and (not add_2_11) (not remove_2_11)) (< x_2_11 10000)) (= x_2_12 x_2_11)))

	:assumption
	(or(not (and (and jump_11 out_2_11) out_2_12)) ( and (and (not add_2_11) (not remove_2_11) )  (= x_2_12 x_2_11)))

	:assumption
	(or(not (and (and jump_11 in_2_11) in_2_12)) ( and (and (not add_2_11) (not remove_2_11) )  (= x_2_12 x_2_11)))

	:assumption
	(or(not (and (and jump_11 recover_2_11) recover_2_12)) ( and (and (not add_2_11) (not remove_2_11) )  (= x_2_12 x_2_11)))

	:assumption
	(or (not (and (not jump_11) out_2_11)) (and ( and (and (and out_2_12 (<= (+ x_2_11 (* 0.9 dt_11)) x_2_12)) (<= x_2_12 (+ x_2_11 (* 1.1 dt_11))))  (< x_2_11 10000)) (< x_2_12 10000)))

	:assumption
	(or (not (and (not jump_11) in_2_11)) (and ( and (and (and in_2_12 (<= (+ x_2_11 (* 0.9 dt_11)) x_2_12)) (<= x_2_12 (+ x_2_11 (* 1.1 dt_11)))) (< x_2_11 10000)) (< x_2_12 10000)))

	:assumption
	(or (not (and (not jump_11) recover_2_11)) (and ( and (and (and recover_2_12 (<= (+ x_2_11 (* 0.9 dt_11)) x_2_12)) (<= x_2_12 (+ x_2_11 (* 1.1 dt_11)))) (< x_2_11 10000)) (< x_2_12 10000)))


	:assumption
	(or  (not out_2_11) (or out_2_12 in_2_12)) 
	:assumption
	(or  (not in_2_11) (or in_2_12 recover_2_12)) 
	:assumption
	(or  (not recover_2_11) (or out_2_12 recover_2_12)) 

	:assumption
( and ( and ( and ( or (not out_2_12) (not in_2_12))( or (not out_2_12) (not recover_2_12)))( or (not in_2_12) (not recover_2_12)))true ) 

	:assumption
	(or(not (and (and jump_11 out_3_11) add_3_11) ) in_3_12 )
	:assumption
	(or (not (and (and jump_11 out_3_11) in_3_12)) (and (and ( and  add_3_11 (not remove_3_11)) (> x_3_11 1)) (= x_3_12 0)))

	:assumption
	(or(not (and (and jump_11 in_3_11) remove_3_11) ) recover_3_12 )
	:assumption
	(or (not (and (and jump_11 in_3_11) recover_3_12)) (and ( and remove_3_11 (not add_3_11)) (= x_3_12 0)))

	:assumption
	(or(not (and jump_11 recover_3_11)  ) (or out_3_12 recover_3_12 ))
	:assumption
	(or (not (and (and jump_11 recover_3_11) out_3_12)) (and (and ( and (not add_3_11) (not remove_3_11)) (< x_3_11 10000)) (= x_3_12 x_3_11)))

	:assumption
	(or(not (and (and jump_11 out_3_11) out_3_12)) ( and (and (not add_3_11) (not remove_3_11) )  (= x_3_12 x_3_11)))

	:assumption
	(or(not (and (and jump_11 in_3_11) in_3_12)) ( and (and (not add_3_11) (not remove_3_11) )  (= x_3_12 x_3_11)))

	:assumption
	(or(not (and (and jump_11 recover_3_11) recover_3_12)) ( and (and (not add_3_11) (not remove_3_11) )  (= x_3_12 x_3_11)))

	:assumption
	(or (not (and (not jump_11) out_3_11)) (and ( and (and (and out_3_12 (<= (+ x_3_11 (* 0.9 dt_11)) x_3_12)) (<= x_3_12 (+ x_3_11 (* 1.1 dt_11))))  (< x_3_11 10000)) (< x_3_12 10000)))

	:assumption
	(or (not (and (not jump_11) in_3_11)) (and ( and (and (and in_3_12 (<= (+ x_3_11 (* 0.9 dt_11)) x_3_12)) (<= x_3_12 (+ x_3_11 (* 1.1 dt_11)))) (< x_3_11 10000)) (< x_3_12 10000)))

	:assumption
	(or (not (and (not jump_11) recover_3_11)) (and ( and (and (and recover_3_12 (<= (+ x_3_11 (* 0.9 dt_11)) x_3_12)) (<= x_3_12 (+ x_3_11 (* 1.1 dt_11)))) (< x_3_11 10000)) (< x_3_12 10000)))


	:assumption
	(or  (not out_3_11) (or out_3_12 in_3_12)) 
	:assumption
	(or  (not in_3_11) (or in_3_12 recover_3_12)) 
	:assumption
	(or  (not recover_3_11) (or out_3_12 recover_3_12)) 

	:assumption
( and ( and ( and ( or (not out_3_12) (not in_3_12))( or (not out_3_12) (not recover_3_12)))( or (not in_3_12) (not recover_3_12)))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 ( and  ( and true add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (>= x_4_0 16.0 ) )  (<= x_4_0 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_0)   ( and true remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (>= x_4_0 5.0 ) )  (<= x_4_0 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( and true add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (>= x_4_0 16.0 ) )  (<= x_4_0 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( and true remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (>= x_4_0 5.0 ) )  (<= x_4_0 5.9 ) )  (= x_4_1 0 ) )  )
 	:assumption
	(or(not (and (and jump_0 rod_0_0) add_3_0) ) rod_3_1 )  
	:assumption
	(or (not (and (and jump_0 rod_0_0) rod_3_1))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( and true add_3_0) )  ( not remove_3_0) )  (>= x_4_0 16.0 ) )  (<= x_4_0 16.1 ) )  (= x_4_1 0 ) )  )
 	:assumption
	(or(not (and (and jump_0 rod_3_0) remove_3_0) ) rod_0_1 )  
	:assumption
	(or (not (and (and jump_0 rod_3_0) rod_0_1))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( and true remove_3_0) )  (>= x_4_0 5.0 ) )  (<= x_4_0 5.9 ) )  (= x_4_1 0 ) )  )
 	:assumption
	(or (not (and (and jump_0 rod_0_0) rod_0_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (= x_4_0 x_4_1) )  )
 	:assumption
	(or (not (and (and jump_0 rod_1_0) rod_1_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (= x_4_0 x_4_1) )  )
 	:assumption
	(or (not (and (and jump_0 rod_2_0) rod_2_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (= x_4_0 x_4_1) )  )
 	:assumption
	(or (not (and (and jump_0 rod_3_0) rod_3_1))( and ( and ( and ( and ( and ( and  ( not add_1_0)   ( not remove_1_0) )  ( not add_2_0) )  ( not remove_2_0) )  ( not add_3_0) )  ( not remove_3_0) )  (= x_4_0 x_4_1) )  )
 
	:assumption
	(or (not (and (not jump_0) rod_0_0)) (and ( and (and (and rod_0_1 (<= (+ x_4_0 (* 0.9 dt_0)) x_4_1)) (<= x_4_1 (+ x_4_0 (* 1.1 dt_0)))) (<= x_4_0 16.1)) (<= x_4_1 16.1)))

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

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

	:assumption
	(or (not (and (not jump_0) rod_3_0)) (and ( and (and (and rod_3_1 (<= (+ x_4_0 (* 0.9 dt_0)) x_4_1)) (<= x_4_1 (+ x_4_0 (* 1.1 dt_0)))) (<= x_4_0 5.9)) (<= x_4_1 5.9)))

	:assumption
	(or  (not rod_0_0) ( or ( or ( or  rod_0_1   rod_1_1  )  rod_2_1  )  rod_3_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
	(or  (not rod_3_0) (or rod_0_1 rod_3_1)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_1) (not rod_1_1))( or (not rod_0_1) (not rod_2_1)))( or (not rod_0_1) (not rod_3_1)))( or (not rod_1_1) (not rod_2_1)))( or (not rod_1_1) (not rod_3_1)))( or (not rod_2_1) (not rod_3_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 ( and  ( and true add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (>= x_4_1 16.0 ) )  (<= x_4_1 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_1)   ( and true remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (>= x_4_1 5.0 ) )  (<= x_4_1 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( and true add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (>= x_4_1 16.0 ) )  (<= x_4_1 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( and true remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (>= x_4_1 5.0 ) )  (<= x_4_1 5.9 ) )  (= x_4_2 0 ) )  )
 	:assumption
	(or(not (and (and jump_1 rod_0_1) add_3_1) ) rod_3_2 )  
	:assumption
	(or (not (and (and jump_1 rod_0_1) rod_3_2))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( and true add_3_1) )  ( not remove_3_1) )  (>= x_4_1 16.0 ) )  (<= x_4_1 16.1 ) )  (= x_4_2 0 ) )  )
 	:assumption
	(or(not (and (and jump_1 rod_3_1) remove_3_1) ) rod_0_2 )  
	:assumption
	(or (not (and (and jump_1 rod_3_1) rod_0_2))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( and true remove_3_1) )  (>= x_4_1 5.0 ) )  (<= x_4_1 5.9 ) )  (= x_4_2 0 ) )  )
 	:assumption
	(or (not (and (and jump_1 rod_0_1) rod_0_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (= x_4_1 x_4_2) )  )
 	:assumption
	(or (not (and (and jump_1 rod_1_1) rod_1_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (= x_4_1 x_4_2) )  )
 	:assumption
	(or (not (and (and jump_1 rod_2_1) rod_2_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (= x_4_1 x_4_2) )  )
 	:assumption
	(or (not (and (and jump_1 rod_3_1) rod_3_2))( and ( and ( and ( and ( and ( and  ( not add_1_1)   ( not remove_1_1) )  ( not add_2_1) )  ( not remove_2_1) )  ( not add_3_1) )  ( not remove_3_1) )  (= x_4_1 x_4_2) )  )
 
	:assumption
	(or (not (and (not jump_1) rod_0_1)) (and ( and (and (and rod_0_2 (<= (+ x_4_1 (* 0.9 dt_1)) x_4_2)) (<= x_4_2 (+ x_4_1 (* 1.1 dt_1)))) (<= x_4_1 16.1)) (<= x_4_2 16.1)))

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

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

	:assumption
	(or (not (and (not jump_1) rod_3_1)) (and ( and (and (and rod_3_2 (<= (+ x_4_1 (* 0.9 dt_1)) x_4_2)) (<= x_4_2 (+ x_4_1 (* 1.1 dt_1)))) (<= x_4_1 5.9)) (<= x_4_2 5.9)))

	:assumption
	(or  (not rod_0_1) ( or ( or ( or  rod_0_2   rod_1_2  )  rod_2_2  )  rod_3_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
	(or  (not rod_3_1) (or rod_0_2 rod_3_2)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_2) (not rod_1_2))( or (not rod_0_2) (not rod_2_2)))( or (not rod_0_2) (not rod_3_2)))( or (not rod_1_2) (not rod_2_2)))( or (not rod_1_2) (not rod_3_2)))( or (not rod_2_2) (not rod_3_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 ( and  ( and true add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (>= x_4_2 16.0 ) )  (<= x_4_2 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_2)   ( and true remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (>= x_4_2 5.0 ) )  (<= x_4_2 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( and true add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (>= x_4_2 16.0 ) )  (<= x_4_2 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( and true remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (>= x_4_2 5.0 ) )  (<= x_4_2 5.9 ) )  (= x_4_3 0 ) )  )
 	:assumption
	(or(not (and (and jump_2 rod_0_2) add_3_2) ) rod_3_3 )  
	:assumption
	(or (not (and (and jump_2 rod_0_2) rod_3_3))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( and true add_3_2) )  ( not remove_3_2) )  (>= x_4_2 16.0 ) )  (<= x_4_2 16.1 ) )  (= x_4_3 0 ) )  )
 	:assumption
	(or(not (and (and jump_2 rod_3_2) remove_3_2) ) rod_0_3 )  
	:assumption
	(or (not (and (and jump_2 rod_3_2) rod_0_3))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( and true remove_3_2) )  (>= x_4_2 5.0 ) )  (<= x_4_2 5.9 ) )  (= x_4_3 0 ) )  )
 	:assumption
	(or (not (and (and jump_2 rod_0_2) rod_0_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (= x_4_2 x_4_3) )  )
 	:assumption
	(or (not (and (and jump_2 rod_1_2) rod_1_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (= x_4_2 x_4_3) )  )
 	:assumption
	(or (not (and (and jump_2 rod_2_2) rod_2_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (= x_4_2 x_4_3) )  )
 	:assumption
	(or (not (and (and jump_2 rod_3_2) rod_3_3))( and ( and ( and ( and ( and ( and  ( not add_1_2)   ( not remove_1_2) )  ( not add_2_2) )  ( not remove_2_2) )  ( not add_3_2) )  ( not remove_3_2) )  (= x_4_2 x_4_3) )  )
 
	:assumption
	(or (not (and (not jump_2) rod_0_2)) (and ( and (and (and rod_0_3 (<= (+ x_4_2 (* 0.9 dt_2)) x_4_3)) (<= x_4_3 (+ x_4_2 (* 1.1 dt_2)))) (<= x_4_2 16.1)) (<= x_4_3 16.1)))

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

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

	:assumption
	(or (not (and (not jump_2) rod_3_2)) (and ( and (and (and rod_3_3 (<= (+ x_4_2 (* 0.9 dt_2)) x_4_3)) (<= x_4_3 (+ x_4_2 (* 1.1 dt_2)))) (<= x_4_2 5.9)) (<= x_4_3 5.9)))

	:assumption
	(or  (not rod_0_2) ( or ( or ( or  rod_0_3   rod_1_3  )  rod_2_3  )  rod_3_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
	(or  (not rod_3_2) (or rod_0_3 rod_3_3)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_3) (not rod_1_3))( or (not rod_0_3) (not rod_2_3)))( or (not rod_0_3) (not rod_3_3)))( or (not rod_1_3) (not rod_2_3)))( or (not rod_1_3) (not rod_3_3)))( or (not rod_2_3) (not rod_3_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 ( and  ( and true add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (>= x_4_3 16.0 ) )  (<= x_4_3 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_3)   ( and true remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (>= x_4_3 5.0 ) )  (<= x_4_3 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( and true add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (>= x_4_3 16.0 ) )  (<= x_4_3 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( and true remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (>= x_4_3 5.0 ) )  (<= x_4_3 5.9 ) )  (= x_4_4 0 ) )  )
 	:assumption
	(or(not (and (and jump_3 rod_0_3) add_3_3) ) rod_3_4 )  
	:assumption
	(or (not (and (and jump_3 rod_0_3) rod_3_4))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( and true add_3_3) )  ( not remove_3_3) )  (>= x_4_3 16.0 ) )  (<= x_4_3 16.1 ) )  (= x_4_4 0 ) )  )
 	:assumption
	(or(not (and (and jump_3 rod_3_3) remove_3_3) ) rod_0_4 )  
	:assumption
	(or (not (and (and jump_3 rod_3_3) rod_0_4))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( and true remove_3_3) )  (>= x_4_3 5.0 ) )  (<= x_4_3 5.9 ) )  (= x_4_4 0 ) )  )
 	:assumption
	(or (not (and (and jump_3 rod_0_3) rod_0_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (= x_4_3 x_4_4) )  )
 	:assumption
	(or (not (and (and jump_3 rod_1_3) rod_1_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (= x_4_3 x_4_4) )  )
 	:assumption
	(or (not (and (and jump_3 rod_2_3) rod_2_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (= x_4_3 x_4_4) )  )
 	:assumption
	(or (not (and (and jump_3 rod_3_3) rod_3_4))( and ( and ( and ( and ( and ( and  ( not add_1_3)   ( not remove_1_3) )  ( not add_2_3) )  ( not remove_2_3) )  ( not add_3_3) )  ( not remove_3_3) )  (= x_4_3 x_4_4) )  )
 
	:assumption
	(or (not (and (not jump_3) rod_0_3)) (and ( and (and (and rod_0_4 (<= (+ x_4_3 (* 0.9 dt_3)) x_4_4)) (<= x_4_4 (+ x_4_3 (* 1.1 dt_3)))) (<= x_4_3 16.1)) (<= x_4_4 16.1)))

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

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

	:assumption
	(or (not (and (not jump_3) rod_3_3)) (and ( and (and (and rod_3_4 (<= (+ x_4_3 (* 0.9 dt_3)) x_4_4)) (<= x_4_4 (+ x_4_3 (* 1.1 dt_3)))) (<= x_4_3 5.9)) (<= x_4_4 5.9)))

	:assumption
	(or  (not rod_0_3) ( or ( or ( or  rod_0_4   rod_1_4  )  rod_2_4  )  rod_3_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
	(or  (not rod_3_3) (or rod_0_4 rod_3_4)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_4) (not rod_1_4))( or (not rod_0_4) (not rod_2_4)))( or (not rod_0_4) (not rod_3_4)))( or (not rod_1_4) (not rod_2_4)))( or (not rod_1_4) (not rod_3_4)))( or (not rod_2_4) (not rod_3_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 ( and  ( and true add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (>= x_4_4 16.0 ) )  (<= x_4_4 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_4)   ( and true remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (>= x_4_4 5.0 ) )  (<= x_4_4 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( and true add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (>= x_4_4 16.0 ) )  (<= x_4_4 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( and true remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (>= x_4_4 5.0 ) )  (<= x_4_4 5.9 ) )  (= x_4_5 0 ) )  )
 	:assumption
	(or(not (and (and jump_4 rod_0_4) add_3_4) ) rod_3_5 )  
	:assumption
	(or (not (and (and jump_4 rod_0_4) rod_3_5))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( and true add_3_4) )  ( not remove_3_4) )  (>= x_4_4 16.0 ) )  (<= x_4_4 16.1 ) )  (= x_4_5 0 ) )  )
 	:assumption
	(or(not (and (and jump_4 rod_3_4) remove_3_4) ) rod_0_5 )  
	:assumption
	(or (not (and (and jump_4 rod_3_4) rod_0_5))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( and true remove_3_4) )  (>= x_4_4 5.0 ) )  (<= x_4_4 5.9 ) )  (= x_4_5 0 ) )  )
 	:assumption
	(or (not (and (and jump_4 rod_0_4) rod_0_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (= x_4_4 x_4_5) )  )
 	:assumption
	(or (not (and (and jump_4 rod_1_4) rod_1_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (= x_4_4 x_4_5) )  )
 	:assumption
	(or (not (and (and jump_4 rod_2_4) rod_2_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (= x_4_4 x_4_5) )  )
 	:assumption
	(or (not (and (and jump_4 rod_3_4) rod_3_5))( and ( and ( and ( and ( and ( and  ( not add_1_4)   ( not remove_1_4) )  ( not add_2_4) )  ( not remove_2_4) )  ( not add_3_4) )  ( not remove_3_4) )  (= x_4_4 x_4_5) )  )
 
	:assumption
	(or (not (and (not jump_4) rod_0_4)) (and ( and (and (and rod_0_5 (<= (+ x_4_4 (* 0.9 dt_4)) x_4_5)) (<= x_4_5 (+ x_4_4 (* 1.1 dt_4)))) (<= x_4_4 16.1)) (<= x_4_5 16.1)))

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

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

	:assumption
	(or (not (and (not jump_4) rod_3_4)) (and ( and (and (and rod_3_5 (<= (+ x_4_4 (* 0.9 dt_4)) x_4_5)) (<= x_4_5 (+ x_4_4 (* 1.1 dt_4)))) (<= x_4_4 5.9)) (<= x_4_5 5.9)))

	:assumption
	(or  (not rod_0_4) ( or ( or ( or  rod_0_5   rod_1_5  )  rod_2_5  )  rod_3_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
	(or  (not rod_3_4) (or rod_0_5 rod_3_5)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_5) (not rod_1_5))( or (not rod_0_5) (not rod_2_5)))( or (not rod_0_5) (not rod_3_5)))( or (not rod_1_5) (not rod_2_5)))( or (not rod_1_5) (not rod_3_5)))( or (not rod_2_5) (not rod_3_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 ( and  ( and true add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (>= x_4_5 16.0 ) )  (<= x_4_5 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_5)   ( and true remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (>= x_4_5 5.0 ) )  (<= x_4_5 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( and true add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (>= x_4_5 16.0 ) )  (<= x_4_5 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( and true remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (>= x_4_5 5.0 ) )  (<= x_4_5 5.9 ) )  (= x_4_6 0 ) )  )
 	:assumption
	(or(not (and (and jump_5 rod_0_5) add_3_5) ) rod_3_6 )  
	:assumption
	(or (not (and (and jump_5 rod_0_5) rod_3_6))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( and true add_3_5) )  ( not remove_3_5) )  (>= x_4_5 16.0 ) )  (<= x_4_5 16.1 ) )  (= x_4_6 0 ) )  )
 	:assumption
	(or(not (and (and jump_5 rod_3_5) remove_3_5) ) rod_0_6 )  
	:assumption
	(or (not (and (and jump_5 rod_3_5) rod_0_6))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( and true remove_3_5) )  (>= x_4_5 5.0 ) )  (<= x_4_5 5.9 ) )  (= x_4_6 0 ) )  )
 	:assumption
	(or (not (and (and jump_5 rod_0_5) rod_0_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (= x_4_5 x_4_6) )  )
 	:assumption
	(or (not (and (and jump_5 rod_1_5) rod_1_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (= x_4_5 x_4_6) )  )
 	:assumption
	(or (not (and (and jump_5 rod_2_5) rod_2_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (= x_4_5 x_4_6) )  )
 	:assumption
	(or (not (and (and jump_5 rod_3_5) rod_3_6))( and ( and ( and ( and ( and ( and  ( not add_1_5)   ( not remove_1_5) )  ( not add_2_5) )  ( not remove_2_5) )  ( not add_3_5) )  ( not remove_3_5) )  (= x_4_5 x_4_6) )  )
 
	:assumption
	(or (not (and (not jump_5) rod_0_5)) (and ( and (and (and rod_0_6 (<= (+ x_4_5 (* 0.9 dt_5)) x_4_6)) (<= x_4_6 (+ x_4_5 (* 1.1 dt_5)))) (<= x_4_5 16.1)) (<= x_4_6 16.1)))

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

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

	:assumption
	(or (not (and (not jump_5) rod_3_5)) (and ( and (and (and rod_3_6 (<= (+ x_4_5 (* 0.9 dt_5)) x_4_6)) (<= x_4_6 (+ x_4_5 (* 1.1 dt_5)))) (<= x_4_5 5.9)) (<= x_4_6 5.9)))

	:assumption
	(or  (not rod_0_5) ( or ( or ( or  rod_0_6   rod_1_6  )  rod_2_6  )  rod_3_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
	(or  (not rod_3_5) (or rod_0_6 rod_3_6)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_6) (not rod_1_6))( or (not rod_0_6) (not rod_2_6)))( or (not rod_0_6) (not rod_3_6)))( or (not rod_1_6) (not rod_2_6)))( or (not rod_1_6) (not rod_3_6)))( or (not rod_2_6) (not rod_3_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 ( and  ( and true add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (>= x_4_6 16.0 ) )  (<= x_4_6 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_6)   ( and true remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (>= x_4_6 5.0 ) )  (<= x_4_6 5.9 ) )  (= x_4_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 ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( and true add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (>= x_4_6 16.0 ) )  (<= x_4_6 16.1 ) )  (= x_4_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 ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( and true remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (>= x_4_6 5.0 ) )  (<= x_4_6 5.9 ) )  (= x_4_7 0 ) )  )
 	:assumption
	(or(not (and (and jump_6 rod_0_6) add_3_6) ) rod_3_7 )  
	:assumption
	(or (not (and (and jump_6 rod_0_6) rod_3_7))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( and true add_3_6) )  ( not remove_3_6) )  (>= x_4_6 16.0 ) )  (<= x_4_6 16.1 ) )  (= x_4_7 0 ) )  )
 	:assumption
	(or(not (and (and jump_6 rod_3_6) remove_3_6) ) rod_0_7 )  
	:assumption
	(or (not (and (and jump_6 rod_3_6) rod_0_7))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( and true remove_3_6) )  (>= x_4_6 5.0 ) )  (<= x_4_6 5.9 ) )  (= x_4_7 0 ) )  )
 	:assumption
	(or (not (and (and jump_6 rod_0_6) rod_0_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (= x_4_6 x_4_7) )  )
 	:assumption
	(or (not (and (and jump_6 rod_1_6) rod_1_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (= x_4_6 x_4_7) )  )
 	:assumption
	(or (not (and (and jump_6 rod_2_6) rod_2_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (= x_4_6 x_4_7) )  )
 	:assumption
	(or (not (and (and jump_6 rod_3_6) rod_3_7))( and ( and ( and ( and ( and ( and  ( not add_1_6)   ( not remove_1_6) )  ( not add_2_6) )  ( not remove_2_6) )  ( not add_3_6) )  ( not remove_3_6) )  (= x_4_6 x_4_7) )  )
 
	:assumption
	(or (not (and (not jump_6) rod_0_6)) (and ( and (and (and rod_0_7 (<= (+ x_4_6 (* 0.9 dt_6)) x_4_7)) (<= x_4_7 (+ x_4_6 (* 1.1 dt_6)))) (<= x_4_6 16.1)) (<= x_4_7 16.1)))

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

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

	:assumption
	(or (not (and (not jump_6) rod_3_6)) (and ( and (and (and rod_3_7 (<= (+ x_4_6 (* 0.9 dt_6)) x_4_7)) (<= x_4_7 (+ x_4_6 (* 1.1 dt_6)))) (<= x_4_6 5.9)) (<= x_4_7 5.9)))

	:assumption
	(or  (not rod_0_6) ( or ( or ( or  rod_0_7   rod_1_7  )  rod_2_7  )  rod_3_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
	(or  (not rod_3_6) (or rod_0_7 rod_3_7)) 


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


	:assumption
	(or(not (and (and jump_7 rod_0_7) add_1_7) ) rod_1_8 )  
	:assumption
	(or (not (and (and jump_7 rod_0_7) rod_1_8))( and ( and ( and ( and ( and ( and ( and ( and  ( and true add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (>= x_4_7 16.0 ) )  (<= x_4_7 16.1 ) )  (= x_4_8 0 ) )  )
 	:assumption
	(or(not (and (and jump_7 rod_1_7) remove_1_7) ) rod_0_8 )  
	:assumption
	(or (not (and (and jump_7 rod_1_7) rod_0_8))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( and true remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (>= x_4_7 5.0 ) )  (<= x_4_7 5.9 ) )  (= x_4_8 0 ) )  )
 	:assumption
	(or(not (and (and jump_7 rod_0_7) add_2_7) ) rod_2_8 )  
	:assumption
	(or (not (and (and jump_7 rod_0_7) rod_2_8))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( and true add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (>= x_4_7 16.0 ) )  (<= x_4_7 16.1 ) )  (= x_4_8 0 ) )  )
 	:assumption
	(or(not (and (and jump_7 rod_2_7) remove_2_7) ) rod_0_8 )  
	:assumption
	(or (not (and (and jump_7 rod_2_7) rod_0_8))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( and true remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (>= x_4_7 5.0 ) )  (<= x_4_7 5.9 ) )  (= x_4_8 0 ) )  )
 	:assumption
	(or(not (and (and jump_7 rod_0_7) add_3_7) ) rod_3_8 )  
	:assumption
	(or (not (and (and jump_7 rod_0_7) rod_3_8))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( and true add_3_7) )  ( not remove_3_7) )  (>= x_4_7 16.0 ) )  (<= x_4_7 16.1 ) )  (= x_4_8 0 ) )  )
 	:assumption
	(or(not (and (and jump_7 rod_3_7) remove_3_7) ) rod_0_8 )  
	:assumption
	(or (not (and (and jump_7 rod_3_7) rod_0_8))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( and true remove_3_7) )  (>= x_4_7 5.0 ) )  (<= x_4_7 5.9 ) )  (= x_4_8 0 ) )  )
 	:assumption
	(or (not (and (and jump_7 rod_0_7) rod_0_8))( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (= x_4_7 x_4_8) )  )
 	:assumption
	(or (not (and (and jump_7 rod_1_7) rod_1_8))( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (= x_4_7 x_4_8) )  )
 	:assumption
	(or (not (and (and jump_7 rod_2_7) rod_2_8))( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (= x_4_7 x_4_8) )  )
 	:assumption
	(or (not (and (and jump_7 rod_3_7) rod_3_8))( and ( and ( and ( and ( and ( and  ( not add_1_7)   ( not remove_1_7) )  ( not add_2_7) )  ( not remove_2_7) )  ( not add_3_7) )  ( not remove_3_7) )  (= x_4_7 x_4_8) )  )
 
	:assumption
	(or (not (and (not jump_7) rod_0_7)) (and ( and (and (and rod_0_8 (<= (+ x_4_7 (* 0.9 dt_7)) x_4_8)) (<= x_4_8 (+ x_4_7 (* 1.1 dt_7)))) (<= x_4_7 16.1)) (<= x_4_8 16.1)))

	:assumption
	(or (not (and (not jump_7) rod_1_7)) (and ( and (and (and rod_1_8 (<= (+ x_4_7 (* 0.9 dt_7)) x_4_8)) (<= x_4_8 (+ x_4_7 (* 1.1 dt_7)))) (<= x_4_7 5.9)) (<= x_4_8 5.9)))

	:assumption
	(or (not (and (not jump_7) rod_2_7)) (and ( and (and (and rod_2_8 (<= (+ x_4_7 (* 0.9 dt_7)) x_4_8)) (<= x_4_8 (+ x_4_7 (* 1.1 dt_7)))) (<= x_4_7 5.9)) (<= x_4_8 5.9)))

	:assumption
	(or (not (and (not jump_7) rod_3_7)) (and ( and (and (and rod_3_8 (<= (+ x_4_7 (* 0.9 dt_7)) x_4_8)) (<= x_4_8 (+ x_4_7 (* 1.1 dt_7)))) (<= x_4_7 5.9)) (<= x_4_8 5.9)))

	:assumption
	(or  (not rod_0_7) ( or ( or ( or  rod_0_8   rod_1_8  )  rod_2_8  )  rod_3_8  ) ) 
	:assumption
	(or  (not rod_1_7) (or rod_0_8 rod_1_8)) 
	:assumption
	(or  (not rod_2_7) (or rod_0_8 rod_2_8)) 
	:assumption
	(or  (not rod_3_7) (or rod_0_8 rod_3_8)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_8) (not rod_1_8))( or (not rod_0_8) (not rod_2_8)))( or (not rod_0_8) (not rod_3_8)))( or (not rod_1_8) (not rod_2_8)))( or (not rod_1_8) (not rod_3_8)))( or (not rod_2_8) (not rod_3_8)))true ) 


	:assumption
	(or(not (and (and jump_8 rod_0_8) add_1_8) ) rod_1_9 )  
	:assumption
	(or (not (and (and jump_8 rod_0_8) rod_1_9))( and ( and ( and ( and ( and ( and ( and ( and  ( and true add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (>= x_4_8 16.0 ) )  (<= x_4_8 16.1 ) )  (= x_4_9 0 ) )  )
 	:assumption
	(or(not (and (and jump_8 rod_1_8) remove_1_8) ) rod_0_9 )  
	:assumption
	(or (not (and (and jump_8 rod_1_8) rod_0_9))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( and true remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (>= x_4_8 5.0 ) )  (<= x_4_8 5.9 ) )  (= x_4_9 0 ) )  )
 	:assumption
	(or(not (and (and jump_8 rod_0_8) add_2_8) ) rod_2_9 )  
	:assumption
	(or (not (and (and jump_8 rod_0_8) rod_2_9))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( and true add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (>= x_4_8 16.0 ) )  (<= x_4_8 16.1 ) )  (= x_4_9 0 ) )  )
 	:assumption
	(or(not (and (and jump_8 rod_2_8) remove_2_8) ) rod_0_9 )  
	:assumption
	(or (not (and (and jump_8 rod_2_8) rod_0_9))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( and true remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (>= x_4_8 5.0 ) )  (<= x_4_8 5.9 ) )  (= x_4_9 0 ) )  )
 	:assumption
	(or(not (and (and jump_8 rod_0_8) add_3_8) ) rod_3_9 )  
	:assumption
	(or (not (and (and jump_8 rod_0_8) rod_3_9))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( and true add_3_8) )  ( not remove_3_8) )  (>= x_4_8 16.0 ) )  (<= x_4_8 16.1 ) )  (= x_4_9 0 ) )  )
 	:assumption
	(or(not (and (and jump_8 rod_3_8) remove_3_8) ) rod_0_9 )  
	:assumption
	(or (not (and (and jump_8 rod_3_8) rod_0_9))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( and true remove_3_8) )  (>= x_4_8 5.0 ) )  (<= x_4_8 5.9 ) )  (= x_4_9 0 ) )  )
 	:assumption
	(or (not (and (and jump_8 rod_0_8) rod_0_9))( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (= x_4_8 x_4_9) )  )
 	:assumption
	(or (not (and (and jump_8 rod_1_8) rod_1_9))( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (= x_4_8 x_4_9) )  )
 	:assumption
	(or (not (and (and jump_8 rod_2_8) rod_2_9))( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (= x_4_8 x_4_9) )  )
 	:assumption
	(or (not (and (and jump_8 rod_3_8) rod_3_9))( and ( and ( and ( and ( and ( and  ( not add_1_8)   ( not remove_1_8) )  ( not add_2_8) )  ( not remove_2_8) )  ( not add_3_8) )  ( not remove_3_8) )  (= x_4_8 x_4_9) )  )
 
	:assumption
	(or (not (and (not jump_8) rod_0_8)) (and ( and (and (and rod_0_9 (<= (+ x_4_8 (* 0.9 dt_8)) x_4_9)) (<= x_4_9 (+ x_4_8 (* 1.1 dt_8)))) (<= x_4_8 16.1)) (<= x_4_9 16.1)))

	:assumption
	(or (not (and (not jump_8) rod_1_8)) (and ( and (and (and rod_1_9 (<= (+ x_4_8 (* 0.9 dt_8)) x_4_9)) (<= x_4_9 (+ x_4_8 (* 1.1 dt_8)))) (<= x_4_8 5.9)) (<= x_4_9 5.9)))

	:assumption
	(or (not (and (not jump_8) rod_2_8)) (and ( and (and (and rod_2_9 (<= (+ x_4_8 (* 0.9 dt_8)) x_4_9)) (<= x_4_9 (+ x_4_8 (* 1.1 dt_8)))) (<= x_4_8 5.9)) (<= x_4_9 5.9)))

	:assumption
	(or (not (and (not jump_8) rod_3_8)) (and ( and (and (and rod_3_9 (<= (+ x_4_8 (* 0.9 dt_8)) x_4_9)) (<= x_4_9 (+ x_4_8 (* 1.1 dt_8)))) (<= x_4_8 5.9)) (<= x_4_9 5.9)))

	:assumption
	(or  (not rod_0_8) ( or ( or ( or  rod_0_9   rod_1_9  )  rod_2_9  )  rod_3_9  ) ) 
	:assumption
	(or  (not rod_1_8) (or rod_0_9 rod_1_9)) 
	:assumption
	(or  (not rod_2_8) (or rod_0_9 rod_2_9)) 
	:assumption
	(or  (not rod_3_8) (or rod_0_9 rod_3_9)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_9) (not rod_1_9))( or (not rod_0_9) (not rod_2_9)))( or (not rod_0_9) (not rod_3_9)))( or (not rod_1_9) (not rod_2_9)))( or (not rod_1_9) (not rod_3_9)))( or (not rod_2_9) (not rod_3_9)))true ) 


	:assumption
	(or(not (and (and jump_9 rod_0_9) add_1_9) ) rod_1_10 )  
	:assumption
	(or (not (and (and jump_9 rod_0_9) rod_1_10))( and ( and ( and ( and ( and ( and ( and ( and  ( and true add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (>= x_4_9 16.0 ) )  (<= x_4_9 16.1 ) )  (= x_4_10 0 ) )  )
 	:assumption
	(or(not (and (and jump_9 rod_1_9) remove_1_9) ) rod_0_10 )  
	:assumption
	(or (not (and (and jump_9 rod_1_9) rod_0_10))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( and true remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (>= x_4_9 5.0 ) )  (<= x_4_9 5.9 ) )  (= x_4_10 0 ) )  )
 	:assumption
	(or(not (and (and jump_9 rod_0_9) add_2_9) ) rod_2_10 )  
	:assumption
	(or (not (and (and jump_9 rod_0_9) rod_2_10))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( and true add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (>= x_4_9 16.0 ) )  (<= x_4_9 16.1 ) )  (= x_4_10 0 ) )  )
 	:assumption
	(or(not (and (and jump_9 rod_2_9) remove_2_9) ) rod_0_10 )  
	:assumption
	(or (not (and (and jump_9 rod_2_9) rod_0_10))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( and true remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (>= x_4_9 5.0 ) )  (<= x_4_9 5.9 ) )  (= x_4_10 0 ) )  )
 	:assumption
	(or(not (and (and jump_9 rod_0_9) add_3_9) ) rod_3_10 )  
	:assumption
	(or (not (and (and jump_9 rod_0_9) rod_3_10))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( and true add_3_9) )  ( not remove_3_9) )  (>= x_4_9 16.0 ) )  (<= x_4_9 16.1 ) )  (= x_4_10 0 ) )  )
 	:assumption
	(or(not (and (and jump_9 rod_3_9) remove_3_9) ) rod_0_10 )  
	:assumption
	(or (not (and (and jump_9 rod_3_9) rod_0_10))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( and true remove_3_9) )  (>= x_4_9 5.0 ) )  (<= x_4_9 5.9 ) )  (= x_4_10 0 ) )  )
 	:assumption
	(or (not (and (and jump_9 rod_0_9) rod_0_10))( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (= x_4_9 x_4_10) )  )
 	:assumption
	(or (not (and (and jump_9 rod_1_9) rod_1_10))( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (= x_4_9 x_4_10) )  )
 	:assumption
	(or (not (and (and jump_9 rod_2_9) rod_2_10))( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (= x_4_9 x_4_10) )  )
 	:assumption
	(or (not (and (and jump_9 rod_3_9) rod_3_10))( and ( and ( and ( and ( and ( and  ( not add_1_9)   ( not remove_1_9) )  ( not add_2_9) )  ( not remove_2_9) )  ( not add_3_9) )  ( not remove_3_9) )  (= x_4_9 x_4_10) )  )
 
	:assumption
	(or (not (and (not jump_9) rod_0_9)) (and ( and (and (and rod_0_10 (<= (+ x_4_9 (* 0.9 dt_9)) x_4_10)) (<= x_4_10 (+ x_4_9 (* 1.1 dt_9)))) (<= x_4_9 16.1)) (<= x_4_10 16.1)))

	:assumption
	(or (not (and (not jump_9) rod_1_9)) (and ( and (and (and rod_1_10 (<= (+ x_4_9 (* 0.9 dt_9)) x_4_10)) (<= x_4_10 (+ x_4_9 (* 1.1 dt_9)))) (<= x_4_9 5.9)) (<= x_4_10 5.9)))

	:assumption
	(or (not (and (not jump_9) rod_2_9)) (and ( and (and (and rod_2_10 (<= (+ x_4_9 (* 0.9 dt_9)) x_4_10)) (<= x_4_10 (+ x_4_9 (* 1.1 dt_9)))) (<= x_4_9 5.9)) (<= x_4_10 5.9)))

	:assumption
	(or (not (and (not jump_9) rod_3_9)) (and ( and (and (and rod_3_10 (<= (+ x_4_9 (* 0.9 dt_9)) x_4_10)) (<= x_4_10 (+ x_4_9 (* 1.1 dt_9)))) (<= x_4_9 5.9)) (<= x_4_10 5.9)))

	:assumption
	(or  (not rod_0_9) ( or ( or ( or  rod_0_10   rod_1_10  )  rod_2_10  )  rod_3_10  ) ) 
	:assumption
	(or  (not rod_1_9) (or rod_0_10 rod_1_10)) 
	:assumption
	(or  (not rod_2_9) (or rod_0_10 rod_2_10)) 
	:assumption
	(or  (not rod_3_9) (or rod_0_10 rod_3_10)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_10) (not rod_1_10))( or (not rod_0_10) (not rod_2_10)))( or (not rod_0_10) (not rod_3_10)))( or (not rod_1_10) (not rod_2_10)))( or (not rod_1_10) (not rod_3_10)))( or (not rod_2_10) (not rod_3_10)))true ) 


	:assumption
	(or(not (and (and jump_10 rod_0_10) add_1_10) ) rod_1_11 )  
	:assumption
	(or (not (and (and jump_10 rod_0_10) rod_1_11))( and ( and ( and ( and ( and ( and ( and ( and  ( and true add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (>= x_4_10 16.0 ) )  (<= x_4_10 16.1 ) )  (= x_4_11 0 ) )  )
 	:assumption
	(or(not (and (and jump_10 rod_1_10) remove_1_10) ) rod_0_11 )  
	:assumption
	(or (not (and (and jump_10 rod_1_10) rod_0_11))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( and true remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (>= x_4_10 5.0 ) )  (<= x_4_10 5.9 ) )  (= x_4_11 0 ) )  )
 	:assumption
	(or(not (and (and jump_10 rod_0_10) add_2_10) ) rod_2_11 )  
	:assumption
	(or (not (and (and jump_10 rod_0_10) rod_2_11))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( and true add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (>= x_4_10 16.0 ) )  (<= x_4_10 16.1 ) )  (= x_4_11 0 ) )  )
 	:assumption
	(or(not (and (and jump_10 rod_2_10) remove_2_10) ) rod_0_11 )  
	:assumption
	(or (not (and (and jump_10 rod_2_10) rod_0_11))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( and true remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (>= x_4_10 5.0 ) )  (<= x_4_10 5.9 ) )  (= x_4_11 0 ) )  )
 	:assumption
	(or(not (and (and jump_10 rod_0_10) add_3_10) ) rod_3_11 )  
	:assumption
	(or (not (and (and jump_10 rod_0_10) rod_3_11))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( and true add_3_10) )  ( not remove_3_10) )  (>= x_4_10 16.0 ) )  (<= x_4_10 16.1 ) )  (= x_4_11 0 ) )  )
 	:assumption
	(or(not (and (and jump_10 rod_3_10) remove_3_10) ) rod_0_11 )  
	:assumption
	(or (not (and (and jump_10 rod_3_10) rod_0_11))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( and true remove_3_10) )  (>= x_4_10 5.0 ) )  (<= x_4_10 5.9 ) )  (= x_4_11 0 ) )  )
 	:assumption
	(or (not (and (and jump_10 rod_0_10) rod_0_11))( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (= x_4_10 x_4_11) )  )
 	:assumption
	(or (not (and (and jump_10 rod_1_10) rod_1_11))( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (= x_4_10 x_4_11) )  )
 	:assumption
	(or (not (and (and jump_10 rod_2_10) rod_2_11))( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (= x_4_10 x_4_11) )  )
 	:assumption
	(or (not (and (and jump_10 rod_3_10) rod_3_11))( and ( and ( and ( and ( and ( and  ( not add_1_10)   ( not remove_1_10) )  ( not add_2_10) )  ( not remove_2_10) )  ( not add_3_10) )  ( not remove_3_10) )  (= x_4_10 x_4_11) )  )
 
	:assumption
	(or (not (and (not jump_10) rod_0_10)) (and ( and (and (and rod_0_11 (<= (+ x_4_10 (* 0.9 dt_10)) x_4_11)) (<= x_4_11 (+ x_4_10 (* 1.1 dt_10)))) (<= x_4_10 16.1)) (<= x_4_11 16.1)))

	:assumption
	(or (not (and (not jump_10) rod_1_10)) (and ( and (and (and rod_1_11 (<= (+ x_4_10 (* 0.9 dt_10)) x_4_11)) (<= x_4_11 (+ x_4_10 (* 1.1 dt_10)))) (<= x_4_10 5.9)) (<= x_4_11 5.9)))

	:assumption
	(or (not (and (not jump_10) rod_2_10)) (and ( and (and (and rod_2_11 (<= (+ x_4_10 (* 0.9 dt_10)) x_4_11)) (<= x_4_11 (+ x_4_10 (* 1.1 dt_10)))) (<= x_4_10 5.9)) (<= x_4_11 5.9)))

	:assumption
	(or (not (and (not jump_10) rod_3_10)) (and ( and (and (and rod_3_11 (<= (+ x_4_10 (* 0.9 dt_10)) x_4_11)) (<= x_4_11 (+ x_4_10 (* 1.1 dt_10)))) (<= x_4_10 5.9)) (<= x_4_11 5.9)))

	:assumption
	(or  (not rod_0_10) ( or ( or ( or  rod_0_11   rod_1_11  )  rod_2_11  )  rod_3_11  ) ) 
	:assumption
	(or  (not rod_1_10) (or rod_0_11 rod_1_11)) 
	:assumption
	(or  (not rod_2_10) (or rod_0_11 rod_2_11)) 
	:assumption
	(or  (not rod_3_10) (or rod_0_11 rod_3_11)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_11) (not rod_1_11))( or (not rod_0_11) (not rod_2_11)))( or (not rod_0_11) (not rod_3_11)))( or (not rod_1_11) (not rod_2_11)))( or (not rod_1_11) (not rod_3_11)))( or (not rod_2_11) (not rod_3_11)))true ) 


	:assumption
	(or(not (and (and jump_11 rod_0_11) add_1_11) ) rod_1_12 )  
	:assumption
	(or (not (and (and jump_11 rod_0_11) rod_1_12))( and ( and ( and ( and ( and ( and ( and ( and  ( and true add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (>= x_4_11 16.0 ) )  (<= x_4_11 16.1 ) )  (= x_4_12 0 ) )  )
 	:assumption
	(or(not (and (and jump_11 rod_1_11) remove_1_11) ) rod_0_12 )  
	:assumption
	(or (not (and (and jump_11 rod_1_11) rod_0_12))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( and true remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (>= x_4_11 5.0 ) )  (<= x_4_11 5.9 ) )  (= x_4_12 0 ) )  )
 	:assumption
	(or(not (and (and jump_11 rod_0_11) add_2_11) ) rod_2_12 )  
	:assumption
	(or (not (and (and jump_11 rod_0_11) rod_2_12))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( and true add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (>= x_4_11 16.0 ) )  (<= x_4_11 16.1 ) )  (= x_4_12 0 ) )  )
 	:assumption
	(or(not (and (and jump_11 rod_2_11) remove_2_11) ) rod_0_12 )  
	:assumption
	(or (not (and (and jump_11 rod_2_11) rod_0_12))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( and true remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (>= x_4_11 5.0 ) )  (<= x_4_11 5.9 ) )  (= x_4_12 0 ) )  )
 	:assumption
	(or(not (and (and jump_11 rod_0_11) add_3_11) ) rod_3_12 )  
	:assumption
	(or (not (and (and jump_11 rod_0_11) rod_3_12))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( and true add_3_11) )  ( not remove_3_11) )  (>= x_4_11 16.0 ) )  (<= x_4_11 16.1 ) )  (= x_4_12 0 ) )  )
 	:assumption
	(or(not (and (and jump_11 rod_3_11) remove_3_11) ) rod_0_12 )  
	:assumption
	(or (not (and (and jump_11 rod_3_11) rod_0_12))( and ( and ( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( and true remove_3_11) )  (>= x_4_11 5.0 ) )  (<= x_4_11 5.9 ) )  (= x_4_12 0 ) )  )
 	:assumption
	(or (not (and (and jump_11 rod_0_11) rod_0_12))( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (= x_4_11 x_4_12) )  )
 	:assumption
	(or (not (and (and jump_11 rod_1_11) rod_1_12))( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (= x_4_11 x_4_12) )  )
 	:assumption
	(or (not (and (and jump_11 rod_2_11) rod_2_12))( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (= x_4_11 x_4_12) )  )
 	:assumption
	(or (not (and (and jump_11 rod_3_11) rod_3_12))( and ( and ( and ( and ( and ( and  ( not add_1_11)   ( not remove_1_11) )  ( not add_2_11) )  ( not remove_2_11) )  ( not add_3_11) )  ( not remove_3_11) )  (= x_4_11 x_4_12) )  )
 
	:assumption
	(or (not (and (not jump_11) rod_0_11)) (and ( and (and (and rod_0_12 (<= (+ x_4_11 (* 0.9 dt_11)) x_4_12)) (<= x_4_12 (+ x_4_11 (* 1.1 dt_11)))) (<= x_4_11 16.1)) (<= x_4_12 16.1)))

	:assumption
	(or (not (and (not jump_11) rod_1_11)) (and ( and (and (and rod_1_12 (<= (+ x_4_11 (* 0.9 dt_11)) x_4_12)) (<= x_4_12 (+ x_4_11 (* 1.1 dt_11)))) (<= x_4_11 5.9)) (<= x_4_12 5.9)))

	:assumption
	(or (not (and (not jump_11) rod_2_11)) (and ( and (and (and rod_2_12 (<= (+ x_4_11 (* 0.9 dt_11)) x_4_12)) (<= x_4_12 (+ x_4_11 (* 1.1 dt_11)))) (<= x_4_11 5.9)) (<= x_4_12 5.9)))

	:assumption
	(or (not (and (not jump_11) rod_3_11)) (and ( and (and (and rod_3_12 (<= (+ x_4_11 (* 0.9 dt_11)) x_4_12)) (<= x_4_12 (+ x_4_11 (* 1.1 dt_11)))) (<= x_4_11 5.9)) (<= x_4_12 5.9)))

	:assumption
	(or  (not rod_0_11) ( or ( or ( or  rod_0_12   rod_1_12  )  rod_2_12  )  rod_3_12  ) ) 
	:assumption
	(or  (not rod_1_11) (or rod_0_12 rod_1_12)) 
	:assumption
	(or  (not rod_2_11) (or rod_0_12 rod_2_12)) 
	:assumption
	(or  (not rod_3_11) (or rod_0_12 rod_3_12)) 


	:assumption
( and ( and ( and ( and ( and ( and ( or (not rod_0_12) (not rod_1_12))( or (not rod_0_12) (not rod_2_12)))( or (not rod_0_12) (not rod_3_12)))( or (not rod_1_12) (not rod_2_12)))( or (not rod_1_12) (not rod_3_12)))( or (not rod_2_12) (not rod_3_12)))true ) 


	:formula
	( or ( or ( or ( or ( or ( or ( or ( or ( or ( or ( or ( or ( and ( and ( and  recover_1_0   recover_2_0 )  recover_3_0 )  rod_0_0 )  ( and ( and ( and  recover_1_1   recover_2_1 )  recover_3_1 )  rod_0_1 ) ) ( and ( and ( and  recover_1_2   recover_2_2 )  recover_3_2 )  rod_0_2 ) ) ( and ( and ( and  recover_1_3   recover_2_3 )  recover_3_3 )  rod_0_3 ) ) ( and ( and ( and  recover_1_4   recover_2_4 )  recover_3_4 )  rod_0_4 ) ) ( and ( and ( and  recover_1_5   recover_2_5 )  recover_3_5 )  rod_0_5 ) ) ( and ( and ( and  recover_1_6   recover_2_6 )  recover_3_6 )  rod_0_6 ) ) ( and ( and ( and  recover_1_7   recover_2_7 )  recover_3_7 )  rod_0_7 ) ) ( and ( and ( and  recover_1_8   recover_2_8 )  recover_3_8 )  rod_0_8 ) ) ( and ( and ( and  recover_1_9   recover_2_9 )  recover_3_9 )  rod_0_9 ) ) ( and ( and ( and  recover_1_10   recover_2_10 )  recover_3_10 )  rod_0_10 ) ) ( and ( and ( and  recover_1_11   recover_2_11 )  recover_3_11 )  rod_0_11 ) ) ( and ( and ( and  recover_1_12   recover_2_12 )  recover_3_12 )  rod_0_12 ) ) )
