YES Problem: q(0(x1)) -> p(p(s(s(0(s(s(s(s(x1))))))))) q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(0(x1)) -> p(s(p(s(0(p(p(p(s(s(s(x1))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(x1)))) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [r](x0) = 12x0, [p](x0) = x0, [s](x0) = x0, [q](x0) = 12x0, [0](x0) = x0 orientation: q(0(x1)) = 12x1 >= x1 = p(p(s(s(0(s(s(s(s(x1))))))))) q(s(x1)) = 12x1 >= 12x1 = p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(0(x1)) = 12x1 >= x1 = p(s(p(s(0(p(p(p(s(s(s(x1))))))))))) r(s(x1)) = 12x1 >= 12x1 = p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = x1 >= x1 = 0(s(s(s(x1)))) problem: q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(x1)))) Matrix Interpretation Processor: dim=4 interpretation: [1 0 0 0] [0 0 0 0] [r](x0) = [0 0 0 0]x0 [0 0 0 0] , [1 0 1 0] [0 0 0 1] [p](x0) = [0 1 0 0]x0 [0 0 0 1] , [1 0 0 0] [0 0 1 0] [s](x0) = [0 0 0 0]x0 [0 1 0 1] , [1 0 0 0] [0 0 0 0] [q](x0) = [0 0 0 0]x0 [0 0 0 0] , [1 1 0 0] [0] [0 1 0 0] [1] [0](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [1] orientation: [1 0 0 0] [1 0 0 0] [0 0 0 0] [0 0 0 0] q(s(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) [0 0 0 0] [0 0 0 0] [1 0 0 0] [1 0 0 0] [0 0 0 0] [0 0 0 0] r(s(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = p(s(p(s(s(q(p(s(p(s(x1)))))))))) [0 0 0 0] [0 0 0 0] [1 0 1 0] [1 0 1 0] [0 1 0 1] [0 0 0 1] p(p(s(x1))) = [0 1 0 1]x1 >= [0 1 0 0]x1 = p(x1) [0 1 0 1] [0 0 0 1] [1 0 0 0] [0 1 0 1] p(s(x1)) = [0 0 1 0]x1 >= x1 = x1 [0 1 0 1] [1 1 0 0] [1] [1 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [1] p(0(x1)) = [0 1 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 0(s(s(s(x1)))) [0 0 0 0] [1] [0 0 0 0] [1] problem: q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 DP Processor: DPs: q#(s(x1)) -> p#(s(s(x1))) q#(s(x1)) -> p#(p(s(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r#(s(x1)) -> p#(s(x1)) r#(s(x1)) -> p#(s(p(s(x1)))) r#(s(x1)) -> q#(p(s(p(s(x1))))) r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) p#(p(s(x1))) -> p#(x1) TRS: q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 TDG Processor: DPs: q#(s(x1)) -> p#(s(s(x1))) q#(s(x1)) -> p#(p(s(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r#(s(x1)) -> p#(s(x1)) r#(s(x1)) -> p#(s(p(s(x1)))) r#(s(x1)) -> q#(p(s(p(s(x1))))) r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) p#(p(s(x1))) -> p#(x1) TRS: q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 graph: r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) r#(s(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) r#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> r#(p(p(s(s(x1))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(p(s(s(x1)))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(s(s(x1))) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> q#(p(s(p(s(x1))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(p(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(x1)) q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> p#(s(s(x1))) -> p#(p(s(x1))) -> p#(x1) EDG Processor: DPs: q#(s(x1)) -> p#(s(s(x1))) q#(s(x1)) -> p#(p(s(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r#(s(x1)) -> p#(s(x1)) r#(s(x1)) -> p#(s(p(s(x1)))) r#(s(x1)) -> q#(p(s(p(s(x1))))) r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) p#(p(s(x1))) -> p#(x1) TRS: q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 graph: r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(s(s(x1))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(p(s(s(x1)))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> r#(p(p(s(s(x1))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(x1)) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(p(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> q#(p(s(p(s(x1))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) CDG Processor: DPs: q#(s(x1)) -> p#(s(s(x1))) q#(s(x1)) -> p#(p(s(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) q#(s(x1)) -> p#(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))) q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r#(s(x1)) -> p#(s(x1)) r#(s(x1)) -> p#(s(p(s(x1)))) r#(s(x1)) -> q#(p(s(p(s(x1))))) r#(s(x1)) -> p#(s(s(q(p(s(p(s(x1)))))))) r#(s(x1)) -> p#(s(p(s(s(q(p(s(p(s(x1)))))))))) p#(p(s(x1))) -> p#(x1) TRS: q(s(x1)) -> p(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) r(s(x1)) -> p(s(p(s(s(q(p(s(p(s(x1)))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 graph: q#(s(x1)) -> p#(p(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/121