# 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