SUCCESS
90.97 (total time)


COMPLETED TRS


                *(x, y) -> d(x, i(y)),
                i(i(x)) -> x,
               i(one()) -> one(),
             i(d(x, y)) -> d(y, x),
 d(i(x), d(y, d(x, z))) -> d(i(z), y),
       d(i(y), d(x, y)) -> i(x),
            d(one(), x) -> i(x),
          d(d(x, y), z) -> d(x, d(z, i(y))),
 d(z, d(y, d(i(z), x))) -> d(i(x), y),
            d(x, one()) -> x,
                d(x, x) -> one(),
       d(y, d(x, i(y))) -> i(x)


STATISTICS

number of inference steps: 29

total time:   90.97
orient:       89.64
rewrite:      1.06
deduce:       0.25
termination:  89.56

external termination prover: aprove07
calls to termination prover: 53 (yes: 43, timeouts: 0)
time limit per call:         5.0