YES(?,O(n^1)) 853.58/216.07 YES(?,O(n^1)) 853.58/216.08 853.58/216.08 Problem: 853.58/216.08 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.58/216.08 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.58/216.08 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.58/216.08 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.58/216.08 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.58/216.08 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.58/216.08 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.58/216.08 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.58/216.08 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.58/216.08 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.58/216.08 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.58/216.08 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.58/216.08 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.58/216.08 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.58/216.08 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.58/216.08 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.58/216.08 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.58/216.08 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.58/216.08 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.58/216.08 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.58/216.08 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.58/216.08 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.58/216.08 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.58/216.08 853.58/216.08 Proof: 853.58/216.08 Complexity Transformation Processor: 853.58/216.08 strict: 853.58/216.08 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.58/216.08 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.58/216.08 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.58/216.08 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.58/216.08 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.58/216.08 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.58/216.08 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.58/216.08 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.58/216.08 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.58/216.08 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.58/216.08 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.58/216.08 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.58/216.08 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.58/216.08 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.58/216.08 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.58/216.08 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.58/216.08 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.58/216.08 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.58/216.08 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.58/216.08 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.58/216.08 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.58/216.08 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.58/216.08 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.58/216.08 weak: 853.58/216.08 853.58/216.08 Matrix Interpretation Processor: dim=1 853.58/216.08 853.58/216.08 max_matrix: 853.58/216.08 1 853.58/216.08 interpretation: 853.58/216.08 [5](x0) = x0 + 1, 853.58/216.08 853.58/216.08 [1](x0) = x0, 853.58/216.08 853.58/216.08 [2](x0) = x0 + 1, 853.58/216.08 853.58/216.08 [3](x0) = x0 + 1, 853.58/216.08 853.58/216.08 [0](x0) = x0, 853.58/216.08 853.58/216.08 [4](x0) = x0 853.58/216.08 orientation: 853.58/216.08 0(1(2(2(3(0(4(4(x1)))))))) = x1 + 3 >= x1 + 2 = 0(4(5(0(3(4(0(4(x1)))))))) 853.58/216.08 853.58/216.08 0(2(2(2(0(5(2(5(4(x1))))))))) = x1 + 6 >= x1 + 2 = 0(0(0(3(4(3(0(1(0(x1))))))))) 853.58/216.08 853.58/216.08 2(1(1(3(4(3(1(1(5(x1))))))))) = x1 + 4 >= x1 + 4 = 1(0(2(3(1(0(5(1(5(x1))))))))) 853.58/216.08 853.58/216.08 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) = x1 + 6 >= x1 + 9 = 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.58/216.08 853.58/216.08 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) = x1 + 6 >= x1 + 4 = 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.58/216.08 853.58/216.08 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) = x1 + 8 >= x1 + 4 = 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.58/216.08 853.58/216.08 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) = x1 + 8 >= x1 + 8 = 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.58/216.09 853.58/216.09 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) = x1 + 10 >= x1 + 10 = 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.58/216.09 853.58/216.09 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) = x1 + 9 >= x1 + 8 = 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.58/216.09 853.58/216.09 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) = x1 + 5 >= x1 + 6 = 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.58/216.09 853.58/216.09 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) = x1 + 6 >= x1 + 9 = 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.58/216.09 853.58/216.09 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) = x1 + 9 >= x1 + 7 = 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.58/216.09 853.58/216.09 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) = x1 + 13 >= x1 + 11 = 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.58/216.09 853.58/216.09 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) = x1 + 10 >= x1 + 8 = 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.58/216.09 853.58/216.09 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) = x1 + 10 >= x1 + 9 = 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.58/216.09 problem: 853.58/216.09 strict: 853.58/216.09 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.58/216.09 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.58/216.09 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.58/216.09 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.58/216.09 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.58/216.09 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.58/216.09 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.58/216.09 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.58/216.09 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.58/216.09 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.58/216.09 weak: 853.58/216.09 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.58/216.09 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.58/216.09 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.58/216.09 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.58/216.09 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.58/216.09 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.58/216.09 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.58/216.09 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.58/216.09 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.58/216.09 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.58/216.09 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.58/216.09 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.58/216.09 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.58/216.09 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.58/216.09 Matrix Interpretation Processor: dim=1 853.58/216.09 853.58/216.09 max_matrix: 853.58/216.09 1 853.58/216.09 interpretation: 853.58/216.09 [5](x0) = x0, 853.58/216.09 853.58/216.09 [1](x0) = x0, 853.58/216.09 853.58/216.09 [2](x0) = x0 + 2, 853.58/216.09 853.58/216.09 [3](x0) = x0 + 4, 853.58/216.09 853.58/216.09 [0](x0) = x0, 853.58/216.09 853.58/216.09 [4](x0) = x0 853.58/216.09 orientation: 853.58/216.09 2(1(1(3(4(3(1(1(5(x1))))))))) = x1 + 10 >= x1 + 6 = 1(0(2(3(1(0(5(1(5(x1))))))))) 853.58/216.09 853.58/216.09 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) = x1 + 14 >= x1 + 12 = 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.58/216.09 853.58/216.09 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) = x1 + 14 >= x1 + 18 = 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.58/216.09 853.58/216.09 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) = x1 + 20 >= x1 + 20 = 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.58/216.09 853.58/216.09 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) = x1 + 14 >= x1 + 16 = 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.58/216.09 853.58/216.09 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) = x1 + 12 >= x1 + 30 = 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.58/216.09 853.58/216.09 0(1(2(2(3(0(4(4(x1)))))))) = x1 + 8 >= x1 + 4 = 0(4(5(0(3(4(0(4(x1)))))))) 853.58/216.09 853.58/216.09 0(2(2(2(0(5(2(5(4(x1))))))))) = x1 + 8 >= x1 + 8 = 0(0(0(3(4(3(0(1(0(x1))))))))) 853.58/216.09 853.58/216.09 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) = x1 + 14 >= x1 + 10 = 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.11 853.67/216.11 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) = x1 + 20 >= x1 + 2 = 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.11 853.67/216.11 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) = x1 + 18 >= x1 + 10 = 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.11 853.67/216.11 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) = x1 + 30 >= x1 + 14 = 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.11 853.67/216.11 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) = x1 + 26 >= x1 + 18 = 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.11 853.67/216.11 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) = x1 + 26 >= x1 + 20 = 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.11 853.67/216.11 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) = x1 + 20 >= x1 + 14 = 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.11 problem: 853.67/216.11 strict: 853.67/216.11 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.67/216.11 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.11 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.67/216.11 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.11 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.67/216.11 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.11 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.67/216.11 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.11 weak: 853.67/216.11 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.11 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.11 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.11 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.11 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.11 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.11 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.67/216.11 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.11 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.67/216.11 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.11 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.67/216.11 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.11 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.67/216.11 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.11 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.67/216.11 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.11 Splitting Processor: 853.67/216.11 strict: 853.67/216.11 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.67/216.11 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.11 weak: 853.67/216.11 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.11 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.11 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.11 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.11 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.11 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.11 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.67/216.11 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.11 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.67/216.11 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.11 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.67/216.11 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.11 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.67/216.11 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.11 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.67/216.11 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.11 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.67/216.11 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.12 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.67/216.12 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.12 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.67/216.12 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.12 Arctic Interpretation Processor: 853.67/216.12 dimension: 1 853.67/216.12 interpretation: 853.67/216.12 [5](x0) = 1x0, 853.67/216.12 853.67/216.12 [1](x0) = 1x0, 853.67/216.12 853.67/216.12 [2](x0) = 1x0, 853.67/216.12 853.67/216.12 [3](x0) = 1x0, 853.67/216.12 853.67/216.12 [0](x0) = 1x0, 853.67/216.12 853.67/216.12 [4](x0) = 1x0 853.67/216.12 orientation: 853.67/216.12 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) = 15x1 >= 14x1 = 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.12 853.67/216.12 2(1(1(3(4(3(1(1(5(x1))))))))) = 9x1 >= 9x1 = 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.12 853.67/216.12 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) = 11x1 >= 11x1 = 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.12 853.67/216.12 0(1(2(2(3(0(4(4(x1)))))))) = 8x1 >= 8x1 = 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.12 853.67/216.12 0(2(2(2(0(5(2(5(4(x1))))))))) = 9x1 >= 9x1 = 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.12 853.67/216.12 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) = 12x1 >= 12x1 = 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.12 853.67/216.12 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) = 14x1 >= 13x1 = 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.12 853.67/216.12 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) = 17x1 >= 17x1 = 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.12 853.67/216.12 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) = 20x1 >= 19x1 = 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.12 853.67/216.12 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) = 20x1 >= 19x1 = 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.12 853.67/216.12 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) = 20x1 >= 20x1 = 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.12 853.67/216.12 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) = 20x1 >= 19x1 = 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.12 853.67/216.12 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) = 17x1 >= 17x1 = 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.12 853.67/216.12 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) = 18x1 >= 18x1 = 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.12 853.67/216.12 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) = 20x1 >= 20x1 = 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.12 problem: 853.67/216.12 strict: 853.67/216.12 853.67/216.12 weak: 853.67/216.12 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.67/216.12 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.12 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.12 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.12 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.12 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.12 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.12 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.12 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.67/216.12 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.12 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.67/216.12 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.12 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.67/216.12 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.12 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.67/216.12 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.12 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.67/216.12 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.12 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.67/216.12 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.12 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.67/216.12 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.12 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.67/216.13 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.13 Qed 853.67/216.13 853.67/216.13 strict: 853.67/216.13 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.67/216.13 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.13 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.67/216.13 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.13 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.67/216.13 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.13 weak: 853.67/216.13 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.67/216.13 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.13 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.13 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.13 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.13 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.13 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.13 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.13 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.67/216.13 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.13 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.67/216.13 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.13 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.67/216.13 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.13 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.67/216.13 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.13 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.67/216.13 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.13 Splitting Processor: 853.67/216.13 strict: 853.67/216.13 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.67/216.13 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.13 weak: 853.67/216.13 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.67/216.13 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.13 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.13 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.13 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.13 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.13 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.13 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.13 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.67/216.13 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.13 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.67/216.13 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.13 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.67/216.13 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.13 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.67/216.13 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.13 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.67/216.13 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.13 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.67/216.13 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.13 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.67/216.13 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.13 Matrix Interpretation Processor: dim=3 853.67/216.13 853.67/216.13 max_matrix: 853.67/216.13 [1 2 0] 853.67/216.13 [0 0 1] 853.67/216.13 [0 0 0] 853.67/216.13 interpretation: 853.67/216.13 [1 0 0] [0] 853.67/216.13 [5](x0) = [0 0 0]x0 + [0] 853.67/216.13 [0 0 0] [2], 853.67/216.13 853.67/216.13 [1 1 0] 853.67/216.13 [1](x0) = [0 0 0]x0 853.67/216.13 [0 0 0] , 853.67/216.13 853.67/216.13 [1 0 0] [0] 853.67/216.13 [2](x0) = [0 0 0]x0 + [0] 853.67/216.13 [0 0 0] [2], 853.67/216.13 853.67/216.13 [1 2 0] 853.67/216.13 [3](x0) = [0 0 0]x0 853.67/216.13 [0 0 0] , 853.67/216.13 853.67/216.13 [1 0 0] 853.67/216.15 [0](x0) = [0 0 0]x0 853.67/216.15 [0 0 0] , 853.67/216.15 853.67/216.15 [1 0 0] 853.67/216.15 [4](x0) = [0 0 1]x0 853.67/216.15 [0 0 0] 853.67/216.15 orientation: 853.67/216.15 [1 0 0] [2] [1 0 0] 853.67/216.15 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.15 [0 0 0] [0] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [1 0 0] 853.67/216.15 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) = [0 0 0]x1 >= [0 0 0]x1 = 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.15 [0 0 0] [0 0 0] 853.67/216.15 853.67/216.15 [1 2 0] [1 0 0] 853.67/216.15 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) = [0 0 0]x1 >= [0 0 0]x1 = 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.15 [0 0 0] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [0] [1 0 0] 853.67/216.15 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.15 [0 0 0] [2] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [0] [1 0 0] 853.67/216.15 2(1(1(3(4(3(1(1(5(x1))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.15 [0 0 0] [2] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [0] [1 0 0] [0] 853.67/216.15 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.15 [0 0 0] [2] [0 0 0] [2] 853.67/216.15 853.67/216.15 [1 0 0] [1 0 0] 853.67/216.15 0(1(2(2(3(0(4(4(x1)))))))) = [0 0 0]x1 >= [0 0 0]x1 = 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.15 [0 0 0] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [1 0 0] 853.67/216.15 0(2(2(2(0(5(2(5(4(x1))))))))) = [0 0 0]x1 >= [0 0 0]x1 = 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.15 [0 0 0] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [0] [1 0 0] 853.67/216.15 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.15 [0 0 0] [2] [0 0 0] 853.67/216.15 853.67/216.15 [1 2 0] [1 0 0] 853.67/216.15 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) = [0 0 0]x1 >= [0 0 0]x1 = 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.15 [0 0 0] [0 0 0] 853.67/216.15 853.67/216.15 [1 0 0] [0] [1 0 0] [0] 853.67/216.17 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.17 [0 0 0] [2] [0 0 0] [2] 853.67/216.17 853.67/216.17 [1 2 0] [0] [1 0 0] [0] 853.67/216.17 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.17 [0 0 0] [2] [0 0 0] [2] 853.67/216.17 853.67/216.17 [1 0 0] [0] [1 0 0] 853.67/216.17 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.17 [0 0 0] [2] [0 0 0] 853.67/216.17 853.67/216.17 [1 0 1] [1 0 0] 853.67/216.17 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) = [0 0 0]x1 >= [0 0 0]x1 = 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.17 [0 0 0] [0 0 0] 853.67/216.17 853.67/216.17 [1 2 0] [0] [1 1 0] [0] 853.67/216.17 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.17 [0 0 0] [0] [0 0 0] [0] 853.67/216.17 problem: 853.67/216.17 strict: 853.67/216.17 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.67/216.17 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.67/216.17 weak: 853.67/216.17 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.67/216.17 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.67/216.17 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.67/216.17 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.67/216.17 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.67/216.17 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.67/216.17 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.67/216.17 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.67/216.17 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.67/216.17 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.67/216.17 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.67/216.17 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.67/216.17 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.67/216.17 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.67/216.17 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.67/216.17 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.67/216.17 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.67/216.17 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.67/216.17 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.67/216.17 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.67/216.17 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.67/216.17 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.67/216.20 Matrix Interpretation Processor: dim=5 853.67/216.20 853.67/216.20 max_matrix: 853.67/216.20 [1 1 0 1 0] 853.67/216.20 [0 0 0 1 0] 853.67/216.20 [0 0 0 0 1] 853.67/216.20 [0 0 0 0 1] 853.67/216.20 [0 0 0 0 0] 853.67/216.20 interpretation: 853.67/216.20 [1 1 0 0 0] 853.67/216.20 [0 0 0 0 0] 853.67/216.20 [5](x0) = [0 0 0 0 1]x0 853.67/216.20 [0 0 0 0 0] 853.67/216.20 [0 0 0 0 0] , 853.67/216.20 853.67/216.20 [1 0 0 1 0] [0] 853.67/216.20 [0 0 0 0 0] [0] 853.67/216.20 [1](x0) = [0 0 0 0 0]x0 + [0] 853.67/216.20 [0 0 0 0 0] [0] 853.67/216.20 [0 0 0 0 0] [1], 853.67/216.20 853.67/216.20 [1 0 0 0 0] [0] 853.67/216.20 [0 0 0 0 0] [0] 853.67/216.20 [2](x0) = [0 0 0 0 0]x0 + [1] 853.67/216.20 [0 0 0 0 0] [0] 853.67/216.20 [0 0 0 0 0] [1], 853.67/216.20 853.67/216.20 [1 0 0 0 0] [0] 853.67/216.20 [0 0 0 1 0] [0] 853.67/216.20 [3](x0) = [0 0 0 0 0]x0 + [0] 853.67/216.20 [0 0 0 0 0] [0] 853.67/216.20 [0 0 0 0 0] [1], 853.78/216.20 853.78/216.20 [1 0 0 0 0] 853.78/216.20 [0 0 0 0 0] 853.78/216.20 [0](x0) = [0 0 0 0 0]x0 853.78/216.20 [0 0 0 0 0] 853.78/216.20 [0 0 0 0 0] , 853.78/216.20 853.78/216.20 [1 0 0 0 0] 853.78/216.20 [0 0 0 0 0] 853.78/216.20 [4](x0) = [0 0 0 0 0]x0 853.78/216.20 [0 0 0 0 1] 853.78/216.20 [0 0 0 0 0] 853.78/216.20 orientation: 853.78/216.20 [1 0 0 0 0] [1] [1 0 0 0 0] 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.20 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.20 853.78/216.20 [1 1 0 0 0] [0] [1 1 0 0 0] [0] 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.20 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 853.78/216.20 853.78/216.20 [1 0 0 1 0] [1] [1 0 0 0 0] [0] 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.20 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.78/216.20 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.20 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 853.78/216.20 853.78/216.20 [1 1 0 0 0] [0] [1 1 0 0 0] 853.78/216.22 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.22 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.78/216.22 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [1] [0 0 0 0 0] 853.78/216.22 853.78/216.22 [1 1 0 0 0] [0] [1 1 0 0 0] [0] 853.78/216.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.22 2(1(1(3(4(3(1(1(5(x1))))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 1(0(2(3(1(0(5(1(5(x1))))))))) 853.78/216.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.22 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 853.78/216.22 853.78/216.22 [1 0 0 0 0] [1 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 853.78/216.22 [1 0 0 0 0] [1 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 0(1(2(2(3(0(4(4(x1)))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(4(5(0(3(4(0(4(x1)))))))) 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 853.78/216.22 [1 0 0 0 0] [1 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 0(2(2(2(0(5(2(5(4(x1))))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(0(0(3(4(3(0(1(0(x1))))))))) 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 853.78/216.22 [1 0 0 0 0] [0] [1 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.22 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.78/216.22 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [1] [0 0 0 0 0] 853.78/216.22 853.78/216.22 [1 0 0 1 0] [1 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.22 [0 0 0 0 0] [0 0 0 0 0] 853.78/216.25 853.78/216.25 [1 1 0 0 0] [1] [1 1 0 0 0] 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.25 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] 853.78/216.25 853.78/216.25 [1 0 0 1 0] [0] [1 0 0 0 0] [0] 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 853.78/216.25 853.78/216.25 [1 1 0 0 0] [0] [1 1 0 0 0] [0] 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 853.78/216.25 853.78/216.25 [1 0 0 0 1] [0] [1 0 0 0 0] [0] 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 853.78/216.25 853.78/216.25 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 853.78/216.25 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.25 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.78/216.26 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 853.78/216.26 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 853.78/216.26 problem: 853.78/216.26 strict: 853.78/216.26 853.78/216.26 weak: 853.78/216.26 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.78/216.26 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.78/216.26 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.78/216.26 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.78/216.26 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.78/216.26 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.78/216.26 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.78/216.26 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.78/216.26 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.78/216.26 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.78/216.26 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.78/216.26 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.78/216.26 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.78/216.26 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.78/216.26 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.78/216.26 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.78/216.26 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.78/216.26 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.78/216.26 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.78/216.26 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.78/216.26 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.78/216.26 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.78/216.26 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.78/216.26 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.78/216.26 Qed 853.78/216.26 853.78/216.26 strict: 853.78/216.26 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.78/216.26 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.78/216.26 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.78/216.26 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.78/216.26 weak: 853.78/216.26 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.78/216.26 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.78/216.26 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.78/216.26 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.78/216.26 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.78/216.26 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.78/216.26 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.78/216.26 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.78/216.26 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.78/216.26 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.78/216.26 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.78/216.26 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.78/216.26 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.78/216.26 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.78/216.26 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.78/216.26 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.78/216.26 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.78/216.26 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.78/216.26 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.78/216.26 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.78/216.26 Bounds Processor: 853.78/216.26 bound: 1 853.78/216.26 enrichment: match 853.78/216.26 automaton: 853.78/216.26 final states: {7} 853.78/216.26 transitions: 853.78/216.26 11(80) -> 81* 853.78/216.26 11(237) -> 238* 853.78/216.26 11(152) -> 153* 853.78/216.26 11(107) -> 108* 853.78/216.27 11(97) -> 98* 853.78/216.27 11(82) -> 83* 853.78/216.27 11(72) -> 73* 853.78/216.27 11(62) -> 63* 853.78/216.27 11(244) -> 245* 853.78/216.27 11(234) -> 235* 853.78/216.27 11(154) -> 155* 853.78/216.27 11(124) -> 125* 853.78/216.27 11(114) -> 115* 853.78/216.27 11(79) -> 80* 853.78/216.27 11(226) -> 227* 853.78/216.27 11(176) -> 177* 853.78/216.27 11(71) -> 72* 853.78/216.27 11(193) -> 194* 853.78/216.27 11(153) -> 154* 853.78/216.27 11(133) -> 134* 853.78/216.27 11(78) -> 79* 853.78/216.27 11(48) -> 49* 853.78/216.27 11(200) -> 201* 853.78/216.27 11(175) -> 176* 853.78/216.27 11(165) -> 166* 853.78/216.27 11(120) -> 121* 853.78/216.27 11(110) -> 111* 853.78/216.27 31(45) -> 46* 853.78/216.27 31(232) -> 233* 853.78/216.27 31(227) -> 228* 853.78/216.27 31(187) -> 188* 853.78/216.27 31(177) -> 178* 853.78/216.27 31(167) -> 168* 853.78/216.27 31(77) -> 78* 853.78/216.27 31(47) -> 48* 853.78/216.27 31(37) -> 38* 853.78/216.27 31(119) -> 120* 853.78/216.27 31(64) -> 65* 853.78/216.27 31(34) -> 35* 853.78/216.27 31(201) -> 202* 853.78/216.27 31(166) -> 167* 853.78/216.27 31(111) -> 112* 853.78/216.27 31(101) -> 102* 853.78/216.27 31(96) -> 97* 853.78/216.27 31(66) -> 67* 853.78/216.27 31(31) -> 32* 853.78/216.27 31(223) -> 224* 853.78/216.27 31(103) -> 104* 853.78/216.27 31(98) -> 99* 853.78/216.27 31(83) -> 84* 853.78/216.27 31(53) -> 54* 853.78/216.27 31(38) -> 39* 853.78/216.27 31(170) -> 171* 853.78/216.27 31(155) -> 156* 853.78/216.27 01(35) -> 36* 853.78/216.27 01(202) -> 203* 853.78/216.27 01(137) -> 138* 853.78/216.27 01(132) -> 133* 853.78/216.27 01(67) -> 68* 853.78/216.27 01(224) -> 225* 853.78/216.27 01(109) -> 110* 853.78/216.27 01(104) -> 105* 853.78/216.27 01(54) -> 55* 853.78/216.27 01(241) -> 242* 853.78/216.27 01(39) -> 40* 853.78/216.27 01(29) -> 30* 853.78/216.27 01(196) -> 197* 853.78/216.27 01(141) -> 142* 853.78/216.27 01(136) -> 137* 853.78/216.27 01(121) -> 122* 853.78/216.27 01(81) -> 82* 853.78/216.27 01(76) -> 77* 853.78/216.27 01(51) -> 52* 853.78/216.27 01(46) -> 47* 853.78/216.27 01(243) -> 244* 853.78/216.27 01(203) -> 204* 853.78/216.27 01(198) -> 199* 853.78/216.27 01(163) -> 164* 853.78/216.27 01(123) -> 124* 853.78/216.27 01(113) -> 114* 853.78/216.27 01(68) -> 69* 853.78/216.27 01(63) -> 64* 853.78/216.27 01(33) -> 34* 853.78/216.27 01(185) -> 186* 853.78/216.27 01(135) -> 136* 853.78/216.27 01(105) -> 106* 853.78/216.27 01(100) -> 101* 853.78/216.27 01(95) -> 96* 853.78/216.27 21(75) -> 76* 853.78/216.27 21(70) -> 71* 853.78/216.27 21(40) -> 41* 853.78/216.27 21(197) -> 198* 853.78/216.27 21(157) -> 158* 853.78/216.27 21(112) -> 113* 853.78/216.27 21(229) -> 230* 853.78/216.27 21(194) -> 195* 853.78/216.27 21(184) -> 185* 853.78/216.27 21(179) -> 180* 853.78/216.27 21(94) -> 95* 853.78/216.27 21(84) -> 85* 853.78/216.27 21(44) -> 45* 853.78/216.27 21(206) -> 207* 853.78/216.27 21(181) -> 182* 853.78/216.27 21(126) -> 127* 853.78/216.27 21(86) -> 87* 853.78/216.27 21(118) -> 119* 853.78/216.27 21(43) -> 44* 853.78/216.27 21(240) -> 241* 853.78/216.27 21(210) -> 211* 853.78/216.27 21(195) -> 196* 853.78/216.27 21(140) -> 141* 853.78/216.27 21(125) -> 126* 853.78/216.27 41(85) -> 86* 853.78/216.27 41(65) -> 66* 853.78/216.27 41(50) -> 51* 853.78/216.27 41(242) -> 243* 853.78/216.27 41(30) -> 31* 853.78/216.27 41(207) -> 208* 853.78/216.27 41(162) -> 163* 853.78/216.27 41(127) -> 128* 853.78/216.27 41(122) -> 123* 853.78/216.27 41(52) -> 53* 853.78/216.27 41(42) -> 43* 853.78/216.27 41(239) -> 240* 853.78/216.27 41(32) -> 33* 853.78/216.27 41(174) -> 175* 853.78/216.27 41(164) -> 165* 853.78/216.27 41(159) -> 160* 853.78/216.27 41(139) -> 140* 853.78/216.27 41(99) -> 100* 853.78/216.27 41(74) -> 75* 853.78/216.27 41(186) -> 187* 853.78/216.27 41(156) -> 157* 853.78/216.27 41(56) -> 57* 853.78/216.27 41(41) -> 42* 853.78/216.27 41(36) -> 37* 853.78/216.27 41(208) -> 209* 853.78/216.27 41(178) -> 179* 853.78/216.27 41(173) -> 174* 853.78/216.27 41(158) -> 159* 853.78/216.27 41(128) -> 129* 853.78/216.27 41(73) -> 74* 853.78/216.27 41(235) -> 236* 853.78/216.27 41(205) -> 206* 853.78/216.27 41(180) -> 181* 853.78/216.27 41(160) -> 161* 853.78/216.27 41(130) -> 131* 853.78/216.27 51(55) -> 56* 853.78/216.27 51(222) -> 223* 853.78/216.27 51(182) -> 183* 853.78/216.27 51(172) -> 173* 853.78/216.27 51(102) -> 103* 853.78/216.27 51(92) -> 93* 853.78/216.27 51(209) -> 210* 853.78/216.27 51(204) -> 205* 853.78/216.27 51(199) -> 200* 853.78/216.27 51(134) -> 135* 853.78/216.27 51(236) -> 237* 853.78/216.27 51(171) -> 172* 853.78/216.27 51(161) -> 162* 853.78/216.27 51(151) -> 152* 853.78/216.27 51(131) -> 132* 853.78/216.27 51(238) -> 239* 853.78/216.27 51(233) -> 234* 853.78/216.27 51(228) -> 229* 853.78/216.27 51(183) -> 184* 853.78/216.27 51(168) -> 169* 853.78/216.27 51(138) -> 139* 853.78/216.27 51(108) -> 109* 853.78/216.27 51(93) -> 94* 853.78/216.27 51(230) -> 231* 853.78/216.27 51(225) -> 226* 853.78/216.27 10(7) -> 7* 853.78/216.27 40(7) -> 7* 853.78/216.27 00(7) -> 7* 853.78/216.27 30(7) -> 7* 853.78/216.27 50(7) -> 7* 853.78/216.27 20(7) -> 7* 853.78/216.27 7 -> 193,92,70,50,29 853.78/216.27 30 -> 118,62 853.78/216.27 49 -> 194,7 853.78/216.27 51 -> 151,130 853.78/216.27 57 -> 29* 853.78/216.27 69 -> 29* 853.78/216.27 71 -> 222* 853.78/216.27 87 -> 29* 853.78/216.27 93 -> 170,107 853.78/216.27 106 -> 71* 853.78/216.27 115 -> 195,71 853.78/216.27 129 -> 71* 853.78/216.27 142 -> 131,51 853.78/216.27 152 -> 93* 853.78/216.27 169 -> 119,71 853.78/216.27 171 -> 232* 853.78/216.27 188 -> 71* 853.78/216.27 211 -> 50* 853.78/216.27 231 -> 151* 853.78/216.27 245 -> 141* 853.78/216.27 problem: 853.78/216.27 strict: 853.78/216.27 853.78/216.27 weak: 853.78/216.27 1(1(4(1(0(1(0(3(3(4(4(1(5(4(0(4(4(5(5(3(x1)))))))))))))))))))) -> 853.78/216.27 1(3(0(3(2(2(4(4(2(0(3(3(4(0(3(0(4(3(4(0(x1)))))))))))))))))))) 853.78/216.27 2(2(0(0(2(1(0(5(3(2(2(1(4(0(5(x1))))))))))))))) -> 853.78/216.27 0(0(3(5(3(0(4(3(1(3(0(2(5(5(x1)))))))))))))) 853.78/216.27 2(1(1(3(4(3(1(1(5(x1))))))))) -> 1(0(2(3(1(0(5(1(5(x1))))))))) 853.78/216.27 5(4(0(4(3(3(1(2(5(3(0(x1))))))))))) -> 5(5(2(5(3(1(5(0(3(5(2(x1))))))))))) 853.78/216.27 0(1(2(2(3(0(4(4(x1)))))))) -> 0(4(5(0(3(4(0(4(x1)))))))) 853.78/216.27 0(2(2(2(0(5(2(5(4(x1))))))))) -> 0(0(0(3(4(3(0(1(0(x1))))))))) 853.78/216.27 2(4(5(0(1(1(3(3(5(3(0(0(x1)))))))))))) -> 4(4(2(2(1(0(4(0(1(3(2(0(x1)))))))))))) 853.78/216.27 4(4(3(0(3(1(5(3(5(1(3(1(5(3(x1)))))))))))))) -> 0(2(4(5(0(0(0(5(1(0(5(4(4(x1))))))))))))) 853.78/216.27 5(1(1(4(1(5(3(0(4(3(2(5(4(1(3(3(5(x1))))))))))))))))) -> 853.78/216.27 5(0(1(0(4(0(2(4(5(1(5(4(1(5(3(3(5(x1))))))))))))))))) 853.78/216.27 2(0(3(3(3(4(1(1(0(4(4(0(3(3(3(0(0(1(5(3(x1)))))))))))))))))))) -> 853.78/216.27 5(3(3(1(4(0(4(5(4(4(4(2(4(3(1(1(1(5(4(x1))))))))))))))))))) 853.78/216.27 2(3(3(2(1(5(0(5(0(1(3(3(2(5(1(5(0(3(0(5(x1)))))))))))))))))))) -> 853.78/216.27 3(4(0(2(5(5(2(4(2(4(3(1(1(4(4(5(5(3(5(x1))))))))))))))))))) 853.78/216.27 3(3(2(2(3(3(4(0(0(0(2(5(0(5(3(0(0(1(1(4(x1)))))))))))))))))))) -> 853.78/216.27 3(1(1(0(3(3(5(4(2(2(1(0(1(1(0(5(0(3(4(0(x1)))))))))))))))))))) 853.78/216.27 4(2(4(1(0(5(0(4(1(0(3(0(2(5(4(3(5(3(5(3(x1)))))))))))))))))))) -> 853.78/216.27 4(2(5(4(4(2(4(5(0(0(3(1(5(0(2(0(2(2(1(x1))))))))))))))))))) 853.78/216.27 3(0(0(4(2(5(5(1(3(0(2(3(3(5(1(4(5(x1))))))))))))))))) -> 853.78/216.27 3(4(0(1(0(5(5(3(1(4(0(3(5(3(2(2(5(x1))))))))))))))))) 853.78/216.27 0(1(4(4(3(2(0(4(1(4(3(4(4(1(5(3(4(4(x1)))))))))))))))))) -> 853.78/216.27 0(2(4(2(3(1(0(1(1(1(3(0(2(4(4(1(1(2(x1)))))))))))))))))) 853.78/216.27 Qed 853.78/216.28 EOF