YES(?,O(n^1)) 979.41/239.69 YES(?,O(n^1)) 979.51/239.70 979.51/239.70 Problem: 979.51/239.70 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.70 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.70 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.70 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.70 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.70 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.70 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.70 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.70 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.70 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.70 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.70 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.70 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.70 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.70 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.70 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.70 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.70 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.70 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.70 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.70 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.70 979.51/239.70 Proof: 979.51/239.70 Complexity Transformation Processor: 979.51/239.70 strict: 979.51/239.70 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.70 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.70 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.70 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.70 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.70 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.70 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.70 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.70 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.70 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.70 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.70 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.70 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.70 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.70 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.70 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.70 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.70 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.70 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.70 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.70 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.70 weak: 979.51/239.70 979.51/239.70 Matrix Interpretation Processor: dim=1 979.51/239.70 979.51/239.70 max_matrix: 979.51/239.70 1 979.51/239.70 interpretation: 979.51/239.70 [3](x0) = x0, 979.51/239.70 979.51/239.70 [0](x0) = x0 + 5, 979.51/239.70 979.51/239.70 [4](x0) = x0 + 3, 979.51/239.70 979.51/239.70 [2](x0) = x0 + 1, 979.51/239.70 979.51/239.70 [1](x0) = x0, 979.51/239.70 979.51/239.70 [5](x0) = x0 + 2 979.51/239.70 orientation: 979.51/239.70 5(5(x1)) = x1 + 4 >= x1 + 24 = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.70 979.51/239.70 5(5(x1)) = x1 + 4 >= x1 + 17 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.70 979.51/239.70 2(5(5(x1))) = x1 + 5 >= x1 + 23 = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.70 979.51/239.70 5(2(4(x1))) = x1 + 6 >= x1 + 21 = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.70 979.51/239.70 5(5(2(x1))) = x1 + 5 >= x1 + 14 = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.70 979.51/239.70 5(5(3(x1))) = x1 + 4 >= x1 + 25 = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.70 979.51/239.70 5(5(5(x1))) = x1 + 6 >= x1 + 25 = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.70 979.51/239.70 2(5(0(4(x1)))) = x1 + 11 >= x1 + 25 = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.70 979.51/239.70 4(5(2(4(x1)))) = x1 + 9 >= x1 + 13 = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.70 979.51/239.70 4(5(5(5(x1)))) = x1 + 9 >= x1 + 16 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.70 979.51/239.70 0(2(5(3(4(x1))))) = x1 + 11 >= x1 + 9 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.70 979.51/239.70 2(5(5(3(4(x1))))) = x1 + 8 >= x1 + 23 = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.70 979.51/239.70 5(5(5(1(4(x1))))) = x1 + 9 >= x1 + 26 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.70 979.51/239.70 0(4(4(5(5(5(x1)))))) = x1 + 17 >= x1 + 17 = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.70 979.51/239.70 1(2(4(5(2(4(x1)))))) = x1 + 10 >= x1 + 15 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.70 979.51/239.70 4(1(5(5(0(4(x1)))))) = x1 + 15 >= x1 + 23 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.70 979.51/239.70 4(2(5(5(1(5(x1)))))) = x1 + 10 >= x1 + 11 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.70 979.51/239.70 5(2(5(5(0(4(x1)))))) = x1 + 15 >= x1 + 18 = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.70 979.51/239.70 5(5(2(4(5(0(x1)))))) = x1 + 15 >= x1 + 22 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.71 979.51/239.71 0(1(5(5(5(3(5(x1))))))) = x1 + 13 >= x1 + 18 = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.71 979.51/239.71 4(4(5(2(4(2(2(x1))))))) = x1 + 14 >= x1 + 19 = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.71 problem: 979.51/239.71 strict: 979.51/239.71 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.71 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.71 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.71 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.71 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.71 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.71 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.71 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.71 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.71 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.71 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.71 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.71 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.71 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.71 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.71 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.71 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.71 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.71 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.71 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.71 weak: 979.51/239.71 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.71 Matrix Interpretation Processor: dim=1 979.51/239.71 979.51/239.71 max_matrix: 979.51/239.71 1 979.51/239.71 interpretation: 979.51/239.71 [3](x0) = x0, 979.51/239.71 979.51/239.71 [0](x0) = x0, 979.51/239.71 979.51/239.71 [4](x0) = x0, 979.51/239.71 979.51/239.71 [2](x0) = x0 + 4, 979.51/239.71 979.51/239.71 [1](x0) = x0, 979.51/239.71 979.51/239.71 [5](x0) = x0 979.51/239.71 orientation: 979.51/239.71 5(5(x1)) = x1 >= x1 + 8 = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.71 979.51/239.71 5(5(x1)) = x1 >= x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.71 979.51/239.71 2(5(5(x1))) = x1 + 4 >= x1 + 8 = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.71 979.51/239.71 5(2(4(x1))) = x1 + 4 >= x1 + 12 = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.71 979.51/239.71 5(5(2(x1))) = x1 + 4 >= x1 + 8 = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.71 979.51/239.71 5(5(3(x1))) = x1 >= x1 = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.71 979.51/239.71 5(5(5(x1))) = x1 >= x1 = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.71 979.51/239.71 2(5(0(4(x1)))) = x1 + 4 >= x1 + 4 = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.71 979.51/239.71 4(5(2(4(x1)))) = x1 + 4 >= x1 + 4 = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.71 979.51/239.71 4(5(5(5(x1)))) = x1 >= x1 + 8 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.71 979.51/239.71 2(5(5(3(4(x1))))) = x1 + 4 >= x1 + 4 = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.71 979.51/239.71 5(5(5(1(4(x1))))) = x1 >= x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.71 979.51/239.71 0(4(4(5(5(5(x1)))))) = x1 >= x1 = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.71 979.51/239.71 1(2(4(5(2(4(x1)))))) = x1 + 8 >= x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.71 979.51/239.71 4(1(5(5(0(4(x1)))))) = x1 >= x1 + 4 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.71 979.51/239.71 4(2(5(5(1(5(x1)))))) = x1 + 4 >= x1 + 12 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.71 979.51/239.71 5(2(5(5(0(4(x1)))))) = x1 + 4 >= x1 + 8 = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.71 979.51/239.71 5(5(2(4(5(0(x1)))))) = x1 + 4 >= x1 + 12 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.71 979.51/239.71 0(1(5(5(5(3(5(x1))))))) = x1 >= x1 + 8 = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.71 979.51/239.71 4(4(5(2(4(2(2(x1))))))) = x1 + 12 >= x1 + 8 = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.71 979.51/239.71 0(2(5(3(4(x1))))) = x1 + 4 >= x1 + 4 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.71 problem: 979.51/239.71 strict: 979.51/239.71 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.71 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.71 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.71 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.71 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.71 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.71 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.71 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.71 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.71 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.71 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.71 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.71 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.72 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.72 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.72 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.72 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.72 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.72 weak: 979.51/239.72 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.72 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.72 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.72 Matrix Interpretation Processor: dim=1 979.51/239.72 979.51/239.72 max_matrix: 979.51/239.72 1 979.51/239.72 interpretation: 979.51/239.72 [3](x0) = x0, 979.51/239.72 979.51/239.72 [0](x0) = x0, 979.51/239.72 979.51/239.72 [4](x0) = x0, 979.51/239.72 979.51/239.72 [2](x0) = x0 + 2, 979.51/239.72 979.51/239.72 [1](x0) = x0, 979.51/239.72 979.51/239.72 [5](x0) = x0 + 1 979.51/239.72 orientation: 979.51/239.72 5(5(x1)) = x1 + 2 >= x1 + 7 = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.72 979.51/239.72 5(5(x1)) = x1 + 2 >= x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.72 979.51/239.72 2(5(5(x1))) = x1 + 4 >= x1 + 5 = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.72 979.51/239.72 5(2(4(x1))) = x1 + 3 >= x1 + 7 = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.72 979.51/239.72 5(5(2(x1))) = x1 + 4 >= x1 + 5 = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.72 979.51/239.72 5(5(3(x1))) = x1 + 2 >= x1 + 2 = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.72 979.51/239.72 5(5(5(x1))) = x1 + 3 >= x1 + 2 = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.72 979.51/239.72 2(5(0(4(x1)))) = x1 + 3 >= x1 + 3 = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.72 979.51/239.72 4(5(2(4(x1)))) = x1 + 3 >= x1 + 4 = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.72 979.51/239.72 4(5(5(5(x1)))) = x1 + 3 >= x1 + 6 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.72 979.51/239.72 2(5(5(3(4(x1))))) = x1 + 4 >= x1 + 3 = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.72 979.51/239.72 5(5(5(1(4(x1))))) = x1 + 3 >= x1 + 1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.72 979.51/239.72 0(4(4(5(5(5(x1)))))) = x1 + 3 >= x1 = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.72 979.51/239.72 4(1(5(5(0(4(x1)))))) = x1 + 2 >= x1 + 2 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.72 979.51/239.72 4(2(5(5(1(5(x1)))))) = x1 + 5 >= x1 + 7 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.72 979.51/239.72 5(2(5(5(0(4(x1)))))) = x1 + 5 >= x1 + 5 = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.72 979.51/239.72 5(5(2(4(5(0(x1)))))) = x1 + 5 >= x1 + 6 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.72 979.51/239.72 0(1(5(5(5(3(5(x1))))))) = x1 + 4 >= x1 + 7 = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.72 979.51/239.72 1(2(4(5(2(4(x1)))))) = x1 + 5 >= x1 + 1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.72 979.51/239.72 4(4(5(2(4(2(2(x1))))))) = x1 + 7 >= x1 + 7 = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.72 979.51/239.72 0(2(5(3(4(x1))))) = x1 + 3 >= x1 + 3 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.72 problem: 979.51/239.72 strict: 979.51/239.72 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.72 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.72 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.72 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.72 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.72 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.72 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.72 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.72 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.72 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.72 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.72 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.72 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.72 weak: 979.51/239.72 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.72 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.72 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.72 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.72 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.72 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.72 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.72 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.72 Splitting Processor: 979.51/239.72 strict: 979.51/239.72 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.72 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.72 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.72 weak: 979.51/239.73 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.73 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.73 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.73 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.73 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.73 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.73 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.73 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.73 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.73 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.73 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.73 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.73 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.73 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.73 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.73 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.73 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.73 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.73 Splitting Processor: 979.51/239.73 strict: 979.51/239.73 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.73 weak: 979.51/239.73 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.73 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.73 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.73 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.73 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.73 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.73 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.73 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.73 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.73 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.73 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.73 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.73 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.73 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.73 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.73 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.73 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.73 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.73 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.73 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.73 Matrix Interpretation Processor: dim=4 979.51/239.73 979.51/239.73 max_matrix: 979.51/239.73 [1 1 0 1] 979.51/239.73 [0 0 1 0] 979.51/239.73 [0 0 0 1] 979.51/239.73 [0 0 0 0] 979.51/239.73 interpretation: 979.51/239.73 [1 0 0 0] 979.51/239.73 [0 0 0 0] 979.51/239.73 [3](x0) = [0 0 0 0]x0 979.51/239.73 [0 0 0 0] , 979.51/239.73 979.51/239.73 [1 0 0 0] [0] 979.51/239.73 [0 0 0 0] [0] 979.51/239.73 [0](x0) = [0 0 0 0]x0 + [0] 979.51/239.73 [0 0 0 0] [1], 979.51/239.73 979.51/239.73 [1 0 0 0] [0] 979.51/239.73 [0 0 0 0] [0] 979.51/239.73 [4](x0) = [0 0 0 0]x0 + [1] 979.51/239.73 [0 0 0 0] [0], 979.51/239.73 979.51/239.73 [1 0 0 0] 979.51/239.73 [0 0 1 0] 979.51/239.73 [2](x0) = [0 0 0 1]x0 979.51/239.73 [0 0 0 0] , 979.51/239.73 979.51/239.73 [1 0 0 0] 979.51/239.73 [0 0 0 0] 979.51/239.73 [1](x0) = [0 0 0 1]x0 979.51/239.73 [0 0 0 0] , 979.51/239.73 979.51/239.73 [1 1 0 1] [0] 979.51/239.73 [0 0 0 0] [0] 979.51/239.73 [5](x0) = [0 0 0 0]x0 + [0] 979.51/239.73 [0 0 0 0] [1] 979.51/239.73 orientation: 979.51/239.73 [1 0 1 0] [1] [1 0 0 0] [0] 979.51/239.73 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.73 5(5(2(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.73 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.73 979.51/239.73 [1 0 0 0] [1] [1 0 0 0] [1] 979.51/239.73 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.73 5(2(4(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.75 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.75 979.51/239.75 [1 0 0 0] [1] [1 0 0 0] [1] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 4(5(2(4(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 979.51/239.75 [1 0 0 0] [3] [1 0 0 0] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] 979.51/239.75 5(5(2(4(5(0(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.75 [0 0 0 0] [1] [0 0 0 0] 979.51/239.75 979.51/239.75 [1 1 0 1] [1] [1 0 0 0] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] 979.51/239.75 5(5(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.75 [0 0 0 0] [1] [0 0 0 0] 979.51/239.75 979.51/239.75 [1 1 0 1] [2] [1 0 0 0] [1] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 5(5(5(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.75 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.75 979.51/239.75 [1 0 0 0] [1] [1 0 0 0] [0] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 2(5(5(3(4(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 979.51/239.75 [1 0 0 0] [2] [1 0 0 0] [1] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 5(5(5(1(4(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.75 [0 0 0 0] [1] [0 0 0 0] [0] 979.51/239.75 979.51/239.75 [1 1 0 1] [2] [1 0 0 0] [0] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 0(4(4(5(5(5(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.75 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.75 979.51/239.75 [1 0 0 0] [1] [1 0 0 0] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] 979.51/239.75 1(2(4(5(2(4(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] 979.51/239.75 979.51/239.75 [1 0 0 0] [1] [1 0 0 0] [1] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.75 979.51/239.75 [1 0 0 0] [0] [1 0 0 0] 979.51/239.75 [0 0 0 0] [0] [0 0 0 0] 979.51/239.75 0(2(5(3(4(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.76 [0 0 0 0] [1] [0 0 0 0] 979.51/239.76 979.51/239.76 [1 1 0 1] [1] [1 0 0 1] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 5(5(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.76 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.76 979.51/239.76 [1 1 0 1] [1] [1 0 0 0] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 2(5(5(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 979.51/239.76 [1 0 0 0] [1] [1 0 0 0] [1] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 5(5(3(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.76 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.76 979.51/239.76 [1 0 0 0] [1] [1 0 0 0] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 2(5(0(4(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 979.51/239.76 [1 1 0 1] [2] [1 1 0 1] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 4(5(5(5(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 979.51/239.76 [1 0 0 0] [2] [1 0 0 0] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 4(1(5(5(0(4(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 979.51/239.76 [1 1 0 1] [1] [1 1 0 1] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] 979.51/239.76 4(2(5(5(1(5(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] 979.51/239.76 979.51/239.76 [1 0 0 0] [2] [1 0 0 0] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 5(2(5(5(0(4(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.76 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.76 979.51/239.76 [1 1 0 1] [2] [1 1 0 1] [0] 979.51/239.76 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.76 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.76 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.76 problem: 979.51/239.76 strict: 979.51/239.76 979.51/239.76 weak: 979.51/239.76 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.76 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.76 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.77 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.77 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.77 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.77 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.77 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.77 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.77 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.77 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.77 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.77 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.77 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.77 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.77 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.77 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.77 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.77 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.77 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.77 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.77 Qed 979.51/239.77 979.51/239.77 strict: 979.51/239.77 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.77 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.77 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.77 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.77 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.77 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.77 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.77 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.77 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.77 weak: 979.51/239.77 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.77 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.77 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.77 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.77 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.77 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.77 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.77 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.77 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.77 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.77 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.77 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.77 Splitting Processor: 979.51/239.77 strict: 979.51/239.77 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.77 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.77 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.77 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.77 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.77 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.77 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.51/239.77 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.51/239.77 weak: 979.51/239.77 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.51/239.77 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.51/239.77 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.51/239.77 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.51/239.77 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.51/239.77 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.51/239.77 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.51/239.77 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.51/239.77 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.51/239.77 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.51/239.77 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.51/239.77 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.51/239.77 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.77 Matrix Interpretation Processor: dim=4 979.51/239.77 979.51/239.77 max_matrix: 979.51/239.77 [1 1 0 0] 979.51/239.77 [0 0 1 0] 979.51/239.77 [0 0 0 1] 979.51/239.77 [0 0 0 0] 979.51/239.77 interpretation: 979.51/239.77 [1 0 0 0] 979.51/239.77 [0 0 1 0] 979.51/239.79 [3](x0) = [0 0 0 0]x0 979.51/239.79 [0 0 0 0] , 979.51/239.79 979.51/239.79 [1 0 0 0] [0] 979.51/239.79 [0 0 1 0] [0] 979.51/239.79 [0](x0) = [0 0 0 0]x0 + [0] 979.51/239.79 [0 0 0 0] [1], 979.51/239.79 979.51/239.79 [1 0 0 0] [0] 979.51/239.79 [0 0 0 0] [0] 979.51/239.79 [4](x0) = [0 0 0 0]x0 + [1] 979.51/239.79 [0 0 0 0] [0], 979.51/239.79 979.51/239.79 [1 0 0 0] 979.51/239.79 [0 0 1 0] 979.51/239.79 [2](x0) = [0 0 0 1]x0 979.51/239.79 [0 0 0 0] , 979.51/239.79 979.51/239.79 [1 0 0 0] [0] 979.51/239.79 [0 0 0 0] [0] 979.51/239.79 [1](x0) = [0 0 0 0]x0 + [1] 979.51/239.79 [0 0 0 0] [0], 979.51/239.79 979.51/239.79 [1 1 0 0] [0] 979.51/239.79 [0 0 0 0] [1] 979.51/239.79 [5](x0) = [0 0 0 0]x0 + [0] 979.51/239.79 [0 0 0 0] [1] 979.51/239.79 orientation: 979.51/239.79 [1 0 1 0] [1] [1 0 1 0] [0] 979.51/239.79 [0 0 0 0] [1] [0 0 0 0] [0] 979.51/239.79 5(5(3(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.51/239.79 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.79 979.51/239.79 [1 1 0 0] [1] [1 0 0 0] [1] 979.51/239.79 [0 0 0 0] [1] [0 0 0 0] [0] 979.51/239.79 5(5(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.51/239.79 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.79 979.51/239.79 [1 1 0 0] [1] [1 0 0 0] [0] 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 2(5(5(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 979.51/239.79 [1 0 0 0] [1] [1 0 0 0] [0] 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 2(5(0(4(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 979.51/239.79 [1 1 0 0] [2] [1 1 0 0] [0] 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 4(5(5(5(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 979.51/239.79 [1 0 0 0] [2] [1 0 0 0] [0] 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 4(1(5(5(0(4(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] [0] 979.51/239.79 979.51/239.79 [1 1 0 0] [1] [1 1 0 0] 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] 979.51/239.79 4(2(5(5(1(5(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.51/239.79 [0 0 0 0] [0] [0 0 0 0] 979.51/239.79 979.51/239.79 [1 0 0 0] [2] [1 0 0 0] [1] 979.51/239.79 [0 0 0 0] [1] [0 0 0 0] [1] 979.51/239.79 5(2(5(5(0(4(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 979.61/239.80 [1 1 0 0] [2] [1 1 0 0] [1] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 979.61/239.80 [1 0 1 0] [1] [1 0 1 0] [0] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 5(5(2(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 979.61/239.80 [1 0 0 0] [1] [1 0 0 0] [0] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [0] 979.61/239.80 5(2(4(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 979.61/239.80 [1 0 0 0] [1] [1 0 0 0] [1] 979.61/239.80 [0 0 0 0] [0] [0 0 0 0] [0] 979.61/239.80 4(5(2(4(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.61/239.80 [0 0 0 0] [0] [0 0 0 0] [0] 979.61/239.80 979.61/239.80 [1 0 1 0] [2] [1 0 0 0] [0] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 5(5(2(4(5(0(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [0] 979.61/239.80 979.61/239.80 [1 1 0 0] [1] [1 0 0 0] [0] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 5(5(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [0] 979.61/239.80 979.61/239.80 [1 1 0 0] [2] [1 0 0 0] [1] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 5(5(5(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 979.61/239.80 [1 0 0 0] [2] [1 0 0 0] [0] 979.61/239.80 [0 0 0 0] [0] [0 0 0 0] [0] 979.61/239.80 2(5(5(3(4(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.61/239.80 [0 0 0 0] [0] [0 0 0 0] [0] 979.61/239.80 979.61/239.80 [1 0 0 0] [2] [1 0 0 0] [1] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [0] 979.61/239.80 5(5(5(1(4(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [0] 979.61/239.80 979.61/239.80 [1 1 0 0] [2] [1 0 0 0] [0] 979.61/239.80 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.80 0(4(4(5(5(5(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.61/239.82 [0 0 0 0] [1] [0 0 0 0] [1] 979.61/239.82 979.61/239.82 [1 0 0 0] [1] [1 0 0 0] 979.61/239.82 [0 0 0 0] [0] [0 0 0 0] 979.61/239.82 1(2(4(5(2(4(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.61/239.82 [0 0 0 0] [0] [0 0 0 0] 979.61/239.82 979.61/239.82 [1 0 0 0] [1] [1 0 0 0] [1] 979.61/239.82 [0 0 0 0] [0] [0 0 0 0] [0] 979.61/239.82 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.61/239.82 [0 0 0 0] [0] [0 0 0 0] [0] 979.61/239.82 979.61/239.82 [1 0 0 0] [1] [1 0 0 0] 979.61/239.82 [0 0 0 0] [1] [0 0 0 0] 979.61/239.82 0(2(5(3(4(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.61/239.82 [0 0 0 0] [1] [0 0 0 0] 979.61/239.82 problem: 979.61/239.82 strict: 979.61/239.82 979.61/239.82 weak: 979.61/239.82 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.61/239.82 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.61/239.82 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.61/239.82 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.61/239.82 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.61/239.82 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.61/239.82 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.61/239.82 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.61/239.82 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.61/239.82 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.61/239.82 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.61/239.82 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.61/239.82 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.61/239.82 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.61/239.82 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.61/239.82 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.61/239.82 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.61/239.82 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.61/239.82 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.61/239.82 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.61/239.82 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.61/239.82 Qed 979.61/239.82 979.61/239.82 strict: 979.61/239.82 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.61/239.82 weak: 979.61/239.82 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.61/239.82 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.61/239.82 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.61/239.82 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.61/239.82 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.61/239.82 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.61/239.82 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.61/239.82 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.61/239.82 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.61/239.82 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.61/239.82 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.61/239.82 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.61/239.82 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.61/239.82 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.61/239.82 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.61/239.82 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.61/239.82 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.61/239.82 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.61/239.83 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.61/239.83 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.61/239.83 Matrix Interpretation Processor: dim=3 979.61/239.83 979.61/239.83 max_matrix: 979.61/239.83 [1 2 0] 979.61/239.83 [0 0 1] 979.61/239.83 [0 0 0] 979.61/239.83 interpretation: 979.61/239.83 [1 0 0] 979.61/239.83 [3](x0) = [0 0 0]x0 979.61/239.83 [0 0 0] , 979.61/239.83 979.61/239.83 [1 0 0] [0] 979.61/239.83 [0](x0) = [0 0 0]x0 + [0] 979.61/239.83 [0 0 0] [1], 979.61/239.83 979.61/239.83 [1 0 0] [0] 979.61/239.83 [4](x0) = [0 0 0]x0 + [0] 979.61/239.83 [0 0 0] [1], 979.61/239.83 979.61/239.83 [1 0 0] [0] 979.61/239.83 [2](x0) = [0 0 1]x0 + [0] 979.61/239.83 [0 0 0] [1], 979.61/239.83 979.61/239.83 [1 0 0] 979.61/239.83 [1](x0) = [0 0 0]x0 979.61/239.83 [0 0 0] , 979.61/239.83 979.61/239.83 [1 2 0] [0] 979.61/239.83 [5](x0) = [0 0 0]x0 + [0] 979.61/239.83 [0 0 0] [1] 979.61/239.83 orientation: 979.61/239.83 [1 2 0] [0] [1 0 0] [0] 979.61/239.83 5(5(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 2 0] [0] [1 0 0] [0] 979.61/239.83 2(5(5(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 0 0] [0] [1 0 0] [0] 979.61/239.83 2(5(0(4(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 2 0] [0] [1 2 0] 979.61/239.83 4(5(5(5(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] 979.61/239.83 979.61/239.83 [1 0 0] [0] [1 0 0] 979.61/239.83 4(1(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] 979.61/239.83 979.61/239.83 [1 2 0] [0] [1 2 0] [0] 979.61/239.83 4(2(5(5(1(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 0 0] [2] [1 0 0] [0] 979.61/239.83 5(2(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 2 0] [0] [1 2 0] [0] 979.61/239.83 0(1(5(5(5(3(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 0 2] [0] [1 0 0] [0] 979.61/239.83 5(5(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 0 0] [2] [1 0 0] [0] 979.61/239.83 5(2(4(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.61/239.83 [0 0 0] [1] [0 0 0] [1] 979.61/239.83 979.61/239.83 [1 0 0] [2] [1 0 0] [2] 979.61/239.84 4(5(2(4(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 979.61/239.84 [1 0 0] [2] [1 0 0] [0] 979.61/239.84 5(5(2(4(5(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 979.61/239.84 [1 2 0] [0] [1 0 0] 979.61/239.84 5(5(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] 979.61/239.84 979.61/239.84 [1 2 0] [0] [1 0 0] [0] 979.61/239.84 5(5(5(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 979.61/239.84 [1 0 0] [0] [1 0 0] [0] 979.61/239.84 2(5(5(3(4(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 979.61/239.84 [1 0 0] [0] [1 0 0] 979.61/239.84 5(5(5(1(4(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] 979.61/239.84 979.61/239.84 [1 2 0] [0] [1 0 0] [0] 979.61/239.84 0(4(4(5(5(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 979.61/239.84 [1 0 0] [2] [1 0 0] 979.61/239.84 1(2(4(5(2(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.61/239.84 [0 0 0] [0] [0 0 0] 979.61/239.84 979.61/239.84 [1 0 0] [2] [1 0 0] [0] 979.61/239.84 4(4(5(2(4(2(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 979.61/239.84 [1 0 0] [0] [1 0 0] 979.61/239.84 0(2(5(3(4(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] 979.61/239.84 979.61/239.84 [1 0 0] [0] [1 0 0] [0] 979.61/239.84 5(5(3(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.61/239.84 [0 0 0] [1] [0 0 0] [1] 979.61/239.84 problem: 979.61/239.84 strict: 979.61/239.84 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.61/239.84 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.61/239.84 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.61/239.84 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.61/239.84 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.61/239.84 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.61/239.84 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.61/239.84 weak: 979.61/239.84 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.61/239.84 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.61/239.84 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.61/239.84 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.61/239.84 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.61/239.84 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.61/239.84 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.61/239.85 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.61/239.85 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.61/239.85 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.61/239.85 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.61/239.85 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.61/239.85 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.61/239.85 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.61/239.85 Matrix Interpretation Processor: dim=5 979.61/239.85 979.61/239.85 max_matrix: 979.61/239.85 [1 0 1 0 0] 979.61/239.85 [0 0 0 0 1] 979.61/239.85 [0 0 0 1 0] 979.61/239.85 [0 0 0 0 1] 979.61/239.85 [0 0 0 0 0] 979.61/239.85 interpretation: 979.61/239.85 [1 0 0 0 0] 979.61/239.85 [0 0 0 0 0] 979.61/239.85 [3](x0) = [0 0 0 0 0]x0 979.61/239.85 [0 0 0 0 1] 979.61/239.85 [0 0 0 0 0] , 979.61/239.85 979.61/239.85 [1 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0] 979.61/239.85 [0](x0) = [0 0 0 0 0]x0 + [0] 979.61/239.85 [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1], 979.61/239.85 979.61/239.85 [1 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1] 979.61/239.85 [4](x0) = [0 0 0 0 0]x0 + [0] 979.61/239.85 [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0], 979.61/239.85 979.61/239.85 [1 0 0 0 0] 979.61/239.85 [0 0 0 0 1] 979.61/239.85 [2](x0) = [0 0 0 0 0]x0 979.61/239.85 [0 0 0 0 0] 979.61/239.85 [0 0 0 0 0] , 979.61/239.85 979.61/239.85 [1 0 0 0 0] 979.61/239.85 [0 0 0 0 1] 979.61/239.85 [1](x0) = [0 0 0 0 0]x0 979.61/239.85 [0 0 0 0 0] 979.61/239.85 [0 0 0 0 0] , 979.61/239.85 979.61/239.85 [1 0 1 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0] 979.61/239.85 [5](x0) = [0 0 0 1 0]x0 + [0] 979.61/239.85 [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1] 979.61/239.85 orientation: 979.61/239.85 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 5(5(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.85 979.61/239.85 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.85 2(5(5(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 979.61/239.85 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.85 2(5(0(4(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 979.61/239.85 [1 0 1 1 0] [0] [1 0 1 0 0] [0] 979.61/239.85 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.85 4(5(5(5(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.85 979.61/239.85 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.88 4(1(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 979.61/239.88 [1 0 1 0 0] [0] [1 0 1 0 0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] 979.61/239.88 4(2(5(5(1(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] 979.61/239.88 979.61/239.88 [1 0 1 0 0] [1] [1 0 1 0 0] [0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.88 979.61/239.88 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 5(2(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.88 979.61/239.88 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 5(5(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.88 979.61/239.88 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 5(2(4(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.88 979.61/239.88 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.61/239.88 4(5(2(4(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.61/239.88 979.61/239.88 [1 0 0 0 0] [0] [1 0 0 0 0] 979.61/239.88 [0 0 0 0 0] [0] [0 0 0 0 0] 979.61/239.88 5(5(2(4(5(0(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.90 979.71/239.90 [1 0 1 1 0] [0] [1 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.90 5(5(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.90 979.71/239.90 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 5(5(5(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.90 979.71/239.90 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.90 2(5(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 979.71/239.90 [1 0 0 0 0] [0] [1 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.90 5(5(5(1(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.90 979.71/239.90 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 0(4(4(5(5(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.90 979.71/239.90 [1 0 0 0 0] [1 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [0 0 0 0 0] 979.71/239.90 1(2(4(5(2(4(x1)))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0 0 0 0 0] 979.71/239.90 [0 0 0 0 0] [0 0 0 0 0] 979.71/239.90 979.71/239.90 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.90 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.90 979.71/239.90 [1 0 0 0 0] [0] [1 0 0 0 0] 979.71/239.91 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.91 0(2(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.71/239.91 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.91 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.91 979.71/239.91 [1 0 0 0 1] [0] [1 0 0 0 0] [0] 979.71/239.91 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.91 5(5(3(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.71/239.91 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.91 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.91 problem: 979.71/239.91 strict: 979.71/239.91 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.71/239.91 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.71/239.91 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.71/239.91 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.71/239.91 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.71/239.91 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.71/239.91 weak: 979.71/239.91 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.71/239.91 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.71/239.91 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.71/239.91 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.71/239.91 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.71/239.91 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.71/239.91 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.71/239.91 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.71/239.91 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.71/239.91 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.71/239.91 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.71/239.91 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.71/239.91 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.71/239.91 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.71/239.91 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.71/239.91 Matrix Interpretation Processor: dim=3 979.71/239.91 979.71/239.91 max_matrix: 979.71/239.91 [1 2 0] 979.71/239.91 [0 0 1] 979.71/239.91 [0 0 0] 979.71/239.91 interpretation: 979.71/239.91 [1 0 0] 979.71/239.91 [3](x0) = [0 0 0]x0 979.71/239.91 [0 0 0] , 979.71/239.91 979.71/239.91 [1 0 0] [0] 979.71/239.91 [0](x0) = [0 0 0]x0 + [0] 979.71/239.91 [0 0 0] [1], 979.71/239.91 979.71/239.91 [1 0 0] 979.71/239.91 [4](x0) = [0 0 0]x0 979.71/239.91 [0 0 0] , 979.71/239.91 979.71/239.91 [1 0 0] 979.71/239.91 [2](x0) = [0 0 0]x0 979.71/239.91 [0 0 0] , 979.71/239.91 979.71/239.91 [1 0 0] 979.71/239.91 [1](x0) = [0 0 0]x0 979.71/239.91 [0 0 0] , 979.71/239.91 979.71/239.91 [1 2 0] [0] 979.71/239.91 [5](x0) = [0 0 1]x0 + [0] 979.71/239.91 [0 0 0] [1] 979.71/239.91 orientation: 979.71/239.91 [1 2 2] [0] [1 0 0] [0] 979.71/239.91 5(5(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.71/239.91 [0 0 0] [1] [0 0 0] [1] 979.71/239.91 979.71/239.91 [1 2 2] [1 0 0] 979.71/239.91 2(5(5(x1))) = [0 0 0]x1 >= [0 0 0]x1 = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.71/239.91 [0 0 0] [0 0 0] 979.71/239.91 979.71/239.91 [1 0 0] [1 0 0] 979.71/239.91 2(5(0(4(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.71/239.91 [0 0 0] [0 0 0] 979.71/239.92 979.71/239.92 [1 2 2] [2] [1 2 0] 979.71/239.92 4(5(5(5(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.71/239.92 [0 0 0] [0] [0 0 0] 979.71/239.92 979.71/239.92 [1 0 0] [2] [1 0 0] 979.71/239.92 4(1(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.71/239.92 [0 0 0] [0] [0 0 0] 979.71/239.92 979.71/239.92 [1 2 0] [1 2 0] 979.71/239.92 4(2(5(5(1(5(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.71/239.92 [0 0 0] [0 0 0] 979.71/239.92 979.71/239.92 [1 2 0] [2] [1 2 0] [0] 979.71/239.92 0(1(5(5(5(3(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] [1] 979.71/239.92 979.71/239.92 [1 0 0] [2] [1 0 0] [0] 979.71/239.92 5(2(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] [1] 979.71/239.92 979.71/239.92 [1 0 0] [0] [1 0 0] [0] 979.71/239.92 5(5(2(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] [1] 979.71/239.92 979.71/239.92 [1 0 0] [0] [1 0 0] [0] 979.71/239.92 5(2(4(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] [1] 979.71/239.92 979.71/239.92 [1 0 0] [1 0 0] 979.71/239.92 4(5(2(4(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.71/239.92 [0 0 0] [0 0 0] 979.71/239.92 979.71/239.92 [1 0 0] [0] [1 0 0] 979.71/239.92 5(5(2(4(5(0(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] 979.71/239.92 979.71/239.92 [1 2 2] [0] [1 0 0] 979.71/239.92 5(5(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] 979.71/239.92 979.71/239.92 [1 2 2] [2] [1 0 0] [0] 979.71/239.92 5(5(5(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] [1] 979.71/239.92 979.71/239.92 [1 0 0] [1 0 0] 979.71/239.92 2(5(5(3(4(x1))))) = [0 0 0]x1 >= [0 0 0]x1 = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.71/239.92 [0 0 0] [0 0 0] 979.71/239.92 979.71/239.92 [1 0 0] [2] [1 0 0] 979.71/239.92 5(5(5(1(4(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.71/239.92 [0 0 0] [1] [0 0 0] 979.71/239.92 979.71/239.92 [1 2 2] [2] [1 0 0] [0] 979.71/239.92 0(4(4(5(5(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.71/239.93 [0 0 0] [1] [0 0 0] [1] 979.71/239.93 979.71/239.93 [1 0 0] [1 0 0] 979.71/239.93 1(2(4(5(2(4(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.71/239.93 [0 0 0] [0 0 0] 979.71/239.93 979.71/239.93 [1 0 0] [1 0 0] 979.71/239.93 4(4(5(2(4(2(2(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.71/239.93 [0 0 0] [0 0 0] 979.71/239.93 979.71/239.93 [1 0 0] [0] [1 0 0] 979.71/239.93 0(2(5(3(4(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.71/239.93 [0 0 0] [1] [0 0 0] 979.71/239.93 979.71/239.93 [1 0 0] [0] [1 0 0] [0] 979.71/239.93 5(5(3(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.71/239.93 [0 0 0] [1] [0 0 0] [1] 979.71/239.93 problem: 979.71/239.93 strict: 979.71/239.93 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.71/239.93 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.71/239.93 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.71/239.93 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.71/239.93 weak: 979.71/239.93 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.71/239.93 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.71/239.93 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.71/239.93 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.71/239.93 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.71/239.93 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.71/239.93 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.71/239.93 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.71/239.93 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.71/239.93 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.71/239.93 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.71/239.93 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.71/239.93 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.71/239.93 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.71/239.93 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.71/239.93 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.71/239.93 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.71/239.93 Matrix Interpretation Processor: dim=5 979.71/239.93 979.71/239.93 max_matrix: 979.71/239.93 [1 0 1 0 0] 979.71/239.93 [0 0 0 1 1] 979.71/239.93 [0 0 0 1 1] 979.71/239.93 [0 0 0 0 1] 979.71/239.93 [0 0 0 0 0] 979.71/239.93 interpretation: 979.71/239.93 [1 0 0 0 0] 979.71/239.93 [0 0 0 0 0] 979.71/239.93 [3](x0) = [0 0 0 1 0]x0 979.71/239.93 [0 0 0 0 0] 979.71/239.93 [0 0 0 0 0] , 979.71/239.93 979.71/239.93 [1 0 0 0 0] [0] 979.71/239.93 [0 0 0 0 0] [0] 979.71/239.93 [0](x0) = [0 0 0 0 0]x0 + [0] 979.71/239.93 [0 0 0 0 0] [0] 979.71/239.93 [0 0 0 0 0] [1], 979.71/239.93 979.71/239.93 [1 0 0 0 0] [0] 979.71/239.93 [0 0 0 1 1] [0] 979.71/239.93 [4](x0) = [0 0 0 0 0]x0 + [0] 979.71/239.93 [0 0 0 0 0] [1] 979.71/239.93 [0 0 0 0 0] [0], 979.71/239.93 979.71/239.93 [1 0 0 0 0] 979.71/239.93 [0 0 0 0 1] 979.71/239.93 [2](x0) = [0 0 0 1 0]x0 979.71/239.93 [0 0 0 0 1] 979.71/239.93 [0 0 0 0 0] , 979.71/239.93 979.71/239.93 [1 0 0 0 0] 979.71/239.93 [0 0 0 0 0] 979.71/239.93 [1](x0) = [0 0 0 0 0]x0 979.71/239.93 [0 0 0 0 1] 979.71/239.93 [0 0 0 0 0] , 979.71/239.93 979.71/239.95 [1 0 1 0 0] [0] 979.71/239.95 [0 0 0 0 0] [0] 979.71/239.95 [5](x0) = [0 0 0 1 1]x0 + [0] 979.71/239.95 [0 0 0 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] 979.71/239.95 orientation: 979.71/239.95 [1 0 1 1 1] [0] [1 0 0 0 1] [0] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 5(5(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 979.71/239.95 [1 0 1 1 1] [0] [1 0 0 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 2(5(5(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 979.71/239.95 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 2(5(0(4(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 979.71/239.95 [1 0 1 0 0] [1] [1 0 1 0 0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.95 4(2(5(5(1(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.95 979.71/239.95 [1 0 1 1 1] [1] [1 0 1 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.71/239.95 4(5(5(5(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 979.71/239.95 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.71/239.95 4(1(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 979.71/239.95 [1 0 1 0 0] [1] [1 0 1 0 0] [1] 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.71/239.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 979.71/239.97 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 5(2(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 979.71/239.97 [1 0 0 1 1] [0] [1 0 0 1 0] [0] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 5(5(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 979.71/239.97 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 5(2(4(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 979.71/239.97 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 4(5(2(4(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 979.71/239.97 [1 0 0 0 0] [1] [1 0 0 0 0] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.97 5(5(2(4(5(0(x1)))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.97 979.71/239.97 [1 0 1 1 1] [0] [1 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 5(5(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.71/239.97 979.71/239.97 [1 0 1 1 1] [1] [1 0 0 0 0] [1] 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 5(5(5(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.71/239.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.97 979.71/239.97 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.71/239.97 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.99 2(5(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.99 979.71/239.99 [1 0 0 0 0] [1] [1 0 0 0 0] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 5(5(5(1(4(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.99 979.71/239.99 [1 0 1 1 1] [1] [1 0 0 0 0] [0] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.99 0(4(4(5(5(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.99 979.71/239.99 [1 0 0 0 0] [1] [1 0 0 0 0] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 1(2(4(5(2(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 979.71/239.99 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.99 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.99 979.71/239.99 [1 0 0 0 0] [1] [1 0 0 0 0] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 0(2(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] 979.71/239.99 979.71/239.99 [1 0 0 1 0] [0] [1 0 0 0 0] [0] 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.99 5(5(3(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.71/239.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.71/239.99 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.71/239.99 problem: 979.71/239.99 strict: 979.71/239.99 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.71/239.99 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.71/239.99 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.71/239.99 weak: 979.71/239.99 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.71/239.99 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.71/239.99 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.81/240.00 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.81/240.00 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.81/240.00 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.81/240.00 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.81/240.00 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.81/240.00 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.81/240.00 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.81/240.00 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.81/240.00 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.81/240.00 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.81/240.00 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.81/240.00 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.81/240.00 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.81/240.00 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.81/240.00 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.81/240.00 Matrix Interpretation Processor: dim=5 979.81/240.00 979.81/240.00 max_matrix: 979.81/240.00 [1 1 0 1 0] 979.81/240.00 [0 0 1 1 0] 979.81/240.00 [0 0 0 1 0] 979.81/240.00 [0 0 0 0 1] 979.81/240.00 [0 0 0 0 0] 979.81/240.00 interpretation: 979.81/240.00 [1 0 0 0 0] 979.81/240.00 [0 0 0 0 0] 979.81/240.00 [3](x0) = [0 0 0 0 0]x0 979.81/240.00 [0 0 0 0 0] 979.81/240.00 [0 0 0 0 0] , 979.81/240.00 979.81/240.00 [1 0 0 0 0] [0] 979.81/240.00 [0 0 0 0 0] [0] 979.81/240.00 [0](x0) = [0 0 0 0 0]x0 + [0] 979.81/240.00 [0 0 0 0 0] [0] 979.81/240.00 [0 0 0 0 0] [1], 979.81/240.00 979.81/240.00 [1 0 0 0 0] 979.81/240.00 [0 0 0 1 0] 979.81/240.00 [4](x0) = [0 0 0 1 0]x0 979.81/240.00 [0 0 0 0 0] 979.81/240.00 [0 0 0 0 0] , 979.81/240.00 979.81/240.00 [1 0 0 1 0] 979.81/240.00 [0 0 1 0 0] 979.81/240.00 [2](x0) = [0 0 0 0 0]x0 979.81/240.00 [0 0 0 0 0] 979.81/240.00 [0 0 0 0 0] , 979.81/240.00 979.81/240.00 [1 0 0 0 0] 979.81/240.00 [0 0 1 1 0] 979.81/240.00 [1](x0) = [0 0 0 0 0]x0 979.81/240.00 [0 0 0 0 0] 979.81/240.00 [0 0 0 0 0] , 979.81/240.00 979.81/240.00 [1 1 0 0 0] [0] 979.81/240.00 [0 0 0 1 0] [0] 979.81/240.00 [5](x0) = [0 0 0 0 0]x0 + [0] 979.81/240.00 [0 0 0 0 1] [0] 979.81/240.00 [0 0 0 0 0] [1] 979.81/240.00 orientation: 979.81/240.00 [1 1 0 1 0] [0] [1 0 0 0 0] [0] 979.81/240.00 [0 0 0 0 1] [0] [0 0 0 0 0] [0] 979.81/240.00 5(5(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.81/240.00 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.81/240.00 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.00 979.81/240.00 [1 1 0 1 0] [1] [1 0 0 1 0] 979.81/240.00 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.00 2(5(5(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.81/240.00 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.00 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.00 979.81/240.00 [1 0 0 0 0] [1] [1 0 0 0 0] 979.81/240.00 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.00 2(5(0(4(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.81/240.00 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.00 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.02 979.81/240.02 [1 1 0 0 1] [1] [1 1 0 0 1] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.02 4(2(5(5(1(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.02 979.81/240.02 [1 1 0 1 1] [0] [1 1 0 0 0] 979.81/240.02 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.02 4(5(5(5(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.02 979.81/240.02 [1 0 0 0 0] [1 0 0 0 0] 979.81/240.02 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.02 4(1(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.02 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.02 979.81/240.02 [1 1 0 0 0] [0] [1 1 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.02 979.81/240.02 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 5(2(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.02 979.81/240.02 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 5(5(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.02 979.81/240.02 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 5(2(4(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.81/240.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.02 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.02 979.81/240.02 [1 0 0 1 0] [1 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.04 4(5(2(4(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.04 979.81/240.04 [1 0 0 0 0] [1] [1 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.04 5(5(2(4(5(0(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 979.81/240.04 [1 1 0 1 0] [0] [1 0 0 0 0] 979.81/240.04 [0 0 0 0 1] [0] [0 0 0 0 0] 979.81/240.04 5(5(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 979.81/240.04 [1 1 0 1 1] [0] [1 0 0 0 0] [0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.81/240.04 5(5(5(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.04 979.81/240.04 [1 0 0 0 0] [1] [1 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.04 2(5(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.04 979.81/240.04 [1 0 0 1 0] [0] [1 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 5(5(5(1(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.04 979.81/240.04 [1 1 0 1 1] [0] [1 0 0 0 0] [0] 979.81/240.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.04 0(4(4(5(5(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.04 979.81/240.04 [1 0 0 1 0] [1 0 0 0 0] 979.81/240.04 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.04 1(2(4(5(2(4(x1)))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.81/240.04 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.06 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.06 979.81/240.06 [1 0 0 1 0] [1 0 0 0 0] 979.81/240.06 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.06 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.81/240.06 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.06 [0 0 0 0 0] [0 0 0 0 0] 979.81/240.06 979.81/240.06 [1 0 0 0 0] [0] [1 0 0 0 0] 979.81/240.06 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.06 0(2(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.81/240.06 [0 0 0 0 0] [0] [0 0 0 0 0] 979.81/240.06 [0 0 0 0 0] [1] [0 0 0 0 0] 979.81/240.06 979.81/240.06 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.81/240.06 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.81/240.06 5(5(3(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.81/240.06 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.81/240.06 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.81/240.06 problem: 979.81/240.06 strict: 979.81/240.06 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.81/240.06 weak: 979.81/240.06 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.81/240.06 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.81/240.06 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.81/240.06 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.81/240.06 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.81/240.06 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.81/240.06 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.81/240.06 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.81/240.06 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.81/240.06 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.81/240.06 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.81/240.06 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.81/240.06 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.81/240.06 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.81/240.06 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.81/240.06 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.81/240.06 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.81/240.06 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.81/240.06 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.81/240.06 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.81/240.06 Matrix Interpretation Processor: dim=4 979.81/240.06 979.81/240.06 max_matrix: 979.81/240.06 [1 1 0 0] 979.81/240.06 [0 0 1 1] 979.81/240.06 [0 0 0 1] 979.81/240.06 [0 0 0 0] 979.81/240.06 interpretation: 979.81/240.06 [1 0 0 0] 979.81/240.06 [0 0 1 0] 979.81/240.06 [3](x0) = [0 0 0 0]x0 979.81/240.06 [0 0 0 0] , 979.81/240.06 979.81/240.06 [1 0 0 0] [0] 979.81/240.06 [0 0 1 0] [0] 979.81/240.06 [0](x0) = [0 0 0 0]x0 + [0] 979.81/240.06 [0 0 0 0] [1], 979.81/240.06 979.81/240.06 [1 0 0 0] [0] 979.81/240.06 [0 0 0 0] [0] 979.81/240.06 [4](x0) = [0 0 0 0]x0 + [1] 979.81/240.06 [0 0 0 0] [0], 979.81/240.06 979.81/240.06 [1 0 0 0] 979.81/240.06 [0 0 1 0] 979.81/240.06 [2](x0) = [0 0 0 1]x0 979.81/240.07 [0 0 0 0] , 979.81/240.07 979.81/240.07 [1 0 0 0] 979.81/240.07 [0 0 0 0] 979.81/240.07 [1](x0) = [0 0 0 1]x0 979.81/240.07 [0 0 0 0] , 979.81/240.07 979.81/240.07 [1 1 0 0] [0] 979.81/240.07 [0 0 0 1] [1] 979.81/240.07 [5](x0) = [0 0 0 0]x0 + [0] 979.81/240.07 [0 0 0 0] [1] 979.81/240.07 orientation: 979.81/240.07 [1 1 0 1] [1] [1 0 0 1] [0] 979.81/240.07 [0 0 0 0] [2] [0 0 0 0] [0] 979.81/240.07 5(5(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.81/240.07 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.07 979.81/240.07 [1 1 0 1] [1] [1 0 0 0] [0] 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 2(5(5(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 979.81/240.07 [1 0 0 0] [1] [1 0 0 0] [0] 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 2(5(0(4(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 979.81/240.07 [1 1 0 0] [1] [1 1 0 0] 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] 979.81/240.07 4(2(5(5(1(5(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] 979.81/240.07 979.81/240.07 [1 1 0 1] [3] [1 1 0 0] [0] 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 4(5(5(5(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 979.81/240.07 [1 0 0 0] [3] [1 0 0 0] [0] 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 4(1(5(5(0(4(x1)))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.81/240.07 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.07 979.81/240.07 [1 1 0 0] [3] [1 1 0 0] [1] 979.81/240.07 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.07 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.81/240.07 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.07 979.81/240.07 [1 0 0 0] [3] [1 0 0 0] [0] 979.81/240.07 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.07 5(2(5(5(0(4(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.81/240.07 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.07 979.81/240.07 [1 0 1 0] [1] [1 0 1 0] [0] 979.81/240.09 [0 0 0 0] [2] [0 0 0 0] [0] 979.81/240.09 5(5(2(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.09 979.81/240.09 [1 0 0 0] [1] [1 0 0 0] [0] 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [0] 979.81/240.09 5(2(4(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.09 979.81/240.09 [1 0 0 0] [1] [1 0 0 0] [1] 979.81/240.09 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.09 4(5(2(4(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.81/240.09 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.09 979.81/240.09 [1 0 1 0] [2] [1 0 0 0] 979.81/240.09 [0 0 0 0] [2] [0 0 0 0] 979.81/240.09 5(5(2(4(5(0(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] 979.81/240.09 979.81/240.09 [1 1 0 1] [1] [1 0 0 0] [0] 979.81/240.09 [0 0 0 0] [2] [0 0 0 0] [1] 979.81/240.09 5(5(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [0] 979.81/240.09 979.81/240.09 [1 1 0 1] [3] [1 0 0 0] [1] 979.81/240.09 [0 0 0 0] [2] [0 0 0 0] [1] 979.81/240.09 5(5(5(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.09 979.81/240.09 [1 0 0 0] [2] [1 0 0 0] [0] 979.81/240.09 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.09 2(5(5(3(4(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.81/240.09 [0 0 0 0] [0] [0 0 0 0] [0] 979.81/240.09 979.81/240.09 [1 0 0 0] [3] [1 0 0 0] [1] 979.81/240.09 [0 0 0 0] [2] [0 0 0 0] [0] 979.81/240.09 5(5(5(1(4(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [0] 979.81/240.09 979.81/240.09 [1 1 0 1] [3] [1 0 0 0] [0] 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.09 0(4(4(5(5(5(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.81/240.09 [0 0 0 0] [1] [0 0 0 0] [1] 979.81/240.09 979.81/240.09 [1 0 0 0] [1] [1 0 0 0] 979.81/240.09 [0 0 0 0] [0] [0 0 0 0] 979.81/240.09 1(2(4(5(2(4(x1)))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.10 [0 0 0 0] [0] [0 0 0 0] 979.91/240.10 979.91/240.10 [1 0 0 0] [1] [1 0 0 0] [1] 979.91/240.10 [0 0 0 0] [0] [0 0 0 0] [0] 979.91/240.10 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.10 [0 0 0 0] [0] [0 0 0 0] [0] 979.91/240.10 979.91/240.10 [1 0 0 0] [1] [1 0 0 0] 979.91/240.10 [0 0 0 0] [1] [0 0 0 0] 979.91/240.10 0(2(5(3(4(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.10 [0 0 0 0] [1] [0 0 0 0] 979.91/240.10 979.91/240.10 [1 0 1 0] [1] [1 0 1 0] [0] 979.91/240.10 [0 0 0 0] [2] [0 0 0 0] [0] 979.91/240.10 5(5(3(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.10 [0 0 0 0] [1] [0 0 0 0] [1] 979.91/240.10 problem: 979.91/240.10 strict: 979.91/240.10 979.91/240.10 weak: 979.91/240.10 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.10 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.91/240.10 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.91/240.10 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.91/240.10 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.91/240.10 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.91/240.10 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.91/240.10 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.91/240.10 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.91/240.10 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.10 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.10 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.10 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.10 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.10 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.10 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.10 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.10 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.10 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.10 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.10 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.10 Qed 979.91/240.10 979.91/240.10 strict: 979.91/240.10 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.10 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.91/240.10 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.91/240.10 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.10 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.91/240.10 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.91/240.10 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.91/240.10 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.91/240.10 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.91/240.10 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.91/240.10 weak: 979.91/240.10 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.10 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.10 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.10 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.10 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.10 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.10 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.10 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.11 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.11 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.11 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.11 Matrix Interpretation Processor: dim=3 979.91/240.11 979.91/240.11 max_matrix: 979.91/240.11 [1 2 0] 979.91/240.11 [0 0 1] 979.91/240.11 [0 0 0] 979.91/240.11 interpretation: 979.91/240.11 [1 0 0] 979.91/240.11 [3](x0) = [0 0 0]x0 979.91/240.11 [0 0 0] , 979.91/240.11 979.91/240.11 [1 0 0] [0] 979.91/240.11 [0](x0) = [0 0 0]x0 + [0] 979.91/240.11 [0 0 0] [1], 979.91/240.11 979.91/240.11 [1 1 0] 979.91/240.11 [4](x0) = [0 0 0]x0 979.91/240.11 [0 0 0] , 979.91/240.11 979.91/240.11 [1 0 0] 979.91/240.11 [2](x0) = [0 0 0]x0 979.91/240.11 [0 0 0] , 979.91/240.11 979.91/240.11 [1 0 0] 979.91/240.11 [1](x0) = [0 0 0]x0 979.91/240.11 [0 0 0] , 979.91/240.11 979.91/240.11 [1 2 0] [0] 979.91/240.11 [5](x0) = [0 0 1]x0 + [0] 979.91/240.11 [0 0 0] [1] 979.91/240.11 orientation: 979.91/240.11 [1 1 0] [0] [1 0 0] [0] 979.91/240.11 5(2(4(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] [1] 979.91/240.11 979.91/240.11 [1 1 0] [1 0 0] 979.91/240.11 4(5(2(4(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.11 [0 0 0] [0 0 0] 979.91/240.11 979.91/240.11 [1 0 0] [1] [1 0 0] 979.91/240.11 5(5(2(4(5(0(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] 979.91/240.11 979.91/240.11 [1 2 2] [0] [1 1 0] 979.91/240.11 5(5(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] 979.91/240.11 979.91/240.11 [1 2 2] [2] [1 0 0] [1] 979.91/240.11 5(5(5(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] [1] 979.91/240.11 979.91/240.11 [1 1 0] [1 1 0] 979.91/240.11 2(5(5(3(4(x1))))) = [0 0 0]x1 >= [0 0 0]x1 = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.11 [0 0 0] [0 0 0] 979.91/240.11 979.91/240.11 [1 1 0] [2] [1 0 0] 979.91/240.11 5(5(5(1(4(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] 979.91/240.11 979.91/240.11 [1 2 2] [3] [1 0 0] [0] 979.91/240.11 0(4(4(5(5(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] [1] 979.91/240.11 979.91/240.11 [1 1 0] [1 0 0] 979.91/240.11 1(2(4(5(2(4(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.11 [0 0 0] [0 0 0] 979.91/240.11 979.91/240.11 [1 0 0] [1 0 0] 979.91/240.11 4(4(5(2(4(2(2(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.11 [0 0 0] [0 0 0] 979.91/240.11 979.91/240.11 [1 1 0] [0] [1 1 0] 979.91/240.11 0(2(5(3(4(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.11 [0 0 0] [1] [0 0 0] 979.91/240.11 979.91/240.11 [1 2 2] [0] [1 0 0] [0] 979.91/240.12 5(5(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.12 [0 0 0] [1] [0 0 0] [1] 979.91/240.12 979.91/240.12 [1 2 2] [1 0 0] 979.91/240.12 2(5(5(x1))) = [0 0 0]x1 >= [0 0 0]x1 = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.91/240.12 [0 0 0] [0 0 0] 979.91/240.12 979.91/240.12 [1 0 0] [0] [1 0 0] [0] 979.91/240.12 5(5(2(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.91/240.12 [0 0 0] [1] [0 0 0] [1] 979.91/240.12 979.91/240.12 [1 0 0] [0] [1 0 0] [0] 979.91/240.12 5(5(3(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.12 [0 0 0] [1] [0 0 0] [1] 979.91/240.12 979.91/240.12 [1 1 0] [1 0 0] 979.91/240.12 2(5(0(4(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.91/240.12 [0 0 0] [0 0 0] 979.91/240.12 979.91/240.12 [1 2 2] [3] [1 2 0] 979.91/240.12 4(5(5(5(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.91/240.12 [0 0 0] [0] [0 0 0] 979.91/240.12 979.91/240.12 [1 1 0] [2] [1 1 0] 979.91/240.12 4(1(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.91/240.12 [0 0 0] [0] [0 0 0] 979.91/240.12 979.91/240.12 [1 2 0] [1 2 0] 979.91/240.12 4(2(5(5(1(5(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.91/240.12 [0 0 0] [0 0 0] 979.91/240.12 979.91/240.12 [1 1 0] [2] [1 1 0] [0] 979.91/240.12 5(2(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.91/240.12 [0 0 0] [1] [0 0 0] [1] 979.91/240.12 979.91/240.12 [1 2 0] [2] [1 2 0] [0] 979.91/240.12 0(1(5(5(5(3(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.91/240.12 [0 0 0] [1] [0 0 0] [1] 979.91/240.12 problem: 979.91/240.12 strict: 979.91/240.12 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.12 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.12 weak: 979.91/240.12 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.12 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.12 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.12 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.12 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.12 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.12 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.12 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.12 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.12 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.12 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.91/240.12 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.91/240.12 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.12 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.91/240.12 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.91/240.12 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.91/240.12 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.91/240.12 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.91/240.12 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.91/240.13 Matrix Interpretation Processor: dim=3 979.91/240.13 979.91/240.13 max_matrix: 979.91/240.13 [1 1 0] 979.91/240.13 [0 0 1] 979.91/240.13 [0 0 0] 979.91/240.13 interpretation: 979.91/240.13 [1 0 0] 979.91/240.13 [3](x0) = [0 0 0]x0 979.91/240.13 [0 0 0] , 979.91/240.13 979.91/240.13 [1 0 0] [0] 979.91/240.13 [0](x0) = [0 0 0]x0 + [0] 979.91/240.13 [0 0 0] [1], 979.91/240.13 979.91/240.13 [1 0 0] [0] 979.91/240.13 [4](x0) = [0 0 0]x0 + [0] 979.91/240.13 [0 0 0] [1], 979.91/240.13 979.91/240.13 [1 0 0] [0] 979.91/240.13 [2](x0) = [0 0 1]x0 + [0] 979.91/240.13 [0 0 0] [1], 979.91/240.13 979.91/240.13 [1 0 0] 979.91/240.13 [1](x0) = [0 0 0]x0 979.91/240.13 [0 0 0] , 979.91/240.13 979.91/240.13 [1 1 0] [0] 979.91/240.13 [5](x0) = [0 0 0]x0 + [0] 979.91/240.13 [0 0 0] [1] 979.91/240.13 orientation: 979.91/240.13 [1 0 0] [1] [1 0 0] [0] 979.91/240.13 5(2(4(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 0 0] [1] [1 0 0] [1] 979.91/240.13 4(5(2(4(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 0 0] [1] [1 0 0] [0] 979.91/240.13 5(5(2(4(5(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 1 0] [0] [1 0 0] 979.91/240.13 5(5(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] 979.91/240.13 979.91/240.13 [1 1 0] [0] [1 0 0] [0] 979.91/240.13 5(5(5(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 0 0] [0] [1 0 0] [0] 979.91/240.13 2(5(5(3(4(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 0 0] [0] [1 0 0] 979.91/240.13 5(5(5(1(4(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] 979.91/240.13 979.91/240.13 [1 1 0] [0] [1 0 0] [0] 979.91/240.13 0(4(4(5(5(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 0 0] [1] [1 0 0] 979.91/240.13 1(2(4(5(2(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.13 [0 0 0] [0] [0 0 0] 979.91/240.13 979.91/240.13 [1 0 0] [1] [1 0 0] [0] 979.91/240.13 4(4(5(2(4(2(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] [1] 979.91/240.13 979.91/240.13 [1 0 0] [0] [1 0 0] 979.91/240.13 0(2(5(3(4(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.13 [0 0 0] [1] [0 0 0] 979.91/240.14 979.91/240.14 [1 1 0] [0] [1 0 0] [0] 979.91/240.14 5(5(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 1 0] [0] [1 0 0] [0] 979.91/240.14 2(5(5(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 0 1] [0] [1 0 0] [0] 979.91/240.14 5(5(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 0 0] [0] [1 0 0] [0] 979.91/240.14 5(5(3(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 0 0] [0] [1 0 0] [0] 979.91/240.14 2(5(0(4(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 1 0] [0] [1 1 0] 979.91/240.14 4(5(5(5(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] 979.91/240.14 979.91/240.14 [1 0 0] [0] [1 0 0] 979.91/240.14 4(1(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] 979.91/240.14 979.91/240.14 [1 1 0] [0] [1 1 0] [0] 979.91/240.14 4(2(5(5(1(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 0 0] [1] [1 0 0] [0] 979.91/240.14 5(2(5(5(0(4(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 979.91/240.14 [1 1 0] [0] [1 1 0] [0] 979.91/240.14 0(1(5(5(5(3(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.91/240.14 [0 0 0] [1] [0 0 0] [1] 979.91/240.14 problem: 979.91/240.14 strict: 979.91/240.14 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.14 weak: 979.91/240.14 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.14 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.14 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.14 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.14 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.14 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.14 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.14 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.14 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.14 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.14 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.14 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 979.91/240.14 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 979.91/240.14 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 979.91/240.14 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 979.91/240.14 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 979.91/240.15 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 979.91/240.15 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 979.91/240.15 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 979.91/240.15 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 979.91/240.15 Matrix Interpretation Processor: dim=5 979.91/240.15 979.91/240.15 max_matrix: 979.91/240.15 [1 0 1 0 0] 979.91/240.15 [0 0 0 1 1] 979.91/240.15 [0 0 0 1 0] 979.91/240.15 [0 0 0 0 1] 979.91/240.15 [0 0 0 0 0] 979.91/240.15 interpretation: 979.91/240.15 [1 0 0 0 0] 979.91/240.15 [0 0 0 0 0] 979.91/240.15 [3](x0) = [0 0 0 0 0]x0 979.91/240.15 [0 0 0 0 1] 979.91/240.15 [0 0 0 0 0] , 979.91/240.15 979.91/240.15 [1 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [0] 979.91/240.15 [0](x0) = [0 0 0 0 0]x0 + [0] 979.91/240.15 [0 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [1], 979.91/240.15 979.91/240.15 [1 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [1] 979.91/240.15 [4](x0) = [0 0 0 0 0]x0 + [0] 979.91/240.15 [0 0 0 0 0] [1] 979.91/240.15 [0 0 0 0 0] [0], 979.91/240.15 979.91/240.15 [1 0 0 0 0] 979.91/240.15 [0 0 0 0 1] 979.91/240.15 [2](x0) = [0 0 0 1 0]x0 979.91/240.15 [0 0 0 0 1] 979.91/240.15 [0 0 0 0 0] , 979.91/240.15 979.91/240.15 [1 0 0 0 0] 979.91/240.15 [0 0 0 0 0] 979.91/240.15 [1](x0) = [0 0 0 0 0]x0 979.91/240.15 [0 0 0 0 0] 979.91/240.15 [0 0 0 0 0] , 979.91/240.15 979.91/240.15 [1 0 1 0 0] [0] 979.91/240.15 [0 0 0 1 0] [0] 979.91/240.15 [5](x0) = [0 0 0 0 0]x0 + [0] 979.91/240.15 [0 0 0 0 1] [0] 979.91/240.15 [0 0 0 0 0] [1] 979.91/240.15 orientation: 979.91/240.15 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.15 4(5(2(4(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.15 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.15 979.91/240.15 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.15 5(2(4(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 979.91/240.15 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.15 979.91/240.15 [1 0 0 0 0] [1] [1 0 0 0 0] 979.91/240.15 [0 0 0 0 0] [0] [0 0 0 0 0] 979.91/240.15 5(5(2(4(5(0(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.15 979.91/240.15 [1 0 1 0 0] [0] [1 0 0 0 0] 979.91/240.15 [0 0 0 0 1] [0] [0 0 0 0 0] 979.91/240.15 5(5(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.15 979.91/240.15 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.91/240.15 5(5(5(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 979.91/240.15 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 979.91/240.18 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 2(5(5(3(4(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.18 979.91/240.18 [1 0 0 0 0] [0] [1 0 0 0 0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.18 5(5(5(1(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.18 979.91/240.18 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.18 0(4(4(5(5(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 979.91/240.18 [1 0 0 0 0] [1] [1 0 0 0 0] 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] 979.91/240.18 1(2(4(5(2(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] 979.91/240.18 979.91/240.18 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 4(4(5(2(4(2(2(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 979.91/240.18 979.91/240.18 [1 0 0 0 0] [0] [1 0 0 0 0] 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] 979.91/240.18 0(2(5(3(4(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [0] [0 0 0 0 0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] 979.91/240.18 979.91/240.18 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 1] [0] [0 0 0 0 0] [0] 979.91/240.18 5(5(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 979.91/240.18 979.91/240.18 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 979.91/240.18 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 2(5(5(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 980.01/240.20 [1 0 0 1 0] [0] [1 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 5(5(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 980.01/240.20 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 5(5(3(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 980.01/240.20 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 2(5(0(4(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 980.01/240.20 [1 0 1 0 0] [0] [1 0 1 0 0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] 980.01/240.20 4(5(5(5(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] 980.01/240.20 980.01/240.20 [1 0 0 0 0] [0] [1 0 0 0 0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] 980.01/240.20 4(1(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] 980.01/240.20 980.01/240.20 [1 0 1 0 0] [0] [1 0 1 0 0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] 980.01/240.20 4(2(5(5(1(5(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] 980.01/240.20 980.01/240.20 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 980.01/240.20 5(2(5(5(0(4(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 980.01/240.20 [1 0 1 0 0] [0] [1 0 1 0 0] [0] 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 0(1(5(5(5(3(5(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 980.01/240.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 980.01/240.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 980.01/240.20 problem: 980.01/240.20 strict: 980.01/240.20 980.01/240.20 weak: 980.01/240.20 4(5(2(4(x1)))) -> 4(1(5(5(2(0(3(1(3(3(x1)))))))))) 980.01/240.20 5(2(4(x1))) -> 0(5(0(2(3(3(4(2(4(2(x1)))))))))) 980.01/240.20 5(5(2(4(5(0(x1)))))) -> 2(1(1(4(2(4(0(4(2(0(x1)))))))))) 980.01/240.20 5(5(x1)) -> 3(4(1(1(1(1(4(4(0(4(x1)))))))))) 980.01/240.20 5(5(5(x1))) -> 5(3(4(1(0(1(4(5(0(0(x1)))))))))) 980.01/240.20 2(5(5(3(4(x1))))) -> 4(5(4(3(1(4(0(2(4(4(x1)))))))))) 980.01/240.20 5(5(5(1(4(x1))))) -> 3(3(0(5(0(4(3(4(4(0(x1)))))))))) 980.01/240.20 0(4(4(5(5(5(x1)))))) -> 0(4(4(4(3(3(4(1(3(1(x1)))))))))) 980.01/240.20 1(2(4(5(2(4(x1)))))) -> 3(3(5(3(0(4(0(3(1(3(x1)))))))))) 980.01/240.20 4(4(5(2(4(2(2(x1))))))) -> 4(0(5(5(4(5(1(2(2(1(x1)))))))))) 980.01/240.20 0(2(5(3(4(x1))))) -> 3(2(4(3(1(5(1(1(3(4(x1)))))))))) 980.01/240.20 5(5(x1)) -> 0(5(4(0(2(5(4(5(2(1(x1)))))))))) 980.01/240.20 2(5(5(x1))) -> 4(2(5(4(4(0(0(1(1(2(x1)))))))))) 980.01/240.20 5(5(2(x1))) -> 0(1(3(2(3(0(3(2(5(3(x1)))))))))) 980.01/240.20 5(5(3(x1))) -> 0(3(5(4(4(1(0(1(5(0(x1)))))))))) 980.01/240.20 2(5(0(4(x1)))) -> 4(4(3(2(4(4(5(1(0(0(x1)))))))))) 980.01/240.20 4(5(5(5(x1)))) -> 1(5(1(2(0(3(2(1(0(5(x1)))))))))) 980.01/240.20 4(1(5(5(0(4(x1)))))) -> 1(0(3(0(4(2(4(4(3(4(x1)))))))))) 980.01/240.20 4(2(5(5(1(5(x1)))))) -> 2(3(4(2(1(1(3(4(2(5(x1)))))))))) 980.01/240.20 5(2(5(5(0(4(x1)))))) -> 0(4(2(3(3(5(2(1(4(4(x1)))))))))) 980.01/240.20 0(1(5(5(5(3(5(x1))))))) -> 5(3(2(5(1(0(1(2(0(5(x1)))))))))) 980.01/240.20 Qed 980.01/240.21 EOF