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) f(f(x)) -> f(c(f(x)))
(2) f(f(x)) -> f(d(f(x)))
(3) g(c(x)) -> x
(4) g(d(x)) -> x
(5) g(c(0)) -> g(d(1))
(6) g(c(1)) -> g(d(0))

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

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

[3]  Label this TRS using following interpretation that is a model:
[f(x)] = 0
[c(x)] = 0
[d(x)] = 0
[g(x)] = 0
[1] = 1
rest default

  thus obtaining new TRS:
(1a) f$0(f$1(x)) -> f$0(c$0(f$1(x)))
(1b) f$0(f$0(x)) -> f$0(c$0(f$0(x)))
(2a) f$0(f$1(x)) -> f$0(d$0(f$1(x)))
(2b) f$0(f$0(x)) -> f$0(d$0(f$0(x)))
(5a) g$0(c$0(0)) -> g$0(d$1(1))
(6a) g$0(c$1(1)) -> g$0(d$0(0))

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

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

[5]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (5)

[6]  Use following polynomial interpretation:
[0] = 3
rest default

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

[7]  Label this TRS using following interpretation over N\{0,1}:
[f(x)] = 3
[d(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1) f{3}(f{i}(x)) -> f{3}(c{3}(f{i}(x)))
(2) f{3}(f{i}(x)) -> f{2}(d{3}(f{i}(x)))

[8]  Use following polynomial interpretation:
[f_{i}(x)] = x + i
[c_{i}(x)] = x
[d_{i}(x)] = x
rest default

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

[9]  Unlabel this TRS to obtain the one consisting of the rules:
(1)

[10]  Label this TRS using following interpretation over N\{0,1}:
[f(x)] = 3
[c(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1) f{3}(f{i}(x)) -> f{2}(c{3}(f{i}(x)))

[11]  Use following polynomial interpretation:
[f_{i}(x)] = x + i
[c_{i}(x)] = x
rest default

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

[12]  Since there are no remaining rules, termination is proved!

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