Input TRS: 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)) Number of strict rules: 3 Direct Order(PosReal,>,Poly) ... removes: 1 3 2 div(x1,x2) weight: (/ 3 16) + 2 * x1 + x2 i(x1) weight: (/ 1 16) + 2 * x1 e() weight: 0 Number of strict rules: 0 YES