Importing snapshot 2015-06-01

FFT/905819/z3.630166.smt2

+(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 sat)
+(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)
+(assert (not (= f1 f2)))
+(assert (not (not (= (f3 f4) 0.0))))
+(assert (< f5 f4))
+(assert (< f4 (* 2.0 f5)))
+(assert (not (= (f3 (- f4 f5)) 0.0)))
+(check-sat)
+(exit)

FFT/905820/z3.631632.smt2

+(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)

FFT/905821/z3.641736.smt2

+(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-sort S2 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (Real) Real)
+(declare-fun f4 () Real)
+(declare-fun f5 (S2) Real)
+(declare-fun f6 () S2)
+(assert (not (= f1 f2)))
+(assert (let ((?v_1 0.0) (?v_0 (f3 (/ (* 2.0 f4) (f5 f6))))) (not (=> (= ?v_0 ?v_1) (=> (= (ite (< ?v_0 ?v_1) (- ?v_0) ?v_0) 1.0) false)))))
+(check-sat)
+(exit)

FFT/905822/z3.631714.smt2

+(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)

FFT/905823/smtlib.631277.smt2

+(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)

FFT/905824/z3.631550.smt2

+(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)

FFT/905825/smtlib.630785.smt2

+(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)

FFT/905826/z3.631878.smt2

+(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)

FFT/905827/smtlib.631113.smt2

+(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)

FFT/905828/smtlib.631031.smt2

+(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)

FFT/905829/smtlib.631195.smt2

+(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)

FFT/905830/z3.631960.smt2

+(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)

FFT/905831/smtlib.630867.smt2

+(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)

FFT/905832/smtlib.630949.smt2

+(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)

FFT/905833/smtlib.640350.smt2

+(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-sort S2 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (Real) Real)
+(declare-fun f4 (Real Real) Real)
+(declare-fun f5 () Real)
+(declare-fun f6 (S2) Real)
+(declare-fun f7 () S2)
+(assert (not (= f1 f2)))
+(assert (let ((?v_1 0.0) (?v_0 (f3 (f4 (* 2.0 f5) (f6 f7))))) (not (=> (= ?v_0 ?v_1) (=> (= (ite (< ?v_0 ?v_1) (- ?v_0) ?v_0) 1.0) false)))))
+(check-sat)
+(exit)

FFT/905834/z3.631468.smt2

+(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)

FFT/905835/z3.631796.smt2

+(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)

FFT/starexec_description.txt

+no description
\ No newline at end of file