YES(?,O(n^2)) 1174.69/295.65 YES(?,O(n^2)) 1174.69/295.66 1174.69/295.66 Problem: 1174.69/295.66 g(c(x1)) -> g(f(c(x1))) 1174.69/295.66 g(f(c(x1))) -> g(f(f(c(x1)))) 1174.69/295.66 g(g(x1)) -> g(f(g(x1))) 1174.69/295.66 f(f(g(x1))) -> g(f(x1)) 1174.69/295.66 1174.69/295.66 Proof: 1174.69/295.66 Complexity Transformation Processor: 1174.69/295.66 strict: 1174.69/295.66 g(c(x1)) -> g(f(c(x1))) 1174.69/295.66 g(f(c(x1))) -> g(f(f(c(x1)))) 1174.69/295.66 g(g(x1)) -> g(f(g(x1))) 1174.69/295.66 f(f(g(x1))) -> g(f(x1)) 1174.69/295.66 weak: 1174.69/295.66 1174.69/295.66 Root-Labeling Processor: 1174.69/295.66 strict: 1174.69/295.66 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.66 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.66 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.66 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.66 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.66 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.66 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.66 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.66 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.66 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.66 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.66 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.66 weak: 1174.69/295.66 1174.69/295.66 Splitting Processor: 1174.69/295.66 strict: 1174.69/295.66 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.66 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.66 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.66 weak: 1174.69/295.66 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.66 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.66 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.66 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.66 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.66 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.66 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.66 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.66 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.66 Arctic Interpretation Processor: 1174.69/295.66 dimension: 1 1174.69/295.66 interpretation: 1174.69/295.66 [f(g)](x0) = x0, 1174.69/295.66 1174.69/295.66 [g(g)](x0) = x0, 1174.69/295.66 1174.69/295.66 [f(f)](x0) = x0, 1174.69/295.66 1174.69/295.66 [c(f)](x0) = 15x0, 1174.69/295.66 1174.69/295.66 [c(c)](x0) = 11x0, 1174.69/295.66 1174.69/295.66 [f(c)](x0) = x0, 1174.69/295.66 1174.69/295.66 [g(f)](x0) = x0, 1174.69/295.66 1174.69/295.66 [c(g)](x0) = x0, 1174.69/295.66 1174.69/295.66 [g(c)](x0) = 1x0 1174.69/295.66 orientation: 1174.69/295.66 g(c)(c(g)(x1)) = 1x1 >= x1 = g(f)(f(c)(c(g)(x1))) 1174.69/295.66 1174.69/295.66 g(c)(c(f)(x1)) = 16x1 >= 15x1 = g(f)(f(c)(c(f)(x1))) 1174.69/295.66 1174.69/295.66 g(f)(f(f)(f(g)(g(c)(x1)))) = 1x1 >= x1 = g(g)(g(f)(f(c)(x1))) 1174.69/295.66 1174.69/295.66 c(f)(f(f)(f(g)(g(g)(x1)))) = 15x1 >= x1 = c(g)(g(f)(f(g)(x1))) 1174.69/295.66 1174.69/295.66 c(f)(f(f)(f(g)(g(c)(x1)))) = 16x1 >= x1 = c(g)(g(f)(f(c)(x1))) 1174.69/295.66 1174.69/295.66 c(f)(f(f)(f(g)(g(f)(x1)))) = 15x1 >= x1 = c(g)(g(f)(f(f)(x1))) 1174.69/295.66 1174.69/295.66 f(f)(f(f)(f(g)(g(c)(x1)))) = 1x1 >= x1 = f(g)(g(f)(f(c)(x1))) 1174.69/295.66 1174.69/295.66 g(c)(c(c)(x1)) = 12x1 >= 11x1 = g(f)(f(c)(c(c)(x1))) 1174.69/295.66 1174.69/295.66 g(f)(f(c)(c(g)(x1))) = x1 >= x1 = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.66 1174.69/295.66 g(f)(f(c)(c(c)(x1))) = 11x1 >= 11x1 = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.66 1174.69/295.66 g(f)(f(c)(c(f)(x1))) = 15x1 >= 15x1 = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.66 1174.69/295.66 g(g)(g(g)(x1)) = x1 >= x1 = g(f)(f(g)(g(g)(x1))) 1174.69/295.66 1174.69/295.66 g(g)(g(c)(x1)) = 1x1 >= 1x1 = g(f)(f(g)(g(c)(x1))) 1174.69/295.66 1174.69/295.66 g(g)(g(f)(x1)) = x1 >= x1 = g(f)(f(g)(g(f)(x1))) 1174.69/295.66 1174.69/295.66 g(f)(f(f)(f(g)(g(g)(x1)))) = x1 >= x1 = g(g)(g(f)(f(g)(x1))) 1174.69/295.66 1174.69/295.66 g(f)(f(f)(f(g)(g(f)(x1)))) = x1 >= x1 = g(g)(g(f)(f(f)(x1))) 1174.69/295.66 1174.69/295.66 f(f)(f(f)(f(g)(g(g)(x1)))) = x1 >= x1 = f(g)(g(f)(f(g)(x1))) 1174.69/295.66 1174.69/295.66 f(f)(f(f)(f(g)(g(f)(x1)))) = x1 >= x1 = f(g)(g(f)(f(f)(x1))) 1174.69/295.66 problem: 1174.69/295.66 strict: 1174.69/295.66 1174.69/295.66 weak: 1174.69/295.66 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.66 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.66 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.66 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.67 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.67 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.67 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.67 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.67 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.67 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.67 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.67 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.67 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.67 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.67 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.67 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.67 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.67 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.67 Qed 1174.69/295.67 1174.69/295.67 strict: 1174.69/295.67 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.67 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.67 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.67 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.67 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.67 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.67 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.67 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.67 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.67 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.67 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.67 weak: 1174.69/295.67 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.67 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.67 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.67 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.67 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.67 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.67 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.67 Matrix Interpretation Processor: dim=3 1174.69/295.67 1174.69/295.67 max_matrix: 1174.69/295.67 [1 1 1] 1174.69/295.67 [0 0 1] 1174.69/295.67 [0 0 1] 1174.69/295.67 interpretation: 1174.69/295.67 [1 0 0] 1174.69/295.67 [f(g)](x0) = [0 0 0]x0 1174.69/295.67 [0 0 1] , 1174.69/295.67 1174.69/295.67 [1 0 0] [0] 1174.69/295.67 [g(g)](x0) = [0 0 0]x0 + [1] 1174.69/295.67 [0 0 1] [1], 1174.69/295.67 1174.69/295.67 [1 0 1] [0] 1174.69/295.67 [f(f)](x0) = [0 0 0]x0 + [1] 1174.69/295.67 [0 0 1] [0], 1174.69/295.67 1174.69/295.67 [1 0 1] [0] 1174.69/295.67 [c(f)](x0) = [0 0 0]x0 + [1] 1174.69/295.67 [0 0 1] [1], 1174.69/295.67 1174.69/295.67 [1 0 0] 1174.69/295.67 [c(c)](x0) = [0 0 1]x0 1174.69/295.67 [0 0 0] , 1174.69/295.67 1174.69/295.67 [1 0 0] [0] 1174.69/295.67 [f(c)](x0) = [0 0 0]x0 + [1] 1174.69/295.67 [0 0 0] [0], 1174.69/295.67 1174.69/295.67 [1 1 0] [0] 1174.69/295.67 [g(f)](x0) = [0 0 0]x0 + [1] 1174.69/295.67 [0 0 1] [1], 1174.69/295.67 1174.69/295.67 [1 1 0] 1174.69/295.67 [c(g)](x0) = [0 0 0]x0 1174.69/295.67 [0 0 0] , 1174.69/295.67 1174.69/295.67 [1 1 0] [1] 1174.69/295.67 [g(c)](x0) = [0 0 0]x0 + [1] 1174.69/295.67 [0 0 0] [1] 1174.69/295.67 orientation: 1174.69/295.67 [1 0 1] [1] [1 0 0] [1] 1174.69/295.67 g(c)(c(c)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(c)(c(c)(x1))) 1174.69/295.67 [0 0 0] [1] [0 0 0] [1] 1174.69/295.67 1174.69/295.67 [1 1 0] [1] [1 1 0] [1] 1174.69/295.67 g(f)(f(c)(c(g)(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.67 [0 0 0] [1] [0 0 0] [1] 1174.69/295.67 1174.69/295.67 [1 0 0] [1] [1 0 0] [1] 1174.69/295.67 g(f)(f(c)(c(c)(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.67 [0 0 0] [1] [0 0 0] [1] 1174.69/295.67 1174.69/295.67 [1 0 1] [1] [1 0 1] [1] 1174.69/295.67 g(f)(f(c)(c(f)(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.67 [0 0 0] [1] [0 0 0] [1] 1174.69/295.67 1174.69/295.67 [1 0 0] [0] [1 0 0] [0] 1174.69/295.67 g(g)(g(g)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(g)(g(g)(x1))) 1174.69/295.68 [0 0 1] [2] [0 0 1] [2] 1174.69/295.68 1174.69/295.68 [1 1 0] [1] [1 1 0] [1] 1174.69/295.68 g(g)(g(c)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(g)(g(c)(x1))) 1174.69/295.68 [0 0 0] [2] [0 0 0] [2] 1174.69/295.68 1174.69/295.68 [1 1 0] [0] [1 1 0] [0] 1174.69/295.68 g(g)(g(f)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(g)(g(f)(x1))) 1174.69/295.68 [0 0 1] [2] [0 0 1] [2] 1174.69/295.68 1174.69/295.68 [1 0 1] [2] [1 0 0] [0] 1174.69/295.68 g(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(g)(x1))) 1174.69/295.68 [0 0 1] [2] [0 0 1] [2] 1174.69/295.68 1174.69/295.68 [1 1 1] [2] [1 0 1] [1] 1174.69/295.68 g(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(f)(x1))) 1174.69/295.68 [0 0 1] [2] [0 0 1] [2] 1174.69/295.68 1174.69/295.68 [1 0 2] [2] [1 0 0] [0] 1174.69/295.68 f(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = f(g)(g(f)(f(g)(x1))) 1174.69/295.68 [0 0 1] [1] [0 0 1] [1] 1174.69/295.68 1174.69/295.68 [1 1 2] [2] [1 0 1] [1] 1174.69/295.68 f(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = f(g)(g(f)(f(f)(x1))) 1174.69/295.68 [0 0 1] [1] [0 0 1] [1] 1174.69/295.68 1174.69/295.68 [1 1 0] [1] [1 1 0] [1] 1174.69/295.68 g(c)(c(g)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(c)(c(g)(x1))) 1174.69/295.68 [0 0 0] [1] [0 0 0] [1] 1174.69/295.68 1174.69/295.68 [1 0 1] [2] [1 0 1] [1] 1174.69/295.68 g(c)(c(f)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(c)(c(f)(x1))) 1174.69/295.68 [0 0 0] [1] [0 0 0] [1] 1174.69/295.68 1174.69/295.68 [1 1 0] [3] [1 0 0] [1] 1174.69/295.68 g(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(c)(x1))) 1174.69/295.68 [0 0 0] [2] [0 0 0] [2] 1174.69/295.68 1174.69/295.68 [1 0 2] [2] [1 0 0] [1] 1174.69/295.68 c(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = c(g)(g(f)(f(g)(x1))) 1174.69/295.68 [0 0 1] [2] [0 0 0] [0] 1174.69/295.68 1174.69/295.68 [1 1 0] [3] [1 0 0] [2] 1174.69/295.68 c(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = c(g)(g(f)(f(c)(x1))) 1174.69/295.68 [0 0 0] [2] [0 0 0] [0] 1174.69/295.68 1174.69/295.68 [1 1 2] [2] [1 0 1] [2] 1174.69/295.68 c(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = c(g)(g(f)(f(f)(x1))) 1174.69/295.68 [0 0 1] [2] [0 0 0] [0] 1174.69/295.68 1174.69/295.68 [1 1 0] [3] [1 0 0] [1] 1174.69/295.68 f(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = f(g)(g(f)(f(c)(x1))) 1174.69/295.68 [0 0 0] [1] [0 0 0] [1] 1174.69/295.68 problem: 1174.69/295.68 strict: 1174.69/295.68 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.68 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.68 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.68 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.68 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.68 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.68 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.68 weak: 1174.69/295.68 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.68 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.68 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.68 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.68 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.68 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.68 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.68 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.68 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.68 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.68 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.68 Arctic Interpretation Processor: 1174.69/295.68 dimension: 1 1174.69/295.68 interpretation: 1174.69/295.68 [f(g)](x0) = x0, 1174.69/295.68 1174.69/295.68 [g(g)](x0) = x0, 1174.69/295.68 1174.69/295.68 [f(f)](x0) = x0, 1174.69/295.68 1174.69/295.68 [c(f)](x0) = x0, 1174.69/295.68 1174.69/295.68 [c(c)](x0) = 8x0, 1174.69/295.68 1174.69/295.68 [f(c)](x0) = x0, 1174.69/295.68 1174.69/295.68 [g(f)](x0) = x0, 1174.69/295.68 1174.69/295.68 [c(g)](x0) = x0, 1174.69/295.68 1174.69/295.68 [g(c)](x0) = 1x0 1174.69/295.68 orientation: 1174.69/295.68 g(c)(c(c)(x1)) = 9x1 >= 8x1 = g(f)(f(c)(c(c)(x1))) 1174.69/295.68 1174.69/295.68 g(f)(f(c)(c(g)(x1))) = x1 >= x1 = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.68 1174.69/295.68 g(f)(f(c)(c(c)(x1))) = 8x1 >= 8x1 = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.68 1174.69/295.68 g(f)(f(c)(c(f)(x1))) = x1 >= x1 = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.68 1174.69/295.68 g(g)(g(g)(x1)) = x1 >= x1 = g(f)(f(g)(g(g)(x1))) 1174.69/295.68 1174.69/295.68 g(g)(g(c)(x1)) = 1x1 >= 1x1 = g(f)(f(g)(g(c)(x1))) 1174.69/295.68 1174.69/295.68 g(g)(g(f)(x1)) = x1 >= x1 = g(f)(f(g)(g(f)(x1))) 1174.69/295.68 1174.69/295.68 g(f)(f(f)(f(g)(g(g)(x1)))) = x1 >= x1 = g(g)(g(f)(f(g)(x1))) 1174.69/295.68 1174.69/295.68 g(f)(f(f)(f(g)(g(f)(x1)))) = x1 >= x1 = g(g)(g(f)(f(f)(x1))) 1174.69/295.68 1174.69/295.68 f(f)(f(f)(f(g)(g(g)(x1)))) = x1 >= x1 = f(g)(g(f)(f(g)(x1))) 1174.69/295.68 1174.69/295.68 f(f)(f(f)(f(g)(g(f)(x1)))) = x1 >= x1 = f(g)(g(f)(f(f)(x1))) 1174.69/295.68 1174.69/295.68 g(c)(c(g)(x1)) = 1x1 >= x1 = g(f)(f(c)(c(g)(x1))) 1174.69/295.68 1174.69/295.68 g(c)(c(f)(x1)) = 1x1 >= x1 = g(f)(f(c)(c(f)(x1))) 1174.69/295.68 1174.69/295.68 g(f)(f(f)(f(g)(g(c)(x1)))) = 1x1 >= x1 = g(g)(g(f)(f(c)(x1))) 1174.69/295.68 1174.69/295.68 c(f)(f(f)(f(g)(g(g)(x1)))) = x1 >= x1 = c(g)(g(f)(f(g)(x1))) 1174.69/295.68 1174.69/295.68 c(f)(f(f)(f(g)(g(c)(x1)))) = 1x1 >= x1 = c(g)(g(f)(f(c)(x1))) 1174.69/295.68 1174.69/295.68 c(f)(f(f)(f(g)(g(f)(x1)))) = x1 >= x1 = c(g)(g(f)(f(f)(x1))) 1174.69/295.68 1174.69/295.68 f(f)(f(f)(f(g)(g(c)(x1)))) = 1x1 >= x1 = f(g)(g(f)(f(c)(x1))) 1174.69/295.68 problem: 1174.69/295.68 strict: 1174.69/295.68 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.68 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.68 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.68 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.68 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.68 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.68 weak: 1174.69/295.68 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.68 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.68 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.68 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.68 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.68 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.68 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.68 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.68 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.68 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.68 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.68 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.68 Matrix Interpretation Processor: dim=3 1174.69/295.68 1174.69/295.68 max_matrix: 1174.69/295.68 [1 1 1] 1174.69/295.68 [0 0 1] 1174.69/295.68 [0 0 1] 1174.69/295.68 interpretation: 1174.69/295.68 [1 0 0] [0] 1174.69/295.68 [f(g)](x0) = [0 0 0]x0 + [1] 1174.69/295.68 [0 0 0] [0], 1174.69/295.68 1174.69/295.68 [1 1 0] 1174.69/295.68 [g(g)](x0) = [0 0 0]x0 1174.69/295.68 [0 0 0] , 1174.69/295.68 1174.69/295.68 [1 0 0] [0] 1174.69/295.68 [f(f)](x0) = [0 0 1]x0 + [1] 1174.69/295.68 [0 0 0] [1], 1174.69/295.68 1174.69/295.68 [1 1 0] [1] 1174.69/295.68 [c(f)](x0) = [0 0 0]x0 + [1] 1174.69/295.68 [0 0 0] [1], 1174.69/295.68 1174.69/295.68 [1 0 0] 1174.69/295.68 [c(c)](x0) = [0 0 0]x0 1174.69/295.68 [0 0 0] , 1174.69/295.68 1174.69/295.68 [1 0 0] [1] 1174.69/295.68 [f(c)](x0) = [0 0 0]x0 + [0] 1174.69/295.69 [0 0 0] [1], 1174.69/295.69 1174.69/295.69 [1 0 0] 1174.69/295.69 [g(f)](x0) = [0 0 0]x0 1174.69/295.69 [0 0 1] , 1174.69/295.69 1174.69/295.69 [1 0 1] 1174.69/295.69 [c(g)](x0) = [0 0 0]x0 1174.69/295.69 [0 0 0] , 1174.69/295.69 1174.69/295.69 [1 0 0] [1] 1174.69/295.69 [g(c)](x0) = [0 0 0]x0 + [1] 1174.69/295.69 [0 0 1] [1] 1174.69/295.69 orientation: 1174.69/295.69 [1 0 1] [1] [1 0 1] [1] 1174.69/295.69 g(f)(f(c)(c(g)(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [1] 1174.69/295.69 1174.69/295.69 [1 0 0] [1] [1 0 0] [1] 1174.69/295.69 g(f)(f(c)(c(c)(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [1] 1174.69/295.69 1174.69/295.69 [1 1 0] [2] [1 1 0] [2] 1174.69/295.69 g(f)(f(c)(c(f)(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [1] 1174.69/295.69 1174.69/295.69 [1 1 0] [1 1 0] 1174.69/295.69 g(g)(g(g)(x1)) = [0 0 0]x1 >= [0 0 0]x1 = g(f)(f(g)(g(g)(x1))) 1174.69/295.69 [0 0 0] [0 0 0] 1174.69/295.69 1174.69/295.69 [1 0 0] [2] [1 0 0] [1] 1174.69/295.69 g(g)(g(c)(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(g)(g(c)(x1))) 1174.69/295.69 [0 0 0] [0] [0 0 0] [0] 1174.69/295.69 1174.69/295.69 [1 0 0] [1 0 0] 1174.69/295.69 g(g)(g(f)(x1)) = [0 0 0]x1 >= [0 0 0]x1 = g(f)(f(g)(g(f)(x1))) 1174.69/295.69 [0 0 0] [0 0 0] 1174.69/295.69 1174.69/295.69 [1 0 0] [1] [1 0 0] [1] 1174.69/295.69 g(c)(c(c)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = g(f)(f(c)(c(c)(x1))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [1] 1174.69/295.69 1174.69/295.69 [1 1 0] [0] [1 0 0] 1174.69/295.69 g(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = g(g)(g(f)(f(g)(x1))) 1174.69/295.69 [0 0 0] [1] [0 0 0] 1174.69/295.69 1174.69/295.69 [1 0 0] [0] [1 0 0] 1174.69/295.69 g(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = g(g)(g(f)(f(f)(x1))) 1174.69/295.69 [0 0 0] [1] [0 0 0] 1174.69/295.69 1174.69/295.69 [1 1 0] [0] [1 0 0] [0] 1174.69/295.69 f(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(g)(x1))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [0] 1174.69/295.69 1174.69/295.69 [1 0 0] [0] [1 0 0] [0] 1174.69/295.69 f(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(f)(x1))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [0] 1174.69/295.69 1174.69/295.69 [1 0 1] [1] [1 0 1] [1] 1174.69/295.69 g(c)(c(g)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = g(f)(f(c)(c(g)(x1))) 1174.69/295.69 [0 0 0] [1] [0 0 0] [1] 1174.69/295.69 1174.69/295.69 [1 1 0] [2] [1 1 0] [2] 1174.69/295.69 g(c)(c(f)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = g(f)(f(c)(c(f)(x1))) 1174.69/295.69 [0 0 0] [2] [0 0 0] [1] 1174.69/295.69 1174.69/295.69 [1 0 0] [1] [1 0 0] [1] 1174.69/295.69 g(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(g)(g(f)(f(c)(x1))) 1174.69/295.70 [0 0 0] [1] [0 0 0] [0] 1174.69/295.70 1174.69/295.70 [1 1 0] [2] [1 0 0] 1174.69/295.70 c(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = c(g)(g(f)(f(g)(x1))) 1174.69/295.70 [0 0 0] [1] [0 0 0] 1174.69/295.70 1174.69/295.70 [1 0 0] [3] [1 0 0] [2] 1174.69/295.70 c(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = c(g)(g(f)(f(c)(x1))) 1174.69/295.70 [0 0 0] [1] [0 0 0] [0] 1174.69/295.70 1174.69/295.70 [1 0 0] [2] [1 0 0] [1] 1174.69/295.70 c(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = c(g)(g(f)(f(f)(x1))) 1174.69/295.70 [0 0 0] [1] [0 0 0] [0] 1174.69/295.70 1174.69/295.70 [1 0 0] [1] [1 0 0] [1] 1174.69/295.70 f(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(c)(x1))) 1174.69/295.70 [0 0 0] [1] [0 0 0] [0] 1174.69/295.70 problem: 1174.69/295.70 strict: 1174.69/295.70 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.70 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.70 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.70 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.69/295.70 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.69/295.70 weak: 1174.69/295.70 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.69/295.70 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.69/295.70 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.69/295.70 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.69/295.70 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.69/295.70 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.69/295.70 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.69/295.70 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.69/295.70 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.69/295.70 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.69/295.70 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.69/295.70 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.69/295.70 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.69/295.70 Matrix Interpretation Processor: dim=2 1174.69/295.70 1174.69/295.70 max_matrix: 1174.69/295.70 [1 3] 1174.69/295.70 [0 1] 1174.69/295.70 interpretation: 1174.69/295.70 [1 0] 1174.69/295.70 [f(g)](x0) = [0 0]x0, 1174.69/295.70 1174.69/295.70 [1 0] 1174.69/295.70 [g(g)](x0) = [0 0]x0, 1174.69/295.70 1174.69/295.70 [1 0] 1174.69/295.70 [f(f)](x0) = [0 0]x0, 1174.69/295.70 1174.69/295.70 [1 3] 1174.69/295.70 [c(f)](x0) = [0 0]x0, 1174.69/295.70 1174.69/295.70 [1 0] [0] 1174.69/295.70 [c(c)](x0) = [0 0]x0 + [2], 1174.69/295.70 1174.69/295.70 1174.69/295.70 [f(c)](x0) = x0, 1174.69/295.70 1174.69/295.70 [1 2] 1174.69/295.70 [g(f)](x0) = [0 0]x0, 1174.69/295.70 1174.69/295.70 [1 1] 1174.69/295.70 [c(g)](x0) = [0 0]x0, 1174.69/295.70 1174.69/295.70 [1 3] 1174.69/295.70 [g(c)](x0) = [0 0]x0 1174.69/295.70 orientation: 1174.69/295.70 [1 1] [1 1] 1174.69/295.70 g(f)(f(c)(c(g)(x1))) = [0 0]x1 >= [0 0]x1 = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.69/295.70 1174.69/295.70 [1 0] [4] [1 0] 1174.69/295.70 g(f)(f(c)(c(c)(x1))) = [0 0]x1 + [0] >= [0 0]x1 = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.69/295.70 1174.69/295.70 [1 3] [1 3] 1174.69/295.70 g(f)(f(c)(c(f)(x1))) = [0 0]x1 >= [0 0]x1 = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.69/295.70 1174.69/295.70 [1 0] [1 0] 1174.69/295.70 g(g)(g(g)(x1)) = [0 0]x1 >= [0 0]x1 = g(f)(f(g)(g(g)(x1))) 1174.69/295.70 1174.69/295.70 [1 2] [1 2] 1174.69/295.70 g(g)(g(f)(x1)) = [0 0]x1 >= [0 0]x1 = g(f)(f(g)(g(f)(x1))) 1174.69/295.70 1174.69/295.70 [1 3] [1 3] 1174.69/295.70 g(g)(g(c)(x1)) = [0 0]x1 >= [0 0]x1 = g(f)(f(g)(g(c)(x1))) 1174.69/295.70 1174.69/295.70 [1 0] [6] [1 0] [4] 1174.79/295.70 g(c)(c(c)(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = g(f)(f(c)(c(c)(x1))) 1174.79/295.70 1174.79/295.70 [1 0] [1 0] 1174.79/295.70 g(f)(f(f)(f(g)(g(g)(x1)))) = [0 0]x1 >= [0 0]x1 = g(g)(g(f)(f(g)(x1))) 1174.79/295.70 1174.79/295.70 [1 2] [1 0] 1174.79/295.70 g(f)(f(f)(f(g)(g(f)(x1)))) = [0 0]x1 >= [0 0]x1 = g(g)(g(f)(f(f)(x1))) 1174.79/295.70 1174.79/295.70 [1 0] [1 0] 1174.79/295.70 f(f)(f(f)(f(g)(g(g)(x1)))) = [0 0]x1 >= [0 0]x1 = f(g)(g(f)(f(g)(x1))) 1174.79/295.70 1174.79/295.70 [1 2] [1 0] 1174.79/295.70 f(f)(f(f)(f(g)(g(f)(x1)))) = [0 0]x1 >= [0 0]x1 = f(g)(g(f)(f(f)(x1))) 1174.79/295.70 1174.79/295.70 [1 1] [1 1] 1174.79/295.70 g(c)(c(g)(x1)) = [0 0]x1 >= [0 0]x1 = g(f)(f(c)(c(g)(x1))) 1174.79/295.70 1174.79/295.70 [1 3] [1 3] 1174.79/295.70 g(c)(c(f)(x1)) = [0 0]x1 >= [0 0]x1 = g(f)(f(c)(c(f)(x1))) 1174.79/295.70 1174.79/295.70 [1 3] [1 2] 1174.79/295.70 g(f)(f(f)(f(g)(g(c)(x1)))) = [0 0]x1 >= [0 0]x1 = g(g)(g(f)(f(c)(x1))) 1174.79/295.70 1174.79/295.70 [1 0] [1 0] 1174.79/295.70 c(f)(f(f)(f(g)(g(g)(x1)))) = [0 0]x1 >= [0 0]x1 = c(g)(g(f)(f(g)(x1))) 1174.79/295.70 1174.79/295.70 [1 3] [1 2] 1174.79/295.70 c(f)(f(f)(f(g)(g(c)(x1)))) = [0 0]x1 >= [0 0]x1 = c(g)(g(f)(f(c)(x1))) 1174.79/295.70 1174.79/295.70 [1 2] [1 0] 1174.79/295.70 c(f)(f(f)(f(g)(g(f)(x1)))) = [0 0]x1 >= [0 0]x1 = c(g)(g(f)(f(f)(x1))) 1174.79/295.70 1174.79/295.70 [1 3] [1 2] 1174.79/295.70 f(f)(f(f)(f(g)(g(c)(x1)))) = [0 0]x1 >= [0 0]x1 = f(g)(g(f)(f(c)(x1))) 1174.79/295.70 problem: 1174.79/295.70 strict: 1174.79/295.70 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.79/295.70 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.79/295.70 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.79/295.70 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.79/295.70 weak: 1174.79/295.70 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.79/295.70 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.79/295.70 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.79/295.70 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.79/295.70 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.79/295.70 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.79/295.70 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.79/295.70 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.79/295.70 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.79/295.70 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.79/295.70 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.79/295.70 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.79/295.70 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.79/295.70 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.79/295.70 Matrix Interpretation Processor: dim=3 1174.79/295.70 1174.79/295.70 max_matrix: 1174.79/295.70 [1 1 1] 1174.79/295.70 [0 0 1] 1174.79/295.70 [0 0 1] 1174.79/295.70 interpretation: 1174.79/295.70 [1 1 0] [0] 1174.79/295.70 [f(g)](x0) = [0 0 0]x0 + [1] 1174.79/295.70 [0 0 0] [0], 1174.79/295.70 1174.79/295.70 [1 1 1] [0] 1174.79/295.70 [g(g)](x0) = [0 0 0]x0 + [1] 1174.79/295.70 [0 0 0] [0], 1174.79/295.70 1174.79/295.70 [1 0 0] [0] 1174.79/295.70 [f(f)](x0) = [0 0 0]x0 + [1] 1174.79/295.70 [0 0 0] [0], 1174.79/295.70 1174.79/295.70 [1 1 0] [0] 1174.79/295.70 [c(f)](x0) = [0 0 0]x0 + [1] 1174.79/295.70 [0 0 0] [1], 1174.79/295.70 1174.79/295.70 [1 1 0] [0] 1174.79/295.70 [c(c)](x0) = [0 0 0]x0 + [0] 1174.79/295.70 [0 0 0] [1], 1174.79/295.70 1174.79/295.70 [1 1 0] 1174.79/295.70 [f(c)](x0) = [0 0 0]x0 1174.79/295.70 [0 0 1] , 1174.79/295.70 1174.79/295.70 [1 0 1] [0] 1174.79/295.70 [g(f)](x0) = [0 0 0]x0 + [1] 1174.79/295.70 [0 0 0] [0], 1174.79/295.70 1174.79/295.70 [1 1 0] [0] 1174.79/295.71 [c(g)](x0) = [0 0 0]x0 + [1] 1174.79/295.71 [0 0 0] [1], 1174.79/295.71 1174.79/295.71 [1 1 1] [1] 1174.79/295.71 [g(c)](x0) = [0 0 1]x0 + [0] 1174.79/295.71 [0 0 0] [1] 1174.79/295.71 orientation: 1174.79/295.71 [1 1 0] [2] [1 1 0] [1] 1174.79/295.71 g(f)(f(c)(c(g)(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 0] [2] [1 1 0] [1] 1174.79/295.71 g(f)(f(c)(c(f)(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 1] [1] [1 1 1] [1] 1174.79/295.71 g(g)(g(g)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(g)(g(g)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 0 1] [1] [1 0 1] [1] 1174.79/295.71 g(g)(g(f)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(g)(g(f)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 0] [1] [1 1 0] [0] 1174.79/295.71 g(f)(f(c)(c(c)(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 2] [2] [1 1 2] [1] 1174.79/295.71 g(g)(g(c)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(g)(g(c)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 0] [2] [1 1 0] [1] 1174.79/295.71 g(c)(c(c)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(c)(c(c)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 1] [1] [1 1 0] [1] 1174.79/295.71 g(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(g)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 0 1] [1] [1 0 0] [1] 1174.79/295.71 g(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(f)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 1] [1] [1 1 0] [1] 1174.79/295.71 f(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(g)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 0 1] [1] [1 0 0] [1] 1174.79/295.71 f(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(f)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 0] [3] [1 1 0] [2] 1174.79/295.71 g(c)(c(g)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(c)(c(g)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 0] [3] [1 1 0] [2] 1174.79/295.71 g(c)(c(f)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(f)(f(c)(c(f)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 2] [1] [1 1 1] [1] 1174.79/295.71 g(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(c)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 1174.79/295.71 [1 1 1] [2] [1 1 0] [1] 1174.79/295.71 c(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = c(g)(g(f)(f(g)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [1] 1174.79/295.71 1174.79/295.71 [1 1 2] [2] [1 1 1] [1] 1174.79/295.71 c(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = c(g)(g(f)(f(c)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [1] 1174.79/295.71 1174.79/295.71 [1 0 1] [2] [1 0 0] [1] 1174.79/295.71 c(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = c(g)(g(f)(f(f)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [1] 1174.79/295.71 1174.79/295.71 [1 1 2] [1] [1 1 1] [1] 1174.79/295.71 f(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(c)(x1))) 1174.79/295.71 [0 0 0] [0] [0 0 0] [0] 1174.79/295.71 problem: 1174.79/295.71 strict: 1174.79/295.71 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.79/295.71 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.79/295.71 weak: 1174.79/295.71 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.79/295.71 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.79/295.71 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.79/295.71 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.79/295.71 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.79/295.71 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.79/295.71 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.79/295.71 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.79/295.71 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.79/295.71 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.79/295.71 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.79/295.71 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.79/295.71 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.79/295.71 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.79/295.71 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.79/295.71 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.79/295.71 Matrix Interpretation Processor: dim=3 1174.79/295.71 1174.79/295.71 max_matrix: 1174.79/295.71 [1 1 1] 1174.79/295.71 [0 1 1] 1174.79/295.71 [0 0 0] 1174.79/295.71 interpretation: 1174.79/295.71 [1 0 0] 1174.79/295.71 [f(g)](x0) = [0 1 1]x0 1174.79/295.71 [0 0 0] , 1174.79/295.71 1174.79/295.71 [1 0 1] [0] 1174.79/295.71 [g(g)](x0) = [0 1 1]x0 + [0] 1174.79/295.71 [0 0 0] [1], 1174.79/295.71 1174.79/295.71 [1 1 0] 1174.79/295.71 [f(f)](x0) = [0 1 0]x0 1174.79/295.71 [0 0 0] , 1174.79/295.71 1174.79/295.71 [1 0 0] [1] 1174.79/295.71 [c(f)](x0) = [0 0 0]x0 + [1] 1174.79/295.71 [0 0 0] [1], 1174.79/295.71 1174.79/295.71 [1 1 0] 1174.79/295.71 [c(c)](x0) = [0 0 0]x0 1174.79/295.71 [0 0 0] , 1174.79/295.71 1174.79/295.71 [1 1 1] 1174.79/295.71 [f(c)](x0) = [0 0 0]x0 1174.79/295.71 [0 0 0] , 1174.79/295.71 1174.79/295.71 [1 0 0] [0] 1174.79/295.71 [g(f)](x0) = [0 1 0]x0 + [0] 1174.79/295.71 [0 0 0] [1], 1174.79/295.71 1174.79/295.71 [1 0 0] 1174.79/295.71 [c(g)](x0) = [0 0 0]x0 1174.79/295.71 [0 0 0] , 1174.79/295.71 1174.79/295.71 [1 1 1] [0] 1174.79/295.71 [g(c)](x0) = [0 1 0]x0 + [0] 1174.79/295.71 [0 0 0] [1] 1174.79/295.71 orientation: 1174.79/295.71 [1 0 1] [1] [1 0 1] [0] 1174.79/295.71 g(g)(g(g)(x1)) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = g(f)(f(g)(g(g)(x1))) 1174.79/295.71 [0 0 0] [1] [0 0 0] [1] 1174.79/295.71 1174.79/295.71 [1 0 0] [1] [1 0 0] [0] 1174.79/295.71 g(g)(g(f)(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = g(f)(f(g)(g(f)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 0 0] [0] [1 0 0] [0] 1174.79/295.72 g(f)(f(c)(c(g)(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(f)(f(c)(c(g)(x1)))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 0 0] [3] [1 0 0] [3] 1174.79/295.72 g(f)(f(c)(c(f)(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(f)(f(c)(c(f)(x1)))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 1 0] [0] [1 1 0] [0] 1174.79/295.72 g(f)(f(c)(c(c)(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(f)(f(c)(c(c)(x1)))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 1 1] [1] [1 1 1] [0] 1174.79/295.72 g(g)(g(c)(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = g(f)(f(g)(g(c)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 1 0] [0] [1 1 0] [0] 1174.79/295.72 g(c)(c(c)(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(c)(c(c)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 1 2] [1] [1 0 0] [1] 1174.79/295.72 g(f)(f(f)(f(g)(g(g)(x1)))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = g(g)(g(f)(f(g)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 1 0] [1] [1 1 0] [1] 1174.79/295.72 g(f)(f(f)(f(g)(g(f)(x1)))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = g(g)(g(f)(f(f)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 2 3] [2] [1 0 0] [0] 1174.79/295.72 f(f)(f(f)(f(g)(g(g)(x1)))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = f(g)(g(f)(f(g)(x1))) 1174.79/295.72 [0 0 0] [0] [0 0 0] [0] 1174.79/295.72 1174.79/295.72 [1 2 0] [2] [1 1 0] [0] 1174.79/295.72 f(f)(f(f)(f(g)(g(f)(x1)))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = f(g)(g(f)(f(f)(x1))) 1174.79/295.72 [0 0 0] [0] [0 0 0] [0] 1174.79/295.72 1174.79/295.72 [1 0 0] [0] [1 0 0] [0] 1174.79/295.72 g(c)(c(g)(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = g(f)(f(c)(c(g)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 0 0] [3] [1 0 0] [3] 1174.79/295.72 g(c)(c(f)(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = g(f)(f(c)(c(f)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 2 1] [1] [1 1 1] [1] 1174.79/295.72 g(f)(f(f)(f(g)(g(c)(x1)))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = g(g)(g(f)(f(c)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] [1] 1174.79/295.72 1174.79/295.72 [1 1 2] [2] [1 0 0] 1174.79/295.72 c(f)(f(f)(f(g)(g(g)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = c(g)(g(f)(f(g)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] 1174.79/295.72 1174.79/295.72 [1 2 1] [2] [1 1 1] 1174.79/295.72 c(f)(f(f)(f(g)(g(c)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = c(g)(g(f)(f(c)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] 1174.79/295.72 1174.79/295.72 [1 1 0] [2] [1 1 0] 1174.79/295.72 c(f)(f(f)(f(g)(g(f)(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = c(g)(g(f)(f(f)(x1))) 1174.79/295.72 [0 0 0] [1] [0 0 0] 1174.79/295.72 1174.79/295.72 [1 3 1] [2] [1 1 1] [0] 1174.79/295.72 f(f)(f(f)(f(g)(g(c)(x1)))) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [1] = f(g)(g(f)(f(c)(x1))) 1174.79/295.72 [0 0 0] [0] [0 0 0] [0] 1174.79/295.72 problem: 1174.79/295.72 strict: 1174.79/295.72 1174.79/295.72 weak: 1174.79/295.72 g(g)(g(g)(x1)) -> g(f)(f(g)(g(g)(x1))) 1174.79/295.72 g(g)(g(f)(x1)) -> g(f)(f(g)(g(f)(x1))) 1174.79/295.72 g(f)(f(c)(c(g)(x1))) -> g(f)(f(f)(f(c)(c(g)(x1)))) 1174.79/295.72 g(f)(f(c)(c(f)(x1))) -> g(f)(f(f)(f(c)(c(f)(x1)))) 1174.79/295.72 g(f)(f(c)(c(c)(x1))) -> g(f)(f(f)(f(c)(c(c)(x1)))) 1174.79/295.72 g(g)(g(c)(x1)) -> g(f)(f(g)(g(c)(x1))) 1174.79/295.72 g(c)(c(c)(x1)) -> g(f)(f(c)(c(c)(x1))) 1174.79/295.72 g(f)(f(f)(f(g)(g(g)(x1)))) -> g(g)(g(f)(f(g)(x1))) 1174.79/295.72 g(f)(f(f)(f(g)(g(f)(x1)))) -> g(g)(g(f)(f(f)(x1))) 1174.79/295.72 f(f)(f(f)(f(g)(g(g)(x1)))) -> f(g)(g(f)(f(g)(x1))) 1174.79/295.72 f(f)(f(f)(f(g)(g(f)(x1)))) -> f(g)(g(f)(f(f)(x1))) 1174.79/295.72 g(c)(c(g)(x1)) -> g(f)(f(c)(c(g)(x1))) 1174.79/295.72 g(c)(c(f)(x1)) -> g(f)(f(c)(c(f)(x1))) 1174.79/295.72 g(f)(f(f)(f(g)(g(c)(x1)))) -> g(g)(g(f)(f(c)(x1))) 1174.79/295.72 c(f)(f(f)(f(g)(g(g)(x1)))) -> c(g)(g(f)(f(g)(x1))) 1174.79/295.72 c(f)(f(f)(f(g)(g(c)(x1)))) -> c(g)(g(f)(f(c)(x1))) 1174.79/295.72 c(f)(f(f)(f(g)(g(f)(x1)))) -> c(g)(g(f)(f(f)(x1))) 1174.79/295.72 f(f)(f(f)(f(g)(g(c)(x1)))) -> f(g)(g(f)(f(c)(x1))) 1174.79/295.72 Qed 1174.79/295.73 EOF