Our choice of input format for Term Rewriting Systems is a very popular one: the TPDB format, which is used since 2003 in the Termination Problem Data Base (TPDB). For more information about the original format you can visit the website of the Termination Problem Data Base. Here is a brief description:

spec          ::= (decl) spec | ε
decl          ::= VAR idlist | FUNCTIONS funclist | 
                  CONSTANTS idlist| RULES listofrules | 
                  TERMS listofterms | COMMENTS listofcoments
idlist        ::= id idlist | ε
funclist      ::= funcdef functlist | ε
funcdef       ::= _id_ | _id | id(int)  
listofrules   ::= rule listofrules | ε
rule          ::= term -> term
term          ::= id | id() | id(termlist) | (term)id(term) |
                  (term)id
termlist      ::= term, termlist | term
listofterms   ::= id = term listofterms | ε
listofcoments ::= string listofcoments | ε

Notes about the grammar:

This are the changes introduced in the format for use with this tool: