TPI Commands

• input, output : Input a file. Output stored formulae.
• deactivate, activate : Deactivate and activate a formula.
• set_role : Set the role (axiom, conjecture, etc.) of a formula.
• delete : Delete a formula.
• start_group, end_group : Start and end a formula group.
• deactivate_group, activate_group, delete_group : Deactivate, activate, and delete a formula group.
• setenv, unsetenv, waitenv : Set, unset, and wait for an environment variable (to be set).
• mktemp : Make a temporary file.
• set_logic : Sets the logic/semantics of the stored formulae.
• execute, execute_async : Execute (asynchronously) a program, with an SZS ontology result.
• filter : Execute a program to filter and replace formulae.
• generate : Execute a program to generate formulae.
• assert : Check an assertion.
• write : Write terms to stdout.
• exit : Halt the TPI system.