YES Problem: a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1)))))))))) b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1)))))))))))) c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 Proof: DP Processor: DPs: a#(s(x1)) -> p#(s(s(x1))) a#(s(x1)) -> p#(p(s(s(x1)))) a#(s(x1)) -> b#(p(p(s(s(x1))))) a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) b#(s(x1)) -> p#(s(x1)) b#(s(x1)) -> p#(s(p(s(x1)))) b#(s(x1)) -> c#(p(s(p(s(x1))))) b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) c#(s(x1)) -> p#(s(x1)) c#(s(x1)) -> p#(s(p(s(x1)))) c#(s(x1)) -> a#(p(s(p(s(x1))))) c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1)))))))))) b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1)))))))))))) c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 TDG Processor: DPs: a#(s(x1)) -> p#(s(s(x1))) a#(s(x1)) -> p#(p(s(s(x1)))) a#(s(x1)) -> b#(p(p(s(s(x1))))) a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) b#(s(x1)) -> p#(s(x1)) b#(s(x1)) -> p#(s(p(s(x1)))) b#(s(x1)) -> c#(p(s(p(s(x1))))) b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) c#(s(x1)) -> p#(s(x1)) c#(s(x1)) -> p#(s(p(s(x1)))) c#(s(x1)) -> a#(p(s(p(s(x1))))) c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1)))))))))) b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1)))))))))))) c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 graph: c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) c#(s(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) c#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> b#(p(p(s(s(x1))))) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> p#(p(s(s(x1)))) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> p#(s(s(x1))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> a#(p(s(p(s(x1))))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(p(s(x1)))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(x1)) b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) b#(s(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) b#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> c#(p(s(p(s(x1))))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(s(p(s(x1)))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(s(x1)) a#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) a#(s(x1)) -> p#(s(s(x1))) -> p#(p(s(x1))) -> p#(x1) EDG Processor: DPs: a#(s(x1)) -> p#(s(s(x1))) a#(s(x1)) -> p#(p(s(s(x1)))) a#(s(x1)) -> b#(p(p(s(s(x1))))) a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) b#(s(x1)) -> p#(s(x1)) b#(s(x1)) -> p#(s(p(s(x1)))) b#(s(x1)) -> c#(p(s(p(s(x1))))) b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) c#(s(x1)) -> p#(s(x1)) c#(s(x1)) -> p#(s(p(s(x1)))) c#(s(x1)) -> a#(p(s(p(s(x1))))) c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1)))))))))) b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1)))))))))))) c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 graph: c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> p#(s(s(x1))) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> p#(p(s(s(x1)))) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> b#(p(p(s(s(x1))))) c#(s(x1)) -> a#(p(s(p(s(x1))))) -> a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(x1)) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(p(s(x1)))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> a#(p(s(p(s(x1))))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) b#(s(x1)) -> c#(p(s(p(s(x1))))) -> c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(s(x1)) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(s(p(s(x1)))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> c#(p(s(p(s(x1))))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) a#(s(x1)) -> b#(p(p(s(s(x1))))) -> b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) a#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) CDG Processor: DPs: a#(s(x1)) -> p#(s(s(x1))) a#(s(x1)) -> p#(p(s(s(x1)))) a#(s(x1)) -> b#(p(p(s(s(x1))))) a#(s(x1)) -> p#(s(b(p(p(s(s(x1))))))) b#(s(x1)) -> p#(s(x1)) b#(s(x1)) -> p#(s(p(s(x1)))) b#(s(x1)) -> c#(p(s(p(s(x1))))) b#(s(x1)) -> p#(s(s(c(p(s(p(s(x1)))))))) b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) c#(s(x1)) -> p#(s(x1)) c#(s(x1)) -> p#(s(p(s(x1)))) c#(s(x1)) -> a#(p(s(p(s(x1))))) c#(s(x1)) -> p#(s(a(p(s(p(s(x1))))))) c#(s(x1)) -> p#(s(p(s(a(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: a(s(x1)) -> s(s(s(p(s(b(p(p(s(s(x1)))))))))) b(s(x1)) -> s(s(s(p(p(s(s(c(p(s(p(s(x1)))))))))))) c(s(x1)) -> p(s(p(s(a(p(s(p(s(x1))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 graph: b#(s(x1)) -> p#(p(s(s(c(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) a#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/225