NO
(ignored inputs)COMMENT COMMENT cops number: 1052 submitted by: Kiraku Shintani
Rewrite Rules (1):
   [ f(a,b) -> c,
     a -> a',
     b -> b',
     c -> f(a',b),
     c -> f(a,b'),
     c -> f(a,b) ]
Rewrite Rules (2):
   [ a -> b,
     a -> c,
     a -> e,
     b -> d,
     c -> a,
     d -> a,
     d -> e,
     g(?x) -> h(a),
     h(?x) -> e ]
both left-linear
check commutation with R1 := (1), R2 := (2)
check CPs are development closed...
...failed
check commutation with R1 := (2), R2 := (1)
check CPs are development closed...
...failed
check non-commutation
check with R1 := (1), R2 := (2)
check counter example from CPs...
check candidate: <f(b,b), c>
Counter example: f(b,b) <-R2- f(a,b) -R1-> c

result: not COM
cops-08MYPbeR.trs: Success(not COM)
(1 msec.)