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) ]
constructed 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),
     f(u(u(O)),u(?y)) -> A,
     f(u(v(O)),u(?y)) -> A,
     f(O,u(?y)) -> A,
     f(u(O),?x_2) -> A,
     f(v(u(O)),u(?y)) -> A,
     f(v(?x_1),v(u(O))) -> B,
     f(v(?x_1),v(v(O))) -> B,
     f(?x_3,v(O)) -> B,
     f(v(?x_1),O) -> B,
     f(v(?x_1),u(v(O))) -> B ]
convertible distinct normal forms: B = A
UNC Completion (Strongly Closed)
problems/216.trs: Success(not UNC)
(44 msec.)