YES(?,O(n^3)) 1031.13/295.37 YES(?,O(n^3)) 1031.13/295.38 1031.13/295.38 Problem: 1031.13/295.38 P(x1) -> Q(Q(p(x1))) 1031.13/295.38 p(p(x1)) -> q(q(x1)) 1031.13/295.38 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.38 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.38 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.38 q(Q(x1)) -> x1 1031.13/295.38 Q(q(x1)) -> x1 1031.13/295.38 p(P(x1)) -> x1 1031.13/295.38 P(p(x1)) -> x1 1031.13/295.38 1031.13/295.38 Proof: 1031.13/295.38 Complexity Transformation Processor: 1031.13/295.38 strict: 1031.13/295.38 P(x1) -> Q(Q(p(x1))) 1031.13/295.38 p(p(x1)) -> q(q(x1)) 1031.13/295.38 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.38 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.38 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.38 q(Q(x1)) -> x1 1031.13/295.38 Q(q(x1)) -> x1 1031.13/295.38 p(P(x1)) -> x1 1031.13/295.38 P(p(x1)) -> x1 1031.13/295.38 weak: 1031.13/295.38 1031.13/295.38 Matrix Interpretation Processor: dim=1 1031.13/295.38 1031.13/295.38 max_matrix: 1031.13/295.38 1 1031.13/295.38 interpretation: 1031.13/295.38 [q](x0) = x0 + 12, 1031.13/295.38 1031.13/295.38 [Q](x0) = x0 + 164, 1031.13/295.38 1031.13/295.38 [p](x0) = x0 + 100, 1031.13/295.38 1031.13/295.38 [P](x0) = x0 + 192 1031.13/295.38 orientation: 1031.13/295.38 P(x1) = x1 + 192 >= x1 + 428 = Q(Q(p(x1))) 1031.13/295.38 1031.13/295.38 p(p(x1)) = x1 + 200 >= x1 + 24 = q(q(x1)) 1031.13/295.38 1031.13/295.38 p(Q(Q(x1))) = x1 + 428 >= x1 + 428 = Q(Q(p(x1))) 1031.13/295.38 1031.13/295.38 Q(p(q(x1))) = x1 + 276 >= x1 + 276 = q(p(Q(x1))) 1031.13/295.38 1031.13/295.38 q(q(p(x1))) = x1 + 124 >= x1 + 124 = p(q(q(x1))) 1031.13/295.38 1031.13/295.38 q(Q(x1)) = x1 + 176 >= x1 = x1 1031.13/295.38 1031.13/295.38 Q(q(x1)) = x1 + 176 >= x1 = x1 1031.13/295.38 1031.13/295.38 p(P(x1)) = x1 + 292 >= x1 = x1 1031.13/295.38 1031.13/295.38 P(p(x1)) = x1 + 292 >= x1 = x1 1031.13/295.38 problem: 1031.13/295.38 strict: 1031.13/295.38 P(x1) -> Q(Q(p(x1))) 1031.13/295.38 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.38 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.38 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.38 weak: 1031.13/295.38 p(p(x1)) -> q(q(x1)) 1031.13/295.38 q(Q(x1)) -> x1 1031.13/295.38 Q(q(x1)) -> x1 1031.13/295.38 p(P(x1)) -> x1 1031.13/295.38 P(p(x1)) -> x1 1031.13/295.38 Matrix Interpretation Processor: dim=1 1031.13/295.38 1031.13/295.38 max_matrix: 1031.13/295.38 1 1031.13/295.38 interpretation: 1031.13/295.38 [q](x0) = x0, 1031.13/295.38 1031.13/295.38 [Q](x0) = x0, 1031.13/295.38 1031.13/295.38 [p](x0) = x0, 1031.13/295.38 1031.13/295.38 [P](x0) = x0 + 8 1031.13/295.38 orientation: 1031.13/295.38 P(x1) = x1 + 8 >= x1 = Q(Q(p(x1))) 1031.13/295.38 1031.13/295.38 p(Q(Q(x1))) = x1 >= x1 = Q(Q(p(x1))) 1031.13/295.38 1031.13/295.38 Q(p(q(x1))) = x1 >= x1 = q(p(Q(x1))) 1031.13/295.38 1031.13/295.38 q(q(p(x1))) = x1 >= x1 = p(q(q(x1))) 1031.13/295.38 1031.13/295.38 p(p(x1)) = x1 >= x1 = q(q(x1)) 1031.13/295.38 1031.13/295.38 q(Q(x1)) = x1 >= x1 = x1 1031.13/295.38 1031.13/295.38 Q(q(x1)) = x1 >= x1 = x1 1031.13/295.38 1031.13/295.38 p(P(x1)) = x1 + 8 >= x1 = x1 1031.13/295.38 1031.13/295.38 P(p(x1)) = x1 + 8 >= x1 = x1 1031.13/295.38 problem: 1031.13/295.38 strict: 1031.13/295.38 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.38 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.38 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.38 weak: 1031.13/295.38 P(x1) -> Q(Q(p(x1))) 1031.13/295.38 p(p(x1)) -> q(q(x1)) 1031.13/295.38 q(Q(x1)) -> x1 1031.13/295.38 Q(q(x1)) -> x1 1031.13/295.38 p(P(x1)) -> x1 1031.13/295.38 P(p(x1)) -> x1 1031.13/295.38 Matrix Interpretation Processor: dim=3 1031.13/295.38 1031.13/295.38 max_matrix: 1031.13/295.38 [1 2 2] 1031.13/295.38 [0 1 3] 1031.13/295.38 [0 0 1] 1031.13/295.38 interpretation: 1031.13/295.38 [0] 1031.13/295.38 [q](x0) = x0 + [1] 1031.13/295.38 [0], 1031.13/295.38 1031.13/295.38 [1 1 0] [0] 1031.13/295.38 [Q](x0) = [0 1 1]x0 + [0] 1031.13/295.38 [0 0 1] [1], 1031.13/295.38 1031.13/295.38 [1 0 1] [0] 1031.13/295.38 [p](x0) = [0 1 0]x0 + [1] 1031.13/295.38 [0 0 1] [0], 1031.13/295.38 1031.13/295.38 [1 2 2] [2] 1031.13/295.38 [P](x0) = [0 1 3]x0 + [2] 1031.13/295.38 [0 0 1] [4] 1031.13/295.38 orientation: 1031.13/295.38 [1 2 2] [2] [1 2 2] [2] 1031.13/295.38 p(Q(Q(x1))) = [0 1 2]x1 + [2] >= [0 1 2]x1 + [2] = Q(Q(p(x1))) 1031.13/295.38 [0 0 1] [2] [0 0 1] [2] 1031.13/295.38 1031.13/295.38 [1 1 1] [2] [1 1 1] [1] 1031.13/295.38 Q(p(q(x1))) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [2] = q(p(Q(x1))) 1031.13/295.38 [0 0 1] [1] [0 0 1] [1] 1031.13/295.38 1031.13/295.38 [1 0 1] [0] [1 0 1] [0] 1031.13/295.38 q(q(p(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = p(q(q(x1))) 1031.13/295.38 [0 0 1] [0] [0 0 1] [0] 1031.13/295.38 1031.13/295.38 [1 2 2] [2] [1 2 2] [2] 1031.13/295.38 P(x1) = [0 1 3]x1 + [2] >= [0 1 2]x1 + [2] = Q(Q(p(x1))) 1031.13/295.38 [0 0 1] [4] [0 0 1] [2] 1031.13/295.38 1031.13/295.38 [1 0 2] [0] [0] 1031.13/295.38 p(p(x1)) = [0 1 0]x1 + [2] >= x1 + [2] = q(q(x1)) 1031.13/295.38 [0 0 1] [0] [0] 1031.13/295.38 1031.13/295.38 [1 1 0] [0] 1031.13/295.38 q(Q(x1)) = [0 1 1]x1 + [1] >= x1 = x1 1031.13/295.38 [0 0 1] [1] 1031.13/295.38 1031.13/295.38 [1 1 0] [1] 1031.13/295.38 Q(q(x1)) = [0 1 1]x1 + [1] >= x1 = x1 1031.13/295.38 [0 0 1] [1] 1031.13/295.38 1031.13/295.38 [1 2 3] [6] 1031.13/295.39 p(P(x1)) = [0 1 3]x1 + [3] >= x1 = x1 1031.13/295.39 [0 0 1] [4] 1031.13/295.39 1031.13/295.39 [1 2 3] [4] 1031.13/295.39 P(p(x1)) = [0 1 3]x1 + [3] >= x1 = x1 1031.13/295.39 [0 0 1] [4] 1031.13/295.39 problem: 1031.13/295.39 strict: 1031.13/295.39 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.39 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.39 weak: 1031.13/295.39 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.39 P(x1) -> Q(Q(p(x1))) 1031.13/295.39 p(p(x1)) -> q(q(x1)) 1031.13/295.39 q(Q(x1)) -> x1 1031.13/295.39 Q(q(x1)) -> x1 1031.13/295.39 p(P(x1)) -> x1 1031.13/295.39 P(p(x1)) -> x1 1031.13/295.39 Matrix Interpretation Processor: dim=3 1031.13/295.39 1031.13/295.39 max_matrix: 1031.13/295.39 [1 2 5] 1031.13/295.39 [0 1 7] 1031.13/295.39 [0 0 1] 1031.13/295.39 interpretation: 1031.13/295.39 [0] 1031.13/295.39 [q](x0) = x0 + [1] 1031.13/295.39 [0], 1031.13/295.39 1031.13/295.39 [1 1 0] [0] 1031.13/295.39 [Q](x0) = [0 1 3]x0 + [0] 1031.13/295.39 [0 0 1] [1], 1031.13/295.39 1031.13/295.39 [1 0 2] [0] 1031.13/295.39 [p](x0) = [0 1 0]x0 + [1] 1031.13/295.39 [0 0 1] [0], 1031.13/295.39 1031.13/295.39 [1 2 5] [2] 1031.13/295.39 [P](x0) = [0 1 7]x0 + [4] 1031.13/295.39 [0 0 1] [2] 1031.13/295.39 orientation: 1031.13/295.39 [1 2 5] [4] [1 2 5] [2] 1031.13/295.39 p(Q(Q(x1))) = [0 1 6]x1 + [4] >= [0 1 6]x1 + [4] = Q(Q(p(x1))) 1031.13/295.39 [0 0 1] [2] [0 0 1] [2] 1031.13/295.39 1031.13/295.39 [1 0 2] [0] [1 0 2] [0] 1031.13/295.39 q(q(p(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = p(q(q(x1))) 1031.13/295.39 [0 0 1] [0] [0 0 1] [0] 1031.13/295.39 1031.13/295.39 [1 1 2] [2] [1 1 2] [2] 1031.13/295.39 Q(p(q(x1))) = [0 1 3]x1 + [2] >= [0 1 3]x1 + [2] = q(p(Q(x1))) 1031.13/295.39 [0 0 1] [1] [0 0 1] [1] 1031.13/295.39 1031.13/295.39 [1 2 5] [2] [1 2 5] [2] 1031.13/295.39 P(x1) = [0 1 7]x1 + [4] >= [0 1 6]x1 + [4] = Q(Q(p(x1))) 1031.13/295.39 [0 0 1] [2] [0 0 1] [2] 1031.13/295.39 1031.13/295.39 [1 0 4] [0] [0] 1031.13/295.39 p(p(x1)) = [0 1 0]x1 + [2] >= x1 + [2] = q(q(x1)) 1031.13/295.39 [0 0 1] [0] [0] 1031.13/295.39 1031.13/295.39 [1 1 0] [0] 1031.13/295.39 q(Q(x1)) = [0 1 3]x1 + [1] >= x1 = x1 1031.13/295.39 [0 0 1] [1] 1031.13/295.39 1031.13/295.39 [1 1 0] [1] 1031.13/295.39 Q(q(x1)) = [0 1 3]x1 + [1] >= x1 = x1 1031.13/295.39 [0 0 1] [1] 1031.13/295.39 1031.13/295.39 [1 2 7] [6] 1031.13/295.39 p(P(x1)) = [0 1 7]x1 + [5] >= x1 = x1 1031.13/295.39 [0 0 1] [2] 1031.13/295.39 1031.13/295.39 [1 2 7] [4] 1031.13/295.39 P(p(x1)) = [0 1 7]x1 + [5] >= x1 = x1 1031.13/295.39 [0 0 1] [2] 1031.13/295.39 problem: 1031.13/295.39 strict: 1031.13/295.39 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.39 weak: 1031.13/295.39 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.39 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.39 P(x1) -> Q(Q(p(x1))) 1031.13/295.39 p(p(x1)) -> q(q(x1)) 1031.13/295.39 q(Q(x1)) -> x1 1031.13/295.39 Q(q(x1)) -> x1 1031.13/295.39 p(P(x1)) -> x1 1031.13/295.39 P(p(x1)) -> x1 1031.13/295.39 Matrix Interpretation Processor: dim=3 1031.13/295.39 1031.13/295.39 max_matrix: 1031.13/295.39 [1 1 3] 1031.13/295.39 [0 1 0] 1031.13/295.39 [0 0 1] 1031.13/295.39 interpretation: 1031.13/295.39 [1 0 1] [0] 1031.13/295.39 [q](x0) = [0 1 0]x0 + [0] 1031.13/295.39 [0 0 1] [1], 1031.13/295.39 1031.13/295.39 [1 0 1] [0] 1031.13/295.39 [Q](x0) = [0 1 0]x0 + [2] 1031.13/295.39 [0 0 1] [0], 1031.13/295.39 1031.13/295.39 [1 1 1] [0] 1031.13/295.39 [p](x0) = [0 1 0]x0 + [0] 1031.13/295.39 [0 0 1] [2], 1031.13/295.39 1031.13/295.39 [1 1 3] [4] 1031.13/295.39 [P](x0) = [0 1 0]x0 + [4] 1031.13/295.39 [0 0 1] [2] 1031.13/295.39 orientation: 1031.13/295.39 [1 1 3] [5] [1 1 3] [3] 1031.13/295.39 q(q(p(x1))) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = p(q(q(x1))) 1031.13/295.39 [0 0 1] [4] [0 0 1] [4] 1031.13/295.39 1031.13/295.39 [1 1 3] [4] [1 1 3] [4] 1031.13/295.39 p(Q(Q(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = Q(Q(p(x1))) 1031.13/295.39 [0 0 1] [2] [0 0 1] [2] 1031.13/295.39 1031.13/295.39 [1 1 3] [4] [1 1 3] [4] 1031.13/295.39 Q(p(q(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q(p(Q(x1))) 1031.13/295.39 [0 0 1] [3] [0 0 1] [3] 1031.13/295.39 1031.13/295.39 [1 1 3] [4] [1 1 3] [4] 1031.13/295.39 P(x1) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = Q(Q(p(x1))) 1031.13/295.39 [0 0 1] [2] [0 0 1] [2] 1031.13/295.39 1031.13/295.39 [1 2 2] [2] [1 0 2] [1] 1031.13/295.39 p(p(x1)) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = q(q(x1)) 1031.13/295.39 [0 0 1] [4] [0 0 1] [2] 1031.13/295.39 1031.13/295.39 [1 0 2] [0] 1031.13/295.39 q(Q(x1)) = [0 1 0]x1 + [2] >= x1 = x1 1031.13/295.39 [0 0 1] [1] 1031.13/295.39 1031.13/295.39 [1 0 2] [1] 1031.13/295.39 Q(q(x1)) = [0 1 0]x1 + [2] >= x1 = x1 1031.13/295.39 [0 0 1] [1] 1031.13/295.39 1031.13/295.39 [1 2 4] [10] 1031.13/295.39 p(P(x1)) = [0 1 0]x1 + [4 ] >= x1 = x1 1031.13/295.39 [0 0 1] [4 ] 1031.13/295.39 1031.13/295.39 [1 2 4] [10] 1031.13/295.39 P(p(x1)) = [0 1 0]x1 + [4 ] >= x1 = x1 1031.13/295.39 [0 0 1] [4 ] 1031.13/295.39 problem: 1031.13/295.39 strict: 1031.13/295.39 1031.13/295.39 weak: 1031.13/295.39 q(q(p(x1))) -> p(q(q(x1))) 1031.13/295.39 p(Q(Q(x1))) -> Q(Q(p(x1))) 1031.13/295.39 Q(p(q(x1))) -> q(p(Q(x1))) 1031.13/295.39 P(x1) -> Q(Q(p(x1))) 1031.13/295.39 p(p(x1)) -> q(q(x1)) 1031.13/295.39 q(Q(x1)) -> x1 1031.13/295.39 Q(q(x1)) -> x1 1031.13/295.39 p(P(x1)) -> x1 1031.13/295.39 P(p(x1)) -> x1 1031.13/295.39 Qed 1031.13/295.39 EOF