Squashed commit of the following:

commit ca6ae86e
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon Jun 5 18:00:17 2017 +0200

    Fixing README.md

commit 2d6488b2
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon Jun 5 16:55:16 2017 +0200

    Fixing README.md

commit 0276d43d
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Thu Jun 1 13:05:16 2017 -0700

    Updating statuses based on solutions from two or more solvers running with a long timeout

commit 226bee72
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Tue May 23 13:29:24 2017 +0200

    2.0 to 2.6, CRLF to LF

commit e64c523d
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Wed May 3 18:23:25 2017 +0200

    Fixing README.md

commit 81b36be6
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Thu Apr 20 10:11:18 2017 +0200

    Fixing README.md

commit 3705819d
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Wed Mar 29 13:47:10 2017 +0200

    Fixing README.md

commit f527fc90
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Tue Mar 28 16:35:58 2017 +0200

    Fixing README.md

commit 200afcd9
Author: Tjark Weber <tjark.weber@gmx.de>
Date:   Thu Mar 16 10:32:03 2017 +0100

    Remove duplicate benchmarks

FFT/smtlib.630785.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.630867.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.630949.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.631031.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.631113.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.631195.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.631277.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/smtlib.640350.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/z3.630166.smt2

+(set-info :smt-lib-version 2.6)
 (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)

FFT/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/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/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/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/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/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/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/z3.641736.smt2

+(set-info :smt-lib-version 2.6)
 (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)

cas/10u05.04.smt2

+(set-info :smt-lib-version 2.6)
 (set-logic QF_UFNRA)
 (set-info :source |
     Simple airplane collision avoidance system model
     Submitted by Tim King (taking@cs.nyu.edu) and Clark Barrett (barrett@cs.nyu.edu)
   |)
-(set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
 (set-info :status sat)
 (set-info :difficulty | unknown |)

cas/20revert.u.smt2

+(set-info :smt-lib-version 2.6)
 (set-logic QF_UFNRA)
 (set-info :source |
     Simple airplane collision avoidance system model
     Submitted by Tim King (taking@cs.nyu.edu) and Clark Barrett (barrett@cs.nyu.edu)
   |)
-(set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
 (set-info :status sat)
 (set-info :difficulty | unknown |)

cas/20u10.09.smt2

+(set-info :smt-lib-version 2.6)
 (set-logic QF_UFNRA)
 (set-info :source |
     Simple airplane collision avoidance system model
     Submitted by Tim King (taking@cs.nyu.edu) and Clark Barrett (barrett@cs.nyu.edu)
   |)
-(set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
 (set-info :status sat)
 (set-info :difficulty | unknown |)