# HG changeset patch
# User sultana
# Date 1378241201 -3600
# Node ID 5278312037f8b6c7d6c7169bde04eea7134fed65
# Parent  a1a45fdc53a3084d6e5662b8494183b7a26d9e60
included axiom formulas (removing a FIXME) in the imported problem;
turned tests into asserts;
changed problem to one which actually succeeds using z3;

diff -r a1a45fdc53a3 -r 5278312037f8 src/HOL/TPTP/TPTP_Parser_Example.thy
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Sep 03 21:46:41 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Sep 03 21:46:41 2013 +0100
@@ -10,7 +10,7 @@
 
 ML_file "sledgehammer_tactics.ML"
 
-import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
+import_tptp "$TPTP/Problems/LCL/LCL414+1.p"
 
 ML {*
 val an_fmlas =
@@ -46,7 +46,7 @@
   let
     val assumptions =
       extract_terms
-       [TPTP_Syntax.Role_Definition (*FIXME include axioms, etc here*)]
+       [TPTP_Syntax.Role_Definition, TPTP_Syntax.Role_Axiom]
        an_fmlas
       |> map snd
     val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
@@ -61,9 +61,13 @@
   {add = [], del = [], only = false} 1)
 *}
 
-ML "auto_prove @{context} an_fmlas"
+ML {*
+@{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
+*}
 
-sledgehammer_params [provers = z3_tptp leo2, debug]
-ML "sh_prove @{context} an_fmlas"
+sledgehammer_params [provers = remote_z3, debug]
+ML {*
+@{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
+*}
 
 end
\ No newline at end of file