MAYBE
(ignored inputs)COMMENT [113] Example 4.14 submitted by: Aart Middeldorp
input TRS:
   [ +(?x,0) -> ?x,
     +(0,?x) -> ?x,
     +(?x,-(?x)) -> 0,
     +(?x,+(-(?x),?y)) -> ?y,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     -(0) -> 0,
     -(-(?x)) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)),
     +(?x,?y) -> +(?y,?x) ]
TRS:
   [ +(?x,0) -> ?x,
     +(0,?x) -> ?x,
     +(?x,-(?x)) -> 0,
     +(?x,+(-(?x),?y)) -> ?y,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     -(0) -> 0,
     -(-(?x)) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check distinct normal forms in critical pair closure...failed
problems/535.trs: Failure(unknown UNC)
(64 msec.)