YES(O(1),O(n^3)) 192.94/60.05 YES(O(1),O(n^3)) 192.94/60.05 192.94/60.05 We are left with following problem, upon which TcT provides the 192.94/60.05 certificate YES(O(1),O(n^3)). 192.94/60.05 192.94/60.05 Strict Trs: 192.94/60.05 { P(x1) -> Q(Q(p(x1))) 192.94/60.05 , P(p(x1)) -> x1 192.94/60.05 , Q(p(q(x1))) -> q(p(Q(x1))) 192.94/60.05 , Q(q(x1)) -> x1 192.94/60.05 , p(P(x1)) -> x1 192.94/60.05 , p(Q(Q(x1))) -> Q(Q(p(x1))) 192.94/60.05 , p(p(x1)) -> q(q(x1)) 192.94/60.05 , q(Q(x1)) -> x1 192.94/60.05 , q(q(p(x1))) -> p(q(q(x1))) } 192.94/60.05 Obligation: 192.94/60.05 derivational complexity 192.94/60.05 Answer: 192.94/60.05 YES(O(1),O(n^3)) 192.94/60.05 192.94/60.05 We use the processor 'matrix interpretation of dimension 1' to 192.94/60.05 orient following rules strictly. 192.94/60.05 192.94/60.05 Trs: 192.94/60.05 { P(x1) -> Q(Q(p(x1))) 192.94/60.05 , P(p(x1)) -> x1 192.94/60.05 , p(P(x1)) -> x1 } 192.94/60.05 192.94/60.05 The induced complexity on above rules (modulo remaining rules) is 192.94/60.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 192.94/60.05 component(s). 192.94/60.05 192.94/60.05 Sub-proof: 192.94/60.05 ---------- 192.94/60.05 TcT has computed the following triangular matrix interpretation. 192.94/60.05 192.94/60.05 [P](x1) = [1] x1 + [1] 192.94/60.05 192.94/60.05 [Q](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 [p](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 [q](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 The order satisfies the following ordering constraints: 192.94/60.05 192.94/60.05 [P(x1)] = [1] x1 + [1] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [Q(Q(p(x1)))] 192.94/60.05 192.94/60.05 [P(p(x1))] = [1] x1 + [1] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [Q(p(q(x1)))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [q(p(Q(x1)))] 192.94/60.05 192.94/60.05 [Q(q(x1))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [p(P(x1))] = [1] x1 + [1] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [p(Q(Q(x1)))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [Q(Q(p(x1)))] 192.94/60.05 192.94/60.05 [p(p(x1))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [q(q(x1))] 192.94/60.05 192.94/60.05 [q(Q(x1))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [q(q(p(x1)))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [p(q(q(x1)))] 192.94/60.05 192.94/60.05 192.94/60.05 We return to the main proof. 192.94/60.05 192.94/60.05 We are left with following problem, upon which TcT provides the 192.94/60.05 certificate YES(O(1),O(n^3)). 192.94/60.05 192.94/60.05 Strict Trs: 192.94/60.05 { Q(p(q(x1))) -> q(p(Q(x1))) 192.94/60.05 , Q(q(x1)) -> x1 192.94/60.05 , p(Q(Q(x1))) -> Q(Q(p(x1))) 192.94/60.05 , p(p(x1)) -> q(q(x1)) 192.94/60.05 , q(Q(x1)) -> x1 192.94/60.05 , q(q(p(x1))) -> p(q(q(x1))) } 192.94/60.05 Weak Trs: 192.94/60.05 { P(x1) -> Q(Q(p(x1))) 192.94/60.05 , P(p(x1)) -> x1 192.94/60.05 , p(P(x1)) -> x1 } 192.94/60.05 Obligation: 192.94/60.05 derivational complexity 192.94/60.05 Answer: 192.94/60.05 YES(O(1),O(n^3)) 192.94/60.05 192.94/60.05 We use the processor 'matrix interpretation of dimension 1' to 192.94/60.05 orient following rules strictly. 192.94/60.05 192.94/60.05 Trs: { p(p(x1)) -> q(q(x1)) } 192.94/60.05 192.94/60.05 The induced complexity on above rules (modulo remaining rules) is 192.94/60.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 192.94/60.05 component(s). 192.94/60.05 192.94/60.05 Sub-proof: 192.94/60.05 ---------- 192.94/60.05 TcT has computed the following triangular matrix interpretation. 192.94/60.05 192.94/60.05 [P](x1) = [1] x1 + [1] 192.94/60.05 192.94/60.05 [Q](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 [p](x1) = [1] x1 + [1] 192.94/60.05 192.94/60.05 [q](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 The order satisfies the following ordering constraints: 192.94/60.05 192.94/60.05 [P(x1)] = [1] x1 + [1] 192.94/60.05 >= [1] x1 + [1] 192.94/60.05 = [Q(Q(p(x1)))] 192.94/60.05 192.94/60.05 [P(p(x1))] = [1] x1 + [2] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [Q(p(q(x1)))] = [1] x1 + [1] 192.94/60.05 >= [1] x1 + [1] 192.94/60.05 = [q(p(Q(x1)))] 192.94/60.05 192.94/60.05 [Q(q(x1))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [p(P(x1))] = [1] x1 + [2] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [p(Q(Q(x1)))] = [1] x1 + [1] 192.94/60.05 >= [1] x1 + [1] 192.94/60.05 = [Q(Q(p(x1)))] 192.94/60.05 192.94/60.05 [p(p(x1))] = [1] x1 + [2] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [q(q(x1))] 192.94/60.05 192.94/60.05 [q(Q(x1))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [q(q(p(x1)))] = [1] x1 + [1] 192.94/60.05 >= [1] x1 + [1] 192.94/60.05 = [p(q(q(x1)))] 192.94/60.05 192.94/60.05 192.94/60.05 We return to the main proof. 192.94/60.05 192.94/60.05 We are left with following problem, upon which TcT provides the 192.94/60.05 certificate YES(O(1),O(n^3)). 192.94/60.05 192.94/60.05 Strict Trs: 192.94/60.05 { Q(p(q(x1))) -> q(p(Q(x1))) 192.94/60.05 , Q(q(x1)) -> x1 192.94/60.05 , p(Q(Q(x1))) -> Q(Q(p(x1))) 192.94/60.05 , q(Q(x1)) -> x1 192.94/60.05 , q(q(p(x1))) -> p(q(q(x1))) } 192.94/60.05 Weak Trs: 192.94/60.05 { P(x1) -> Q(Q(p(x1))) 192.94/60.05 , P(p(x1)) -> x1 192.94/60.05 , p(P(x1)) -> x1 192.94/60.05 , p(p(x1)) -> q(q(x1)) } 192.94/60.05 Obligation: 192.94/60.05 derivational complexity 192.94/60.05 Answer: 192.94/60.05 YES(O(1),O(n^3)) 192.94/60.05 192.94/60.05 We use the processor 'matrix interpretation of dimension 1' to 192.94/60.05 orient following rules strictly. 192.94/60.05 192.94/60.05 Trs: 192.94/60.05 { Q(q(x1)) -> x1 192.94/60.05 , q(Q(x1)) -> x1 } 192.94/60.05 192.94/60.05 The induced complexity on above rules (modulo remaining rules) is 192.94/60.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 192.94/60.05 component(s). 192.94/60.05 192.94/60.05 Sub-proof: 192.94/60.05 ---------- 192.94/60.05 TcT has computed the following triangular matrix interpretation. 192.94/60.05 192.94/60.05 [P](x1) = [1] x1 + [2] 192.94/60.05 192.94/60.05 [Q](x1) = [1] x1 + [1] 192.94/60.05 192.94/60.05 [p](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 [q](x1) = [1] x1 + [0] 192.94/60.05 192.94/60.05 The order satisfies the following ordering constraints: 192.94/60.05 192.94/60.05 [P(x1)] = [1] x1 + [2] 192.94/60.05 >= [1] x1 + [2] 192.94/60.05 = [Q(Q(p(x1)))] 192.94/60.05 192.94/60.05 [P(p(x1))] = [1] x1 + [2] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [Q(p(q(x1)))] = [1] x1 + [1] 192.94/60.05 >= [1] x1 + [1] 192.94/60.05 = [q(p(Q(x1)))] 192.94/60.05 192.94/60.05 [Q(q(x1))] = [1] x1 + [1] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [p(P(x1))] = [1] x1 + [2] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [p(Q(Q(x1)))] = [1] x1 + [2] 192.94/60.05 >= [1] x1 + [2] 192.94/60.05 = [Q(Q(p(x1)))] 192.94/60.05 192.94/60.05 [p(p(x1))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [q(q(x1))] 192.94/60.05 192.94/60.05 [q(Q(x1))] = [1] x1 + [1] 192.94/60.05 > [1] x1 + [0] 192.94/60.05 = [x1] 192.94/60.05 192.94/60.05 [q(q(p(x1)))] = [1] x1 + [0] 192.94/60.05 >= [1] x1 + [0] 192.94/60.05 = [p(q(q(x1)))] 192.94/60.05 192.94/60.05 192.94/60.05 We return to the main proof. 192.94/60.05 192.94/60.05 We are left with following problem, upon which TcT provides the 192.94/60.05 certificate YES(O(1),O(n^3)). 192.94/60.05 192.94/60.05 Strict Trs: 192.94/60.05 { Q(p(q(x1))) -> q(p(Q(x1))) 192.94/60.05 , p(Q(Q(x1))) -> Q(Q(p(x1))) 192.94/60.05 , q(q(p(x1))) -> p(q(q(x1))) } 192.94/60.05 Weak Trs: 192.94/60.05 { P(x1) -> Q(Q(p(x1))) 192.94/60.05 , P(p(x1)) -> x1 192.94/60.05 , Q(q(x1)) -> x1 192.94/60.05 , p(P(x1)) -> x1 192.94/60.05 , p(p(x1)) -> q(q(x1)) 192.94/60.05 , q(Q(x1)) -> x1 } 192.94/60.05 Obligation: 192.94/60.05 derivational complexity 192.94/60.05 Answer: 192.94/60.05 YES(O(1),O(n^3)) 192.94/60.05 192.94/60.05 We use the processor 'matrix interpretation of dimension 3' to 192.94/60.05 orient following rules strictly. 192.94/60.05 192.94/60.05 Trs: { Q(p(q(x1))) -> q(p(Q(x1))) } 192.94/60.05 192.94/60.05 The induced complexity on above rules (modulo remaining rules) is 192.94/60.05 YES(?,O(n^3)) . These rules are moved into the corresponding weak 192.94/60.05 component(s). 192.94/60.05 192.94/60.05 Sub-proof: 192.94/60.05 ---------- 192.94/60.05 TcT has computed the following triangular matrix interpretation. 192.94/60.05 192.94/60.05 [1 1 2] [2] 192.94/60.05 [P](x1) = [0 1 0] x1 + [2] 192.94/60.05 [0 0 1] [1] 192.94/60.05 192.94/60.05 [1 0 1] [0] 192.94/60.05 [Q](x1) = [0 1 0] x1 + [1] 192.94/60.05 [0 0 1] [0] 192.94/60.05 192.94/60.05 [1 1 0] [0] 192.94/60.05 [p](x1) = [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [1] 192.94/60.06 192.94/60.06 [1 0 0] [0] 192.94/60.06 [q](x1) = [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [1] 192.94/60.06 192.94/60.06 The order satisfies the following ordering constraints: 192.94/60.06 192.94/60.06 [P(x1)] = [1 1 2] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 1 2] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [1] 192.94/60.06 = [Q(Q(p(x1)))] 192.94/60.06 192.94/60.06 [P(p(x1))] = [1 2 2] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [Q(p(q(x1)))] = [1 1 1] [2] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 1 1] [1] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 = [q(p(Q(x1)))] 192.94/60.06 192.94/60.06 [Q(q(x1))] = [1 0 1] [1] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [1] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [p(P(x1))] = [1 2 2] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [p(Q(Q(x1)))] = [1 1 2] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 1 2] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [1] 192.94/60.06 = [Q(Q(p(x1)))] 192.94/60.06 192.94/60.06 [p(p(x1))] = [1 2 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [2] 192.94/60.06 >= [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [2] 192.94/60.06 = [q(q(x1))] 192.94/60.06 192.94/60.06 [q(Q(x1))] = [1 0 1] [0] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [q(q(p(x1)))] = [1 1 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [3] 192.94/60.06 >= [1 1 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [3] 192.94/60.06 = [p(q(q(x1)))] 192.94/60.06 192.94/60.06 192.94/60.06 We return to the main proof. 192.94/60.06 192.94/60.06 We are left with following problem, upon which TcT provides the 192.94/60.06 certificate YES(O(1),O(n^3)). 192.94/60.06 192.94/60.06 Strict Trs: 192.94/60.06 { p(Q(Q(x1))) -> Q(Q(p(x1))) 192.94/60.06 , q(q(p(x1))) -> p(q(q(x1))) } 192.94/60.06 Weak Trs: 192.94/60.06 { P(x1) -> Q(Q(p(x1))) 192.94/60.06 , P(p(x1)) -> x1 192.94/60.06 , Q(p(q(x1))) -> q(p(Q(x1))) 192.94/60.06 , Q(q(x1)) -> x1 192.94/60.06 , p(P(x1)) -> x1 192.94/60.06 , p(p(x1)) -> q(q(x1)) 192.94/60.06 , q(Q(x1)) -> x1 } 192.94/60.06 Obligation: 192.94/60.06 derivational complexity 192.94/60.06 Answer: 192.94/60.06 YES(O(1),O(n^3)) 192.94/60.06 192.94/60.06 We use the processor 'matrix interpretation of dimension 3' to 192.94/60.06 orient following rules strictly. 192.94/60.06 192.94/60.06 Trs: { p(Q(Q(x1))) -> Q(Q(p(x1))) } 192.94/60.06 192.94/60.06 The induced complexity on above rules (modulo remaining rules) is 192.94/60.06 YES(?,O(n^3)) . These rules are moved into the corresponding weak 192.94/60.06 component(s). 192.94/60.06 192.94/60.06 Sub-proof: 192.94/60.06 ---------- 192.94/60.06 TcT has computed the following triangular matrix interpretation. 192.94/60.06 192.94/60.06 [1 2 2] [2] 192.94/60.06 [P](x1) = [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 192.94/60.06 [1 1 0] [0] 192.94/60.06 [Q](x1) = [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [1] 192.94/60.06 192.94/60.06 [1 0 2] [0] 192.94/60.06 [p](x1) = [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [0] 192.94/60.06 192.94/60.06 [1 0 0] [0] 192.94/60.06 [q](x1) = [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [0] 192.94/60.06 192.94/60.06 The order satisfies the following ordering constraints: 192.94/60.06 192.94/60.06 [P(x1)] = [1 2 2] [2] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 >= [1 2 2] [2] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 = [Q(Q(p(x1)))] 192.94/60.06 192.94/60.06 [P(p(x1))] = [1 2 4] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [Q(p(q(x1)))] = [1 1 2] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 1 2] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [1] 192.94/60.06 = [q(p(Q(x1)))] 192.94/60.06 192.94/60.06 [Q(q(x1))] = [1 1 0] [1] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [1] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [p(P(x1))] = [1 2 4] [6] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [p(Q(Q(x1)))] = [1 2 2] [4] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 2 2] [2] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [2] 192.94/60.06 = [Q(Q(p(x1)))] 192.94/60.06 192.94/60.06 [p(p(x1))] = [1 0 4] [0] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [0] 192.94/60.06 >= [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [q(q(x1))] 192.94/60.06 192.94/60.06 [q(Q(x1))] = [1 1 0] [0] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [q(q(p(x1)))] = [1 0 2] [0] 192.94/60.06 [0 1 0] x1 + [3] 192.94/60.06 [0 0 1] [0] 192.94/60.06 >= [1 0 2] [0] 192.94/60.06 [0 1 0] x1 + [3] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [p(q(q(x1)))] 192.94/60.06 192.94/60.06 192.94/60.06 We return to the main proof. 192.94/60.06 192.94/60.06 We are left with following problem, upon which TcT provides the 192.94/60.06 certificate YES(?,O(n^3)). 192.94/60.06 192.94/60.06 Strict Trs: { q(q(p(x1))) -> p(q(q(x1))) } 192.94/60.06 Weak Trs: 192.94/60.06 { P(x1) -> Q(Q(p(x1))) 192.94/60.06 , P(p(x1)) -> x1 192.94/60.06 , Q(p(q(x1))) -> q(p(Q(x1))) 192.94/60.06 , Q(q(x1)) -> x1 192.94/60.06 , p(P(x1)) -> x1 192.94/60.06 , p(Q(Q(x1))) -> Q(Q(p(x1))) 192.94/60.06 , p(p(x1)) -> q(q(x1)) 192.94/60.06 , q(Q(x1)) -> x1 } 192.94/60.06 Obligation: 192.94/60.06 derivational complexity 192.94/60.06 Answer: 192.94/60.06 YES(?,O(n^3)) 192.94/60.06 192.94/60.06 TcT has computed the following triangular matrix interpretation. 192.94/60.06 192.94/60.06 [1 5 2] [4] 192.94/60.06 [P](x1) = [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 192.94/60.06 [1 1 0] [0] 192.94/60.06 [Q](x1) = [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [1] 192.94/60.06 192.94/60.06 [1 3 2] [0] 192.94/60.06 [p](x1) = [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [0] 192.94/60.06 192.94/60.06 [1 2 0] [0] 192.94/60.06 [q](x1) = [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [0] 192.94/60.06 192.94/60.06 The order satisfies the following ordering constraints: 192.94/60.06 192.94/60.06 [P(x1)] = [1 5 2] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 >= [1 5 2] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 = [Q(Q(p(x1)))] 192.94/60.06 192.94/60.06 [P(p(x1))] = [1 8 4] [14] 192.94/60.06 [0 1 0] x1 + [4] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [Q(p(q(x1)))] = [1 6 2] [6] 192.94/60.06 [0 1 0] x1 + [3] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 6 2] [6] 192.94/60.06 [0 1 0] x1 + [3] 192.94/60.06 [0 0 1] [1] 192.94/60.06 = [q(p(Q(x1)))] 192.94/60.06 192.94/60.06 [Q(q(x1))] = [1 3 0] [1] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [1] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [p(P(x1))] = [1 8 4] [14] 192.94/60.06 [0 1 0] x1 + [4] 192.94/60.06 [0 0 1] [2] 192.94/60.06 > [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [p(Q(Q(x1)))] = [1 5 2] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 >= [1 5 2] [4] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [2] 192.94/60.06 = [Q(Q(p(x1)))] 192.94/60.06 192.94/60.06 [p(p(x1))] = [1 6 4] [6] 192.94/60.06 [0 1 0] x1 + [4] 192.94/60.06 [0 0 1] [0] 192.94/60.06 > [1 4 0] [2] 192.94/60.06 [0 1 0] x1 + [2] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [q(q(x1))] 192.94/60.06 192.94/60.06 [q(Q(x1))] = [1 3 0] [0] 192.94/60.06 [0 1 0] x1 + [1] 192.94/60.06 [0 0 1] [1] 192.94/60.06 >= [1 0 0] [0] 192.94/60.06 [0 1 0] x1 + [0] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [x1] 192.94/60.06 192.94/60.06 [q(q(p(x1)))] = [1 7 2] [10] 192.94/60.06 [0 1 0] x1 + [4] 192.94/60.06 [0 0 1] [0] 192.94/60.06 > [1 7 2] [8] 192.94/60.06 [0 1 0] x1 + [4] 192.94/60.06 [0 0 1] [0] 192.94/60.06 = [p(q(q(x1)))] 192.94/60.06 192.94/60.06 192.94/60.06 Hurray, we answered YES(O(1),O(n^3)) 192.94/60.08 EOF