eprover.drv 322 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7
(* Why driver for Eprover *)

valid   "Proof found"
invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
8
unknown "No proof found" ""
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12
fail    "Failure.*"                   "\"\\0\""
time "why3cpulimit time : %s s"

import "tptp.gen"
13
import "discrimination.gen"