Module Saturate

module Saturate: sig .. end

Main saturation algorithm.

It uses inference rules and simplification rules from Superposition.

val check_timeout : float option -> bool
check whether we still have some time w.r.t timeout
type szs_status = 
| Unsat of ProofStep.of_
| Sat
| Unknown
| Error of string
| Timeout
The SZS status of a state
module type S = sig .. end
module Make: 
functor (E : Env.S) -> S with module Env = E