Commit 122c0632 authored by MARCHE Claude's avatar MARCHE Claude

Support for Metis (seems to work) and MetiTarski (does not work)

parent 9a024325
(* Why driver for Metis *)
valid "SZS status Theorem"
valid "SZS status Unsatisfiable"
unknown "SZS status CounterSatisfiable" ""
unknown "SZS status Satisfiable" ""
unknown "SZS status Unknown" ""
timeout "SZS status Timeout"
unknown "SZS status GaveUp" ""
fail "SZS status Error" ""
import "tptp.gen"
import "discrimination.gen"
(* Why driver for MetiTarski *)
valid "Proof found"
invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
import "tptp.gen"
import "discrimination.gen"
......@@ -19,26 +19,30 @@
version="1.6"/>
<prover
id="4"
name="Metis"
version="2.3"/>
<prover
id="5"
name="Spass"
version="3.7"/>
<prover
id="5"
id="6"
name="Vampire"
version="0.6"/>
<prover
id="6"
id="7"
name="Yices"
version="1.0.38"/>
<prover
id="7"
id="8"
name="Z3"
version="2.19"/>
<prover
id="8"
id="9"
name="Z3"
version="3.2"/>
<prover
id="9"
id="10"
name="Z3"
version="4.3.1"/>
<file
......@@ -120,6 +124,14 @@
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="4.95"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -127,7 +139,7 @@
<result status="valid" time="4.66"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -135,7 +147,7 @@
<result status="valid" time="1.83"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="7"
memlimit="0"
obsolete="false"
......@@ -143,7 +155,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -151,7 +163,7 @@
<result status="valid" time="1.02"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -159,7 +171,7 @@
<result status="valid" time="0.48"/>
</proof>
<proof
prover="9"
prover="10"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -213,7 +225,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.98"/>
<result status="unknown" time="4.50"/>
</proof>
<proof
prover="5"
......@@ -221,18 +233,26 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="9.98"/>
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="9.98"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -240,7 +260,7 @@
<result status="timeout" time="4.95"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -248,7 +268,7 @@
<result status="timeout" time="4.96"/>
</proof>
<proof
prover="9"
prover="10"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -298,6 +318,14 @@
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="4.99"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -305,7 +333,7 @@
<result status="valid" time="4.52"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="20"
memlimit="1000"
obsolete="false"
......@@ -313,7 +341,7 @@
<result status="valid" time="1.56"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="7"
memlimit="0"
obsolete="false"
......@@ -321,7 +349,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -329,7 +357,7 @@
<result status="valid" time="1.54"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -337,7 +365,7 @@
<result status="valid" time="0.76"/>
</proof>
<proof
prover="9"
prover="10"
timelimit="30"
memlimit="1000"
obsolete="false"
......
......@@ -19,30 +19,34 @@
version="1.6"/>
<prover
id="4"
name="Metis"
version="2.3"/>
<prover
id="5"
name="Spass"
version="3.7"/>
<prover
id="5"
id="6"
name="Vampire"
version="0.6"/>
<prover
id="6"
id="7"
name="Yices"
version="1.0.38"/>
<prover
id="7"
id="8"
name="Z3"
version="2.19"/>
<prover
id="8"
id="9"
name="Z3"
version="3.2"/>
<prover
id="9"
id="10"
name="Z3"
version="4.3.1"/>
<prover
id="10"
id="11"
name="Zenon"
version="0.7.1"/>
<file
......@@ -98,10 +102,10 @@
<proof
prover="4"
timelimit="5"
memlimit="0"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -109,7 +113,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
......@@ -117,7 +121,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
......@@ -125,7 +129,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="8"
......@@ -138,13 +142,21 @@
<proof
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="2.12"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -195,10 +207,10 @@
<proof
prover="4"
timelimit="5"
memlimit="0"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="5"
......@@ -222,7 +234,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
......@@ -235,13 +247,21 @@
<proof
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -292,10 +312,10 @@
<proof
prover="4"
timelimit="5"
memlimit="0"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="5"
......@@ -303,7 +323,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
......@@ -311,7 +331,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
......@@ -319,7 +339,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="8"
......@@ -332,13 +352,21 @@
<proof
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="2.12"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -387,7 +415,15 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -395,7 +431,7 @@
<result status="valid" time="0.04"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -403,7 +439,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -411,7 +447,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -419,7 +455,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -470,10 +506,10 @@
<proof
prover="4"
timelimit="5"
memlimit="0"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
......@@ -481,7 +517,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
......@@ -489,7 +525,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="7"
......@@ -497,7 +533,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
......@@ -510,13 +546,21 @@
<proof
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -567,13 +611,21 @@
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -581,7 +633,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -589,7 +641,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -597,7 +649,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -605,7 +657,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -613,7 +665,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -664,13 +716,21 @@
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -678,7 +738,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -686,7 +746,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -694,7 +754,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -702,7 +762,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="10"
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
......
......@@ -197,6 +197,24 @@ version_old = "1.5.4"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/simplify.drv"
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --time-limit %t %f"
driver = "drivers/metis.drv"
[ATP metitarski]
name = "MetiTarski"
exec = "metit"
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
version_ok = "2.2"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --time %t %f"
driver = "drivers/metitarski.drv"
[ATP spass]
name = "Spass"
exec = "SPASS"
......
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