search

aditink / algebraic_simplification_cesar

Egg Heuristics for algebraic simplification used by the CESAR tool.
GNU General Public License v2.0
2 stars 3 forks source link

Setup testing #2

Open aditink opened 2 weeks ago

aditink commented 2 weeks ago

Create a framework that runs test formula/assumption pairs to check for regression.

aditink commented 2 weeks ago

@zhufangu is working on this.

aditink commented 2 weeks ago

Here are some cases to include:

Formula Assumption Result
(and (or (> B ( (^ (+ ( 2 e) (* (- 2) p)) (- 1)) (^ v 2))) (<= v 0)) (> e p)) (and (> A 0) (and (> B 0) (and (> T 0) (>= v 0)))) (> ( B ( 2 (- e p))) (^ v 2))
(< (+ ( A T) v) (^ ( ( B (^ (+ A B) (- 1))) (+ (+ ( ( 2 A) e) ( (* (- 2) A) p)) (^ v 2))) (/ 1 2))) (and (> ( B ( 2 (- e p))) (^ v 2)) (and (> A 0) (and (> B 0) (and (> T 0) (>= v 0))))) (< (+ ( A T) v) (^ ( B ( (^ (+ A B) (- 1)) (+ ( (* A 2) (- e p)) (^ v 2)))) (/ 1 2)))
(> (+ (+ e ( ( (/ 1 2) B) (^ t 2))) ( ( (- 1) t) v)) p) (and (or (<= B (* (^ t (- 1)) v)) (<= t 0)) (and (> A 0) (and (> B 0) (and (> T 0) (and (>= v 0) (>= t 0)))))) (> (- (+ e ( (/ 1 2) ( B (^ t 2)))) (* t v)) p)
(> ( B (+ (+ ( 2 e) ( (- 2) p)) ( ( (- 1) t) (+ ( A t) ( 2 v))))) (^ (+ ( A t) v) 2)) (and (>= t 0) (and (>= v 0) (and (> A 0) (and (> B 0) (and (<= t T) (> T 0)))))) (> ( B (- ( 2 (- e p)) ( t (+ ( t A) ( 2 v))))) (^ (+ ( t A) v) 2))
(or (and (= e 0) (or (and (= v 0) (< (+ ( ( 2 B) p) ( ( A (+ A B)) (^ T 2))) 0)) (and (> v 0) (< (+ (+ ( ( 2 B) p) (^ (+ ( A T) v) 2)) ( ( B T) (+ ( A T) ( 2 v)))) 0)))) (and (distinct e 0) (or (and (= v 0) (< (+ p ( ( ( ( (/ 1 2) A) (^ B (- 1))) (+ A B)) (^ T 2))) e)) (and (> v 0) (< (+ (^ (+ ( A T) v) 2) ( B (+ (+ (+ ( (- 2) e) ( 2 p)) ( A (^ T 2))) ( ( 2 T) v)))) 0))))) (and (> ( 2 ( B (- e p))) (^ v 2)) (and (> A 0) (and (> B 0) (and (> T 0) (>= v 0))))) (or (and (= e 0) (< (+ (+ ( 2 ( B p)) (^ (+ ( A T) v) 2)) ( ( B T) (+ ( A T) ( 2 v)))) 0)) (and (distinct e 0) (< (+ (^ (+ ( A T) v) 2) ( B (+ (+ ( 2 (- p e)) ( A (^ T 2))) ( v (* 2 T))))) 0)))
(or (and (< (+ (+ Tx ( ( 2 T) V)) y) (+ Ty x)) (or (and (= Tx x) (> Ty y)) (or (and (> (+ Tx Ty) (+ x y)) (< Tx x)) (and (> Tx x) (and (> x 0) (< (+ Tx y) (+ Ty x))))))) (or (and (= x 0) (< (+ Tx y) Ty)) (or (and (< Tx x) (and (< (+ Tx (* T V)) x) (<= (+ Tx Ty) (+ x y)))) (or (and (< (+ (+ Tx x) y) Ty) (or (and (> (+ Tx x) 0) (< x 0)) (or (<= Tx x) (> x 0)))) (or (< (+ Tx x) 0) (and (> Ty y) (<= (+ Tx x) 0))))))) (and (or (and (< y Ty) (or (> Ty (+ (+ Tx x) y)) (> (+ Ty x) (+ Tx y)))) (or (< Tx x) (< (+ Tx x) 0))) (and (> Tx 0) (and (> Ty 0) (and (> V 0) (> T 0))))) (or (and (< (+ (+ Tx ( 2 ( T V))) y) (+ Ty x)) (or (and (> Tx x) (> x 0)) (and (> (+ Tx Ty) (+ x y)) (<= Tx x)))) (or (or (= x 0) (or (< (+ Tx x) 0) (and (> Ty y) (<= (+ Tx x) 0)))) (or (and (< (+ (+ Tx x) y) Ty) (or (> x 0) (and (> (+ Tx x) 0) (< x 0)))) (and (< (+ Tx (* T V)) x) (<= (+ Tx Ty) (+ x y))))))
(or (and (< (+ (+ (+ Tx ( ( 2 T) V)) x) y) Ty) (or (and (= (+ Tx x) 0) (> Ty y)) (or (and (> (+ Tx x) 0) (and (< x 0) (< (+ (+ Tx x) y) Ty))) (and (> (+ (+ Tx Ty) x) y) (< (+ Tx x) 0))))) (or (< Tx x) (or (and (< (+ Tx y) (+ Ty x)) (or (< x 0) (or (> Tx x) (<= (+ Tx x) 0)))) (or (and (< (+ Tx x) 0) (and (< (+ (+ Tx (* T V)) x) 0) (<= (+ (+ Tx Ty) x) y))) (and (<= Tx x) (> Ty y)))))) (and (or (and (< y Ty) (or (> Ty (+ (+ Tx x) y)) (> (+ Ty x) (+ Tx y)))) (or (< Tx x) (< (+ Tx x) 0))) (and (> Tx 0) (and (> Ty 0) (and (> V 0) (> T 0))))) (or (and (< (+ (+ (+ Tx ( 2 ( T V))) x) y) Ty) (or (and (> (+ Tx x) 0) (< x 0)) (and (> (+ (+ Tx Ty) x) y) (<= (+ Tx x) 0)))) (or (< Tx x) (or (and (< (+ Tx y) (+ Ty x)) (> Tx x)) (or (and (< (+ (+ Tx (* T V)) x) 0) (<= (+ (+ Tx Ty) x) y)) (and (> Ty y) (<= Tx x))))))
(or (= x 0) (or (< (+ Tx x) 0) (or (and (< (+ (+ Tx ( ( 2 T) V)) y) (+ Ty x)) (and (or (> Tx x) (> (+ Tx Ty) (+ x y))) (or (<= Tx x) (>= x 0)))) (or (and (= (+ Tx x) 0) (> Ty y)) (or (and (< (+ (+ Tx x) y) Ty) (or (>= x 0) (distinct (+ Tx x) 0))) (and (< (+ Tx (* T V)) x) (<= (+ Tx Ty) (+ x y)))))))) (and (or (and (< y Ty) (or (> Ty (+ (+ Tx x) y)) (> (+ Ty x) (+ Tx y)))) (or (< Tx x) (< (+ Tx x) 0))) (and (> Tx 0) (and (> Ty 0) (and (> V 0) (> T 0))))) (or (and (< (+ (+ Tx ( 2 ( T V))) y) (+ Ty x)) (and (> (+ Tx Ty) (+ x y)) (>= x 0))) (or (and (< (+ Tx (* T V)) x) (<= (+ Tx Ty) (+ x y))) (or (and (< (+ (+ Tx x) y) Ty) (distinct (+ Tx x) 0)) (or (< (+ Tx x) 0) (= 0 (+ Tx x))))))
(or (<= (+ Tx x) 0) (or (and (< (+ Tx ( T V)) x) (<= (+ Tx Ty) (+ x y))) (or (and (> (+ Tx Ty) (+ x y)) (and (>= x 0) (< (+ (+ Tx ( (* 2 T) V)) y) (+ Ty x)))) (< (+ (+ Tx x) y) Ty)))) (and (or (and (< y Ty) (or (> Ty (+ (+ Tx x) y)) (> (+ Ty x) (+ Tx y)))) (or (< Tx x) (< (+ Tx x) 0))) (and (> Tx 0) (and (> Ty 0) (and (> V 0) (> T 0))))) (or (<= (+ Tx x) 0) (or (and (>= x 0) (< (+ (+ Tx ( 2 ( T V))) y) (+ Ty x))) (or (< (+ Tx (* T V)) x) (< (+ (+ Tx x) y) Ty))))
(and (or (> x 0) (or (and (> v 0) (or (and (> timeToRed 0) (or (and (= B ( (^ timeToRed (- 1)) v)) (distinct ( B (^ timeToRed 2)) ( 2 (+ ( timeToRed v) x)))) (or (and (> B ( (^ timeToRed (- 1)) v)) (distinct (+ (^ v 2) ( ( 2 B) x)) 0)) (or (and (< B ( (^ timeToRed (- 1)) v)) (< ( B (^ timeToRed 2)) ( 2 (+ ( timeToRed v) x)))) (>= x 0))))) (and (< (+ (^ v 2) ( ( 2 B) x)) 0) (or (distinct B ( (^ timeToRed (- 1)) v)) (<= timeToRed 0))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( timeToRed v) x)) 0))))) (or (and (> timeToRed 0) (distinct v 0)) (distinct x 0))) (and (> B 0) (and (> T 0) (>= v 0))) (or (> x 0) (or (and (> v 0) (or (and (> timeToRed 0) (or (and (< B ( v (^ timeToRed (- 1)))) (< ( B (^ timeToRed 2)) ( 2 (+ ( v timeToRed) x)))) (and (distinct (+ (^ v 2) ( x ( B 2))) 0) (>= B ( v (^ timeToRed (- 1))))))) (and (< (+ (^ v 2) ( x ( B 2))) 0) (distinct B ( v (^ timeToRed (- 1))))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( v timeToRed) x)) 0)))))
(or (and (= v 0) (distinct x 0)) (and (> v 0) (or (and (< x 0) (or (and (< ( v (+ ( T v) x)) 0) (or (and (<= (+ ( 2 B) ( (^ v 2) (^ x (- 1)))) 0) (> timeToRed ( (^ (+ ( ( 2 B) T) ( (- 2) v)) (- 1)) (+ ( B (^ T 2)) ( 2 x))))) (> ( x (+ (^ v 2) ( ( 2 B) x))) 0))) (or (and (= (+ T ( (^ v (- 1)) x)) 0) (or (and (= ( B (^ T 2)) ( 2 (+ ( T v) x))) (> ( v (+ ( timeToRed v) x)) 0)) (or (and (< ( 2 (+ ( T v) x)) ( B (^ T 2))) (and (<= (+ ( 2 B) ( (^ v 2) (^ x (- 1)))) 0) (> timeToRed ( (^ (+ ( ( 2 B) T) ( (- 2) v)) (- 1)) (+ ( B (^ T 2)) ( 2 x)))))) (> ( x (+ (^ v 2) ( ( 2 B) x))) 0)))) (or (and (> ( v (+ ( T v) x)) 0) (and (< T ( ( (- 2) (^ v (- 1))) x)) (or (and (< ( B (^ T 2)) ( 2 (+ ( T v) x))) (> (+ ( B timeToRed) (^ (+ (^ v 2) ( ( 2 B) x)) (/ 1 2))) v)) (or (and (= ( B (^ T 2)) ( 2 (+ ( T v) x))) (> timeToRed T)) (or (and (< ( 2 (+ ( T v) x)) ( B (^ T 2))) (and (<= (+ ( 2 B) ( (^ v 2) (^ x (- 1)))) 0) (> timeToRed ( (^ (+ ( ( 2 B) T) ( (- 2) v)) (- 1)) (+ ( B (^ T 2)) ( 2 x)))))) (> ( x (+ (^ v 2) ( ( 2 B) x))) 0)))))) (or (and (= T ( ( (- 2) (^ v (- 1))) x)) (or (and (< ( B T) v) (> (+ ( B timeToRed) (^ (+ (^ v 2) ( ( 2 B) x)) (/ 1 2))) v)) (> ( B T) v))) (and (> T ( ( (- 2) (^ v (- 1))) x)) (or (and (< ( x (+ (^ v 2) ( ( 2 B) x))) 0) (> (+ ( B timeToRed) (^ (+ (^ v 2) ( ( 2 B) x)) (/ 1 2))) v)) (> ( x (+ (^ v 2) ( ( 2 B) x))) 0)))))))) (or (and (= x 0) (> timeToRed 0)) (> x 0))))) (and (or (> x 0) (or (and (> v 0) (or (and (> timeToRed 0) (or (and (< B ( v (^ timeToRed (- 1)))) (< ( B (^ timeToRed 2)) ( 2 (+ ( v timeToRed) x)))) (and (not (= (+ (^ v 2) ( x ( B 2))) 0)) (>= B ( v (^ timeToRed (- 1))))))) (and (< (+ (^ v 2) ( x ( B 2))) 0) (not (= B ( v (^ timeToRed (- 1)))))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( v timeToRed) x)) 0))))) (and (> B 0) (and (> T 0) (>= v 0)))) (or (and (< x 0) (or (and (> ( v (+ ( v T) x)) 0) (and (< T ( (^ v (- 1)) ( x (- 2)))) (or (and (> timeToRed ( (^ ( 2 (- ( T B) v)) (- 1)) (+ ( B (^ T 2)) ( x 2)))) (and (<= (+ ( 2 B) ( (^ v 2) (^ x (- 1)))) 0) (< ( (+ ( v T) x) 2) ( B (^ T 2))))) (or (> ( x (+ (^ v 2) ( x ( 2 B)))) 0) (or (and (< ( B (^ T 2)) ( (+ ( v T) x) 2)) (> (+ ( B timeToRed) (^ (+ (^ v 2) ( x ( 2 B))) (/ 1 2))) v)) (and (= ( B (^ T 2)) ( (+ ( v T) x) 2)) (> timeToRed T))))))) (or (or (and (< ( v (+ ( v T) x)) 0) (or (and (> timeToRed ( (^ ( 2 (- ( T B) v)) (- 1)) (+ ( B (^ T 2)) ( x 2)))) (<= (+ ( 2 B) ( (^ v 2) (^ x (- 1)))) 0)) (> ( x (+ (^ v 2) ( x ( 2 B)))) 0))) (and (>= T ( (^ v (- 1)) ( x (- 2)))) (or (> ( x (+ (^ v 2) ( x ( 2 B)))) 0) (and (> (+ ( B timeToRed) (^ (+ (^ v 2) ( x ( 2 B))) (/ 1 2))) v) (< ( x (+ (^ v 2) ( x ( 2 B)))) 0))))) (and (= 0 (+ T ( x (^ v (- 1))))) (or (> ( x (+ (^ v 2) ( x ( 2 B)))) 0) (or (and (> timeToRed ( (^ ( 2 (- ( T B) v)) (- 1)) (+ ( B (^ T 2)) ( x 2)))) (and (<= (+ ( 2 B) ( (^ v 2) (^ x (- 1)))) 0) (< ( (+ ( v T) x) 2) ( B (^ T 2))))) (and (= ( B (^ T 2)) ( (+ ( v T) x) 2)) (> ( v (+ ( v timeToRed) x)) 0)))))))) (or (= 0 x) (> x 0)))
(or (and (= v 0) (distinct x 0)) (and (> v 0) (or (and (< x 0) (or (> ( v (+ ( timeToRed v) x)) 0) (or (and (= (+ ( 3 timeToRed) ( ( 2 (^ v (- 1))) x)) 0) (or (and (< T timeToRed) (= B ( (^ timeToRed (- 1)) v))) (or (and (< (+ (^ v 3) ( ( ( 2 B) v) (+ ( T v) x))) 0) (distinct B ( (^ timeToRed (- 1)) v))) (and (< B ( ( 2 (^ timeToRed (- 2))) (+ ( timeToRed v) x))) (< (+ T ( (^ 2 (/ 1 2)) (^ ( (^ B (- 1)) (+ ( timeToRed v) x)) (/ 1 2)))) timeToRed))))) (or (and (< (+ (^ v 3) ( ( ( 2 B) v) (+ ( T v) x))) 0) (or (= (+ timeToRed ( (^ v (- 1)) x)) 0) (or (and (distinct (+ ( 2 B) ( (^ v 2) (^ (+ ( timeToRed v) x) (- 1)))) 0) (or (and (> ( v (+ ( ( 3 timeToRed) v) ( 2 x))) 0) (< ( v (+ ( timeToRed v) x)) 0)) (< ( v (+ ( ( 3 timeToRed) v) ( 2 x))) 0))) (<= timeToRed 0)))) (and (or (and (> timeToRed 0) (< ( v (+ ( ( 3 timeToRed) v) ( 2 x))) 0)) (and (< ( v (+ ( timeToRed v) x)) 0) (> ( v (+ ( ( 3 timeToRed) v) ( 2 x))) 0))) (or (and (< T timeToRed) (= (+ ( 2 B) ( (^ v 2) (^ (+ ( timeToRed v) x) (- 1)))) 0)) (and (< B ( ( 2 (^ timeToRed (- 2))) (+ ( timeToRed v) x))) (< (+ T ( (^ 2 (/ 1 2)) (^ ( (^ B (- 1)) (+ ( timeToRed v) x)) (/ 1 2)))) timeToRed)))))))) (or (and (= x 0) (> timeToRed 0)) (> x 0))))) (and (or (> x 0) (or (and (> v 0) (or (and (> timeToRed 0) (or (and (< B ( v (^ timeToRed (- 1)))) (< ( B (^ timeToRed 2)) ( 2 (+ ( v timeToRed) x)))) (and (not (= (+ (^ v 2) ( x ( B 2))) 0)) (>= B ( v (^ timeToRed (- 1))))))) (and (< (+ (^ v 2) ( x ( B 2))) 0) (not (= B ( v (^ timeToRed (- 1)))))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( v timeToRed) x)) 0))))) (and (> B 0) (and (> T 0) (>= v 0)))) (or (= v 0) (and (> v 0) (or (> x 0) (and (or (and (= 0 (+ ( 3 timeToRed) ( x ( 2 (^ v (- 1)))))) (or (and (< T timeToRed) (= ( B timeToRed) v)) (and (< (+ (^ v 3) ( 2 ( (+ ( v T) x) ( v B)))) 0) (distinct B ( v (^ timeToRed (- 1))))))) (or (> ( v (+ ( v timeToRed) x)) 0) (or (and (or (and (< ( v (+ ( v ( 3 timeToRed)) ( x 2))) 0) (> timeToRed 0)) (and (> ( v (+ ( v ( 3 timeToRed)) ( x 2))) 0) (< ( v (+ ( v timeToRed) x)) 0))) (and (< T timeToRed) (= 0 (+ ( 2 B) ( (^ v 2) (^ (+ ( v timeToRed) x) (- 1))))))) (and (< (+ (^ v 3) ( 2 ( (+ ( v T) x) ( v B)))) 0) (or (= 0 (+ timeToRed ( x (^ v (- 1))))) (and (distinct (+ ( 2 B) ( (^ v 2) (^ (+ ( v timeToRed) x) (- 1)))) 0) (or (< ( v (+ ( v ( 3 timeToRed)) ( x 2))) 0) (and (> ( v (+ ( v ( 3 timeToRed)) ( x 2))) 0) (< ( v (+ ( v timeToRed) x)) 0))))))))) (<= x 0)))))
(or (> x 0) (or (and (> v 0) (or (and (> timeToRed 0) (or (and (= B ( (^ timeToRed (- 1)) v)) (distinct ( B (^ timeToRed 2)) ( 2 (+ ( timeToRed v) x)))) (or (and (> B ( (^ timeToRed (- 1)) v)) (distinct (+ (^ v 2) ( ( 2 B) x)) 0)) (or (and (< B ( (^ timeToRed (- 1)) v)) (< ( B (^ timeToRed 2)) ( 2 (+ ( timeToRed v) x)))) (>= x 0))))) (and (< (+ (^ v 2) ( ( 2 B) x)) 0) (or (distinct B ( (^ timeToRed (- 1)) v)) (<= timeToRed 0))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( timeToRed v) x)) 0))))) (and (> B 0) (and (> T 0) (>= v 0))) (or (> x 0) (or (and (> v 0) (or (and (< (+ (^ v 2) ( x ( 2 B))) 0) (distinct B ( v (^ timeToRed (- 1))))) (and (> timeToRed 0) (or (and (< B ( v (^ timeToRed (- 1)))) (< ( B (^ timeToRed 2)) ( 2 (+ ( v timeToRed) x)))) (and (distinct (+ (^ v 2) ( x ( 2 B))) 0) (>= B ( v (^ timeToRed (- 1))))))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( v timeToRed) x)) 0)))))
(and (or (> x 0) (or (and (> v 0) (or (and (< (+ (^ v 2) ( ( 2 B) x)) 0) (distinct B ( (^ timeToRed (- 1)) v))) (and (or (distinct (+ (^ v 2) ( ( 2 B) x)) 0) (< B ( (^ timeToRed (- 1)) v))) (and (or (>= B ( (^ timeToRed (- 1)) v)) (< ( B (^ timeToRed 2)) ( 2 (+ ( timeToRed v) x)))) (> timeToRed 0))))) (and (< x 0) (or (<= v 0) (> ( v (+ ( timeToRed v) x)) 0))))) (or (and (> timeToRed 0) (distinct v 0)) (distinct x 0))) (and (> B 0) (and (> T 0) (>= v 0))) (or (> x 0) (or (and (> v 0) (or (and (< (+ (^ v 2) ( 2 ( x B))) 0) (distinct B ( v (^ timeToRed (- 1))))) (and (distinct (+ (^ v 2) ( 2 ( x B))) 0) (and (or (>= B ( v (^ timeToRed (- 1)))) (< ( B (^ timeToRed 2)) ( 2 (+ ( v timeToRed) x)))) (> timeToRed 0))))) (and (< x 0) (or (<= v 0) (> ( v (+ (* v timeToRed) x)) 0)))))
(and (or (and (>= g ( r (^ v 2))) (> m (^ ( g (^ r (- 1))) (/ 1 2)))) (and (> m (^ ( g (^ p (- 1))) (/ 1 2))) (<= ( p (^ v 2)) g))) (or (< x 0) (< v m))) (and (> T 0) (and (> p 0) (and (> g 0) (and (> r 0) (and (> m 0) (> v 0)))))) (or (and (>= g ( r (^ v 2))) (> m (^ ( g (^ r (- 1))) (/ 1 2)))) (and (> m (^ ( g (^ p (- 1))) (/ 1 2))) (<= ( (^ v 2) p) g)))
aditink commented 2 weeks ago
Some more examples: Formula Assumption Result
(or (and (= y 0) (and (or (< ( T v) R) (< x R)) (or (>= x R) (> (+ R x) 0)))) (or (and (= (+ R y) 0) (or (and (< ( T v) (+ R x)) (and (< y (+ R ( T v))) (and (< y (+ ( 2 R) x)) (<= x y)))) (and (> (+ R ( T v)) y) (and (< x R) (< y x))))) (or (and (or (and (>= x R) (< ( T v) (+ R y))) (and (> R x) (> (+ R x) 0))) (or (and (> y 0) (< y R)) (and (> (+ R y) 0) (< y 0)))) (and (< (+ R y) 0) (and (> R x) (> (+ R x) 0)))))) (and (or (and (<= x 0) (and (> (+ R x) 0) (< y R))) (or (and (> x 0) (and (< y R) (> R x))) (or (and (< y 0) (or (and (= R ( T v)) (and (> x 0) (or (and (= 0 (+ R y)) (< x R)) (> (+ R y) 0)))) (or (and (< ( T v) (+ R x)) (and (< x R) (or (and (= 0 (+ R y)) (not (= R ( T v)))) (< (+ R y) 0)))) (and (> (+ R x) ( T v)) (and (> (+ R y) 0) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))) (and (>= y 0) (and (> R y) (or (and (> x 0) (= R ( T v))) (and (> (+ R x) ( T v)) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))))) (and (> v 0) (and (> T 0) (> R 0)))) (or (and (= y 0) (or (< ( T v) R) (< x R))) (or (and (or (and (>= x R) (< ( T v) (+ R y))) (> R x)) (or (> y 0) (and (> (+ R y) 0) (< y 0)))) (<= (+ R y) 0)))
(or (and (<= (+ R y) 0) (or (and (= x 0) (< ( T v) R)) (and (< x (+ R ( T v))) (and (< ( T v) (+ R x)) (or (and (> x 0) (< x R)) (< x 0)))))) (and (> (+ R y) 0) (and (< y R) (or (and (= x 0) (< ( T v) R)) (or (and (< ( T v) (+ R x)) (or (and (> x 0) (< x R)) (< x 0))) (and (< ( T v) (* 2 R)) (>= x R))))))) (and (or (and (<= x 0) (and (> (+ R x) 0) (< y R))) (or (and (> x 0) (and (< y R) (> R x))) (or (and (< y 0) (or (and (= R ( T v)) (and (> x 0) (or (and (= 0 (+ R y)) (< x R)) (> (+ R y) 0)))) (or (and (< ( T v) (+ R x)) (and (< x R) (or (and (= 0 (+ R y)) (not (= R ( T v)))) (< (+ R y) 0)))) (and (> (+ R x) ( T v)) (and (> (+ R y) 0) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))) (and (>= y 0) (and (> R y) (or (and (> x 0) (= R ( T v))) (and (> (+ R x) ( T v)) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))))) (and (> v 0) (and (> T 0) (> R 0)))) (or (and (= 0 x) (< ( T v) R)) (or (and (< ( T v) (+ R x)) (or (and (> x 0) (< x R)) (< x 0))) (>= x R)))
(or (and (= y 0) (> R ( T v))) (or (> R x) (or (and (distinct y 0) (> (+ R y) ( T v))) (<= (+ R y) 0)))) (and (or (and (<= x 0) (and (> (+ R x) 0) (< y R))) (or (and (> x 0) (and (< y R) (> R x))) (or (and (< y 0) (or (and (= R ( T v)) (and (> x 0) (or (and (= 0 (+ R y)) (< x R)) (> (+ R y) 0)))) (or (and (< ( T v) (+ R x)) (and (< x R) (or (and (= 0 (+ R y)) (not (= R ( T v)))) (< (+ R y) 0)))) (and (> (+ R x) ( T v)) (and (> (+ R y) 0) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))) (and (>= y 0) (and (> R y) (or (and (> x 0) (= R ( T v))) (and (> (+ R x) ( T v)) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))))) (and (> v 0) (and (> T 0) (> R 0)))) (or (> R x) (or (and (= y 0) (> R ( T v))) (and (distinct y 0) (> (+ R y) ( T v)))))
(or (and (= x 0) (< ( T v) R)) (or (and (< ( T v) (+ R x)) (distinct x 0)) (>= x R))) (and (or (and (<= x 0) (and (> (+ R x) 0) (< y R))) (or (and (> x 0) (and (< y R) (> R x))) (or (and (< y 0) (or (and (= R ( T v)) (and (> x 0) (or (and (= 0 (+ R y)) (< x R)) (> (+ R y) 0)))) (or (and (< ( T v) (+ R x)) (and (< x R) (or (and (= 0 (+ R y)) (not (= R ( T v)))) (< (+ R y) 0)))) (and (> (+ R x) ( T v)) (and (> (+ R y) 0) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))) (and (>= y 0) (and (> R y) (or (and (> x 0) (= R ( T v))) (and (> (+ R x) ( T v)) (or (and (< R ( T v)) (< ( T v) ( R 2))) (< ( T v) R))))))))) (and (> v 0) (and (> T 0) (> R 0)))) (or (and (= x 0) (< ( T v) R)) (and (< ( T v) (+ R x)) (distinct x 0)))
(or (and (> (+ ( 3000 (+ (- 51) ( 50 gt))) produced) 0) (and (> (+ (+ ( 7000000 gt) ( 48 produced)) stored) 7344000) (or (and (> gt 1) (and (< ( 35 gt) 36) (<= produced 3000))) (and (>= ( 35 gt) 36) (< (+ ( 437500 gt) ( 3 produced)) 459000))))) (and (or (>= ( 35 gt) 36) (> produced 3000)) (and (or (< ( 35 gt) 36) (>= (+ ( 437500 gt) ( 3 produced)) 459000)) (> stored 0)))) (and (or (and (<= produced 3000) (or (and (> (+ ( 3000 (- ( 50 gt) 51)) produced) 0) (and (> (+ (+ ( gt 7000000) ( produced 48)) stored) 7344000) (< (+ ( gt 437500) ( produced 3)) 459000))) (and (> (+ ( gt 150000) produced) 3000) (> (+ ( produced 4) ( stored 3)) 612000)))) (and (> stored 0) (or (>= (+ ( gt 437500) (* produced 3)) 459000) (> produced 3000)))) (and (= T 1) (>= i 0))) (or (and (> (+ ( 3000 (- ( 50 gt) 51)) produced) 0) (or (and (> gt 1) (and (< ( gt 35) 36) (<= produced 3000))) (and (>= ( gt 35) 36) (< (+ ( gt 437500) ( produced 3)) 459000)))) (and (or (>= ( gt 35) 36) (> produced 3000)) (or (< ( gt 35) 36) (>= (+ ( gt 437500) ( produced 3)) 459000))))
(or (and (or (> gt 1) (<= produced 3000)) (and (or (<= gt 1) (<= (+ ( 3000 (+ (- 51) ( 50 gt))) produced) 0)) (and (> (+ ( 150000 gt) produced) 3000) (> (+ ( 4 produced) ( 3 stored)) 612000)))) (or (and (> gt 1) (or (and (> (+ ( 3000 (+ (- 51) ( 50 gt))) produced) 0) (and (> (+ (+ ( 7000000 gt) ( 48 produced)) stored) 7344000) (< (+ ( 437500 gt) ( 3 produced)) 446500))) (and (> stored 200000) (>= (+ ( 437500 gt) (* 3 produced)) 446500)))) (and (<= gt 1) (and (> produced 3000) (> stored 200000))))) (and (or (and (<= produced 3000) (or (and (> (+ ( 3000 (- ( 50 gt) 51)) produced) 0) (and (> (+ (+ ( gt 7000000) ( produced 48)) stored) 7344000) (< (+ ( gt 437500) ( produced 3)) 459000))) (and (> (+ ( gt 150000) produced) 3000) (> (+ ( produced 4) ( stored 3)) 612000)))) (and (> stored 0) (or (>= (+ ( gt 437500) (* produced 3)) 459000) (> produced 3000)))) (and (= T 1) (>= i 0))) (or (and (<= produced 3000) (<= (+ ( 3000 (- ( 50 gt) 51)) produced) 0)) (or (and (> gt 1) (or (and (> (+ ( 3000 (- ( 50 gt) 51)) produced) 0) (< (+ ( gt 437500) ( produced 3)) 446500)) (and (> stored 200000) (>= (+ ( gt 437500) ( produced 3)) 446500)))) (and (<= gt 1) (and (> stored 200000) (> produced 3000)))))
(or (and (> gt 1) (> (+ ( 3000 (+ (- 51) ( 50 gt))) produced) 0)) (or (and (>= ( 35 gt) 36) (>= (+ ( 437500 gt) ( 3 produced)) 459000)) (and (< ( 35 gt) 36) (> produced 3000)))) (and (or (and (<= produced 3000) (or (and (> (+ ( 3000 (- ( 50 gt) 51)) produced) 0) (and (> (+ (+ ( gt 7000000) ( produced 48)) stored) 7344000) (< (+ ( gt 437500) ( produced 3)) 459000))) (and (> (+ ( gt 150000) produced) 3000) (> (+ ( produced 4) ( stored 3)) 612000)))) (and (> stored 0) (or (>= (+ ( gt 437500) (* produced 3)) 459000) (> produced 3000)))) (and (= T 1) (>= i 0))) (or (and (> gt 1) (> (+ ( 3000 (- ( gt 50) 51)) produced) 0)) (and (< (* gt 35) 36) (> produced 3000)))
(or (and (> (+ (+ ( 4 produced) ( 3 stored)) ( ( 3 slope) t)) (+ 612000 ( ( ( 20 (+ (- 400) i)) i) t))) (and (<= produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ ( 150000 gt) produced) (+ 3000 ( ( ( 5 (+ (- 300) i)) (+ (- 100) i)) t))))) (and (> produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ stored ( slope t)) 0))) (and (= T 1) (and (>= i 0) (>= t 0))) (or (and (> (+ ( 150000 gt) produced) (+ 3000 ( t ( ( 5 (- i 300)) (- i 100))))) (and (> (+ (+ ( 4 produced) ( 3 stored)) ( 3 ( slope t))) (+ 612000 ( t ( 20 ( i (- i 400)))))) (<= produced (+ 3000 ( t ( i ( (- i 400) 5))))))) (and (> produced (+ 3000 ( t ( i ( (- i 400) 5))))) (> (+ stored ( slope t)) 0)))
(or (and (> (+ ( 150000 gt) produced) (+ 3000 ( ( ( 5 (+ (- 300) i)) (+ (- 100) i)) t))) (and (> (+ (+ ( 4 produced) ( 3 stored)) ( ( 3 slope) t)) (+ 612000 ( ( ( 20 (+ (- 400) i)) i) t))) (<= produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))))) (and (> produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ stored ( slope t)) 0))) (and (= T 1) (and (>= i 0) (>= t 0))) (or (and (> (+ (+ ( produced 4) ( 3 stored)) ( t ( 3 slope))) (+ 612000 ( t ( i ( 20 (- i 400)))))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( (- i 300) ( 5 ( (- i 100) t))))) (<= produced (+ 3000 ( 5 ( (- i 400) ( i t))))))) (and (> produced (+ 3000 ( 5 ( (- i 400) ( i t))))) (> (+ stored ( t slope)) 0)))
(or (and (> (+ ( 4 produced) ( 3 stored)) (+ 612000 ( ( 20 (+ (- 1050000) ( (+ (- 400) i) i))) t))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( ( ( 5 (+ (- 300) i)) (+ (- 100) i)) t))) (<= produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))))) (and (> produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ stored ( 7000000 t)) 0))) (and (= T 1) (and (>= i 0) (and (>= s 0) (and (<= s t) (<= t (+ s T)))))) (or (and (> (+ ( 4 produced) ( 3 stored)) (+ 612000 ( (- ( i (- i 400)) 1050000) ( 20 t)))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( t ( 5 ( (- i 300) (- i 100)))))) (<= produced (+ 3000 ( i ( (- i 400) ( t 5))))))) (and (> produced (+ 3000 ( i ( (- i 400) ( t 5))))) (> (+ stored ( t 7000000)) 0)))
(or (and (> (+ ( 4 produced) ( 3 stored)) (+ 612000 ( ( ( 20 (+ (- 100) i)) i) t))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( ( ( 5 (+ (- 300) i)) (+ (- 100) i)) t))) (<= produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))))) (and (> produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> stored ( (* 2000 i) t)))) (and (= T 1) (and (>= i 0) (and (>= s 0) (and (<= s t) (<= t (+ s T)))))) (or (and (> (+ ( 4 produced) ( 3 stored)) (+ 612000 ( i ( 20 ( (- i 100) t))))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( (- i 100) ( t ( 5 (- i 300)))))) (<= produced (+ 3000 ( i ( t ( 5 (- i 400)))))))) (and (> produced (+ 3000 ( i ( t ( 5 (- i 400)))))) (> stored ( i (* t 2000)))))
(or (and (> (+ ( 4 produced) ( 3 stored)) 612000) (and (> (+ ( 150000 gt) produced) 3000) (<= produced ( (- 3000) (+ (- 1) ( 50 t)))))) (and (> produced ( (- 3000) (+ (- 1) ( 50 t)))) (> stored ( 200000 t)))) (and (= T 1) (and (>= i 0) (and (>= s 0) (and (<= s t) (<= t (+ s T)))))) (or (and (<= produced ( (- 3000) (- ( 50 t) 1))) (and (> (+ ( 4 produced) ( 3 stored)) 612000) (> (+ ( 150000 gt) produced) 3000))) (and (> produced ( (- 3000) (- ( 50 t) 1))) (> stored ( t 200000))))
(or (and (> (+ (+ ( 4 produced) ( 3 stored)) ( ( 3 slope) t)) (+ 612000 ( ( ( 20 (+ (- 400) i)) i) t))) (and (<= produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ ( 150000 gt) produced) (+ 3000 ( ( ( 5 (+ (- 300) i)) (+ (- 100) i)) t))))) (and (> produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ stored ( slope t)) 0))) (and (<= t 1) (and (= 1 T) (and (>= i 0) (>= t 0)))) (or (and (> (+ ( 150000 gt) produced) (+ 3000 ( t ( ( 5 (- i 300)) (- i 100))))) (and (> (+ (+ ( 4 produced) ( 3 stored)) ( 3 ( slope t))) (+ 612000 ( t ( 20 ( i (- i 400)))))) (<= produced (+ 3000 ( t ( i ( (- i 400) 5))))))) (and (> produced (+ 3000 ( t ( i ( (- i 400) 5))))) (> (+ stored ( slope t)) 0)))
(or (and (> (+ ( 4 produced) ( 3 stored)) (+ 612000 ( ( 20 (+ (- 1050000) ( (+ (- 400) i) i))) t))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( ( ( 5 (+ (- 300) i)) (+ (- 100) i)) t))) (<= produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))))) (and (> produced (+ 3000 ( ( ( 5 (+ (- 400) i)) i) t))) (> (+ stored ( 7000000 t)) 0))) (and (= T 1) (and (>= i 0) (and (>= t 0) (<= t 1)))) (or (and (> (+ ( 4 produced) ( 3 stored)) (+ 612000 ( (- ( i (- i 400)) 1050000) ( 20 t)))) (and (> (+ ( 150000 gt) produced) (+ 3000 ( t ( 5 ( (- i 300) (- i 100)))))) (<= produced (+ 3000 ( i ( (- i 400) ( t 5))))))) (and (> produced (+ 3000 ( i ( (- i 400) ( t 5))))) (> (+ stored ( t 7000000)) 0)))
(and (> stored 200000) (or (> produced 3000) (and (> (+ ( 150000 gt) produced) 3000) (> (+ ( 4 produced) (* 3 stored)) 612000)))) (and (or (and (> (+ ( produced 4) ( 3 stored)) 612000) (and (<= produced 3000) (> (+ (* 150000 gt) produced) 3000))) (and (> produced 3000) (> stored 0))) (and (= T 1) (>= i 0))) (> stored 200000)