YES
Input TRS:
    1: +(0(),x) -> x
    2: +(s(x),y) -> s(+(x,y))
Infeasibility test:
    +(x,a()) --> 0()
Co-Order(NegReal,≥,Sum) ... succeeded.
     a()	weight: -1
     s(x1)	weight: x1
     0()	weight: (- (/ 1 2))
    #(x1)	weight: x1
     +(x1,x2)	weight: x2