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

[2]  Label this TRS using following interpretation that is a quasi-model:
[f(x,y)] = 0
[a] = 1
[g(x)] = 0
[h(x)] = 1
rest default

  thus obtaining new TRS:
(1a) f$11(a,x) -> f$01(g$1(x),x)
(1b) f$10(a,x) -> f$00(g$0(x),x)
(2a) h$0(g$1(x)) -> h$1(a)
(2b) h$0(g$0(x)) -> h$1(a)
(3a) g$1(h$1(x)) -> g$1(x)
(3b) g$1(h$0(x)) -> g$0(x)
(4a) h$1(h$1(x)) -> x
(4b) h$1(h$0(x)) -> x
(D1) f$10(x,y) ->= f$00(x,y)
(D2) f$11(x,y) ->= f$01(x,y)
(D3) f$11(x,y) ->= f$10(x,y)
(D4) f$01(x,y) ->= f$00(x,y)
(D5) g$1(x) ->= g$0(x)
(D6) h$1(x) ->= h$0(x)

[3]  Use following polynomial interpretation:
[f$10(x,y)] = xy
[f$11(x,y)] = xy
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1a)-(1b), (D1)-(D2)

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

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

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

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

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

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

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