Function is_valid 

pub fn is_valid(
    formula: Formula,
    limit_in_seconds: u64,
) -> Result<bool, ProverError>

Check if a given formula is valid

Must pass a time limit in seconds to avoid infinite loops (default is 60)

Example

use theorem_prover::{lang::{Formula, Pred, Term, Var}, ProverError, Imply, Exists, Forall, Pred, Var};
let formula = Imply!(
    Exists!("x", Pred!("p", [Var!("x")])),
    Forall!("x", Pred!("p", [Var!("x")]))
);

is_valid(formula, 5).unwrap() will evaluate to false