EQUATIONS: 
plus(x,0()) = x
plus(x,s(y())) = s(plus(x,y()))
times(x,0()) = 0()
times(x,s(y())) = plus(times(x,y()),x)
fac(0()) = s(0())
fac(s(x)) = times(s(x),fac(x))

COMPLETE TRS:
RULES:
plus(x,0()) -> x
times(x,0()) -> 0()
fac(0()) -> s(0())
times(s(s(0())),times(s(0()),s(0()))) -> fac(s(s(0())))
times(times(s(y()),s(y())),fac(plus(times(s(y()),y()),y()))) ->
  fac(times(s(y()),s(y())))
times(plus(x,s(y())),fac(plus(x,y()))) -> fac(plus(x,s(y())))
s(plus(x,y())) -> plus(x,s(y()))
plus(times(x,y()),x) -> times(x,s(y()))
times(s(x),fac(x)) -> fac(s(x))
times(0(),s(y())) -> times(0(),y())
fac(s(0())) -> times(s(0()),s(0()))
plus(times(y(),y()),s(y())) -> s(times(y(),s(y())))

SUCCESS
MaxTRS: 2 
Search time: 0.06 seconds