Tyrolean Termination Tool 2

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) )
input Upload a file (SRS or TRS) in the standard format. See http://www.lri.fr/~marche/tpdb/format.html for details.
LPO lexicographic path order (strict precedence) KBO Knuth-Bendix order (strict precedence) POLY linear polynomials with coefficients in {0, ..., 31} (intermediate coefficients in {0, ..., 63}) MATRIX(2) matrices of dimension 2 with coefficients in {0, ..., 7} (intermediate coefficients in {0, ..., 15}) MATRIX(3) matrices of dimension 3 with coefficients in {0, ..., 3} (intermediate coefficients in {0, ..., 7}) AUTO The strategy used in the November 2008 competition for TRSs/SRSs. COMPLEXITY The strategy used in the November 2008 competition for complexity certificates (derivational complexity). CP Computes overlaps, critical pairs and determines which ones are joinable. EXPERT Expert mode; enter your own strategy