MAYBE
Input TRS:
    1: gcd(z,y) -> gcd(x,y) | iadd(z) --> tp2(x,y)
    2: gcd(y,z) -> gcd(x,y) | iadd(z) --> tp2(x,y)
    3: gcd(x,0()) -> x
    4: gcd(0(),x) -> x
    5: iadd(y) -> tp2(0(),y)
    6: iadd(s(z)) -> tp2(s(x),y) | iadd(z) --> tp2(x,y)
    7: iadd(add(x,y)) -> tp2(x,y)
Infeasibility test:
    iadd(x1) --> tp2(x2,x3)
Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.