author sultana Tue Sep 03 21:46:41 2013 +0100 (2013-09-03) changeset 53393 5278312037f8 parent 53392 a1a45fdc53a3 child 53394 f26f00cbd573
included axiom formulas (removing a FIXME) in the imported problem;
turned tests into asserts;
changed problem to one which actually succeeds using z3;
```     1.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Sep 03 21:46:41 2013 +0100
1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Sep 03 21:46:41 2013 +0100
1.3 @@ -10,7 +10,7 @@
1.4
1.5  ML_file "sledgehammer_tactics.ML"
1.6
1.7 -import_tptp "\$TPTP/Problems/CSR/CSR077+1.p"
1.8 +import_tptp "\$TPTP/Problems/LCL/LCL414+1.p"
1.9
1.10  ML {*
1.11  val an_fmlas =
1.12 @@ -46,7 +46,7 @@
1.13    let
1.14      val assumptions =
1.15        extract_terms
1.16 -       [TPTP_Syntax.Role_Definition (*FIXME include axioms, etc here*)]
1.17 +       [TPTP_Syntax.Role_Definition, TPTP_Syntax.Role_Axiom]
1.18         an_fmlas
1.19        |> map snd
1.20      val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
1.21 @@ -61,9 +61,13 @@
1.22    {add = [], del = [], only = false} 1)
1.23  *}
1.24
1.25 -ML "auto_prove @{context} an_fmlas"
1.26 +ML {*
1.27 +@{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
1.28 +*}
1.29
1.30 -sledgehammer_params [provers = z3_tptp leo2, debug]
1.31 -ML "sh_prove @{context} an_fmlas"
1.32 +sledgehammer_params [provers = remote_z3, debug]
1.33 +ML {*
1.34 +@{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
1.35 +*}
1.36
1.37  end
1.38 \ No newline at end of file
```