Commit 2619a202 authored by Tjark Weber's avatar Tjark Weber
Browse files

Remove duplicate benchmarks

parent c9e0c4f9
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (= (f3 f4 (- f5 f6)) (- (f3 f4 f5)))))
(assert (forall ((?v0 Real)) (= (f3 f4 (+ f6 ?v0)) (- (f3 f4 ?v0)))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (forall ((?v0 Real)) (= (f3 f4 (+ f5 ?v0)) (- (f3 f4 ?v0)))))
(assert (not (= (f3 f4 (- f6 f5)) (- (f3 f4 f6)))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) 0.0))))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) 0.0))))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (< f5 f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) 0.0))))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 () Real)
(declare-fun f4 (S2 Real) Real)
(declare-fun f5 () S2)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f3) (< ?v_0 (f4 f5 ?v0)))))))
(assert (let ((?v_0 0.0)) (not (=> (< ?v_0 f6) (=> (< f6 f3) (not (= (f4 f5 f6) ?v_0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 (- f5 f6)) 0.0))))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 (- f5 f6)) 0.0))))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (< (- f5 f6) f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 (- f5 f6)) 0.0))))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 () Real)
(declare-fun f4 (S2 Real) Real)
(declare-fun f5 () S2)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f3) (< ?v_0 (f4 f5 ?v0)))))))
(assert (let ((?v_1 0.0) (?v_0 (- f6 f3))) (not (=> (< ?v_1 ?v_0) (=> (< ?v_0 f3) (not (= (f4 f5 ?v_0) ?v_1)))))))
(check-sat)
(exit)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment