YES(?,O(n^1)) 65.89/31.70 YES(?,O(n^1)) 65.89/31.70 65.89/31.70 We are left with following problem, upon which TcT provides the 65.89/31.70 certificate YES(?,O(n^1)). 65.89/31.70 65.89/31.70 Strict Trs: 65.89/31.70 { b(x1) -> c(c(x1)) 65.89/31.70 , b(c(a(x1))) -> a(b(a(b(c(x1))))) 65.89/31.70 , c(d(x1)) -> a(b(c(a(x1)))) 65.89/31.70 , a(a(x1)) -> a(c(b(a(x1)))) } 65.89/31.70 Obligation: 65.89/31.70 derivational complexity 65.89/31.70 Answer: 65.89/31.70 YES(?,O(n^1)) 65.89/31.70 65.89/31.70 The problem is match-bounded by 4. The enriched problem is 65.89/31.70 compatible with the following automaton. 65.89/31.70 { b_0(1) -> 1 65.89/31.70 , b_1(2) -> 5 65.89/31.70 , b_1(4) -> 3 65.89/31.70 , b_1(6) -> 7 65.89/31.70 , b_2(5) -> 20 65.89/31.70 , b_2(10) -> 9 65.89/31.70 , b_2(16) -> 15 65.89/31.70 , b_2(18) -> 17 65.89/31.70 , b_3(17) -> 22 65.89/31.70 , b_3(23) -> 22 65.89/31.70 , b_3(32) -> 31 65.89/31.70 , b_3(34) -> 33 65.89/31.70 , c_0(1) -> 1 65.89/31.70 , c_1(1) -> 2 65.89/31.70 , c_1(2) -> 1 65.89/31.70 , c_1(3) -> 2 65.89/31.70 , c_1(6) -> 4 65.89/31.70 , c_1(7) -> 3 65.89/31.70 , c_1(19) -> 2 65.89/31.70 , c_2(1) -> 18 65.89/31.70 , c_2(2) -> 11 65.89/31.70 , c_2(3) -> 18 65.89/31.70 , c_2(4) -> 12 65.89/31.70 , c_2(6) -> 13 65.89/31.70 , c_2(8) -> 18 65.89/31.70 , c_2(9) -> 8 65.89/31.70 , c_2(11) -> 5 65.89/31.70 , c_2(12) -> 3 65.89/31.70 , c_2(13) -> 7 65.89/31.70 , c_2(15) -> 18 65.89/31.70 , c_2(19) -> 18 65.89/31.70 , c_2(20) -> 19 65.89/31.70 , c_3(5) -> 24 65.89/31.70 , c_3(10) -> 14 65.89/31.70 , c_3(14) -> 9 65.89/31.70 , c_3(15) -> 34 65.89/31.70 , c_3(16) -> 25 65.89/31.70 , c_3(18) -> 26 65.89/31.70 , c_3(19) -> 34 65.89/31.70 , c_3(22) -> 21 65.89/31.70 , c_3(24) -> 20 65.89/31.70 , c_3(25) -> 15 65.89/31.70 , c_3(26) -> 17 65.89/31.70 , c_4(17) -> 27 65.89/31.70 , c_4(23) -> 27 65.89/31.70 , c_4(27) -> 22 65.89/31.70 , c_4(32) -> 35 65.89/31.70 , c_4(34) -> 36 65.89/31.70 , c_4(35) -> 31 65.89/31.70 , c_4(36) -> 33 65.89/31.70 , a_0(1) -> 1 65.89/31.70 , a_1(1) -> 6 65.89/31.70 , a_1(3) -> 1 65.89/31.70 , a_1(3) -> 2 65.89/31.70 , a_1(3) -> 5 65.89/31.70 , a_1(3) -> 6 65.89/31.70 , a_1(3) -> 17 65.89/31.70 , a_1(3) -> 18 65.89/31.70 , a_1(5) -> 4 65.89/31.70 , a_1(19) -> 6 65.89/31.70 , a_2(3) -> 10 65.89/31.70 , a_2(8) -> 4 65.89/31.70 , a_2(8) -> 6 65.89/31.70 , a_2(8) -> 16 65.89/31.70 , a_2(15) -> 3 65.89/31.70 , a_2(15) -> 5 65.89/31.70 , a_2(15) -> 17 65.89/31.70 , a_2(17) -> 16 65.89/31.70 , a_2(19) -> 1 65.89/31.70 , a_2(19) -> 2 65.89/31.70 , a_2(19) -> 4 65.89/31.70 , a_2(19) -> 5 65.89/31.70 , a_2(19) -> 6 65.89/31.70 , a_2(19) -> 17 65.89/31.70 , a_2(19) -> 18 65.89/31.70 , a_3(15) -> 23 65.89/31.70 , a_3(19) -> 17 65.89/31.70 , a_3(21) -> 10 65.89/31.70 , a_3(21) -> 16 65.89/31.70 , a_3(31) -> 17 65.89/31.70 , a_3(33) -> 32 65.89/31.70 , d_0(1) -> 1 } 65.89/31.70 65.89/31.70 Hurray, we answered YES(?,O(n^1)) 65.89/31.76 EOF