YES Problem: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 Proof: DP Processor: DPs: P#(x1) -> p#(x1) P#(x1) -> Q#(p(x1)) P#(x1) -> Q#(Q(p(x1))) p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) Q#(p(q(x1))) -> q#(p(Q(x1))) q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> p#(q(q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 TDG Processor: DPs: P#(x1) -> p#(x1) P#(x1) -> Q#(p(x1)) P#(x1) -> Q#(Q(p(x1))) p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) Q#(p(q(x1))) -> q#(p(Q(x1))) q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> p#(q(q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 graph: q#(q(p(x1))) -> q#(q(x1)) -> q#(q(p(x1))) -> p#(q(q(x1))) q#(q(p(x1))) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> q#(x1) -> q#(q(p(x1))) -> p#(q(q(x1))) q#(q(p(x1))) -> q#(x1) -> q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> q#(x1) -> q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(p(x1)) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> p#(x1) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(p(x1)) -> q#(q(x1)) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(p(x1)) -> q#(x1) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> q#(q(x1)) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> q#(x1) Q#(p(q(x1))) -> Q#(x1) -> Q#(p(q(x1))) -> q#(p(Q(x1))) Q#(p(q(x1))) -> Q#(x1) -> Q#(p(q(x1))) -> p#(Q(x1)) Q#(p(q(x1))) -> Q#(x1) -> Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(p(x1)) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> p#(x1) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(p(x1)) -> q#(q(x1)) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(p(x1)) -> q#(x1) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> Q#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> Q#(x1) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> p#(x1) -> p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) -> p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) -> q#(q(p(x1))) -> p#(q(q(x1))) p#(p(x1)) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(q(x1)) p#(p(x1)) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(x1) p#(p(x1)) -> q#(x1) -> q#(q(p(x1))) -> p#(q(q(x1))) p#(p(x1)) -> q#(x1) -> q#(q(p(x1))) -> q#(q(x1)) p#(p(x1)) -> q#(x1) -> q#(q(p(x1))) -> q#(x1) P#(x1) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) P#(x1) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> p#(Q(x1)) P#(x1) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> Q#(x1) P#(x1) -> Q#(p(x1)) -> Q#(p(q(x1))) -> q#(p(Q(x1))) P#(x1) -> Q#(p(x1)) -> Q#(p(q(x1))) -> p#(Q(x1)) P#(x1) -> Q#(p(x1)) -> Q#(p(q(x1))) -> Q#(x1) P#(x1) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) P#(x1) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(p(x1)) P#(x1) -> p#(x1) -> p#(Q(Q(x1))) -> p#(x1) P#(x1) -> p#(x1) -> p#(p(x1)) -> q#(q(x1)) P#(x1) -> p#(x1) -> p#(p(x1)) -> q#(x1) SCC Processor: #sccs: 1 #rules: 11 #arcs: 50/196 DPs: q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> p#(q(q(x1))) p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 Arctic Interpretation Processor: dimension: 1 interpretation: [q#](x0) = x0, [Q#](x0) = x0, [p#](x0) = 2x0, [q](x0) = x0, [Q](x0) = x0, [p](x0) = 2x0, [P](x0) = 2x0 + 0 orientation: q#(q(p(x1))) = 2x1 >= x1 = q#(q(x1)) q#(q(p(x1))) = 2x1 >= x1 = q#(x1) q#(q(p(x1))) = 2x1 >= 2x1 = p#(q(q(x1))) p#(p(x1)) = 4x1 >= x1 = q#(x1) p#(p(x1)) = 4x1 >= x1 = q#(q(x1)) p#(Q(Q(x1))) = 2x1 >= 2x1 = p#(x1) p#(Q(Q(x1))) = 2x1 >= 2x1 = Q#(p(x1)) Q#(p(q(x1))) = 2x1 >= x1 = Q#(x1) Q#(p(q(x1))) = 2x1 >= 2x1 = p#(Q(x1)) p#(Q(Q(x1))) = 2x1 >= 2x1 = Q#(Q(p(x1))) Q#(p(q(x1))) = 2x1 >= 2x1 = q#(p(Q(x1))) P(x1) = 2x1 + 0 >= 2x1 = Q(Q(p(x1))) p(p(x1)) = 4x1 >= x1 = q(q(x1)) p(Q(Q(x1))) = 2x1 >= 2x1 = Q(Q(p(x1))) Q(p(q(x1))) = 2x1 >= 2x1 = q(p(Q(x1))) q(q(p(x1))) = 2x1 >= 2x1 = p(q(q(x1))) q(Q(x1)) = x1 >= x1 = x1 Q(q(x1)) = x1 >= x1 = x1 p(P(x1)) = 4x1 + 2 >= x1 = x1 P(p(x1)) = 4x1 + 0 >= x1 = x1 problem: DPs: q#(q(p(x1))) -> p#(q(q(x1))) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 EDG Processor: DPs: q#(q(p(x1))) -> p#(q(q(x1))) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 graph: q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> p#(x1) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(p(x1)) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> p#(x1) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(p(x1)) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) Arctic Interpretation Processor: dimension: 1 interpretation: [q#](x0) = 4x0, [Q#](x0) = 6x0, [p#](x0) = 13x0, [q](x0) = x0, [Q](x0) = 2x0, [p](x0) = 9x0, [P](x0) = 13x0 + 0 orientation: q#(q(p(x1))) = 13x1 >= 13x1 = p#(q(q(x1))) p#(Q(Q(x1))) = 17x1 >= 13x1 = p#(x1) p#(Q(Q(x1))) = 17x1 >= 15x1 = Q#(p(x1)) Q#(p(q(x1))) = 15x1 >= 15x1 = p#(Q(x1)) p#(Q(Q(x1))) = 17x1 >= 17x1 = Q#(Q(p(x1))) Q#(p(q(x1))) = 15x1 >= 15x1 = q#(p(Q(x1))) P(x1) = 13x1 + 0 >= 13x1 = Q(Q(p(x1))) p(p(x1)) = 18x1 >= x1 = q(q(x1)) p(Q(Q(x1))) = 13x1 >= 13x1 = Q(Q(p(x1))) Q(p(q(x1))) = 11x1 >= 11x1 = q(p(Q(x1))) q(q(p(x1))) = 9x1 >= 9x1 = p(q(q(x1))) q(Q(x1)) = 2x1 >= x1 = x1 Q(q(x1)) = 2x1 >= x1 = x1 p(P(x1)) = 22x1 + 9 >= x1 = x1 P(p(x1)) = 22x1 + 0 >= x1 = x1 problem: DPs: q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 EDG Processor: DPs: q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 graph: q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> p#(Q(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [q#](x0) = 8x0, [Q#](x0) = 9x0, [p#](x0) = 15x0, [q](x0) = 1x0, [Q](x0) = 2x0, [p](x0) = 8x0, [P](x0) = 12x0 + 13 orientation: q#(q(p(x1))) = 17x1 >= 17x1 = p#(q(q(x1))) Q#(p(q(x1))) = 18x1 >= 17x1 = p#(Q(x1)) p#(Q(Q(x1))) = 19x1 >= 19x1 = Q#(Q(p(x1))) Q#(p(q(x1))) = 18x1 >= 18x1 = q#(p(Q(x1))) P(x1) = 12x1 + 13 >= 12x1 = Q(Q(p(x1))) p(p(x1)) = 16x1 >= 2x1 = q(q(x1)) p(Q(Q(x1))) = 12x1 >= 12x1 = Q(Q(p(x1))) Q(p(q(x1))) = 11x1 >= 11x1 = q(p(Q(x1))) q(q(p(x1))) = 10x1 >= 10x1 = p(q(q(x1))) q(Q(x1)) = 3x1 >= x1 = x1 Q(q(x1)) = 3x1 >= x1 = x1 p(P(x1)) = 20x1 + 21 >= x1 = x1 P(p(x1)) = 20x1 + 13 >= x1 = x1 problem: DPs: q#(q(p(x1))) -> p#(q(q(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 EDG Processor: DPs: q#(q(p(x1))) -> p#(q(q(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 graph: q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> p#(q(q(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) Matrix Interpretation Processor: dim=4 interpretation: [q#](x0) = [0 0 1 0]x0, [Q#](x0) = [0 0 1 0]x0, [p#](x0) = [1 0 1 0]x0, [0 0 0 1] [0 1 0 0] [q](x0) = [0 0 1 0]x0 [1 0 0 0] , [0 0 0 1] [0] [1 1 0 0] [0] [Q](x0) = [0 0 1 0]x0 + [0] [1 0 0 0] [1], [0 0 0 1] [0 1 0 0] [p](x0) = [1 0 1 0]x0 [1 0 0 0] , [0 0 0 1] [1] [1 1 0 1] [1] [P](x0) = [1 0 1 0]x0 + [0] [1 0 0 0] [1] orientation: q#(q(p(x1))) = [1 0 1 0]x1 >= [1 0 1 0]x1 = p#(q(q(x1))) p#(Q(Q(x1))) = [1 0 1 0]x1 + [1] >= [1 0 1 0]x1 = Q#(Q(p(x1))) Q#(p(q(x1))) = [0 0 1 1]x1 >= [0 0 1 1]x1 = q#(p(Q(x1))) [0 0 0 1] [1] [0 0 0 1] [1] [1 1 0 1] [1] [1 1 0 1] [0] P(x1) = [1 0 1 0]x1 + [0] >= [1 0 1 0]x1 + [0] = Q(Q(p(x1))) [1 0 0 0] [1] [1 0 0 0] [1] [1 0 0 0] [0 1 0 0] p(p(x1)) = [1 0 1 1]x1 >= x1 = q(q(x1)) [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [1] [1 1 0 1] [0] [1 1 0 1] [0] p(Q(Q(x1))) = [1 0 1 0]x1 + [1] >= [1 0 1 0]x1 + [0] = Q(Q(p(x1))) [1 0 0 0] [1] [1 0 0 0] [1] [0 0 0 1] [0] [0 0 0 1] [0] [1 1 0 0] [0] [1 1 0 0] [0] Q(p(q(x1))) = [0 0 1 1]x1 + [0] >= [0 0 1 1]x1 + [0] = q(p(Q(x1))) [1 0 0 0] [1] [1 0 0 0] [1] [0 0 0 1] [0 0 0 1] [0 1 0 0] [0 1 0 0] q(q(p(x1))) = [1 0 1 0]x1 >= [1 0 1 0]x1 = p(q(q(x1))) [1 0 0 0] [1 0 0 0] [1 0 0 0] [1] [1 1 0 0] [0] q(Q(x1)) = [0 0 1 0]x1 + [0] >= x1 = x1 [0 0 0 1] [0] [1 0 0 0] [0] [0 1 0 1] [0] Q(q(x1)) = [0 0 1 0]x1 + [0] >= x1 = x1 [0 0 0 1] [1] [1 0 0 0] [1] [1 1 0 1] [1] p(P(x1)) = [1 0 1 1]x1 + [1] >= x1 = x1 [0 0 0 1] [1] [1 0 0 0] [1] [1 1 0 1] [1] P(p(x1)) = [1 0 1 1]x1 + [0] >= x1 = x1 [0 0 0 1] [1] problem: DPs: q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 EDG Processor: DPs: q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 graph: Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> p#(q(q(x1))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4