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(s(X)) -> f(X)
(2) g(cons(0,Y)) -> g(Y)
(3) g(cons(s(X),Y)) -> s(X)
(4) h(cons(X,Y)) -> h(g(cons(X,Y)))

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

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

[3]  Use following polynomial interpretation:
[s(x)] = x + 1
rest default

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

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

  thus obtaining new TRS:
(4a) h$0(cons$11(X,Y)) -> h$1(g$0(cons$11(X,Y)))
(4b) h$0(cons$10(X,Y)) -> h$1(g$0(cons$10(X,Y)))
(4c) h$0(cons$01(X,Y)) -> h$1(g$0(cons$01(X,Y)))
(4d) h$0(cons$00(X,Y)) -> h$1(g$0(cons$00(X,Y)))

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

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

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

../tpdb/TRS/nontermin/Rubio-inn/test830.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory