YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) g(A) -> A
(2) g(B) -> A
(3) g(B) -> B
(4) g(C) -> A
(5) g(C) -> B
(6) g(C) -> C
(7) foldf(x,nil) -> x
(8) foldf(x,cons(y,z)) -> f(foldf(x,z),y)
(9) f(t,x) -> f'(t,g(x))
(10) f'(triple`1(a,triple`2(b,c)),C) -> triple`1(a,triple`2(b,cons(C,c)))
(11) f'(triple`1(a,triple`2(b,c)),B) -> f(triple`1(a,triple`2(b,c)),A)
(12) f'(triple`1(a,triple`2(b,c)),A) -> f''(foldf(triple`1(cons(A,a),triple`2(nil,c)),b))
(13) f''(triple`1(a,triple`2(b,c))) -> foldf(triple`1(a,triple`2(b,nil)),c)

[2]  Use following polynomial interpretation:
[C] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(4)-(5)

[3]  Use following polynomial interpretation:
[B] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2), (11)

[4]  Label this TRS using following interpretation that is a model:
[B] = 1
rest default

  thus obtaining new TRS:
(1a) g$0(A) -> A
(3a) g$1(B) -> B
(6a) g$0(C) -> C
(7a) foldf$10(x,nil) -> x
(7b) foldf$00(x,nil) -> x
(8a) foldf$11(x,cons$11(y,z)) -> f$11(foldf$11(x,z),y)
(8b) foldf$11(x,cons$01(y,z)) -> f$10(foldf$11(x,z),y)
(8c) foldf$11(x,cons$10(y,z)) -> f$11(foldf$10(x,z),y)
(8d) foldf$10(x,cons$00(y,z)) -> f$10(foldf$10(x,z),y)
(8e) foldf$01(x,cons$11(y,z)) -> f$11(foldf$01(x,z),y)
(8f) foldf$01(x,cons$01(y,z)) -> f$10(foldf$01(x,z),y)
(8g) foldf$01(x,cons$10(y,z)) -> f$01(foldf$00(x,z),y)
(8h) foldf$00(x,cons$00(y,z)) -> f$00(foldf$00(x,z),y)
(9a) f$11(t,x) -> f'$11(t,g$1(x))
(9b) f$10(t,x) -> f'$10(t,g$0(x))
(9c) f$01(t,x) -> f'$01(t,g$1(x))
(9d) f$00(t,x) -> f'$00(t,g$0(x))
(10a) f'$10(triple`1$11(a,triple`2$11(b,c)),C) -> triple`1$11(a,triple`2$11(b,cons$01(C,c)))
(10b) f'$10(triple`1$11(a,triple`2$10(b,c)),C) -> triple`1$11(a,triple`2$10(b,cons$00(C,c)))
(10c) f'$10(triple`1$11(a,triple`2$01(b,c)),C) -> triple`1$11(a,triple`2$01(b,cons$01(C,c)))
(10d) f'$10(triple`1$10(a,triple`2$00(b,c)),C) -> triple`1$10(a,triple`2$00(b,cons$00(C,c)))
(10e) f'$10(triple`1$01(a,triple`2$11(b,c)),C) -> triple`1$01(a,triple`2$11(b,cons$01(C,c)))
(10f) f'$10(triple`1$01(a,triple`2$10(b,c)),C) -> triple`1$01(a,triple`2$10(b,cons$00(C,c)))
(10g) f'$10(triple`1$01(a,triple`2$01(b,c)),C) -> triple`1$01(a,triple`2$01(b,cons$01(C,c)))
(10h) f'$00(triple`1$00(a,triple`2$00(b,c)),C) -> triple`1$00(a,triple`2$00(b,cons$00(C,c)))
(12a) f'$10(triple`1$11(a,triple`2$11(b,c)),A) -> f''$1(foldf$11(triple`1$11(cons$01(A,a),triple`2$01(nil,c)),b))
(12b) f'$10(triple`1$11(a,triple`2$01(b,c)),A) -> f''$1(foldf$10(triple`1$11(cons$01(A,a),triple`2$01(nil,c)),b))
(12c) f'$10(triple`1$11(a,triple`2$10(b,c)),A) -> f''$1(foldf$11(triple`1$10(cons$01(A,a),triple`2$00(nil,c)),b))
(12d) f'$10(triple`1$10(a,triple`2$00(b,c)),A) -> f''$1(foldf$10(triple`1$10(cons$01(A,a),triple`2$00(nil,c)),b))
(12e) f'$10(triple`1$01(a,triple`2$11(b,c)),A) -> f''$1(foldf$11(triple`1$01(cons$00(A,a),triple`2$01(nil,c)),b))
(12f) f'$10(triple`1$01(a,triple`2$01(b,c)),A) -> f''$1(foldf$10(triple`1$01(cons$00(A,a),triple`2$01(nil,c)),b))
(12g) f'$10(triple`1$01(a,triple`2$10(b,c)),A) -> f''$1(foldf$01(triple`1$00(cons$00(A,a),triple`2$00(nil,c)),b))
(12h) f'$00(triple`1$00(a,triple`2$00(b,c)),A) -> f''$0(foldf$00(triple`1$00(cons$00(A,a),triple`2$00(nil,c)),b))
(13a) f''$1(triple`1$11(a,triple`2$11(b,c))) -> foldf$11(triple`1$11(a,triple`2$10(b,nil)),c)
(13b) f''$1(triple`1$11(a,triple`2$10(b,c))) -> foldf$10(triple`1$11(a,triple`2$10(b,nil)),c)
(13c) f''$1(triple`1$11(a,triple`2$01(b,c))) -> foldf$11(triple`1$10(a,triple`2$00(b,nil)),c)
(13d) f''$1(triple`1$10(a,triple`2$00(b,c))) -> foldf$10(triple`1$10(a,triple`2$00(b,nil)),c)
(13e) f''$1(triple`1$01(a,triple`2$11(b,c))) -> foldf$11(triple`1$01(a,triple`2$10(b,nil)),c)
(13f) f''$1(triple`1$01(a,triple`2$10(b,c))) -> foldf$10(triple`1$01(a,triple`2$10(b,nil)),c)
(13g) f''$1(triple`1$01(a,triple`2$01(b,c))) -> foldf$01(triple`1$00(a,triple`2$00(b,nil)),c)
(13h) f''$0(triple`1$00(a,triple`2$00(b,c))) -> foldf$00(triple`1$00(a,triple`2$00(b,nil)),c)

[5]  Use following polynomial interpretation:
[triple`1$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12g), (13g)

[6]  Use following polynomial interpretation:
[triple`1$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12c), (13c)

[7]  Use following polynomial interpretation:
[triple`2$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12a), (12e), (13a), (13e)

[8]  Use following polynomial interpretation:
[foldf$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8g)

[9]  Use following polynomial interpretation:
[f$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9c)

[10]  Use following polynomial interpretation:
[cons$10(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8c)

[11]  Use following polynomial interpretation:
[cons$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8a), (8e)

[12]  Use following polynomial interpretation:
[f$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9a)

[13]  Use following polynomial interpretation:
[g$1(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3a)

[14]  Unlabel this TRS to obtain the one consisting of the rules:
(1), (6)-(10), (12)-(13)

[15]  Label this TRS using following interpretation that is a model:
[A] = 1
rest default

  thus obtaining new TRS:
(1a) g$1(A) -> A
(6a) g$0(C) -> C
(7a) foldf$10(x,nil) -> x
(7b) foldf$00(x,nil) -> x
(8a) foldf$11(x,cons$11(y,z)) -> f$11(foldf$11(x,z),y)
(8b) foldf$11(x,cons$01(y,z)) -> f$10(foldf$11(x,z),y)
(8c) foldf$11(x,cons$10(y,z)) -> f$11(foldf$10(x,z),y)
(8d) foldf$10(x,cons$00(y,z)) -> f$10(foldf$10(x,z),y)
(8e) foldf$01(x,cons$11(y,z)) -> f$11(foldf$01(x,z),y)
(8f) foldf$01(x,cons$01(y,z)) -> f$10(foldf$01(x,z),y)
(8g) foldf$01(x,cons$10(y,z)) -> f$01(foldf$00(x,z),y)
(8h) foldf$00(x,cons$00(y,z)) -> f$00(foldf$00(x,z),y)
(9a) f$11(t,x) -> f'$11(t,g$1(x))
(9b) f$10(t,x) -> f'$10(t,g$0(x))
(9c) f$01(t,x) -> f'$01(t,g$1(x))
(9d) f$00(t,x) -> f'$00(t,g$0(x))
(10a) f'$10(triple`1$11(a,triple`2$11(b,c)),C) -> triple`1$11(a,triple`2$11(b,cons$01(C,c)))
(10b) f'$10(triple`1$11(a,triple`2$10(b,c)),C) -> triple`1$11(a,triple`2$10(b,cons$00(C,c)))
(10c) f'$10(triple`1$11(a,triple`2$01(b,c)),C) -> triple`1$11(a,triple`2$01(b,cons$01(C,c)))
(10d) f'$10(triple`1$10(a,triple`2$00(b,c)),C) -> triple`1$10(a,triple`2$00(b,cons$00(C,c)))
(10e) f'$10(triple`1$01(a,triple`2$11(b,c)),C) -> triple`1$01(a,triple`2$11(b,cons$01(C,c)))
(10f) f'$10(triple`1$01(a,triple`2$10(b,c)),C) -> triple`1$01(a,triple`2$10(b,cons$00(C,c)))
(10g) f'$10(triple`1$01(a,triple`2$01(b,c)),C) -> triple`1$01(a,triple`2$01(b,cons$01(C,c)))
(10h) f'$00(triple`1$00(a,triple`2$00(b,c)),C) -> triple`1$00(a,triple`2$00(b,cons$00(C,c)))
(12a) f'$11(triple`1$11(a,triple`2$11(b,c)),A) -> f''$1(foldf$11(triple`1$11(cons$11(A,a),triple`2$01(nil,c)),b))
(12b) f'$11(triple`1$11(a,triple`2$01(b,c)),A) -> f''$1(foldf$10(triple`1$11(cons$11(A,a),triple`2$01(nil,c)),b))
(12c) f'$11(triple`1$11(a,triple`2$10(b,c)),A) -> f''$1(foldf$11(triple`1$10(cons$11(A,a),triple`2$00(nil,c)),b))
(12d) f'$11(triple`1$10(a,triple`2$00(b,c)),A) -> f''$1(foldf$10(triple`1$10(cons$11(A,a),triple`2$00(nil,c)),b))
(12e) f'$11(triple`1$01(a,triple`2$11(b,c)),A) -> f''$1(foldf$11(triple`1$11(cons$10(A,a),triple`2$01(nil,c)),b))
(12f) f'$11(triple`1$01(a,triple`2$01(b,c)),A) -> f''$1(foldf$10(triple`1$11(cons$10(A,a),triple`2$01(nil,c)),b))
(12g) f'$11(triple`1$01(a,triple`2$10(b,c)),A) -> f''$1(foldf$11(triple`1$10(cons$10(A,a),triple`2$00(nil,c)),b))
(12h) f'$01(triple`1$00(a,triple`2$00(b,c)),A) -> f''$1(foldf$10(triple`1$10(cons$10(A,a),triple`2$00(nil,c)),b))
(13a) f''$1(triple`1$11(a,triple`2$11(b,c))) -> foldf$11(triple`1$11(a,triple`2$10(b,nil)),c)
(13b) f''$1(triple`1$11(a,triple`2$10(b,c))) -> foldf$10(triple`1$11(a,triple`2$10(b,nil)),c)
(13c) f''$1(triple`1$11(a,triple`2$01(b,c))) -> foldf$11(triple`1$10(a,triple`2$00(b,nil)),c)
(13d) f''$1(triple`1$10(a,triple`2$00(b,c))) -> foldf$10(triple`1$10(a,triple`2$00(b,nil)),c)
(13e) f''$1(triple`1$01(a,triple`2$11(b,c))) -> foldf$11(triple`1$01(a,triple`2$10(b,nil)),c)
(13f) f''$1(triple`1$01(a,triple`2$10(b,c))) -> foldf$10(triple`1$01(a,triple`2$10(b,nil)),c)
(13g) f''$1(triple`1$01(a,triple`2$01(b,c))) -> foldf$01(triple`1$00(a,triple`2$00(b,nil)),c)
(13h) f''$0(triple`1$00(a,triple`2$00(b,c))) -> foldf$00(triple`1$00(a,triple`2$00(b,nil)),c)

[16]  Use following polynomial interpretation:
[f''$0(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(13h)

[17]  Use following polynomial interpretation:
[triple`1$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12e)-(12g), (13g)

[18]  Use following polynomial interpretation:
[triple`1$00(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12h)

[19]  Use following polynomial interpretation:
[triple`1$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12c), (13c)

[20]  Use following polynomial interpretation:
[triple`2$11(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(12a), (13a), (13e)

[21]  Use following polynomial interpretation:
[foldf$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8g)

[22]  Use following polynomial interpretation:
[f$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(9c)

[23]  Use following polynomial interpretation:
[cons$10(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8c)

[24]  Use following polynomial interpretation:
[foldf$00(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7b)

[25]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
f'$11 > nil
f''$1 > nil
f$00 > g$0
f$00 > f'$00
foldf$00 > f$00
f$10 > g$0
f$10 > f'$10
foldf$01 > f$10
foldf$10 > f$10
foldf$11 > f$10
f$11 > g$1
f$11 > f'$11
foldf$01 > f$11
foldf$11 > f$11
f'$00 > cons$00
f'$00 > triple`2$00
f'$00 > triple`1$00
f'$10 > cons$00
f'$10 > cons$01
f'$10 > triple`2$00
f'$10 > triple`2$01
f'$10 > triple`2$10
f'$10 > triple`2$11
f'$10 > triple`1$01
f'$10 > triple`1$10
f'$10 > triple`1$11
f'$11 > cons$11
f'$11 > f''$1
f'$11 > triple`2$00
f'$11 > triple`2$01
f'$11 > triple`1$10
f'$11 > triple`1$11
f'$11 > foldf$10
f''$1 > triple`2$00
f''$1 > triple`2$10
f''$1 > triple`1$01
f''$1 > triple`1$10
f''$1 > triple`1$11
f''$1 > foldf$10


../tpdb/TRS/Cime/filliatre.trs, 0.02, Y
Couldn't open file <60>: 60: No such file or directory