NO
(ignored inputs)COMMENT doi:10.1145/322248.322251 cops number: 78 submitted by: Takahito Aoto , Junichi Yoshida , Yoshihito Toyama [22] Example 12.4 with typo; fixed as Cops #109
input TRS:
   [ join : 2,
     meet : 2,
     joint : 2 ]
   [ join(?x,meet(?x,?y)) -> ?x,
     meet(?x,joint(?y,?z)) -> join(meet(?x,?y),meet(?x,?z)),
     meet(?x,?x) -> ?x,
     join(?x,?x) -> ?x,
     meet(meet(?x,?y),?z) -> meet(?x,meet(?y,?z)),
     meet(?x,?y) -> meet(?y,?x),
     join(join(?x,?y),?z) -> join(?x,join(?y,?z)),
     join(?x,?y) -> join(?y,?x) ]
unknown Strongly Non-Overlapping
unknown Right-Reducible
Check distinct normal forms in critical pair closure
distinct normal forms of a term: ?z = joint(?z,?z)
cops-DKt52Uaz.trs: Success(not UNR)
(13 msec.)