Commit 200afcd9 authored by Tjark Weber's avatar Tjark Weber
Browse files

Remove duplicate benchmarks

parent 3060dedb
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (or (not (= (f3 f4) 0.0)) (not (= (f5 f4) 1.0)))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(check-sat)
(exit)
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (or (not (= (f3 f4) 0.0)) (not (= (f5 f4) 1.0)))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(assert (< f4 (* 2.0 f6)))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(check-sat)
(exit)
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (or (not (= (f3 f4) 0.0)) (not (= (f5 f4) 1.0)))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(check-sat)
(exit)
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (or (not (= (f3 f4) 0.0)) (not (= (f5 f4) 1.0)))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(check-sat)
(exit)
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (or (not (= (f3 f4) 0.0)) (not (= (f5 f4) 1.0)))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(check-sat)
(exit)
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (or (not (= (f3 f4) 0.0)) (not (= (f5 f4) 1.0)))))
(assert (let ((?v_0 0.0)) (=> (< ?v_0 f4) (=> (< f4 f6) (not (= (f3 f4) ?v_0))))))
(assert (=> (= f4 f6) (not (= (f5 f4) 1.0))))
(assert (=> (< f6 f4) (=> (< f4 (* 2.0 f6)) (not (= (f3 f4) 0.0)))))
(assert (< 0.0 f4))
(assert (< f4 (* 2.0 f6)))
(check-sat)
(exit)
(set-logic QF_UFNRA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 () Real)
(declare-fun f4 () Real)
(declare-fun f5 (Real) Real)
(declare-fun f6 (Real) Real)
(assert (not (= f1 f2)))
(assert (let ((?v_0 0.0)) (let ((?v_2 (< ?v_0 f3)) (?v_1 (not (= (f5 f3) ?v_0))) (?v_4 (not (= (f6 f3) 1.0))) (?v_3 (< f3 (* 2.0 f4)))) (not (=> (=> ?v_2 (=> (< f3 f4) ?v_1)) (=> (=> (= f3 f4) ?v_4) (=> (=> (< f4 f3) (=> ?v_3 ?v_1)) (=> ?v_2 (=> ?v_3 (or ?v_1 ?v_4))))))))))
(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