YES Problem: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) Proof: DP Processor: DPs: r#(e(x1)) -> r#(x1) r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> r#(x1) i#(t(x1)) -> e#(r(x1)) e#(w(x1)) -> i#(x1) e#(w(x1)) -> r#(i(x1)) t#(e(x1)) -> r#(e(x1)) w#(r(x1)) -> t#(x1) w#(r(x1)) -> i#(t(x1)) e#(r(x1)) -> w#(x1) e#(r(x1)) -> e#(w(x1)) r#(i(t(e(r(x1))))) -> e#(x1) r#(i(t(e(r(x1))))) -> t#(e(x1)) r#(i(t(e(r(x1))))) -> i#(t(e(x1))) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) TDG Processor: DPs: r#(e(x1)) -> r#(x1) r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> r#(x1) i#(t(x1)) -> e#(r(x1)) e#(w(x1)) -> i#(x1) e#(w(x1)) -> r#(i(x1)) t#(e(x1)) -> r#(e(x1)) w#(r(x1)) -> t#(x1) w#(r(x1)) -> i#(t(x1)) e#(r(x1)) -> w#(x1) e#(r(x1)) -> e#(w(x1)) r#(i(t(e(r(x1))))) -> e#(x1) r#(i(t(e(r(x1))))) -> t#(e(x1)) r#(i(t(e(r(x1))))) -> i#(t(e(x1))) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) graph: t#(e(x1)) -> r#(e(x1)) -> r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) t#(e(x1)) -> r#(e(x1)) -> r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) t#(e(x1)) -> r#(e(x1)) -> r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) t#(e(x1)) -> r#(e(x1)) -> r#(i(t(e(r(x1))))) -> i#(t(e(x1))) t#(e(x1)) -> r#(e(x1)) -> r#(i(t(e(r(x1))))) -> t#(e(x1)) t#(e(x1)) -> r#(e(x1)) -> r#(i(t(e(r(x1))))) -> e#(x1) t#(e(x1)) -> r#(e(x1)) -> r#(e(x1)) -> w#(r(x1)) t#(e(x1)) -> r#(e(x1)) -> r#(e(x1)) -> r#(x1) e#(w(x1)) -> i#(x1) -> i#(t(x1)) -> e#(r(x1)) e#(w(x1)) -> i#(x1) -> i#(t(x1)) -> r#(x1) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> i#(t(e(x1))) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> t#(e(x1)) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> e#(x1) e#(w(x1)) -> r#(i(x1)) -> r#(e(x1)) -> w#(r(x1)) e#(w(x1)) -> r#(i(x1)) -> r#(e(x1)) -> r#(x1) e#(r(x1)) -> e#(w(x1)) -> e#(r(x1)) -> e#(w(x1)) e#(r(x1)) -> e#(w(x1)) -> e#(r(x1)) -> w#(x1) e#(r(x1)) -> e#(w(x1)) -> e#(w(x1)) -> r#(i(x1)) e#(r(x1)) -> e#(w(x1)) -> e#(w(x1)) -> i#(x1) e#(r(x1)) -> w#(x1) -> w#(r(x1)) -> i#(t(x1)) e#(r(x1)) -> w#(x1) -> w#(r(x1)) -> t#(x1) i#(t(x1)) -> e#(r(x1)) -> e#(r(x1)) -> e#(w(x1)) i#(t(x1)) -> e#(r(x1)) -> e#(r(x1)) -> w#(x1) i#(t(x1)) -> e#(r(x1)) -> e#(w(x1)) -> r#(i(x1)) i#(t(x1)) -> e#(r(x1)) -> e#(w(x1)) -> i#(x1) i#(t(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) i#(t(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) i#(t(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) i#(t(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> i#(t(e(x1))) i#(t(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> t#(e(x1)) i#(t(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> e#(x1) i#(t(x1)) -> r#(x1) -> r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> r#(x1) -> r#(e(x1)) -> r#(x1) w#(r(x1)) -> t#(x1) -> t#(e(x1)) -> r#(e(x1)) w#(r(x1)) -> i#(t(x1)) -> i#(t(x1)) -> e#(r(x1)) w#(r(x1)) -> i#(t(x1)) -> i#(t(x1)) -> r#(x1) r#(i(t(e(r(x1))))) -> t#(e(x1)) -> t#(e(x1)) -> r#(e(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) -> e#(r(x1)) -> e#(w(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) -> e#(r(x1)) -> w#(x1) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) -> e#(w(x1)) -> r#(i(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) -> e#(w(x1)) -> i#(x1) r#(i(t(e(r(x1))))) -> e#(x1) -> e#(r(x1)) -> e#(w(x1)) r#(i(t(e(r(x1))))) -> e#(x1) -> e#(r(x1)) -> w#(x1) r#(i(t(e(r(x1))))) -> e#(x1) -> e#(w(x1)) -> r#(i(x1)) r#(i(t(e(r(x1))))) -> e#(x1) -> e#(w(x1)) -> i#(x1) r#(i(t(e(r(x1))))) -> i#(t(e(x1))) -> i#(t(x1)) -> e#(r(x1)) r#(i(t(e(r(x1))))) -> i#(t(e(x1))) -> i#(t(x1)) -> r#(x1) r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) -> w#(r(x1)) -> i#(t(x1)) r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) -> w#(r(x1)) -> t#(x1) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(i(t(e(r(x1))))) -> i#(t(e(x1))) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(i(t(e(r(x1))))) -> t#(e(x1)) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(i(t(e(r(x1))))) -> e#(x1) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(e(x1)) -> w#(r(x1)) r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) -> r#(e(x1)) -> r#(x1) r#(e(x1)) -> w#(r(x1)) -> w#(r(x1)) -> i#(t(x1)) r#(e(x1)) -> w#(r(x1)) -> w#(r(x1)) -> t#(x1) r#(e(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) r#(e(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> w#(r(i(t(e(x1))))) r#(e(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> r#(i(t(e(x1)))) r#(e(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> i#(t(e(x1))) r#(e(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> t#(e(x1)) r#(e(x1)) -> r#(x1) -> r#(i(t(e(r(x1))))) -> e#(x1) r#(e(x1)) -> r#(x1) -> r#(e(x1)) -> w#(r(x1)) r#(e(x1)) -> r#(x1) -> r#(e(x1)) -> r#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [t#](x0) = 10x0, [e#](x0) = 6x0, [i#](x0) = 4x0, [w#](x0) = 6x0, [r#](x0) = 8x0, [i](x0) = x0, [t](x0) = 6x0, [w](x0) = 2x0, [r](x0) = 4x0, [e](x0) = 2x0 orientation: r#(e(x1)) = 10x1 >= 8x1 = r#(x1) r#(e(x1)) = 10x1 >= 10x1 = w#(r(x1)) i#(t(x1)) = 10x1 >= 8x1 = r#(x1) i#(t(x1)) = 10x1 >= 10x1 = e#(r(x1)) e#(w(x1)) = 8x1 >= 4x1 = i#(x1) e#(w(x1)) = 8x1 >= 8x1 = r#(i(x1)) t#(e(x1)) = 12x1 >= 10x1 = r#(e(x1)) w#(r(x1)) = 10x1 >= 10x1 = t#(x1) w#(r(x1)) = 10x1 >= 10x1 = i#(t(x1)) e#(r(x1)) = 10x1 >= 6x1 = w#(x1) e#(r(x1)) = 10x1 >= 8x1 = e#(w(x1)) r#(i(t(e(r(x1))))) = 20x1 >= 6x1 = e#(x1) r#(i(t(e(r(x1))))) = 20x1 >= 12x1 = t#(e(x1)) r#(i(t(e(r(x1))))) = 20x1 >= 12x1 = i#(t(e(x1))) r#(i(t(e(r(x1))))) = 20x1 >= 16x1 = r#(i(t(e(x1)))) r#(i(t(e(r(x1))))) = 20x1 >= 18x1 = w#(r(i(t(e(x1))))) r#(i(t(e(r(x1))))) = 20x1 >= 20x1 = e#(w(r(i(t(e(x1)))))) r(e(x1)) = 6x1 >= 6x1 = w(r(x1)) i(t(x1)) = 6x1 >= 6x1 = e(r(x1)) e(w(x1)) = 4x1 >= 4x1 = r(i(x1)) t(e(x1)) = 8x1 >= 6x1 = r(e(x1)) w(r(x1)) = 6x1 >= 6x1 = i(t(x1)) e(r(x1)) = 6x1 >= 4x1 = e(w(x1)) r(i(t(e(r(x1))))) = 16x1 >= 16x1 = e(w(r(i(t(e(x1)))))) problem: DPs: r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> e#(r(x1)) e#(w(x1)) -> r#(i(x1)) w#(r(x1)) -> t#(x1) w#(r(x1)) -> i#(t(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) EDG Processor: DPs: r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> e#(r(x1)) e#(w(x1)) -> r#(i(x1)) w#(r(x1)) -> t#(x1) w#(r(x1)) -> i#(t(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) graph: e#(w(x1)) -> r#(i(x1)) -> r#(e(x1)) -> w#(r(x1)) e#(w(x1)) -> r#(i(x1)) -> r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) i#(t(x1)) -> e#(r(x1)) -> e#(w(x1)) -> r#(i(x1)) w#(r(x1)) -> i#(t(x1)) -> i#(t(x1)) -> e#(r(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) -> e#(w(x1)) -> r#(i(x1)) r#(e(x1)) -> w#(r(x1)) -> w#(r(x1)) -> t#(x1) r#(e(x1)) -> w#(r(x1)) -> w#(r(x1)) -> i#(t(x1)) SCC Processor: #sccs: 1 #rules: 5 #arcs: 7/36 DPs: e#(w(x1)) -> r#(i(x1)) r#(i(t(e(r(x1))))) -> e#(w(r(i(t(e(x1)))))) r#(e(x1)) -> w#(r(x1)) w#(r(x1)) -> i#(t(x1)) i#(t(x1)) -> e#(r(x1)) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) Matrix Interpretation Processor: dim=4 interpretation: [e#](x0) = [0 0 1 0]x0, [i#](x0) = [0], [w#](x0) = [0], [r#](x0) = [1 0 0 0]x0, [0 0 1 0] [0 1 0 0] [i](x0) = [0 0 0 0]x0 [0 0 0 1] , [0 0 0 1] [1] [0 1 0 0] [0] [t](x0) = [0 0 0 1]x0 + [1] [0 0 0 1] [0], [0 0 0 1] [1] [0 1 0 0] [0] [w](x0) = [0 0 1 0]x0 + [0] [0 0 0 1] [0], [0 0 0 1] [1] [0 1 0 0] [0] [r](x0) = [0 0 0 0]x0 + [0] [0 0 0 1] [0], [1 0 0 0] [0 1 0 0] [e](x0) = [0 0 0 0]x0 [0 0 0 1] orientation: e#(w(x1)) = [0 0 1 0]x1 >= [0 0 1 0]x1 = r#(i(x1)) r#(i(t(e(r(x1))))) = [0 0 0 1]x1 + [1] >= [0] = e#(w(r(i(t(e(x1)))))) r#(e(x1)) = [1 0 0 0]x1 >= [0] = w#(r(x1)) w#(r(x1)) = [0] >= [0] = i#(t(x1)) i#(t(x1)) = [0] >= [0] = e#(r(x1)) [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] r(e(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = w(r(x1)) [0 0 0 1] [0] [0 0 0 1] [0] [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] i(t(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = e(r(x1)) [0 0 0 1] [0] [0 0 0 1] [0] [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] e(w(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = r(i(x1)) [0 0 0 1] [0] [0 0 0 1] [0] [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] t(e(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 + [0] = r(e(x1)) [0 0 0 1] [0] [0 0 0 1] [0] [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] w(r(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = i(t(x1)) [0 0 0 1] [0] [0 0 0 1] [0] [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] e(r(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = e(w(x1)) [0 0 0 1] [0] [0 0 0 1] [0] [0 0 0 1] [1] [0 0 0 1] [1] [0 1 0 0] [0] [0 1 0 0] [0] r(i(t(e(r(x1))))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = e(w(r(i(t(e(x1)))))) [0 0 0 1] [0] [0 0 0 1] [0] problem: DPs: e#(w(x1)) -> r#(i(x1)) r#(e(x1)) -> w#(r(x1)) w#(r(x1)) -> i#(t(x1)) i#(t(x1)) -> e#(r(x1)) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) EDG Processor: DPs: e#(w(x1)) -> r#(i(x1)) r#(e(x1)) -> w#(r(x1)) w#(r(x1)) -> i#(t(x1)) i#(t(x1)) -> e#(r(x1)) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) graph: e#(w(x1)) -> r#(i(x1)) -> r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> e#(r(x1)) -> e#(w(x1)) -> r#(i(x1)) w#(r(x1)) -> i#(t(x1)) -> i#(t(x1)) -> e#(r(x1)) r#(e(x1)) -> w#(r(x1)) -> w#(r(x1)) -> i#(t(x1)) Matrix Interpretation Processor: dim=4 interpretation: [e#](x0) = [0 0 0 1]x0, [i#](x0) = [1 0 0 0]x0, [w#](x0) = [0 0 0 1]x0 + [1], [r#](x0) = [0 0 1 0]x0, [0 0 0 0] [0 1 0 0] [i](x0) = [0 0 0 1]x0 [1 0 0 0] , [1 0 0 1] [0] [1 0 0 1] [0] [t](x0) = [0 0 0 1]x0 + [1] [1 0 0 1] [1], [0 0 0 0] [0] [0 1 0 0] [0] [w](x0) = [0 1 0 0]x0 + [1] [1 0 0 1] [0], [0 0 0 0] [1 0 0 1] [r](x0) = [0 0 1 0]x0 [1 0 0 1] , [0 0 0 0] [0] [0 0 0 1] [0] [e](x0) = [1 0 0 1]x0 + [1] [1 0 0 1] [0] orientation: e#(w(x1)) = [1 0 0 1]x1 >= [0 0 0 1]x1 = r#(i(x1)) r#(e(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = w#(r(x1)) w#(r(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 = i#(t(x1)) i#(t(x1)) = [1 0 0 1]x1 >= [1 0 0 1]x1 = e#(r(x1)) [0 0 0 0] [0] [0 0 0 0] [0] [1 0 0 1] [0] [1 0 0 1] [0] r(e(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = w(r(x1)) [1 0 0 1] [0] [1 0 0 1] [0] [0 0 0 0] [0] [0 0 0 0] [0] [1 0 0 1] [0] [1 0 0 1] [0] i(t(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = e(r(x1)) [1 0 0 1] [0] [1 0 0 1] [0] [0 0 0 0] [0] [0 0 0 0] [1 0 0 1] [0] [1 0 0 0] e(w(x1)) = [1 0 0 1]x1 + [1] >= [0 0 0 1]x1 = r(i(x1)) [1 0 0 1] [0] [1 0 0 0] [1 0 0 1] [0] [0 0 0 0] [0] [1 0 0 1] [0] [1 0 0 1] [0] t(e(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = r(e(x1)) [1 0 0 1] [1] [1 0 0 1] [0] [0 0 0 0] [0] [0 0 0 0] [0] [1 0 0 1] [0] [1 0 0 1] [0] w(r(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = i(t(x1)) [1 0 0 1] [0] [1 0 0 1] [0] [0 0 0 0] [0] [0 0 0 0] [0] [1 0 0 1] [0] [1 0 0 1] [0] e(r(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = e(w(x1)) [1 0 0 1] [0] [1 0 0 1] [0] [0 0 0 0] [0] [0 0 0 0] [0] [1 0 0 1] [0] [1 0 0 1] [0] r(i(t(e(r(x1))))) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = e(w(r(i(t(e(x1)))))) [1 0 0 1] [0] [1 0 0 1] [0] problem: DPs: e#(w(x1)) -> r#(i(x1)) r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> e#(r(x1)) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) EDG Processor: DPs: e#(w(x1)) -> r#(i(x1)) r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> e#(r(x1)) TRS: r(e(x1)) -> w(r(x1)) i(t(x1)) -> e(r(x1)) e(w(x1)) -> r(i(x1)) t(e(x1)) -> r(e(x1)) w(r(x1)) -> i(t(x1)) e(r(x1)) -> e(w(x1)) r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1)))))) graph: e#(w(x1)) -> r#(i(x1)) -> r#(e(x1)) -> w#(r(x1)) i#(t(x1)) -> e#(r(x1)) -> e#(w(x1)) -> r#(i(x1)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/9