Commit 3ed1ce1e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix my own silliness in provers-data.conf + remove bogus prelude from tptp.drv

parent 73ee2d1e
(* Why driver for tptp first-order logic solvers *) (* Why driver for first-order tptp provers *)
prelude "% this is a why prelude for tptp solvers
fof(two_constants, axiom, ~ ('0' = '1'))."
printer "tptp" printer "tptp"
filename "%f-%t-%g.p" filename "%f-%t-%g.p"
......
...@@ -62,7 +62,7 @@ driver = "drivers/simplify.drv" ...@@ -62,7 +62,7 @@ driver = "drivers/simplify.drv"
[ATP spass] [ATP spass]
name = "Spass" name = "Spass"
exec = "SPASS" exec = "SPASS"
version_switch = "|| false" version_switch = "-TPTP || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)" version_regexp = "SPASS V \\([^ \n\t]+\\)"
command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1" command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv" driver = "drivers/tptp.drv"
......
...@@ -69,6 +69,7 @@ theory UnitaryCommutativeRing ...@@ -69,6 +69,7 @@ theory UnitaryCommutativeRing
clone export CommutativeRing clone export CommutativeRing
logic one : t logic one : t
axiom Unitary : forall x:t. one * x = x axiom Unitary : forall x:t. one * x = x
axiom NonTrivialRing : zero <> one
end end
theory Field theory Field
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment