YES
(ignored inputs)COMMENT cops number: 406
Conditional Rewrite Rules:
   [ f(?x,?y) -> g(?x) | c(g(?x)) == c(a),
     f(?x,?y) -> h(?x) | c(h(?x)) == c(a),
     g(s(?x)) -> ?x,
     h(s(?x)) -> ?x ]
Check whether all rules are type 3
OK
Check whether the input is deterministic
OK
Result of unraveling:
   [ f(?x,?x_1) -> U1(c(g(?x)),?x,?x_1),
     U1(c(a),?x,?x_1) -> g(?x),
     f(?x,?x_1) -> U1(c(h(?x)),?x,?x_1),
     U1(c(a),?x,?x_1) -> h(?x),
     g(s(?x)) -> ?x,
     h(s(?x)) -> ?x ]
Check whether U(R) is terminating
OK
Check whether the input is weakly left-linear
OK
Check whether U(R) is confluent
U(R) is not confluent
Conditional critical pairs (CCPs):
   [ h(?x_1) = g(?x_1) | c(h(?x_1)) == c(a),c(g(?x_1)) == c(a),
     g(?x) = h(?x) | c(g(?x)) == c(a),c(h(?x)) == c(a) ]
Check whether the input is almost orthogonale
not almost orthogonal
OK
Check whether the input is absolutely irreducible
OK
Check whether all CCPs are joinable
OK
cops-iziLJiQG.trs: Success(CR)
(1 msec.)