MAYBE
  TPA v.1.0

Result: Couldn't prove (non-)termination of that system. Only partial proof available.

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) f(X,g(X)) -> f(1,g(X))
(2) g(1) -> g(0)

[2]  Label this TRS using following interpretation over N\{0,1}:
[f(x,y)] = 2
[g(x)] = 2
[1] = 3
rest default

  This interpretation is a model and yields following TRS:
(1) f{i,2}(X,g{i}(X)) -> f{3,2}(1,g{i}(X))
(2) g{3}(1) -> g{2}(0)

[3]  Use following polynomial interpretation:
[f_{i,j}(x,y)] = x + y - 2
[g_{i}(x)] = x + i
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2)

[4]  Unlabel this TRS to obtain the one consisting of the rules:
(1)


../tpdb/TRS/nontermin/Rubio-inn/gkg.trs, 0., U
Couldn't open file <60>: 60: No such file or directory