YES(?,O(n^4)) 914.76/297.11 YES(?,O(n^4)) 914.76/297.11 914.76/297.11 We are left with following problem, upon which TcT provides the 914.76/297.11 certificate YES(?,O(n^4)). 914.76/297.11 914.76/297.11 Strict Trs: 914.76/297.11 { a(a(x1)) -> c(b(x1)) 914.76/297.11 , c(c(x1)) -> b(a(x1)) 914.76/297.11 , b(b(x1)) -> a(c(x1)) } 914.76/297.11 Obligation: 914.76/297.11 derivational complexity 914.76/297.11 Answer: 914.76/297.11 YES(?,O(n^4)) 914.76/297.11 914.76/297.11 TcT has computed the following matrix interpretation satisfying 914.76/297.11 not(EDA). 914.76/297.11 914.76/297.11 [1 0 0 1] [0] 914.76/297.11 [a](x1) = [0 0 0 1] x1 + [0] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 [0 0 1 0] [1] 914.76/297.11 914.76/297.11 [1 1 0 0] [0] 914.76/297.11 [c](x1) = [0 0 0 1] x1 + [1] 914.76/297.11 [0 1 0 0] [0] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 914.76/297.11 [1 0 1 0] [0] 914.76/297.11 [b](x1) = [0 0 0 0] x1 + [0] 914.76/297.11 [0 1 0 0] [1] 914.76/297.11 [0 0 1 0] [0] 914.76/297.11 914.76/297.11 The order satisfies the following ordering constraints: 914.76/297.11 914.76/297.11 [a(a(x1))] = [1 0 1 1] [1] 914.76/297.11 [0 0 1 0] x1 + [1] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 [0 0 0 0] [1] 914.76/297.11 > [1 0 1 0] [0] 914.76/297.11 [0 0 1 0] x1 + [1] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 = [c(b(x1))] 914.76/297.11 914.76/297.11 [c(c(x1))] = [1 1 0 1] [1] 914.76/297.11 [0 0 0 0] x1 + [1] 914.76/297.11 [0 0 0 1] [1] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 > [1 0 0 1] [0] 914.76/297.11 [0 0 0 0] x1 + [0] 914.76/297.11 [0 0 0 1] [1] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 = [b(a(x1))] 914.76/297.11 914.76/297.11 [b(b(x1))] = [1 1 1 0] [1] 914.76/297.11 [0 0 0 0] x1 + [0] 914.76/297.11 [0 0 0 0] [1] 914.76/297.11 [0 1 0 0] [1] 914.76/297.11 > [1 1 0 0] [0] 914.76/297.11 [0 0 0 0] x1 + [0] 914.76/297.11 [0 0 0 0] [0] 914.76/297.11 [0 1 0 0] [1] 914.76/297.11 = [a(c(x1))] 914.76/297.11 914.76/297.11 914.76/297.11 Hurray, we answered YES(?,O(n^4)) 914.76/297.11 EOF