SUCCESS 27.58 (total time) COMPLETED TRS a(a(a(a(x)))) -> a(a(a(x))), a(a(a(c(x)))) -> a(a(a(x))), a(a(b(a(x)))) -> a(a(x)), a(b(a(a(a(x))))) -> a(a(a(x))), a(c(a(x))) -> a(a(a(x))), b(a(a(c(x)))) -> b(a(a(a(x)))), b(a(b(x))) -> b(x), c(a(a(x))) -> a(b(a(a(x)))), c(a(b(a(a(x))))) -> a(a(a(x))), c(a(c(x))) -> a(a(c(x))), c(b(x)) -> a(a(b(x))), c(c(x)) -> a(b(a(a(x)))) STATISTICS number of inference steps: 35 total time: 27.58 orient: 19.96 rewrite: 6.33 deduce: 1.20 termination: 19.74 termination checked internally with ttt2fast termination checks: 173 (yes: 91, timeouts: 0) timelimit per check: 0.7