SUCCESS
615.76 (total time)

COMPLETED TRS
k(one) -> one
h(one) -> one
g(one) -> one
f(one) -> one
i(k(x)) -> k(i(x))
i(h(x)) -> h(i(x))
i(g(x)) -> g(i(x))
i(f(x)) -> f(i(x))
i(i(x)) -> x
i(one) -> one
i(*(x, y)) -> *(i(y), i(x))
*(k(x), k(y)) -> k(*(x, y))
*(k(x), *(k(y), z)) -> *(k(*(x, y)), z)
*(h(y), k(x)) -> *(k(x), h(y))
*(h(y), *(k(x), z)) -> *(k(x), *(h(y), z))
*(h(x), h(y)) -> h(*(x, y))
*(h(x), *(h(y), z)) -> *(h(*(x, y)), z)
*(g(y), k(x)) -> *(k(x), g(y))
*(g(y), h(x)) -> *(h(x), g(y))
*(g(y), *(k(x), z)) -> *(k(x), *(g(y), z))
*(g(y), *(h(x), z)) -> *(h(x), *(g(y), z))
*(g(x), g(y)) -> g(*(x, y))
*(g(x), *(g(y), z)) -> *(g(*(x, y)), z)
*(f(y), k(x)) -> *(k(x), f(y))
*(f(y), h(x)) -> *(h(x), f(y))
*(f(y), g(x)) -> *(g(x), f(y))
*(f(y), *(k(x), z)) -> *(k(x), *(f(y), z))
*(f(y), *(h(x), z)) -> *(h(x), *(f(y), z))
*(f(y), *(g(x), z)) -> *(g(x), *(f(y), z))
*(f(x), f(y)) -> f(*(x, y))
*(f(x), *(f(y), z)) -> *(f(*(x, y)), z)
*(i(x), *(x, y)) -> y
*(i(x), x) -> one
*(one, x) -> x
*(*(x, y), z) -> *(x, *(y, z))
*(x, i(x)) -> one
*(x, one) -> x
*(x, *(i(x), y)) -> y

STATISTICS (MKBtt) 
General
 number of iterations:    62 
 number of nodes:         4227 
 number of processes:     240 
 time for orient:         484.55
 time for rewrite:        10.93
 time for deduce:         3.76

Isomorphisms
 check: renamings (repeatedly)

Selection
 strategy: (el(min(e(sum(smax)) + c(sum(smax)))), (data(smax), ( -el(#), ?)))
 time for selection:      10.12

Termination Checks  (internal)
 strategy: dp;(edg; sccs; (spsc | csf | cds | size | caf | ccs | emb | lpo))+
 termination checks:      5968 (yes: 3817, timeouts: 0)
 time limit for check:    10.00
 termination time:        458.70

Indexing  (Code Tree)
 Variants:                0.24
 Encompassments:          3.00
 Overlaps:                0.27
 Maintenance:             0.00