SUCCESS
248.95 (total time)


COMPLETED TRS

 
             b(x) -> c(c(x)),
          a(a(x)) -> d(c(x)),
       a(c(c(x))) -> c(c(c(x))),
       a(d(c(x))) -> d(c(a(x))),
    c(c(c(a(x)))) -> c(c(c(x))),
    c(c(c(c(x)))) -> c(c(c(x))),
          c(d(x)) -> d(c(x)),
    d(c(a(c(x)))) -> c(c(c(x))),
    d(c(a(d(x)))) -> c(c(c(x))),
 d(c(c(a(c(x))))) -> c(c(c(x))),
 d(c(c(a(d(x))))) -> c(c(c(x))),
    d(c(c(c(x)))) -> c(c(c(x))),
          d(d(x)) -> c(c(a(c(x))))



STATISTICS

number of inference steps: 15 

total time:   248.95
orient:       247.85
rewrite:      0.92
deduce:       0.15
termination:  247.76

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