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