YES(?,O(n^2)) 1164.66/295.94 YES(?,O(n^2)) 1164.66/295.94 1164.66/295.94 Problem: 1164.66/295.94 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.66/295.94 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.66/295.94 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.66/295.94 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.66/295.94 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.66/295.94 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.66/295.94 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.66/295.94 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.66/295.94 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.66/295.94 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.66/295.94 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.66/295.94 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.66/295.94 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.66/295.94 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.66/295.94 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.66/295.94 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.66/295.94 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.66/295.94 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.66/295.94 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.66/295.94 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.66/295.94 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.66/295.94 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.66/295.94 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.66/295.94 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.66/295.94 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.66/295.94 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.66/295.94 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.66/295.94 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.66/295.94 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.66/295.94 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.66/295.94 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.66/295.94 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.66/295.94 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.66/295.94 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.66/295.94 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.66/295.94 1164.66/295.94 Proof: 1164.66/295.94 Complexity Transformation Processor: 1164.66/295.94 strict: 1164.66/295.94 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.66/295.94 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.66/295.94 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.66/295.94 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.66/295.94 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.66/295.94 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.66/295.94 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.66/295.94 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.66/295.94 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.66/295.94 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.66/295.94 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.66/295.94 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.66/295.94 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.66/295.94 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.66/295.94 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.66/295.94 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.66/295.94 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.66/295.94 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.66/295.94 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.66/295.94 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.66/295.94 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.66/295.94 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.66/295.94 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.66/295.94 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.66/295.94 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.66/295.94 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.66/295.94 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.66/295.94 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.66/295.94 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.66/295.94 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.66/295.94 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.66/295.94 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.66/295.94 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.66/295.94 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.66/295.94 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.66/295.94 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.66/295.94 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.66/295.94 weak: 1164.66/295.94 1164.66/295.94 Matrix Interpretation Processor: dim=2 1164.66/295.94 1164.66/295.94 max_matrix: 1164.66/295.94 [1 2] 1164.66/295.94 [0 0] 1164.66/295.94 interpretation: 1164.66/295.94 [1 0] 1164.66/295.94 [5](x0) = [0 0]x0, 1164.66/295.94 1164.66/295.94 [1 0] [0] 1164.66/295.94 [4](x0) = [0 0]x0 + [1], 1164.66/295.94 1164.66/295.94 [1 2] 1164.66/295.94 [3](x0) = [0 0]x0, 1164.66/295.94 1164.66/295.94 [1 0] 1164.66/295.94 [2](x0) = [0 0]x0, 1164.66/295.94 1164.66/295.94 [1 0] [1] 1164.66/295.94 [0](x0) = [0 0]x0 + [0], 1164.66/295.94 1164.66/295.94 [1 0] 1164.66/295.94 [1](x0) = [0 0]x0 1164.66/295.94 orientation: 1164.66/295.94 [1 0] [2] [1 0] [2] 1164.66/295.94 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(1(2(0(x1)))) 1164.66/295.94 1164.66/295.94 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(1(0(x1)))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(4(0(x1)))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(1(3(0(2(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(1(3(0(4(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(2(0(1(2(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(0(1(2(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(0(3(1(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(4(0(4(1(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(0(2(0(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(2(0(0(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(0(2(2(1(2(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(1(2(4(2(0(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [2] [1 0] [2] 1164.66/295.95 0(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(0(3(0(4(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(2(1(1(x1)))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(1(1(x1)))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(1(3(0(4(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(0(2(1(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(3(1(2(4(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(4(2(1(2(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(1(2(4(3(0(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(1(0(4(4(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(2(1(3(0(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(5(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(1(5(x1)))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(5(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(4(5(1(x1)))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(5(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(2(3(1(5(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(5(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(1(5(2(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 0(5(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(3(1(2(5(2(x1)))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 5(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 5(1(2(4(0(x1))))) 1164.66/295.95 1164.66/295.95 [1 0] [1] [1 0] [1] 1164.66/295.95 5(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 5(0(2(1(2(4(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [1] [1 0] [1] 1164.66/295.96 5(0(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 5(1(2(3(0(4(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(0(1(5(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(4(1(0(5(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(0(2(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(3(0(2(1(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(0(2(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(3(0(2(0(1(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(1(0(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(2(0(1(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [1] [1 0] [1] 1164.66/295.96 0(1(1(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(1(3(1(0(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [1] [1 0] [1] 1164.66/295.96 5(0(1(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(5(1(2(0(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [1] [1 0] [1] 1164.66/295.96 5(3(0(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 5(1(2(3(0(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [1 0] 1164.66/295.96 5(3(1(5(x1)))) = [0 0]x1 >= [0 0]x1 = 5(3(1(2(5(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [1 0] 1164.66/295.96 5(3(2(1(x1)))) = [0 0]x1 >= [0 0]x1 = 1(2(3(5(2(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [1] [1 0] [1] 1164.66/295.96 5(4(0(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(5(0(4(x1))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(0(5(1(5(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(2(5(5(0(0(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(5(3(0(1(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(5(3(0(4(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [3] [1 0] [1] 1164.66/295.96 0(5(3(4(1(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(3(5(4(5(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [2] [1 0] [2] 1164.66/295.96 0(5(4(0(1(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0(1(3(0(4(5(x1)))))) 1164.66/295.96 1164.66/295.96 [1 0] [1 0] 1164.66/295.96 5(4(2(1(1(x1))))) = [0 0]x1 >= [0 0]x1 = 5(4(1(2(1(2(x1)))))) 1164.66/295.96 problem: 1164.66/295.96 strict: 1164.66/295.96 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.66/295.96 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.66/295.96 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.66/295.96 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.66/295.96 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.66/295.96 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.66/295.96 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.66/295.96 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.66/295.96 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.66/295.96 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.66/295.96 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.66/295.96 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.66/295.96 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.66/295.96 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.66/295.96 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.66/295.96 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.66/295.96 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.66/295.96 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.66/295.96 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.66/295.96 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.66/295.96 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.66/295.96 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.66/295.96 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.66/295.96 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.66/295.96 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.66/295.96 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.66/295.96 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.66/295.96 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.66/295.96 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.66/295.96 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.66/295.96 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.66/295.96 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.66/295.96 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.66/295.96 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.66/295.96 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.66/295.96 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.66/295.96 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.66/295.96 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.66/295.96 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.66/295.96 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.66/295.96 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.66/295.96 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.66/295.96 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.66/295.97 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.66/295.97 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.66/295.97 weak: 1164.66/295.97 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.66/295.97 Matrix Interpretation Processor: dim=2 1164.66/295.97 1164.66/295.97 max_matrix: 1164.66/295.97 [1 2] 1164.66/295.97 [0 0] 1164.66/295.97 interpretation: 1164.66/295.97 [1 2] 1164.66/295.97 [5](x0) = [0 0]x0, 1164.66/295.97 1164.66/295.97 [1 0] [0] 1164.66/295.97 [4](x0) = [0 0]x0 + [1], 1164.66/295.97 1164.66/295.97 [1 2] 1164.66/295.97 [3](x0) = [0 0]x0, 1164.66/295.97 1164.66/295.97 [1 0] 1164.66/295.97 [2](x0) = [0 0]x0, 1164.66/295.97 1164.66/295.97 [1 0] 1164.66/295.97 [0](x0) = [0 0]x0, 1164.66/295.97 1164.66/295.97 [1 2] 1164.66/295.97 [1](x0) = [0 0]x0 1164.66/295.97 orientation: 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(1(2(0(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(1(0(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(4(0(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(1(3(0(2(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(1(3(0(4(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(2(0(1(2(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(0(1(2(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(0(3(1(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(4(0(4(1(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(2(0(2(0(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(2(2(0(0(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(0(2(2(1(2(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(1(2(4(2(0(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(2(0(3(0(4(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(2(1(1(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(1(1(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(1(3(0(4(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(2(0(2(1(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(3(1(2(4(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(4(2(1(2(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(1(2(4(3(0(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(2(1(0(4(4(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(2(2(1(3(0(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(5(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(1(5(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(5(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(4(5(1(x1)))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(5(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(2(3(1(5(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(5(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(1(5(2(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(5(1(x1))) = [0 0]x1 >= [0 0]x1 = 0(3(1(2(5(2(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 5(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 5(1(2(4(0(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 5(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 5(0(2(1(2(4(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 5(0(1(x1))) = [0 0]x1 >= [0 0]x1 = 5(1(2(3(0(4(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(0(1(5(x1)))) = [0 0]x1 >= [0 0]x1 = 0(4(1(0(5(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(0(2(1(x1)))) = [0 0]x1 >= [0 0]x1 = 2(0(3(0(2(1(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(0(2(1(x1)))) = [0 0]x1 >= [0 0]x1 = 2(3(0(2(0(1(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 0(1(0(1(x1)))) = [0 0]x1 >= [0 0]x1 = 1(0(2(0(1(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(1(1(1(x1)))) = [0 0]x1 >= [0 0]x1 = 1(1(3(1(0(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 5(0(1(1(x1)))) = [0 0]x1 >= [0 0]x1 = 1(5(1(2(0(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 5(3(0(1(x1)))) = [0 0]x1 >= [0 0]x1 = 5(1(2(3(0(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 2] 1164.66/295.97 5(3(1(5(x1)))) = [0 0]x1 >= [0 0]x1 = 5(3(1(2(5(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 5(3(2(1(x1)))) = [0 0]x1 >= [0 0]x1 = 1(2(3(5(2(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [2] [1 0] 1164.66/295.97 5(4(0(1(x1)))) = [0 0]x1 + [0] >= [0 0]x1 = 1(2(5(0(4(x1))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(0(5(1(5(x1))))) = [0 0]x1 >= [0 0]x1 = 1(2(5(5(0(0(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [1 0] 1164.66/295.97 0(5(3(0(1(x1))))) = [0 0]x1 >= [0 0]x1 = 1(0(5(3(0(4(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [2] [1 2] 1164.66/295.97 0(5(4(0(1(x1))))) = [0 0]x1 + [0] >= [0 0]x1 = 0(1(3(0(4(5(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [2] [1 0] [2] 1164.66/295.97 5(4(2(1(1(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 5(4(1(2(1(2(x1)))))) 1164.66/295.97 1164.66/295.97 [1 2] [2] [1 2] [2] 1164.66/295.97 0(5(3(4(1(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(3(5(4(5(x1)))))) 1164.66/295.97 problem: 1164.66/295.97 strict: 1164.66/295.97 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.66/295.97 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.66/295.97 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.66/295.97 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.66/295.97 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.66/295.97 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.66/295.97 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.66/295.97 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.66/295.97 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.66/295.97 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.66/295.97 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.66/295.97 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.66/295.97 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.66/295.97 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.66/295.97 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.66/295.97 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.66/295.97 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.66/295.97 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.66/295.97 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.66/295.97 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.66/295.97 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.66/295.97 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.66/295.97 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.66/295.97 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.66/295.97 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.66/295.97 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.66/295.97 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.66/295.97 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.66/295.97 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.66/295.97 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.66/295.97 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.66/295.97 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.66/295.97 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.66/295.97 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.66/295.97 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.66/295.97 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.66/295.97 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.66/295.97 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.66/295.97 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.66/295.97 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.66/295.97 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.66/295.97 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.66/295.98 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.66/295.98 weak: 1164.66/295.98 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.66/295.98 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.66/295.98 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.66/295.98 Splitting Processor: 1164.66/295.98 strict: 1164.66/295.98 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.66/295.98 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.66/295.98 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.66/295.98 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.66/295.98 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.66/295.98 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.66/295.98 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.66/295.98 weak: 1164.66/295.98 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.66/295.98 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.66/295.98 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.66/295.98 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.66/295.98 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.66/295.98 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.66/295.98 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.66/295.98 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.66/295.98 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.66/295.98 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.66/295.98 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.66/295.98 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.66/295.98 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.66/295.98 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.66/295.98 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.66/295.98 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.66/295.98 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.66/295.98 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.66/295.98 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.66/295.98 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.66/295.98 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.66/295.98 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.66/295.98 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.66/295.98 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.66/295.98 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.66/295.98 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.66/295.98 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.66/295.98 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.66/295.98 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.66/295.98 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.66/295.98 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.66/295.98 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.66/295.98 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.66/295.98 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.66/295.98 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.66/295.98 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.66/295.98 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.66/295.98 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.66/295.98 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.66/295.98 Matrix Interpretation Processor: dim=2 1164.66/295.98 1164.66/295.98 max_matrix: 1164.66/295.98 [1 1] 1164.66/295.98 [0 0] 1164.66/295.98 interpretation: 1164.66/295.98 [1 1] [0] 1164.66/295.98 [5](x0) = [0 0]x0 + [1], 1164.66/295.98 1164.66/295.98 [1 1] 1164.66/295.98 [4](x0) = [0 0]x0, 1164.66/295.98 1164.66/295.98 [1 0] 1164.66/295.98 [3](x0) = [0 0]x0, 1164.66/295.98 1164.66/295.98 [1 1] 1164.66/295.98 [2](x0) = [0 0]x0, 1164.66/295.98 1164.66/295.98 [1 1] [0] 1164.66/295.98 [0](x0) = [0 0]x0 + [1], 1164.66/295.98 1164.66/295.98 [1 1] [0] 1164.66/295.98 [1](x0) = [0 0]x0 + [1] 1164.66/295.98 orientation: 1164.66/295.98 [1 1] [2] [1 1] [1] 1164.66/295.98 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(0(x1)))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [1] 1164.66/295.98 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(0(2(x1))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [1] 1164.66/295.98 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(0(4(x1))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [1] 1164.66/295.98 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(0(1(2(x1))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [0] 1164.66/295.98 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(0(3(1(x1))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [1] 1164.66/295.98 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(3(0(4(x1)))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [2] 1164.66/295.98 0(0(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(3(0(2(1(x1)))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [2] 1164.66/295.98 5(4(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(5(0(4(x1))))) 1164.66/295.98 1164.66/295.98 [1 1] [3] [1 1] [2] 1164.66/295.98 0(5(4(0(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(0(4(5(x1)))))) 1164.66/295.98 1164.66/295.98 [1 1] [2] [1 1] [2] 1164.66/295.99 0(5(3(4(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(3(5(4(5(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(0(x1)))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(4(0(x1)))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(0(1(2(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(0(4(1(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(0(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(0(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(2(1(2(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(4(2(0(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(1(x1)))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(1(x1)))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(3(0(4(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(1(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(3(1(2(4(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(4(2(1(2(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(2(4(3(0(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(4(4(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(1(3(0(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(5(x1)))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(5(1(x1)))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(1(5(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(5(2(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(2(5(2(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 5(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(1(2(4(0(x1))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [2] 1164.66/295.99 5(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(0(2(1(2(4(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [2] [1 1] [1] 1164.66/295.99 5(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(1(2(3(0(4(x1)))))) 1164.66/295.99 1164.66/295.99 [1 1] [3] [1 1] [3] 1164.66/295.99 0(0(1(5(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(1(0(5(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [2] [1 1] [2] 1164.75/296.00 0(0(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(3(0(2(0(1(x1)))))) 1164.75/296.00 1164.75/296.00 [1 1] [3] [1 1] [3] 1164.75/296.00 0(1(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(1(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [3] [1 1] [2] 1164.75/296.00 0(1(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(3(1(0(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [3] [1 1] [3] 1164.75/296.00 5(0(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(5(1(2(0(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [1] [1 1] [1] 1164.75/296.00 5(3(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(1(2(3(0(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [1] [1 1] [1] 1164.75/296.00 5(3(1(5(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(3(1(2(5(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [1] [1 1] [0] 1164.75/296.00 5(3(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(3(5(2(x1))))) 1164.75/296.00 1164.75/296.00 [1 1] [4] [1 1] [4] 1164.75/296.00 0(0(5(1(5(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(5(5(0(0(x1)))))) 1164.75/296.00 1164.75/296.00 [1 1] [2] [1 1] [2] 1164.75/296.00 0(5(3(0(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(5(3(0(4(x1)))))) 1164.75/296.00 1164.75/296.00 [1 1] [2] [1 1] [2] 1164.75/296.00 5(4(2(1(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(4(1(2(1(2(x1)))))) 1164.75/296.00 problem: 1164.75/296.00 strict: 1164.75/296.00 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.75/296.00 weak: 1164.75/296.00 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.75/296.00 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.75/296.00 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.75/296.00 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.75/296.00 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.75/296.00 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.75/296.00 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.75/296.00 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.75/296.00 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.75/296.00 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.75/296.00 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.75/296.00 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.75/296.00 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.75/296.00 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.75/296.00 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.75/296.00 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.75/296.00 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.75/296.00 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.75/296.00 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.75/296.00 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.75/296.00 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.75/296.00 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.75/296.00 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.75/296.00 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.75/296.00 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.75/296.00 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.75/296.00 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.75/296.00 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.75/296.00 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.75/296.00 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.75/296.00 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.75/296.00 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.75/296.00 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.75/296.00 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.75/296.00 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.75/296.00 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.75/296.00 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.75/296.00 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.75/296.00 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.75/296.00 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.75/296.00 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.75/296.00 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.75/296.00 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.75/296.00 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.75/296.00 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.75/296.00 Matrix Interpretation Processor: dim=2 1164.75/296.00 1164.75/296.00 max_matrix: 1164.75/296.00 [1 2] 1164.75/296.00 [0 0] 1164.75/296.00 interpretation: 1164.75/296.00 [1 2] [0] 1164.75/296.00 [5](x0) = [0 0]x0 + [1], 1164.75/296.00 1164.75/296.00 [1 1] 1164.75/296.00 [4](x0) = [0 0]x0, 1164.75/296.00 1164.75/296.00 [1 0] 1164.75/296.00 [3](x0) = [0 0]x0, 1164.75/296.00 1164.75/296.00 [1 0] 1164.75/296.00 [2](x0) = [0 0]x0, 1164.75/296.00 1164.75/296.00 [1 2] [0] 1164.75/296.00 [0](x0) = [0 0]x0 + [1], 1164.75/296.00 1164.75/296.00 [1 2] [0] 1164.75/296.00 [1](x0) = [0 0]x0 + [1] 1164.75/296.00 orientation: 1164.75/296.00 [1 2] [2] [1 2] 1164.75/296.00 0(0(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = 2(0(3(0(2(1(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(0(x1)))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 0] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(0(2(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 1] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(0(4(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 0] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(0(1(2(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [0] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(0(3(1(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 1] [0] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(3(0(4(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [3] [1 1] [2] 1164.75/296.00 5(4(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(5(0(4(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [5] [1 2] [3] 1164.75/296.00 0(5(4(0(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(0(4(5(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [3] [1 2] [3] 1164.75/296.00 0(5(3(4(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(3(5(4(5(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(0(x1)))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [3] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(4(0(x1)))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 0] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(0(1(2(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(0(4(1(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [0] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(0(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(0(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 0] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(2(1(2(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(4(2(0(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(1(x1)))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(1(x1)))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 1] [2] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(3(0(4(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [0] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(1(x1))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 1] [2] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(3(1(2(4(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 0] [2] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(4(2(1(2(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 2] [2] 1164.75/296.00 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(2(4(3(0(x1)))))) 1164.75/296.00 1164.75/296.00 [1 2] [4] [1 1] [2] 1164.75/296.01 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(4(4(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 2] [0] 1164.75/296.01 0(1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(1(3(0(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 2] [2] 1164.75/296.01 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(5(x1)))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 2] [3] 1164.75/296.01 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(5(1(x1)))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 2] [2] 1164.75/296.01 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(1(5(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 0] [2] 1164.75/296.01 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(5(2(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 0] [0] 1164.75/296.01 0(5(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(3(1(2(5(2(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 2] [3] 1164.75/296.01 5(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(1(2(4(0(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 1] [2] 1164.75/296.01 5(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(0(2(1(2(4(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 1] [2] 1164.75/296.01 5(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(1(2(3(0(4(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [6] [1 2] [5] 1164.75/296.01 0(0(1(5(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(4(1(0(5(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [2] [1 2] [2] 1164.75/296.01 0(0(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(3(0(2(0(1(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [6] [1 2] [4] 1164.75/296.01 0(1(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(1(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [6] [1 2] [4] 1164.75/296.01 0(1(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(3(1(0(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [6] [1 2] [4] 1164.75/296.01 5(0(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(5(1(2(0(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [2] [1 2] [2] 1164.75/296.01 5(3(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(1(2(3(0(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [2] [1 2] [0] 1164.75/296.01 5(3(1(5(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(3(1(2(5(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [0] [1 0] [0] 1164.75/296.01 5(3(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(3(5(2(x1))))) 1164.75/296.01 1164.75/296.01 [1 2] [8] [1 2] [6] 1164.75/296.01 0(0(5(1(5(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(5(5(0(0(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [4] [1 1] [4] 1164.75/296.01 0(5(3(0(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(5(3(0(4(x1)))))) 1164.75/296.01 1164.75/296.01 [1 2] [2] [1 0] [1] 1164.75/296.01 5(4(2(1(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 5(4(1(2(1(2(x1)))))) 1164.75/296.01 problem: 1164.75/296.01 strict: 1164.75/296.01 1164.75/296.01 weak: 1164.75/296.01 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.75/296.01 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.75/296.01 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.75/296.01 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.75/296.01 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.75/296.01 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.75/296.01 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.75/296.01 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.75/296.01 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.75/296.01 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.75/296.01 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.75/296.01 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.75/296.01 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.75/296.01 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.75/296.01 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.75/296.01 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.75/296.01 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.75/296.02 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.75/296.02 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.75/296.02 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.75/296.02 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.75/296.02 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.75/296.02 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.75/296.02 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.75/296.02 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.75/296.02 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.75/296.02 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.75/296.02 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.75/296.02 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.75/296.02 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.75/296.02 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.75/296.02 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.75/296.02 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.75/296.02 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.75/296.02 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.75/296.02 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.75/296.02 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.75/296.02 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.75/296.02 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.75/296.02 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.75/296.02 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.75/296.02 Qed 1164.75/296.02 1164.75/296.02 strict: 1164.75/296.02 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.75/296.02 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.75/296.02 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.75/296.02 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.75/296.02 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.75/296.02 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.75/296.02 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.75/296.02 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.75/296.02 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.75/296.02 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.75/296.02 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.75/296.02 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.75/296.02 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.75/296.02 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.75/296.02 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.75/296.02 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.75/296.02 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.75/296.02 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.75/296.02 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.75/296.02 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.75/296.02 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.75/296.02 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.75/296.02 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.75/296.02 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.75/296.02 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.75/296.02 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.75/296.02 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.75/296.02 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.75/296.02 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.75/296.02 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.75/296.02 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.75/296.02 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.75/296.02 weak: 1164.75/296.02 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.75/296.02 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.75/296.02 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.75/296.02 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.75/296.02 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.75/296.02 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.75/296.02 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.75/296.02 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.75/296.02 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.75/296.02 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.75/296.02 Matrix Interpretation Processor: dim=2 1164.75/296.02 1164.75/296.02 max_matrix: 1164.75/296.02 [1 1] 1164.75/296.02 [0 1] 1164.75/296.02 interpretation: 1164.75/296.02 1164.75/296.02 [5](x0) = x0, 1164.75/296.02 1164.75/296.02 1164.75/296.02 [4](x0) = x0, 1164.75/296.02 1164.75/296.02 1164.75/296.02 [3](x0) = x0, 1164.75/296.02 1164.75/296.02 1164.75/296.02 [2](x0) = x0, 1164.75/296.02 1164.75/296.02 [1 1] 1164.75/296.02 [0](x0) = [0 1]x0, 1164.75/296.02 1164.75/296.02 [0] 1164.75/296.02 [1](x0) = x0 + [1] 1164.75/296.02 orientation: 1164.75/296.02 [1 2] [2] [1 2] [1] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(1(2(0(x1)))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [0] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(0(4(0(x1)))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [2] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(2(0(1(2(x1))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [2] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(4(0(4(1(x1))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [0] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(2(0(2(0(x1))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [0] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(2(2(0(0(x1))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [2] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(0(2(2(1(2(x1)))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [1] 1164.75/296.02 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(1(2(4(2(0(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [2] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 0(2(1(1(x1)))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [2] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 0(3(1(1(x1)))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [0] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(1(3(0(4(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [1] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(2(0(2(1(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [1] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(0(3(1(2(4(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [1] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(0(4(2(1(2(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [0] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(1(2(4(3(0(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [0] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(2(1(0(4(4(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [0] 1164.75/296.02 0(1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(2(2(1(3(0(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [1] 1164.75/296.02 0(5(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(3(1(5(x1)))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [1] 1164.75/296.02 0(5(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(4(5(1(x1)))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [1] 1164.75/296.02 0(5(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(2(3(1(5(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [1] 1164.75/296.02 0(5(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(3(1(5(2(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [1] 1164.75/296.02 0(5(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(3(1(2(5(2(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [0] 1164.75/296.02 5(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 5(1(2(4(0(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [1] 1164.75/296.02 5(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 5(0(2(1(2(4(x1)))))) 1164.75/296.02 1164.75/296.02 [1 1] [1] [1 1] [0] 1164.75/296.02 5(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 5(1(2(3(0(4(x1)))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [1] 1164.75/296.02 0(0(1(5(x1)))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(4(1(0(5(x1))))) 1164.75/296.02 1164.75/296.02 [1 2] [2] [1 2] [2] 1164.75/296.02 0(0(2(1(x1)))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 2(3(0(2(0(1(x1)))))) 1164.75/296.02 1164.75/296.02 [1 2] [3] [1 2] [2] 1164.75/296.02 0(1(0(1(x1)))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(0(2(0(1(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [3] [1 1] [0] 1164.75/296.02 0(1(1(1(x1)))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = 1(1(3(1(0(x1))))) 1164.75/296.02 1164.75/296.02 [1 1] [2] [1 1] [0] 1164.75/296.03 5(0(1(1(x1)))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1(5(1(2(0(x1))))) 1164.75/296.03 1164.75/296.03 [1 1] [1] [1 1] [0] 1164.75/296.03 5(3(0(1(x1)))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 5(1(2(3(0(x1))))) 1164.75/296.03 1164.75/296.03 [0] [0] 1164.75/296.03 5(3(1(5(x1)))) = x1 + [1] >= x1 + [1] = 5(3(1(2(5(x1))))) 1164.75/296.03 1164.75/296.03 [0] [0] 1164.75/296.03 5(3(2(1(x1)))) = x1 + [1] >= x1 + [1] = 1(2(3(5(2(x1))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [0] 1164.75/296.03 0(0(5(1(5(x1))))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(2(5(5(0(0(x1)))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [0] 1164.75/296.03 0(5(3(0(1(x1))))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(0(5(3(0(4(x1)))))) 1164.75/296.03 1164.75/296.03 [0] [0] 1164.75/296.03 5(4(2(1(1(x1))))) = x1 + [2] >= x1 + [2] = 5(4(1(2(1(2(x1)))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [1] 1164.75/296.03 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(3(1(0(x1)))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [1] 1164.75/296.03 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(1(3(0(2(x1))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [1] 1164.75/296.03 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(1(3(0(4(x1))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [2] 1164.75/296.03 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(3(0(1(2(x1))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [2] 1164.75/296.03 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(3(0(3(1(x1))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [0] 1164.75/296.03 0(0(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(2(0(3(0(4(x1)))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [2] 1164.75/296.03 0(0(2(1(x1)))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 2(0(3(0(2(1(x1)))))) 1164.75/296.03 1164.75/296.03 [1 1] [1] [1 1] [0] 1164.75/296.03 5(4(0(1(x1)))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(2(5(0(4(x1))))) 1164.75/296.03 1164.75/296.03 [1 2] [2] [1 2] [1] 1164.75/296.03 0(5(4(0(1(x1))))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(1(3(0(4(5(x1)))))) 1164.75/296.03 1164.75/296.03 [1 1] [1] [1 1] [0] 1164.75/296.03 0(5(3(4(1(x1))))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(0(3(5(4(5(x1)))))) 1164.75/296.03 problem: 1164.75/296.03 strict: 1164.75/296.03 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.75/296.03 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.75/296.03 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.75/296.03 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.75/296.03 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.75/296.03 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.75/296.03 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.75/296.03 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.75/296.03 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.75/296.03 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.75/296.03 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.75/296.03 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.75/296.03 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.75/296.03 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.75/296.03 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.75/296.03 weak: 1164.75/296.03 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.75/296.03 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.75/296.03 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.75/296.03 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.75/296.03 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.75/296.03 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.75/296.03 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.75/296.03 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.75/296.03 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.75/296.03 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.75/296.03 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.75/296.03 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.75/296.03 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.75/296.03 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.75/296.03 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.75/296.03 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.75/296.03 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.75/296.03 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.75/296.03 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.75/296.03 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.75/296.04 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.75/296.04 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.75/296.04 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.75/296.04 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.75/296.04 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.75/296.04 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.75/296.04 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.75/296.04 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.75/296.04 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.75/296.04 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.75/296.04 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.75/296.04 Matrix Interpretation Processor: dim=3 1164.75/296.04 1164.75/296.04 max_matrix: 1164.75/296.04 [1 1 0] 1164.75/296.04 [0 1 1] 1164.75/296.04 [0 0 0] 1164.75/296.04 interpretation: 1164.75/296.04 [1 0 0] 1164.75/296.04 [5](x0) = [0 1 1]x0 1164.75/296.04 [0 0 0] , 1164.75/296.04 1164.75/296.04 [1 0 0] [0] 1164.75/296.04 [4](x0) = [0 0 0]x0 + [0] 1164.75/296.04 [0 0 0] [1], 1164.75/296.04 1164.75/296.04 [1 0 0] 1164.75/296.04 [3](x0) = [0 0 0]x0 1164.75/296.04 [0 0 0] , 1164.75/296.04 1164.75/296.04 [1 0 0] 1164.75/296.04 [2](x0) = [0 1 0]x0 1164.75/296.04 [0 0 0] , 1164.75/296.04 1164.75/296.04 [1 1 0] [0] 1164.75/296.04 [0](x0) = [0 1 0]x0 + [1] 1164.75/296.04 [0 0 0] [0], 1164.75/296.04 1164.75/296.04 [1 0 0] 1164.75/296.04 [1](x0) = [0 1 0]x0 1164.75/296.04 [0 0 0] 1164.75/296.04 orientation: 1164.75/296.04 [1 2 0] [1] [1 2 0] [1] 1164.75/296.04 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(2(0(1(2(x1))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 2 0] [1] [1 0 0] [0] 1164.75/296.04 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(4(0(4(1(x1))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 2 0] [1] [1 2 0] [1] 1164.75/296.04 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(0(2(2(1(2(x1)))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 1 0] [0] 1164.75/296.04 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 0(2(1(1(x1)))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(1(x1)))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 0(5(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(5(x1)))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 0(5(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(4(5(1(x1)))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 0(5(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(2(3(1(5(x1))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 0(5(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(5(2(x1))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 0(5(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(2(5(2(x1)))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 1 0] [0] [1 0 0] [0] 1164.75/296.04 5(0(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(0(2(1(2(4(x1)))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.04 1164.75/296.04 [1 2 0] [1] [1 2 0] [1] 1164.75/296.04 0(0(2(1(x1)))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [0] = 2(3(0(2(0(1(x1)))))) 1164.75/296.04 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 0 0] [1 0 0] 1164.75/296.05 5(3(1(5(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 5(3(1(2(5(x1))))) 1164.75/296.05 [0 0 0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 0 0] [1 0 0] 1164.75/296.05 5(3(2(1(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 1(2(3(5(2(x1))))) 1164.75/296.05 [0 0 0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 0 0] [0] [1 0 0] [0] 1164.75/296.05 5(4(2(1(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(4(1(2(1(2(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 2 0] [1] [1 2 0] [1] 1164.75/296.05 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(1(2(0(x1)))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 2 0] [1] [1 1 0] [0] 1164.75/296.05 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 1(0(4(0(x1)))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 2 0] [1] [1 2 0] [1] 1164.75/296.05 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(0(2(0(x1))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 2 0] [1] [1 2 0] [1] 1164.75/296.05 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(2(0(0(x1))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 2 0] [1] [1 1 0] [0] 1164.75/296.05 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(1(2(4(2(0(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 0 0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 1(1(3(0(4(x1))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 1 0] [0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 1(2(0(2(1(x1))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 0 0] [0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(3(1(2(4(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 0 0] [0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(4(2(1(2(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 1 0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 1(1(2(4(3(0(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 0 0] [0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(1(0(4(4(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] [0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 1 0] 1164.75/296.05 0(1(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 1(2(2(1(3(0(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 1 0] 1164.75/296.05 5(0(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 5(1(2(4(0(x1))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 1 0] [0] [1 0 0] 1164.75/296.05 5(0(1(x1))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 5(1(2(3(0(4(x1)))))) 1164.75/296.05 [0 0 0] [0] [0 0 0] 1164.75/296.05 1164.75/296.05 [1 2 2] [1] [1 1 1] [0] 1164.75/296.06 0(0(1(5(x1)))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 0(4(1(0(5(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 2 0] [1] 1164.75/296.06 0(1(0(1(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(0(2(0(1(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 1 0] [0] [1 1 0] 1164.75/296.06 0(1(1(1(x1)))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 1(1(3(1(0(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] 1164.75/296.06 1164.75/296.06 [1 1 0] [0] [1 1 0] [0] 1164.75/296.06 5(0(1(1(x1)))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 1(5(1(2(0(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 1 0] [1 1 0] 1164.75/296.06 5(3(0(1(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 5(1(2(3(0(x1))))) 1164.75/296.06 [0 0 0] [0 0 0] 1164.75/296.06 1164.75/296.06 [1 2 2] [1] [1 2 0] [1] 1164.75/296.06 0(0(5(1(5(x1))))) = [0 1 1]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(5(5(0(0(x1)))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 1 0] [0] [1 0 0] [0] 1164.75/296.06 0(5(3(0(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(5(3(0(4(x1)))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 1 0] [0] 1164.75/296.06 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(3(1(0(x1)))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 1 0] [0] 1164.75/296.06 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(1(3(0(2(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 0 0] [0] 1164.75/296.06 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(1(3(0(4(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 1 0] [0] 1164.75/296.06 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(3(0(1(2(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 0 0] [0] 1164.75/296.06 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(3(0(3(1(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 0 0] [0] 1164.75/296.06 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 1(2(0(3(0(4(x1)))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 2 0] [1] [1 1 0] [0] 1164.75/296.06 0(0(2(1(x1)))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [1] = 2(0(3(0(2(1(x1)))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 1 0] [0] [1 0 0] [0] 1164.75/296.06 5(4(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(5(0(4(x1))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 1 0] [1] [1 0 0] [0] 1164.75/296.06 0(5(4(0(1(x1))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(1(3(0(4(5(x1)))))) 1164.75/296.06 [0 0 0] [0] [0 0 0] [0] 1164.75/296.06 1164.75/296.06 [1 0 0] [0] [1 0 0] [0] 1164.75/296.06 0(5(3(4(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(3(5(4(5(x1)))))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 problem: 1164.75/296.07 strict: 1164.75/296.07 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.75/296.07 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.75/296.07 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.75/296.07 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.75/296.07 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.75/296.07 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.75/296.07 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.75/296.07 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.75/296.07 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.75/296.07 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.75/296.07 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.75/296.07 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.75/296.07 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.75/296.07 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.75/296.07 weak: 1164.75/296.07 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.75/296.07 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.75/296.07 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.75/296.07 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.75/296.07 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.75/296.07 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.75/296.07 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.75/296.07 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.75/296.07 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.75/296.07 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.75/296.07 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.75/296.07 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.75/296.07 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.75/296.07 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.75/296.07 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.75/296.07 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.75/296.07 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.75/296.07 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.75/296.07 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.75/296.07 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.75/296.07 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.75/296.07 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.75/296.07 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.75/296.07 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.75/296.07 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.75/296.07 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.75/296.07 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.75/296.07 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.75/296.07 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.75/296.07 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.75/296.07 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.75/296.07 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.75/296.07 Matrix Interpretation Processor: dim=3 1164.75/296.07 1164.75/296.07 max_matrix: 1164.75/296.07 [1 1 0] 1164.75/296.07 [0 1 1] 1164.75/296.07 [0 0 0] 1164.75/296.07 interpretation: 1164.75/296.07 [1 1 0] [0] 1164.75/296.07 [5](x0) = [0 1 0]x0 + [1] 1164.75/296.07 [0 0 0] [0], 1164.75/296.07 1164.75/296.07 [1 0 0] [0] 1164.75/296.07 [4](x0) = [0 0 0]x0 + [0] 1164.75/296.07 [0 0 0] [1], 1164.75/296.07 1164.75/296.07 [1 0 0] 1164.75/296.07 [3](x0) = [0 1 1]x0 1164.75/296.07 [0 0 0] , 1164.75/296.07 1164.75/296.07 [1 0 0] 1164.75/296.07 [2](x0) = [0 0 0]x0 1164.75/296.07 [0 0 0] , 1164.75/296.07 1164.75/296.07 [1 0 0] 1164.75/296.07 [0](x0) = [0 1 0]x0 1164.75/296.07 [0 0 0] , 1164.75/296.07 1164.75/296.07 [1 1 0] [0] 1164.75/296.07 [1](x0) = [0 1 1]x0 + [1] 1164.75/296.07 [0 0 0] [0] 1164.75/296.07 orientation: 1164.75/296.07 [1 1 0] [0] [1 0 0] 1164.75/296.07 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 = 0(2(0(1(2(x1))))) 1164.75/296.07 [0 0 0] [0] [0 0 0] 1164.75/296.07 1164.75/296.07 [1 1 0] [0] [1 0 0] 1164.75/296.07 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(2(1(2(x1)))))) 1164.75/296.07 [0 0 0] [0] [0 0 0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 2 1] [1] 1164.75/296.07 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [0] = 0(2(1(1(x1)))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 2 1] [1] 1164.75/296.07 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [2] = 0(3(1(1(x1)))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 2 0] [1] 1164.75/296.07 0(5(1(x1))) = [0 1 1]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(1(5(x1)))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 2 1] [1] 1164.75/296.07 0(5(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [0] = 0(4(5(1(x1)))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 2 0] [1] 1164.75/296.07 0(5(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [0] = 0(2(3(1(5(x1))))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 0 0] [1] 1164.75/296.07 0(5(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 0(3(1(5(2(x1))))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 0 0] [0] 1164.75/296.07 0(5(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 0(3(1(2(5(2(x1)))))) 1164.75/296.07 [0 0 0] [0] [0 0 0] [0] 1164.75/296.07 1164.75/296.07 [1 2 1] [1] [1 0 0] [0] 1164.75/296.08 5(0(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 5(0(2(1(2(4(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [1 1 0] 1164.75/296.08 0(0(2(1(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 2(3(0(2(0(1(x1)))))) 1164.75/296.08 [0 0 0] [0 0 0] 1164.75/296.08 1164.75/296.08 [1 3 0] [3] [1 1 0] [1] 1164.75/296.08 5(3(1(5(x1)))) = [0 1 0]x1 + [3] >= [0 0 0]x1 + [2] = 5(3(1(2(5(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 5(3(2(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(3(5(2(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [0] 1164.75/296.08 5(4(2(1(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(4(1(2(1(2(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 1 0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 = 0(4(0(4(1(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(0(x1)))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(4(0(x1)))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(0(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(0(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(4(2(0(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 1(1(3(0(4(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 1 0] [0] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(2(0(2(1(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 1(0(3(1(2(4(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [0] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(0(4(2(1(2(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 1(1(2(4(3(0(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [0] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(2(1(0(4(4(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 1 0] [0] 1164.75/296.08 0(1(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(2(2(1(3(0(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 5(0(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 5(1(2(4(0(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 5(0(1(x1))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 5(1(2(3(0(4(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 0] [1] [1 2 0] [1] 1164.75/296.08 0(0(1(5(x1)))) = [0 1 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(4(1(0(5(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 1 0] [0] 1164.75/296.08 0(1(0(1(x1)))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(0(2(0(1(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 3 2] [3] [1 3 0] [3] 1164.75/296.08 0(1(1(1(x1)))) = [0 1 1]x1 + [3] >= [0 1 0]x1 + [3] = 1(1(3(1(0(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 3 2] [3] [1 0 0] [3] 1164.75/296.08 5(0(1(1(x1)))) = [0 1 1]x1 + [3] >= [0 0 0]x1 + [3] = 1(5(1(2(0(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 5(3(0(1(x1)))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 5(1(2(3(0(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 3 0] [3] [1 2 0] [1] 1164.75/296.08 0(0(5(1(5(x1))))) = [0 1 0]x1 + [3] >= [0 0 0]x1 + [1] = 1(2(5(5(0(0(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 2 1] [1] [1 0 0] [1] 1164.75/296.08 0(5(3(0(1(x1))))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 1(0(5(3(0(4(x1)))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 1 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 1 0]x1 + [1] = 0(3(1(0(x1)))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.08 1164.75/296.08 [1 1 0] [0] [1 0 0] [0] 1164.75/296.08 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(3(0(2(x1))))) 1164.75/296.08 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [0] [1 0 0] [0] 1164.75/296.09 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(3(0(4(x1))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [0] [1 0 0] [0] 1164.75/296.09 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(0(1(2(x1))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [0] [1 1 0] [0] 1164.75/296.09 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = 0(3(0(3(1(x1))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [0] [1 0 0] [0] 1164.75/296.09 0(0(1(x1))) = [0 1 1]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(3(0(4(x1)))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [1 1 0] 1164.75/296.09 0(0(2(1(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 2(0(3(0(2(1(x1)))))) 1164.75/296.09 [0 0 0] [0 0 0] 1164.75/296.09 1164.75/296.09 [1 1 0] [0] [1 0 0] [0] 1164.75/296.09 5(4(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(5(0(4(x1))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [0] [1 1 0] [0] 1164.75/296.09 0(5(4(0(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(3(0(4(5(x1)))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 1164.75/296.09 [1 1 0] [1] [1 1 0] [1] 1164.75/296.09 0(5(3(4(1(x1))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 1(0(3(5(4(5(x1)))))) 1164.75/296.09 [0 0 0] [0] [0 0 0] [0] 1164.75/296.09 problem: 1164.75/296.09 strict: 1164.75/296.09 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.75/296.09 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.75/296.09 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.75/296.09 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.75/296.09 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.75/296.09 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.75/296.09 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.75/296.09 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.75/296.09 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.75/296.09 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.75/296.09 weak: 1164.75/296.09 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.75/296.09 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.75/296.09 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.75/296.09 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.75/296.09 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.75/296.09 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.75/296.09 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.75/296.09 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.75/296.09 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.75/296.09 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.75/296.09 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.75/296.09 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.75/296.09 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.75/296.09 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.75/296.09 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.75/296.09 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.75/296.09 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.75/296.09 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.75/296.09 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.75/296.09 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.75/296.09 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.75/296.09 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.75/296.09 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.75/296.09 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.75/296.09 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.75/296.09 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.75/296.09 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.75/296.09 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.75/296.09 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.75/296.09 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.75/296.09 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.75/296.09 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.75/296.09 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.75/296.09 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.75/296.09 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.85/296.10 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.85/296.10 Matrix Interpretation Processor: dim=3 1164.85/296.10 1164.85/296.10 max_matrix: 1164.85/296.10 [1 1 1] 1164.85/296.10 [0 1 1] 1164.85/296.10 [0 0 0] 1164.85/296.10 interpretation: 1164.85/296.10 [1 0 0] 1164.85/296.10 [5](x0) = [0 1 1]x0 1164.85/296.10 [0 0 0] , 1164.85/296.10 1164.85/296.10 [1 0 0] [0] 1164.85/296.10 [4](x0) = [0 0 0]x0 + [0] 1164.85/296.10 [0 0 0] [1], 1164.85/296.10 1164.85/296.10 [1 0 0] [0] 1164.85/296.10 [3](x0) = [0 0 0]x0 + [0] 1164.85/296.10 [0 0 0] [1], 1164.85/296.10 1164.85/296.10 [1 0 0] 1164.85/296.10 [2](x0) = [0 0 0]x0 1164.85/296.10 [0 0 0] , 1164.85/296.10 1164.85/296.10 [1 1 0] [0] 1164.85/296.10 [0](x0) = [0 0 0]x0 + [1] 1164.85/296.10 [0 0 0] [0], 1164.85/296.10 1164.85/296.10 [1 1 1] [0] 1164.85/296.10 [1](x0) = [0 0 0]x0 + [1] 1164.85/296.10 [0 0 0] [0] 1164.85/296.10 orientation: 1164.85/296.10 [1 1 1] [2] [1 0 0] [1] 1164.85/296.10 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(2(0(1(2(x1))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [2] [1 0 0] [1] 1164.85/296.10 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(0(2(2(1(2(x1)))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [2] [1 1 1] [1] 1164.85/296.10 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(2(1(1(x1)))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [2] [1 1 1] [1] 1164.85/296.10 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(1(x1)))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 1 1] [0] 1164.85/296.10 0(5(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(5(x1)))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 1 1] [0] 1164.85/296.10 0(5(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(4(5(1(x1)))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 1 1] [0] 1164.85/296.10 0(5(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(2(3(1(5(x1))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 0 0] [0] 1164.85/296.10 0(5(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(5(2(x1))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 1 1] [1] 1164.85/296.10 0(0(2(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(3(0(2(0(1(x1)))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [0] [1 0 0] [0] 1164.85/296.10 5(3(2(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(3(5(2(x1))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 0 0] [0] 1164.85/296.10 0(5(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(2(5(2(x1)))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [1] [1 0 0] [0] 1164.85/296.10 5(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(0(2(1(2(4(x1)))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.10 1164.85/296.10 [1 1 1] [0] [1 0 0] [0] 1164.85/296.10 5(3(1(5(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(3(1(2(5(x1))))) 1164.85/296.10 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [1] [1 0 0] [0] 1164.85/296.11 5(4(2(1(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(4(1(2(1(2(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 1] [0] 1164.85/296.11 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(4(0(4(1(x1))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [1] 1164.85/296.11 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(0(x1)))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [1] 1164.85/296.11 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(4(0(x1)))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [0] 1164.85/296.11 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(0(x1))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [1] 1164.85/296.11 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(0(x1))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [1] 1164.85/296.11 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(4(2(0(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 0 0] [2] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(1(3(0(4(x1))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 1] [0] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(1(x1))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 0 0] [1] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(3(1(2(4(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 0 0] [1] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(4(2(1(2(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [1] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(1(2(4(3(0(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 0 0] [1] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(1(0(4(4(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [2] [1 1 0] [1] 1164.85/296.11 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(1(3(0(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [1] [1 1 0] [0] 1164.85/296.11 5(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(1(2(4(0(x1))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.11 1164.85/296.11 [1 1 1] [1] [1 0 0] [0] 1164.85/296.11 5(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(1(2(3(0(4(x1)))))) 1164.85/296.11 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 1 1] [1] 1164.85/296.12 0(0(1(5(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(4(1(0(5(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [3] [1 1 1] [2] 1164.85/296.12 0(1(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(0(1(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [3] [1 1 0] [3] 1164.85/296.12 0(1(1(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(1(3(1(0(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 1 0] [1] 1164.85/296.12 5(0(1(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(5(1(2(0(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [1] [1 1 0] [0] 1164.85/296.12 5(3(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(1(2(3(0(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 1 0] [1] 1164.85/296.12 0(0(5(1(5(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(5(5(0(0(x1)))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 0 0] [2] 1164.85/296.12 0(5(3(0(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(5(3(0(4(x1)))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 1 0] [1] 1164.85/296.12 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(1(0(x1)))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 0 0] [2] 1164.85/296.12 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(3(0(2(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 0 0] [2] 1164.85/296.12 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(3(0(4(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 0 0] [1] 1164.85/296.12 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(0(1(2(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 1 1] [0] 1164.85/296.12 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(3(0(3(1(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 0 0] [0] 1164.85/296.12 0(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(3(0(4(x1)))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [1] [1 1 1] 1164.85/296.12 0(0(2(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 2(0(3(0(2(1(x1)))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] 1164.85/296.12 1164.85/296.12 [1 1 1] [1] [1 0 0] [0] 1164.85/296.12 5(4(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(5(0(4(x1))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.12 1164.85/296.12 [1 1 1] [2] [1 0 0] [2] 1164.85/296.12 0(5(4(0(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(3(0(4(5(x1)))))) 1164.85/296.12 [0 0 0] [0] [0 0 0] [0] 1164.85/296.13 1164.85/296.13 [1 1 1] [1] [1 0 0] [1] 1164.85/296.13 0(5(3(4(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(3(5(4(5(x1)))))) 1164.85/296.13 [0 0 0] [0] [0 0 0] [0] 1164.85/296.13 problem: 1164.85/296.13 strict: 1164.85/296.13 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.85/296.13 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.85/296.13 weak: 1164.85/296.13 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.85/296.13 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.85/296.13 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.85/296.13 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.85/296.13 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.85/296.13 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.85/296.13 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.85/296.13 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.85/296.13 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.85/296.13 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.85/296.13 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.85/296.13 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.85/296.13 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.85/296.13 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.85/296.13 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.85/296.13 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.85/296.13 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.85/296.13 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.85/296.13 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.85/296.13 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.85/296.13 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.85/296.13 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.85/296.13 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.85/296.13 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.85/296.13 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.85/296.13 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.85/296.13 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.85/296.13 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.85/296.13 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.85/296.13 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.85/296.13 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.85/296.13 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.85/296.13 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.85/296.13 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.85/296.13 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.85/296.13 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.85/296.13 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.85/296.13 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.85/296.13 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.85/296.13 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.85/296.13 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.85/296.13 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.85/296.13 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.85/296.13 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.85/296.13 Matrix Interpretation Processor: dim=3 1164.85/296.13 1164.85/296.13 max_matrix: 1164.85/296.13 [1 1 0] 1164.85/296.13 [0 0 1] 1164.85/296.13 [0 0 1] 1164.85/296.13 interpretation: 1164.85/296.13 [1 0 0] [0] 1164.85/296.13 [5](x0) = [0 0 0]x0 + [0] 1164.85/296.13 [0 0 0] [1], 1164.85/296.13 1164.85/296.13 [1 0 0] [0] 1164.85/296.13 [4](x0) = [0 0 1]x0 + [1] 1164.85/296.13 [0 0 0] [0], 1164.85/296.13 1164.85/296.13 [1 1 0] 1164.85/296.13 [3](x0) = [0 0 0]x0 1164.85/296.13 [0 0 0] , 1164.85/296.13 1164.85/296.13 [1 0 0] 1164.85/296.13 [2](x0) = [0 0 1]x0 1164.85/296.13 [0 0 0] , 1164.85/296.13 1164.85/296.13 [1 0 0] 1164.85/296.13 [0](x0) = [0 0 0]x0 1164.85/296.13 [0 0 1] , 1164.85/296.13 1164.85/296.13 [1 0 0] [0] 1164.85/296.13 [1](x0) = [0 0 0]x0 + [0] 1164.85/296.13 [0 0 0] [1] 1164.85/296.13 orientation: 1164.85/296.13 [1 0 0] [1 0 0] 1164.85/296.13 0(0(2(1(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 2(3(0(2(0(1(x1)))))) 1164.85/296.13 [0 0 0] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [1] [1 0 0] [0] 1164.85/296.13 5(3(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(3(5(2(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(0(1(2(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(2(1(2(x1)))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(1(1(x1)))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(1(1(x1)))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(5(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(1(5(x1)))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(5(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(4(5(1(x1)))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(5(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(3(1(5(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(5(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(1(5(2(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(5(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(1(2(5(2(x1)))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(1(2(4(x1)))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 5(3(1(5(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(3(1(2(5(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 5(4(2(1(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(4(1(2(1(2(x1)))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(4(0(4(1(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(2(0(x1)))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(0(x1)))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(0(2(0(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(2(0(0(x1))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.13 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(2(4(2(0(x1)))))) 1164.85/296.13 [0 0 0] [1] [0 0 0] [1] 1164.85/296.13 1164.85/296.13 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(3(0(4(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(0(2(1(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(1(2(4(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(2(1(2(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(2(4(3(0(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(0(4(4(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(2(1(3(0(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(1(2(4(0(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(1(2(3(0(4(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] 1164.85/296.14 0(0(1(5(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(4(1(0(5(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(2(0(1(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(1(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(3(1(0(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 5(0(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(1(2(0(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 5(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(1(2(3(0(x1))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(0(5(1(5(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(5(5(0(0(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.14 1164.85/296.14 [1 0 0] [0] [1 0 0] [0] 1164.85/296.14 0(5(3(0(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(5(3(0(4(x1)))))) 1164.85/296.14 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] 1164.85/296.15 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(1(0(x1)))) 1164.85/296.15 [0 0 0] [1] [0 0 0] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] [0] 1164.85/296.15 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(0(2(x1))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] [0] 1164.85/296.15 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(0(4(x1))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] 1164.85/296.15 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(0(1(2(x1))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] 1164.85/296.15 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(3(0(3(1(x1))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] [0] 1164.85/296.15 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(0(3(0(4(x1)))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 1164.85/296.15 [1 0 0] [1 0 0] 1164.85/296.15 0(0(2(1(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = 2(0(3(0(2(1(x1)))))) 1164.85/296.15 [0 0 0] [0 0 0] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] [0] 1164.85/296.15 5(4(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(5(0(4(x1))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 1164.85/296.15 [1 0 0] [0] [1 0 0] [0] 1164.85/296.15 0(5(4(0(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(0(4(5(x1)))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 1164.85/296.15 [1 0 0] [2] [1 0 0] [0] 1164.85/296.15 0(5(3(4(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(5(4(5(x1)))))) 1164.85/296.15 [0 0 0] [1] [0 0 0] [1] 1164.85/296.15 problem: 1164.85/296.15 strict: 1164.85/296.15 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.85/296.15 weak: 1164.85/296.15 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.85/296.15 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.85/296.15 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.85/296.15 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.85/296.15 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.85/296.15 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.85/296.15 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.85/296.15 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.85/296.15 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.85/296.15 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.85/296.15 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.85/296.15 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.85/296.15 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.85/296.15 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.85/296.15 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.85/296.15 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.85/296.15 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.85/296.15 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.85/296.15 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.85/296.15 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.85/296.15 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.85/296.15 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.85/296.15 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.85/296.15 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.85/296.15 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.85/296.15 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.85/296.15 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.85/296.15 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.85/296.15 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.85/296.15 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.85/296.15 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.85/296.16 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.85/296.16 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.85/296.16 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.85/296.16 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.85/296.16 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.85/296.16 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.85/296.16 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.85/296.16 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.85/296.16 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.85/296.16 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.85/296.16 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.85/296.16 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.85/296.16 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.85/296.16 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.85/296.16 Matrix Interpretation Processor: dim=3 1164.85/296.16 1164.85/296.16 max_matrix: 1164.85/296.16 [1 1 1] 1164.85/296.16 [0 1 0] 1164.85/296.16 [0 0 0] 1164.85/296.16 interpretation: 1164.85/296.16 [1 0 1] 1164.85/296.16 [5](x0) = [0 1 0]x0 1164.85/296.16 [0 0 0] , 1164.85/296.16 1164.85/296.16 [1 0 0] 1164.85/296.16 [4](x0) = [0 1 0]x0 1164.85/296.16 [0 0 0] , 1164.85/296.16 1164.85/296.16 [1 0 0] 1164.85/296.16 [3](x0) = [0 1 0]x0 1164.85/296.16 [0 0 0] , 1164.85/296.16 1164.85/296.16 [1 0 0] 1164.85/296.16 [2](x0) = [0 1 0]x0 1164.85/296.16 [0 0 0] , 1164.85/296.16 1164.85/296.16 [1 1 1] [0] 1164.85/296.16 [0](x0) = [0 1 0]x0 + [0] 1164.85/296.16 [0 0 0] [1], 1164.85/296.16 1164.85/296.16 [1 0 1] [0] 1164.85/296.16 [1](x0) = [0 1 0]x0 + [2] 1164.85/296.16 [0 0 0] [0] 1164.85/296.16 orientation: 1164.85/296.16 [1 2 1] [5] [1 2 1] [4] 1164.85/296.16 0(0(2(1(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 2(3(0(2(0(1(x1)))))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [0] 1164.85/296.16 1164.85/296.16 [1 0 1] [0] [1 0 0] [0] 1164.85/296.16 5(3(2(1(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(3(5(2(x1))))) 1164.85/296.16 [0 0 0] [0] [0 0 0] [0] 1164.85/296.16 1164.85/296.16 [1 2 1] [5] [1 2 0] [4] 1164.85/296.16 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(2(0(1(2(x1))))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 2 1] [5] [1 2 0] [5] 1164.85/296.16 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(0(2(2(1(2(x1)))))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 1 1] [4] [1 1 1] [4] 1164.85/296.16 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 0(2(1(1(x1)))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 1 1] [4] [1 1 1] [4] 1164.85/296.16 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 0(3(1(1(x1)))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 1 1] [2] [1 1 1] [2] 1164.85/296.16 0(5(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(1(5(x1)))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 1 1] [2] [1 1 1] [2] 1164.85/296.16 0(5(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(4(5(1(x1)))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 1 1] [2] [1 1 1] [2] 1164.85/296.16 0(5(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(2(3(1(5(x1))))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.16 1164.85/296.16 [1 1 1] [2] [1 1 0] [2] 1164.85/296.16 0(5(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(1(5(2(x1))))) 1164.85/296.16 [0 0 0] [1] [0 0 0] [1] 1164.85/296.17 1164.85/296.17 [1 1 1] [2] [1 1 0] [2] 1164.85/296.17 0(5(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(1(2(5(2(x1)))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [1] 1164.85/296.17 1164.85/296.17 [1 1 1] [3] [1 1 0] [3] 1164.85/296.17 5(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 5(0(2(1(2(4(x1)))))) 1164.85/296.17 [0 0 0] [0] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 0 1] [0] [1 0 1] [0] 1164.85/296.17 5(3(1(5(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 5(3(1(2(5(x1))))) 1164.85/296.17 [0 0 0] [0] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 0 1] [0] [1 0 0] [0] 1164.85/296.17 5(4(2(1(1(x1))))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 5(4(1(2(1(2(x1)))))) 1164.85/296.17 [0 0 0] [0] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 2 1] [5] [1 2 1] [4] 1164.85/296.17 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(4(0(4(1(x1))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [1] 1164.85/296.17 1164.85/296.17 [1 2 1] [5] [1 2 1] [2] 1164.85/296.17 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(1(2(0(x1)))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [1] 1164.85/296.17 1164.85/296.17 [1 2 1] [5] [1 2 1] [1] 1164.85/296.17 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(0(4(0(x1)))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 2 1] [5] [1 2 1] [0] 1164.85/296.17 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(0(2(0(x1))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 2 1] [5] [1 2 1] [1] 1164.85/296.17 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(2(0(0(x1))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 2 1] [5] [1 2 1] [2] 1164.85/296.17 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(1(2(4(2(0(x1)))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [1] 1164.85/296.17 1164.85/296.17 [1 1 1] [4] [1 1 0] [0] 1164.85/296.17 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(1(3(0(4(x1))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 1 1] [4] [1 1 1] [2] 1164.85/296.17 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(2(0(2(1(x1))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 1 1] [4] [1 1 0] [3] 1164.85/296.17 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(0(3(1(2(4(x1)))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 1 1] [4] [1 1 0] [3] 1164.85/296.17 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(0(4(2(1(2(x1)))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 1 1] [4] [1 1 1] [0] 1164.85/296.17 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(1(2(4(3(0(x1)))))) 1164.85/296.17 [0 0 0] [1] [0 0 0] [0] 1164.85/296.17 1164.85/296.17 [1 1 1] [4] [1 1 0] [1] 1164.85/296.17 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(2(1(0(4(4(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [4] [1 1 1] [0] 1164.85/296.18 0(1(1(x1))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(2(2(1(3(0(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [3] [1 1 1] [0] 1164.85/296.18 5(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 5(1(2(4(0(x1))))) 1164.85/296.18 [0 0 0] [0] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [3] [1 1 0] [0] 1164.85/296.18 5(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 5(1(2(3(0(4(x1)))))) 1164.85/296.18 [0 0 0] [0] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 1] [3] 1164.85/296.18 0(0(1(5(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(4(1(0(5(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 2 1] [7] [1 2 1] [5] 1164.85/296.18 0(1(0(1(x1)))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(0(2(0(1(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [6] [1 1 1] [1] 1164.85/296.18 0(1(1(1(x1)))) = [0 1 0]x1 + [6] >= [0 1 0]x1 + [6] = 1(1(3(1(0(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [5] [1 1 1] [0] 1164.85/296.18 5(0(1(1(x1)))) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [4] = 1(5(1(2(0(x1))))) 1164.85/296.18 [0 0 0] [0] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [2] [1 1 1] [0] 1164.85/296.18 5(3(0(1(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 5(1(2(3(0(x1))))) 1164.85/296.18 [0 0 0] [0] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 1] [2] 1164.85/296.18 0(0(5(1(5(x1))))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(5(5(0(0(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 2 1] [4] [1 2 0] [1] 1164.85/296.18 0(5(3(0(1(x1))))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(0(5(3(0(4(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 1] [3] 1164.85/296.18 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(1(0(x1)))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 0] [2] 1164.85/296.18 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(1(3(0(2(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 0] [2] 1164.85/296.18 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(1(3(0(4(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 0] [4] 1164.85/296.18 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(0(1(2(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 1] [4] 1164.85/296.18 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(3(0(3(1(x1))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 0] [0] 1164.85/296.18 0(0(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(0(3(0(4(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 2 1] [5] [1 2 1] [4] 1164.85/296.18 0(0(2(1(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 2(0(3(0(2(1(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 1 1] [2] [1 1 0] [1] 1164.85/296.18 5(4(0(1(x1)))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(2(5(0(4(x1))))) 1164.85/296.18 [0 0 0] [0] [0 0 0] [0] 1164.85/296.18 1164.85/296.18 [1 2 1] [4] [1 2 1] [2] 1164.85/296.18 0(5(4(0(1(x1))))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(1(3(0(4(5(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [1] 1164.85/296.18 1164.85/296.18 [1 1 1] [2] [1 1 1] [1] 1164.85/296.18 0(5(3(4(1(x1))))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1(0(3(5(4(5(x1)))))) 1164.85/296.18 [0 0 0] [1] [0 0 0] [0] 1164.85/296.18 problem: 1164.85/296.18 strict: 1164.85/296.18 1164.85/296.18 weak: 1164.85/296.18 0(0(2(1(x1)))) -> 2(3(0(2(0(1(x1)))))) 1164.85/296.18 5(3(2(1(x1)))) -> 1(2(3(5(2(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(2(0(1(2(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(0(2(2(1(2(x1)))))) 1164.85/296.18 0(1(1(x1))) -> 0(2(1(1(x1)))) 1164.85/296.18 0(1(1(x1))) -> 0(3(1(1(x1)))) 1164.85/296.18 0(5(1(x1))) -> 0(3(1(5(x1)))) 1164.85/296.18 0(5(1(x1))) -> 0(4(5(1(x1)))) 1164.85/296.18 0(5(1(x1))) -> 0(2(3(1(5(x1))))) 1164.85/296.18 0(5(1(x1))) -> 0(3(1(5(2(x1))))) 1164.85/296.18 0(5(1(x1))) -> 0(3(1(2(5(2(x1)))))) 1164.85/296.18 5(0(1(x1))) -> 5(0(2(1(2(4(x1)))))) 1164.85/296.18 5(3(1(5(x1)))) -> 5(3(1(2(5(x1))))) 1164.85/296.18 5(4(2(1(1(x1))))) -> 5(4(1(2(1(2(x1)))))) 1164.85/296.18 0(0(1(x1))) -> 0(4(0(4(1(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(1(2(0(x1)))) 1164.85/296.18 0(0(1(x1))) -> 1(0(4(0(x1)))) 1164.85/296.18 0(0(1(x1))) -> 1(2(0(2(0(x1))))) 1164.85/296.18 0(0(1(x1))) -> 1(2(2(0(0(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(1(2(4(2(0(x1)))))) 1164.85/296.18 0(1(1(x1))) -> 1(1(3(0(4(x1))))) 1164.85/296.18 0(1(1(x1))) -> 1(2(0(2(1(x1))))) 1164.85/296.18 0(1(1(x1))) -> 1(0(3(1(2(4(x1)))))) 1164.85/296.18 0(1(1(x1))) -> 1(0(4(2(1(2(x1)))))) 1164.85/296.18 0(1(1(x1))) -> 1(1(2(4(3(0(x1)))))) 1164.85/296.18 0(1(1(x1))) -> 1(2(1(0(4(4(x1)))))) 1164.85/296.18 0(1(1(x1))) -> 1(2(2(1(3(0(x1)))))) 1164.85/296.18 5(0(1(x1))) -> 5(1(2(4(0(x1))))) 1164.85/296.18 5(0(1(x1))) -> 5(1(2(3(0(4(x1)))))) 1164.85/296.18 0(0(1(5(x1)))) -> 0(4(1(0(5(x1))))) 1164.85/296.18 0(1(0(1(x1)))) -> 1(0(2(0(1(x1))))) 1164.85/296.18 0(1(1(1(x1)))) -> 1(1(3(1(0(x1))))) 1164.85/296.18 5(0(1(1(x1)))) -> 1(5(1(2(0(x1))))) 1164.85/296.18 5(3(0(1(x1)))) -> 5(1(2(3(0(x1))))) 1164.85/296.18 0(0(5(1(5(x1))))) -> 1(2(5(5(0(0(x1)))))) 1164.85/296.18 0(5(3(0(1(x1))))) -> 1(0(5(3(0(4(x1)))))) 1164.85/296.18 0(0(1(x1))) -> 0(3(1(0(x1)))) 1164.85/296.18 0(0(1(x1))) -> 0(1(3(0(2(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(1(3(0(4(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(3(0(1(2(x1))))) 1164.85/296.18 0(0(1(x1))) -> 0(3(0(3(1(x1))))) 1164.85/296.18 0(0(1(x1))) -> 1(2(0(3(0(4(x1)))))) 1164.85/296.18 0(0(2(1(x1)))) -> 2(0(3(0(2(1(x1)))))) 1164.85/296.18 5(4(0(1(x1)))) -> 1(2(5(0(4(x1))))) 1164.85/296.18 0(5(4(0(1(x1))))) -> 0(1(3(0(4(5(x1)))))) 1164.85/296.18 0(5(3(4(1(x1))))) -> 1(0(3(5(4(5(x1)))))) 1164.85/296.18 Qed 1164.85/296.19 EOF