YES(?,O(n^1)) 478.29/120.41 YES(?,O(n^1)) 478.29/120.42 478.29/120.42 Problem: 478.29/120.42 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.42 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.42 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.42 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.42 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.42 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.42 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.42 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.42 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.42 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.42 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.42 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.42 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.42 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.42 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.42 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.42 478.29/120.42 Proof: 478.29/120.42 Complexity Transformation Processor: 478.29/120.42 strict: 478.29/120.42 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.42 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.42 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.42 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.42 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.42 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.42 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.42 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.42 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.42 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.42 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.42 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.42 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.42 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.42 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.42 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.42 weak: 478.29/120.42 478.29/120.42 Matrix Interpretation Processor: dim=1 478.29/120.42 478.29/120.42 max_matrix: 478.29/120.42 1 478.29/120.42 interpretation: 478.29/120.42 [0](x0) = x0 + 5, 478.29/120.42 478.29/120.42 [2](x0) = x0, 478.29/120.42 478.29/120.42 [5](x0) = x0, 478.29/120.42 478.29/120.42 [4](x0) = x0, 478.29/120.42 478.29/120.42 [1](x0) = x0 + 2, 478.29/120.42 478.29/120.42 [3](x0) = x0 + 1 478.29/120.42 orientation: 478.29/120.42 1(3(3(x1))) = x1 + 4 >= x1 + 7 = 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.42 478.29/120.42 0(3(3(3(x1)))) = x1 + 8 >= x1 + 12 = 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.42 478.29/120.42 0(3(3(3(1(x1))))) = x1 + 10 >= x1 + 20 = 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.42 478.29/120.42 1(2(3(3(3(x1))))) = x1 + 5 >= x1 + 15 = 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.42 478.29/120.42 1(4(4(2(2(x1))))) = x1 + 2 >= x1 + 20 = 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.42 478.29/120.42 0(3(3(1(4(3(x1)))))) = x1 + 10 >= x1 + 23 = 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.42 478.29/120.42 3(3(3(3(4(0(x1)))))) = x1 + 9 >= x1 + 19 = 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.42 478.29/120.42 4(0(1(3(4(0(x1)))))) = x1 + 13 >= x1 + 31 = 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.42 478.29/120.42 4(1(4(4(4(1(x1)))))) = x1 + 4 >= x1 + 11 = 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.42 478.29/120.42 0(1(3(5(2(2(3(x1))))))) = x1 + 9 >= x1 + 27 = 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.42 478.29/120.42 0(2(3(1(3(2(5(x1))))))) = x1 + 9 >= x1 + 15 = 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.42 478.29/120.42 1(1(3(3(5(3(1(x1))))))) = x1 + 9 >= x1 + 19 = 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.42 478.29/120.42 3(5(2(0(1(3(3(x1))))))) = x1 + 10 >= x1 + 3 = 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.42 478.29/120.42 4(1(4(2(4(0(1(x1))))))) = x1 + 9 >= x1 + 9 = 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.42 478.29/120.42 4(5(1(2(4(4(4(x1))))))) = x1 + 2 >= x1 + 17 = 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.42 478.29/120.42 5(1(4(5(3(3(3(x1))))))) = x1 + 5 >= x1 + 4 = 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.42 problem: 478.29/120.42 strict: 478.29/120.42 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.42 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.42 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.42 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.42 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.42 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.42 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.42 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.42 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.43 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.43 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.43 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.43 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.43 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.43 weak: 478.29/120.43 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.43 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.43 Matrix Interpretation Processor: dim=1 478.29/120.43 478.29/120.43 max_matrix: 478.29/120.43 1 478.29/120.43 interpretation: 478.29/120.43 [0](x0) = x0 + 1, 478.29/120.43 478.29/120.43 [2](x0) = x0 + 1, 478.29/120.43 478.29/120.43 [5](x0) = x0, 478.29/120.43 478.29/120.43 [4](x0) = x0, 478.29/120.43 478.29/120.43 [1](x0) = x0, 478.29/120.43 478.29/120.43 [3](x0) = x0 + 2 478.29/120.43 orientation: 478.29/120.43 1(3(3(x1))) = x1 + 4 >= x1 + 7 = 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.43 478.29/120.43 0(3(3(3(x1)))) = x1 + 7 >= x1 + 6 = 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.43 478.29/120.43 0(3(3(3(1(x1))))) = x1 + 7 >= x1 + 5 = 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.43 478.29/120.43 1(2(3(3(3(x1))))) = x1 + 7 >= x1 + 5 = 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.43 478.29/120.43 1(4(4(2(2(x1))))) = x1 + 2 >= x1 + 5 = 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.43 478.29/120.43 0(3(3(1(4(3(x1)))))) = x1 + 7 >= x1 + 11 = 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.43 478.29/120.43 3(3(3(3(4(0(x1)))))) = x1 + 9 >= x1 + 8 = 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.43 478.29/120.43 4(0(1(3(4(0(x1)))))) = x1 + 4 >= x1 + 10 = 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.43 478.29/120.43 4(1(4(4(4(1(x1)))))) = x1 >= x1 + 5 = 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.43 478.29/120.43 0(1(3(5(2(2(3(x1))))))) = x1 + 7 >= x1 + 9 = 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.43 478.29/120.43 0(2(3(1(3(2(5(x1))))))) = x1 + 7 >= x1 + 11 = 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.43 478.29/120.43 1(1(3(3(5(3(1(x1))))))) = x1 + 6 >= x1 + 8 = 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.43 478.29/120.43 4(1(4(2(4(0(1(x1))))))) = x1 + 2 >= x1 + 3 = 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.43 478.29/120.43 4(5(1(2(4(4(4(x1))))))) = x1 + 1 >= x1 + 4 = 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.43 478.29/120.43 3(5(2(0(1(3(3(x1))))))) = x1 + 8 >= x1 + 8 = 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.43 478.29/120.43 5(1(4(5(3(3(3(x1))))))) = x1 + 6 >= x1 + 6 = 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.43 problem: 478.29/120.43 strict: 478.29/120.43 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.43 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.43 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.43 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.43 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.43 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.43 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.43 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.43 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.43 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.43 weak: 478.29/120.43 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.43 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.43 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.43 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.43 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.43 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.43 Matrix Interpretation Processor: dim=1 478.29/120.43 478.29/120.43 max_matrix: 478.29/120.43 1 478.29/120.43 interpretation: 478.29/120.43 [0](x0) = x0, 478.29/120.43 478.29/120.43 [2](x0) = x0, 478.29/120.43 478.29/120.43 [5](x0) = x0, 478.29/120.43 478.29/120.43 [4](x0) = x0, 478.29/120.43 478.29/120.43 [1](x0) = x0 + 4, 478.29/120.43 478.29/120.43 [3](x0) = x0 + 2 478.29/120.43 orientation: 478.29/120.43 1(3(3(x1))) = x1 + 8 >= x1 + 4 = 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.43 478.29/120.43 1(4(4(2(2(x1))))) = x1 + 4 >= x1 + 20 = 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.43 478.29/120.43 0(3(3(1(4(3(x1)))))) = x1 + 10 >= x1 + 6 = 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.43 478.29/120.43 4(0(1(3(4(0(x1)))))) = x1 + 6 >= x1 + 2 = 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.43 478.29/120.43 4(1(4(4(4(1(x1)))))) = x1 + 8 >= x1 + 12 = 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.43 478.29/120.43 0(1(3(5(2(2(3(x1))))))) = x1 + 8 >= x1 + 4 = 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.43 478.29/120.43 0(2(3(1(3(2(5(x1))))))) = x1 + 8 >= x1 + 10 = 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.43 478.29/120.43 1(1(3(3(5(3(1(x1))))))) = x1 + 18 >= x1 + 8 = 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.44 478.29/120.44 4(1(4(2(4(0(1(x1))))))) = x1 + 8 >= x1 + 8 = 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.44 478.29/120.44 4(5(1(2(4(4(4(x1))))))) = x1 + 4 >= x1 + 14 = 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.44 478.29/120.44 0(3(3(3(x1)))) = x1 + 6 >= x1 + 4 = 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.44 478.29/120.44 0(3(3(3(1(x1))))) = x1 + 10 >= x1 + 10 = 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.44 478.29/120.44 1(2(3(3(3(x1))))) = x1 + 10 >= x1 + 10 = 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.44 478.29/120.44 3(3(3(3(4(0(x1)))))) = x1 + 8 >= x1 + 8 = 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.44 478.29/120.44 3(5(2(0(1(3(3(x1))))))) = x1 + 10 >= x1 + 6 = 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.44 478.29/120.44 5(1(4(5(3(3(3(x1))))))) = x1 + 10 >= x1 + 8 = 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.44 problem: 478.29/120.44 strict: 478.29/120.44 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.44 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.44 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.44 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.44 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.44 weak: 478.29/120.44 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.44 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.44 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.44 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.44 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.44 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.44 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.44 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.44 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.44 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.44 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.44 Matrix Interpretation Processor: dim=1 478.29/120.44 478.29/120.44 max_matrix: 478.29/120.44 1 478.29/120.44 interpretation: 478.29/120.44 [0](x0) = x0, 478.29/120.44 478.29/120.44 [2](x0) = x0, 478.29/120.44 478.29/120.44 [5](x0) = x0, 478.29/120.44 478.29/120.44 [4](x0) = x0 + 1, 478.29/120.44 478.29/120.44 [1](x0) = x0 + 3, 478.29/120.44 478.29/120.44 [3](x0) = x0 + 3 478.29/120.44 orientation: 478.29/120.44 1(4(4(2(2(x1))))) = x1 + 5 >= x1 + 15 = 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.44 478.29/120.44 4(1(4(4(4(1(x1)))))) = x1 + 10 >= x1 + 14 = 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.44 478.29/120.44 0(2(3(1(3(2(5(x1))))))) = x1 + 9 >= x1 + 13 = 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.44 478.29/120.44 4(1(4(2(4(0(1(x1))))))) = x1 + 9 >= x1 + 7 = 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.44 478.29/120.44 4(5(1(2(4(4(4(x1))))))) = x1 + 7 >= x1 + 15 = 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.44 478.29/120.44 1(3(3(x1))) = x1 + 9 >= x1 + 8 = 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.44 478.29/120.44 0(3(3(1(4(3(x1)))))) = x1 + 13 >= x1 + 11 = 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.44 478.29/120.44 4(0(1(3(4(0(x1)))))) = x1 + 8 >= x1 + 3 = 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.44 478.29/120.44 0(1(3(5(2(2(3(x1))))))) = x1 + 9 >= x1 + 8 = 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.44 478.29/120.44 1(1(3(3(5(3(1(x1))))))) = x1 + 18 >= x1 + 9 = 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.44 478.29/120.44 0(3(3(3(x1)))) = x1 + 9 >= x1 + 9 = 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.44 478.29/120.44 0(3(3(3(1(x1))))) = x1 + 12 >= x1 + 11 = 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.44 478.29/120.44 1(2(3(3(3(x1))))) = x1 + 12 >= x1 + 11 = 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.44 478.29/120.44 3(3(3(3(4(0(x1)))))) = x1 + 13 >= x1 + 10 = 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.44 478.29/120.44 3(5(2(0(1(3(3(x1))))))) = x1 + 12 >= x1 + 12 = 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.44 478.29/120.44 5(1(4(5(3(3(3(x1))))))) = x1 + 13 >= x1 + 12 = 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.44 problem: 478.29/120.44 strict: 478.29/120.44 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.44 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.44 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.44 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.44 weak: 478.29/120.44 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.44 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.44 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.44 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.46 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.46 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.46 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.46 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.46 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.46 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.46 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.46 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.46 Splitting Processor: 478.29/120.46 strict: 478.29/120.46 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.46 weak: 478.29/120.46 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.46 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.46 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.46 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.46 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.46 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.46 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.46 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.46 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.46 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.29/120.46 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.29/120.46 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.29/120.46 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.29/120.46 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.29/120.46 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.29/120.46 Matrix Interpretation Processor: dim=5 478.29/120.46 478.29/120.46 max_matrix: 478.29/120.46 [1 1 0 0 0] 478.29/120.46 [0 0 1 1 1] 478.29/120.46 [0 0 0 0 1] 478.29/120.46 [0 0 0 0 1] 478.29/120.46 [0 0 0 0 0] 478.29/120.46 interpretation: 478.29/120.46 [1 0 0 0 0] [0] 478.29/120.46 [0 0 0 0 0] [0] 478.29/120.46 [0](x0) = [0 0 0 0 0]x0 + [0] 478.29/120.46 [0 0 0 0 0] [1] 478.29/120.46 [0 0 0 0 0] [1], 478.29/120.46 478.29/120.46 [1 0 0 0 0] [0] 478.29/120.46 [0 0 0 0 0] [0] 478.29/120.46 [2](x0) = [0 0 0 0 0]x0 + [1] 478.29/120.46 [0 0 0 0 1] [0] 478.29/120.46 [0 0 0 0 0] [0], 478.29/120.46 478.29/120.46 [1 0 0 0 0] 478.29/120.46 [0 0 0 1 0] 478.29/120.46 [5](x0) = [0 0 0 0 0]x0 478.29/120.46 [0 0 0 0 0] 478.29/120.46 [0 0 0 0 0] , 478.29/120.46 478.29/120.46 [1 0 0 0 0] 478.29/120.46 [0 0 0 0 1] 478.29/120.46 [4](x0) = [0 0 0 0 1]x0 478.29/120.46 [0 0 0 0 1] 478.29/120.46 [0 0 0 0 0] , 478.29/120.46 478.29/120.46 [1 1 0 0 0] [0] 478.29/120.46 [0 0 0 0 0] [0] 478.29/120.46 [1](x0) = [0 0 0 0 0]x0 + [1] 478.29/120.46 [0 0 0 0 0] [1] 478.29/120.46 [0 0 0 0 0] [0], 478.29/120.46 478.29/120.46 [1 0 0 0 0] 478.29/120.46 [0 0 1 0 0] 478.29/120.46 [3](x0) = [0 0 0 0 0]x0 478.29/120.46 [0 0 0 0 0] 478.29/120.46 [0 0 0 0 0] 478.29/120.46 orientation: 478.29/120.46 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 478.29/120.46 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.29/120.46 0(2(3(1(3(2(5(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.29/120.46 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.29/120.46 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.29/120.46 478.29/120.46 [1 1 0 0 0] [1 1 0 0 0] 478.29/120.46 [0 0 0 0 0] [0 0 0 0 0] 478.29/120.46 4(1(4(2(4(0(1(x1))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.29/120.46 [0 0 0 0 0] [0 0 0 0 0] 478.29/120.46 [0 0 0 0 0] [0 0 0 0 0] 478.29/120.46 478.29/120.46 [1 0 0 0 0] [0] [1 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 1(3(3(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 478.29/120.48 [1 0 0 0 0] [0] [1 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 0(3(3(1(4(3(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 478.29/120.48 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.29/120.48 4(0(1(3(4(0(x1)))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.29/120.48 478.29/120.48 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.29/120.48 0(1(3(5(2(2(3(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.29/120.48 478.29/120.48 [1 1 0 0 0] [0] [1 1 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 1(1(3(3(5(3(1(x1))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 478.29/120.48 [1 0 0 0 0] [0] [1 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 0(3(3(3(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 478.29/120.48 [1 1 0 0 0] [0] [1 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 0(3(3(3(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 478.29/120.48 [1 0 0 0 0] [0] [1 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.29/120.48 1(2(3(3(3(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.29/120.48 [0 0 0 0 0] [1] [0 0 0 0 0] 478.29/120.48 [0 0 0 0 0] [0] [0 0 0 0 0] 478.44/120.50 478.44/120.50 [1 0 0 0 0] [1 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 3(3(3(3(4(0(x1)))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 478.44/120.50 [1 0 0 0 0] [1 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 3(5(2(0(1(3(3(x1))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 478.44/120.50 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.50 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.50 5(1(4(5(3(3(3(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.50 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.50 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.50 478.44/120.50 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.50 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.50 1(4(4(2(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.50 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.50 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.50 478.44/120.50 [1 1 0 0 0] [1 1 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 4(1(4(4(4(1(x1)))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 478.44/120.50 [1 0 0 0 0] [1 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 4(5(1(2(4(4(4(x1))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.50 problem: 478.44/120.50 strict: 478.44/120.50 478.44/120.50 weak: 478.44/120.50 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.50 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.50 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.50 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.50 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.50 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.50 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.50 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.50 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.50 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.50 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.50 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.51 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.51 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.51 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.51 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.51 Qed 478.44/120.51 478.44/120.51 strict: 478.44/120.51 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.51 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.51 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.51 weak: 478.44/120.51 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.51 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.51 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.51 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.51 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.51 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.51 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.51 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.51 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.51 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.51 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.51 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.51 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.51 Splitting Processor: 478.44/120.51 strict: 478.44/120.51 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.51 weak: 478.44/120.51 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.51 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.51 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.51 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.51 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.51 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.51 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.51 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.51 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.51 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.51 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.51 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.51 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.51 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.51 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.51 Splitting Processor: 478.44/120.51 strict: 478.44/120.51 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.51 weak: 478.44/120.51 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.51 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.51 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.51 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.51 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.51 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.51 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.51 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.51 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.51 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.51 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.51 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.51 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.51 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.51 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.51 Bounds Processor: 478.44/120.51 bound: 1 478.44/120.51 enrichment: match 478.44/120.51 automaton: 478.44/120.51 final states: {7} 478.44/120.51 transitions: 478.44/120.51 11(45) -> 46* 478.44/120.51 11(242) -> 243* 478.44/120.51 11(40) -> 41* 478.44/120.51 11(227) -> 228* 478.44/120.51 11(62) -> 63* 478.44/120.51 11(57) -> 58* 478.44/120.51 11(27) -> 28* 478.44/120.51 11(44) -> 45* 478.44/120.51 11(39) -> 40* 478.44/120.51 11(41) -> 42* 478.44/120.51 11(26) -> 27* 478.44/120.51 11(21) -> 22* 478.44/120.51 11(193) -> 194* 478.44/120.51 11(173) -> 174* 478.44/120.51 11(68) -> 69* 478.44/120.51 11(170) -> 171* 478.44/120.51 21(70) -> 71* 478.44/120.51 21(379) -> 380* 478.44/120.51 21(152) -> 153* 478.44/120.51 21(52) -> 53* 478.44/120.51 21(37) -> 38* 478.44/120.51 21(214) -> 215* 478.44/120.51 21(194) -> 195* 478.44/120.51 21(381) -> 382* 478.44/120.51 21(124) -> 125* 478.44/120.51 21(69) -> 70* 478.44/120.51 21(54) -> 55* 478.44/120.51 21(438) -> 439* 478.44/120.51 21(221) -> 222* 478.44/120.51 21(216) -> 217* 478.44/120.51 21(106) -> 107* 478.44/120.51 21(278) -> 279* 478.44/120.51 21(56) -> 57* 478.44/120.51 21(36) -> 37* 478.44/120.51 21(420) -> 421* 478.44/120.51 21(188) -> 189* 478.44/120.51 21(123) -> 124* 478.44/120.51 21(93) -> 94* 478.44/120.51 21(275) -> 276* 478.44/120.51 21(43) -> 44* 478.44/120.51 21(90) -> 91* 478.44/120.51 01(60) -> 61* 478.44/120.51 01(30) -> 31* 478.44/120.51 01(20) -> 21* 478.44/120.51 01(192) -> 193* 478.44/120.51 01(172) -> 173* 478.44/120.51 01(142) -> 143* 478.44/120.51 01(117) -> 118* 478.44/120.51 01(107) -> 108* 478.44/120.51 01(102) -> 103* 478.44/120.51 01(67) -> 68* 478.44/120.51 01(244) -> 245* 478.44/120.51 01(42) -> 43* 478.44/120.51 01(22) -> 23* 478.44/120.51 01(164) -> 165* 478.44/120.51 01(361) -> 362* 478.44/120.51 01(149) -> 150* 478.44/120.51 01(119) -> 120* 478.44/120.51 01(104) -> 105* 478.44/120.51 01(276) -> 277* 478.44/120.51 01(236) -> 237* 478.44/120.51 01(196) -> 197* 478.44/120.51 01(146) -> 147* 478.44/120.51 01(121) -> 122* 478.44/120.51 01(111) -> 112* 478.44/120.51 01(308) -> 309* 478.44/120.51 01(91) -> 92* 478.44/120.51 01(51) -> 52* 478.44/120.51 01(430) -> 431* 478.44/120.51 01(183) -> 184* 478.44/120.51 01(143) -> 144* 478.44/120.51 01(250) -> 251* 478.44/120.51 01(38) -> 39* 478.44/120.51 01(195) -> 196* 478.44/120.51 01(185) -> 186* 478.44/120.51 01(175) -> 176* 478.44/120.51 01(155) -> 156* 478.44/120.51 01(150) -> 151* 478.44/120.51 01(145) -> 146* 478.44/120.51 01(120) -> 121* 478.44/120.51 41(272) -> 273* 478.44/120.51 41(25) -> 26* 478.44/120.51 41(424) -> 425* 478.44/120.51 41(222) -> 223* 478.44/120.51 41(212) -> 213* 478.44/120.51 41(162) -> 163* 478.44/120.51 41(274) -> 275* 478.44/120.51 41(184) -> 185* 478.44/120.51 41(109) -> 110* 478.44/120.51 41(89) -> 90* 478.44/120.51 41(64) -> 65* 478.44/120.51 41(59) -> 60* 478.44/120.51 41(226) -> 227* 478.44/120.51 41(19) -> 20* 478.44/120.51 41(383) -> 384* 478.44/120.51 41(176) -> 177* 478.44/120.51 41(373) -> 374* 478.44/120.51 41(161) -> 162* 478.44/120.51 41(141) -> 142* 478.44/120.51 41(318) -> 319* 478.44/120.51 41(238) -> 239* 478.44/120.51 41(223) -> 224* 478.44/120.51 41(218) -> 219* 478.44/120.51 41(213) -> 214* 478.44/120.51 41(168) -> 169* 478.44/120.51 41(340) -> 341* 478.44/120.51 41(320) -> 321* 478.44/120.51 41(432) -> 433* 478.44/120.51 41(28) -> 29* 478.44/120.51 41(382) -> 383* 478.44/120.51 41(140) -> 141* 478.44/120.51 51(277) -> 278* 478.44/120.51 51(65) -> 66* 478.44/120.51 51(182) -> 183* 478.44/120.51 51(92) -> 93* 478.44/120.51 51(436) -> 437* 478.44/120.51 51(154) -> 155* 478.44/120.51 51(144) -> 145* 478.44/120.51 51(24) -> 25* 478.44/120.51 51(211) -> 212* 478.44/120.51 51(191) -> 192* 478.44/120.51 51(186) -> 187* 478.44/120.51 51(171) -> 172* 478.44/120.51 51(166) -> 167* 478.44/120.51 51(151) -> 152* 478.44/120.51 51(273) -> 274* 478.44/120.51 51(71) -> 72* 478.44/120.51 51(66) -> 67* 478.44/120.51 51(233) -> 234* 478.44/120.51 51(385) -> 386* 478.44/120.51 51(163) -> 164* 478.44/120.51 51(118) -> 119* 478.44/120.51 51(88) -> 89* 478.44/120.51 51(280) -> 281* 478.44/120.51 51(63) -> 64* 478.44/120.51 51(225) -> 226* 478.44/120.51 51(367) -> 368* 478.44/120.51 51(95) -> 96* 478.44/120.51 31(55) -> 56* 478.44/120.51 31(217) -> 218* 478.44/120.51 31(187) -> 188* 478.44/120.51 31(384) -> 385* 478.44/120.51 31(167) -> 168* 478.44/120.51 31(147) -> 148* 478.44/120.51 31(122) -> 123* 478.44/120.51 31(279) -> 280* 478.44/120.51 31(234) -> 235* 478.44/120.51 31(224) -> 225* 478.44/120.51 31(174) -> 175* 478.44/120.51 31(139) -> 140* 478.44/120.51 31(94) -> 95* 478.44/120.51 31(281) -> 282* 478.44/120.51 31(96) -> 97* 478.44/120.51 31(380) -> 381* 478.44/120.51 31(153) -> 154* 478.44/120.51 31(108) -> 109* 478.44/120.51 31(103) -> 104* 478.44/120.51 31(58) -> 59* 478.44/120.51 31(53) -> 54* 478.44/120.51 31(235) -> 236* 478.44/120.51 31(23) -> 24* 478.44/120.51 31(220) -> 221* 478.44/120.51 31(215) -> 216* 478.44/120.52 31(190) -> 191* 478.44/120.52 31(165) -> 166* 478.44/120.52 31(105) -> 106* 478.44/120.52 10(7) -> 7* 478.44/120.52 40(7) -> 7* 478.44/120.52 20(7) -> 7* 478.44/120.52 00(7) -> 7* 478.44/120.52 30(7) -> 7* 478.44/120.52 50(7) -> 7* 478.44/120.52 7 -> 182,139,62,51,36,19 478.44/120.52 20 -> 320,88 478.44/120.52 22 -> 242* 478.44/120.52 29 -> 239,63,52,65,20,30,7 478.44/120.52 31 -> 21* 478.44/120.52 37 -> 244,220 478.44/120.52 45 -> 361* 478.44/120.52 46 -> 63,7 478.44/120.52 52 -> 170,161,102 478.44/120.52 60 -> 373* 478.44/120.52 61 -> 245,150,52,7 478.44/120.52 63 -> 238,149 478.44/120.52 64 -> 183,7 478.44/120.52 67 -> 233* 478.44/120.52 71 -> 250* 478.44/120.52 72 -> 64,52,239,20,7 478.44/120.52 89 -> 190* 478.44/120.52 96 -> 379,367,308,272 478.44/120.52 97 -> 140,63,238,149,7,19 478.44/120.52 103 -> 117* 478.44/120.52 110 -> 111,28 478.44/120.52 112 -> 21* 478.44/120.52 123 -> 318* 478.44/120.52 125 -> 162,20,7 478.44/120.52 148 -> 60* 478.44/120.52 150 -> 420* 478.44/120.52 156 -> 95* 478.44/120.52 169 -> 71* 478.44/120.52 177 -> 168* 478.44/120.52 183 -> 211* 478.44/120.52 189 -> 26* 478.44/120.52 197 -> 96* 478.44/120.52 219 -> 96* 478.44/120.52 228 -> 71* 478.44/120.52 237 -> 27* 478.44/120.52 239 -> 65* 478.44/120.52 243 -> 41* 478.44/120.52 245 -> 21* 478.44/120.52 251 -> 52* 478.44/120.52 281 -> 438,436,430,424 478.44/120.52 282 -> 63,238,7,149 478.44/120.52 309 -> 340,102 478.44/120.52 319 -> 141* 478.44/120.52 321 -> 142* 478.44/120.52 341 -> 162* 478.44/120.52 362 -> 170* 478.44/120.52 368 -> 183* 478.44/120.52 374 -> 88* 478.44/120.52 386 -> 28* 478.44/120.52 421 -> 53* 478.44/120.52 425 -> 88* 478.44/120.52 431 -> 432,102 478.44/120.52 433 -> 162* 478.44/120.52 437 -> 183* 478.44/120.52 439 -> 220* 478.44/120.52 problem: 478.44/120.52 strict: 478.44/120.52 478.44/120.52 weak: 478.44/120.52 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.52 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.52 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.52 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.52 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.52 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.52 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.52 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.52 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.52 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.52 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.52 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.52 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.52 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.52 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.52 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.52 Qed 478.44/120.52 478.44/120.52 strict: 478.44/120.52 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.52 weak: 478.44/120.52 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.52 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.52 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.52 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.52 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.52 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.52 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.52 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.52 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.52 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.52 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.52 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.52 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.52 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.52 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.52 Matrix Interpretation Processor: dim=5 478.44/120.52 478.44/120.52 max_matrix: 478.44/120.52 [1 1 0 0 0] 478.44/120.52 [0 0 1 1 1] 478.44/120.52 [0 0 0 1 1] 478.44/120.53 [0 0 0 0 1] 478.44/120.53 [0 0 0 0 0] 478.44/120.53 interpretation: 478.44/120.53 [1 0 0 0 0] 478.44/120.53 [0 0 0 0 0] 478.44/120.53 [0](x0) = [0 0 0 0 1]x0 478.44/120.53 [0 0 0 0 1] 478.44/120.53 [0 0 0 0 0] , 478.44/120.53 478.44/120.53 [1 0 0 0 0] [0] 478.44/120.53 [0 0 0 1 0] [0] 478.44/120.53 [2](x0) = [0 0 0 0 1]x0 + [0] 478.44/120.53 [0 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [0], 478.44/120.53 478.44/120.53 [1 0 0 0 0] 478.44/120.53 [0 0 0 0 0] 478.44/120.53 [5](x0) = [0 0 0 1 0]x0 478.44/120.53 [0 0 0 0 1] 478.44/120.53 [0 0 0 0 0] , 478.44/120.53 478.44/120.53 [1 0 0 0 0] [0] 478.44/120.53 [0 0 1 0 0] [0] 478.44/120.53 [4](x0) = [0 0 0 1 0]x0 + [0] 478.44/120.53 [0 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [0], 478.44/120.53 478.44/120.53 [1 1 0 0 0] [0] 478.44/120.53 [0 0 1 0 0] [0] 478.44/120.53 [1](x0) = [0 0 0 1 0]x0 + [0] 478.44/120.53 [0 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [1], 478.44/120.53 478.44/120.53 [1 0 0 0 0] [0] 478.44/120.53 [0 0 0 0 1] [0] 478.44/120.53 [3](x0) = [0 0 0 0 0]x0 + [0] 478.44/120.53 [0 0 0 0 1] [0] 478.44/120.53 [0 0 0 0 0] [1] 478.44/120.53 orientation: 478.44/120.53 [1 1 0 0 0] [1] [1 1 0 0 0] [0] 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 4(1(4(4(4(1(x1)))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.53 478.44/120.53 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 4(5(1(2(4(4(4(x1))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.53 478.44/120.53 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 1(4(4(2(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.53 478.44/120.53 [1 0 0 0 0] [1 0 0 0 0] 478.44/120.53 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.53 0(2(3(1(3(2(5(x1))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.53 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.53 [0 0 0 0 0] [0 0 0 0 0] 478.44/120.53 478.44/120.53 [1 1 0 0 0] [0] [1 1 0 0 0] [0] 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.53 4(1(4(2(4(0(1(x1))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.53 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.53 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 478.44/120.56 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 1(3(3(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.56 478.44/120.56 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 0(3(3(1(4(3(x1)))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 478.44/120.56 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.56 4(0(1(3(4(0(x1)))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 478.44/120.56 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 0(1(3(5(2(2(3(x1))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 478.44/120.56 [1 1 0 0 0] [1] [1 1 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.56 1(1(3(3(5(3(1(x1))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.56 478.44/120.56 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 0(3(3(3(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 478.44/120.56 [1 1 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 0(3(3(3(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.56 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.56 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.56 478.44/120.56 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.57 1(2(3(3(3(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.57 478.44/120.57 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.57 3(3(3(3(4(0(x1)))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.57 478.44/120.57 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 478.44/120.57 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.57 3(5(2(0(1(3(3(x1))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.57 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.57 478.44/120.57 [1 0 0 0 0] [1] [1 0 0 0 0] [0] 478.44/120.57 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.57 5(1(4(5(3(3(3(x1))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 478.44/120.57 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 478.44/120.57 problem: 478.44/120.57 strict: 478.44/120.57 478.44/120.57 weak: 478.44/120.57 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.57 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.57 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.57 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.57 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.57 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.57 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.57 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.57 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.57 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.57 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.57 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.57 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.57 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.57 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.57 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.57 Qed 478.44/120.57 478.44/120.57 strict: 478.44/120.57 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.57 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.57 weak: 478.44/120.57 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.57 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.57 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.57 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.57 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.57 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.57 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.57 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.57 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.58 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.58 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.58 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.58 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.58 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.58 Bounds Processor: 478.44/120.58 bound: 1 478.44/120.58 enrichment: match 478.44/120.58 automaton: 478.44/120.58 final states: {7} 478.44/120.58 transitions: 478.44/120.58 11(55) -> 56* 478.44/120.58 11(50) -> 51* 478.44/120.58 11(466) -> 467* 478.44/120.58 11(254) -> 255* 478.44/120.58 11(27) -> 28* 478.44/120.58 11(22) -> 23* 478.44/120.58 11(189) -> 190* 478.44/120.58 11(179) -> 180* 478.44/120.58 11(24) -> 25* 478.44/120.58 11(465) -> 466* 478.44/120.58 11(460) -> 461* 478.44/120.58 11(238) -> 239* 478.44/120.58 11(36) -> 37* 478.44/120.58 11(223) -> 224* 478.44/120.58 11(163) -> 164* 478.44/120.58 11(108) -> 109* 478.44/120.58 11(28) -> 29* 478.44/120.58 11(23) -> 24* 478.44/120.58 11(180) -> 181* 478.44/120.58 11(160) -> 161* 478.44/120.58 21(282) -> 283* 478.44/120.58 21(35) -> 36* 478.44/120.58 21(20) -> 21* 478.44/120.58 21(217) -> 218* 478.44/120.58 21(197) -> 198* 478.44/120.58 21(511) -> 512* 478.44/120.58 21(67) -> 68* 478.44/120.58 21(52) -> 53* 478.44/120.58 21(249) -> 250* 478.44/120.58 21(199) -> 200* 478.44/120.58 21(139) -> 140* 478.44/120.58 21(89) -> 90* 478.44/120.58 21(64) -> 65* 478.44/120.58 21(251) -> 252* 478.44/120.58 21(19) -> 20* 478.44/120.58 21(106) -> 107* 478.44/120.58 21(253) -> 254* 478.44/120.58 21(51) -> 52* 478.44/120.58 21(31) -> 32* 478.44/120.58 21(430) -> 431* 478.44/120.58 21(26) -> 27* 478.44/120.58 21(178) -> 179* 478.44/120.58 21(285) -> 286* 478.44/120.58 21(33) -> 34* 478.44/120.58 21(432) -> 433* 478.44/120.58 21(190) -> 191* 478.44/120.58 21(509) -> 510* 478.44/120.58 21(105) -> 106* 478.44/120.58 01(65) -> 66* 478.44/120.58 01(459) -> 460* 478.44/120.58 01(237) -> 238* 478.44/120.58 01(30) -> 31* 478.44/120.58 01(25) -> 26* 478.44/120.58 01(192) -> 193* 478.44/120.58 01(162) -> 163* 478.44/120.58 01(142) -> 143* 478.44/120.58 01(122) -> 123* 478.44/120.58 01(102) -> 103* 478.44/120.58 01(491) -> 492* 478.44/120.58 01(87) -> 88* 478.44/120.58 01(461) -> 462* 478.44/120.58 01(239) -> 240* 478.44/120.58 01(229) -> 230* 478.44/120.58 01(371) -> 372* 478.44/120.58 01(159) -> 160* 478.44/120.58 01(144) -> 145* 478.44/120.58 01(119) -> 120* 478.44/120.58 01(114) -> 115* 478.44/120.58 01(99) -> 100* 478.44/120.58 01(49) -> 50* 478.44/120.58 01(39) -> 40* 478.44/120.58 01(191) -> 192* 478.44/120.58 01(101) -> 102* 478.44/120.58 01(495) -> 496* 478.44/120.58 01(283) -> 284* 478.44/120.58 01(248) -> 249* 478.44/120.58 01(21) -> 22* 478.44/120.58 01(188) -> 189* 478.44/120.58 01(173) -> 174* 478.44/120.58 01(370) -> 371* 478.44/120.58 01(153) -> 154* 478.44/120.58 01(123) -> 124* 478.44/120.58 01(103) -> 104* 478.44/120.58 01(472) -> 473* 478.44/120.58 01(175) -> 176* 478.44/120.58 01(165) -> 166* 478.44/120.58 01(342) -> 343* 478.44/120.58 01(120) -> 121* 478.44/120.58 01(499) -> 500* 478.44/120.58 01(90) -> 91* 478.44/120.58 01(85) -> 86* 478.44/120.58 41(474) -> 475* 478.44/120.58 41(464) -> 465* 478.44/120.58 41(242) -> 243* 478.44/120.58 41(434) -> 435* 478.44/120.58 41(424) -> 425* 478.44/120.58 41(222) -> 223* 478.44/120.58 41(384) -> 385* 478.44/120.58 41(374) -> 375* 478.44/120.58 41(369) -> 370* 478.44/120.58 41(157) -> 158* 478.44/120.58 41(117) -> 118* 478.44/120.58 41(92) -> 93* 478.44/120.58 41(279) -> 280* 478.44/120.58 41(476) -> 477* 478.44/120.58 41(219) -> 220* 478.44/120.58 41(174) -> 175* 478.44/120.58 41(513) -> 514* 478.44/120.58 41(281) -> 282* 478.44/120.58 41(256) -> 257* 478.44/120.58 41(433) -> 434* 478.44/120.58 41(201) -> 202* 478.44/120.58 41(196) -> 197* 478.44/120.58 41(368) -> 369* 478.44/120.58 41(166) -> 167* 478.44/120.58 41(151) -> 152* 478.44/120.58 41(505) -> 506* 478.44/120.58 41(61) -> 62* 478.44/120.58 41(46) -> 47* 478.44/120.58 41(218) -> 219* 478.44/120.58 41(118) -> 119* 478.44/120.58 41(507) -> 508* 478.44/120.58 41(497) -> 498* 478.44/120.58 41(93) -> 94* 478.44/120.58 41(63) -> 64* 478.44/120.58 41(38) -> 39* 478.44/120.58 41(437) -> 438* 478.44/120.58 41(235) -> 236* 478.44/120.58 41(195) -> 196* 478.44/120.58 41(150) -> 151* 478.44/120.58 41(489) -> 490* 478.44/120.58 51(45) -> 46* 478.44/120.58 51(404) -> 405* 478.44/120.58 51(187) -> 188* 478.44/120.58 51(172) -> 173* 478.44/120.58 51(152) -> 153* 478.44/120.58 51(501) -> 502* 478.44/120.58 51(284) -> 285* 478.44/120.58 51(62) -> 63* 478.44/120.58 51(47) -> 48* 478.44/120.58 51(436) -> 437* 478.44/120.58 51(194) -> 195* 478.44/120.58 51(503) -> 504* 478.44/120.58 51(69) -> 70* 478.44/120.58 51(463) -> 464* 478.44/120.58 51(241) -> 242* 478.44/120.58 51(226) -> 227* 478.44/120.58 51(221) -> 222* 478.44/120.58 51(176) -> 177* 478.44/120.58 51(161) -> 162* 478.44/120.58 51(141) -> 142* 478.44/120.58 51(121) -> 122* 478.44/120.58 51(66) -> 67* 478.44/120.58 51(138) -> 139* 478.44/120.58 51(517) -> 518* 478.44/120.58 51(280) -> 281* 478.44/120.58 51(53) -> 54* 478.44/120.58 51(48) -> 49* 478.44/120.58 51(225) -> 226* 478.44/120.58 51(372) -> 373* 478.44/120.58 51(170) -> 171* 478.44/120.58 51(155) -> 156* 478.44/120.58 51(100) -> 101* 478.44/120.58 51(287) -> 288* 478.44/120.58 31(70) -> 71* 478.44/120.58 31(252) -> 253* 478.44/120.58 31(227) -> 228* 478.44/120.58 31(177) -> 178* 478.44/120.58 31(37) -> 38* 478.44/120.58 31(32) -> 33* 478.44/120.58 31(431) -> 432* 478.44/120.58 31(164) -> 165* 478.44/120.58 31(154) -> 155* 478.44/120.58 31(124) -> 125* 478.44/120.58 31(104) -> 105* 478.44/120.58 31(286) -> 287* 478.44/120.58 31(34) -> 35* 478.44/120.58 31(216) -> 217* 478.44/120.58 31(186) -> 187* 478.44/120.58 31(156) -> 157* 478.44/120.58 31(116) -> 117* 478.44/120.58 31(91) -> 92* 478.44/120.58 31(288) -> 289* 478.44/120.58 31(86) -> 87* 478.44/120.58 31(435) -> 436* 478.44/120.58 31(228) -> 229* 478.44/120.58 31(198) -> 199* 478.44/120.58 31(88) -> 89* 478.44/120.58 31(68) -> 69* 478.44/120.58 31(462) -> 463* 478.44/120.58 31(255) -> 256* 478.44/120.58 31(250) -> 251* 478.44/120.58 31(447) -> 448* 478.44/120.58 31(240) -> 241* 478.44/120.58 31(220) -> 221* 478.44/120.58 31(200) -> 201* 478.44/120.58 31(140) -> 141* 478.44/120.58 10(7) -> 7* 478.44/120.58 40(7) -> 7* 478.44/120.58 20(7) -> 7* 478.44/120.58 00(7) -> 7* 478.44/120.58 30(7) -> 7* 478.44/120.58 50(7) -> 7* 478.44/120.58 7 -> 172,116,61,55,30,19 478.44/120.58 20 -> 216,114 478.44/120.58 28 -> 159* 478.44/120.58 29 -> 56,45,7 478.44/120.58 30 -> 505* 478.44/120.58 31 -> 7,150,108,85 478.44/120.58 39 -> 424* 478.44/120.58 40 -> 473,145,115,7 478.44/120.58 45 -> 472* 478.44/120.58 46 -> 7* 478.44/120.58 47 -> 475,7 478.44/120.58 53 -> 248* 478.44/120.58 54 -> 514,506,46,173,31,236,7 478.44/120.58 56 -> 235,144,45 478.44/120.58 62 -> 374,237 478.44/120.58 63 -> 225,186 478.44/120.58 70 -> 430,404,342,279 478.44/120.58 71 -> 117,56,144,235,45,7,19 478.44/120.58 86 -> 138,99 478.44/120.58 93 -> 459* 478.44/120.58 94 -> 514,506,47,236,56,31,7 478.44/120.58 105 -> 368* 478.44/120.58 107 -> 506,62,151,7 478.44/120.58 109 -> 170,23 478.44/120.58 114 -> 507* 478.44/120.58 115 -> 31,7,22 478.44/120.58 117 -> 517* 478.44/120.58 125 -> 39* 478.44/120.58 143 -> 69* 478.44/120.58 145 -> 85* 478.44/120.58 158 -> 53* 478.44/120.58 167 -> 157* 478.44/120.58 171 -> 162* 478.44/120.58 173 -> 474,194 478.44/120.58 181 -> 93* 478.44/120.58 193 -> 70* 478.44/120.58 195 -> 447* 478.44/120.58 202 -> 70* 478.44/120.58 224 -> 53* 478.44/120.58 230 -> 180* 478.44/120.58 236 -> 62* 478.44/120.58 243 -> 179* 478.44/120.58 257 -> 114* 478.44/120.58 288 -> 511,503,491,489 478.44/120.58 289 -> 56,144,7,30,61,172,116,55,19,235,45 478.44/120.58 343 -> 384,85 478.44/120.58 373 -> 191* 478.44/120.58 375 -> 370* 478.44/120.58 385 -> 151* 478.44/120.58 405 -> 173* 478.44/120.58 425 -> 62* 478.44/120.58 438 -> 28* 478.44/120.58 447 -> 509,501,495,476 478.44/120.58 448 -> 70* 478.44/120.58 466 -> 499* 478.44/120.58 467 -> 46* 478.44/120.58 472 -> 513* 478.44/120.58 473 -> 31* 478.44/120.58 475 -> 47* 478.44/120.58 477 -> 62* 478.44/120.58 490 -> 62* 478.44/120.58 492 -> 497,85 478.44/120.58 496 -> 150* 478.44/120.58 498 -> 151* 478.44/120.58 500 -> 108* 478.44/120.58 502 -> 173* 478.44/120.58 504 -> 173* 478.44/120.58 506 -> 62* 478.44/120.58 508 -> 62* 478.44/120.58 510 -> 216* 478.44/120.58 512 -> 216* 478.44/120.58 514 -> 62* 478.44/120.58 518 -> 242* 478.44/120.58 problem: 478.44/120.58 strict: 478.44/120.58 478.44/120.58 weak: 478.44/120.58 1(4(4(2(2(x1))))) -> 1(1(2(0(1(1(1(0(2(2(x1)))))))))) 478.44/120.58 0(2(3(1(3(2(5(x1))))))) -> 0(4(3(1(2(3(2(3(2(0(x1)))))))))) 478.44/120.58 4(1(4(2(4(0(1(x1))))))) -> 5(2(2(1(0(5(5(4(5(1(x1)))))))))) 478.44/120.58 1(3(3(x1))) -> 3(5(3(2(5(0(2(4(5(4(x1)))))))))) 478.44/120.58 0(3(3(1(4(3(x1)))))) -> 4(4(3(0(2(3(0(3(0(0(x1)))))))))) 478.44/120.58 4(0(1(3(4(0(x1)))))) -> 2(2(3(0(0(0(5(0(0(0(x1)))))))))) 478.44/120.58 0(1(3(5(2(2(3(x1))))))) -> 0(3(0(0(5(0(0(4(4(3(x1)))))))))) 478.44/120.58 1(1(3(3(5(3(1(x1))))))) -> 3(5(0(5(3(2(5(0(0(1(x1)))))))))) 478.44/120.58 0(3(3(3(x1)))) -> 5(4(3(5(3(0(5(4(4(0(x1)))))))))) 478.44/120.58 0(3(3(3(1(x1))))) -> 5(4(4(0(3(1(0(5(1(0(x1)))))))))) 478.44/120.58 1(2(3(3(3(x1))))) -> 4(1(1(2(3(5(0(4(0(5(x1)))))))))) 478.44/120.58 3(3(3(3(4(0(x1)))))) -> 3(0(0(2(1(0(5(3(5(4(x1)))))))))) 478.44/120.58 3(5(2(0(1(3(3(x1))))))) -> 3(4(3(2(3(2(4(4(5(5(x1)))))))))) 478.44/120.58 5(1(4(5(3(3(3(x1))))))) -> 5(1(4(5(3(4(4(2(3(2(x1)))))))))) 478.44/120.58 4(1(4(4(4(1(x1)))))) -> 4(1(0(3(3(5(5(5(4(1(x1)))))))))) 478.44/120.58 4(5(1(2(4(4(4(x1))))))) -> 4(1(1(4(5(3(0(1(0(4(x1)))))))))) 478.44/120.58 Qed 478.44/120.59 EOF