YES
(VAR x y z)
(RULES 
min(x,0) -> 0
min(0,y) -> 0
min(s(x),s(y)) -> s(min(x,y))
max(x,0) -> x
max(0,y) -> y
max(s(x),s(y)) -> s(max(x,y))
-(x,0) -> x
-(s(x),s(y)) -> -(x,y)
gcd(s(x),s(y),z) -> gcd(-(max(x,y),min(x,y)),s(min(x,y)),z)
gcd(x,s(y),s(z)) -> gcd(x,-(max(y,z),min(y,z)),s(min(y,z)))
gcd(s(x),y,s(z)) -> gcd(-(max(x,z),min(x,z)),y,s(min(x,z)))
gcd(x,0,0) -> x
gcd(0,y,0) -> y
gcd(0,0,z) -> z
)

Proving termination of rewriting for gcd_triple:

-> Dependency pairs:
nF_min(s(x),s(y)) -> nF_min(x,y)
nF_max(s(x),s(y)) -> nF_max(x,y)
nF_-(s(x),s(y)) -> nF_-(x,y)
nF_gcd(s(x),s(y),z) -> nF_gcd(-(max(x,y),min(x,y)),s(min(x,y)),z)
nF_gcd(s(x),s(y),z) -> nF_-(max(x,y),min(x,y))
nF_gcd(s(x),s(y),z) -> nF_max(x,y)
nF_gcd(s(x),s(y),z) -> nF_min(x,y)
nF_gcd(x,s(y),s(z)) -> nF_gcd(x,-(max(y,z),min(y,z)),s(min(y,z)))
nF_gcd(x,s(y),s(z)) -> nF_-(max(y,z),min(y,z))
nF_gcd(x,s(y),s(z)) -> nF_max(y,z)
nF_gcd(x,s(y),s(z)) -> nF_min(y,z)
nF_gcd(s(x),y,s(z)) -> nF_gcd(-(max(x,z),min(x,z)),y,s(min(x,z)))
nF_gcd(s(x),y,s(z)) -> nF_-(max(x,z),min(x,z))
nF_gcd(s(x),y,s(z)) -> nF_max(x,z)
nF_gcd(s(x),y,s(z)) -> nF_min(x,z)

-> Proof of termination for gcd_triple_1_1:
-> -> Dependency pairs in cycle:
nF_gcd(s(x),s(y),z) -> nF_gcd(-(max(x,y),min(x,y)),s(min(x,y)),z)
nF_gcd(s(x),y,s(z)) -> nF_gcd(-(max(x,z),min(x,z)),y,s(min(x,z)))
nF_gcd(x,s(y),s(z)) -> nF_gcd(x,-(max(y,z),min(y,z)),s(min(y,z)))

UsableRules:
min(x,0) -> 0
min(0,y) -> 0
min(s(x),s(y)) -> s(min(x,y))
max(x,0) -> x
max(0,y) -> y
max(s(x),s(y)) -> s(max(x,y))
-(x,0) -> x
-(s(x),s(y)) -> -(x,y)

Polynomial Interpretation:

[min](X1,X2) = 1/2.X1 + 1/2.X2
[0] = 0
[s](X) = 2.X + 2
[max](X1,X2) = X1 + X2
[-](X1,X2) = X1
[gcd](X1,X2,X3) = 0
[nF_gcd](X1,X2,X3) = 2.X1 + 2.X2 + 2.X3

TIME: 5.506e-3

-> -> Dependency pairs in cycle:
nF_gcd(s(x),s(y),z) -> nF_gcd(-(max(x,y),min(x,y)),s(min(x,y)),z)
nF_gcd(s(x),y,s(z)) -> nF_gcd(-(max(x,z),min(x,z)),y,s(min(x,z)))

UsableRules:
min(x,0) -> 0
min(0,y) -> 0
min(s(x),s(y)) -> s(min(x,y))
max(x,0) -> x
max(0,y) -> y
max(s(x),s(y)) -> s(max(x,y))
-(x,0) -> x
-(s(x),s(y)) -> -(x,y)

Polynomial Interpretation:

[min](X1,X2) = X1
[0] = 0
[s](X) = 2.X + 2
[max](X1,X2) = X1 + X2
[-](X1,X2) = X1
[gcd](X1,X2,X3) = 0
[nF_gcd](X1,X2,X3) = 2.X1 + X2 + X3

TIME: 5.924e-3

-> -> Dependency pairs in cycle:
nF_gcd(s(x),s(y),z) -> nF_gcd(-(max(x,y),min(x,y)),s(min(x,y)),z)

UsableRules:
min(x,0) -> 0
min(0,y) -> 0
min(s(x),s(y)) -> s(min(x,y))
max(x,0) -> x
max(0,y) -> y
max(s(x),s(y)) -> s(max(x,y))
-(x,0) -> x
-(s(x),s(y)) -> -(x,y)

Polynomial Interpretation:

[min](X1,X2) = X1
[0] = 0
[s](X) = 2.X + 2
[max](X1,X2) = X1 + X2
[-](X1,X2) = X1
[gcd](X1,X2,X3) = 0
[nF_gcd](X1,X2,X3) = 2.X1 + X2

TIME: 4.261e-3


-> Proof of termination for gcd_triple_1_2:
-> -> Dependency pairs in cycle:
nF_-(s(x),s(y)) -> nF_-(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for gcd_triple_1_3:
-> -> Dependency pairs in cycle:
nF_max(s(x),s(y)) -> nF_max(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for gcd_triple_1_4:
-> -> Dependency pairs in cycle:
nF_min(s(x),s(y)) -> nF_min(x,y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.