You can run SAD on the problems from the TPTP Problem Library or try your own problem in the format of TPTP. Browse the problem library, find the problem you are interested in, and enter its name in the input field below. The name has to follow the standard problem naming scheme (e.g. FLD037-1.p, MSC007-2.005.p, SET027+3.p, etc). Then use the command [Load] to download the problem into the edit window. You may enter a problem manually in the edit window as well.

In our system, we do not keep a local copy of the TPTP library: problems and axioms are downloaded directly from the TPTP web page. Therefore we put some constraints on the include instructions in the problems: any include instruction must occupy a separate line in the input, inclusion is allowed for the TPTP Axioms only, selective inclusion is not supported. These requirements are compatible with all the problems in the TPTP Library v2.6.0.

Use the command [Parse] to see the translation of the input TPTP problem to the first-order language (axioms included). Use the command [Prove with Moses] or [Prove with] to launch proof search. Remember that the problems that do not contain conjectures must be checked for (in)satisfiability, so SAD tries to deduce a contradiction from the input formulas and clauses (so that the empty input task is equivalent to the empty sequent).