YES
(VAR x y z t a b c)
(RULES 
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x,nil) -> x
foldf(x,cons(y,z)) -> f(foldf(x,z),y)
f(t,x) -> f'(t,g(x))
f'(triple(a,b,c),C) -> triple(a,b,cons(C,c))
f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b))
f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c)
)

Proving termination of rewriting for filliatre:

-> Dependency pairs:
nF_foldf(x,cons(y,z)) -> nF_f(foldf(x,z),y)
nF_foldf(x,cons(y,z)) -> nF_foldf(x,z)
nF_f(t,x) -> nF_f'(t,g(x))
nF_f(t,x) -> nF_g(x)
nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A)
nF_f'(triple(a,b,c),A) -> nF_f''(foldf(triple(cons(A,a),nil,c),b))
nF_f'(triple(a,b,c),A) -> nF_foldf(triple(cons(A,a),nil,c),b)
nF_f''(triple(a,b,c)) -> nF_foldf(triple(a,b,nil),c)

-> Proof of termination for filliatre_1:
-> -> Dependency pairs in cycle:
nF_foldf(x,cons(y,z)) -> nF_f(foldf(x,z),y)
nF_f''(triple(a,b,c)) -> nF_foldf(triple(a,b,nil),c)
nF_f'(triple(a,b,c),A) -> nF_f''(foldf(triple(cons(A,a),nil,c),b))
nF_f(t,x) -> nF_f'(t,g(x))
nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A)
nF_f'(triple(a,b,c),A) -> nF_foldf(triple(cons(A,a),nil,c),b)
nF_foldf(x,cons(y,z)) -> nF_foldf(x,z)

UsableRules:
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x,nil) -> x
foldf(x,cons(y,z)) -> f(foldf(x,z),y)
f(t,x) -> f'(t,g(x))
f'(triple(a,b,c),C) -> triple(a,b,cons(C,c))
f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b))
f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c)

Polynomial Interpretation:

[g](X) = 0
[A] = 0
[B] = 0
[C] = 0
[foldf](X1,X2) = X1 + X2
[nil] = 0
[cons](X1,X2) = X2 + 1
[f](X1,X2) = X1 + 1
[f'](X1,X2) = X1 + 1
[triple](X1,X2,X3) = X1 + X2 + X3 + 1
[f''](X) = X
[nF_foldf](X1,X2) = X1 + X2
[nF_f''](X) = X
[nF_f'](X1,X2) = X1 + 1
[nF_f](X1,X2) = X1 + 1

TIME: 7.9343e-2

-> -> Dependency pairs in cycle:
nF_foldf(x,cons(y,z)) -> nF_f(foldf(x,z),y)
nF_f'(triple(a,b,c),A) -> nF_foldf(triple(cons(A,a),nil,c),b)
nF_f(t,x) -> nF_f'(t,g(x))
nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A)
nF_f''(triple(a,b,c)) -> nF_foldf(triple(a,b,nil),c)
nF_f'(triple(a,b,c),A) -> nF_f''(foldf(triple(cons(A,a),nil,c),b))

UsableRules:
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x,nil) -> x
foldf(x,cons(y,z)) -> f(foldf(x,z),y)
f(t,x) -> f'(t,g(x))
f'(triple(a,b,c),C) -> triple(a,b,cons(C,c))
f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b))
f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c)

Polynomial Interpretation:

[g](X) = X
[A] = 1
[B] = 1
[C] = 1
[foldf](X1,X2) = X1 + X2
[nil] = 0
[cons](X1,X2) = X1 + X2
[f](X1,X2) = X1 + X2
[f'](X1,X2) = X1 + X2
[triple](X1,X2,X3) = X2 + X3
[f''](X) = X
[nF_foldf](X1,X2) = X1 + X2
[nF_f'](X1,X2) = X1 + X2
[nF_f](X1,X2) = X1 + X2
[nF_f''](X) = X

TIME: 8.1994e-2

-> -> Dependency pairs in cycle:
nF_foldf(x,cons(y,z)) -> nF_f(foldf(x,z),y)
nF_f'(triple(a,b,c),A) -> nF_foldf(triple(cons(A,a),nil,c),b)
nF_f(t,x) -> nF_f'(t,g(x))
nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A)

UsableRules:
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x,nil) -> x
foldf(x,cons(y,z)) -> f(foldf(x,z),y)
f(t,x) -> f'(t,g(x))
f'(triple(a,b,c),C) -> triple(a,b,cons(C,c))
f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b))
f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c)

Polynomial Interpretation:

[g](X) = X
[A] = 0
[B] = 1
[C] = 1
[foldf](X1,X2) = X1
[nil] = 0
[cons](X1,X2) = X1
[f](X1,X2) = X1
[f'](X1,X2) = X1
[triple](X1,X2,X3) = X2
[f''](X) = X
[nF_foldf](X1,X2) = X1 + X2
[nF_f'](X1,X2) = X1 + X2
[nF_f](X1,X2) = X1 + X2

TIME: 6.936600000000004e-2

-> -> Dependency pairs in cycle:
nF_foldf(x,cons(y,z)) -> nF_f(foldf(x,z),y)
nF_f'(triple(a,b,c),A) -> nF_foldf(triple(cons(A,a),nil,c),b)
nF_f(t,x) -> nF_f'(t,g(x))

UsableRules:
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x,nil) -> x
foldf(x,cons(y,z)) -> f(foldf(x,z),y)
f(t,x) -> f'(t,g(x))
f'(triple(a,b,c),C) -> triple(a,b,cons(C,c))
f'(triple(a,b,c),B) -> f(triple(a,b,c),A)
f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b))
f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c)

Polynomial Interpretation:

[g](X) = 0
[A] = 0
[B] = 0
[C] = 0
[foldf](X1,X2) = X1 + X2
[nil] = 0
[cons](X1,X2) = X2 + 1
[f](X1,X2) = X1 + 1
[f'](X1,X2) = X1 + 1
[triple](X1,X2,X3) = X2 + X3 + 1
[f''](X) = X
[nF_foldf](X1,X2) = X1 + X2
[nF_f'](X1,X2) = X1
[nF_f](X1,X2) = X1 + 1

TIME: 6.3434e-2


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



Termination was proved succesfully.