SUCCESS
13.17 (total time)


COMPLETED TRS


 a(a(a(a(x0)))) -> a(a(a(x0))),
 a(a(a(c(x0)))) -> a(a(a(x0))),
 a(a(b(a(x0)))) -> a(a(x0)),
 a(b(a(a(x0)))) -> c(a(a(x0))),
    a(c(a(x0))) -> a(a(a(x0))),
 b(a(a(c(x0)))) -> b(a(a(a(x0)))),
    b(a(b(x0))) -> b(x0),
 b(c(a(a(x0)))) -> b(a(a(x0))),
 c(a(a(a(x0)))) -> a(a(a(x0))),
 c(a(a(c(x0)))) -> a(a(a(x0))),
    c(a(c(x0))) -> a(a(c(x0))),
       c(b(x0)) -> a(a(b(x0))),
       c(c(x0)) -> c(a(a(x0)))


STATISTICS

total time:   13.17
termination:  11.41

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