SUCCESS
10.95 (total time)


COMPLETED TRS

 
       /(x, y) -> *(y, x),
       \(x, y) -> *(y, x),
 *(*(x, y), x) -> y,
 *(x, *(y, x)) -> y



STATISTICS

number of inference steps: 12 

total time:   10.95
orient:       10.89
rewrite:      0.01
deduce:       0.04
termination:  10.89

external termination prover: aprove07
calls to termination prover: 8 (yes: 8, timeouts: 0)
timelimit per call:          5.0