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) plus(x,0) -> x
(2) plus(x,s(y)) -> s(plus(x,y))
(3) times(0,y) -> 0
(4) times(x,0) -> 0
(5) times(s(x),y) -> plus(times(x,y),y)
(6) p(s(s(x))) -> s(p(s(x)))
(7) p(s(0)) -> 0
(8) fac(s(x)) -> times(fac(p(s(x))),s(x))

[2]  Label this TRS using following interpretation over N\{0,1}:
[s(x)] = x + 1
[times(x,y)] = (x-2)*(y-2) + 2
[p(x)] = max(2, x - 1)
[fac(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1) plus{i,2}(x,0) -> x
(2) plus{i,j + 1}(x,s{j}(y)) -> s{j + i - 2}(plus{i,j}(x,y))
(3) times{2,j}(0,y) -> 0
(4) times{i,2}(x,0) -> 0
(5) times{i + 1,j}(s{i}(x),y) -> plus{6 + i*j - 2j - 2i,j}(times{i,j}(x,y),y)
(6) p{2 + i}(s{i + 1}(s{i}(x))) -> s{i}(p{i + 1}(s{i}(x)))
(7) p{3}(s{2}(0)) -> 0
(8) fac{i + 1}(s{i}(x)) -> times{2,i + 1}(fac{i}(p{i + 1}(s{i}(x))),s{i}(x))

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: plus: Lex-LR, times: Lex-LR, 
Precedence:
plus{i,j} = plus{k,l} for all i, j, k, l
plus{i,j} > s{k} for all i, j, k
times{i,j} > plus{k,l} for all i, j, k, l
p{i} > s{k} for all i, k
times{i,j} = times{k,l} for all i, j, k, l
fac{i} > times{k,l} for all i, k, l
p{i} = p{k} for all i, k
fac{i} > p{k} for all i, k
fac{i} > fac{k} for i > k


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