NO
(ignored inputs)COMMENT [38] Example 4
input TRS:
   [ f(u(O),u(?y)) -> A,
     f(v(?x),v(O)) -> B,
     O -> u(O),
     O -> v(O),
     u(?x) -> ?x,
     v(?x) -> ?x,
     f(?x,?y) -> f(?x,u(?y)),
     f(?x,?y) -> f(v(?x),?y) ]
TRS:
   [ f(u(O),u(?y)) -> A,
     f(v(?x),v(O)) -> B,
     O -> u(O),
     O -> v(O),
     u(?x) -> ?x,
     v(?x) -> ?x,
     f(?x,?y) -> f(?x,u(?y)),
     f(?x,?y) -> f(v(?x),?y) ]
New rules by rule reversing:
   [ f(u(O),u(?y)) -> A,
     f(v(?x),v(O)) -> B,
     O -> O,
     u(O) -> O,
     O -> O,
     v(O) -> O,
     u(?x) -> ?x,
     v(?x) -> ?x,
     f(?x,?y) -> f(?x,?y),
     f(?x,u(?y)) -> f(?x,?y),
     f(?x,?y) -> f(?x,?y),
     f(v(?x),?y) -> f(?x,?y) ]
constructed TRS:
   [ f(u(O),u(?y)) -> A,
     f(v(?x),v(O)) -> B,
     O -> O,
     u(O) -> O,
     O -> O,
     v(O) -> O,
     u(?x) -> ?x,
     v(?x) -> ?x,
     f(?x,?y) -> f(?x,?y),
     f(?x,u(?y)) -> f(?x,?y),
     f(?x,?y) -> f(?x,?y),
     f(v(?x),?y) -> f(?x,?y),
     f(O,u(?y)) -> A,
     f(u(O),O) -> A,
     f(u(O),?x_2) -> A,
     f(O,v(O)) -> B,
     f(v(?x_1),O) -> B,
     f(?x_3,v(O)) -> B ]
convertible distinct normal forms: A = B
UNC Completion (Development Closed)
problems/216.trs: Success(not UNC)
(16 msec.)