(* Why driver for first-order tptp provers *)

printer "tptp"
filename "%f-%t-%g.p"

valid   "Proof found"
invalid "Completion found"
timeout "Ran out of time"
timeout "Resource limit exceeded"
unknown "No Proof Found"            "Unknown"
fail    "Failure"                   "Failure"

(* to be improved *)

transformation "simplify_recursive_definition"
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"

transformation "encoding_tptp"

theory BuiltIn
  syntax logic (=)  "(%1 = %2)"
end

(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)