NO
(ignored inputs)COMMENT [113] Example 4.15; correction of Cops #536 submitted by: Takahito Aoto
input TRS:
   [ xor(?x,0) -> ?x,
     xor(0,?x) -> ?x,
     xor(?x,?x) -> 0,
     and(?x,0) -> 0,
     and(0,?x) -> 0,
     and(?x,1) -> ?x,
     and(1,?x) -> ?x,
     and(?x,?x) -> ?x,
     xor(xor(?x,?y),?z) -> xor(?x,xor(?y,?z)),
     xor(?x,xor(?y,?z)) -> xor(?y,xor(?x,?z)),
     xor(?x,?y) -> xor(?y,?x),
     xor(?x,xor(?x,?y)) -> ?y,
     and(and(?x,?y),?z) -> and(?x,and(?y,?z)),
     and(?x,and(?y,?z)) -> and(?y,and(?x,?z)),
     and(?x,?y) -> and(?y,?x),
     and(?x,and(?x,?y)) -> and(?x,?y),
     and(?x,xor(?y,?z)) -> xor(and(?x,?y),xor(?x,?z)),
     and(xor(?x,?y),?z) -> xor(and(?x,?z),and(?y,?z)) ]
TRS:
   [ xor(?x,0) -> ?x,
     xor(0,?x) -> ?x,
     xor(?x,?x) -> 0,
     and(?x,0) -> 0,
     and(0,?x) -> 0,
     and(?x,1) -> ?x,
     and(1,?x) -> ?x,
     and(?x,?x) -> ?x,
     xor(xor(?x,?y),?z) -> xor(?x,xor(?y,?z)),
     xor(?x,xor(?y,?z)) -> xor(?y,xor(?x,?z)),
     xor(?x,?y) -> xor(?y,?x),
     xor(?x,xor(?x,?y)) -> ?y,
     and(and(?x,?y),?z) -> and(?x,and(?y,?z)),
     and(?x,and(?y,?z)) -> and(?y,and(?x,?z)),
     and(?x,?y) -> and(?y,?x),
     and(?x,and(?x,?y)) -> and(?x,?y),
     and(?x,xor(?y,?z)) -> xor(and(?x,?y),xor(?x,?z)),
     and(xor(?x,?y),?z) -> xor(and(?x,?z),and(?y,?z)) ]
New rules by rule reversing:
   [ xor(?x,0) -> ?x,
     xor(0,?x) -> ?x,
     xor(?x,?x) -> 0,
     and(?x,0) -> 0,
     and(0,?x) -> 0,
     and(?x,1) -> ?x,
     and(1,?x) -> ?x,
     and(?x,?x) -> ?x,
     xor(xor(?x,?y),?z) -> xor(?x,xor(?y,?z)),
     xor(?x,xor(?y,?z)) -> xor(?y,xor(?x,?z)),
     xor(?x,?y) -> xor(?y,?x),
     xor(?x,xor(?x,?y)) -> ?y,
     and(and(?x,?y),?z) -> and(?x,and(?y,?z)),
     and(?x,and(?y,?z)) -> and(?y,and(?x,?z)),
     and(?x,?y) -> and(?y,?x),
     and(?x,and(?x,?y)) -> and(?x,?y),
     xor(and(?x,?y),xor(?x,?z)) -> and(?x,xor(?y,?z)),
     xor(and(?x,?z),and(?y,?z)) -> and(xor(?x,?y),?z) ]
Check distinct normal forms in critical pair closure
convertible distinct normal forms: ?x = 0
problems/765.trs: Success(not UNC)
(8 msec.)