0.00/0.02 NO 0.00/0.02 (ignored inputs)COMMENT COPS 10 700 COMMENT submitted by: Kiraku Shintani 0.00/0.02 Rewrite Rules (1): 0.00/0.02 [ f(g(f(?x))) -> ?x, 0.00/0.02 f(g(?x)) -> g(f(?x)) ] 0.00/0.02 Rewrite Rules (2): 0.00/0.02 [ a -> a, 0.00/0.02 f(h(a,a)) -> f(b), 0.00/0.02 c -> b ] 0.00/0.02 both left-linear 0.00/0.02 check commutation with R1 := (1), R2 := (2) 0.00/0.02 check CPs are development closed... 0.00/0.02 ...failed 0.00/0.02 check commutation with R1 := (2), R2 := (1) 0.00/0.02 check CPs are development closed... 0.00/0.02 ...failed 0.00/0.02 check non-commutation 0.00/0.02 check with R1 := (1), R2 := (2) 0.00/0.02 check counter example from CPs... 0.00/0.02 check candidate: 0.00/0.02 Counter example: f(g(f(b))) <-R2- f(g(f(h(a,a)))) -R1-> h(a,a) 0.00/0.02 0.00/0.02 result: not COM 0.00/0.02 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not COM) 0.00/0.02 (0 msec.) 0.00/0.02 EOF