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) app(g,app(h,app(g,x))) -> app(g,x)
(2) app(g,app(g,x)) -> app(g,app(h,app(g,x)))
(3) app(h,app(h,x)) -> app(h,app(app(f,app(h,x)),x))

[2]  Apply uncurrying transformation with <app> as function application symbol to obtain the following TRS:
(1) g(h(g(x))) -> g(x)
(2) g(g(x)) -> g(h(g(x)))
(3) h(h(x)) -> h(f(h(x),x))

[3]  Eliminate dummy symbol <f>, to obtain the following TRS:
(1) g(h(g(x))) -> g(x)
(2) g(g(x)) -> g(h(g(x)))
(3a) h(h(x)) -> h(#0)
(3b) h(h(x)) -> #1(h(x))
(3c) h(h(x)) -> #2(x)

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

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

[5]  Label this TRS using following interpretation over N\{0,1}:
[g(x)] = 3
[h(x)] = 2
[#2(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(2) g{3}(g{i}(x)) -> g{2}(h{3}(g{i}(x)))
(3a) h{2}(h{i}(x)) -> h{2}(#0)
(3b) h{2}(h{i}(x)) -> #1{2}(h{i}(x))
(3c) h{2}(h{i}(x)) -> #2{i}(x)

[6]  Use following polynomial interpretation:
[g_{i}(x)] = x + i
[h_{i}(x)] = x
[#1_{i}(x)] = x
[#2_{i}(x)] = x
rest default

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

[7]  Unlabel this TRS to obtain the one consisting of the rules:
(3), (3), (3)

[8]  Use following polynomial interpretation:
[h(x)] = x + 1
rest default

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

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

../tpdb/TRS/currying/Ste92/motivation.trs, 0., Y
Couldn't open file <60>: 60: No such file or directory