Commit 98be3171 authored by MARCHE Claude's avatar MARCHE Claude

Add missing driver file for Zenon Modulo

parent 80fcc07d
(* Why driver for first-order tptp provers *)
printer "tptp-tff1"
filename "%f-%t-%g.p"
valid "PROOF-FOUND"
timeout "Zenon error: could not find a proof within the time limit"
outofmemory "Zenon error: could not find a proof within the memory size limit"
unknown "NO-PROOF" "no proof found"
time "why3cpulimit time : %s s"
(* to be improved *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
import "discrimination.gen"
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