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: DP Processor: DPs: q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) 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#(0(x1)) -> p#(s(s(s(x1)))) r#(0(x1)) -> p#(p(s(s(s(x1))))) r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(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(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)))) TDG Processor: DPs: q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) 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#(0(x1)) -> p#(s(s(s(x1)))) r#(0(x1)) -> p#(p(s(s(s(x1))))) r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(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(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)))) 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))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) r#(0(x1)) -> p#(p(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(x1) r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(s(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) r#(0(x1)) -> p#(s(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(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)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(s(s(x1))))))))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(p(s(s(s(x1))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(s(s(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) q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) EDG Processor: DPs: q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) 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#(0(x1)) -> p#(s(s(s(x1)))) r#(0(x1)) -> p#(p(s(s(s(x1))))) r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(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(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)))) graph: r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) r#(s(x1)) -> q#(p(s(p(s(x1))))) -> q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) 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))))))))))))) r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) r#(0(x1)) -> p#(p(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(s(s(s(x1)))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(p(s(s(s(x1))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) q#(s(x1)) -> r#(p(p(s(s(x1))))) -> r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(s(s(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) q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) CDG Processor: DPs: q#(0(x1)) -> p#(s(s(0(s(s(s(s(x1)))))))) q#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) 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#(0(x1)) -> p#(s(s(s(x1)))) r#(0(x1)) -> p#(p(s(s(s(x1))))) r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) r#(0(x1)) -> p#(s(0(p(p(p(s(s(s(x1))))))))) r#(0(x1)) -> p#(s(p(s(0(p(p(p(s(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(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)))) graph: r#(0(x1)) -> p#(p(p(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) r#(0(x1)) -> p#(p(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(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#(0(x1)) -> p#(p(s(s(0(s(s(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/324