Princess is a theorem prover developed and maintained by Uppsala University and the University of Regensburg. Princess accepts input in its own format, in SMT-LIB format, or in TPTP.