YES(?,O(n^3)) 1173.78/296.43 YES(?,O(n^3)) 1173.78/296.44 1173.78/296.44 Problem: 1173.78/296.44 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.44 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.44 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.44 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.44 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.44 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.44 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.44 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.44 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.44 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.44 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.44 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.44 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.44 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.44 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.44 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.44 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.44 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.44 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.44 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.44 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.44 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.44 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.44 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.44 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.44 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.44 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.44 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.44 1173.78/296.44 Proof: 1173.78/296.44 Complexity Transformation Processor: 1173.78/296.44 strict: 1173.78/296.44 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.44 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.44 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.44 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.44 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.44 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.44 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.44 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.44 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.44 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.44 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.44 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.44 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.44 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.44 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.44 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.44 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.44 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.44 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.44 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.44 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.44 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.44 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.44 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.44 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.44 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.44 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.44 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.44 weak: 1173.78/296.44 1173.78/296.44 Matrix Interpretation Processor: dim=1 1173.78/296.44 1173.78/296.44 max_matrix: 1173.78/296.44 1 1173.78/296.44 interpretation: 1173.78/296.44 [5](x0) = x0, 1173.78/296.44 1173.78/296.44 [4](x0) = x0, 1173.78/296.44 1173.78/296.44 [3](x0) = x0 + 1, 1173.78/296.44 1173.78/296.44 [1](x0) = x0 + 3, 1173.78/296.44 1173.78/296.44 [2](x0) = x0 + 2, 1173.78/296.44 1173.78/296.44 [0](x0) = x0 + 4 1173.78/296.44 orientation: 1173.78/296.44 1(2(0(x1))) = x1 + 9 >= x1 + 10 = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.44 1173.78/296.44 1(0(0(4(5(x1))))) = x1 + 11 >= x1 + 14 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.44 1173.78/296.44 2(0(3(0(2(x1))))) = x1 + 13 >= x1 + 14 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.44 1173.78/296.44 2(1(0(1(0(x1))))) = x1 + 16 >= x1 + 11 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.44 1173.78/296.44 3(4(2(0(2(x1))))) = x1 + 9 >= x1 + 13 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.44 1173.78/296.44 0(3(5(2(4(0(x1)))))) = x1 + 11 >= x1 + 14 = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.46 1173.78/296.46 1(1(2(0(4(5(x1)))))) = x1 + 12 >= x1 + 18 = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.46 1173.78/296.46 2(1(1(0(1(2(x1)))))) = x1 + 17 >= x1 + 11 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.46 1173.78/296.46 2(2(0(1(1(1(x1)))))) = x1 + 17 >= x1 + 12 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.46 1173.78/296.46 2(4(1(0(4(2(x1)))))) = x1 + 11 >= x1 + 14 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.46 1173.78/296.46 2(4(2(1(1(1(x1)))))) = x1 + 13 >= x1 + 9 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.46 1173.78/296.46 3(0(1(0(0(2(x1)))))) = x1 + 18 >= x1 + 13 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.46 1173.78/296.46 3(0(1(1(1(1(x1)))))) = x1 + 17 >= x1 + 10 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.46 1173.78/296.46 4(1(1(2(0(2(x1)))))) = x1 + 14 >= x1 + 11 = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.46 1173.78/296.46 0(2(1(1(1(1(0(x1))))))) = x1 + 22 >= x1 + 10 = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.46 1173.78/296.46 0(2(4(1(1(1(5(x1))))))) = x1 + 15 >= x1 + 13 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.46 1173.78/296.46 0(4(2(0(0(4(1(x1))))))) = x1 + 17 >= x1 + 14 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.46 1173.78/296.46 0(4(3(0(5(4(1(x1))))))) = x1 + 12 >= x1 + 17 = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.46 1173.78/296.46 1(0(5(2(2(0(0(x1))))))) = x1 + 19 >= x1 + 6 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.46 1173.78/296.46 1(1(3(4(5(0(0(x1))))))) = x1 + 15 >= x1 + 12 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.46 1173.78/296.46 1(4(3(1(5(0(5(x1))))))) = x1 + 11 >= x1 + 15 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.46 1173.78/296.46 1(5(0(2(0(5(5(x1))))))) = x1 + 13 >= x1 + 14 = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.46 1173.78/296.46 2(0(1(5(2(0(5(x1))))))) = x1 + 15 >= x1 + 7 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.46 1173.78/296.46 2(4(0(5(4(1(4(x1))))))) = x1 + 9 >= x1 + 8 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.46 1173.78/296.46 3(4(1(4(0(4(5(x1))))))) = x1 + 8 >= x1 + 16 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.46 1173.78/296.46 4(1(0(4(2(0(0(x1))))))) = x1 + 17 >= x1 + 21 = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.46 1173.78/296.46 4(1(0(4(2(0(3(x1))))))) = x1 + 14 >= x1 + 19 = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.46 1173.78/296.46 4(1(1(1(0(1(2(x1))))))) = x1 + 18 >= x1 + 15 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.46 problem: 1173.78/296.46 strict: 1173.78/296.46 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.46 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.46 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.46 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.46 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.46 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.46 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.46 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.46 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.46 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.46 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.46 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.46 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.46 weak: 1173.78/296.46 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.46 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.46 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.46 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.46 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.46 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.46 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.46 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.46 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.46 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.46 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.46 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.46 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.46 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.46 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.46 Matrix Interpretation Processor: dim=1 1173.78/296.46 1173.78/296.46 max_matrix: 1173.78/296.46 1 1173.78/296.46 interpretation: 1173.78/296.46 [5](x0) = x0 + 1, 1173.78/296.46 1173.78/296.46 [4](x0) = x0, 1173.78/296.46 1173.78/296.46 [3](x0) = x0, 1173.78/296.46 1173.78/296.46 [1](x0) = x0 + 4, 1173.78/296.46 1173.78/296.46 [2](x0) = x0, 1173.78/296.46 1173.78/296.46 [0](x0) = x0 + 8 1173.78/296.46 orientation: 1173.78/296.46 1(2(0(x1))) = x1 + 12 >= x1 + 14 = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 1(0(0(4(5(x1))))) = x1 + 21 >= x1 + 13 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(0(3(0(2(x1))))) = x1 + 16 >= x1 + 13 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 3(4(2(0(2(x1))))) = x1 + 8 >= x1 + 10 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 0(3(5(2(4(0(x1)))))) = x1 + 17 >= x1 + 9 = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 1(1(2(0(4(5(x1)))))) = x1 + 17 >= x1 + 21 = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(4(1(0(4(2(x1)))))) = x1 + 12 >= x1 + 17 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.47 1173.78/296.47 0(4(3(0(5(4(1(x1))))))) = x1 + 21 >= x1 + 22 = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.47 1173.78/296.47 1(4(3(1(5(0(5(x1))))))) = x1 + 18 >= x1 + 13 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 1(5(0(2(0(5(5(x1))))))) = x1 + 23 >= x1 + 20 = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.47 1173.78/296.47 3(4(1(4(0(4(5(x1))))))) = x1 + 13 >= x1 + 12 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 4(1(0(4(2(0(0(x1))))))) = x1 + 28 >= x1 + 28 = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.47 1173.78/296.47 4(1(0(4(2(0(3(x1))))))) = x1 + 20 >= x1 + 29 = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(1(0(1(0(x1))))) = x1 + 24 >= x1 + 10 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(1(1(0(1(2(x1)))))) = x1 + 20 >= x1 + 6 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(2(0(1(1(1(x1)))))) = x1 + 20 >= x1 + 6 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(4(2(1(1(1(x1)))))) = x1 + 12 >= x1 + 9 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.47 1173.78/296.47 3(0(1(0(0(2(x1)))))) = x1 + 28 >= x1 + 10 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 3(0(1(1(1(1(x1)))))) = x1 + 24 >= x1 + 6 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.47 1173.78/296.47 4(1(1(2(0(2(x1)))))) = x1 + 16 >= x1 + 8 = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 0(2(1(1(1(1(0(x1))))))) = x1 + 32 >= x1 + 18 = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.47 1173.78/296.47 0(2(4(1(1(1(5(x1))))))) = x1 + 21 >= x1 + 8 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 0(4(2(0(0(4(1(x1))))))) = x1 + 28 >= x1 + 17 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.47 1173.78/296.47 1(0(5(2(2(0(0(x1))))))) = x1 + 29 >= x1 + 7 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.47 1173.78/296.47 1(1(3(4(5(0(0(x1))))))) = x1 + 25 >= x1 + 14 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(0(1(5(2(0(5(x1))))))) = x1 + 22 >= x1 + 8 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.47 1173.78/296.47 2(4(0(5(4(1(4(x1))))))) = x1 + 13 >= x1 + 12 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.47 1173.78/296.47 4(1(1(1(0(1(2(x1))))))) = x1 + 24 >= x1 + 14 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.47 problem: 1173.78/296.47 strict: 1173.78/296.47 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.47 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.47 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.47 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.47 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.47 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.47 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.47 weak: 1173.78/296.47 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.47 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.47 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.47 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.47 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.47 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.47 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.47 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.47 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.47 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.47 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.47 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.47 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.47 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.47 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.47 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.47 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.47 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.47 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.48 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.48 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.48 Matrix Interpretation Processor: dim=2 1173.78/296.48 1173.78/296.48 max_matrix: 1173.78/296.48 [1 1] 1173.78/296.48 [0 1] 1173.78/296.48 interpretation: 1173.78/296.48 [1 0] 1173.78/296.48 [5](x0) = [0 0]x0, 1173.78/296.48 1173.78/296.48 1173.78/296.48 [4](x0) = x0, 1173.78/296.48 1173.78/296.48 [1 0] 1173.78/296.48 [3](x0) = [0 0]x0, 1173.78/296.48 1173.78/296.48 [1 1] [0] 1173.78/296.48 [1](x0) = [0 0]x0 + [1], 1173.78/296.48 1173.78/296.48 1173.78/296.48 [2](x0) = x0, 1173.78/296.48 1173.78/296.48 1173.78/296.48 [0](x0) = x0 1173.78/296.48 orientation: 1173.78/296.48 [1 1] [0] [1 0] 1173.78/296.48 1(2(0(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [1 0] 1173.78/296.48 3(4(2(0(2(x1))))) = [0 0]x1 >= [0 0]x1 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [1] [1 0] 1173.78/296.48 1(1(2(0(4(5(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [0] [1 0] [0] 1173.78/296.48 2(4(1(0(4(2(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [1 1] 1173.78/296.48 0(4(3(0(5(4(1(x1))))))) = [0 0]x1 >= [0 0]x1 = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [0] [1 0] 1173.78/296.48 4(1(0(4(2(0(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [0] [1 0] 1173.78/296.48 4(1(0(4(2(0(3(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [0] [1 0] [0] 1173.78/296.48 1(0(0(4(5(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [1 0] 1173.78/296.48 2(0(3(0(2(x1))))) = [0 0]x1 >= [0 0]x1 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [1 0] 1173.78/296.48 0(3(5(2(4(0(x1)))))) = [0 0]x1 >= [0 0]x1 = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [0] [1 0] 1173.78/296.48 1(4(3(1(5(0(5(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [0] [1 0] 1173.78/296.48 1(5(0(2(0(5(5(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 0] [1 0] 1173.78/296.48 3(4(1(4(0(4(5(x1))))))) = [0 0]x1 >= [0 0]x1 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [1] [1 1] [1] 1173.78/296.48 2(1(0(1(0(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [2] [1 0] 1173.78/296.48 2(1(1(0(1(2(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [2] [1 0] 1173.78/296.48 2(2(0(1(1(1(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [2] [1 1] [0] 1173.78/296.48 2(4(2(1(1(1(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [1 0] 1173.78/296.48 3(0(1(0(0(2(x1)))))) = [0 0]x1 >= [0 0]x1 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [3] [1 1] 1173.78/296.48 3(0(1(1(1(1(x1)))))) = [0 0]x1 + [0] >= [0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.48 1173.78/296.48 [1 1] [1] [1 0] 1173.78/296.49 4(1(1(2(0(2(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 1] [3] [1 0] [0] 1173.78/296.49 0(2(1(1(1(1(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 0] [2] [1 0] 1173.78/296.49 0(2(4(1(1(1(5(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 1] [0] [1 1] 1173.78/296.49 0(4(2(0(0(4(1(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 0] [0] [1 0] [0] 1173.78/296.49 1(0(5(2(2(0(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 0] [1] [1 0] [0] 1173.78/296.49 1(1(3(4(5(0(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 0] [0] [1 0] 1173.78/296.49 2(0(1(5(2(0(5(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 1] [1 1] 1173.78/296.49 2(4(0(5(4(1(4(x1))))))) = [0 0]x1 >= [0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.49 1173.78/296.49 [1 1] [3] [1 0] 1173.78/296.49 4(1(1(1(0(1(2(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.49 problem: 1173.78/296.49 strict: 1173.78/296.49 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.78/296.49 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.78/296.49 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.78/296.49 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.78/296.49 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.78/296.49 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.78/296.49 weak: 1173.78/296.49 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.78/296.49 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.78/296.49 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.78/296.49 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.78/296.49 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.78/296.49 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.78/296.49 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.78/296.49 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.78/296.49 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.78/296.49 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.78/296.49 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.78/296.49 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.78/296.49 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.78/296.49 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.78/296.49 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.78/296.49 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.78/296.49 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.78/296.49 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.78/296.49 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.78/296.49 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.78/296.49 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.78/296.49 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.78/296.49 Matrix Interpretation Processor: dim=3 1173.78/296.49 1173.78/296.49 max_matrix: 1173.78/296.49 [1 1 0] 1173.78/296.49 [0 0 1] 1173.78/296.49 [0 0 1] 1173.78/296.49 interpretation: 1173.78/296.49 [1 0 0] 1173.78/296.49 [5](x0) = [0 0 0]x0 1173.78/296.49 [0 0 0] , 1173.78/296.49 1173.78/296.49 [1 0 0] 1173.78/296.49 [4](x0) = [0 0 0]x0 1173.78/296.49 [0 0 1] , 1173.78/296.49 1173.78/296.49 [1 0 0] 1173.78/296.49 [3](x0) = [0 0 0]x0 1173.78/296.49 [0 0 0] , 1173.78/296.49 1173.78/296.49 [1 1 0] 1173.78/296.49 [1](x0) = [0 0 0]x0 1173.78/296.49 [0 0 1] , 1173.78/296.49 1173.78/296.49 [1 0 0] 1173.78/296.49 [2](x0) = [0 0 0]x0 1173.88/296.50 [0 0 1] , 1173.88/296.50 1173.88/296.50 [1 0 0] [0] 1173.88/296.50 [0](x0) = [0 0 1]x0 + [0] 1173.88/296.50 [0 0 0] [2] 1173.88/296.50 orientation: 1173.88/296.50 [1 0 0] [0] [1 0 0] [0] 1173.88/296.50 1(2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] [2] 1173.88/296.50 1173.88/296.50 [1 0 0] [1 0 0] 1173.88/296.50 3(4(2(0(2(x1))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.50 [0 0 0] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 1] [0] [1 0 0] 1173.88/296.50 2(4(1(0(4(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 1 0] [0] [1 1 0] [0] 1173.88/296.50 0(4(3(0(5(4(1(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] [2] 1173.88/296.50 1173.88/296.50 [1 0 0] [2] [1 0 0] [2] 1173.88/296.50 4(1(0(4(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] [0] 1173.88/296.50 1173.88/296.50 [1 0 0] [2] [1 0 0] [0] 1173.88/296.50 4(1(0(4(2(0(3(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] [2] 1173.88/296.50 1173.88/296.50 [1 0 0] [0] [1 0 0] 1173.88/296.50 1(1(2(0(4(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 0] [2] [1 0 0] 1173.88/296.50 1(0(0(4(5(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 0] [0] [1 0 0] 1173.88/296.50 2(0(3(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 0] [0] [1 0 0] [0] 1173.88/296.50 0(3(5(2(4(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.50 [0 0 0] [2] [0 0 0] [2] 1173.88/296.50 1173.88/296.50 [1 0 0] [1 0 0] 1173.88/296.50 1(4(3(1(5(0(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.50 [0 0 0] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 0] [1 0 0] 1173.88/296.50 1(5(0(2(0(5(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.50 [0 0 0] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 0] [1 0 0] 1173.88/296.50 3(4(1(4(0(4(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.50 [0 0 0] [0 0 0] 1173.88/296.50 1173.88/296.50 [1 0 1] [2] [1 0 0] 1173.88/296.50 2(1(0(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 1] [0] [1 0 0] 1173.88/296.51 2(1(1(0(1(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 1 0] [0] [1 0 0] 1173.88/296.51 2(2(0(1(1(1(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 1 0] [1 0 0] 1173.88/296.51 2(4(2(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.51 [0 0 1] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 0] [2] [1 0 0] 1173.88/296.51 3(0(1(0(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.51 [0 0 0] [0] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 1 0] [1 1 0] 1173.88/296.51 3(0(1(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.51 [0 0 0] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 0] [0] [1 0 0] [0] 1173.88/296.51 4(1(1(2(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] [2] 1173.88/296.51 1173.88/296.51 [1 0 1] [0] [1 0 0] [0] 1173.88/296.51 0(2(1(1(1(1(0(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] [2] 1173.88/296.51 1173.88/296.51 [1 0 0] [0] [1 0 0] 1173.88/296.51 0(2(4(1(1(1(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 1 0] [0] [1 1 0] 1173.88/296.51 0(4(2(0(0(4(1(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 0] [0] [1 0 0] 1173.88/296.51 1(0(5(2(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 0] [1 0 0] 1173.88/296.51 1(1(3(4(5(0(0(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.51 [0 0 0] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 0] [0] [1 0 0] 1173.88/296.51 2(0(1(5(2(0(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 0] [0] [1 0 0] 1173.88/296.51 2(4(0(5(4(1(4(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.51 [0 0 0] [2] [0 0 0] 1173.88/296.51 1173.88/296.51 [1 0 1] [0] [1 0 0] 1173.88/296.51 4(1(1(1(0(1(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.52 [0 0 0] [2] [0 0 0] 1173.88/296.52 problem: 1173.88/296.52 strict: 1173.88/296.52 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.52 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.52 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.52 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.52 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.52 weak: 1173.88/296.52 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.52 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.52 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.52 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.52 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.52 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.52 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.52 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.52 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.52 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.52 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.52 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.52 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.52 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.52 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.52 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.52 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.52 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.52 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.52 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.52 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.52 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.52 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.52 Splitting Processor: 1173.88/296.52 strict: 1173.88/296.52 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.52 weak: 1173.88/296.52 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.52 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.52 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.52 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.52 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.52 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.52 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.52 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.52 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.52 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.52 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.52 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.52 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.52 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.52 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.52 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.52 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.52 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.52 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.52 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.52 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.52 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.52 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.52 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.52 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.52 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.52 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.52 Matrix Interpretation Processor: dim=3 1173.88/296.52 1173.88/296.52 max_matrix: 1173.88/296.52 [1 1 0] 1173.88/296.52 [0 0 1] 1173.88/296.52 [0 0 1] 1173.88/296.52 interpretation: 1173.88/296.52 [1 0 0] 1173.88/296.54 [5](x0) = [0 0 0]x0 1173.88/296.54 [0 0 0] , 1173.88/296.54 1173.88/296.54 [1 0 0] 1173.88/296.54 [4](x0) = [0 0 0]x0 1173.88/296.54 [0 0 1] , 1173.88/296.54 1173.88/296.54 [1 0 0] 1173.88/296.54 [3](x0) = [0 0 0]x0 1173.88/296.54 [0 0 0] , 1173.88/296.54 1173.88/296.54 [1 1 0] 1173.88/296.54 [1](x0) = [0 0 0]x0 1173.88/296.54 [0 0 1] , 1173.88/296.54 1173.88/296.54 [1 0 0] 1173.88/296.54 [2](x0) = [0 0 0]x0 1173.88/296.54 [0 0 1] , 1173.88/296.54 1173.88/296.54 [1 0 0] [0] 1173.88/296.54 [0](x0) = [0 0 1]x0 + [0] 1173.88/296.54 [0 0 1] [1] 1173.88/296.54 orientation: 1173.88/296.54 [1 0 1] [2] [1 0 0] [1] 1173.88/296.54 4(1(0(4(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.54 [0 0 1] [3] [0 0 0] [0] 1173.88/296.54 1173.88/296.54 [1 0 0] [1] [1 0 0] [0] 1173.88/296.54 4(1(0(4(2(0(3(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.54 [0 0 0] [2] [0 0 0] [1] 1173.88/296.54 1173.88/296.54 [1 0 0] [0] [1 0 0] 1173.88/296.54 1(1(2(0(4(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.54 [0 0 0] [1] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 0] [1] [1 0 0] 1173.88/296.54 1(0(0(4(5(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.54 [0 0 0] [2] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 0] [0] [1 0 0] 1173.88/296.54 2(0(3(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.54 [0 0 0] [1] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 0] [0] [1 0 0] [0] 1173.88/296.54 0(3(5(2(4(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.54 [0 0 0] [1] [0 0 0] [1] 1173.88/296.54 1173.88/296.54 [1 0 0] [1 0 0] 1173.88/296.54 1(4(3(1(5(0(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.54 [0 0 0] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 0] [1 0 0] 1173.88/296.54 1(5(0(2(0(5(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.54 [0 0 0] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 0] [1 0 0] 1173.88/296.54 3(4(1(4(0(4(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.54 [0 0 0] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 2] [1] [1 0 0] 1173.88/296.54 2(1(0(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.54 [0 0 1] [2] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 0 1] [0] [1 0 0] 1173.88/296.54 2(1(1(0(1(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.54 [0 0 1] [1] [0 0 0] 1173.88/296.54 1173.88/296.54 [1 1 0] [0] [1 0 0] 1173.88/296.54 2(2(0(1(1(1(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.54 [0 0 1] [1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 1 0] [1 0 0] 1173.88/296.55 2(4(2(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.55 [0 0 1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 1] [1] [1 0 0] 1173.88/296.55 3(0(1(0(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.55 [0 0 0] [0] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 1 0] [1 1 0] 1173.88/296.55 3(0(1(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.55 [0 0 0] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 0] [0] [1 0 0] [0] 1173.88/296.55 4(1(1(2(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.55 [0 0 1] [1] [0 0 0] [1] 1173.88/296.55 1173.88/296.55 [1 0 1] [0] [1 0 0] [0] 1173.88/296.55 0(2(1(1(1(1(0(x1))))))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.55 [0 0 1] [2] [0 0 0] [1] 1173.88/296.55 1173.88/296.55 [1 0 0] [0] [1 0 0] 1173.88/296.55 0(2(4(1(1(1(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.55 [0 0 0] [1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 1 0] [0] [1 1 0] 1173.88/296.55 0(4(2(0(0(4(1(x1))))))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.55 [0 0 1] [3] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 0] [0] [1 0 0] 1173.88/296.55 1(0(5(2(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.55 [0 0 0] [1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 0] [1 0 0] 1173.88/296.55 1(1(3(4(5(0(0(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.55 [0 0 0] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 0] [0] [1 0 0] 1173.88/296.55 2(0(1(5(2(0(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.55 [0 0 0] [1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 0] [0] [1 0 0] 1173.88/296.55 2(4(0(5(4(1(4(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.55 [0 0 0] [1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 1] [0] [1 0 0] 1173.88/296.55 4(1(1(1(0(1(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.55 [0 0 1] [1] [0 0 0] 1173.88/296.55 1173.88/296.55 [1 0 0] [0] [1 0 0] [0] 1173.88/296.55 1(2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.55 [0 0 1] [1] [0 0 0] [1] 1173.88/296.55 1173.88/296.55 [1 0 0] [1 0 0] 1173.88/296.56 3(4(2(0(2(x1))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.56 [0 0 0] [0 0 0] 1173.88/296.56 1173.88/296.56 [1 0 1] [0] [1 0 0] 1173.88/296.56 2(4(1(0(4(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.56 [0 0 1] [1] [0 0 0] 1173.88/296.56 1173.88/296.56 [1 1 0] [0] [1 1 0] [0] 1173.88/296.56 0(4(3(0(5(4(1(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.56 [0 0 0] [1] [0 0 0] [1] 1173.88/296.56 problem: 1173.88/296.56 strict: 1173.88/296.56 1173.88/296.56 weak: 1173.88/296.56 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.56 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.56 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.56 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.56 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.56 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.56 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.56 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.56 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.56 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.56 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.56 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.56 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.56 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.56 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.56 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.56 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.56 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.56 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.56 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.56 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.56 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.56 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.56 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.56 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.56 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.56 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.56 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.56 Qed 1173.88/296.56 1173.88/296.56 strict: 1173.88/296.56 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.56 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.56 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.56 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.56 weak: 1173.88/296.56 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.56 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.56 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.56 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.56 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.56 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.56 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.56 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.56 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.56 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.56 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.56 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.56 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.56 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.56 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.56 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.57 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.57 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.57 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.57 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.57 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.57 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.57 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.57 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.57 Matrix Interpretation Processor: dim=3 1173.88/296.57 1173.88/296.57 max_matrix: 1173.88/296.57 [1 1 0] 1173.88/296.57 [0 0 1] 1173.88/296.57 [0 0 1] 1173.88/296.57 interpretation: 1173.88/296.57 [1 0 0] 1173.88/296.57 [5](x0) = [0 0 0]x0 1173.88/296.57 [0 0 0] , 1173.88/296.57 1173.88/296.57 [1 0 0] 1173.88/296.57 [4](x0) = [0 0 0]x0 1173.88/296.57 [0 0 1] , 1173.88/296.57 1173.88/296.57 [1 0 0] 1173.88/296.57 [3](x0) = [0 0 0]x0 1173.88/296.57 [0 0 0] , 1173.88/296.57 1173.88/296.57 [1 1 0] 1173.88/296.57 [1](x0) = [0 0 0]x0 1173.88/296.57 [0 0 1] , 1173.88/296.57 1173.88/296.57 [1 0 0] 1173.88/296.57 [2](x0) = [0 0 1]x0 1173.88/296.57 [0 0 1] , 1173.88/296.57 1173.88/296.57 [1 0 0] [0] 1173.88/296.57 [0](x0) = [0 0 1]x0 + [0] 1173.88/296.57 [0 0 0] [2] 1173.88/296.57 orientation: 1173.88/296.57 [1 0 0] [2] [1 0 0] [0] 1173.88/296.57 1(2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] [2] 1173.88/296.57 1173.88/296.57 [1 0 0] [1 0 0] 1173.88/296.57 3(4(2(0(2(x1))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.57 [0 0 0] [0 0 0] 1173.88/296.57 1173.88/296.57 [1 0 1] [0] [1 0 0] 1173.88/296.57 2(4(1(0(4(2(x1)))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] 1173.88/296.57 1173.88/296.57 [1 1 0] [0] [1 1 0] [0] 1173.88/296.57 0(4(3(0(5(4(1(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] [2] 1173.88/296.57 1173.88/296.57 [1 0 0] [2] [1 0 0] [2] 1173.88/296.57 4(1(0(4(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] [0] 1173.88/296.57 1173.88/296.57 [1 0 0] [2] [1 0 0] [0] 1173.88/296.57 4(1(0(4(2(0(3(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] [2] 1173.88/296.57 1173.88/296.57 [1 0 0] [2] [1 0 0] 1173.88/296.57 1(1(2(0(4(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] 1173.88/296.57 1173.88/296.57 [1 0 0] [2] [1 0 0] 1173.88/296.57 1(0(0(4(5(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] 1173.88/296.57 1173.88/296.57 [1 0 0] [0] [1 0 0] 1173.88/296.57 2(0(3(0(2(x1))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.57 [0 0 0] [2] [0 0 0] 1173.88/296.57 1173.88/296.57 [1 0 0] [0] [1 0 0] [0] 1173.88/296.58 0(3(5(2(4(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] [2] 1173.88/296.58 1173.88/296.58 [1 0 0] [1 0 0] 1173.88/296.58 1(4(3(1(5(0(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.58 [0 0 0] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 0 0] [1 0 0] 1173.88/296.58 1(5(0(2(0(5(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.58 [0 0 0] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 0 0] [1 0 0] 1173.88/296.58 3(4(1(4(0(4(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.58 [0 0 0] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 0 1] [2] [1 0 1] 1173.88/296.58 2(1(0(1(0(x1))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 0 2] [0] [1 0 0] 1173.88/296.58 2(1(1(0(1(2(x1)))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 1 0] [0] [1 0 0] 1173.88/296.58 2(2(0(1(1(1(x1)))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 1 0] [1 0 0] 1173.88/296.58 2(4(2(1(1(1(x1)))))) = [0 0 1]x1 >= [0 0 0]x1 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.58 [0 0 1] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 0 0] [2] [1 0 0] 1173.88/296.58 3(0(1(0(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.58 [0 0 0] [0] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 1 0] [1 1 0] 1173.88/296.58 3(0(1(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.58 [0 0 0] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 0 0] [2] [1 0 0] [0] 1173.88/296.58 4(1(1(2(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] [2] 1173.88/296.58 1173.88/296.58 [1 0 1] [0] [1 0 0] [0] 1173.88/296.58 0(2(1(1(1(1(0(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] [2] 1173.88/296.58 1173.88/296.58 [1 0 0] [0] [1 0 0] 1173.88/296.58 0(2(4(1(1(1(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] 1173.88/296.58 1173.88/296.58 [1 1 0] [0] [1 1 0] 1173.88/296.58 0(4(2(0(0(4(1(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.58 [0 0 0] [2] [0 0 0] 1173.88/296.59 1173.88/296.59 [1 0 0] [0] [1 0 0] 1173.88/296.59 1(0(5(2(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.59 [0 0 0] [2] [0 0 0] 1173.88/296.59 1173.88/296.59 [1 0 0] [1 0 0] 1173.88/296.59 1(1(3(4(5(0(0(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.59 [0 0 0] [0 0 0] 1173.88/296.59 1173.88/296.59 [1 0 0] [0] [1 0 0] 1173.88/296.59 2(0(1(5(2(0(5(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.59 [0 0 0] [2] [0 0 0] 1173.88/296.59 1173.88/296.59 [1 0 0] [0] [1 0 0] 1173.88/296.59 2(4(0(5(4(1(4(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.59 [0 0 0] [2] [0 0 0] 1173.88/296.59 1173.88/296.59 [1 0 2] [0] [1 0 0] 1173.88/296.59 4(1(1(1(0(1(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.59 [0 0 0] [2] [0 0 0] 1173.88/296.59 problem: 1173.88/296.59 strict: 1173.88/296.59 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.88/296.59 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.88/296.59 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.88/296.59 weak: 1173.88/296.59 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.88/296.59 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.88/296.59 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.88/296.59 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.88/296.59 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.88/296.59 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.88/296.59 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.88/296.59 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.88/296.59 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.88/296.59 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.88/296.59 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.88/296.59 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.88/296.59 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.88/296.59 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.88/296.59 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.88/296.59 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.88/296.59 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.88/296.59 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.88/296.59 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.88/296.59 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.88/296.59 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.88/296.59 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.88/296.59 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.88/296.59 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.88/296.59 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.88/296.59 Matrix Interpretation Processor: dim=3 1173.88/296.59 1173.88/296.59 max_matrix: 1173.88/296.59 [1 1 0] 1173.88/296.59 [0 1 1] 1173.88/296.59 [0 0 1] 1173.88/296.59 interpretation: 1173.88/296.59 [1 1 0] 1173.88/296.59 [5](x0) = [0 0 0]x0 1173.88/296.59 [0 0 0] , 1173.88/296.59 1173.88/296.59 [1 1 0] 1173.88/296.59 [4](x0) = [0 0 0]x0 1173.88/296.59 [0 0 1] , 1173.88/296.59 1173.88/296.59 [1 0 0] 1173.88/296.59 [3](x0) = [0 0 0]x0 1173.88/296.59 [0 0 0] , 1173.88/296.59 1173.88/296.59 [1 1 0] 1173.88/296.59 [1](x0) = [0 0 0]x0 1173.88/296.59 [0 0 1] , 1173.88/296.59 1173.88/296.59 [1 0 0] 1173.88/296.59 [2](x0) = [0 1 1]x0 1173.88/296.59 [0 0 1] , 1173.98/296.61 1173.98/296.61 [1 0 0] [0] 1173.98/296.61 [0](x0) = [0 1 1]x0 + [0] 1173.98/296.61 [0 0 0] [1] 1173.98/296.61 orientation: 1173.98/296.61 [1 1 2] [1] [1 0 0] 1173.98/296.61 3(4(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.98/296.61 [0 0 0] [0] [0 0 0] 1173.98/296.61 1173.98/296.61 [1 1 2] [0] [1 1 1] 1173.98/296.61 2(4(1(0(4(2(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] 1173.98/296.61 1173.98/296.61 [1 1 0] [0] [1 1 0] [0] 1173.98/296.61 0(4(3(0(5(4(1(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] [1] 1173.98/296.61 1173.98/296.61 [1 1 1] [1] [1 0 0] [0] 1173.98/296.61 1(2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] [1] 1173.98/296.61 1173.98/296.61 [1 1 1] [3] [1 1 1] [1] 1173.98/296.61 4(1(0(4(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] [0] 1173.98/296.61 1173.98/296.61 [1 0 0] [2] [1 0 0] [0] 1173.98/296.61 4(1(0(4(2(0(3(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] [1] 1173.98/296.61 1173.98/296.61 [1 1 0] [1] [1 0 0] [1] 1173.98/296.61 1(1(2(0(4(5(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] [0] 1173.98/296.61 1173.98/296.61 [1 1 0] [1] [1 0 0] 1173.98/296.61 1(0(0(4(5(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] 1173.98/296.61 1173.98/296.61 [1 0 0] [0] [1 0 0] 1173.98/296.61 2(0(3(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] 1173.98/296.61 1173.98/296.61 [1 1 1] [1] [1 0 0] [0] 1173.98/296.61 0(3(5(2(4(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.98/296.61 [0 0 0] [1] [0 0 0] [1] 1173.98/296.61 1173.98/296.61 [1 1 0] [1 0 0] 1173.98/296.61 1(4(3(1(5(0(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.98/296.61 [0 0 0] [0 0 0] 1173.98/296.61 1173.98/296.61 [1 1 0] [2] [1 1 0] [2] 1173.98/296.61 1(5(0(2(0(5(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.98/296.61 [0 0 0] [0] [0 0 0] [0] 1173.98/296.61 1173.98/296.61 [1 1 0] [1 0 0] 1173.98/296.61 3(4(1(4(0(4(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.98/296.61 [0 0 0] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 1] [1] [1 1 1] 1173.98/296.62 2(1(0(1(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 2] [0] [1 1 0] 1173.98/296.62 2(1(1(0(1(2(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 0] [0] [1 1 0] 1173.98/296.62 2(2(0(1(1(1(x1)))))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 1] [1 1 0] 1173.98/296.62 2(4(2(1(1(1(x1)))))) = [0 0 1]x1 >= [0 0 0]x1 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.98/296.62 [0 0 1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 2] [1] [1 0 0] 1173.98/296.62 3(0(1(0(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.98/296.62 [0 0 0] [0] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 0] [1 1 0] 1173.98/296.62 3(0(1(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.98/296.62 [0 0 0] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 2] [1] [1 0 0] [0] 1173.98/296.62 4(1(1(2(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] [1] 1173.98/296.62 1173.98/296.62 [1 1 1] [0] [1 1 0] [0] 1173.98/296.62 0(2(1(1(1(1(0(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] [1] 1173.98/296.62 1173.98/296.62 [1 1 0] [0] [1 0 0] 1173.98/296.62 0(2(4(1(1(1(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 1] [2] [1 1 0] 1173.98/296.62 0(4(2(0(0(4(1(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 1] [3] [1 1 1] 1173.98/296.62 1(0(5(2(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 1] [1] [1 0 0] 1173.98/296.62 1(1(3(4(5(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.98/296.62 [0 0 0] [0] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 0] [1] [1 1 0] 1173.98/296.62 2(0(1(5(2(0(5(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.98/296.62 [0 0 0] [1] [0 0 0] 1173.98/296.62 1173.98/296.62 [1 1 0] [0] [1 1 0] 1173.98/296.63 2(4(0(5(4(1(4(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.98/296.63 [0 0 0] [1] [0 0 0] 1173.98/296.63 1173.98/296.63 [1 1 2] [0] [1 1 1] 1173.98/296.63 4(1(1(1(0(1(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.98/296.63 [0 0 0] [1] [0 0 0] 1173.98/296.63 problem: 1173.98/296.63 strict: 1173.98/296.63 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.98/296.63 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.98/296.63 weak: 1173.98/296.63 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.98/296.63 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.98/296.63 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.98/296.63 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.98/296.63 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.98/296.63 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.98/296.63 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.98/296.63 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.98/296.63 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.98/296.63 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.98/296.63 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.98/296.63 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.98/296.63 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.98/296.63 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.98/296.63 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.98/296.63 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.98/296.63 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.98/296.63 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.98/296.63 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.98/296.63 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.98/296.63 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.98/296.63 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.98/296.63 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.98/296.63 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.98/296.63 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.98/296.63 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.98/296.63 Matrix Interpretation Processor: dim=3 1173.98/296.63 1173.98/296.63 max_matrix: 1173.98/296.63 [1 1 0] 1173.98/296.63 [0 1 1] 1173.98/296.63 [0 0 1] 1173.98/296.63 interpretation: 1173.98/296.63 [1 1 0] 1173.98/296.63 [5](x0) = [0 0 0]x0 1173.98/296.63 [0 0 0] , 1173.98/296.63 1173.98/296.63 [1 1 0] 1173.98/296.63 [4](x0) = [0 0 0]x0 1173.98/296.63 [0 0 1] , 1173.98/296.63 1173.98/296.63 [1 0 0] 1173.98/296.63 [3](x0) = [0 0 0]x0 1173.98/296.63 [0 0 0] , 1173.98/296.63 1173.98/296.63 [1 1 0] 1173.98/296.63 [1](x0) = [0 0 1]x0 1173.98/296.63 [0 0 1] , 1173.98/296.63 1173.98/296.63 1173.98/296.63 [2](x0) = x0 1173.98/296.63 , 1173.98/296.63 1173.98/296.63 [1 0 0] [0] 1173.98/296.63 [0](x0) = [0 1 1]x0 + [0] 1173.98/296.63 [0 0 0] [1] 1173.98/296.63 orientation: 1173.98/296.63 [1 1 1] [1] [1 1 1] 1173.98/296.63 2(4(1(0(4(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.98/296.63 [0 0 0] [1] [0 0 0] 1173.98/296.63 1173.98/296.63 [1 1 1] [0] [1 1 1] [0] 1173.98/296.63 0(4(3(0(5(4(1(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.98/296.63 [0 0 0] [1] [0 0 0] [1] 1173.98/296.63 1173.98/296.63 [1 1 1] [1 0 0] 1173.98/296.63 3(4(2(0(2(x1))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.98/296.64 [0 0 0] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 1 1] [0] [1 0 0] [0] 1173.98/296.64 1(2(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] [1] 1173.98/296.64 1173.98/296.64 [1 1 1] [3] [1 1 1] [1] 1173.98/296.64 4(1(0(4(2(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] [0] 1173.98/296.64 1173.98/296.64 [1 0 0] [2] [1 0 0] [0] 1173.98/296.64 4(1(0(4(2(0(3(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] [1] 1173.98/296.64 1173.98/296.64 [1 1 0] [1] [1 0 0] [1] 1173.98/296.64 1(1(2(0(4(5(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] [0] 1173.98/296.64 1173.98/296.64 [1 1 0] [1] [1 0 0] 1173.98/296.64 1(0(0(4(5(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 0 0] [0] [1 0 0] 1173.98/296.64 2(0(3(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 1 1] [0] [1 0 0] [0] 1173.98/296.64 0(3(5(2(4(0(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] [1] 1173.98/296.64 1173.98/296.64 [1 1 0] [1 0 0] 1173.98/296.64 1(4(3(1(5(0(5(x1))))))) = [0 0 0]x1 >= [0 0 0]x1 = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.98/296.64 [0 0 0] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 1 0] [1] [1 1 0] [1] 1173.98/296.64 1(5(0(2(0(5(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.98/296.64 [0 0 0] [0] [0 0 0] [0] 1173.98/296.64 1173.98/296.64 [1 1 0] [1] [1 0 0] 1173.98/296.64 3(4(1(4(0(4(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.98/296.64 [0 0 0] [0] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 1 1] [2] [1 1 1] 1173.98/296.64 2(1(0(1(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 1 2] [1] [1 1 0] 1173.98/296.64 2(1(1(0(1(2(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.98/296.64 [0 0 0] [1] [0 0 0] 1173.98/296.64 1173.98/296.64 [1 1 2] [0] [1 1 0] 1173.98/296.64 2(2(0(1(1(1(x1)))))) = [0 0 2]x1 + [0] >= [0 0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 3] [1 1 0] 1173.98/296.65 2(4(2(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.98/296.65 [0 0 1] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 1] [1] [1 0 0] 1173.98/296.65 3(0(1(0(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.98/296.65 [0 0 0] [0] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 3] [1 1 1] 1173.98/296.65 3(0(1(1(1(1(x1)))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.98/296.65 [0 0 0] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 1] [2] [1 0 0] [0] 1173.98/296.65 4(1(1(2(0(2(x1)))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] [1] 1173.98/296.65 1173.98/296.65 [1 1 1] [3] [1 1 0] [0] 1173.98/296.65 0(2(1(1(1(1(0(x1))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] [1] 1173.98/296.65 1173.98/296.65 [1 1 0] [0] [1 0 0] 1173.98/296.65 0(2(4(1(1(1(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 2] [1] [1 1 0] [1] 1173.98/296.65 0(4(2(0(0(4(1(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] [0] 1173.98/296.65 1173.98/296.65 [1 1 1] [1] [1 1 0] 1173.98/296.65 1(0(5(2(2(0(0(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 1] [1] [1 0 0] 1173.98/296.65 1(1(3(4(5(0(0(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.98/296.65 [0 0 0] [0] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 0] [0] [1 1 0] 1173.98/296.65 2(0(1(5(2(0(5(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 1] [0] [1 1 1] 1173.98/296.65 2(4(0(5(4(1(4(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] 1173.98/296.65 1173.98/296.65 [1 1 2] [3] [1 1 0] 1173.98/296.65 4(1(1(1(0(1(2(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.98/296.65 [0 0 0] [1] [0 0 0] 1173.98/296.65 problem: 1173.98/296.65 strict: 1173.98/296.65 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.98/296.65 weak: 1173.98/296.65 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.98/296.65 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.98/296.66 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.98/296.66 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.98/296.66 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.98/296.66 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.98/296.66 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.98/296.66 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.98/296.66 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.98/296.66 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.98/296.66 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.98/296.66 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.98/296.66 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.98/296.66 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.98/296.66 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.98/296.66 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.98/296.66 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.98/296.66 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.98/296.66 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.98/296.66 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.98/296.66 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.98/296.66 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.98/296.66 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.98/296.66 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.98/296.66 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.98/296.66 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.98/296.66 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.98/296.66 Matrix Interpretation Processor: dim=2 1173.98/296.66 1173.98/296.66 max_matrix: 1173.98/296.66 [1 1] 1173.98/296.66 [0 1] 1173.98/296.66 interpretation: 1173.98/296.66 [1 0] 1173.98/296.66 [5](x0) = [0 0]x0, 1173.98/296.66 1173.98/296.66 1173.98/296.66 [4](x0) = x0, 1173.98/296.66 1173.98/296.66 [1 0] 1173.98/296.66 [3](x0) = [0 0]x0, 1173.98/296.66 1173.98/296.66 [1 1] [0] 1173.98/296.66 [1](x0) = [0 0]x0 + [1], 1173.98/296.66 1173.98/296.66 1173.98/296.66 [2](x0) = x0, 1173.98/296.66 1173.98/296.66 [1] 1173.98/296.66 [0](x0) = x0 + [1] 1173.98/296.66 orientation: 1173.98/296.66 [1 1] [2] [1 1] [1] 1173.98/296.66 0(4(3(0(5(4(1(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 1] [2] [1 0] [1] 1173.98/296.66 2(4(1(0(4(2(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 0] [1] [1 0] [1] 1173.98/296.66 3(4(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 1] [2] [1 0] [1] 1173.98/296.66 1(2(0(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 1] [6] [1 0] [5] 1173.98/296.66 4(1(0(4(2(0(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 0] [4] [1 0] [3] 1173.98/296.66 4(1(0(4(2(0(3(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 0] [3] [1 0] [3] 1173.98/296.66 1(1(2(0(4(5(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.98/296.66 1173.98/296.66 [1 0] [4] [1 0] [0] 1173.98/296.66 1(0(0(4(5(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [2] [1 0] [1] 1173.98/296.67 2(0(3(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [2] [1 0] [1] 1173.98/296.67 0(3(5(2(4(0(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [1] [1 0] [1] 1173.98/296.67 1(4(3(1(5(0(5(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [2] [1 0] [2] 1173.98/296.67 1(5(0(2(0(5(5(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [2] [1 0] [1] 1173.98/296.67 3(4(1(4(0(4(5(x1))))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [5] [1 1] [1] 1173.98/296.67 2(1(0(1(0(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [4] [1 0] 1173.98/296.67 2(1(1(0(1(2(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 = 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [3] [1 0] 1173.98/296.67 2(2(0(1(1(1(x1)))))) = [0 0]x1 + [2] >= [0 0]x1 = 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [2] [1 1] [0] 1173.98/296.67 2(4(2(1(1(1(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [5] [1 0] [1] 1173.98/296.67 3(0(1(0(0(2(x1)))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [4] [1 1] 1173.98/296.67 3(0(1(1(1(1(x1)))))) = [0 0]x1 + [0] >= [0 0]x1 = 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [3] [1 0] [1] 1173.98/296.67 4(1(1(2(0(2(x1)))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [6] [1 0] [1] 1173.98/296.67 0(2(1(1(1(1(0(x1))))))) = [0 0]x1 + [2] >= [0 0]x1 + [2] = 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [3] [1 0] [1] 1173.98/296.67 0(2(4(1(1(1(5(x1))))))) = [0 0]x1 + [2] >= [0 0]x1 + [0] = 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [3] [1 1] [2] 1173.98/296.67 0(4(2(0(0(4(1(x1))))))) = [0 0]x1 + [4] >= [0 0]x1 + [0] = 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [4] [1 0] [0] 1173.98/296.67 1(0(5(2(2(0(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [3] [1 0] [0] 1173.98/296.67 1(1(3(4(5(0(0(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 0] [2] [1 0] 1173.98/296.67 2(0(1(5(2(0(5(x1))))))) = [0 0]x1 + [2] >= [0 0]x1 = 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [1] [1 1] 1173.98/296.67 2(4(0(5(4(1(4(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 = 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.98/296.67 1173.98/296.67 [1 1] [5] [1 0] [1] 1173.98/296.67 4(1(1(1(0(1(2(x1))))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.98/296.67 problem: 1173.98/296.67 strict: 1173.98/296.67 1173.98/296.67 weak: 1173.98/296.67 0(4(3(0(5(4(1(x1))))))) -> 0(3(1(5(3(1(2(5(4(1(x1)))))))))) 1173.98/296.67 2(4(1(0(4(2(x1)))))) -> 1(5(1(3(2(3(4(4(4(0(x1)))))))))) 1173.98/296.67 3(4(2(0(2(x1))))) -> 3(5(3(0(3(3(2(5(3(2(x1)))))))))) 1173.98/296.67 1(2(0(x1))) -> 4(0(3(3(5(4(5(1(4(3(x1)))))))))) 1173.98/296.67 4(1(0(4(2(0(0(x1))))))) -> 4(2(2(3(1(0(0(3(4(0(x1)))))))))) 1173.98/296.67 4(1(0(4(2(0(3(x1))))))) -> 0(4(3(0(0(1(5(4(3(2(x1)))))))))) 1173.98/296.67 1(1(2(0(4(5(x1)))))) -> 3(0(5(4(2(1(0(2(3(3(x1)))))))))) 1173.98/296.67 1(0(0(4(5(x1))))) -> 1(4(3(1(3(1(4(5(2(3(x1)))))))))) 1173.98/296.67 2(0(3(0(2(x1))))) -> 3(3(1(2(2(4(5(0(4(3(x1)))))))))) 1173.98/296.67 0(3(5(2(4(0(x1)))))) -> 4(4(0(2(3(2(2(5(3(2(x1)))))))))) 1173.98/296.67 1(4(3(1(5(0(5(x1))))))) -> 5(0(3(3(2(4(1(3(3(2(x1)))))))))) 1173.98/296.67 1(5(0(2(0(5(5(x1))))))) -> 2(5(2(5(4(2(0(0(5(5(x1)))))))))) 1173.98/296.67 3(4(1(4(0(4(5(x1))))))) -> 3(2(2(1(3(4(3(3(0(3(x1)))))))))) 1173.98/296.67 2(1(0(1(0(x1))))) -> 3(5(4(5(4(3(3(1(1(2(x1)))))))))) 1173.98/296.67 2(1(1(0(1(2(x1)))))) -> 3(4(4(1(3(2(2(2(5(5(x1)))))))))) 1173.98/296.67 2(2(0(1(1(1(x1)))))) -> 2(3(4(1(5(2(2(2(5(4(x1)))))))))) 1173.98/296.67 2(4(2(1(1(1(x1)))))) -> 1(3(5(4(3(4(3(1(4(4(x1)))))))))) 1173.98/296.67 3(0(1(0(0(2(x1)))))) -> 2(4(2(5(3(5(0(3(3(2(x1)))))))))) 1173.98/296.67 3(0(1(1(1(1(x1)))))) -> 3(2(2(4(4(5(2(4(5(1(x1)))))))))) 1173.98/296.67 4(1(1(2(0(2(x1)))))) -> 4(0(3(4(4(4(2(3(2(3(x1)))))))))) 1173.98/296.67 0(2(1(1(1(1(0(x1))))))) -> 0(1(5(5(3(5(2(5(5(5(x1)))))))))) 1173.98/296.67 0(2(4(1(1(1(5(x1))))))) -> 4(4(3(4(3(2(3(0(2(2(x1)))))))))) 1173.98/296.67 0(4(2(0(0(4(1(x1))))))) -> 4(2(5(4(1(0(4(3(3(1(x1)))))))))) 1173.98/296.67 1(0(5(2(2(0(0(x1))))))) -> 1(5(4(4(3(4(5(4(5(2(x1)))))))))) 1173.98/296.67 1(1(3(4(5(0(0(x1))))))) -> 1(3(1(5(3(4(1(4(5(3(x1)))))))))) 1173.98/296.67 2(0(1(5(2(0(5(x1))))))) -> 4(3(3(5(5(3(1(3(5(5(x1)))))))))) 1173.98/296.67 2(4(0(5(4(1(4(x1))))))) -> 3(4(5(5(1(5(3(5(1(4(x1)))))))))) 1173.98/296.67 4(1(1(1(0(1(2(x1))))))) -> 3(3(2(3(3(0(1(5(5(2(x1)))))))))) 1173.98/296.67 Qed 1173.98/296.68 EOF