Princess Web Interface

Princess is a theorem prover developed and maintained by Uppsala University.
Princess accepts input in its own format, in SMT-LIB format, or in TPTP.
It optionally uses OSTRICH to solve string constraints written using a superset of a subset of the new SMT-LIB string theory.

Load a predefined example: ... or enter some formulas:

Send given input to Princess
Save input on the server and make it available through a private link
  String solver:
String solver to apply to this problem
Enable incremental SMT-LIB processing
Output models/ countermodels
Search for most-general constraints satisfying a formula
Pretty-print proof for valid/unsatisfiable problems. Warning: this will lead to certain quantifiers being ignored, and destroys completeness