(list

(benchmark true
  :status sat
  :formula (true))

;damn special case, cannot proof-check it
;(benchmark false
;  :status unsat
;  :formula (false))

(benchmark congr1
  :status unsat
  :formula  (and 
  (= (f x) (f y)) 
  (= (f y) (f x)) 
  (not (= (f (f x)) (f (f y))) )
))

(benchmark congr2
  :status unsat
  :formula  (and 
  (= x x1) 
  (= y y1) 
  (not (= (f (f x y)) (f (f x1 y1))) )
))

(benchmark bool1
  :status sat
  :formula  (and 
  (or (not x) (not y) z) 
  (or y z)
  (or (not z) (not x)) 
  (or z y x)))

(benchmark php
  :status unsat
  :formula  (and 
  (and p1 p2 p3 p4 p5)
  (implies (and p1 p2 p3 p4) (not p5))
  (implies (and p1 p2 p3 p5) (not p4))
  (implies (and p1 p2 p4 p5) (not p3))
  (implies (and p1 p3 p4 p5) (not p2))
  (implies (and p2 p3 p4 p5) (not p1))))
  
(benchmark congr3
  :status unsat
  :formula  (and
  (= (f a b) a)
  (= (f (f a b) b) c)
  (not (= (g a) (g c)))))
  
(benchmark bool2
  :status sat
  :formula  (and
  (or (not x) (not y)) 
  (or (not y) x)))

(benchmark congr_ax
  :status unsat
  :formula  (not
  (implies (= x y) (= (f x) (f y)))))

(benchmark plus1
  :status unsat
  :formula  (not
  (implies (= x y) (= (+ 1 x) (+ 1 y)))))

(benchmark plus2
  :status unsat
  :formula  (not
  (implies (= (+ 1 x) (+ 1 y)) (= x y))))

(benchmark congr12
  :status sat
  :formula  (not
  (implies (= (f x) (f y)) (= x y))))

(benchmark plus_neg
  :status unsat
  :formula 
  (= (+ 1 x) x))

(benchmark plus-neg2
  :status unsat
  :formula 
  (= (+ 1 (+ 1 x)) x))

(benchmark plus_neg3
  :status unsat
  :formula 
  (= (+ 1 (+ 1 (+ 1 x))) x))

(benchmark ibot
  :status unsat
  :formula 
  (and
    (= ibot (f c3))
    (not (= ibot c1))
    (= ibot xyz54)
    (= c1 (f c2))
    (= c2 c3)))

(benchmark something
  :status unsat
  :formula 
  (and
    (f.1 x)
    (not (f.1 y))
    (= x y)))
    
(benchmark bug1
  :status unsat
  :formula  (and
  (= xx121 (+ 1 (+ 1 xx99)))
  (= xx151 (+ (+ 1 1) (+ (+ 1 1) xx121)))
  (= (+ 1 (+ 1 (+ 1 q2.h0))) (+ (+ 1 1) xx151))
  (not (= (q1.c0 xx1) xx265))
  (= (+ 1 q1.h0) xx15)
  (not (= (+ 1 (+ 1 (+ 1 (+ 1 q1.h0)))) (+ 1 (+ 1 (+ 1 xx15)))))
  (not (= xx265 (q2.c0 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 q2.h0)))))))))
  (not (= (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 q2.h0)))))) xx121))
  (not (= xx1 (+ 1 xx15)))
  (not (= (+ 1 q2.h0) xx99))))

(benchmark number-literals
  :status unsat
  :formula
    (or
      (< 3 2)
      (<= 3 2)
      (>= 2 3)
      (> 2 3)
      (> -2 3)
      (= 2 3)
    ))
    
(benchmark utvpi-1
  :status unsat
  :formula
  (not (implies (<= x (- y 1)) (< x (+ y 0)))))

(benchmark utvpi-2
  :status unsat
  :formula
	(and
	(< (- a 1) (- b 1))
	(<= x (- a 1))
	(>= x b)
	))
	
(benchmark utvpi-3
  :status unsat
  :formula
	(and
	(<= y 9)
	(= x 10)
	(>= y x)
	))
	
(benchmark utvpi-4
  :status unsat
  :formula
	(and
	(<= x 9)
	(= a 10)
	(>= x (+ a 0))
	))

(benchmark utvpi-5
  :status unsat
  :formula
	(and
	(= Max 1000)
	(<= N Max)
	(not (<= N 1000))
	))
	
(benchmark utvpi-6
  :status sat
  :formula
	(and
	(> (s self2) 0)
	(<= (t (- (s self))) 0)
	(=  (t (- (s self))) (- (s self) 1))
	(=  (dummy1 qux) dummy2)
	(=  (dummy3 (- (s self))) dummy4)
	(= self self2)
	))
	
(benchmark utvpi-7
  :status sat
  :formula
	(and
	(= self x4)
	(= (s (t c1 self (- (s c1 self) 1)) self) true) ; dummy
	(= (s (t c2 self (+ (s c2 self) 1)) x5) true) ; dummy
	(=  (s (t c1 self (- (s c1 self) 1)) self) (- (s c1 self) 1))
	(<= (s (t c1 self (- (s c1 self) 1)) x4) 0)
	(> (s c1 x4) 0)
	))

(benchmark utvpi-8
  :status sat
  :formula
	(and
	(m.i (+ (- n 1) 1) dum)
	(not (< 0 n))
	(>= n 0)
	(m.i (- n 1) dum)
	(= foo bar)
	))

(benchmark utvpi-ugly-bug
  :status sat
  :formula
	(and
	(> a (- b 2))
	(!= a b)
	(> b (- a 1))
	))

(benchmark tc-1
  :status unsat
  :formula
	(and
	(not (= o c))
	(<: o c)
	(<: c o)
	))

(benchmark tc-2
  :status unsat
  :formula
	(and
	(= ta ap)
	(= ap ts)
	(not (<: ts ta))
	))


(benchmark tc-3
  :status unsat
  :formula
	(and
	  (or
	     (!= v1 v2)
	     (!= v2 v3)
	     (!= v3 v4)
	     (!= v4 v5)
	  )

	  (<: v1 v2)
	  (<: v2 v3)
	  (<: v3 v4)
	  (<: v4 v5)
	  (<: v5 v1)
	))


(benchmark tc-4
  :status unsat
  :formula
	(not
	  (implies
	    (and
	      (<: a1 b) (<: a2 b)
	      (<: b c)
	      (<: c d1) (<: c d2))
	    (and
	      (<: a1 d1) (<: a1 d2)
	      (<: a2 d1) (<: a2 d2)
	      (<: a1 c) (<: a2 c)
	      (<: b d1) (<: b d2)))))

(benchmark tc-5
  :status unsat
  :formula
	(not
	  (implies
	    (and
	      (<: a1 b) (<: a2 b)
	      (= b c)
	      (<: c d1) (<: c d2))
	    (and
	      (<: a1 d1) (<: a1 d2)
	      (<: a2 d1) (<: a2 d2)
	      (<: a1 c) (<: a2 c)
	      (<: b d1) (<: b d2)))))

(benchmark tc-6
  :status unsat
  :formula
    (and
      (or
        (!= v1 v2) (!= v1 v3) (!= v1 v4) (!= v1 v5) (!= v1 v6) (!= v1
        v7) (!= v1 v8) (!= v1 v9) (!= v1 v10) (!= v1 v11) (!= v1 v12)
        (!= v1 v13) (!= v1 v14) (!= v1 v15) (!= v1 v16) (!= v1 v17)
        (!= v1 v18) (!= v1 v19) (!= v1 v20) (!= v2 v3) (!= v2 v4) (!=
        v2 v5) (!= v2 v6) (!= v2 v7) (!= v2 v8) (!= v2 v9) (!= v2 v10)
        (!= v2 v11) (!= v2 v12) (!= v2 v13) (!= v2 v14) (!= v2 v15)
        (!= v2 v16) (!= v2 v17) (!= v2 v18) (!= v2 v19) (!= v2 v20) (!=
        v3 v4) (!= v3 v5) (!= v3 v6) (!= v3 v7) (!= v3 v8) (!= v3 v9)
        (!= v3 v10) (!= v3 v11) (!= v3 v12) (!= v3 v13) (!= v3 v14)
        (!= v3 v15) (!= v3 v16) (!= v3 v17) (!= v3 v18) (!= v3 v19) (!=
        v3 v20) (!= v4 v5) (!= v4 v6) (!= v4 v7) (!= v4 v8) (!= v4 v9)
        (!= v4 v10) (!= v4 v11) (!= v4 v12) (!= v4 v13) (!= v4 v14)
        (!= v4 v15) (!= v4 v16) (!= v4 v17) (!= v4 v18) (!= v4 v19) (!=
        v4 v20) (!= v5 v6) (!= v5 v7) (!= v5 v8) (!= v5 v9) (!= v5 v10)
        (!= v5 v11) (!= v5 v12) (!= v5 v13) (!= v5 v14) (!= v5 v15)
        (!= v5 v16) (!= v5 v17) (!= v5 v18) (!= v5 v19) (!= v5 v20)
        (!= v6 v7) (!= v6 v8) (!= v6 v9) (!= v6 v10) (!= v6 v11) (!=
        v6 v12) (!= v6 v13) (!= v6 v14) (!= v6 v15) (!= v6 v16) (!= v6
        v17) (!= v6 v18) (!= v6 v19) (!= v6 v20) (!= v7 v8) (!= v7 v9)
        (!= v7 v10) (!= v7 v11) (!= v7 v12) (!= v7 v13) (!= v7 v14)
        (!= v7 v15) (!= v7 v16) (!= v7 v17) (!= v7 v18) (!= v7 v19)
        (!= v7 v20) (!= v8 v9) (!= v8 v10) (!= v8 v11) (!= v8 v12)
        (!= v8 v13) (!= v8 v14) (!= v8 v15) (!= v8 v16) (!= v8 v17)
        (!= v8 v18) (!= v8 v19) (!= v8 v20) (!= v9 v10) (!= v9 v11)
        (!= v9 v12) (!= v9 v13) (!= v9 v14) (!= v9 v15) (!= v9 v16)
        (!= v9 v17) (!= v9 v18) (!= v9 v19) (!= v9 v20) (!= v10 v11)
        (!= v10 v12) (!= v10 v13) (!= v10 v14) (!= v10 v15) (!= v10 v16)
        (!= v10 v17) (!= v10 v18) (!= v10 v19) (!= v10 v20) (!= v11 v12)
        (!= v11 v13) (!= v11 v14) (!= v11 v15) (!= v11 v16) (!= v11 v17)
        (!= v11 v18) (!= v11 v19) (!= v11 v20) (!= v12 v13) (!= v12 v14)
        (!= v12 v15) (!= v12 v16) (!= v12 v17) (!= v12 v18) (!= v12 v19)
        (!= v12 v20) (!= v13 v14) (!= v13 v15) (!= v13 v16) (!= v13 v17)
        (!= v13 v18) (!= v13 v19) (!= v13 v20) (!= v14 v15) (!= v14 v16)
        (!= v14 v17) (!= v14 v18) (!= v14 v19) (!= v14 v20) (!= v15 v16)
        (!= v15 v17) (!= v15 v18) (!= v15 v19) (!= v15 v20) (!= v16 v17)
        (!= v16 v18) (!= v16 v19) (!= v16 v20) (!= v17 v18) (!= v17 v19)
        (!= v17 v20) (!= v18 v19) (!= v18 v20) (!= v19 v20))
     (<: v1 v2) (<: v2 v3) (<: v3 v4) (<: v4 v5) (<: v5 v6) (<: v6 v7)
     (<: v7 v8) (<: v8 v9) (<: v9 v10) (<: v10 v11) (<: v11 v12) (<:
     v12 v13) (<: v13 v14) (<: v14 v15) (<: v15 v16) (<: v16 v17) (<:
     v17 v18) (<: v18 v19) (<: v19 v20) (<: v20 v1)))

; Q-tests start here
(benchmark q1
  :status unsat
  :formula
    (and
      (forall (x y) (= (car (cons x y)) x))
      (not (implies (= (cons a b) (cons c d)) (= a c)))))


(benchmark q2
  :status unsat
  :formula
    (not
	(implies
	(forall (m i x dum)
	  (PATS (select (store m i x) i dum))
	  (= (select (store m i x) i dum) x))
	(implies
	 (forall (r) (= (select b r 0) (+ (select a r 0) 1)))
	 (implies
	  (forall (r) (= (select c r 0)
			  (+ (select (store a r (+ (select a r 0) 1)) r 0) 1)))
	  (= (select c r 0) (+ (select b r 0) 1)))))))
	  
(benchmark trans-mult
  :status unsat
  :formula
	(not
	  (implies
	    (and
	      (forall (x y z) (implies (and (r.1 x y) (r.1 y z)) (r.1 x z)))
	      (forall (x y z) (implies (and (r.2 x y) (r.2 y z)) (r.2 x z)))
	      (forall (x y) (iff (r.3 x y) (and (r.1 x y) (r.2 x y)))))
	    (forall (x y z) (implies (and (r.3 x y) (r.3 y z)) (r.3 x z))))))
	    
(benchmark exam-1
  :status sat
  :formula
	(not
	(implies (exists (x) (a. x)) (implies
	  (exists (x) (implies (a. x) (b. x)))
	    (exists (x) (b. x))))))
    
(benchmark exam-2
  :status unsat
  :formula
	(not
	(implies (forall (x) (a. x)) (implies
	  (exists (x) (implies (a. x) (b. x)))
	    (exists (x) (b. x))))))

	
) ; test