MAYBE
(ignored inputs)COMMENT [117] Example 4.3.12 submitted by: Aart Middeldorp
input TRS:
   [ max(L(?x)) -> ?x,
     max(N(L(0),L(?y))) -> ?y,
     max(N(L(s(?x)),L(s(?y)))) -> s(max(N(L(?x),L(?y)))),
     max(N(L(?x),N(?y,?z))) -> max(N(L(?x),L(max(N(?y,?z))))),
     N(?x,N(?y,?z)) -> N(N(?x,?y),?z),
     N(N(?x,?y),?z) -> N(?x,N(?y,?z)),
     N(?x,?y) -> N(?y,?x) ]
TRS:
   [ max(L(?x)) -> ?x,
     max(N(L(0),L(?y))) -> ?y,
     max(N(L(s(?x)),L(s(?y)))) -> s(max(N(L(?x),L(?y)))),
     max(N(L(?x),N(?y,?z))) -> max(N(L(?x),L(max(N(?y,?z))))),
     N(?x,N(?y,?z)) -> N(N(?x,?y),?z),
     N(N(?x,?y),?z) -> N(?x,N(?y,?z)),
     N(?x,?y) -> N(?y,?x) ]
Check distinct normal forms in critical pair closure...failed
problems/540.trs: Failure(unknown UNC)
(40 msec.)