SUCCESS 33.65 (total time) COMPLETED TRS b(b(x)) -> b(c(x)), b(a(c(x))) -> d(d(x)), b(c(a(x))) -> b(c(x)), b(d(a(c(x)))) -> b(c(x)), b(d(a(d(x)))) -> b(c(x)), b(d(c(x))) -> b(c(x)), b(d(d(x))) -> b(c(x)), a(b(x)) -> b(c(x)), a(a(x)) -> d(c(x)), a(d(c(x))) -> d(c(a(x))), a(d(d(x))) -> b(c(x)), c(b(x)) -> b(c(x)), c(c(x)) -> b(x), c(d(x)) -> d(c(x)), d(b(x)) -> b(d(x)), d(c(a(c(x)))) -> b(c(x)), d(c(a(d(x)))) -> b(c(x)), d(d(c(x))) -> b(c(x)), d(d(d(x))) -> b(c(x)) STATISTICS number of inference steps: 33 total time: 33.65 orient: 28.94 rewrite: 4.03 deduce: 0.47 termination: 28.04 external termination prover: ttt2fast termination checks: 305 (yes: 204, timeouts: 0) timelimit per check: 1.0