SUCCESS
46.45 (total time)


COMPLETED TRS


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



STATISTICS

number of inference steps: 92

total time:   46.45
orient:       20.76
rewrite:      22.25
deduce:       3.25
termination:  20.30

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