SUCCESS
0.52 (total time)

COMPLETED TRS
*(fac(0), fac(0)) -> fac(fac(0))
*(*(s(y), s(y)), fac(+(*(s(y), y), y))) -> fac(*(s(y), s(y)))
*(s(x), fac(x)) -> fac(s(x))
*(0, s(y)) -> *(0, y)
*(x, 0) -> 0
s(0) -> fac(0)
s(+(*(s(y), y), y)) -> *(s(y), s(y))
+(*(x, y), x) -> *(x, s(y))
+(x, s(y)) -> s(+(x, y))
+(x, 0) -> x