SUCCESS
6135.95 (total time)


COMPLETED TRS

 
    trans(x, trans(i(x), y)) -> y,
             trans(x, one()) -> x,
              trans(x, i(x)) -> one(),
       trans(trans(x, y), z) -> trans(x, trans(y, z)),
             trans(one(), x) -> x,
              trans(i(x), x) -> one(),
    trans(i(x), trans(x, y)) -> y,
 trans(f(x), trans(f(y), z)) -> trans(f(trans(x, y)), z),
           trans(f(x), f(y)) -> f(trans(x, y)),
 trans(f(y), trans(g(x), z)) -> trans(g(x), trans(f(y), z)),
 trans(f(y), trans(h(x), z)) -> trans(h(x), trans(f(y), z)),
           trans(f(y), g(x)) -> trans(g(x), f(y)),
           trans(f(y), h(x)) -> trans(h(x), f(y)),
 trans(g(x), trans(g(y), z)) -> trans(g(trans(x, y)), z),
           trans(g(x), g(y)) -> g(trans(x, y)),
 trans(h(x), trans(g(y), z)) -> trans(g(y), trans(h(x), z)),
 trans(h(x), trans(h(y), z)) -> trans(h(trans(x, y)), z),
           trans(h(x), g(y)) -> trans(g(y), h(x)),
           trans(h(x), h(y)) -> h(trans(x, y)),
              i(trans(x, y)) -> trans(i(y), i(x)),
                    i(one()) -> one(),
                     i(i(x)) -> x,
                     i(f(x)) -> f(i(x)),
                     i(g(x)) -> g(i(x)),
                     i(h(x)) -> h(i(x)),
                    f(one()) -> one(),
                    g(one()) -> one(),
                    h(one()) -> one()



STATISTICS

number of inference steps: 341 

total time:   6135.95
orient:       5084.76
rewrite:      805.20
deduce:       139.91
termination:  3501.33

external termination prover: ./ttt2micro
calls to termination prover: 28539 (yes: 21519, timeouts: 0)
time limit per call:         1.0