Extra theories added as requires in the input

The standard input may depend on arbitrary module

Does not prefix first order connectives while printing,
Explicit terms
Use different signature states

Drop TPTP related code