NO
(ignored inputs)COMMENT COMMENT cops number: 1097 submitted by: Kiraku Shintani
Rewrite Rules (1):
   [ c(a(?x)) -> c(c(?x)),
     c(c(?x)) -> a(b(?x)),
     a(a(?x)) -> b(c(?x)),
     b(a(?x)) -> c(c(?x)),
     c(a(?x)) -> b(a(?x)),
     b(c(?x)) -> a(b(?x)),
     c(c(?x)) -> a(b(?x)),
     b(c(?x)) -> c(a(?x)) ]
Rewrite Rules (2):
   [ c(b(?x)) -> c(a(?x)),
     b(c(?x)) -> c(b(?x)),
     a(b(?x)) -> c(c(?x)),
     a(a(?x)) -> a(b(?x)),
     a(c(?x)) -> a(a(?x)),
     c(c(?x)) -> a(a(?x)),
     a(a(?x)) -> b(c(?x)),
     b(b(?x)) -> c(b(?x)) ]
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: <c(c(a(?x))), a(b(b(?x)))>
check candidate: <b(c(a(?x))), a(b(b(?x)))>
check candidate: <c(c(a(?x))), a(b(b(?x)))>
check candidate: <b(c(a(?x))), c(a(b(?x)))>
check candidate: <c(b(?x)), a(b(?x))>
check candidate: <c(b(?x)), c(a(?x))>
Counter example: c(b(?x)) <-R2- b(c(?x)) -R1-> c(a(?x))

result: not COM
cops-BspABou6.trs: Success(not COM)
(3 msec.)