YES(?,O(n^1)) 98.17/25.28 YES(?,O(n^1)) 98.17/25.29 98.17/25.29 Problem: 98.17/25.29 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.29 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.17/25.29 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.29 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.29 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.29 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.29 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.29 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.29 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.29 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.17/25.29 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.29 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.17/25.29 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.17/25.29 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.29 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.29 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.29 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.29 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.29 98.17/25.29 Proof: 98.17/25.29 Complexity Transformation Processor: 98.17/25.29 strict: 98.17/25.29 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.30 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.30 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.17/25.30 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.30 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.30 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.30 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.30 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.30 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.30 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.30 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.30 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.17/25.30 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.17/25.30 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.17/25.30 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.17/25.30 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.17/25.30 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.17/25.30 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.17/25.30 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.17/25.30 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.31 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.31 weak: 98.27/25.31 98.27/25.31 Matrix Interpretation Processor: dim=1 98.27/25.31 98.27/25.31 max_matrix: 98.27/25.31 1 98.27/25.31 interpretation: 98.27/25.31 [1](x0) = x0 + 16, 98.27/25.31 98.27/25.31 [0](x0) = x0 + 4, 98.27/25.31 98.27/25.31 [2](x0) = x0 + 20 98.27/25.31 orientation: 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(0(1(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(0(2(1(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(1(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 76 = 0(1(1(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(1(2(0(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(1(2(2(0(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 0(1(2(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(2(1(0(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 0(2(1(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 0(2(2(1(0(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 0(2(2(1(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 1(0(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 1(0(2(0(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 64 = 1(0(2(2(0(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 1(0(2(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 76 = 1(1(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 1(2(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 76 = 1(2(1(0(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 1(2(2(0(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 1(2(2(2(0(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 2(1(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.31 98.27/25.31 0(0(1(0(2(x1))))) = x1 + 48 >= x1 + 80 = 2(2(2(1(0(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 64 = 0(1(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 76 = 0(1(1(2(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 0(1(2(2(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 64 = 0(2(1(0(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 0(2(1(2(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 64 = 0(2(2(1(0(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 0(2(2(1(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(0(2(2(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(2(0(2(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(2(2(0(2(x1))))) 98.27/25.31 98.27/25.31 0(1(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(2(2(2(0(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 0(1(2(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 0(2(1(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 64 = 1(0(0(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 76 = 1(0(1(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 64 = 1(0(2(0(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 76 = 1(0(2(1(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 64 = 1(0(2(2(0(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 1(0(2(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 76 = 1(1(0(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 1(2(0(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 76 = 1(2(1(0(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 1(2(2(0(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 1(2(2(2(0(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(0(1(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(0(2(1(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(1(0(2(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(1(2(0(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(1(2(2(0(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(2(0(1(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(2(1(2(0(x1))))) 98.27/25.31 98.27/25.31 1(0(1(0(2(x1))))) = x1 + 60 >= x1 + 80 = 2(2(2(1(0(x1))))) 98.27/25.31 98.27/25.31 1(0(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(0(2(2(2(x1))))) 98.27/25.32 98.27/25.32 1(0(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(2(0(2(2(x1))))) 98.27/25.32 98.27/25.32 1(0(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(2(2(0(2(x1))))) 98.27/25.32 98.27/25.32 1(0(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 1(2(2(2(0(x1))))) 98.27/25.32 98.27/25.32 1(0(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(1(0(2(2(x1))))) 98.27/25.32 98.27/25.32 1(0(2(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 0(1(2(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 0(2(1(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 0(2(2(1(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 64 = 1(0(0(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 76 = 1(0(1(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 64 = 1(0(2(0(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 76 = 1(0(2(1(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 64 = 1(0(2(2(0(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 1(0(2(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 76 = 1(1(0(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 1(2(0(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 76 = 1(2(1(0(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 1(2(2(0(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 1(2(2(2(0(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(0(1(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(1(0(2(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(1(2(0(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(2(0(1(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.32 98.27/25.32 1(1(2(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(2(2(1(0(x1))))) 98.27/25.32 98.27/25.32 1(2(2(0(2(x1))))) = x1 + 80 >= x1 + 80 = 1(0(2(2(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(0(1(2(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(0(2(1(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(1(0(2(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(1(2(0(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(1(2(2(0(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(2(0(1(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(2(1(2(0(x1))))) 98.27/25.32 98.27/25.32 2(0(1(0(2(x1))))) = x1 + 64 >= x1 + 80 = 2(2(2(1(0(x1))))) 98.27/25.32 98.27/25.32 2(1(1(0(2(x1))))) = x1 + 76 >= x1 + 64 = 2(0(1(0(2(x1))))) 98.27/25.32 98.27/25.32 2(1(1(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(0(2(1(2(x1))))) 98.27/25.32 98.27/25.32 2(1(1(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(1(2(0(2(x1))))) 98.27/25.32 98.27/25.32 2(1(1(0(2(x1))))) = x1 + 76 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.32 98.27/25.32 2(1(2(0(2(x1))))) = x1 + 80 >= x1 + 80 = 2(0(1(2(2(x1))))) 98.27/25.32 98.27/25.32 2(1(2(0(2(x1))))) = x1 + 80 >= x1 + 80 = 2(1(0(2(2(x1))))) 98.27/25.32 98.27/25.32 2(1(2(0(2(x1))))) = x1 + 80 >= x1 + 80 = 2(2(1(0(2(x1))))) 98.27/25.32 98.27/25.32 2(1(2(0(2(x1))))) = x1 + 80 >= x1 + 80 = 2(2(2(1(0(x1))))) 98.27/25.32 problem: 98.27/25.32 strict: 98.27/25.32 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.32 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.32 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.27/25.32 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.27/25.32 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.33 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.27/25.33 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.33 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.33 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.33 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.33 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.33 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.33 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.33 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.27/25.33 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.33 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.33 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.33 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.33 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.33 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.33 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.33 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.33 weak: 98.27/25.33 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.33 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.33 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.27/25.33 Matrix Interpretation Processor: dim=1 98.27/25.33 98.27/25.33 max_matrix: 98.27/25.33 1 98.27/25.33 interpretation: 98.27/25.33 [1](x0) = x0 + 4, 98.27/25.33 98.27/25.33 [0](x0) = x0 + 4, 98.27/25.33 98.27/25.33 [2](x0) = x0 98.27/25.33 orientation: 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(0(1(2(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(0(2(1(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(1(0(2(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(1(1(2(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(1(2(0(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(1(2(2(0(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 0(1(2(2(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(2(1(0(2(x1))))) 98.27/25.33 98.27/25.33 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 0(2(1(2(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 0(2(2(1(0(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 0(2(2(1(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(0(2(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(2(0(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(2(2(0(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(0(2(2(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(1(0(2(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(2(0(2(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(2(1(0(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(2(2(0(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(2(2(2(0(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(1(0(2(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.34 98.27/25.34 0(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(2(2(1(0(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 0(1(0(2(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 0(1(1(2(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 0(1(2(2(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 0(2(1(0(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 0(2(1(2(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 0(2(2(1(0(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 0(2(2(1(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(0(2(2(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(0(2(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(2(0(2(x1))))) 98.27/25.34 98.27/25.34 0(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(2(2(0(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 0(1(2(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 0(2(1(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(0(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(1(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(2(0(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(2(1(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(0(2(2(0(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(0(2(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(1(0(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(2(0(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 12 = 1(2(1(0(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(2(2(0(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 1(2(2(2(0(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(0(1(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(0(2(1(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(1(0(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(1(2(0(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(1(2(2(0(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(2(0(1(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(2(1(2(0(x1))))) 98.27/25.34 98.27/25.34 1(0(1(0(2(x1))))) = x1 + 16 >= x1 + 8 = 2(2(2(1(0(x1))))) 98.27/25.34 98.27/25.34 1(0(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(0(2(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(0(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(2(0(2(x1))))) 98.27/25.34 98.27/25.34 1(0(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(2(2(0(x1))))) 98.27/25.34 98.27/25.34 1(0(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(0(2(2(x1))))) 98.27/25.34 98.27/25.34 1(0(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.34 98.27/25.34 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 0(1(2(2(2(x1))))) 98.27/25.34 98.27/25.34 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 0(2(1(2(2(x1))))) 98.27/25.34 98.27/25.34 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 0(2(2(1(2(x1))))) 98.27/25.34 98.27/25.34 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(0(1(2(2(x1))))) 98.27/25.34 98.27/25.34 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(0(2(1(2(x1))))) 98.27/25.34 98.27/25.34 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(0(2(2(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(1(0(2(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(0(2(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(2(1(0(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(2(0(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 1(2(2(2(0(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(0(1(2(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(0(2(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(2(0(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(0(1(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(2(1(0(x1))))) 98.27/25.35 98.27/25.35 1(2(2(0(2(x1))))) = x1 + 8 >= x1 + 8 = 1(0(2(2(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(0(1(2(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(0(2(1(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(0(2(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(2(0(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(2(2(0(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(0(1(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(1(2(0(x1))))) 98.27/25.35 98.27/25.35 2(0(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(2(1(0(x1))))) 98.27/25.35 98.27/25.35 2(1(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(0(2(1(2(x1))))) 98.27/25.35 98.27/25.35 2(1(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(1(2(0(2(x1))))) 98.27/25.35 98.27/25.35 2(1(1(0(2(x1))))) = x1 + 12 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.35 98.27/25.35 2(1(2(0(2(x1))))) = x1 + 8 >= x1 + 8 = 2(0(1(2(2(x1))))) 98.27/25.35 98.27/25.35 2(1(2(0(2(x1))))) = x1 + 8 >= x1 + 8 = 2(1(0(2(2(x1))))) 98.27/25.35 98.27/25.35 2(1(2(0(2(x1))))) = x1 + 8 >= x1 + 8 = 2(2(1(0(2(x1))))) 98.27/25.35 98.27/25.35 2(1(2(0(2(x1))))) = x1 + 8 >= x1 + 8 = 2(2(2(1(0(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(0(0(2(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(0(2(0(2(x1))))) 98.27/25.35 98.27/25.35 1(1(2(0(2(x1))))) = x1 + 12 >= x1 + 12 = 1(0(2(2(0(x1))))) 98.27/25.35 98.27/25.35 2(1(1(0(2(x1))))) = x1 + 12 >= x1 + 12 = 2(0(1(0(2(x1))))) 98.27/25.35 problem: 98.27/25.35 strict: 98.27/25.35 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.35 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.35 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.35 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.35 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.35 weak: 98.27/25.35 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.35 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.27/25.35 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.35 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.35 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.35 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.35 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.35 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.35 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.27/25.35 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.35 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.35 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.35 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.35 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.35 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.27/25.35 Matrix Interpretation Processor: dim=2 98.27/25.35 98.27/25.35 max_matrix: 98.27/25.35 [1 1] 98.27/25.35 [0 0] 98.27/25.35 interpretation: 98.27/25.35 [1 0] [1] 98.27/25.35 [1](x0) = [0 0]x0 + [1], 98.27/25.35 98.27/25.35 [1 1] [0] 98.27/25.35 [0](x0) = [0 0]x0 + [1], 98.27/25.35 98.27/25.35 [1 1] 98.27/25.35 [2](x0) = [0 0]x0 98.27/25.35 orientation: 98.27/25.35 [1 1] [3] [1 1] [2] 98.27/25.35 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(0(2(2(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [3] 98.27/25.35 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(1(2(2(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [2] 98.27/25.35 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(0(2(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [2] 98.27/25.35 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(0(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [3] 98.27/25.35 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(1(2(2(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [3] 98.27/25.35 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(1(2(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [2] 98.27/25.35 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.27/25.35 98.27/25.35 [1 1] [3] [1 1] [3] 98.27/25.36 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [2] [1 1] [1] 98.27/25.36 1(2(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(1(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(0(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(1(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(0(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(0(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [1] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [3] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.36 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.27/25.36 98.27/25.36 [1 1] [3] [1 1] [2] 98.27/25.37 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [1] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [3] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(1(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [3] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(1(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [1] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [3] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [2] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [3] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.27/25.37 98.27/25.37 [1 1] [3] [1 1] [3] 98.27/25.37 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(2(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [2] [1 1] [1] 98.27/25.38 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [2] [1 1] [2] 98.27/25.38 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [2] [1 1] [2] 98.27/25.38 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [2] [1 1] [2] 98.27/25.38 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [2] [1 1] [2] 98.27/25.38 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [2] [1 1] [2] 98.27/25.38 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [1] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(2(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [2] 98.27/25.38 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.27/25.38 98.27/25.38 [1 1] [3] [1 1] [3] 98.27/25.38 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(0(2(x1))))) 98.27/25.38 problem: 98.27/25.38 strict: 98.27/25.38 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.27/25.38 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.27/25.38 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.27/25.38 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.38 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.38 weak: 98.27/25.38 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.27/25.38 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.27/25.38 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.39 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.39 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.39 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.39 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.27/25.39 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.39 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.39 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.39 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.39 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.39 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.39 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.27/25.39 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.27/25.39 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.27/25.39 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.27/25.39 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.27/25.39 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.27/25.39 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.27/25.39 Matrix Interpretation Processor: dim=2 98.27/25.39 98.27/25.39 max_matrix: 98.27/25.39 [1 1] 98.27/25.39 [0 0] 98.27/25.39 interpretation: 98.27/25.39 [1 0] [1] 98.27/25.39 [1](x0) = [0 0]x0 + [1], 98.27/25.39 98.27/25.39 [1 0] [1] 98.27/25.39 [0](x0) = [0 0]x0 + [1], 98.27/25.39 98.27/25.39 [1 1] 98.27/25.39 [2](x0) = [0 0]x0 98.27/25.39 orientation: 98.27/25.39 [1 1] [4] [1 1] [3] 98.27/25.39 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(1(2(2(x1))))) 98.27/25.39 98.27/25.39 [1 1] [4] [1 1] [3] 98.27/25.39 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(1(2(2(x1))))) 98.27/25.39 98.27/25.39 [1 1] [4] [1 1] [4] 98.27/25.39 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(1(2(x1))))) 98.27/25.39 98.27/25.39 [1 1] [4] [1 1] [4] 98.36/25.40 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(0(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [4] 98.36/25.40 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(0(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 0] [4] 98.36/25.40 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(0(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [3] [1 1] [2] 98.36/25.40 1(2(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 0] [3] 98.36/25.40 2(1(2(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(1(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(0(2(1(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(0(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(1(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(0(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 0] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(0(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [2] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(0(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 0] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(0(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 0] [4] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [2] 98.36/25.40 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.40 98.36/25.40 [1 1] [4] [1 1] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [4] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 0] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 0] [3] 98.36/25.41 0(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [2] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [2] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 0] [3] 98.36/25.41 0(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [2] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(1(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [4] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [4] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(1(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 0] [4] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [2] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [3] 98.36/25.41 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.41 98.36/25.41 [1 1] [4] [1 1] [4] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [4] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(2(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [4] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [3] 98.36/25.42 1(0(1(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [2] 98.36/25.42 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [3] 98.36/25.42 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(0(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [2] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(1(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(2(2(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [2] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [4] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(2(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [4] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [3] 98.36/25.42 2(0(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [3] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 0] [4] 98.36/25.42 1(1(2(0(2(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.36/25.42 98.36/25.42 [1 1] [4] [1 1] [4] 98.36/25.42 2(1(1(0(2(x1))))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(0(2(x1))))) 98.36/25.42 problem: 98.36/25.42 strict: 98.36/25.42 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.36/25.42 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.36/25.42 weak: 98.36/25.42 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.36/25.42 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.36/25.42 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.36/25.42 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.36/25.42 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.36/25.42 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.36/25.42 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.36/25.42 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.36/25.42 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.36/25.43 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.36/25.43 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.36/25.43 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.36/25.43 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.36/25.43 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.36/25.43 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.36/25.43 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.36/25.43 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.36/25.43 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.36/25.43 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.36/25.43 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.36/25.43 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.36/25.43 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.36/25.43 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.36/25.44 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.36/25.44 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.36/25.44 Matrix Interpretation Processor: dim=3 98.36/25.44 98.36/25.44 max_matrix: 98.36/25.44 [1 1 1] 98.36/25.44 [0 0 1] 98.36/25.44 [0 0 0] 98.36/25.44 interpretation: 98.36/25.44 [1 1 0] [0] 98.36/25.44 [1](x0) = [0 0 0]x0 + [1] 98.36/25.44 [0 0 0] [1], 98.36/25.44 98.36/25.44 [1 0 0] [1] 98.36/25.44 [0](x0) = [0 0 1]x0 + [0] 98.36/25.44 [0 0 0] [1], 98.36/25.44 98.36/25.44 [1 0 1] 98.36/25.44 [2](x0) = [0 0 0]x0 98.36/25.44 [0 0 0] 98.36/25.44 orientation: 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(1(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(1(2(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(1(2(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 2(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.44 [0 0 0] [0] [0 0 0] [0] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(0(2(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [3] 98.36/25.44 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(1(0(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [3] 98.36/25.44 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(2(1(0(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [2] [1 0 1] [1] 98.36/25.44 1(2(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.44 [0 0 0] [1] [0 0 0] [1] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 2(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.44 [0 0 0] [0] [0 0 0] [0] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 2(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.44 [0 0 0] [0] [0 0 0] [0] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 2(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.44 [0 0 0] [0] [0 0 0] [0] 98.36/25.44 98.36/25.44 [1 0 1] [3] [1 0 1] [2] 98.36/25.44 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(0(1(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(0(2(1(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [2] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(0(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [2] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(1(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(0(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 0] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(2(0(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [1] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(1(0(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [2] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(1(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(2(1(0(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [2] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(2(1(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 0] [3] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [1] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [2] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.36/25.45 [0 0 0] [1] [0 0 0] [1] 98.36/25.45 98.36/25.45 [1 0 1] [3] [1 0 1] [2] 98.36/25.45 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 0] [2] 98.36/25.46 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [0] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [0] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [0] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [1] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(1(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(2(1(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [1] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 0] [2] 98.36/25.46 0(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [1] 98.36/25.46 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [2] 98.36/25.46 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(1(2(2(x1))))) 98.36/25.46 [0 0 0] [1] [0 0 0] [1] 98.36/25.46 98.36/25.46 [1 0 1] [3] [1 0 1] [3] 98.36/25.46 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(1(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [3] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(1(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 0] [3] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [1] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(1(0(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(1(0(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 0] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [1] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [0] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [3] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [0] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [0] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [3] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [0] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 0] [3] 98.36/25.47 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(2(2(0(x1))))) 98.36/25.47 [0 0 0] [1] [0 0 0] [0] 98.36/25.47 98.36/25.47 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [0] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [0] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 0] [3] 98.36/25.48 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(1(2(0(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [0] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [0] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [1] 98.36/25.48 1(0(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 0] [2] 98.36/25.48 1(0(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [0] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(0(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [0] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [1] 98.36/25.48 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(1(2(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(1(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 0(2(2(1(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [1] 98.36/25.48 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(0(2(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 1] [2] 98.36/25.48 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(0(2(x1))))) 98.36/25.48 [0 0 0] [1] [0 0 0] [1] 98.36/25.48 98.36/25.48 [1 0 1] [3] [1 0 0] [2] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(2(2(2(0(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [1] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [3] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.49 [0 0 0] [1] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(0(1(2(2(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [3] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(0(2(2(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [3] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 0] [3] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(2(2(0(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(0(1(2(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 0] [3] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(1(2(0(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [2] 98.36/25.49 2(0(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(2(1(0(x1))))) 98.36/25.49 [0 0 0] [0] [0 0 0] [0] 98.36/25.49 98.36/25.49 [1 0 1] [3] [1 0 1] [3] 98.46/25.50 2(1(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(0(2(1(2(x1))))) 98.46/25.50 [0 0 0] [0] [0 0 0] [0] 98.46/25.50 98.46/25.50 [1 0 1] [3] [1 0 1] [3] 98.46/25.50 2(1(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(1(2(0(2(x1))))) 98.46/25.50 [0 0 0] [0] [0 0 0] [0] 98.46/25.50 98.46/25.50 [1 0 1] [3] [1 0 1] [2] 98.46/25.50 2(1(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(2(1(0(2(x1))))) 98.46/25.50 [0 0 0] [0] [0 0 0] [0] 98.46/25.50 98.46/25.50 [1 0 1] [3] [1 0 1] [3] 98.46/25.50 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(0(2(2(x1))))) 98.46/25.50 [0 0 0] [1] [0 0 0] [1] 98.46/25.50 98.46/25.50 [1 0 1] [3] [1 0 1] [3] 98.46/25.50 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(0(2(x1))))) 98.46/25.50 [0 0 0] [1] [0 0 0] [1] 98.46/25.50 98.46/25.50 [1 0 1] [3] [1 0 0] [3] 98.46/25.50 1(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(0(2(2(0(x1))))) 98.46/25.50 [0 0 0] [1] [0 0 0] [1] 98.46/25.50 98.46/25.50 [1 0 1] [3] [1 0 1] [3] 98.46/25.50 2(1(1(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 2(0(1(0(2(x1))))) 98.46/25.50 [0 0 0] [0] [0 0 0] [0] 98.46/25.50 problem: 98.46/25.50 strict: 98.46/25.50 98.46/25.50 weak: 98.46/25.50 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.46/25.50 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.46/25.50 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.46/25.50 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.46/25.50 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.46/25.50 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.46/25.50 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.46/25.50 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.46/25.50 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.46/25.50 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.46/25.50 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.46/25.50 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.46/25.50 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 98.46/25.50 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 98.46/25.50 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 98.46/25.50 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 98.46/25.50 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 98.46/25.50 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 98.46/25.50 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 98.46/25.50 Qed 98.46/25.51 EOF