CSI
TRS
For input use the standard TRS format. See http://www.lri.fr/~marche/tpdb/format.html for details.

Example:

(VAR x y)
(RULES
f(g(x),y) -> f(x,y)
)
 (examples: )
input Upload a file (TRS) in the standard format. See http://www.lri.fr/~marche/tpdb/format.html for details.  
KB Knuth-Bendix Criterion   DD Decreasing Diagrams   NOTCR Disprove Confluence   order-sorted Find order-sorted decomposition   AUTO automatic mode  
EXPERT Expert mode; enter your own strategy