SUCCESS
617.33 (total time)


COMPLETED TRS


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



STATISTICS

number of inference steps: 141

total time:   617.33
orient:       232.42
rewrite:      368.04
deduce:       11.58
termination:  204.61

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