YES(?,O(n^1)) 668.05/168.61 YES(?,O(n^1)) 668.05/168.62 668.05/168.62 Problem: 668.05/168.62 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.05/168.62 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.62 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.05/168.62 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.05/168.62 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.05/168.62 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.05/168.62 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.62 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.62 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.05/168.62 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.05/168.62 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.05/168.62 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.05/168.62 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.05/168.62 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.05/168.62 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.05/168.62 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.05/168.62 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.05/168.62 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.62 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.05/168.62 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.05/168.62 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.05/168.62 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.05/168.62 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.05/168.62 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.05/168.62 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.05/168.62 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.05/168.62 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.05/168.62 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.05/168.62 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.05/168.62 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.05/168.62 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.05/168.62 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.05/168.62 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.05/168.62 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.05/168.62 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.05/168.62 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.05/168.62 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.05/168.62 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.05/168.62 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.05/168.62 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.05/168.62 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.05/168.62 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.05/168.62 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.05/168.62 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.05/168.62 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.05/168.62 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.05/168.62 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.05/168.62 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.05/168.62 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.05/168.62 668.05/168.62 Proof: 668.05/168.62 Complexity Transformation Processor: 668.05/168.62 strict: 668.05/168.62 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.05/168.62 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.62 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.05/168.62 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.05/168.62 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.05/168.62 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.05/168.62 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.62 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.62 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.05/168.62 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.05/168.62 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.05/168.62 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.05/168.62 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.05/168.62 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.05/168.62 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.05/168.62 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.05/168.62 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.05/168.62 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.62 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.05/168.62 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.05/168.62 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.05/168.62 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.05/168.62 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.05/168.62 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.05/168.62 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.05/168.62 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.05/168.62 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.05/168.62 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.05/168.62 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.05/168.62 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.05/168.62 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.05/168.62 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.05/168.62 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.05/168.62 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.05/168.62 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.05/168.62 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.05/168.62 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.05/168.62 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.05/168.62 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.05/168.62 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.05/168.62 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.05/168.62 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.05/168.62 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.05/168.62 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.05/168.62 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.05/168.62 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.05/168.62 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.05/168.62 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.05/168.62 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.05/168.62 weak: 668.05/168.62 668.05/168.62 Matrix Interpretation Processor: dim=2 668.05/168.62 668.05/168.62 max_matrix: 668.05/168.62 [1 1] 668.05/168.62 [0 0] 668.05/168.62 interpretation: 668.05/168.62 [1 0] 668.05/168.62 [5](x0) = [0 0]x0, 668.05/168.62 668.05/168.62 [1 0] 668.05/168.62 [4](x0) = [0 0]x0, 668.05/168.62 668.05/168.62 [1 0] 668.05/168.62 [3](x0) = [0 0]x0, 668.05/168.62 668.05/168.62 [1 0] [0] 668.05/168.62 [0](x0) = [0 0]x0 + [1], 668.05/168.63 668.05/168.63 [1 1] 668.05/168.63 [1](x0) = [0 0]x0, 668.05/168.63 668.05/168.63 [1 1] [0] 668.05/168.63 [2](x0) = [0 0]x0 + [1] 668.05/168.63 orientation: 668.05/168.63 [1 1] [1] [1 1] [0] 668.05/168.63 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(x1)))) 668.05/168.63 668.05/168.63 [1 1] [1] [1 0] [0] 668.05/168.63 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(x1)))) 668.05/168.63 668.05/168.63 [1 1] [1] [1 0] [0] 668.05/168.63 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(4(4(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(0(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(4(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] 668.05/168.63 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 1(3(4(4(4(0(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(4(3(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(3(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(3(3(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(3(4(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(5(5(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(4(4(3(4(0(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(4(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(4(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(4(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(3(x1)))) 668.05/168.63 668.05/168.63 [1 1] [1] [1 1] 668.05/168.63 2(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 5(0(2(1(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 1] 668.05/168.63 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 1(3(5(2(x1)))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(5(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 1] 668.05/168.63 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 1(4(3(5(2(x1))))) 668.05/168.63 668.05/168.63 [1 1] [1] [1 1] 668.05/168.63 0(2(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = 5(0(0(2(1(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.63 0(3(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(1(3(4(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 1] [0] 668.05/168.63 0(3(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(3(4(2(1(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [1] [1 1] [1] 668.05/168.63 0(3(2(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 1(3(4(0(2(2(x1)))))) 668.05/168.63 668.05/168.63 [1 1] [1] [1 0] 668.05/168.63 0(4(1(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = 1(4(0(2(5(x1))))) 668.05/168.63 668.05/168.63 [1 1] [0] [1 0] [0] 668.05/168.64 0(4(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(3(4(4(0(0(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(5(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(3(5(4(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(5(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(5(3(4(0(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(5(3(x1))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(3(3(x1))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 1] [1] 668.05/168.64 2(0(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [1] 668.05/168.64 2(0(4(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 2(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(5(2(3(3(x1))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 2(5(4(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(2(4(x1))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 1] [0] 668.05/168.64 0(0(3(2(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(1(3(5(2(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [1] 668.05/168.64 0(1(0(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(3(2(0(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [1] 668.05/168.64 0(1(0(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(3(1(0(0(5(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(3(2(5(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(1(3(3(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [0] 668.05/168.64 0(5(1(1(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(1(1(5(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [2] [1 1] [1] 668.05/168.64 0(5(1(2(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(2(1(2(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(5(3(2(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(2(5(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(5(5(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(1(3(5(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [1] 668.05/168.64 2(0(3(1(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [2] [1 1] 668.05/168.64 2(2(0(3(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = 1(3(0(2(5(2(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [2] [1 1] [1] 668.05/168.64 2(2(0(5(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] 668.05/168.64 2(5(5(4(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.05/168.64 problem: 668.05/168.64 strict: 668.05/168.64 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.05/168.64 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.05/168.64 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.05/168.64 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.64 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.64 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.05/168.64 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.05/168.64 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.05/168.64 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.05/168.64 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.05/168.64 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.05/168.64 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.05/168.64 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.05/168.64 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.05/168.64 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.64 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.05/168.64 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.05/168.64 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.05/168.64 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.05/168.64 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.05/168.64 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.05/168.64 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.05/168.64 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.05/168.64 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.05/168.64 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.05/168.64 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.05/168.64 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.05/168.64 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.05/168.64 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.05/168.64 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.05/168.64 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.05/168.64 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.05/168.64 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.05/168.64 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.05/168.64 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.05/168.64 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.05/168.64 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.05/168.64 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.05/168.64 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.05/168.64 weak: 668.05/168.64 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.05/168.64 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.64 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.05/168.64 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.05/168.64 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.05/168.64 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.05/168.64 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.05/168.64 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.05/168.64 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.05/168.64 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.05/168.64 Matrix Interpretation Processor: dim=2 668.05/168.64 668.05/168.64 max_matrix: 668.05/168.64 [1 1] 668.05/168.64 [0 0] 668.05/168.64 interpretation: 668.05/168.64 [1 0] 668.05/168.64 [5](x0) = [0 0]x0, 668.05/168.64 668.05/168.64 [1 0] 668.05/168.64 [4](x0) = [0 0]x0, 668.05/168.64 668.05/168.64 [1 1] 668.05/168.64 [3](x0) = [0 0]x0, 668.05/168.64 668.05/168.64 [1 0] [0] 668.05/168.64 [0](x0) = [0 0]x0 + [1], 668.05/168.64 668.05/168.64 [1 1] 668.05/168.64 [1](x0) = [0 0]x0, 668.05/168.64 668.05/168.64 [1 1] [0] 668.05/168.64 [2](x0) = [0 0]x0 + [1] 668.05/168.64 orientation: 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(0(x1))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(4(x1))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] 668.05/168.64 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 1(3(4(4(4(0(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 1] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(x1)))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(x1)))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 1] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(4(3(x1))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 1] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(3(x1))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 1] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(3(3(x1))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(3(4(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(5(5(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [1] [1 0] [0] 668.05/168.64 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(4(4(3(4(0(x1)))))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(4(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(4(x1)))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(4(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(x1)))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(x1)))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 0] [0] 668.05/168.64 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(x1)))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 1] [0] 668.05/168.64 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(3(x1)))) 668.05/168.64 668.05/168.64 [1 1] [0] [1 1] 668.05/168.64 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 1(3(5(2(x1)))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 0] [0] 668.05/168.65 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(5(x1))))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 1] 668.05/168.65 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 1(4(3(5(2(x1))))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 0] [0] 668.05/168.65 0(3(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(1(3(4(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(3(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(3(4(2(1(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [2] [1 1] [1] 668.05/168.65 0(3(2(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 1(3(4(0(2(2(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 0] [0] 668.05/168.65 0(4(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(3(4(4(0(0(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 0] [0] 668.05/168.65 0(5(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(3(5(4(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 0] [0] 668.05/168.65 0(5(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(5(3(4(0(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(5(3(x1))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(3(3(x1))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [1] 668.05/168.65 2(0(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 0] [1] 668.05/168.65 2(0(4(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 2(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(5(2(3(3(x1))))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 0] [0] 668.05/168.65 2(5(4(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(2(4(x1))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(0(3(2(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(1(3(5(2(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [2] [1 0] [2] 668.05/168.65 0(1(0(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(3(2(0(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [2] [1 0] [1] 668.05/168.65 0(1(0(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(3(1(0(0(5(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(3(2(5(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(1(3(3(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 0] [0] 668.05/168.65 0(5(3(2(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(2(5(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 0] [0] 668.05/168.65 0(5(5(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(1(3(5(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 0] [1] 668.05/168.65 2(0(3(1(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [0] [1 0] 668.05/168.65 2(5(5(4(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(x1)))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] [0] 668.05/168.65 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(x1)))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 0] [0] 668.05/168.65 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(4(4(x1)))))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] 668.05/168.65 2(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 = 5(0(2(1(x1)))) 668.05/168.65 668.05/168.65 [1 1] [1] [1 1] 668.05/168.65 0(2(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = 5(0(0(2(1(x1))))) 668.05/168.66 668.05/168.66 [1 1] [1] [1 0] 668.05/168.66 0(4(1(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = 1(4(0(2(5(x1))))) 668.05/168.66 668.05/168.66 [1 1] [1] [1 0] [0] 668.05/168.66 0(5(1(1(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(1(1(5(x1)))))) 668.05/168.66 668.05/168.66 [1 1] [2] [1 1] [1] 668.05/168.66 0(5(1(2(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(2(1(2(x1)))))) 668.05/168.66 668.05/168.66 [1 1] [2] [1 1] [1] 668.05/168.66 2(2(0(3(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 1(3(0(2(5(2(x1)))))) 668.05/168.66 668.05/168.66 [1 1] [2] [1 1] [1] 668.05/168.66 2(2(0(5(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.05/168.66 problem: 668.05/168.66 strict: 668.05/168.66 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.05/168.66 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.05/168.66 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.05/168.66 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.05/168.66 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.05/168.66 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.05/168.66 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.66 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.05/168.66 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.05/168.66 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.05/168.66 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.05/168.66 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.05/168.66 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.05/168.66 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.05/168.66 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.05/168.66 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.05/168.66 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.05/168.66 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.05/168.66 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.05/168.66 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.05/168.66 weak: 668.05/168.66 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.66 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.66 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.05/168.66 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.05/168.66 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.05/168.66 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.05/168.66 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.05/168.66 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.05/168.66 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.05/168.66 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.05/168.66 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.05/168.66 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.05/168.66 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.05/168.66 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.05/168.66 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.05/168.66 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.05/168.66 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.05/168.66 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.05/168.66 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.05/168.66 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.05/168.66 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.66 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.05/168.66 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.05/168.66 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.05/168.66 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.05/168.66 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.05/168.66 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.05/168.66 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.05/168.66 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.05/168.66 Matrix Interpretation Processor: dim=2 668.05/168.66 668.05/168.66 max_matrix: 668.05/168.66 [1 1] 668.05/168.66 [0 0] 668.05/168.66 interpretation: 668.05/168.66 [1 0] 668.05/168.66 [5](x0) = [0 0]x0, 668.05/168.66 668.05/168.66 [1 1] 668.05/168.66 [4](x0) = [0 0]x0, 668.05/168.66 668.05/168.66 [1 1] 668.05/168.66 [3](x0) = [0 0]x0, 668.05/168.66 668.05/168.66 [1 0] [0] 668.05/168.66 [0](x0) = [0 0]x0 + [1], 668.05/168.66 668.05/168.66 [1 1] [0] 668.05/168.66 [1](x0) = [0 0]x0 + [1], 668.05/168.66 668.05/168.66 [1 1] [0] 668.05/168.66 [2](x0) = [0 0]x0 + [1] 668.05/168.66 orientation: 668.05/168.66 [1 1] [1] [1 0] [1] 668.05/168.66 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(0(x1))))) 668.05/168.66 668.05/168.66 [1 1] [1] [1 1] [0] 668.05/168.66 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(4(x1))))) 668.05/168.66 668.05/168.66 [1 1] [1] [1 0] [1] 668.05/168.66 0(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(4(4(4(0(x1)))))) 668.05/168.66 668.05/168.66 [1 1] [1] [1 1] [0] 668.05/168.66 0(4(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(4(x1)))) 668.05/168.66 668.05/168.66 [1 1] [1] [1 1] [1] 668.05/168.67 0(4(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [1] 668.05/168.67 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 0(4(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(3(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(5(2(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 0] [1] 668.05/168.67 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(5(x1))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 2(3(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(4(3(5(2(x1))))) 668.05/168.67 668.05/168.67 [1 1] [2] [1 1] [1] 668.05/168.67 0(3(1(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(1(3(4(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 0(5(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(3(5(4(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 0] [1] 668.05/168.67 0(5(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(5(3(4(0(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [2] [1 1] [1] 668.05/168.67 2(0(3(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [2] [1 0] [1] 668.05/168.67 2(0(4(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 2(5(4(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(2(4(x1))))) 668.05/168.67 668.05/168.67 [1 1] [2] [1 0] [2] 668.05/168.67 0(1(0(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(4(3(2(0(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [3] [1 1] [2] 668.05/168.67 2(0(3(1(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [1] 668.05/168.67 2(5(5(4(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 5(5(2(1(3(4(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [1] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(x1)))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(4(3(x1))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [1] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(4(3(x1))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [0] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(3(3(x1))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 1] [1] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(3(4(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 0] [0] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(3(4(5(5(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 0] [1] 668.05/168.67 0(3(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(4(4(3(4(0(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [2] [1 1] [2] 668.05/168.67 0(3(2(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(3(4(2(1(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [2] [1 1] [2] 668.05/168.67 0(3(2(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(4(0(2(2(x1)))))) 668.05/168.67 668.05/168.67 [1 1] [1] [1 0] [1] 668.05/168.67 0(4(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(3(4(4(0(0(x1)))))) 668.05/168.67 668.05/168.68 [1 1] [1] [1 1] [0] 668.05/168.68 0(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(5(3(x1))))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [0] 668.05/168.68 0(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(3(3(x1))))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [0] 668.05/168.68 2(5(3(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(5(2(3(3(x1))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 1] [0] 668.05/168.68 0(0(3(2(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(1(3(5(2(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 0] [2] 668.05/168.68 0(1(0(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(3(1(0(0(5(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [0] 668.05/168.68 0(3(2(5(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(1(3(3(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 0] [1] 668.05/168.68 0(5(3(2(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(3(4(2(5(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 0] [0] 668.05/168.68 0(5(5(3(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(1(3(5(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [1] 668.05/168.68 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(x1)))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [1] 668.05/168.68 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(3(x1)))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [1] 668.05/168.68 0(1(2(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(4(4(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [1] 668.05/168.68 2(0(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 5(0(2(1(x1)))) 668.05/168.68 668.05/168.68 [1 1] [1] [1 1] [1] 668.05/168.68 0(2(0(1(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 5(0(0(2(1(x1))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 0] [1] 668.05/168.68 0(4(1(2(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(4(0(2(5(x1))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 0] [2] 668.05/168.68 0(5(1(1(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(4(1(1(5(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 1] [2] 668.05/168.68 0(5(1(2(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(5(2(1(2(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [3] [1 1] [1] 668.05/168.68 2(2(0(3(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(3(0(2(5(2(x1)))))) 668.05/168.68 668.05/168.68 [1 1] [2] [1 1] [2] 668.05/168.68 2(2(0(5(1(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.05/168.68 problem: 668.05/168.68 strict: 668.05/168.68 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.05/168.68 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.05/168.68 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.05/168.68 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.05/168.68 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.05/168.68 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.05/168.68 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.05/168.68 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.05/168.68 weak: 668.05/168.68 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.05/168.68 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.05/168.68 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.68 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.05/168.68 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.05/168.68 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.05/168.68 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.05/168.68 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.05/168.68 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.05/168.68 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.05/168.68 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.05/168.68 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.05/168.68 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.68 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.68 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.05/168.68 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.05/168.68 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.05/168.68 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.05/168.68 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.05/168.68 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.05/168.68 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.05/168.68 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.05/168.68 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.05/168.68 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.05/168.68 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.05/168.68 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.05/168.68 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.05/168.68 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.05/168.68 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.05/168.68 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.05/168.68 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.05/168.68 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.05/168.68 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.68 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.05/168.68 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.05/168.68 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.05/168.68 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.05/168.68 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.05/168.68 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.05/168.68 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.05/168.68 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.05/168.68 Splitting Processor: 668.05/168.68 strict: 668.05/168.68 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.05/168.68 weak: 668.05/168.68 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.05/168.68 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.05/168.68 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.68 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.05/168.68 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.05/168.68 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.05/168.68 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.05/168.68 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.05/168.68 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.05/168.68 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.05/168.68 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.05/168.68 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.05/168.68 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.68 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.05/168.68 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.05/168.68 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.05/168.68 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.05/168.68 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.05/168.68 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.05/168.68 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.05/168.68 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.05/168.68 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.05/168.68 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.05/168.68 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.05/168.68 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.05/168.68 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.05/168.68 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.05/168.68 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.05/168.68 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.05/168.68 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.05/168.68 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.05/168.68 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.05/168.68 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.05/168.68 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.05/168.68 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.05/168.68 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.05/168.68 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.05/168.68 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.05/168.68 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.05/168.68 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.05/168.68 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.05/168.68 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.05/168.68 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.05/168.68 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.05/168.68 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.05/168.68 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.05/168.68 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.05/168.68 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.05/168.68 Matrix Interpretation Processor: dim=5 668.05/168.68 668.05/168.68 max_matrix: 668.05/168.68 [1 0 1 0 0] 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [0 0 0 1 0] 668.05/168.68 [0 0 0 0 1] 668.05/168.68 [0 0 0 0 0] 668.05/168.68 interpretation: 668.05/168.68 [1 0 0 0 0] 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [5](x0) = [0 0 0 0 0]x0 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [0 0 0 0 0] , 668.05/168.68 668.05/168.68 [1 0 0 0 0] 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [4](x0) = [0 0 0 0 0]x0 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [0 0 0 0 0] , 668.05/168.68 668.05/168.68 [1 0 0 0 0] [0] 668.05/168.68 [0 0 0 0 0] [1] 668.05/168.68 [3](x0) = [0 0 0 0 0]x0 + [0] 668.05/168.68 [0 0 0 0 0] [0] 668.05/168.68 [0 0 0 0 0] [1], 668.05/168.68 668.05/168.68 [1 0 1 0 0] 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [0](x0) = [0 0 0 0 0]x0 668.05/168.68 [0 0 0 0 1] 668.05/168.68 [0 0 0 0 0] , 668.05/168.68 668.05/168.68 [1 0 1 0 0] 668.05/168.68 [0 0 0 0 0] 668.05/168.68 [1](x0) = [0 0 0 1 0]x0 668.05/168.68 [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] , 668.15/168.70 668.15/168.70 [1 0 1 0 0] 668.15/168.70 [0 0 0 0 0] 668.15/168.70 [2](x0) = [0 0 0 1 0]x0 668.15/168.70 [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] 668.15/168.70 orientation: 668.15/168.70 [1 0 1 0 0] [1] [1 0 1 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 0(1(0(3(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(1(4(3(2(0(x1)))))) 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 0(3(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(1(3(4(4(x1))))) 668.15/168.70 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 0(4(1(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(1(4(4(x1)))) 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 0(4(2(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(3(4(x1)))) 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 0(4(2(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(4(3(x1)))) 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [1 0 1 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 2(3(1(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 1(3(5(2(x1)))) 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [1 0 1 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 2(3(1(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 1(4(3(5(2(x1))))) 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 1 0] [0] [1 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 0(3(1(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(1(4(1(3(4(x1)))))) 668.15/168.70 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 0(5(3(1(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(1(4(3(5(4(x1)))))) 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.70 668.15/168.70 [1 0 1 0 0] [0] [1 0 1 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 2(0(3(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 2(0(1(3(5(2(x1)))))) 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.70 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.72 2(0(4(1(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 2(0(1(4(5(x1))))) 668.15/168.72 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.72 2(5(4(2(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(5(2(4(x1))))) 668.15/168.72 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 1 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 2(0(3(1(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 2(1(0(1(3(4(x1)))))) 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(1(3(x1)))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(3(4(x1)))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(0(2(4(3(x1))))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(1(4(3(x1))))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(4(3(3(x1))))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(1(3(3(4(x1)))))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 668.15/168.72 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.72 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(3(4(5(5(x1)))))) 668.15/168.72 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.72 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [0] [1 0 1 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 0(3(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(4(4(3(4(0(x1)))))) 668.15/168.74 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 1 0] [0] [1 0 1 1 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 0(3(2(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(0(3(4(2(1(x1)))))) 668.15/168.74 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 1 0] [0] [1 0 1 1 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 0(3(2(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 1(3(4(0(2(2(x1)))))) 668.15/168.74 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [1 0 1 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 0(4(3(2(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 2(3(4(4(0(0(x1)))))) 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 0(5(3(2(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(4(5(3(x1))))) 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 0(5(3(2(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(5(3(3(x1))))) 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 2(5(3(2(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 2(5(2(3(3(x1))))) 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 1 0] [1 0 1 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 0(0(3(2(1(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(0(1(3(5(2(x1)))))) 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [1] [1 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 0(1(0(3(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 2(3(1(0(0(5(x1)))))) 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 668.15/168.74 [1 0 1 0 0] [0] [1 0 0 0 0] 668.15/168.74 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.74 0(3(2(5(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(2(5(1(3(3(x1)))))) 668.15/168.74 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(5(3(2(1(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(1(3(4(2(5(x1)))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(5(5(3(2(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(5(1(3(5(x1)))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 1 1 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(1(2(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(0(2(1(x1)))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(1(2(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(1(3(x1)))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(1(2(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(0(2(1(4(4(x1)))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 1 1 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 2(0(1(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 5(0(2(1(x1)))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 1 1 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(2(0(1(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 5(0(0(2(1(x1))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(4(1(2(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 1(4(0(2(5(x1))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(5(1(1(2(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(4(1(1(5(x1)))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 1 0] [1 0 1 1 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 0(5(1(2(2(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(5(2(1(2(x1)))))) 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.76 668.15/168.76 [1 0 1 0 0] [1] [1 0 1 0 0] 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 2(2(0(3(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 1(3(0(2(5(2(x1)))))) 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [1 0 1 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 2(2(0(5(1(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 2(0(2(1(5(1(x1)))))) 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [0] [1 0 1 0 0] 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 0(3(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 0(1(3(4(0(x1))))) 668.15/168.77 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [0] [1 0 1 0 0] 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 0(3(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 1(3(4(4(4(0(x1)))))) 668.15/168.77 [0 0 0 0 0] [1] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 0(4(1(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(1(4(x1)))) 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 0(4(2(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(1(4(x1)))) 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 2(3(1(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(2(1(3(5(x1))))) 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [1 0 1 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 0(5(3(1(x1)))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0(1(5(3(4(0(x1)))))) 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 668.15/168.77 [1 0 1 0 0] [1 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 2(5(5(4(1(x1))))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 [0 0 0 0 0] [0 0 0 0 0] 668.15/168.77 problem: 668.15/168.77 strict: 668.15/168.77 668.15/168.77 weak: 668.15/168.77 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.15/168.77 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.15/168.77 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.15/168.77 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.15/168.77 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.15/168.77 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.15/168.77 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.15/168.77 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.15/168.77 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.15/168.77 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.15/168.77 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.15/168.77 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.15/168.78 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.15/168.78 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.15/168.78 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.15/168.78 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.15/168.78 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.15/168.78 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.15/168.78 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.15/168.78 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.15/168.78 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.15/168.78 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.15/168.78 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.15/168.78 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.15/168.78 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.15/168.78 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.15/168.78 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.15/168.78 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.15/168.78 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.15/168.78 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.15/168.78 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.15/168.78 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.15/168.78 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.15/168.78 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.15/168.78 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.15/168.78 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.15/168.78 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.15/168.78 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.15/168.78 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.15/168.78 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.15/168.78 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.15/168.78 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.15/168.78 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.15/168.78 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.15/168.78 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.15/168.78 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.15/168.78 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.15/168.78 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.15/168.78 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.15/168.78 Qed 668.15/168.78 668.15/168.78 strict: 668.15/168.78 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.15/168.78 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.15/168.78 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.15/168.78 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.15/168.78 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.15/168.78 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.15/168.78 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.15/168.78 weak: 668.15/168.78 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.15/168.78 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.15/168.78 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.15/168.78 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.15/168.78 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.15/168.78 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.15/168.78 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.15/168.78 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.15/168.78 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.15/168.78 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.15/168.78 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.15/168.78 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.15/168.78 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.15/168.78 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.15/168.78 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.15/168.78 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.15/168.78 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.15/168.78 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.15/168.78 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.15/168.78 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.15/168.78 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.15/168.78 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.15/168.78 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.15/168.78 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.15/168.78 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.15/168.78 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.15/168.78 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.15/168.78 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.15/168.78 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.15/168.78 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.15/168.78 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.15/168.78 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.15/168.78 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.15/168.78 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.15/168.78 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.15/168.78 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.15/168.78 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.15/168.78 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.15/168.78 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.15/168.78 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.15/168.78 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.15/168.78 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.15/168.78 Splitting Processor: 668.15/168.78 strict: 668.15/168.78 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.15/168.78 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.15/168.78 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.15/168.78 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.15/168.78 weak: 668.15/168.78 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.15/168.79 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.15/168.79 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.15/168.79 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.15/168.79 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.15/168.79 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.15/168.79 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.15/168.79 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.15/168.79 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.15/168.79 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.15/168.79 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.15/168.79 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.15/168.79 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.15/168.79 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.15/168.79 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.15/168.79 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.15/168.79 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.15/168.79 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.15/168.79 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.15/168.79 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.15/168.79 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.15/168.79 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.15/168.79 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.15/168.79 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.15/168.79 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.15/168.79 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.15/168.79 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.15/168.79 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.15/168.79 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.15/168.79 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.15/168.79 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.15/168.79 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.15/168.79 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.15/168.79 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.15/168.79 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.15/168.79 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.15/168.79 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.15/168.79 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.15/168.79 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.15/168.79 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.15/168.79 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.15/168.79 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.15/168.79 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.15/168.79 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.15/168.79 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.15/168.79 Matrix Interpretation Processor: dim=5 668.15/168.79 668.15/168.79 max_matrix: 668.15/168.79 [1 1 1 1 0] 668.15/168.79 [0 0 1 1 0] 668.15/168.79 [0 0 0 1 1] 668.15/168.79 [0 0 0 0 1] 668.15/168.79 [0 0 0 0 0] 668.15/168.79 interpretation: 668.15/168.79 [1 0 0 0 0] 668.15/168.79 [0 0 0 1 0] 668.15/168.79 [5](x0) = [0 0 0 0 0]x0 668.15/168.79 [0 0 0 0 0] 668.15/168.79 [0 0 0 0 0] , 668.15/168.79 668.15/168.79 [1 0 0 0 0] 668.15/168.79 [0 0 0 0 0] 668.15/168.79 [4](x0) = [0 0 0 0 0]x0 668.15/168.79 [0 0 0 0 0] 668.15/168.79 [0 0 0 0 0] , 668.15/168.79 668.15/168.79 [1 1 0 0 0] 668.15/168.79 [0 0 1 0 0] 668.15/168.79 [3](x0) = [0 0 0 0 0]x0 668.15/168.79 [0 0 0 0 1] 668.15/168.79 [0 0 0 0 0] , 668.15/168.79 668.15/168.79 [1 1 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [0] 668.15/168.79 [0](x0) = [0 0 0 1 0]x0 + [0] 668.15/168.79 [0 0 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [1], 668.15/168.79 668.15/168.79 [1 1 1 0 0] [0] 668.15/168.79 [0 0 0 1 0] [0] 668.15/168.79 [1](x0) = [0 0 0 0 0]x0 + [0] 668.15/168.79 [0 0 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [1], 668.15/168.79 668.15/168.79 [1 1 0 1 0] [0] 668.15/168.79 [0 0 1 0 0] [0] 668.15/168.79 [2](x0) = [0 0 0 0 1]x0 + [0] 668.15/168.79 [0 0 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [1] 668.15/168.79 orientation: 668.15/168.79 [1 1 1 1 0] [0] [1 1 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.15/168.79 0(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(1(3(4(0(x1))))) 668.15/168.79 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.15/168.79 668.15/168.79 [1 1 1 1 0] [0] [1 1 0 0 0] [0] 668.15/168.79 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.15/168.79 0(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 1(3(4(4(4(0(x1)))))) 668.15/168.79 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.80 668.25/168.80 [1 1 1 1 0] [1] [1 1 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 0(5(3(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(5(3(4(0(x1)))))) 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.80 668.25/168.80 [1 1 1 0 0] [0] [1 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 0(4(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.80 668.25/168.80 [1 1 0 1 0] [0] [1 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 0(4(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.80 668.25/168.80 [1 1 1 1 0] [1] [1 0 0 1 0] [0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 2(3(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(1(3(5(x1))))) 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.80 668.25/168.80 [1 1 1 0 0] [0] [1 0 0 0 0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] 668.25/168.80 2(5(5(4(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] 668.25/168.80 668.25/168.80 [1 1 1 1 1] [1] [1 1 0 1 0] [0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 0(1(0(3(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(4(3(2(0(x1)))))) 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.80 668.25/168.80 [1 1 1 1 0] [0] [1 0 0 0 0] [0] 668.25/168.80 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.80 0(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(1(3(4(4(x1))))) 668.25/168.81 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.81 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.81 668.25/168.81 [1 1 1 0 0] [0] [1 0 0 0 0] [0] 668.25/168.81 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.81 0(4(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(4(4(x1)))) 668.25/168.81 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.81 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.81 668.25/168.81 [1 1 0 1 0] [0] [1 0 0 0 0] [0] 668.25/168.81 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.81 0(4(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.25/168.81 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.81 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 0 1 0] [0] [1 1 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 0(4(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(4(3(x1)))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 1 0] [1] [1 1 0 1 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 2(3(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(3(5(2(x1)))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 1 0] [1] [1 1 0 1 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 2(3(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(4(3(5(2(x1))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 1 0] [0] [1 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 0(3(1(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(1(4(1(3(4(x1)))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 1 0] [1] [1 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 0(5(3(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(4(3(5(4(x1)))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 1 0] [0] [1 1 0 1 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.25/168.82 2(0(3(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 0 0] [0] [1 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 2(0(4(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 0 1 0] [0] [1 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 2(5(4(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(5(2(4(x1))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.82 668.25/168.82 [1 1 1 1 0] [0] [1 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.25/168.82 2(0(3(1(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.25/168.82 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.82 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 1 1 0 1] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 1 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(0(2(4(3(x1))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 1 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(1(4(3(x1))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 1 1 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(4(3(3(x1))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(1(3(3(4(x1)))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(3(4(5(5(x1)))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [0] [1 1 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 2(4(4(3(4(0(x1)))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 0] [1] [1 1 1 1 0] [0] 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 0(3(2(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(0(3(4(2(1(x1)))))) 668.25/168.84 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.84 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.84 668.25/168.84 [1 1 1 1 1] [1] [1 1 1 1 1] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(3(2(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 1(3(4(0(2(2(x1)))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 0] [0] [1 1 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(4(3(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(3(4(4(0(0(x1)))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 0] [1] [1 1 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(5(3(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(4(5(3(x1))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 0] [1] [1 1 1 0 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(5(3(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(5(3(3(x1))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 0] [1] [1 1 1 0 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 2(5(3(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(5(2(3(3(x1))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 0] [1] [1 1 0 1 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(0(3(2(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(0(1(3(5(2(x1)))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 1] [1] [1 0 0 1 0] [1] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(1(0(3(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(3(1(0(0(5(x1)))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 0 0] [0] [1 1 1 0 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(3(2(5(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(2(5(1(3(3(x1)))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.86 668.25/168.86 [1 1 1 1 0] [1] [1 0 0 1 0] [0] 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 0(5(3(2(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(1(3(4(2(5(x1)))))) 668.25/168.86 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.86 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 0] [0] [1 0 0 1 0] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(5(5(3(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(5(1(3(5(x1)))))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 1] [0] [1 1 1 1 0] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(1(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(0(2(1(x1)))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 1] [0] [1 1 1 0 1] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(1(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 1] [0] [1 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(1(2(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(0(2(1(4(4(x1)))))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 0] [0] [1 1 1 1 0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] 668.25/168.88 2(0(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 5(0(2(1(x1)))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] 668.25/168.88 668.25/168.88 [1 1 1 1 0] [0] [1 1 1 1 0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] 668.25/168.88 0(2(0(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 5(0(0(2(1(x1))))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] 668.25/168.88 668.25/168.88 [1 1 1 1 1] [0] [1 0 0 1 0] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(4(1(2(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(4(0(2(5(x1))))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 1] [0] [1 0 0 1 0] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(5(1(1(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(4(1(1(5(x1)))))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.88 668.25/168.88 [1 1 1 1 1] [1] [1 1 1 1 1] [0] 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 0(5(1(2(2(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(2(5(2(1(2(x1)))))) 668.25/168.88 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.88 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.89 668.25/168.89 [1 1 1 1 0] [1] [1 1 0 1 0] [0] 668.25/168.89 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.89 2(2(0(3(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 1(3(0(2(5(2(x1)))))) 668.25/168.89 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.89 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.89 668.25/168.89 [1 1 1 0 0] [0] [1 1 1 0 0] [0] 668.25/168.89 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.25/168.89 2(2(0(5(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.25/168.89 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.25/168.89 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 668.25/168.89 problem: 668.25/168.89 strict: 668.25/168.89 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.25/168.89 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.25/168.89 weak: 668.25/168.89 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.25/168.89 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.25/168.89 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.25/168.89 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.25/168.89 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.25/168.89 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.25/168.89 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.25/168.89 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.25/168.89 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.25/168.89 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.25/168.89 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.25/168.89 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.25/168.89 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.25/168.89 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.25/168.89 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.25/168.89 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.25/168.89 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.25/168.89 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.25/168.89 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.25/168.89 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.25/168.89 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.25/168.89 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.25/168.89 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.25/168.89 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.25/168.89 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.25/168.89 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.25/168.89 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.25/168.89 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.25/168.89 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.25/168.89 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.25/168.89 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.25/168.89 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.25/168.89 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.25/168.89 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.25/168.89 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.25/168.89 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.25/168.89 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.25/168.89 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.25/168.89 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.25/168.89 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.25/168.89 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.25/168.89 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.25/168.89 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.25/168.89 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.25/168.89 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.25/168.89 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.25/168.89 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.25/168.89 Matrix Interpretation Processor: dim=3 668.25/168.89 668.25/168.89 max_matrix: 668.25/168.89 [1 2 1] 668.25/168.89 [0 0 1] 668.25/168.89 [0 0 0] 668.25/168.89 interpretation: 668.25/168.89 [1 0 0] 668.25/168.89 [5](x0) = [0 0 0]x0 668.25/168.89 [0 0 0] , 668.25/168.89 668.25/168.89 [1 1 0] 668.25/168.89 [4](x0) = [0 0 0]x0 668.25/168.89 [0 0 0] , 668.25/168.89 668.25/168.89 [1 1 1] 668.25/168.89 [3](x0) = [0 0 0]x0 668.25/168.89 [0 0 0] , 668.25/168.89 668.25/168.89 [1 0 0] [0] 668.25/168.89 [0](x0) = [0 0 0]x0 + [0] 668.25/168.89 [0 0 0] [1], 668.25/168.89 668.25/168.89 [1 2 1] [0] 668.25/168.89 [1](x0) = [0 0 0]x0 + [0] 668.25/168.89 [0 0 0] [1], 668.25/168.89 668.25/168.89 [1 2 0] [0] 668.25/168.89 [2](x0) = [0 0 1]x0 + [0] 668.25/168.89 [0 0 0] [1] 668.35/168.90 orientation: 668.35/168.90 [1 2 1] [1] [1 0 0] [0] 668.35/168.90 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(0(x1))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 0 0] [0] 668.35/168.90 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(4(4(4(0(x1)))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 0 0] [0] 668.35/168.90 0(5(3(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(5(3(4(0(x1)))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [0] [1 1 0] [0] 668.35/168.90 0(4(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [0] [1 1 0] [0] 668.35/168.90 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 0 0] [0] 668.35/168.90 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(5(x1))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [0] [1 1 0] 668.35/168.90 2(5(5(4(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.35/168.90 [0 0 0] [1] [0 0 0] 668.35/168.90 668.35/168.90 [1 2 1] [2] [1 0 0] [2] 668.35/168.90 0(1(0(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(3(2(0(x1)))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 1 0] [0] 668.35/168.90 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(4(x1))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [0] [1 1 0] [0] 668.35/168.90 0(4(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(4(x1)))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [0] [1 1 0] [0] 668.35/168.90 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [0] [1 1 1] [0] 668.35/168.90 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(3(x1)))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 2 0] [0] 668.35/168.90 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(5(2(x1)))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 2 0] [0] 668.35/168.90 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(3(5(2(x1))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [2] [1 1 0] [0] 668.35/168.90 0(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(1(3(4(x1)))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 1 0] [0] 668.35/168.90 0(5(3(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(3(5(4(x1)))))) 668.35/168.90 [0 0 0] [1] [0 0 0] [1] 668.35/168.90 668.35/168.90 [1 2 1] [1] [1 2 0] [0] 668.35/168.91 2(0(3(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [0] [1 0 0] [0] 668.35/168.91 2(0(4(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [0] [1 1 0] [0] 668.35/168.91 2(5(4(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(2(4(x1))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [2] [1 1 0] [1] 668.35/168.91 2(0(3(1(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 1] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 0] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 1] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(4(3(x1))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 1] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(3(x1))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 1] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(3(3(x1))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 0] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(3(4(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 0 0] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(5(5(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 0 0] [0] 668.35/168.91 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(4(4(3(4(0(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [2] [1 2 1] [1] 668.35/168.91 0(3(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(3(4(2(1(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 2] [2] [1 2 2] [0] 668.35/168.91 0(3(2(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(4(0(2(2(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 0 0] [0] 668.35/168.91 0(4(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(4(4(0(0(x1)))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 1] [0] 668.35/168.91 0(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(5(3(x1))))) 668.35/168.91 [0 0 0] [1] [0 0 0] [1] 668.35/168.91 668.35/168.91 [1 2 1] [1] [1 1 1] [0] 668.35/168.92 0(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(3(3(x1))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [1] [1 1 1] [0] 668.35/168.92 2(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(5(2(3(3(x1))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [2] [1 2 0] [0] 668.35/168.92 0(0(3(2(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(1(3(5(2(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [2] [1 0 0] [2] 668.35/168.92 0(1(0(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(1(0(0(5(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [1] [1 1 1] [0] 668.35/168.92 0(3(2(5(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(1(3(3(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [2] [1 0 0] [0] 668.35/168.92 0(5(3(2(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(2(5(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [1] [1 0 0] [0] 668.35/168.92 0(5(5(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(1(3(5(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 2] [1] [1 2 1] [0] 668.35/168.92 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(x1)))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 2] [1] [1 1 1] [0] 668.35/168.92 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 2] [1] [1 1 0] [0] 668.35/168.92 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(4(4(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [0] [1 2 1] 668.35/168.92 2(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(2(1(x1)))) 668.35/168.92 [0 0 0] [1] [0 0 0] 668.35/168.92 668.35/168.92 [1 2 1] [0] [1 2 1] 668.35/168.92 0(2(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(0(2(1(x1))))) 668.35/168.92 [0 0 0] [1] [0 0 0] 668.35/168.92 668.35/168.92 [1 2 2] [1] [1 0 0] [0] 668.35/168.92 0(4(1(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(2(5(x1))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 2] [2] [1 0 0] [1] 668.35/168.92 0(5(1(1(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(1(1(5(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 2] [3] [1 2 2] [1] 668.35/168.92 0(5(1(2(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(2(1(2(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.92 668.35/168.92 [1 2 1] [3] [1 2 0] [1] 668.35/168.92 2(2(0(3(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(2(5(2(x1)))))) 668.35/168.92 [0 0 0] [1] [0 0 0] [1] 668.35/168.93 668.35/168.93 [1 2 1] [2] [1 2 1] [0] 668.35/168.93 2(2(0(5(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.35/168.93 [0 0 0] [1] [0 0 0] [1] 668.35/168.93 problem: 668.35/168.93 strict: 668.35/168.93 668.35/168.93 weak: 668.35/168.93 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.35/168.93 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.35/168.93 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.35/168.93 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.35/168.93 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.35/168.93 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.35/168.93 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.35/168.93 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.35/168.93 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.35/168.93 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.35/168.93 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.35/168.93 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.35/168.93 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.35/168.93 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.35/168.93 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.35/168.93 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.35/168.93 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.35/168.93 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.35/168.93 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.35/168.93 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.35/168.93 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.35/168.93 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.35/168.93 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.35/168.93 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.35/168.93 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.35/168.93 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.35/168.93 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.35/168.93 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.35/168.93 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.35/168.93 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.35/168.93 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.35/168.93 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.35/168.93 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.35/168.93 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.35/168.93 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.35/168.93 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.35/168.93 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.35/168.93 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.35/168.93 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.35/168.93 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.35/168.93 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.35/168.93 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.35/168.93 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.35/168.93 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.35/168.93 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.35/168.93 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.35/168.93 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.35/168.93 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.35/168.93 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.35/168.93 Qed 668.35/168.93 668.35/168.93 strict: 668.35/168.93 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.35/168.93 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.35/168.93 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.35/168.93 weak: 668.35/168.93 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.35/168.93 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.35/168.93 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.35/168.93 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.35/168.93 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.35/168.93 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.35/168.93 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.35/168.93 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.35/168.93 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.35/168.93 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.35/168.93 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.35/168.93 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.35/168.93 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.35/168.93 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.35/168.93 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.35/168.93 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.35/168.93 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.35/168.93 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.35/168.93 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.35/168.93 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.35/168.93 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.35/168.93 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.35/168.93 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.35/168.93 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.35/168.93 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.35/168.93 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.35/168.93 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.35/168.93 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.35/168.93 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.35/168.94 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.35/168.94 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.35/168.94 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.35/168.94 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.35/168.94 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.35/168.94 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.35/168.94 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.35/168.94 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.35/168.94 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.35/168.94 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.35/168.94 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.35/168.94 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.35/168.94 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.35/168.94 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.35/168.94 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.35/168.94 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.35/168.94 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.35/168.94 Matrix Interpretation Processor: dim=5 668.35/168.94 668.35/168.94 max_matrix: 668.35/168.94 [1 0 1 1 0] 668.35/168.94 [0 0 0 0 1] 668.35/168.94 [0 0 0 1 1] 668.35/168.94 [0 0 0 0 1] 668.35/168.94 [0 0 0 0 0] 668.35/168.94 interpretation: 668.35/168.94 [1 0 0 1 0] 668.35/168.94 [0 0 0 0 0] 668.35/168.94 [5](x0) = [0 0 0 0 0]x0 668.35/168.94 [0 0 0 0 1] 668.35/168.94 [0 0 0 0 0] , 668.35/168.94 668.35/168.94 [1 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [1] 668.35/168.94 [4](x0) = [0 0 0 0 0]x0 + [0] 668.35/168.94 [0 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [1], 668.35/168.94 668.35/168.94 [1 0 1 0 0] [0] 668.35/168.94 [0 0 0 0 0] [1] 668.35/168.94 [3](x0) = [0 0 0 0 0]x0 + [0] 668.35/168.94 [0 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [1], 668.35/168.94 668.35/168.94 [1 0 0 1 0] [0] 668.35/168.94 [0 0 0 0 1] [0] 668.35/168.94 [0](x0) = [0 0 0 0 0]x0 + [1] 668.35/168.94 [0 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [0], 668.35/168.94 668.35/168.94 [1 0 1 1 0] 668.35/168.94 [0 0 0 0 0] 668.35/168.94 [1](x0) = [0 0 0 0 0]x0 668.35/168.94 [0 0 0 0 0] 668.35/168.94 [0 0 0 0 0] , 668.35/168.94 668.35/168.94 [1 0 1 0 0] 668.35/168.94 [0 0 0 0 0] 668.35/168.94 [2](x0) = [0 0 0 1 1]x0 668.35/168.94 [0 0 0 0 0] 668.35/168.94 [0 0 0 0 0] 668.35/168.94 orientation: 668.35/168.94 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.94 0(4(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(4(x1)))) 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 668.35/168.94 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.94 0(4(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(4(x1)))) 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 668.35/168.94 [1 0 1 1 0] [0] [1 0 0 1 0] [0] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 2(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(3(5(x1))))) 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 668.35/168.94 [1 0 1 1 0] [1] [1 0 0 0 0] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.94 2(5(5(4(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.94 668.35/168.94 [1 0 1 1 1] [1] [1 0 0 1 0] [1] 668.35/168.94 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.94 0(1(0(3(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(4(3(2(0(x1)))))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.96 0(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(3(4(4(x1))))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.96 0(4(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(4(4(x1)))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.96 0(4(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(3(4(x1)))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 0 0] [0] [1 0 1 0 0] [0] 668.35/168.96 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.96 0(4(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(4(3(x1)))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [0] [1 0 1 0 0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.96 2(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(3(5(2(x1)))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [0] [1 0 1 0 0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.96 2(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(4(3(5(2(x1))))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [0] [1 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.96 0(3(1(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(4(1(3(4(x1)))))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [1] [1 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 0(5(3(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(4(3(5(4(x1)))))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 668.35/168.96 [1 0 1 1 0] [1] [1 0 1 0 0] [1] 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.96 2(0(3(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(0(1(3(5(2(x1)))))) 668.35/168.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 0] [1] [1 0 0 1 0] [1] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 2(0(4(1(x1)))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(0(1(4(5(x1))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 0 0] [0] [1 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 2(5(4(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(5(2(4(x1))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 0] [1] [1 0 0 0 0] [1] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 2(0(3(1(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(1(0(1(3(4(x1)))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 1] [0] [1 0 1 0 0] [0] 668.35/168.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.97 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(3(x1)))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 1] [0] [1 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.97 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(3(4(x1)))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 1] [0] [1 0 1 0 0] [0] 668.35/168.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.97 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(0(2(4(3(x1))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 1] [0] [1 0 1 0 0] [0] 668.35/168.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.97 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(4(3(x1))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 1] [0] [1 0 1 0 0] [0] 668.35/168.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.97 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(4(3(3(x1))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 668.35/168.97 [1 0 1 1 1] [0] [1 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.97 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(3(3(4(x1)))))) 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.97 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [0] [1 0 0 1 1] [0] 668.35/168.99 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.99 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(3(4(5(5(x1)))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [0] [1 0 0 1 0] [0] 668.35/168.99 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.99 0(3(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(4(4(3(4(0(x1)))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 0] [0] [1 0 1 1 0] [0] 668.35/168.99 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.99 0(3(2(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(0(3(4(2(1(x1)))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [0] [1 0 1 1 1] 668.35/168.99 [0 0 0 0 0] [1] [0 0 0 0 0] 668.35/168.99 0(3(2(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(3(4(0(2(2(x1)))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [0] [1 0 0 1 0] [0] 668.35/168.99 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.35/168.99 0(4(3(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(3(4(4(0(0(x1)))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [1] [1 0 1 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 0(5(3(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(4(5(3(x1))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [1] [1 0 1 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 0(5(3(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(5(3(3(x1))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 668.35/168.99 [1 0 1 1 1] [0] [1 0 1 0 0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.99 2(5(3(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 2(5(2(3(3(x1))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] 668.35/168.99 668.35/168.99 [1 0 1 1 0] [0] [1 0 1 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 0(0(3(2(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(0(1(3(5(2(x1)))))) 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.35/168.99 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 1] [1] [1 0 0 1 1] [1] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 0(1(0(3(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 2(3(1(0(0(5(x1)))))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 0] [0] [1 0 1 0 0] [0] 668.45/169.01 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.45/169.01 0(3(2(5(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(5(1(3(3(x1)))))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 0] [1] [1 0 0 1 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 0(5(3(2(1(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(3(4(2(5(x1)))))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 1] [1] [1 0 0 1 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 0(5(5(3(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(5(1(3(5(x1)))))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 1] [0] [1 0 1 1 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 0(1(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(0(2(1(x1)))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 1] [0] [1 0 1 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 0(1(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(1(3(x1)))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 1] [0] [1 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 0(1(2(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(0(2(1(4(4(x1)))))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.01 668.45/169.01 [1 0 1 1 0] [1] [1 0 1 1 0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.01 2(0(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 5(0(2(1(x1)))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.01 668.45/169.01 [1 0 1 1 0] [1] [1 0 1 1 0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.01 0(2(0(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 5(0(0(2(1(x1))))) 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.01 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.03 668.45/169.03 [1 0 1 1 1] [0] [1 0 0 1 0] 668.45/169.03 [0 0 0 0 0] [1] [0 0 0 0 0] 668.45/169.03 0(4(1(2(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(4(0(2(5(x1))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.03 668.45/169.03 [1 0 1 1 1] [0] [1 0 0 1 1] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 0(5(1(1(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(4(1(1(5(x1)))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 668.45/169.03 [1 0 1 1 1] [0] [1 0 1 1 1] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 0(5(1(2(2(x1))))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(2(5(2(1(2(x1)))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 668.45/169.03 [1 0 1 1 0] [1] [1 0 1 0 0] [1] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 2(2(0(3(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 1(3(0(2(5(2(x1)))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 668.45/169.03 [1 0 1 1 0] [1] [1 0 1 1 0] [1] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 2(2(0(5(1(x1))))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 2(0(2(1(5(1(x1)))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 668.45/169.03 [1 0 1 1 0] [0] [1 0 0 1 0] [0] 668.45/169.03 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 668.45/169.03 0(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(3(4(0(x1))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 668.45/169.03 [1 0 1 1 0] [0] [1 0 0 1 0] 668.45/169.03 [0 0 0 0 0] [1] [0 0 0 0 0] 668.45/169.03 0(3(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(3(4(4(4(0(x1)))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] 668.45/169.03 668.45/169.03 [1 0 1 1 0] [1] [1 0 0 1 0] [1] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 0(5(3(1(x1)))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 0(1(5(3(4(0(x1)))))) 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 668.45/169.03 problem: 668.45/169.03 strict: 668.45/169.03 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.45/169.03 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.45/169.03 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.45/169.03 weak: 668.45/169.03 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.45/169.03 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.45/169.03 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.45/169.03 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.45/169.03 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.45/169.04 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.45/169.04 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.45/169.04 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.45/169.04 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.45/169.04 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.45/169.04 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.45/169.04 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.45/169.04 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.45/169.04 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.45/169.04 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.45/169.04 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.45/169.04 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.45/169.04 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.45/169.04 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.45/169.04 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.45/169.04 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.45/169.04 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.45/169.04 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.45/169.04 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.45/169.04 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.45/169.04 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.45/169.04 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.45/169.04 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.45/169.04 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.45/169.04 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.45/169.04 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.45/169.04 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.45/169.04 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.45/169.04 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.45/169.04 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.45/169.04 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.45/169.04 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.45/169.04 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.45/169.04 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.45/169.04 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.45/169.04 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.45/169.04 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.45/169.04 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.45/169.04 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.45/169.04 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.45/169.04 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.45/169.04 Matrix Interpretation Processor: dim=3 668.45/169.04 668.45/169.04 max_matrix: 668.45/169.04 [1 2 1] 668.45/169.04 [0 0 1] 668.45/169.04 [0 0 0] 668.45/169.04 interpretation: 668.45/169.04 [1 0 0] 668.45/169.04 [5](x0) = [0 0 0]x0 668.45/169.04 [0 0 0] , 668.45/169.04 668.45/169.04 [1 2 0] 668.45/169.04 [4](x0) = [0 0 0]x0 668.45/169.04 [0 0 0] , 668.45/169.04 668.45/169.04 [1 1 1] 668.45/169.04 [3](x0) = [0 0 0]x0 668.45/169.04 [0 0 0] , 668.45/169.04 668.45/169.04 [1 0 0] [0] 668.45/169.04 [0](x0) = [0 0 0]x0 + [0] 668.45/169.04 [0 0 0] [1], 668.45/169.04 668.45/169.04 [1 2 1] [0] 668.45/169.04 [1](x0) = [0 0 0]x0 + [0] 668.45/169.04 [0 0 0] [1], 668.45/169.04 668.45/169.04 [1 2 0] [0] 668.45/169.04 [2](x0) = [0 0 1]x0 + [0] 668.45/169.04 [0 0 0] [1] 668.45/169.04 orientation: 668.45/169.04 [1 2 1] [0] [1 2 0] [0] 668.45/169.04 0(4(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 2] [0] [1 2 0] [0] 668.45/169.04 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 0 0] [0] 668.45/169.04 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(5(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [0] [1 2 0] 668.45/169.04 2(5(5(4(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.45/169.04 [0 0 0] [1] [0 0 0] 668.45/169.04 668.45/169.04 [1 2 1] [2] [1 0 0] [2] 668.45/169.04 0(1(0(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(3(2(0(x1)))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 2 0] [0] 668.45/169.04 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(4(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [0] [1 2 0] [0] 668.45/169.04 0(4(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(4(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 2] [0] [1 2 0] [0] 668.45/169.04 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 2] [0] [1 1 1] [0] 668.45/169.04 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(3(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 2 0] [0] 668.45/169.04 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(5(2(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 2 0] [0] 668.45/169.04 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(3(5(2(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [2] [1 2 0] [0] 668.45/169.04 0(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(1(3(4(x1)))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 2 0] [0] 668.45/169.04 0(5(3(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(3(5(4(x1)))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 2 0] [0] 668.45/169.04 2(0(3(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [0] [1 0 0] [0] 668.45/169.04 2(0(4(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 2] [0] [1 2 0] [0] 668.45/169.04 2(5(4(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(2(4(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [2] [1 2 0] [1] 668.45/169.04 2(0(3(1(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 1 1] [0] 668.45/169.04 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 2 0] [0] 668.45/169.04 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 1 1] [0] 668.45/169.04 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(4(3(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 1 1] [0] 668.45/169.04 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(3(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.04 668.45/169.04 [1 2 1] [1] [1 1 1] [0] 668.45/169.04 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(3(3(x1))))) 668.45/169.04 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 2 0] [0] 668.45/169.05 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(3(4(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 0 0] [0] 668.45/169.05 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(5(5(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 0 0] [0] 668.45/169.05 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(4(4(3(4(0(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [2] [1 2 1] [2] 668.45/169.05 0(3(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(3(4(2(1(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 2] [2] [1 2 2] [0] 668.45/169.05 0(3(2(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(4(0(2(2(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 0 0] [0] 668.45/169.05 0(4(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(4(4(0(0(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 1 1] [0] 668.45/169.05 0(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(5(3(x1))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 1 1] [0] 668.45/169.05 0(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(3(3(x1))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 1 1] [0] 668.45/169.05 2(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(5(2(3(3(x1))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [2] [1 2 0] [0] 668.45/169.05 0(0(3(2(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(1(3(5(2(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [2] [1 0 0] [2] 668.45/169.05 0(1(0(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(1(0(0(5(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 1 1] [0] 668.45/169.05 0(3(2(5(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(1(3(3(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [2] [1 0 0] [0] 668.45/169.05 0(5(3(2(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(2(5(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 1] [1] [1 0 0] [0] 668.45/169.05 0(5(5(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(1(3(5(x1)))))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 2] [1] [1 2 1] [0] 668.45/169.05 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(x1)))) 668.45/169.05 [0 0 0] [1] [0 0 0] [1] 668.45/169.05 668.45/169.05 [1 2 2] [1] [1 1 1] [0] 668.45/169.06 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 2] [1] [1 2 0] [0] 668.45/169.06 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(4(4(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 1] [0] [1 2 1] 668.45/169.06 2(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(2(1(x1)))) 668.45/169.06 [0 0 0] [1] [0 0 0] 668.45/169.06 668.45/169.06 [1 2 1] [0] [1 2 1] 668.45/169.06 0(2(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(0(2(1(x1))))) 668.45/169.06 [0 0 0] [1] [0 0 0] 668.45/169.06 668.45/169.06 [1 2 2] [1] [1 0 0] [0] 668.45/169.06 0(4(1(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(2(5(x1))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 2] [2] [1 0 0] [1] 668.45/169.06 0(5(1(1(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(1(1(5(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 2] [3] [1 2 2] [1] 668.45/169.06 0(5(1(2(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(2(1(2(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 1] [3] [1 2 0] [1] 668.45/169.06 2(2(0(3(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(2(5(2(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 1] [2] [1 2 1] [0] 668.45/169.06 2(2(0(5(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 1] [1] [1 0 0] [0] 668.45/169.06 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(0(x1))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 1] [1] [1 0 0] [0] 668.45/169.06 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(4(4(4(0(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 668.45/169.06 [1 2 1] [1] [1 0 0] [0] 668.45/169.06 0(5(3(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(5(3(4(0(x1)))))) 668.45/169.06 [0 0 0] [1] [0 0 0] [1] 668.45/169.06 problem: 668.45/169.06 strict: 668.45/169.06 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.45/169.06 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.45/169.06 weak: 668.45/169.06 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.45/169.06 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.45/169.06 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.45/169.06 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.45/169.06 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.45/169.06 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.45/169.06 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.45/169.06 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.45/169.06 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.45/169.06 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.45/169.06 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.45/169.06 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.45/169.06 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.45/169.06 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.45/169.06 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.45/169.06 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.45/169.06 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.45/169.06 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.45/169.06 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.45/169.06 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.45/169.06 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.45/169.07 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.45/169.07 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.45/169.07 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.45/169.07 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.45/169.07 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.45/169.07 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.45/169.07 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.45/169.07 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.45/169.07 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.45/169.07 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.45/169.07 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.45/169.07 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.45/169.07 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.45/169.07 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.45/169.07 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.45/169.07 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.45/169.07 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.45/169.07 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.45/169.07 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.45/169.07 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.45/169.07 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.45/169.07 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.45/169.07 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.45/169.07 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.45/169.07 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.45/169.07 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.45/169.07 Matrix Interpretation Processor: dim=3 668.45/169.07 668.45/169.07 max_matrix: 668.45/169.07 [1 2 1] 668.45/169.07 [0 0 1] 668.45/169.07 [0 0 0] 668.45/169.07 interpretation: 668.45/169.07 [1 0 0] 668.45/169.07 [5](x0) = [0 0 0]x0 668.45/169.07 [0 0 0] , 668.45/169.07 668.45/169.07 [1 1 1] 668.45/169.07 [4](x0) = [0 0 0]x0 668.45/169.07 [0 0 0] , 668.45/169.07 668.45/169.07 [1 1 1] 668.45/169.07 [3](x0) = [0 0 0]x0 668.45/169.07 [0 0 0] , 668.45/169.07 668.45/169.07 [1 0 0] [0] 668.45/169.07 [0](x0) = [0 0 0]x0 + [0] 668.45/169.07 [0 0 0] [1], 668.45/169.07 668.45/169.07 [1 2 1] [0] 668.45/169.07 [1](x0) = [0 0 0]x0 + [0] 668.45/169.07 [0 0 0] [1], 668.45/169.07 668.45/169.07 [1 2 0] [0] 668.45/169.07 [2](x0) = [0 0 1]x0 + [0] 668.45/169.07 [0 0 0] [1] 668.45/169.07 orientation: 668.45/169.07 [1 2 1] [1] [1 1 1] [0] 668.45/169.07 0(4(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.07 668.45/169.07 [1 2 1] [1] [1 1 1] [0] 668.45/169.07 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(x1)))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.07 668.45/169.07 [1 2 1] [1] [1 0 0] [0] 668.45/169.07 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(5(x1))))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.07 668.45/169.07 [1 2 1] [1] [1 1 1] 668.45/169.07 2(5(5(4(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(5(2(1(3(4(x1)))))) 668.45/169.07 [0 0 0] [1] [0 0 0] 668.45/169.07 668.45/169.07 [1 2 1] [2] [1 0 0] [2] 668.45/169.07 0(1(0(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(3(2(0(x1)))))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.07 668.45/169.07 [1 2 1] [1] [1 1 1] [0] 668.45/169.07 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(4(x1))))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.07 668.45/169.07 [1 2 1] [1] [1 1 1] [0] 668.45/169.07 0(4(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(4(x1)))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.07 668.45/169.07 [1 2 1] [1] [1 1 1] [0] 668.45/169.07 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.45/169.07 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(4(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(3(x1)))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 2 0] [0] 668.45/169.08 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(5(2(x1)))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 2 0] [0] 668.45/169.08 2(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(3(5(2(x1))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [2] [1 1 1] [1] 668.45/169.08 0(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(1(3(4(x1)))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(5(3(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(3(5(4(x1)))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 2 0] [0] 668.45/169.08 2(0(3(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(3(5(2(x1)))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 0 0] [0] 668.45/169.08 2(0(4(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(4(5(x1))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 2(5(4(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(2(4(x1))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [2] [1 1 1] [1] 668.45/169.08 2(0(3(1(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(1(0(1(3(4(x1)))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(x1)))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(4(3(x1))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(4(3(x1))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(3(3(x1))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 1 1] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(3(4(x1)))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.08 668.45/169.08 [1 2 1] [1] [1 0 0] [0] 668.45/169.08 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(4(5(5(x1)))))) 668.45/169.08 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 0 0] [1] 668.45/169.09 0(3(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(4(4(3(4(0(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [2] [1 2 1] [2] 668.45/169.09 0(3(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(3(4(2(1(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 2] [2] [1 2 2] [1] 668.45/169.09 0(3(2(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(4(0(2(2(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 0 0] [1] 668.45/169.09 0(4(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(4(4(0(0(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 1 1] [0] 668.45/169.09 0(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(5(3(x1))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 1 1] [0] 668.45/169.09 0(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(3(3(x1))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 1 1] [0] 668.45/169.09 2(5(3(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(5(2(3(3(x1))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [2] [1 2 0] [0] 668.45/169.09 0(0(3(2(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(1(3(5(2(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [2] [1 0 0] [2] 668.45/169.09 0(1(0(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(3(1(0(0(5(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 1 1] [0] 668.45/169.09 0(3(2(5(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(1(3(3(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [2] [1 0 0] [1] 668.45/169.09 0(5(3(2(1(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(2(5(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [1] [1 0 0] [0] 668.45/169.09 0(5(5(3(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(1(3(5(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 2] [1] [1 2 1] [0] 668.45/169.09 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(x1)))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 2] [1] [1 1 1] [0] 668.45/169.09 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(1(3(x1)))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 2] [1] [1 1 1] [0] 668.45/169.09 0(1(2(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(4(4(x1)))))) 668.45/169.09 [0 0 0] [1] [0 0 0] [1] 668.45/169.09 668.45/169.09 [1 2 1] [0] [1 2 1] 668.55/169.10 2(0(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(2(1(x1)))) 668.55/169.10 [0 0 0] [1] [0 0 0] 668.55/169.10 668.55/169.10 [1 2 1] [0] [1 2 1] 668.55/169.10 0(2(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(0(2(1(x1))))) 668.55/169.10 [0 0 0] [1] [0 0 0] 668.55/169.10 668.55/169.10 [1 2 2] [2] [1 0 0] [1] 668.55/169.10 0(4(1(2(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(2(5(x1))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 2] [2] [1 0 0] [2] 668.55/169.10 0(5(1(1(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(4(1(1(5(x1)))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 2] [3] [1 2 2] [1] 668.55/169.10 0(5(1(2(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(5(2(1(2(x1)))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 1] [3] [1 2 0] [1] 668.55/169.10 2(2(0(3(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(2(5(2(x1)))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 1] [2] [1 2 1] [0] 668.55/169.10 2(2(0(5(1(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(2(1(5(1(x1)))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 1] [1] [1 0 0] [1] 668.55/169.10 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(3(4(0(x1))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 1] [1] [1 0 0] [1] 668.55/169.10 0(3(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(4(4(4(0(x1)))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 668.55/169.10 [1 2 1] [1] [1 0 0] [1] 668.55/169.10 0(5(3(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(5(3(4(0(x1)))))) 668.55/169.10 [0 0 0] [1] [0 0 0] [1] 668.55/169.10 problem: 668.55/169.10 strict: 668.55/169.10 668.55/169.10 weak: 668.55/169.10 0(4(1(x1))) -> 0(2(1(4(x1)))) 668.55/169.10 0(4(2(x1))) -> 0(2(1(4(x1)))) 668.55/169.10 2(3(1(x1))) -> 0(2(1(3(5(x1))))) 668.55/169.10 2(5(5(4(1(x1))))) -> 5(5(2(1(3(4(x1)))))) 668.55/169.10 0(1(0(3(2(x1))))) -> 0(1(4(3(2(0(x1)))))) 668.55/169.10 0(3(1(x1))) -> 0(1(3(4(4(x1))))) 668.55/169.10 0(4(1(x1))) -> 0(1(4(4(x1)))) 668.55/169.10 0(4(2(x1))) -> 0(2(3(4(x1)))) 668.55/169.10 0(4(2(x1))) -> 0(2(4(3(x1)))) 668.55/169.10 2(3(1(x1))) -> 1(3(5(2(x1)))) 668.55/169.10 2(3(1(x1))) -> 1(4(3(5(2(x1))))) 668.55/169.10 0(3(1(1(x1)))) -> 0(1(4(1(3(4(x1)))))) 668.55/169.10 0(5(3(1(x1)))) -> 0(1(4(3(5(4(x1)))))) 668.55/169.10 2(0(3(1(x1)))) -> 2(0(1(3(5(2(x1)))))) 668.55/169.10 2(0(4(1(x1)))) -> 2(0(1(4(5(x1))))) 668.55/169.10 2(5(4(2(x1)))) -> 0(2(5(2(4(x1))))) 668.55/169.10 2(0(3(1(1(x1))))) -> 2(1(0(1(3(4(x1)))))) 668.55/169.10 0(3(2(x1))) -> 0(2(1(3(x1)))) 668.55/169.10 0(3(2(x1))) -> 0(2(3(4(x1)))) 668.55/169.10 0(3(2(x1))) -> 0(0(2(4(3(x1))))) 668.55/169.10 0(3(2(x1))) -> 0(2(1(4(3(x1))))) 668.55/169.10 0(3(2(x1))) -> 0(2(4(3(3(x1))))) 668.55/169.10 0(3(2(x1))) -> 0(2(1(3(3(4(x1)))))) 668.55/169.10 0(3(2(x1))) -> 0(2(3(4(5(5(x1)))))) 668.55/169.10 0(3(2(x1))) -> 2(4(4(3(4(0(x1)))))) 668.55/169.10 0(3(2(1(x1)))) -> 0(0(3(4(2(1(x1)))))) 668.55/169.10 0(3(2(2(x1)))) -> 1(3(4(0(2(2(x1)))))) 668.55/169.10 0(4(3(2(x1)))) -> 2(3(4(4(0(0(x1)))))) 668.55/169.10 0(5(3(2(x1)))) -> 0(2(4(5(3(x1))))) 668.55/169.10 0(5(3(2(x1)))) -> 0(2(5(3(3(x1))))) 668.55/169.10 2(5(3(2(x1)))) -> 2(5(2(3(3(x1))))) 668.55/169.10 0(0(3(2(1(x1))))) -> 0(0(1(3(5(2(x1)))))) 668.55/169.10 0(1(0(3(2(x1))))) -> 2(3(1(0(0(5(x1)))))) 668.55/169.10 0(3(2(5(1(x1))))) -> 0(2(5(1(3(3(x1)))))) 668.55/169.10 0(5(3(2(1(x1))))) -> 0(1(3(4(2(5(x1)))))) 668.55/169.10 0(5(5(3(2(x1))))) -> 0(2(5(1(3(5(x1)))))) 668.55/169.10 0(1(2(x1))) -> 0(0(2(1(x1)))) 668.55/169.10 0(1(2(x1))) -> 0(2(1(3(x1)))) 668.55/169.10 0(1(2(x1))) -> 0(0(2(1(4(4(x1)))))) 668.55/169.10 2(0(1(x1))) -> 5(0(2(1(x1)))) 668.55/169.10 0(2(0(1(x1)))) -> 5(0(0(2(1(x1))))) 668.55/169.10 0(4(1(2(x1)))) -> 1(4(0(2(5(x1))))) 668.55/169.10 0(5(1(1(2(x1))))) -> 0(2(4(1(1(5(x1)))))) 668.55/169.10 0(5(1(2(2(x1))))) -> 0(2(5(2(1(2(x1)))))) 668.55/169.10 2(2(0(3(1(x1))))) -> 1(3(0(2(5(2(x1)))))) 668.55/169.10 2(2(0(5(1(x1))))) -> 2(0(2(1(5(1(x1)))))) 668.55/169.10 0(3(1(x1))) -> 0(1(3(4(0(x1))))) 668.55/169.10 0(3(1(x1))) -> 1(3(4(4(4(0(x1)))))) 668.55/169.10 0(5(3(1(x1)))) -> 0(1(5(3(4(0(x1)))))) 668.55/169.10 Qed 668.55/169.10 EOF