YES(?,O(n^4)) 1166.39/296.31 YES(?,O(n^4)) 1166.39/296.32 1166.39/296.32 Problem: 1166.39/296.32 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.39/296.32 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.39/296.32 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.39/296.32 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.39/296.32 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.39/296.32 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.39/296.32 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.39/296.32 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.39/296.32 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.39/296.32 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.39/296.32 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.39/296.32 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.39/296.32 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.39/296.32 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.39/296.32 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.39/296.32 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.39/296.32 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.39/296.32 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.39/296.32 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.39/296.32 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.39/296.32 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.39/296.32 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.39/296.32 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.39/296.32 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.39/296.32 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.39/296.32 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.39/296.32 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.39/296.32 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.39/296.32 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.39/296.32 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.39/296.32 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.39/296.32 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.39/296.32 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.39/296.32 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.39/296.32 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.39/296.32 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.39/296.32 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.39/296.32 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.39/296.32 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.39/296.32 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.39/296.32 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.39/296.32 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.39/296.32 1166.39/296.32 Proof: 1166.39/296.32 Complexity Transformation Processor: 1166.39/296.32 strict: 1166.39/296.32 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.39/296.32 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.39/296.32 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.39/296.32 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.39/296.32 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.39/296.32 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.39/296.32 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.39/296.32 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.39/296.32 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.39/296.32 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.39/296.32 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.39/296.32 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.39/296.32 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.39/296.32 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.39/296.32 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.39/296.32 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.39/296.32 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.39/296.32 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.39/296.32 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.39/296.32 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.39/296.32 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.39/296.32 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.39/296.32 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.39/296.32 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.39/296.32 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.39/296.32 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.39/296.32 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.39/296.32 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.39/296.32 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.39/296.32 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.39/296.32 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.39/296.32 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.39/296.32 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.39/296.32 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.39/296.32 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.39/296.32 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.39/296.32 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.39/296.32 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.39/296.32 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.39/296.32 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.39/296.32 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.39/296.32 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.39/296.32 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.39/296.32 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.39/296.32 weak: 1166.39/296.32 1166.39/296.32 Matrix Interpretation Processor: dim=3 1166.39/296.32 1166.39/296.32 max_matrix: 1166.39/296.32 [1 1 0] 1166.39/296.32 [0 1 1] 1166.39/296.32 [0 0 1] 1166.39/296.32 interpretation: 1166.39/296.32 [1 1 0] 1166.39/296.32 [5](x0) = [0 0 0]x0 1166.39/296.32 [0 0 1] , 1166.39/296.33 1166.39/296.33 [1 0 0] 1166.39/296.33 [4](x0) = [0 0 0]x0 1166.39/296.33 [0 0 0] , 1166.39/296.33 1166.39/296.33 [1 0 0] 1166.39/296.33 [2](x0) = [0 0 0]x0 1166.39/296.33 [0 0 0] , 1166.39/296.33 1166.39/296.33 [1 0 0] 1166.39/296.33 [3](x0) = [0 1 1]x0 1166.39/296.33 [0 0 1] , 1166.39/296.33 1166.39/296.33 1166.39/296.33 [0](x0) = x0 1166.39/296.33 , 1166.39/296.33 1166.39/296.33 [1 0 0] [0] 1166.39/296.33 [1](x0) = [0 1 0]x0 + [0] 1166.39/296.33 [0 0 0] [1] 1166.39/296.33 orientation: 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(0(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(0(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(0(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(0(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(1(0(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] [0] 1166.39/296.33 0(1(0(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] [1] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(1(0(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] [0] 1166.39/296.33 0(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] [1] 1166.39/296.33 1166.39/296.33 [1 0 0] [0] [1 0 0] 1166.39/296.33 0(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(1(x1)))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] [0] 1166.39/296.33 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(5(4(4(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] [1] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.33 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.39/296.33 [0 0 0] [1] [0 0 0] 1166.39/296.33 1166.39/296.33 [1 1 0] [0] [1 0 0] 1166.39/296.34 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] [0] 1166.39/296.34 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] [0] 1166.39/296.34 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 1 0] 1166.39/296.34 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] [0] 1166.39/296.34 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] 1166.39/296.34 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] [0] 1166.39/296.34 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] [0] 1166.39/296.34 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] 1166.39/296.34 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] 1166.39/296.34 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 0 0] [0] [1 0 0] 1166.39/296.34 0(1(3(0(x1)))) = [0 1 1]x1 + [0] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 1 0] 1166.39/296.34 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] 1166.39/296.34 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 0 0] [0] [1 0 0] 1166.39/296.34 0(3(0(1(x1)))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 0 0] [0] [1 0 0] 1166.39/296.34 0(3(1(0(x1)))) = [0 1 0]x1 + [1] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 0 0] [0] [1 0 0] [0] 1166.39/296.34 0(3(1(1(x1)))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [0] = 5(1(1(0(3(4(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 1 0] [0] [1 0 0] 1166.39/296.34 5(0(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] 1166.39/296.34 1166.39/296.34 [1 0 0] [0] [1 0 0] [0] 1166.39/296.34 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.39/296.34 [0 0 0] [1] [0 0 0] [1] 1166.39/296.34 1166.39/296.34 [1 0 0] [0] [1 0 0] 1166.39/296.34 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] 1166.39/296.35 1166.39/296.35 [1 0 0] [0] [1 0 0] [0] 1166.39/296.35 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 0 0] [0] [1 0 0] 1166.39/296.35 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] 1166.39/296.35 1166.39/296.35 [1 1 0] [0] [1 1 0] 1166.39/296.35 5(1(5(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(5(1(x1))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] 1166.39/296.35 1166.39/296.35 [1 1 0] [1] [1 0 0] [0] 1166.39/296.35 5(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(5(2(3(x1))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [1] [1 1 0] [0] 1166.39/296.35 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [1] [1 0 0] [0] 1166.39/296.35 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [1] [1 0 0] 1166.39/296.35 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] 1166.39/296.35 1166.39/296.35 [1 1 0] [1] [1 1 0] [0] 1166.39/296.35 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [1] [1 0 0] [0] 1166.39/296.35 5(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [0] [1 0 0] [0] 1166.39/296.35 0(1(2(5(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 0 0] [0] [1 0 0] [0] 1166.39/296.35 0(1(4(2(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [0] [1 0 0] 1166.39/296.35 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] 1166.39/296.35 1166.39/296.35 [1 0 0] [0] [1 0 0] [0] 1166.39/296.35 5(0(1(4(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] [1] 1166.39/296.35 1166.39/296.35 [1 1 0] [0] [1 0 0] 1166.39/296.35 5(5(1(0(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.39/296.35 [0 0 0] [1] [0 0 0] 1166.39/296.35 problem: 1166.39/296.35 strict: 1166.39/296.35 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.39/296.35 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.39/296.35 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.39/296.35 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.39/296.35 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.39/296.35 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.39/296.35 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.39/296.35 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.39/296.35 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.39/296.35 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.39/296.35 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.39/296.35 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.39/296.35 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.39/296.35 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.39/296.35 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.39/296.35 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.39/296.35 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.39/296.35 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.39/296.36 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.39/296.36 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.39/296.36 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.39/296.36 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.39/296.36 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.39/296.36 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.39/296.36 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.39/296.36 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.39/296.36 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.39/296.36 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.39/296.36 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.39/296.36 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.39/296.36 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.39/296.36 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.39/296.36 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.39/296.36 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.39/296.36 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.39/296.36 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.39/296.36 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.39/296.36 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.39/296.36 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.39/296.36 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.39/296.36 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.39/296.36 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.39/296.36 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.39/296.36 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.39/296.36 weak: 1166.39/296.36 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.39/296.36 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.39/296.36 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.39/296.36 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.39/296.36 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.39/296.36 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.39/296.36 Matrix Interpretation Processor: dim=3 1166.39/296.36 1166.39/296.36 max_matrix: 1166.39/296.36 [1 1 0] 1166.39/296.36 [0 1 1] 1166.39/296.36 [0 0 1] 1166.39/296.36 interpretation: 1166.39/296.36 [1 1 0] 1166.39/296.36 [5](x0) = [0 0 1]x0 1166.39/296.36 [0 0 1] , 1166.39/296.36 1166.39/296.36 [1 0 0] 1166.39/296.36 [4](x0) = [0 0 0]x0 1166.39/296.36 [0 0 0] , 1166.39/296.36 1166.39/296.36 [1 0 0] 1166.39/296.36 [2](x0) = [0 1 0]x0 1166.39/296.36 [0 0 0] , 1166.39/296.36 1166.39/296.36 [1 0 0] 1166.39/296.36 [3](x0) = [0 0 0]x0 1166.39/296.36 [0 0 1] , 1166.39/296.36 1166.39/296.36 [1 0 0] 1166.39/296.36 [0](x0) = [0 1 1]x0 1166.39/296.36 [0 0 1] , 1166.39/296.36 1166.39/296.36 [1 1 0] [0] 1166.39/296.36 [1](x0) = [0 0 0]x0 + [0] 1166.39/296.36 [0 0 1] [1] 1166.39/296.36 orientation: 1166.39/296.36 [1 1 0] [0] [1 1 0] 1166.39/296.36 0(0(1(x1))) = [0 0 2]x1 + [2] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 0] [0] [1 1 0] 1166.39/296.36 0(0(1(x1))) = [0 0 2]x1 + [2] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 0] [0] [1 0 0] 1166.39/296.36 0(0(1(x1))) = [0 0 2]x1 + [2] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 0] [0] [1 1 0] 1166.39/296.36 0(0(1(x1))) = [0 0 2]x1 + [2] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 1] [0] [1 1 0] 1166.39/296.36 0(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 1] [0] [1 0 0] [0] 1166.39/296.36 0(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] [1] 1166.39/296.36 1166.39/296.36 [1 1 1] [0] [1 1 0] 1166.39/296.36 0(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.39/296.36 [0 0 1] [1] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 0] [0] [1 1 0] [0] 1166.39/296.36 0(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.39/296.36 [0 0 1] [2] [0 0 0] [1] 1166.39/296.36 1166.39/296.36 [1 1 0] [0] [1 1 0] 1166.39/296.36 0(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.39/296.36 [0 0 1] [2] [0 0 0] 1166.39/296.36 1166.39/296.36 [1 1 1] [1] [1 1 0] 1166.39/296.36 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(1(x1)))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [1] [1 1 0] 1166.39/296.37 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [1] [1 1 0] 1166.39/296.37 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [1] [1 0 0] [0] 1166.39/296.37 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(4(5(4(4(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] [1] 1166.39/296.37 1166.39/296.37 [1 1 1] [1] [1 0 0] 1166.39/296.37 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [1] [1 1 0] 1166.39/296.37 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [0] [1 1 0] 1166.39/296.37 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [0] [1 1 0] 1166.39/296.37 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [0] [1 1 0] 1166.39/296.37 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 1] [0] [1 0 0] [0] 1166.39/296.37 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] [1] 1166.39/296.37 1166.39/296.37 [1 1 1] [0] [1 0 0] [0] 1166.39/296.37 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] [1] 1166.39/296.37 1166.39/296.37 [1 1 1] [0] [1 1 0] 1166.39/296.37 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 0] [0] [1 0 0] [0] 1166.39/296.37 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.39/296.37 [0 0 1] [2] [0 0 0] [2] 1166.39/296.37 1166.39/296.37 [1 1 0] [0] [1 1 0] 1166.39/296.37 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.39/296.37 [0 0 1] [2] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 0] [0] [1 1 0] [0] 1166.39/296.37 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.39/296.37 [0 0 1] [2] [0 0 0] [1] 1166.39/296.37 1166.39/296.37 [1 1 0] [0] [1 0 0] [0] 1166.39/296.37 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.39/296.37 [0 0 1] [2] [0 0 0] [2] 1166.39/296.37 1166.39/296.37 [1 1 0] [0] [1 1 0] 1166.39/296.37 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.39/296.37 [0 0 1] [2] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 0] [0] [1 0 0] 1166.39/296.37 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.39/296.37 [0 0 1] [2] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 0 0] [0] [1 0 0] 1166.39/296.37 0(1(3(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.39/296.37 [0 0 1] [1] [0 0 0] 1166.39/296.37 1166.39/296.37 [1 1 2] [0] [1 1 1] 1166.39/296.38 0(1(5(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 2] [0] [1 1 1] 1166.39/296.38 0(1(5(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 0] [0] [1 0 0] 1166.39/296.38 0(3(0(1(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 1] [0] [1 1 0] 1166.39/296.38 0(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 0] [0] [1 0 0] [0] 1166.39/296.38 0(3(1(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [2] = 5(1(1(0(3(4(x1)))))) 1166.39/296.38 [0 0 1] [2] [0 0 0] [2] 1166.39/296.38 1166.39/296.38 [1 1 2] [1] [1 0 0] 1166.39/296.38 5(0(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 1] [0] [1 0 0] [0] 1166.39/296.38 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] [1] 1166.39/296.38 1166.39/296.38 [1 1 1] [0] [1 1 0] 1166.39/296.38 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 0 0] [0] [1 0 0] [0] 1166.39/296.38 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] [1] 1166.39/296.38 1166.39/296.38 [1 0 0] [0] [1 0 0] 1166.39/296.38 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 1] [1] [1 1 1] [1] 1166.39/296.38 5(1(5(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 5(4(1(5(1(x1))))) 1166.39/296.38 [0 0 1] [2] [0 0 0] [0] 1166.39/296.38 1166.39/296.38 [1 1 2] [0] [1 0 0] [0] 1166.39/296.38 0(1(2(5(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] [1] 1166.39/296.38 1166.39/296.38 [1 0 0] [0] [1 0 0] [0] 1166.39/296.38 0(1(4(2(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] [1] 1166.39/296.38 1166.39/296.38 [1 1 1] [0] [1 1 1] 1166.39/296.38 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 0 0] [1] [1 0 0] [0] 1166.39/296.38 5(0(1(4(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.39/296.38 [0 0 0] [1] [0 0 0] [1] 1166.39/296.38 1166.39/296.38 [1 1 3] [1] [1 1 1] 1166.39/296.38 5(5(1(0(0(x1))))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] 1166.39/296.38 1166.39/296.38 [1 1 0] [0] [1 0 0] [0] 1166.39/296.38 5(3(0(1(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(5(2(3(x1))))) 1166.39/296.38 [0 0 1] [1] [0 0 0] [1] 1166.39/296.38 1166.39/296.38 [1 1 1] [0] [1 1 1] [0] 1166.39/296.39 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.39/296.39 [0 0 1] [1] [0 0 0] [1] 1166.39/296.39 1166.39/296.39 [1 1 1] [0] [1 0 0] [0] 1166.39/296.39 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.39/296.39 [0 0 1] [1] [0 0 0] [1] 1166.39/296.39 1166.39/296.39 [1 1 1] [0] [1 1 1] 1166.39/296.39 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.39/296.39 [0 0 1] [1] [0 0 0] 1166.39/296.39 1166.39/296.39 [1 1 1] [0] [1 1 0] [0] 1166.39/296.39 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.39/296.39 [0 0 1] [1] [0 0 0] [1] 1166.39/296.39 1166.39/296.39 [1 1 0] [0] [1 0 0] [0] 1166.39/296.39 5(3(1(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.39/296.39 [0 0 1] [2] [0 0 0] [2] 1166.39/296.39 problem: 1166.39/296.39 strict: 1166.39/296.39 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.39/296.39 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.39/296.39 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.39/296.39 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.39/296.39 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.39/296.39 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.39/296.39 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.39/296.39 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.39/296.39 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.39/296.39 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.39/296.39 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.39/296.39 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.39/296.39 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.39/296.39 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.39/296.39 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.39/296.39 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.39/296.39 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.39/296.39 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.39/296.39 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.39/296.39 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.39/296.39 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.39/296.39 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.39/296.39 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.39/296.39 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.39/296.39 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.39/296.39 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.39/296.39 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.39/296.39 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.39/296.39 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.39/296.39 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.39/296.39 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.39/296.39 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.39/296.39 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.39/296.39 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.39/296.39 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.39/296.39 weak: 1166.39/296.39 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.39/296.39 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.39/296.39 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.39/296.39 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.39/296.39 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.39/296.39 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.39/296.39 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.39/296.39 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.39/296.39 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.39/296.39 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.39/296.39 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.39/296.39 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.39/296.39 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.39/296.39 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.39/296.39 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.39/296.39 Matrix Interpretation Processor: dim=3 1166.39/296.39 1166.39/296.39 max_matrix: 1166.39/296.39 [1 1 0] 1166.39/296.39 [0 1 1] 1166.39/296.39 [0 0 1] 1166.39/296.39 interpretation: 1166.39/296.39 [1 1 0] 1166.39/296.39 [5](x0) = [0 0 1]x0 1166.39/296.39 [0 0 1] , 1166.39/296.39 1166.39/296.39 [1 0 0] 1166.39/296.39 [4](x0) = [0 0 0]x0 1166.39/296.39 [0 0 0] , 1166.39/296.39 1166.39/296.39 [1 0 0] 1166.39/296.39 [2](x0) = [0 0 0]x0 1166.39/296.39 [0 0 0] , 1166.39/296.39 1166.39/296.39 [1 0 0] 1166.39/296.39 [3](x0) = [0 1 1]x0 1166.39/296.39 [0 0 1] , 1166.39/296.39 1166.39/296.39 1166.39/296.39 [0](x0) = x0 1166.39/296.39 , 1166.39/296.39 1166.39/296.39 [0] 1166.39/296.39 [1](x0) = x0 + [0] 1166.39/296.39 [1] 1166.39/296.39 orientation: 1166.39/296.39 [0] [1 0 0] 1166.39/296.39 0(0(1(x1))) = x1 + [0] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.39/296.39 [1] [0 0 0] 1166.39/296.39 1166.39/296.39 [0] [1 0 0] 1166.49/296.40 0(0(1(x1))) = x1 + [0] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.49/296.40 [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] 1166.49/296.40 0(0(1(x1))) = x1 + [0] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.49/296.40 [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] 1166.49/296.40 0(0(1(x1))) = x1 + [0] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.49/296.40 [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] 1166.49/296.40 0(1(0(x1))) = x1 + [0] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.49/296.40 [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] [0] 1166.49/296.40 0(1(0(x1))) = x1 + [0] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.49/296.40 [1] [0 0 0] [1] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] 1166.49/296.40 0(1(0(x1))) = x1 + [0] >= [0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.49/296.40 [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] [0] 1166.49/296.40 0(1(1(x1))) = x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.49/296.40 [2] [0 0 0] [1] 1166.49/296.40 1166.49/296.40 [0] [1 0 0] 1166.49/296.40 0(1(1(x1))) = x1 + [0] >= [0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.49/296.40 [2] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] 1166.49/296.40 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.49/296.40 [0 0 1] [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] 1166.49/296.40 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.49/296.40 [0 0 1] [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] 1166.49/296.40 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.49/296.40 [0 0 1] [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] [0] 1166.49/296.40 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.49/296.40 [0 0 1] [1] [0 0 0] [1] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] [0] 1166.49/296.40 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.49/296.40 [0 0 1] [1] [0 0 0] [1] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 1 0] 1166.49/296.40 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.49/296.40 [0 0 1] [1] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] [0] 1166.49/296.40 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.49/296.40 [0 0 1] [2] [0 0 0] [2] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] 1166.49/296.40 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.49/296.40 [0 0 1] [2] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] [0] 1166.49/296.40 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.49/296.40 [0 0 1] [2] [0 0 0] [1] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] [0] 1166.49/296.40 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.49/296.40 [0 0 1] [2] [0 0 0] [2] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] 1166.49/296.40 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.49/296.40 [0 0 1] [2] [0 0 0] 1166.49/296.40 1166.49/296.40 [1 1 0] [0] [1 0 0] 1166.49/296.41 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.49/296.41 [0 0 1] [2] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] 1166.49/296.41 0(1(3(0(x1)))) = [0 1 1]x1 + [0] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 1 0] 1166.49/296.41 0(1(5(0(x1)))) = [0 0 1]x1 + [0] >= [0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 0 0] 1166.49/296.41 0(1(5(0(x1)))) = [0 0 1]x1 + [0] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] 1166.49/296.41 0(3(0(1(x1)))) = [0 1 1]x1 + [1] >= [0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] 1166.49/296.41 0(3(1(0(x1)))) = [0 1 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] [0] 1166.49/296.41 0(3(1(1(x1)))) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [2] = 5(1(1(0(3(4(x1)))))) 1166.49/296.41 [0 0 1] [2] [0 0 0] [2] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] [0] 1166.49/296.41 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] [1] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] 1166.49/296.41 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] [0] 1166.49/296.41 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] [1] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] 1166.49/296.41 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 1] [1] [1 1 0] 1166.49/296.41 5(1(5(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 5(4(1(5(1(x1))))) 1166.49/296.41 [0 0 1] [2] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 0 0] [0] 1166.49/296.41 0(1(2(5(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] [1] 1166.49/296.41 1166.49/296.41 [1 0 0] [0] [1 0 0] [0] 1166.49/296.41 0(1(4(2(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] [1] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 0 0] 1166.49/296.41 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.49/296.41 [0 0 0] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 0 0] 1166.49/296.41 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(1(x1)))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 0 0] 1166.49/296.41 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.49/296.41 [0 0 1] [1] [0 0 0] 1166.49/296.41 1166.49/296.41 [1 1 0] [0] [1 0 0] 1166.49/296.41 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] 1166.49/296.42 1166.49/296.42 [1 1 0] [0] [1 0 0] [0] 1166.49/296.42 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 0(1(4(5(4(4(x1)))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] [1] 1166.49/296.42 1166.49/296.42 [1 1 0] [0] [1 0 0] 1166.49/296.42 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] 1166.49/296.42 1166.49/296.42 [1 1 0] [0] [1 0 0] 1166.49/296.42 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] 1166.49/296.42 1166.49/296.42 [1 1 0] [0] [1 0 0] 1166.49/296.42 5(0(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] 1166.49/296.42 1166.49/296.42 [1 0 0] [0] [1 0 0] [0] 1166.49/296.42 5(0(1(4(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.49/296.42 [0 0 0] [1] [0 0 0] [1] 1166.49/296.42 1166.49/296.42 [1 1 1] [1] [1 0 0] 1166.49/296.42 5(5(1(0(0(x1))))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] 1166.49/296.42 1166.49/296.42 [1 1 1] [1] [1 0 0] [0] 1166.49/296.42 5(3(0(1(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 0(1(5(2(3(x1))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] [1] 1166.49/296.42 1166.49/296.42 [1 1 1] [1] [1 1 0] [0] 1166.49/296.42 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] [1] 1166.49/296.42 1166.49/296.42 [1 1 1] [1] [1 0 0] [0] 1166.49/296.42 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] [1] 1166.49/296.42 1166.49/296.42 [1 1 1] [1] [1 0 0] 1166.49/296.42 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] 1166.49/296.42 1166.49/296.42 [1 1 1] [1] [1 1 0] [0] 1166.49/296.42 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.49/296.42 [0 0 1] [1] [0 0 0] [1] 1166.49/296.42 1166.49/296.42 [1 1 1] [2] [1 0 0] [0] 1166.49/296.42 5(3(1(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.49/296.42 [0 0 1] [2] [0 0 0] [2] 1166.49/296.42 problem: 1166.49/296.42 strict: 1166.49/296.42 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.49/296.42 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.49/296.42 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.49/296.42 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.49/296.42 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.49/296.42 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.49/296.42 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.49/296.42 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.49/296.42 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.49/296.42 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.49/296.42 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.49/296.42 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.49/296.42 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.49/296.42 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.49/296.42 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.49/296.42 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.49/296.42 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.49/296.42 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.49/296.42 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.49/296.42 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.49/296.42 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.49/296.42 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.49/296.42 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.49/296.42 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.49/296.42 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.49/296.42 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.49/296.42 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.49/296.43 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.49/296.43 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.49/296.43 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.49/296.43 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.49/296.43 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.49/296.43 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.49/296.43 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.49/296.43 weak: 1166.49/296.43 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.49/296.43 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.49/296.43 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.49/296.43 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.49/296.43 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.49/296.43 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.49/296.43 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.49/296.43 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.49/296.43 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.49/296.43 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.49/296.43 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.49/296.43 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.49/296.43 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.49/296.43 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.49/296.43 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.49/296.43 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.49/296.43 Matrix Interpretation Processor: dim=3 1166.49/296.43 1166.49/296.43 max_matrix: 1166.49/296.43 [1 1 0] 1166.49/296.43 [0 1 1] 1166.49/296.43 [0 0 1] 1166.49/296.43 interpretation: 1166.49/296.43 [1 0 0] 1166.49/296.43 [5](x0) = [0 0 0]x0 1166.49/296.43 [0 0 1] , 1166.49/296.43 1166.49/296.43 [1 0 0] 1166.49/296.43 [4](x0) = [0 0 0]x0 1166.49/296.43 [0 0 0] , 1166.49/296.43 1166.49/296.43 [1 0 0] 1166.49/296.43 [2](x0) = [0 0 0]x0 1166.49/296.43 [0 0 0] , 1166.49/296.43 1166.49/296.43 [1 0 0] 1166.49/296.43 [3](x0) = [0 0 1]x0 1166.49/296.43 [0 0 1] , 1166.49/296.43 1166.49/296.43 [1 1 0] 1166.49/296.43 [0](x0) = [0 0 0]x0 1166.49/296.43 [0 0 1] , 1166.49/296.43 1166.49/296.43 [1 0 0] [0] 1166.49/296.43 [1](x0) = [0 1 0]x0 + [0] 1166.49/296.43 [0 0 0] [1] 1166.49/296.43 orientation: 1166.49/296.43 [1 1 0] [0] [1 1 0] 1166.49/296.43 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.43 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.43 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 1 0] 1166.49/296.43 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.43 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] [0] 1166.49/296.43 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] [1] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.43 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] [0] 1166.49/296.43 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] [1] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.43 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.43 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.49/296.43 [0 0 0] [1] [0 0 0] 1166.49/296.43 1166.49/296.43 [1 1 0] [0] [1 0 0] 1166.49/296.44 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 0 0] 1166.49/296.44 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 0 0] [0] 1166.49/296.44 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 0 0] [0] 1166.49/296.44 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 0 0] 1166.49/296.44 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 0 0] [0] [1 0 0] [0] 1166.49/296.44 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.44 1166.49/296.44 [1 0 0] [0] [1 0 0] 1166.49/296.44 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 0 0] [0] [1 0 0] [0] 1166.49/296.44 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.44 1166.49/296.44 [1 0 0] [0] [1 0 0] [0] 1166.49/296.44 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.44 1166.49/296.44 [1 0 0] [0] [1 0 0] 1166.49/296.44 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 0 0] [0] [1 0 0] 1166.49/296.44 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 1] [0] [1 0 0] 1166.49/296.44 0(1(3(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 0 0] 1166.49/296.44 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 1 0] 1166.49/296.44 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 0] [1] [1 1 0] 1166.49/296.44 0(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 1 0] [1] [1 0 0] 1166.49/296.44 0(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] 1166.49/296.44 1166.49/296.44 [1 0 0] [1] [1 0 0] [0] 1166.49/296.44 0(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(1(1(0(3(4(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.44 1166.49/296.44 [1 1 0] [0] [1 0 0] [0] 1166.49/296.44 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.49/296.44 [0 0 0] [1] [0 0 0] [1] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] 1166.49/296.45 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] [0] 1166.49/296.45 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] [1] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] 1166.49/296.45 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] [0] 1166.49/296.45 0(1(2(5(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] [1] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] [0] 1166.49/296.45 0(1(4(2(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] [1] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] 1166.49/296.45 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 0 0] [0] [1 0 0] 1166.49/296.45 5(1(5(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(5(1(x1))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] 1166.49/296.45 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(1(x1)))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] 1166.49/296.45 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] 1166.49/296.45 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] [0] 1166.49/296.45 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(5(4(4(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] [1] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] 1166.49/296.45 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] 1166.49/296.45 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] 1166.49/296.45 5(0(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] [0] 1166.49/296.45 5(0(1(4(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] [1] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 1 0] 1166.49/296.45 5(5(1(0(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] 1166.49/296.45 1166.49/296.45 [1 1 0] [0] [1 0 0] [0] 1166.49/296.45 5(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(5(2(3(x1))))) 1166.49/296.45 [0 0 0] [1] [0 0 0] [1] 1166.49/296.46 1166.49/296.46 [1 1 0] [0] [1 1 0] [0] 1166.49/296.46 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.49/296.46 [0 0 0] [1] [0 0 0] [1] 1166.49/296.46 1166.49/296.46 [1 1 0] [0] [1 0 0] [0] 1166.49/296.46 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.49/296.46 [0 0 0] [1] [0 0 0] [1] 1166.49/296.46 1166.49/296.46 [1 1 0] [0] [1 1 0] 1166.49/296.46 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.49/296.46 [0 0 0] [1] [0 0 0] 1166.49/296.46 1166.49/296.46 [1 1 0] [0] [1 0 0] [0] 1166.49/296.46 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.49/296.46 [0 0 0] [1] [0 0 0] [1] 1166.49/296.46 1166.49/296.46 [1 0 0] [0] [1 0 0] [0] 1166.49/296.46 5(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.49/296.46 [0 0 0] [1] [0 0 0] [1] 1166.49/296.46 problem: 1166.49/296.46 strict: 1166.49/296.46 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.49/296.46 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.49/296.46 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.49/296.46 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.49/296.46 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.49/296.46 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.49/296.46 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.49/296.46 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.49/296.46 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.49/296.46 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.49/296.46 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.49/296.46 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.49/296.46 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.49/296.46 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.49/296.46 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.49/296.46 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.49/296.46 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.49/296.46 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.49/296.46 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.49/296.46 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.49/296.46 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.49/296.46 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.49/296.46 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.49/296.46 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.49/296.46 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.49/296.46 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.49/296.46 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.49/296.46 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.49/296.46 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.49/296.46 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.49/296.46 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.49/296.46 weak: 1166.49/296.46 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.49/296.46 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.49/296.46 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.49/296.46 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.49/296.46 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.49/296.46 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.49/296.46 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.49/296.46 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.49/296.46 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.49/296.46 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.49/296.46 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.49/296.46 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.49/296.46 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.49/296.46 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.49/296.46 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.49/296.46 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.49/296.46 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.49/296.46 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.49/296.46 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.49/296.46 Matrix Interpretation Processor: dim=3 1166.49/296.46 1166.49/296.46 max_matrix: 1166.49/296.46 [1 1 0] 1166.49/296.46 [0 1 1] 1166.49/296.46 [0 0 1] 1166.49/296.46 interpretation: 1166.49/296.46 1166.49/296.46 [5](x0) = x0 1166.49/296.46 , 1166.49/296.46 1166.49/296.46 [1 0 0] 1166.49/296.46 [4](x0) = [0 0 0]x0 1166.49/296.46 [0 0 0] , 1166.49/296.46 1166.49/296.46 [1 0 0] 1166.49/296.46 [2](x0) = [0 0 0]x0 1166.49/296.46 [0 0 0] , 1166.49/296.46 1166.49/296.46 [1 0 0] [0] 1166.49/296.46 [3](x0) = [0 0 1]x0 + [0] 1166.49/296.46 [0 0 0] [2], 1166.49/296.46 1166.49/296.46 [1 1 0] [0] 1166.49/296.46 [0](x0) = [0 0 0]x0 + [0] 1166.49/296.46 [0 0 0] [2], 1166.49/296.47 1166.49/296.47 [1 0 0] [0] 1166.49/296.47 [1](x0) = [0 1 0]x0 + [0] 1166.49/296.47 [0 0 0] [2] 1166.49/296.47 orientation: 1166.49/296.47 [1 1 0] [0] [1 1 0] [0] 1166.49/296.47 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(3(0(1(x1))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(4(0(5(4(1(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] 1166.49/296.47 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 1 0] 1166.49/296.47 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(1(2(x1))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(5(4(1(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(3(4(1(1(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(2(1(x1))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(5(4(1(x1))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(0(2(2(1(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] [0] 1166.49/296.47 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 1 0] [0] [1 0 0] 1166.49/296.47 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.49/296.47 [0 0 0] [2] [0 0 0] 1166.49/296.47 1166.49/296.47 [1 0 0] [0] [1 0 0] [0] 1166.49/296.47 5(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.49/296.47 [0 0 0] [2] [0 0 0] [2] 1166.49/296.47 1166.49/296.47 [1 0 0] [0] [1 0 0] 1166.49/296.47 5(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.49/296.48 [0 0 0] [2] [0 0 0] 1166.49/296.48 1166.49/296.48 [1 0 0] [0] [1 0 0] [0] 1166.49/296.48 5(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 0 0] [0] [1 0 0] [0] 1166.49/296.48 5(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 0 0] [0] [1 0 0] [0] 1166.49/296.48 5(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 + [0] = 3(5(2(3(1(1(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 0 0] [0] [1 0 0] 1166.49/296.48 5(1(1(x1))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] 1166.49/296.48 1166.49/296.48 [1 1 0] [2] [1 0 0] [0] 1166.49/296.48 0(1(3(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(2(0(2(1(3(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 0 0] [0] 1166.49/296.48 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(5(4(1(5(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 1 0] [0] 1166.49/296.48 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(4(2(1(0(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 0 0] [0] 1166.49/296.48 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 0 0] [0] 1166.49/296.48 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(4(2(2(1(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 0 0] [0] 1166.49/296.48 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 1 0] 1166.49/296.48 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 1 0] [0] 1166.49/296.48 0(1(2(5(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 1 0] [0] 1166.49/296.48 0(1(4(2(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [0] [1 1 0] 1166.49/296.48 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] 1166.49/296.48 1166.49/296.48 [1 1 0] [2] [1 1 0] [0] 1166.49/296.48 0(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(4(1(3(0(x1)))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.48 1166.49/296.48 [1 1 0] [2] [1 0 0] [0] 1166.49/296.48 0(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(0(2(3(1(x1))))) 1166.49/296.48 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 0 0] [2] [1 0 0] [0] 1166.49/296.49 0(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(1(1(0(3(4(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 0 0] [0] [1 0 0] 1166.49/296.49 5(1(5(1(x1)))) = [0 1 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(5(1(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(4(1(x1)))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 1 0] 1166.49/296.49 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(1(2(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(5(4(4(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(5(4(1(4(4(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 1 0] [0] 1166.49/296.49 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(4(3(0(1(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(0(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(0(4(1(3(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 1 0] [0] 1166.49/296.49 5(0(1(4(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 1 0] [0] 1166.49/296.49 5(5(1(0(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(5(0(4(1(0(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(3(0(1(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(1(5(2(3(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 1 0] [0] 1166.49/296.49 5(3(1(0(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(3(1(0(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 1 0] 1166.49/296.49 5(3(1(0(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] 1166.49/296.49 1166.49/296.49 [1 1 0] [0] [1 0 0] [0] 1166.49/296.49 5(3(1(0(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 1(3(0(4(3(5(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 1166.49/296.49 [1 0 0] [0] [1 0 0] [0] 1166.49/296.49 5(3(1(1(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 1(1(5(3(3(4(x1)))))) 1166.49/296.49 [0 0 0] [2] [0 0 0] [2] 1166.49/296.49 problem: 1166.49/296.49 strict: 1166.49/296.49 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.49/296.49 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.49/296.49 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.49/296.49 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.49/296.49 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.49/296.49 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.49/296.49 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.49/296.49 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.49/296.49 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.49/296.49 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.49/296.49 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.49/296.49 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.49/296.49 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.49/296.49 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.49/296.49 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.49/296.49 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.49/296.49 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.49/296.49 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.49/296.49 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.49/296.49 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.49/296.49 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.49/296.49 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.49/296.49 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.49/296.49 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.49/296.49 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.49/296.49 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.49/296.49 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.49/296.49 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.49/296.49 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.49/296.49 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.49/296.49 weak: 1166.49/296.49 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.49/296.49 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.49/296.49 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.49/296.49 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.49/296.49 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.49/296.49 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.49/296.49 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.49/296.49 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.49/296.49 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.49/296.49 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.49/296.49 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.49/296.49 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.49/296.49 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.49/296.49 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.49/296.49 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.49/296.49 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.49/296.49 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.49/296.49 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.49/296.49 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.49/296.49 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.49/296.49 Matrix Interpretation Processor: dim=3 1166.49/296.49 1166.49/296.49 max_matrix: 1166.49/296.49 [1 1 1] 1166.49/296.49 [0 1 1] 1166.49/296.49 [0 0 1] 1166.49/296.49 interpretation: 1166.49/296.49 [1 0 0] 1166.49/296.49 [5](x0) = [0 1 1]x0 1166.49/296.49 [0 0 1] , 1166.49/296.49 1166.49/296.49 [1 0 0] 1166.49/296.49 [4](x0) = [0 0 1]x0 1166.49/296.49 [0 0 0] , 1166.49/296.49 1166.49/296.49 [1 0 0] 1166.49/296.49 [2](x0) = [0 1 0]x0 1166.49/296.49 [0 0 0] , 1166.49/296.49 1166.49/296.49 [1 0 0] 1166.49/296.49 [3](x0) = [0 0 0]x0 1166.49/296.49 [0 0 1] , 1166.49/296.49 1166.49/296.49 [1 0 0] 1166.49/296.50 [0](x0) = [0 1 1]x0 1166.49/296.50 [0 0 1] , 1166.49/296.50 1166.49/296.50 [1 1 1] [0] 1166.49/296.50 [1](x0) = [0 0 0]x0 + [0] 1166.49/296.50 [0 0 0] [1] 1166.49/296.50 orientation: 1166.49/296.50 [1 1 1] [0] [1 1 1] 1166.49/296.50 0(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.49/296.50 [0 0 0] [1] [0 0 0] 1166.49/296.50 1166.49/296.50 [1 1 1] [0] [1 1 1] 1166.49/296.50 0(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.49/296.50 [0 0 0] [1] [0 0 0] 1166.49/296.50 1166.49/296.50 [1 1 1] [0] [1 0 0] 1166.49/296.50 0(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.49/296.50 [0 0 0] [1] [0 0 0] 1166.49/296.50 1166.49/296.50 [1 1 1] [0] [1 1 1] 1166.49/296.50 0(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 1 0] 1166.59/296.50 0(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 0 1] [0] 1166.59/296.50 0(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [1] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 1 1] [0] 1166.59/296.50 0(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(0(2(5(4(1(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [0] 1166.59/296.50 1166.59/296.50 [1 1 1] [1] [1 1 1] [0] 1166.59/296.50 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [1] 1166.59/296.50 1166.59/296.50 [1 1 1] [1] [1 1 1] [1] 1166.59/296.50 0(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 5(0(3(4(1(1(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [0] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 1 1] 1166.59/296.50 5(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 1 1] [0] 1166.59/296.50 5(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(0(5(4(1(x1))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [0] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 1 1] 1166.59/296.50 5(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 0 0] [0] 1166.59/296.50 5(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [1] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 0 0] [0] 1166.59/296.50 5(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [1] 1166.59/296.50 1166.59/296.50 [1 1 2] [0] [1 0 1] 1166.59/296.50 5(1(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.59/296.50 [0 0 0] [1] [0 0 0] 1166.59/296.50 1166.59/296.50 [1 1 1] [1] [1 0 1] [1] 1166.59/296.50 5(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.59/296.50 [0 0 0] [1] [0 0 0] [1] 1166.59/296.50 1166.59/296.50 [1 1 1] [1] [1 1 1] [1] 1166.59/296.51 5(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(4(1(1(x1)))) 1166.59/296.51 [0 0 0] [1] [0 0 0] [0] 1166.59/296.51 1166.59/296.51 [1 1 1] [1] [1 1 1] [0] 1166.59/296.51 5(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.59/296.51 [0 0 0] [1] [0 0 0] [1] 1166.59/296.51 1166.59/296.51 [1 1 1] [1] [1 0 0] [1] 1166.59/296.51 5(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.59/296.51 [0 0 0] [1] [0 0 0] [1] 1166.59/296.51 1166.59/296.51 [1 1 1] [1] [1 1 1] [1] 1166.59/296.51 5(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 3(5(2(3(1(1(x1)))))) 1166.59/296.51 [0 0 0] [1] [0 0 0] [0] 1166.59/296.51 1166.59/296.51 [1 1 1] [1] [1 0 1] [0] 1166.59/296.51 5(1(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 4(1(2(1(5(4(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [0] 1166.59/296.52 1166.59/296.52 [1 1 3] [0] [1 1 2] [0] 1166.59/296.52 0(1(5(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(0(5(4(1(5(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [0] 1166.59/296.52 1166.59/296.52 [1 1 3] [0] [1 1 2] 1166.59/296.52 0(1(5(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] 1166.59/296.52 1166.59/296.52 [1 1 1] [0] [1 0 0] [0] 1166.59/296.52 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [1] 1166.59/296.52 1166.59/296.52 [1 1 1] [0] [1 1 1] 1166.59/296.52 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] 1166.59/296.52 1166.59/296.52 [1 0 1] [0] [1 0 0] [0] 1166.59/296.52 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [1] 1166.59/296.52 1166.59/296.52 [1 0 1] [0] [1 0 1] 1166.59/296.52 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] 1166.59/296.52 1166.59/296.52 [1 1 2] [0] [1 0 0] [0] 1166.59/296.52 0(1(2(5(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [1] 1166.59/296.52 1166.59/296.52 [1 0 0] [0] [1 0 0] [0] 1166.59/296.52 0(1(4(2(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [1] 1166.59/296.52 1166.59/296.52 [1 1 2] [1] [1 1 2] [1] 1166.59/296.52 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(4(2(1(1(0(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [0] 1166.59/296.52 1166.59/296.52 [1 0 1] [0] [1 0 1] 1166.59/296.52 0(1(3(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] 1166.59/296.52 1166.59/296.52 [1 1 1] [0] [1 0 1] [0] 1166.59/296.52 0(3(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(0(4(1(3(0(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [0] 1166.59/296.52 1166.59/296.52 [1 1 2] [0] [1 1 1] 1166.59/296.52 0(3(1(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] 1166.59/296.52 1166.59/296.52 [1 1 1] [1] [1 0 0] [1] 1166.59/296.52 0(3(1(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(1(1(0(3(4(x1)))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [1] 1166.59/296.52 1166.59/296.52 [1 1 1] [2] [1 1 1] [2] 1166.59/296.52 5(1(5(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(4(1(5(1(x1))))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [0] 1166.59/296.52 1166.59/296.52 [1 1 1] [0] [1 1 1] [0] 1166.59/296.52 5(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(5(4(1(x1)))) 1166.59/296.52 [0 0 0] [1] [0 0 0] [0] 1166.59/296.52 1166.59/296.52 [1 1 1] [0] [1 1 1] [0] 1166.59/296.52 5(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 2(5(4(0(1(x1))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [0] 1166.59/296.53 1166.59/296.53 [1 1 1] [0] [1 1 0] 1166.59/296.53 5(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] 1166.59/296.53 1166.59/296.53 [1 1 1] [0] [1 0 0] [0] 1166.59/296.53 5(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(1(4(5(4(4(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 1] [0] [1 0 0] [0] 1166.59/296.53 5(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 0(5(4(1(4(4(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [0] 1166.59/296.53 1166.59/296.53 [1 1 1] [0] [1 1 1] [0] 1166.59/296.53 5(0(1(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 5(0(4(3(0(1(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [0] 1166.59/296.53 1166.59/296.53 [1 1 2] [0] [1 0 1] [0] 1166.59/296.53 5(0(1(0(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 5(0(0(4(1(3(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [0] 1166.59/296.53 1166.59/296.53 [1 0 1] [0] [1 0 0] [0] 1166.59/296.53 5(0(1(4(0(x1))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 3] [0] [1 1 2] [0] 1166.59/296.53 5(5(1(0(0(x1))))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = 5(5(0(4(1(0(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [0] 1166.59/296.53 1166.59/296.53 [1 1 1] [0] [1 0 0] [0] 1166.59/296.53 5(3(0(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(5(2(3(x1))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 2] [0] [1 0 1] [0] 1166.59/296.53 5(3(1(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 2] [0] [1 0 1] [0] 1166.59/296.53 5(3(1(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 2] [0] [1 1 2] [0] 1166.59/296.53 5(3(1(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 5(4(3(1(0(x1))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [0] 1166.59/296.53 1166.59/296.53 [1 1 2] [0] [1 0 0] [0] 1166.59/296.53 5(3(1(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 1] [1] [1 0 0] [1] 1166.59/296.53 5(3(1(1(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.59/296.53 [0 0 0] [1] [0 0 0] [1] 1166.59/296.53 problem: 1166.59/296.53 strict: 1166.59/296.53 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.59/296.53 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.59/296.53 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.59/296.53 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.59/296.53 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.59/296.53 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.59/296.53 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.59/296.53 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.59/296.53 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.59/296.53 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.59/296.53 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.59/296.53 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.59/296.53 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.59/296.53 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.59/296.53 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.59/296.53 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.59/296.53 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.59/296.53 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.59/296.53 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.59/296.53 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.59/296.53 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.59/296.53 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.59/296.53 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.59/296.53 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.59/296.53 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.59/296.53 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.59/296.53 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.59/296.53 weak: 1166.59/296.53 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.59/296.53 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.59/296.53 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.59/296.53 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.59/296.53 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.59/296.53 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.59/296.53 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.59/296.53 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.59/296.53 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.59/296.53 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.59/296.53 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.59/296.53 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.59/296.53 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.59/296.53 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.59/296.53 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.59/296.53 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.59/296.53 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.59/296.53 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.59/296.53 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.59/296.53 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.59/296.53 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.59/296.53 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.59/296.53 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.59/296.53 Matrix Interpretation Processor: dim=3 1166.59/296.53 1166.59/296.53 max_matrix: 1166.59/296.53 [1 1 1] 1166.59/296.53 [0 1 1] 1166.59/296.53 [0 0 1] 1166.59/296.53 interpretation: 1166.59/296.53 [1 0 1] 1166.59/296.53 [5](x0) = [0 0 0]x0 1166.59/296.53 [0 0 1] , 1166.59/296.53 1166.59/296.53 [1 0 0] 1166.59/296.53 [4](x0) = [0 0 0]x0 1166.59/296.53 [0 0 0] , 1166.59/296.53 1166.59/296.53 [1 0 0] 1166.59/296.53 [2](x0) = [0 0 0]x0 1166.59/296.53 [0 0 0] , 1166.59/296.53 1166.59/296.53 [1 0 0] 1166.59/296.53 [3](x0) = [0 0 1]x0 1166.59/296.53 [0 0 1] , 1166.59/296.53 1166.59/296.53 [1 1 0] 1166.59/296.53 [0](x0) = [0 0 0]x0 1166.59/296.53 [0 0 1] , 1166.59/296.53 1166.59/296.53 [0] 1166.59/296.53 [1](x0) = x0 + [0] 1166.59/296.53 [1] 1166.59/296.53 orientation: 1166.59/296.53 [1 1 0] [0] [1 1 0] 1166.59/296.53 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] 1166.59/296.53 1166.59/296.53 [1 1 0] [0] [1 0 0] 1166.59/296.53 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] 1166.59/296.53 1166.59/296.53 [1 1 0] [0] [1 0 0] 1166.59/296.53 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] 1166.59/296.53 1166.59/296.53 [1 1 0] [0] [1 1 0] 1166.59/296.53 0(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] 1166.59/296.53 1166.59/296.53 [1 1 0] [0] [1 0 0] 1166.59/296.53 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] 1166.59/296.53 1166.59/296.53 [1 1 0] [0] [1 0 0] [0] 1166.59/296.53 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] [1] 1166.59/296.53 1166.59/296.53 [1 1 0] [0] [1 0 0] 1166.59/296.53 0(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.59/296.53 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 0] [0] [1 0 0] 1166.59/296.54 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.59/296.54 [0 0 1] [2] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 1] [1] [1 0 0] 1166.59/296.54 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 1] [1] [1 0 0] 1166.59/296.54 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 1] [1] [1 0 0] 1166.59/296.54 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 1] [1] [1 0 0] [0] 1166.59/296.54 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] [1] 1166.59/296.54 1166.59/296.54 [1 1 1] [1] [1 0 0] [0] 1166.59/296.54 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] [1] 1166.59/296.54 1166.59/296.54 [1 1 1] [1] [1 0 1] 1166.59/296.54 5(1(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 0 1] [2] [1 0 0] [0] 1166.59/296.54 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.59/296.54 [0 0 1] [2] [0 0 0] [2] 1166.59/296.54 1166.59/296.54 [1 0 1] [2] [1 0 0] 1166.59/296.54 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.59/296.54 [0 0 1] [2] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 0 1] [2] [1 0 0] [0] 1166.59/296.54 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.59/296.54 [0 0 1] [2] [0 0 0] [2] 1166.59/296.54 1166.59/296.54 [1 0 1] [2] [1 0 0] 1166.59/296.54 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.59/296.54 [0 0 1] [2] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 1] [0] [1 0 1] 1166.59/296.54 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 1] [0] [1 1 0] 1166.59/296.54 0(1(5(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.59/296.54 [0 0 1] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 0] [1] [1 0 0] [0] 1166.59/296.54 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.59/296.54 [0 0 0] [1] [0 0 0] [1] 1166.59/296.54 1166.59/296.54 [1 1 0] [1] [1 0 0] 1166.59/296.54 5(1(2(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.59/296.54 [0 0 0] [1] [0 0 0] 1166.59/296.54 1166.59/296.54 [1 1 0] [1] [1 0 0] [0] 1166.59/296.54 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.59/296.54 [0 0 0] [1] [0 0 0] [1] 1166.59/296.54 1166.59/296.54 [1 1 0] [1] [1 1 0] 1166.59/296.54 5(1(4(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.59/296.55 [0 0 0] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [0] [1 1 0] [0] 1166.59/296.55 0(1(2(5(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.59/296.55 [0 0 0] [1] [0 0 0] [1] 1166.59/296.55 1166.59/296.55 [1 1 0] [0] [1 1 0] [0] 1166.59/296.55 0(1(4(2(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.59/296.55 [0 0 0] [1] [0 0 0] [1] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 1 0] 1166.59/296.55 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.59/296.55 [0 0 0] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 0] [0] [1 0 0] [0] 1166.59/296.55 0(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.59/296.55 [0 0 1] [2] [0 0 0] [1] 1166.59/296.55 1166.59/296.55 [1 0 1] [2] [1 0 0] [0] 1166.59/296.55 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.59/296.55 [0 0 1] [2] [0 0 0] [1] 1166.59/296.55 1166.59/296.55 [1 0 1] [2] [1 0 0] 1166.59/296.55 5(1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.59/296.55 [0 0 1] [2] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [0] [1 0 0] 1166.59/296.55 0(1(3(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 1 0] 1166.59/296.55 0(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 0 0] 1166.59/296.55 0(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 0 1] [2] [1 0 0] [2] 1166.59/296.55 0(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(1(1(0(3(4(x1)))))) 1166.59/296.55 [0 0 1] [2] [0 0 0] [2] 1166.59/296.55 1166.59/296.55 [1 0 2] [3] [1 0 1] [1] 1166.59/296.55 5(1(5(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(4(1(5(1(x1))))) 1166.59/296.55 [0 0 1] [2] [0 0 0] [0] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 0 0] 1166.59/296.55 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(1(x1)))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 1 0] 1166.59/296.55 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 0 0] 1166.59/296.55 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 0 0] [0] 1166.59/296.55 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(4(5(4(4(x1)))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] [1] 1166.59/296.55 1166.59/296.55 [1 1 1] [1] [1 0 0] 1166.59/296.55 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.59/296.55 [0 0 1] [1] [0 0 0] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 1 0] 1166.59/296.56 5(0(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 0 0] 1166.59/296.56 5(0(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] 1166.59/296.56 1166.59/296.56 [1 1 0] [1] [1 1 0] [0] 1166.59/296.56 5(0(1(4(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.59/296.56 [0 0 0] [1] [0 0 0] [1] 1166.59/296.56 1166.59/296.56 [1 1 2] [2] [1 1 0] 1166.59/296.56 5(5(1(0(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 0 0] [0] 1166.59/296.56 5(3(0(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(5(2(3(x1))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] [1] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 1 1] [0] 1166.59/296.56 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] [1] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 0 0] [0] 1166.59/296.56 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] [1] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 1 0] 1166.59/296.56 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] 1166.59/296.56 1166.59/296.56 [1 1 1] [1] [1 0 1] [0] 1166.59/296.56 5(3(1(0(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.59/296.56 [0 0 1] [1] [0 0 0] [1] 1166.59/296.56 1166.59/296.56 [1 0 1] [2] [1 0 0] [0] 1166.59/296.56 5(3(1(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.59/296.56 [0 0 1] [2] [0 0 0] [2] 1166.59/296.56 problem: 1166.59/296.56 strict: 1166.59/296.56 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.59/296.56 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.59/296.56 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.59/296.56 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.59/296.56 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.59/296.56 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.59/296.56 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.59/296.56 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.59/296.56 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.59/296.56 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.59/296.56 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.59/296.56 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.59/296.56 weak: 1166.59/296.56 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.59/296.56 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.59/296.56 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.59/296.56 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.59/296.56 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.59/296.56 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.59/296.56 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.59/296.56 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.59/296.56 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.59/296.56 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.59/296.56 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.59/296.56 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.59/296.56 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.59/296.56 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.59/296.56 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.59/296.56 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.59/296.56 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.59/296.56 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.59/296.56 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.59/296.56 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.59/296.57 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.59/296.57 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.59/296.57 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.59/296.57 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.59/296.57 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.59/296.57 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.59/296.57 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.59/296.57 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.59/296.57 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.59/296.57 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.59/296.57 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.59/296.57 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.59/296.57 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.59/296.57 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.59/296.57 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.59/296.57 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.59/296.57 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.59/296.57 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.59/296.57 Matrix Interpretation Processor: dim=4 1166.59/296.57 1166.59/296.57 max_matrix: 1166.59/296.57 [1 1 1 0] 1166.59/296.57 [0 0 1 0] 1166.59/296.57 [0 0 0 1] 1166.59/296.57 [0 0 0 1] 1166.59/296.57 interpretation: 1166.59/296.57 [1 0 0 0] 1166.59/296.57 [0 0 0 0] 1166.59/296.57 [5](x0) = [0 0 0 1]x0 1166.59/296.57 [0 0 0 1] , 1166.59/296.57 1166.59/296.57 [1 0 0 0] 1166.59/296.57 [0 0 1 0] 1166.59/296.57 [4](x0) = [0 0 0 0]x0 1166.59/296.57 [0 0 0 0] , 1166.59/296.57 1166.59/296.57 [1 0 0 0] 1166.59/296.57 [0 0 0 0] 1166.59/296.57 [2](x0) = [0 0 0 0]x0 1166.59/296.57 [0 0 0 0] , 1166.59/296.57 1166.59/296.57 [1 1 0 0] 1166.59/296.57 [0 0 0 0] 1166.59/296.57 [3](x0) = [0 0 0 0]x0 1166.59/296.57 [0 0 0 1] , 1166.59/296.57 1166.59/296.57 [1 1 1 0] 1166.59/296.57 [0 0 0 0] 1166.59/296.57 [0](x0) = [0 0 0 1]x0 1166.59/296.57 [0 0 0 1] , 1166.59/296.57 1166.59/296.57 [1 1 1 0] [0] 1166.59/296.57 [0 0 0 0] [0] 1166.59/296.57 [1](x0) = [0 0 0 1]x0 + [0] 1166.59/296.57 [0 0 0 1] [1] 1166.59/296.57 orientation: 1166.59/296.57 [1 1 1 2] [1] [1 1 1 1] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.57 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.59/296.57 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.57 1166.59/296.57 [1 1 1 2] [1] [1 1 1 0] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.57 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.59/296.57 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.57 1166.59/296.57 [1 1 1 2] [1] [1 0 1 0] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.57 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.59/296.57 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.57 1166.59/296.57 [1 1 1 2] [1] [1 1 1 1] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.57 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.59/296.57 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.57 1166.59/296.57 [1 1 1 2] [0] [1 0 0 0] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.57 0(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.59/296.57 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.57 1166.59/296.57 [1 1 1 2] [0] [1 0 0 0] [0] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] [0] 1166.59/296.57 0(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.59/296.57 [0 0 0 1] [1] [0 0 0 0] [1] 1166.59/296.57 1166.59/296.57 [1 1 1 2] [0] [1 1 1 0] 1166.59/296.57 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 0(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 2] [1] [1 1 1 2] [1] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] [0] 1166.59/296.59 0(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 5(0(3(4(1(1(x1)))))) 1166.59/296.59 [0 0 0 1] [2] [0 0 0 0] [0] 1166.59/296.59 1166.59/296.59 [1 1 1 2] [0] [1 0 0 1] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 0(1(5(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 2] [0] [1 1 1 1] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 0(1(5(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 0] [0] [1 1 1 0] [0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] [0] 1166.59/296.59 0(1(2(5(0(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.59/296.59 [0 0 0 0] [1] [0 0 0 0] [1] 1166.59/296.59 1166.59/296.59 [1 1 1 0] [0] [1 1 1 0] [0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] [0] 1166.59/296.59 0(1(4(2(0(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.59/296.59 [0 0 0 0] [1] [0 0 0 0] [1] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 1 1 0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 1 1 0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 1 1 0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 1 0 0] [0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] [0] 1166.59/296.59 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] [1] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 0 0 0] [0] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] [0] 1166.59/296.59 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] [1] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 0 0 1] 1166.59/296.59 [0 0 0 0] [0] [0 0 0 0] 1166.59/296.59 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.59/296.59 [0 0 0 1] [1] [0 0 0 0] 1166.59/296.59 1166.59/296.59 [1 1 1 1] [0] [1 0 0 0] [0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.60 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [1] = 1(1(5(4(x1)))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] [2] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 1 1 1] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.60 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 5(4(1(1(x1)))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 0 0 0] [0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.60 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [1] = 1(1(4(5(4(4(x1)))))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] [2] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 1 1 1] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.60 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] 1166.69/296.60 1166.69/296.60 [1 1 1 0] [0] [1 0 0 0] [0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.60 5(1(2(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.69/296.60 [0 0 0 0] [1] [0 0 0 0] [1] 1166.69/296.60 1166.69/296.60 [1 1 1 0] [0] [1 1 1 0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.60 5(1(2(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.69/296.60 [0 0 0 0] [1] [0 0 0 0] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 1 0 0] [0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.60 5(1(4(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.69/296.60 [0 0 0 0] [1] [0 0 0 0] [1] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 1 1 0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.60 5(1(4(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.69/296.60 [0 0 0 0] [1] [0 0 0 0] 1166.69/296.60 1166.69/296.60 [1 1 1 2] [1] [1 1 1 2] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.60 1(4(5(1(0(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.69/296.60 [0 0 0 0] [1] [0 0 0 0] 1166.69/296.60 1166.69/296.60 [1 1 1 2] [1] [1 1 1 1] [0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.60 0(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] [1] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 1 1 1] [0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.60 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] [1] 1166.69/296.60 1166.69/296.60 [1 1 1 1] [0] [1 0 0 0] 1166.69/296.60 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.60 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.69/296.60 [0 0 0 1] [2] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 1 0 0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 0(1(3(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 1 1 1] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 0(3(0(1(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 1 1 0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 0(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 0 1 0] [0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.62 0(3(1(1(x1)))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [2] = 5(1(1(0(3(4(x1)))))) 1166.69/296.62 [0 0 0 1] [2] [0 0 0 0] [2] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [1] [1 1 1 1] [1] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.62 5(1(5(1(x1)))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 5(4(1(5(1(x1))))) 1166.69/296.62 [0 0 0 1] [2] [0 0 0 0] [0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 1 1 0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(4(1(x1)))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 1 1 1] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 0 0 0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 0 0 0] [0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.62 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [1] = 0(1(4(5(4(4(x1)))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 0 0 0] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 1] [0] [1 1 1 1] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.62 1166.69/296.62 [1 1 1 2] [0] [1 1 0 1] 1166.69/296.62 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.62 5(0(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.69/296.62 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 1 1 1] [0] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.63 5(0(1(4(0(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.69/296.63 [0 0 0 0] [1] [0 0 0 0] [1] 1166.69/296.63 1166.69/296.63 [1 1 1 2] [0] [1 1 1 2] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.63 5(5(1(0(0(x1))))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.69/296.63 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 1 0 0] [0] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.63 5(3(0(1(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [1] = 0(1(5(2(3(x1))))) 1166.69/296.63 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 1 1 0] [0] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.63 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.69/296.63 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 1 0 0] [0] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.63 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.69/296.63 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 1 1 1] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.63 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.69/296.63 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 0 0 0] [0] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.63 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.69/296.63 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.63 1166.69/296.63 [1 1 1 1] [0] [1 0 1 0] [0] 1166.69/296.63 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.63 5(3(1(1(x1)))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [1] = 1(1(5(3(3(4(x1)))))) 1166.69/296.63 [0 0 0 1] [2] [0 0 0 0] [2] 1166.69/296.63 problem: 1166.69/296.63 strict: 1166.69/296.63 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.69/296.63 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.69/296.63 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.69/296.63 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.69/296.63 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.69/296.63 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.69/296.63 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.69/296.63 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.69/296.63 weak: 1166.69/296.63 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.69/296.63 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.69/296.63 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.69/296.63 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.69/296.63 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.69/296.63 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.69/296.63 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.69/296.63 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.69/296.63 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.69/296.63 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.69/296.63 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.69/296.63 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.69/296.63 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.69/296.63 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.69/296.63 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.69/296.64 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.69/296.64 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.69/296.64 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.69/296.64 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.69/296.64 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.69/296.64 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.69/296.64 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.69/296.64 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.69/296.64 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.69/296.64 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.69/296.64 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.69/296.64 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.69/296.64 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.69/296.64 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.69/296.64 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.69/296.64 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.69/296.64 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.69/296.64 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.69/296.64 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.69/296.64 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.69/296.64 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.69/296.64 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.69/296.64 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.69/296.64 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.69/296.64 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.69/296.64 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.69/296.64 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.69/296.64 Matrix Interpretation Processor: dim=3 1166.69/296.64 1166.69/296.64 max_matrix: 1166.69/296.64 [1 1 0] 1166.69/296.64 [0 1 1] 1166.69/296.64 [0 0 1] 1166.69/296.64 interpretation: 1166.69/296.64 [1 0 0] 1166.69/296.64 [5](x0) = [0 0 1]x0 1166.69/296.64 [0 0 1] , 1166.69/296.64 1166.69/296.64 [1 0 0] 1166.69/296.64 [4](x0) = [0 1 0]x0 1166.69/296.64 [0 0 0] , 1166.69/296.64 1166.69/296.64 [1 0 0] 1166.69/296.64 [2](x0) = [0 0 0]x0 1166.69/296.64 [0 0 0] , 1166.69/296.64 1166.69/296.64 [1 0 0] 1166.69/296.64 [3](x0) = [0 0 0]x0 1166.69/296.64 [0 0 1] , 1166.69/296.64 1166.69/296.64 [1 1 0] 1166.69/296.64 [0](x0) = [0 0 1]x0 1166.69/296.64 [0 0 1] , 1166.69/296.64 1166.69/296.64 [1 1 0] [0] 1166.69/296.64 [1](x0) = [0 0 1]x0 + [0] 1166.69/296.64 [0 0 1] [1] 1166.69/296.64 orientation: 1166.69/296.64 [1 1 2] [0] [1 0 0] 1166.69/296.64 0(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.69/296.64 [0 0 1] [1] [0 0 0] 1166.69/296.64 1166.69/296.64 [1 1 2] [0] [1 0 0] [0] 1166.69/296.64 0(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.69/296.64 [0 0 1] [1] [0 0 0] [1] 1166.69/296.64 1166.69/296.64 [1 1 2] [0] [1 1 0] 1166.69/296.64 0(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.69/296.64 [0 0 1] [1] [0 0 0] 1166.69/296.64 1166.69/296.64 [1 1 2] [1] [1 1 1] 1166.69/296.64 0(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.69/296.64 [0 0 1] [2] [0 0 0] 1166.69/296.64 1166.69/296.64 [1 1 2] [0] [1 0 1] 1166.69/296.64 0(1(5(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.69/296.64 [0 0 1] [1] [0 0 0] 1166.69/296.64 1166.69/296.64 [1 1 2] [0] [1 1 1] 1166.69/296.64 0(1(5(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.69/296.64 [0 0 1] [1] [0 0 0] 1166.69/296.64 1166.69/296.64 [1 1 0] [0] [1 1 0] [0] 1166.69/296.64 0(1(2(5(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.69/296.64 [0 0 0] [1] [0 0 0] [1] 1166.69/296.64 1166.69/296.64 [1 1 0] [0] [1 1 0] [0] 1166.69/296.64 0(1(4(2(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.69/296.65 [0 0 0] [1] [0 0 0] [1] 1166.69/296.65 1166.69/296.65 [1 1 2] [1] [1 1 1] 1166.69/296.65 0(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(2(3(0(1(x1))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 2] [1] [1 1 0] 1166.69/296.65 0(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 2] [1] [1 0 0] 1166.69/296.65 0(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 2] [1] [1 1 1] 1166.69/296.65 0(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 4(0(5(4(0(1(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 1 0] 1166.69/296.65 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 1 0] 1166.69/296.65 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 1 0] 1166.69/296.65 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 0 0] [0] 1166.69/296.65 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] [1] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 0 0] [0] 1166.69/296.65 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] [1] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 0 1] 1166.69/296.65 5(1(0(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.69/296.65 [0 0 1] [1] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 0 0] [0] 1166.69/296.65 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(1(5(4(x1)))) 1166.69/296.65 [0 0 1] [2] [0 0 0] [2] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 1 1] 1166.69/296.65 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 5(4(1(1(x1)))) 1166.69/296.65 [0 0 1] [2] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 0 0] [0] 1166.69/296.65 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(1(4(5(4(4(x1)))))) 1166.69/296.65 [0 0 1] [2] [0 0 0] [2] 1166.69/296.65 1166.69/296.65 [1 1 1] [0] [1 1 1] 1166.69/296.65 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.69/296.65 [0 0 1] [2] [0 0 0] 1166.69/296.65 1166.69/296.65 [1 1 0] [0] [1 0 0] [0] 1166.69/296.65 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.69/296.65 [0 0 0] [1] [0 0 0] [1] 1166.69/296.65 1166.69/296.65 [1 1 0] [0] [1 1 0] 1166.69/296.65 5(1(2(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.69/296.65 [0 0 0] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.69/296.66 [0 0 0] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 0] 1166.69/296.66 5(1(4(0(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.69/296.66 [0 0 0] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 2] [1] [1 1 2] 1166.69/296.66 1(4(5(1(0(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.69/296.66 [0 0 0] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 2] [1] [1 1 0] [0] 1166.69/296.66 0(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.69/296.66 [0 0 1] [2] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 0] [0] 1166.69/296.66 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.69/296.66 [0 0 1] [2] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] 1166.69/296.66 5(1(1(x1))) = [0 0 1]x1 + [2] >= [0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.69/296.66 [0 0 1] [2] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] 1166.69/296.66 0(1(3(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 1] 1166.69/296.66 0(3(0(1(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 0] 1166.69/296.66 0(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 0(3(1(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [2] = 5(1(1(0(3(4(x1)))))) 1166.69/296.66 [0 0 1] [2] [0 0 0] [2] 1166.69/296.66 1166.69/296.66 [1 1 1] [1] [1 1 1] [1] 1166.69/296.66 5(1(5(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 5(4(1(5(1(x1))))) 1166.69/296.66 [0 0 1] [2] [0 0 0] [0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 0] 1166.69/296.66 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(1(x1)))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 1] 1166.69/296.66 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 2(5(4(0(1(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] 1166.69/296.66 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(4(5(4(4(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 0] 1166.69/296.66 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 1] 1166.69/296.66 5(0(1(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(4(3(0(1(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 2] [0] [1 0 1] 1166.69/296.66 5(0(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 1] [0] 1166.69/296.66 5(0(1(4(0(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.69/296.66 [0 0 0] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 2] [0] [1 1 2] 1166.69/296.66 5(5(1(0(0(x1))))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 5(3(0(1(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(5(2(3(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 0] [0] 1166.69/296.66 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 1 1] 1166.69/296.66 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 5(3(1(0(x1)))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.69/296.66 [0 0 1] [1] [0 0 0] [1] 1166.69/296.66 1166.69/296.66 [1 1 1] [0] [1 0 0] [0] 1166.69/296.66 5(3(1(1(x1)))) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [1] = 1(1(5(3(3(4(x1)))))) 1166.69/296.66 [0 0 1] [2] [0 0 0] [2] 1166.69/296.66 problem: 1166.69/296.66 strict: 1166.69/296.66 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.69/296.66 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.69/296.66 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.69/296.66 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.69/296.66 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.69/296.66 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.69/296.66 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.69/296.66 weak: 1166.69/296.66 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.69/296.66 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.69/296.66 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.69/296.66 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.69/296.66 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.69/296.66 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.69/296.66 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.69/296.66 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.69/296.66 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.69/296.66 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.69/296.66 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.69/296.66 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.69/296.66 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.69/296.66 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.69/296.66 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.69/296.66 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.69/296.66 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.69/296.66 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.69/296.66 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.69/296.66 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.69/296.66 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.69/296.67 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.69/296.67 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.69/296.67 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.69/296.67 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.69/296.67 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.69/296.67 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.69/296.67 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.69/296.67 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.69/296.67 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.69/296.67 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.69/296.67 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.69/296.67 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.69/296.67 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.69/296.67 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.69/296.67 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.69/296.67 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.69/296.67 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.69/296.67 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.69/296.67 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.69/296.67 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.69/296.67 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.69/296.67 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.69/296.67 Matrix Interpretation Processor: dim=4 1166.69/296.67 1166.69/296.67 max_matrix: 1166.69/296.67 [1 1 0 1] 1166.69/296.67 [0 1 1 0] 1166.69/296.67 [0 0 1 1] 1166.69/296.67 [0 0 0 1] 1166.69/296.67 interpretation: 1166.69/296.67 [1 1 0 0] 1166.69/296.67 [0 0 0 0] 1166.69/296.67 [5](x0) = [0 0 0 1]x0 1166.69/296.67 [0 0 0 1] , 1166.69/296.67 1166.69/296.67 [1 0 0 0] 1166.69/296.67 [0 0 0 0] 1166.69/296.67 [4](x0) = [0 0 1 0]x0 1166.69/296.67 [0 0 0 0] , 1166.69/296.67 1166.69/296.67 [1 0 0 0] 1166.69/296.67 [0 0 0 0] 1166.69/296.67 [2](x0) = [0 0 0 0]x0 1166.69/296.67 [0 0 0 0] , 1166.69/296.67 1166.69/296.67 [1 0 0 0] 1166.69/296.67 [0 1 0 0] 1166.69/296.67 [3](x0) = [0 0 0 0]x0 1166.69/296.67 [0 0 0 1] , 1166.69/296.67 1166.69/296.67 [1 0 0 1] 1166.69/296.67 [0 1 0 0] 1166.69/296.67 [0](x0) = [0 0 0 1]x0 1166.69/296.67 [0 0 0 1] , 1166.69/296.67 1166.69/296.67 [1 0 0 0] [0] 1166.69/296.67 [0 1 1 0] [0] 1166.69/296.67 [1](x0) = [0 0 0 0]x0 + [0] 1166.69/296.67 [0 0 0 1] [1] 1166.69/296.67 orientation: 1166.69/296.67 [1 0 0 2] [1] [1 0 0 0] 1166.69/296.67 [0 1 0 1] [0] [0 0 0 0] 1166.69/296.67 0(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(2(1(2(x1))))) 1166.69/296.67 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.67 1166.69/296.67 [1 0 0 2] [1] [1 0 0 0] [0] 1166.69/296.67 [0 1 0 1] [0] [0 0 0 0] [0] 1166.69/296.67 0(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(0(0(5(4(x1))))) 1166.69/296.67 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.67 1166.69/296.67 [1 0 0 2] [1] [1 0 0 0] 1166.69/296.67 [0 1 0 1] [0] [0 0 0 0] 1166.69/296.67 0(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(2(5(4(1(x1)))))) 1166.69/296.67 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.67 1166.69/296.67 [1 1 0 2] [1] [1 1 0 0] 1166.69/296.67 [0 0 0 1] [0] [0 0 0 0] 1166.69/296.67 0(1(5(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(5(4(1(5(x1)))))) 1166.69/296.67 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.67 1166.69/296.67 [1 1 0 2] [1] [1 0 0 1] 1166.69/296.67 [0 0 0 1] [0] [0 0 0 0] 1166.69/296.67 0(1(5(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(4(2(1(0(x1)))))) 1166.69/296.67 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.67 1166.69/296.67 [1 1 0 1] [1] [1 0 0 1] [0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.69 0(1(2(5(0(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(4(0(2(0(x1)))))) 1166.69/296.69 [0 0 0 0] [1] [0 0 0 0] [1] 1166.69/296.69 1166.69/296.69 [1 0 0 1] [1] [1 0 0 1] [0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.69 0(1(4(2(0(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(0(4(2(3(0(x1)))))) 1166.69/296.69 [0 0 0 0] [1] [0 0 0 0] [1] 1166.69/296.69 1166.69/296.69 [1 0 0 1] [2] [1 0 0 0] 1166.69/296.69 [0 1 1 0] [0] [0 0 0 0] 1166.69/296.69 0(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 5(0(3(4(1(1(x1)))))) 1166.69/296.69 [0 0 0 1] [2] [0 0 0 0] 1166.69/296.69 1166.69/296.69 [1 0 0 2] [2] [1 0 0 1] [1] 1166.69/296.69 [0 1 1 0] [0] [0 0 0 0] [0] 1166.69/296.69 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 0(2(3(0(1(x1))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] [0] 1166.69/296.69 1166.69/296.69 [1 0 0 2] [2] [1 0 0 0] 1166.69/296.69 [0 1 1 0] [0] [0 0 0 0] 1166.69/296.69 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(4(0(5(4(1(x1)))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.69 1166.69/296.69 [1 0 0 2] [2] [1 0 0 0] 1166.69/296.69 [0 1 1 0] [0] [0 0 0 0] 1166.69/296.69 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 2(1(0(0(3(4(x1)))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.69 1166.69/296.69 [1 0 0 2] [2] [1 0 0 1] [1] 1166.69/296.69 [0 1 1 0] [0] [0 0 0 0] [0] 1166.69/296.69 0(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 4(0(5(4(0(1(x1)))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] [0] 1166.69/296.69 1166.69/296.69 [1 1 0 2] [0] [1 0 0 0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.69 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(2(2(1(x1))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.69 1166.69/296.69 [1 1 0 2] [0] [1 0 0 0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.69 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(5(4(1(x1))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.69 1166.69/296.69 [1 1 0 2] [0] [1 0 0 0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] 1166.69/296.69 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(0(2(2(1(x1)))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] 1166.69/296.69 1166.69/296.69 [1 1 0 2] [0] [1 0 0 0] [0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.69 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(0(5(2(3(x1)))))) 1166.69/296.69 [0 0 0 1] [1] [0 0 0 0] [1] 1166.69/296.69 1166.69/296.69 [1 1 0 2] [0] [1 0 0 0] [0] 1166.69/296.69 [0 0 0 0] [0] [0 0 0 0] [0] 1166.69/296.69 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(0(4(4(2(x1)))))) 1166.79/296.70 [0 0 0 1] [1] [0 0 0 0] [1] 1166.79/296.70 1166.79/296.70 [1 1 0 2] [0] [1 1 0 0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.70 5(1(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 4(4(1(0(4(5(x1)))))) 1166.79/296.70 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.70 1166.79/296.70 [1 1 1 0] [0] [1 0 0 0] [0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.70 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(1(5(4(x1)))) 1166.79/296.70 [0 0 0 1] [2] [0 0 0 0] [2] 1166.79/296.70 1166.79/296.70 [1 1 1 0] [0] [1 0 0 0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.70 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 5(4(1(1(x1)))) 1166.79/296.70 [0 0 0 1] [2] [0 0 0 0] 1166.79/296.70 1166.79/296.70 [1 1 1 0] [0] [1 0 0 0] [0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.70 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(1(4(5(4(4(x1)))))) 1166.79/296.70 [0 0 0 1] [2] [0 0 0 0] [2] 1166.79/296.70 1166.79/296.70 [1 1 1 0] [0] [1 0 0 0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.70 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 3(5(2(3(1(1(x1)))))) 1166.79/296.70 [0 0 0 1] [2] [0 0 0 0] 1166.79/296.70 1166.79/296.70 [1 0 0 1] [0] [1 0 0 0] [0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.70 5(1(2(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(0(5(4(2(x1)))))) 1166.79/296.70 [0 0 0 0] [1] [0 0 0 0] [1] 1166.79/296.70 1166.79/296.70 [1 0 0 1] [0] [1 0 0 0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.70 5(1(2(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 5(0(4(2(2(1(x1)))))) 1166.79/296.70 [0 0 0 0] [1] [0 0 0 0] 1166.79/296.70 1166.79/296.70 [1 0 0 2] [0] [1 0 0 0] [0] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.70 5(1(4(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(4(0(2(3(x1)))))) 1166.79/296.70 [0 0 0 0] [1] [0 0 0 0] [1] 1166.79/296.70 1166.79/296.70 [1 0 0 2] [0] [1 0 0 1] 1166.79/296.70 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.70 5(1(4(0(x1)))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = 4(5(2(1(3(0(x1)))))) 1166.79/296.70 [0 0 0 0] [1] [0 0 0 0] 1166.79/296.70 1166.79/296.70 [1 1 0 2] [0] [1 0 0 1] 1166.79/296.70 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.70 1(4(5(1(0(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 5(4(2(1(1(0(x1)))))) 1166.79/296.70 [0 0 0 0] [1] [0 0 0 0] 1166.79/296.70 1166.79/296.70 [1 0 0 1] [2] [1 0 0 0] [0] 1166.79/296.70 [0 1 1 0] [0] [0 0 0 0] [0] 1166.79/296.70 0(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(0(3(4(1(x1))))) 1166.79/296.70 [0 0 0 1] [2] [0 0 0 0] [1] 1166.79/296.70 1166.79/296.71 [1 1 1 0] [0] [1 0 0 0] [0] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.71 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(5(3(4(1(x1))))) 1166.79/296.71 [0 0 0 1] [2] [0 0 0 0] [1] 1166.79/296.71 1166.79/296.71 [1 1 1 0] [0] [1 0 0 0] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.71 5(1(1(x1))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 4(1(2(1(5(4(x1)))))) 1166.79/296.71 [0 0 0 1] [2] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 0 0 2] [1] [1 0 0 0] 1166.79/296.71 [0 1 0 0] [0] [0 0 0 0] 1166.79/296.71 0(1(3(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(2(0(2(1(3(x1)))))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 0 0 2] [2] [1 0 0 1] 1166.79/296.71 [0 1 1 0] [0] [0 0 0 0] 1166.79/296.71 0(3(0(1(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(4(1(3(0(x1)))))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 0 0 2] [1] [1 0 0 0] 1166.79/296.71 [0 1 0 1] [0] [0 0 0 0] 1166.79/296.71 0(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(0(2(3(1(x1))))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 0 0 1] [2] [1 0 0 0] [0] 1166.79/296.71 [0 1 1 0] [0] [0 0 0 0] [0] 1166.79/296.71 0(3(1(1(x1)))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [2] = 5(1(1(0(3(4(x1)))))) 1166.79/296.71 [0 0 0 1] [2] [0 0 0 0] [2] 1166.79/296.71 1166.79/296.71 [1 1 1 1] [1] [1 1 1 0] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.71 5(1(5(1(x1)))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 = 5(4(1(5(1(x1))))) 1166.79/296.71 [0 0 0 1] [2] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 1 1 1] [1] [1 0 0 0] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.71 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(4(1(x1)))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 1 1 1] [1] [1 0 0 1] [1] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.71 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 2(5(4(0(1(x1))))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] [0] 1166.79/296.71 1166.79/296.71 [1 1 1 1] [1] [1 0 0 0] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.71 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(2(1(2(x1))))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.71 1166.79/296.71 [1 1 1 1] [1] [1 0 0 0] [1] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.71 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [1] = 0(1(4(5(4(4(x1)))))) 1166.79/296.71 [0 0 0 1] [1] [0 0 0 0] [1] 1166.79/296.71 1166.79/296.71 [1 1 1 1] [1] [1 0 0 0] 1166.79/296.71 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.71 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 0(5(4(1(4(4(x1)))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.72 1166.79/296.72 [1 1 1 1] [1] [1 0 0 1] [1] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(0(1(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 5(0(4(3(0(1(x1)))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] [0] 1166.79/296.72 1166.79/296.72 [1 1 0 3] [1] [1 0 0 0] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.72 5(0(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(0(0(4(1(3(x1)))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.72 1166.79/296.72 [1 0 0 2] [1] [1 0 0 2] [0] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(0(1(4(0(x1))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(5(4(0(0(x1)))))) 1166.79/296.72 [0 0 0 0] [1] [0 0 0 0] [1] 1166.79/296.72 1166.79/296.72 [1 1 0 3] [0] [1 0 0 1] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.72 5(5(1(0(0(x1))))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(5(0(4(1(0(x1)))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.72 1166.79/296.72 [1 1 1 1] [1] [1 0 0 0] [1] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(3(0(1(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [1] = 0(1(5(2(3(x1))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] [1] 1166.79/296.72 1166.79/296.72 [1 1 0 2] [0] [1 1 0 1] [0] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(4(3(5(0(x1))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] [1] 1166.79/296.72 1166.79/296.72 [1 1 0 2] [0] [1 0 0 0] [0] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(5(0(4(3(x1))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] [1] 1166.79/296.72 1166.79/296.72 [1 1 0 2] [0] [1 0 0 1] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] 1166.79/296.72 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = 5(4(3(1(0(x1))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] 1166.79/296.72 1166.79/296.72 [1 1 0 2] [0] [1 1 0 0] [0] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(3(1(0(x1)))) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = 1(3(0(4(3(5(x1)))))) 1166.79/296.72 [0 0 0 1] [1] [0 0 0 0] [1] 1166.79/296.72 1166.79/296.72 [1 1 1 0] [0] [1 0 0 0] [0] 1166.79/296.72 [0 0 0 0] [0] [0 0 0 0] [0] 1166.79/296.72 5(3(1(1(x1)))) = [0 0 0 1]x1 + [2] >= [0 0 0 0]x1 + [0] = 1(1(5(3(3(4(x1)))))) 1166.79/296.72 [0 0 0 1] [2] [0 0 0 0] [2] 1166.79/296.72 problem: 1166.79/296.72 strict: 1166.79/296.72 1166.79/296.72 weak: 1166.79/296.72 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 1166.79/296.72 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 1166.79/296.72 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 1166.79/296.72 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 1166.79/296.73 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 1166.79/296.73 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 1166.79/296.73 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1166.79/296.73 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 1166.79/296.73 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 1166.79/296.73 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 1166.79/296.73 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 1166.79/296.73 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 1166.79/296.73 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 1166.79/296.73 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 1166.79/296.73 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 1166.79/296.73 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 1166.79/296.73 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 1166.79/296.73 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 1166.79/296.73 5(1(1(x1))) -> 1(1(5(4(x1)))) 1166.79/296.73 5(1(1(x1))) -> 5(4(1(1(x1)))) 1166.79/296.73 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 1166.79/296.73 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 1166.79/296.73 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 1166.79/296.73 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 1166.79/296.73 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 1166.79/296.73 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 1166.79/296.73 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 1166.79/296.73 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 1166.79/296.73 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 1166.79/296.73 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 1166.79/296.73 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 1166.79/296.73 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 1166.79/296.73 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 1166.79/296.73 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 1166.79/296.73 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 1166.79/296.73 5(0(1(x1))) -> 0(5(4(1(x1)))) 1166.79/296.73 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 1166.79/296.73 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 1166.79/296.73 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 1166.79/296.73 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 1166.79/296.73 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 1166.79/296.73 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 1166.79/296.73 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 1166.79/296.73 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) 1166.79/296.73 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 1166.79/296.73 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 1166.79/296.73 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 1166.79/296.73 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 1166.79/296.73 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 1166.79/296.73 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 1166.79/296.73 Qed 1166.79/296.73 EOF