Check whether a conclusion is logically entailed by a set of premises, by asking whether (premises AND NOT conclusion) is unsatisfiable, cross-checked in both Z3 and cvc5.

YOU (the calling model) are responsible for translating the user's prose question into declarations, premises, and conclusion. This server does NOT interpret English — it only runs the SMT-LIB you hand it. Pass the user's original wording in prose so the English and the formalization travel together in the evidence trail.

Before presenting the verdict to the user as an answer about their original English question, SHOW THEM THE FORMALIZATION (the declarations, premises, and conclusion, or the assembled smtlib_script) and get their agreement that it captures what they meant. A verdict from this tool is a fact about the formalization, not directly about the user's English — whether the formalization is a faithful translation of their intent is the user's call, not yours.

Report exactly what the solvers returned. Do not upgrade "both solvers said unsat under these bounds" into an unqualified "yes, this is true" — an ENTAILMENT_HOLDS verdict is bounded-unsat relative to the premises and declarations as written, not an unbounded proof about the world. Read the caveats list and pass its contents along; each one names a specific way the guarantee is weaker than it may sound (quantifiers, nonlinear arithmetic, uninterpreted sorts, or a bounded check). If status comes back DISAGREEMENT, that is the headline: tell the user the two solvers returned different verdicts and that the result must not be trusted, do not average or pick one to report.

declarations are full SMT-LIB forms, e.g. (declare-const x Int) or (declare-fun key (String) String). premises and conclusion are bare boolean terms, e.g. (> x 5) — this tool wraps each premise in (assert ...) for you (a premise that already starts with (assert is accepted as-is, not double-wrapped).

Worked example (propositional modus ponens): declarations = ["(declare-const p Bool)", "(declare-const q Bool)"] premises = ["(=> p q)", "p"] conclusion = "q" -> entailment holds (both solvers report the negated-conclusion script is unsatisfiable).

Check whether a set of constraints is jointly satisfiable, cross-checked in both Z3 and cvc5.

YOU (the calling model) are responsible for translating the user's prose question into declarations and constraints. This server does NOT interpret English — it only runs the SMT-LIB you hand it. Pass the user's original wording in prose so the English and the formalization travel together in the evidence trail.

Before presenting the verdict to the user as an answer about their original English question, SHOW THEM THE FORMALIZATION (the declarations and constraints, or the assembled smtlib_script) and get their agreement that it captures what they meant. A verdict from this tool is a fact about the formalization, not directly about the user's English.

Report exactly what the solvers returned. An UNSATISFIABLE verdict is bounded-unsat relative to the constraints and declarations as written, not an unbounded proof about the world — do not upgrade it into a stronger claim. Read the caveats list and pass its contents along (quantifiers, nonlinear arithmetic, uninterpreted sorts, or bounded checks each get their own caveat). If status comes back DISAGREEMENT, that is the headline: the two solvers returned different verdicts and the result must not be trusted.

declarations are full SMT-LIB forms, e.g. (declare-const x Int). constraints are bare boolean terms, e.g. (> x 5) — this tool wraps each in (assert ...) for you (a constraint that already starts with (assert is accepted as-is).

Example: declarations = ["(declare-const x Int)"] constraints = ["(> x 5)", "(< x 8)"] -> satisfiable (both solvers find a witness, e.g. x = 6).

Run a fully-assembled SMT-LIB v2 script verbatim, cross-checked in both Z3 and cvc5. Use this when check_entailment / check_satisfiability's fixed shapes (declarations + premises/constraints + optional single conclusion) are not expressive enough — e.g. you need multiple (check-sat) calls, push/pop, or solver-specific tactics.

YOU (the calling model) build the entire script yourself, including (check-sat). This server does not interpret English and does not modify your script. As with the other tools: report exactly what came back, do not upgrade unsat under bounds into an unbounded claim, and treat a DISAGREEMENT between the two solvers as the headline finding, not a footnote.

Report which Z3 and cvc5 binaries this server resolved (path, whether the binary was found, and its reported version string). Useful for confirming the environment before trusting any verdict from this server, and for attaching solver versions to an audit trail.