YES
Input TRS:
    1: f(k(z),a()) -> g(x,x) | h(z) --> x | x --> b()
    2: f(k(a()),h(a())) -> k(x) | a() --> x
    3: k(x) -> h(x)
    4: k(x) -> b()
    5: k(x) -> a()
    6: a() -> b()
    7: g(x,x) -> a()
Infeasibility test:
    f(x,y) --> g(z,z)
Co-Order(NegReal,≥,Sum) ... succeeded.
     a()	weight: (- (/ 1 2))
     h(x1)	weight: (- (/ 3 2))
     b()	weight: (- (/ 1 2))
     k(x1)	weight: (- (/ 1 2))
     f(x1,x2)	weight: (- (/ 1 2))
    #(x1)	weight: x1
     g(x1,x2)	weight: 0