SUCCESS
508.24 (total time)


COMPLETED TRS


             g(x) -> *(f(x), x),
    *(f(f(x)), y) -> *(x, y),
   *(f(one()), x) -> x,
 *(f(*(x, y)), z) -> *(f(y), *(f(x), z)),
 *(f(x), *(x, y)) -> y,
      *(one(), x) -> x,
    *(*(x, y), z) -> *(x, *(y, z)),
 *(x, *(f(x), y)) -> y



STATISTICS

number of inference steps: 140

total time:   508.24
orient:       285.52
rewrite:      187.06
deduce:       23.06
termination:  279.71

external termination prover: ttt2fast
calls to termination prover: 658 (yes: 508, timeouts: 0)
timelimit per call:          1.0