An entailment prover for a fragment of first-order logic with inductive definitions. Only these definitions can be used in the demo.
Set timeout in seconds, 0 disables it.