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) sum(nil) -> 0
(10) sum(cons(x,l)) -> +(x,sum(l))
(11) prod(nil) -> s(0)
(12) prod(cons(x,l)) -> *(x,prod(l))

[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 > *


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