SUCCESS
105.17 (total time)


COMPLETED TRS


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


STATISTICS

number of inference steps: 14

total time:   105.17
orient:       104.41
rewrite:      0.69
deduce:       0.08
termination:  104.34

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