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) +(x,0) -> x
(2) +(0,x) -> x
(3) +(s(x),s(y)) -> s(s(+(x,y)))
(4) +(+(x,y),z) -> +(x,+(y,z))
(5) *(x,0) -> 0
(6) *(0,x) -> 0
(7) *(s(x),s(y)) -> s(+(*(x,y),+(x,y)))
(8) *(*(x,y),z) -> *(x,*(y,z))
(9) app(nil,l) -> l
(10) app(cons(x,l1),l2) -> cons(x,app(l1,l2))
(11) sum(nil) -> 0
(12) sum(cons(x,l)) -> +(x,sum(l))
(13) sum(app(l1,l2)) -> +(sum(l1),sum(l2))
(14) prod(nil) -> s(0)
(15) prod(cons(x,l)) -> *(x,prod(l))
(16) prod(app(l1,l2)) -> *(prod(l1),prod(l2))

[2]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: +: Lex-LR, *: Lex-LR, 
Precedence:
+ > s
* > +
sum > +
sum > 0
prod > 0
* > s
prod > s
prod > *
app > cons


../tpdb/TRS/Cime/list-sum-prod-assoc-append.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory