YES
Input TRS:
    1: gcd(add(x,y),y) -> gcd(x,y)
    2: gcd(y,add(x,y)) -> gcd(x,y)
    3: gcd(x,0()) -> x
    4: gcd(0(),x) -> x
    5: gcd(x,y) -> gcd(y,x) | leq(y,x) --> false()
    6: add(0(),y) -> y
    7: add(s(x),y) -> s(add(x,y))
Infeasibility test:
    leq(x2,0()) --> false()
Symbol transition graph:
    add	-->  # 0 add false gcd leq s
    gcd	-->  # 0 add false gcd leq s
  Collapsable symbols: { gcd gcd add }