YES
Input TRS:
    1: f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) --> c(a(b()))
    2: f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) --> c(a(a(b())))
    3: a(x) -> b()
    4: a(x) -> f(x,x)
Infeasibility test:
    c(f(c(c(x1)),y)) --> c(a(b()))
    c(f(c(x1),c(c(c(c(y)))))) --> c(a(a(b())))
Co-Order(NegReal,≥,Sum) ... succeeded.
     a(x1)	weight: (- (/ 105935 4))
     b()	weight: (- (/ 105935 4))
     c(x1)	weight: -151974 + x1
     f(x1,x2)	weight: (- (/ 390735 2)) + x1
    #(x1,x2)	weight: x1