YES
  TPA v.1.0

Result: TRS is terminating

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) div(X,e) -> i(X)
(2) i(div(X,Y)) -> div(Y,X)
(3) div(div(X,Y),Z) -> div(Y,div(i(X),Z))

[2]  Use following polynomial interpretation:
[div(x,y)] = x + y + 1
rest default

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

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

  This interpretation is a model and yields following TRS:
(2) i{j + i + 1}(div{i,j}(X,Y)) -> div{j,i}(Y,X)
(3) div{j + i + 1,k}(div{i,j}(X,Y),Z) -> div{j,k + i + 1}(Y,div{i,k}(i{i}(X),Z))

[4]  Use following polynomial interpretation:
[div_{i,j}(x,y)] = x + y - 2 + i
[i_{i}(x)] = x + i
rest default

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

[5]  Since there are no remaining rules, termination is proved!

../tpdb/TRS/Rubio/lescanne.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory