SUCCESS
6.06 (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:   6.06
orient:       4.79
rewrite:      1.12
deduce:       0.09
termination:  4.74

external termination prover: ttt2fast
calls to termination prover: 47 (yes: 33, timeouts: 0)
timelimit per call:          1.0