SUCCESS
78.64 (total time)


COMPLETED TRS

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



STATISTICS

total time:   78.64
termination:  65.94

external termination prover: ttt2fast
termination checks: 608 (yes: 389, timeouts: 0)
timelimit per check: 1.0