added CASC-related files, to keep a public record of the Isabelle submission at the competition

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC/ReadMe	Tue May 21 11:01:14 2013 +0200
@@ -0,0 +1,168 @@
+Isabelle/HOL 2013 at CASC-24
+
+Notes to Geoff:
+
+  Once you have open the archive, Isabelle and its tool are ready to go. The
+  various tools are invoked as follows:
+
+  	Isabelle, competition version:
+  		./bin/isabelle tptp_isabelle %d %s
+
+  	Isabelle, demo version:
+  		./bin/isabelle tptp_isabelle_hot %d %s
+
+  	Nitpick and Nitrox:
+  		./bin/isabelle tptp_nitpick %d %s
+
+  	Refute:
+  		./bin/isabelle tptp_refute %d %s
+
+  Here's an example:
+
+    ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SET/SET014^4.p
+
+  The output should look as follows:
+
+    > val it = (): unit
+    val commit = fn: unit -> bool
+    Loading theory "Scratch_tptp_isabelle_hot_29414_2568"
+    running nitpick for 7 s
+    FAILURE: nitpick
+    running simp for 15 s
+    SUCCESS: simp
+    % SZS status Theorem
+
+  Additional sanity tests:
+
+  	./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/CSR/CSR150^3.p
+  	./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SYO/SYO304^5.p
+    ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/PUZ/PUZ087^1.p
+
+  The first problem is unprovable; the second one is proved by Satallax; the
+  third one is proved by LEO-II.
+
+  All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS statuses
+  of the form
+
+  	% SZS status XXX
+
+  where XXX is in the set
+
+    {Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable}
+
+  Nitpick and Nitrox also output a model within "% SZS begin" and "% SZS end"
+  tags.
+
+  In 2011, there were some problems with Java (needed for Nitpick), because it
+  required so much memory at startup. I doubt there will be any problems this
+  year, because Isabelle now includes its own version of Java, but the solution
+  back then was to replace
+
+  	exec "$ISABELLE_TOOL" java
+
+  in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with
+
+  	/usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java
+
+  See the emails we exchanged on July 18, 2011, with the subject "No problem on
+  my Linux 64-bit".
+
+  Enjoy!
+
+
+Notes to myself:
+
+  I downloaded the official Isabelle2013 Linux package from
+
+    http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013_linux.tar.gz
+
+  on a "macbroy" machine and renamed the directory "Isabelle2013-CASC". I built
+  a "HOL-TPTP" image:
+
+    ./bin/isabelle build -b HOL-TPTP
+
+  I copied the heaps over to "./heaps":
+
+    mv ~/.isabelle/Isabelle2013/heaps .
+
+  To use this image and suppress some scary output, I added
+
+    HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val it = (): unit"
+
+  to the next-to-last lines of "src/HOL/TPTP/lib/Tools/tptp_[inrs]*".
+
+  At this point I tested the "SYN044^4" mentioned above.
+
+  I renamed "README" to "README.orig" and copied this "ReadMe" over.
+
+  Next, I installed and enabled ATPs.
+
+  LEO-II (1.4.3):
+
+    I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved LEO-II from
+
+      http://www.ags.uni-sb.de/~leo/leo2_v1.4.3.tgz
+
+    I did "make opt". I copied
+    "bin/leo.opt" to "~/Isabelle2013-CASC/contrib/leo".
+
+    I added this line to "etc/settings":
+
+      LEO2_HOME=$ISABELLE_HOME/contrib
+
+  Satallax (2.7):
+
+    I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved Satallax from
+
+      http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz
+
+    I added E to the path so that it gets detected by Satallax's configure
+    script:
+
+      export PATH=$PATH:~/Isabelle2013-CASC/contrib/e-1.6-2/x86-linux
+
+    I followed the instructions in "satallax-2.7/INSTALL". I copied
+    "bin/satallax.opt" to "~/Isabelle2013-CASC/contrib/satallax".
+
+    I added this line to "etc/settings":
+
+      SATALLAX_HOME=$ISABELLE_HOME/contrib
+
+  Vampire (2.6):
+
+    I copied the file "vampire_rel.linux64" from the 2012 CASC archive to
+    "~/Isabelle2013-CASC/contrib/vampire".
+
+    I added these lines to "etc/settings":
+
+      VAMPIRE_HOME=$ISABELLE_HOME/contrib
+      VAMPIRE_VERSION=2.6
+
+  Z3 (3.2):
+
+    I uncommented the following line in "contrib/z3-3.2/etc/settings":
+
+      # Z3_NON_COMMERCIAL="yes"
+
+  To test that the examples actually worked, I did
+
+    ./bin/isabelle tty
+    theory T imports Main begin;
+    lemma "a = b ==> [b] = [a]";
+    sledgehammer [e leo2 satallax spass vampire z3 z3_tptp] ();
+
+  and I performed the aforementioned sanity tests.
+
+  Ideas for next year:
+
+    * Unfold definitions, esp. if it makes the problem more first-order (cf.
+      "SEU466^1").
+    * Detect and remove needless definitions.
+    * Expand "p b" to "(b & p True) | (~ b & p False)" (cf. "CSR148^3").
+    * Select subset of axioms (cf. "CSR148^3").
+
+  That's it.
+
+
+                Jasmin Blanchette
+                21 May 2013

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC/SysDesc_Isabelle.html	Tue May 21 11:01:14 2013 +0200
@@ -0,0 +1,183 @@
+<HR><!------------------------------------------------------------------------>
+<H2>Isabelle/HOL 2013</H2>
+Jasmin C. Blanchette<sup>1</sup>, Lawrence C. Paulson<sup>2</sup>,
+Tobias Nipkow<sup>1</sup>, Makarius Wenzel<sup>3</sup> <BR>
+<sup>1</sup>Technische Universit&auml;t M&uuml;nchen, Germany <BR>
+<sup>2</sup>University of Cambridge, United Kingdom <BR>
+<sup>3</sup>Universit&eacute; Paris Sud, France <BR>
+
+<H3>Architecture</H3>
+
+Isabelle/HOL 2013 [<A HREF="#References">NPW13</A>] is the higher-order 
+logic incarnation of the generic proof assistant 
+<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2013</A>.
+Isabelle/HOL provides several automatic proof tactics, notably an equational
+reasoner [<A HREF="#References">Nip89</A>], a classical reasoner [<A
+HREF="#References">Pau94</A>], and a tableau prover [<A
+HREF="#References">Pau99</A>]. It also integrates external first- and
+higher-order provers via its subsystem Sledgehammer [<A
+HREF="#References">PB10</A>, <A HREF="#References">BBP11</A>].
+
+<P>
+Isabelle includes a parser for the TPTP syntaxes CNF, FOF, TFF0, and THF0, due
+to Nik Sultana. It also includes TPTP versions of its popular tools, invokable
+on the command line as <tt>isabelle tptp_<em>tool</em> <em>max_secs</em>
+<em>file.p</em></tt>. For example:
+
+<blockquote><pre>
+isabelle tptp_isabelle_hot 100 SEU/SEU824^3.p
+</pre></blockquote>
+
+<P>
+Two versions of Isabelle participate this year. The <em>demo</em> (or HOT) version
+includes its competitors LEO-II [<A HREF="#References">BPTF08</A>] and Satallax
+[<A HREF="#References">Bro12</A>] as Sledgehammer backends, whereas the
+<em>competition</em> version leaves them out.
+
+<H3>Strategies</H3>
+
+The <em>Isabelle</em> tactic submitted to the competition simply tries the
+following tactics sequentially:
+
+<DL>
+<DT> <tt>sledgehammer</tt>
+<DD> Invokes the following sequence of provers as oracles via Sledgehammer:
+	<UL>
+	<LI> <tt>satallax</tt>&mdash;Satallax 2.4 [<A HREF="#References">Bro12</A>] (<em>demo only</em>);
+	<LI> <tt>leo2</tt>&mdash;LEO-II 1.3.2 [<A HREF="#References">BPTF08</A>] (<em>demo only</em>);
+	<LI> <tt>spass</tt>&mdash;SPASS 3.8ds [<A HREF="#References">BPWW12</A>];
+	<LI> <tt>vampire</tt>&mdash;Vampire 1.8 (revision 1435) [<A HREF="#References">RV02</A>];
+	<LI> <tt>e</tt>&mdash;E 1.4 [<A HREF="#References">Sch04</A>];
+	<LI> <tt>z3_tptp</tt>&mdash;Z3 3.2 with TPTP syntax [<A HREF="#References">dMB08</A>].
+	</UL>
+<DT> <tt>nitpick</tt>
+<DD> For problems involving only the type <tt>$o</tt> of Booleans, checks
+	 whether a finite model exists using Nitpick [<A HREF="#References">BN10</A>].
+<DT> <tt>simp</tt>
+<DD> Performs equational reasoning using rewrite rules [<A HREF="#References">Nip89</A>].
+<DT> <tt>blast</tt>
+<DD> Searches for a proof using a fast untyped tableau prover and then
+     attempts to reconstruct the proof using Isabelle tactics
+     [<A HREF="#References">Pau99</A>].
+<DT> <tt>auto+spass</tt>
+<DD> Combines simplification and classical reasoning
+	 [<A HREF="#References">Pau94</A>] under one roof; then invoke Sledgehammer
+     with SPASS on any subgoals that emerge.
+<DT> <tt>z3</tt>
+<DD> Invokes the SMT solver Z3 3.2 [<A HREF="#References">dMB08</A>].
+<DT> <tt>cvc3</tt>
+<DD> Invokes the SMT solver CVC3 2.2 [<A HREF="#References">BT07</A>].
+<DT> <tt>fast</tt>
+<DD> Searches for a proof using sequent-style reasoning, performing a
+     depth-first search [<A HREF="#References">Pau94</A>]. Unlike
+     <tt>blast</tt>, it construct proofs directly in Isabelle. That makes it
+     slower but enables it to work in the presence of the more unusual features
+     of HOL, such as type classes and function unknowns.
+<DT> <tt>best</tt>
+<DD> Similar to <tt>fast</tt>, except that it performs a best-first search.
+<DT> <tt>force</tt>
+<DD> Similar to <tt>auto</tt>, but more exhaustive.
+<DT> <tt>meson</tt>
+<DD> Implements Loveland's MESON procedure [<A HREF="#References">Lov78</A>].
+Constructs proofs directly in Isabelle.
+<DT> <tt>fastforce</tt>
+<DD> Combines <tt>fast</tt> and <tt>force</tt>.
+</DL>
+
+<H3>Implementation</H3>
+
+Isabelle is a generic theorem prover written in Standard ML. Its meta-logic,
+Isabelle/Pure, provides an intuitionistic fragment of higher-order logic. The
+HOL object logic extends pure with a more elaborate version of higher-order
+logic, complete with the familiar connectives and quantifiers. Other object
+logics are available, notably FOL (first-order logic) and ZF
+(Zermelo&ndash;Fraenkel set theory).
+<P>
+The implementation of Isabelle relies on a small LCF-style kernel, meaning that
+inferences are implemented as operations on an abstract <tt>theorem</tt>
+datatype. Assuming the kernel is correct, all values of type <tt>theorem</tt>
+are correct by construction.
+<P>
+Most of the code for Isabelle was written by the Isabelle teams at the
+University of Cambridge and the Technische Universit&auml;t M&uuml;nchen.
+Isabelle/HOL is available for all major platforms under a BSD-style license
+from
+<PRE>
+    <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE>
+
+<H3>Expected Competition Performance</H3>
+
+<P>
+Isabelle won last year by a thin margin. This year: first or second place.
+
+<H3>References</H3>
+<DL>
+
+<DT> BBP11
+<DD> Blanchette J. C., B&ouml;hme S., Paulson L. C. (2011),
+     <STRONG>Extending Sledgehammer with SMT Solvers</STRONG>,
+     CADE-23, LNAI 6803, pp. 116&ndash;130, Springer.
+<DT> BN10
+<DD> Blanchette J. C., Nipkow T. (2010),
+     <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>,
+     ITP 2010, <EM>LNCS</EM> 6172, pp. 131&ndash;146, Springer.
+<DT> BPTF08
+<DD> Benzm&uuml;ller C., Paulson L. C., Theiss F., Fietzke A. (2008),
+  	 <STRONG>LEO-II&mdash;A Cooperative Automatic Theorem Prover for Higher-Order Logic</STRONG>,
+  	 IJCAR 2008, <EM>LNAI</EM> 5195, pp. 162&ndash;170, Springer.
+<DT> BPWW12
+<DD> Blanchette J. C., Popescu A., Wand D., Weidenbach C. (2012),
+	 <STRONG>More SPASS with Isabelle</STRONG>,
+	 ITP 2012, Springer.
+<DT> Bro12
+<DD> Brown C. (2012),
+	 <STRONG>Satallax: An Automated Higher-Order Prover (System Description)</STRONG>,
+	 IJCAR 2012, Springer.
+<DT> BT07
+<DD> Barrett C., Tinelli C. (2007),
+	 <STRONG>CVC3 (System Description)</STRONG>,
+  	 CAV 2007, <EM>LNCS</EM> 4590, pp. 298&ndash;302, Springer.
+<DT> dMB08
+<DD> de Moura L. M., Bj&oslash;rner N. (2008),
+     <STRONG>Z3: An Efficient SMT Solver</STRONG>,
+	 TACAS 2008, <EM>LNCS</EM> 4963, pp. 337&ndash;340, Springer.
+<DT> Lov78
+<DD> Loveland D. W. (1978),
+     <STRONG>Automated Theorem Proving: A Logical Basis</STRONG>,
+     North-Holland Publishing Co.
+<DT> Nip89
+<DD> Nipkow T. (1989),
+     <STRONG>Equational Reasoning in Isabelle</STRONG>,
+     <EM>Sci. Comput. Program.</EM> 12(2),
+     pp. 123&ndash;149,
+     Elsevier.
+<DT> NPW13
+<DD> Nipkow T., Paulson L. C., Wenzel M. (2013),
+     <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>,
+     <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>.
+<DT> Pau94
+<DD> Paulson L. C. (1994),
+     <STRONG>Isabelle: A Generic Theorem Prover</STRONG>,
+     <EM>LNCS</EM> 828,
+     Springer.
+<DT> Pau99
+<DD> Paulson L. C. (1999),
+     <STRONG>A Generic Tableau Prover and Its Integration with Isabelle</STRONG>,
+     <EM>J. Univ. Comp. Sci.</EM> 5,
+     pp. 73&ndash;87.
+<DT> PB10
+<DD> Paulson L. C., Blanchette J. C. (2010),
+     <STRONG>Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers</STRONG>,
+     IWIL-2010.
+<DT> RV02
+<DD> Riazanov A., Voronkov A. (2002),
+  	 <STRONG>The Design and Implementation of Vampire</STRONG>,
+  	 <EM>AI Comm.</EM> 15(2-3), 91&ndash;110.
+<DT> Sch04
+<DD> Schulz S. (2004),
+  	 <STRONG>System Description: E 0.81</STRONG>,
+  	 IJCAR 2004, <EM>LNAI</EM> 3097, pp. 223&ndash;228, Springer.
+</DL>
+<P>
+
+<HR><!------------------------------------------------------------------------>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC/SysDesc_Nitpick.html	Tue May 21 11:01:14 2013 +0200
@@ -0,0 +1,82 @@
+<HR><!------------------------------------------------------------------------>
+<H2>Nitpick 2013</H2>
+Jasmin C. Blanchette<BR>
+Technische Universit&auml;t M&uuml;nchen, Germany <BR>
+
+<H3>Architecture</H3>
+
+Nitpick [<A HREF="#References">BN10</A>] is an open source counterexample 
+generator for Isabelle/HOL [<A HREF="#References">NPW13</A>]. It builds on
+Kodkod [<A HREF="#References">TJ07</A>], a highly optimized first-order
+relational model finder based on SAT. The name Nitpick is appropriated from a
+now retired Alloy precursor. In a case study, it was applied successfully to a
+formalization of the C++ memory model [<A HREF="#References">BWB+11</A>].
+
+<H3>Strategies</H3>
+
+<p>
+Nitpick employs Kodkod to find a finite model of the negated conjecture. The
+translation from HOL to Kodkod's first-order relational logic (FORL) is
+parameterized by the cardinalities of the atomic types occurring in it. Nitpick
+enumerates the possible cardinalities for each atomic type, exploiting
+monotonicity to prune the search space [<A HREF="#References">BK11</A>]. If a
+formula has a finite counterexample, the tool eventually finds it, unless it
+runs out of resources.
+
+<p>
+SAT solvers are particularly sensitive to the encoding of problems, so special
+care is needed when translating HOL formulas.
+As a rule, HOL scalars are mapped to FORL singletons and functions are mapped to
+FORL relations accompanied by a constraint. More specifically,
+an <i>n</i>-ary first-order function (curried or not) can be coded as an
+(<i>n</i> + 1)-ary relation accompanied by a constraint. However, if the return
+type is the type of Booleans, the function is more efficiently coded as an
+unconstrained <i>n</i>-ary relation.
+Higher-order quantification and functions bring complications of their own. A
+function from &sigma; to &tau; cannot be directly passed as an argument in FORL;
+Nitpick's workaround is to pass |&sigma;| arguments of type &tau; that encode a
+function table.
+
+<H3>Implementation</H3>
+
+<p>
+Nitpick, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle
+itself, which adheres to the LCF small-kernel discipline, Nitpick does not
+certify its results and must be trusted.
+<P>
+Nitpick is available as part of Isabelle/HOL for all major platforms under a
+BSD-style license from
+<PRE>
+    <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE>
+
+<H3>Expected Competition Performance</H3>
+
+Thanks to Kodkod's amazing power, we expect that Nitpick will beat both Satallax
+and Refute with its hands tied behind its back in the TNT category.
+
+<H3>References</H3>
+<DL>
+<DT> BK11
+<DD> Blanchette J. C., Krauss A. (2011),
+     <STRONG>Monotonicity Inference for Higher-Order Formulas</STRONG>,
+     <EM>J. Autom. Reasoning</EM> 47(4), pp. 369&ndash;398, 2011.
+<DT> BN10
+<DD> Blanchette J. C., Nipkow T. (2010),
+     <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>,
+     ITP 2010, <EM>LNCS</EM> 6172, pp. 131&ndash;146, Springer.
+<DT> BWB+11
+<DD> Blanchette J. C., Weber T., Batty M., Owens S., Sarkar S. (2011),
+	 <STRONG>Nitpicking C++ Concurrency</STRONG>,
+	 PPDP 2011, pp. 113&ndash;124, ACM Press.
+<DT> NPW13
+<DD> Nipkow T., Paulson L. C., Wenzel M. (2013),
+     <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>,
+     <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>.
+<DT> TJ07
+<DD> Torlak E., Jackson D. (2007),
+     <STRONG>Kodkod: A Relational Model Finder</STRONG>, TACAS 2007,
+	 <EM>LNCS</EM> 4424, pp. 632&ndash;647, Springer.
+</DL>
+<P>
+
+<HR><!------------------------------------------------------------------------>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC/SysDesc_Nitrox.html	Tue May 21 11:01:14 2013 +0200
@@ -0,0 +1,78 @@
+<HR><!------------------------------------------------------------------------>
+<H2>Nitrox 2013</H2>
+Jasmin C. Blanchette<sup>1</sup>, Emina Torlak<sup>2</sup><BR>
+<sup>1</sup>Technische Universit&auml;t M&uuml;nchen, Germany <BR>
+<sup>2</sup>University of California, Berkeley, USA <BR>
+
+<H3>Architecture</H3>
+
+Nitrox is the first-order version of Nitpick [<A HREF="#References">BN10</A>],
+an open source counterexample generator for Isabelle/HOL
+[<A HREF="#References">NPW13</A>]. It builds on Kodkod
+[<A HREF="#References">TJ07</A>], a highly optimized first-order relational
+model finder based on SAT. The name Nitrox is a portmanteau of <b><i>Nit</i></b>pick
+and Pa<b><i>r</i></b>ad<b><i>ox</i></b> (clever, eh?).
+
+<H3>Strategies</H3>
+
+<p>
+Nitrox employs Kodkod to find a finite model of the negated conjecture. It
+performs a few transformations on the input, such as pushing quantifiers inside,
+but 99% of the solving logic is in Kodkod and the underlying SAT solver.
+
+<p>
+The translation from HOL to Kodkod's first-order relational logic (FORL) is
+parameterized by the cardinalities of the atomic types occurring in it. Nitrox
+enumerates the possible cardinalities for the universe. If a formula has a
+finite counterexample, the tool eventually finds it, unless it runs out of
+resources.
+
+<p>
+Nitpick is optimized to work with higher-order logic (HOL) and its definitional
+principles (e.g., (co)inductive predicates, (co)inductive datatypes,
+(co)recursive functions). When invoked on untyped first-order problem, few of
+its optimizations come into play, and the problem handed to Kodkod is
+essentially a first-order relational logic (FORL) rendering of the TPTP FOF
+problem. There are two main exceptions:
+<ul>
+<li> Nested quantifiers are moved as far inside the formula as possible before
+Kodkod gets a chance to look at them [<A HREF="#References">BN10</A>].
+<li> Definitions invoked with fixed arguments are specialized.
+</ul>
+
+<H3>Implementation</H3>
+
+<p>
+Nitrox, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle
+itself, which adheres to the LCF small-kernel discipline, Nitrox does not
+certify its results and must be trusted. Kodkod is written in Java. MiniSat 1.14
+is used as the SAT solver.
+
+<H3>Expected Competition Performance</H3>
+
+Since Nitpick was designed for HOL, it doesn't have any type inference &agrave;
+la Paradox. It also doesn't use the SAT solver incrementally, which penalizes it
+a bit (but not as much as the missing type inference). Kodkod itself is known to
+perform less well on FOF than Paradox, because it is designed and optimized for
+a somewhat different logic, FORL. On the other hand, Kodkod's symmetry breaking
+might be better calibrated than Paradox's. Hence, we expect Nitrox to end up in
+second or third place in the FNT category.
+
+<H3>References</H3>
+<DL>
+<DT> BN10
+<DD> Blanchette J. C., Nipkow T. (2010),
+     <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>,
+     ITP 2010, <EM>LNCS</EM> 6172, pp. 131&ndash;146, Springer.
+<DT> NPW13
+<DD> Nipkow T., Paulson L. C., Wenzel M. (2013),
+     <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>,
+     <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>.
+<DT> TJ07
+<DD> Torlak E., Jackson D. (2007),
+     <STRONG>Kodkod: A Relational Model Finder</STRONG>, TACAS 2007,
+	 <EM>LNCS</EM> 4424, pp. 632&ndash;647, Springer.
+</DL>
+<P>
+
+<HR><!------------------------------------------------------------------------>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC/SysDesc_Refute.html	Tue May 21 11:01:14 2013 +0200
@@ -0,0 +1,55 @@
+<HR><!------------------------------------------------------------------------>
+<H2>Refute 2013</H2>
+Jasmin C. Blanchette<sup>1</sup>, Tjark Weber<sup>2</sup><BR>
+<sup>1</sup>Technische Universit&auml;t M&uuml;nchen, Germany <BR>
+<sup>2</sup>Uppsala Universitet, Sweden <BR>
+
+<H3>Architecture</H3>
+
+Refute [<A HREF="#References">Web08</A>] is an open source counterexample 
+generator for Isabelle/HOL [<A HREF="#References">NPW13</A>] based on a
+SAT solver, and Nitpick's [<A HREF="#References">BN10</A>] precursor.
+
+<H3>Strategies</H3>
+
+<p>
+Refute employs a SAT solver to find a finite model of the negated conjecture.
+The translation from HOL to propositional logic is parameterized by the
+cardinalities of the atomic types occurring in the conjecture. Refute enumerates
+the possible cardinalities for each atomic type. If a formula has a finite
+counterexample, the tool eventually finds it, unless it runs out of resources.
+
+<H3>Implementation</H3>
+
+<p>
+Refute, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle
+itself, which adheres to the LCF small-kernel discipline, Refute does not
+certify its results and must be trusted.
+<P>
+Refute is available as part of Isabelle/HOL for all major platforms under a
+BSD-style license from
+<PRE>
+    <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE>
+
+<H3>Expected Competition Performance</H3>
+
+We expect that Refute will solve about 75% of the problems solved by Nitpick in
+the TNT category, and perhaps a few problems that Nitpick cannot solve.
+
+<H3>References</H3>
+<DL>
+<DT> BN10
+<DD> Blanchette J. C., Nipkow T. (2010),
+     <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>,
+     ITP 2010, <EM>LNCS</EM> 6172, pp. 131&ndash;146, Springer.
+<DT> NPW13
+<DD> Nipkow T., Paulson L. C., Wenzel M. (2013),
+     <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>,
+     <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>.
+<DT> Web08
+<DD> Weber T. (2008),
+     <STRONG>SAT-based Finite Model Generation for Higher-Order Logic</STRONG>, Ph.D. thesis.
+</DL>
+<P>
+
+<HR><!------------------------------------------------------------------------>