YES Problem: i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1))))))))) i(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) Proof: DP Processor: DPs: i#(0(x1)) -> p#(s(x1)) i#(0(x1)) -> p#(s(p(s(x1)))) i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) i#(s(x1)) -> p#(s(s(s(s(x1))))) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j#(0(x1)) -> p#(s(x1)) j#(0(x1)) -> p#(s(p(s(x1)))) j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j#(s(x1)) -> p#(s(x1)) j#(s(x1)) -> p#(s(p(s(x1)))) j#(s(x1)) -> i#(p(s(p(s(x1))))) j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1))))))))) i(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) TDG Processor: DPs: i#(0(x1)) -> p#(s(x1)) i#(0(x1)) -> p#(s(p(s(x1)))) i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) i#(s(x1)) -> p#(s(s(s(s(x1))))) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j#(0(x1)) -> p#(s(x1)) j#(0(x1)) -> p#(s(p(s(x1)))) j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j#(s(x1)) -> p#(s(x1)) j#(s(x1)) -> p#(s(p(s(x1)))) j#(s(x1)) -> i#(p(s(p(s(x1))))) j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1))))))))) i(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) graph: j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) j#(s(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) j#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(s(s(s(x1))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(p(s(x1)))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(x1)) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) j#(0(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) j#(0(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> i#(p(s(p(s(x1))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(s(p(s(x1)))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(s(x1)) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(p(s(x1)))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(x1)) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(s(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(x1) i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) i#(0(x1)) -> p#(s(p(s(x1)))) -> p#(p(s(x1))) -> p#(x1) i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) i#(0(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) EDG Processor: DPs: i#(0(x1)) -> p#(s(x1)) i#(0(x1)) -> p#(s(p(s(x1)))) i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) i#(s(x1)) -> p#(s(s(s(s(x1))))) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j#(0(x1)) -> p#(s(x1)) j#(0(x1)) -> p#(s(p(s(x1)))) j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j#(s(x1)) -> p#(s(x1)) j#(s(x1)) -> p#(s(p(s(x1)))) j#(s(x1)) -> i#(p(s(p(s(x1))))) j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1))))))))) i(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) graph: j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(x1)) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(p(s(x1)))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(s(s(s(x1))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) j#(s(x1)) -> i#(p(s(p(s(x1))))) -> i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(x1)) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(p(s(x1)))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(s(x1)) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(s(p(s(x1)))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> i#(p(s(p(s(x1))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) -> j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) CDG Processor: DPs: i#(0(x1)) -> p#(s(x1)) i#(0(x1)) -> p#(s(p(s(x1)))) i#(0(x1)) -> p#(s(0(p(s(p(s(x1))))))) i#(0(x1)) -> p#(s(p(s(0(p(s(p(s(x1))))))))) i#(s(x1)) -> p#(s(s(s(s(x1))))) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) i#(s(x1)) -> p#(s(p(p(p(p(s(s(s(s(x1)))))))))) i#(s(x1)) -> p#(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))) i#(s(x1)) -> j#(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))) i#(s(x1)) -> p#(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))) i#(s(x1)) -> p#(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j#(0(x1)) -> p#(s(x1)) j#(0(x1)) -> p#(s(p(s(x1)))) j#(0(x1)) -> p#(s(s(0(p(s(p(s(x1)))))))) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) j#(0(x1)) -> p#(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j#(s(x1)) -> p#(s(x1)) j#(s(x1)) -> p#(s(p(s(x1)))) j#(s(x1)) -> i#(p(s(p(s(x1))))) j#(s(x1)) -> p#(s(s(i(p(s(p(s(x1)))))))) j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) p#(p(s(x1))) -> p#(x1) TRS: i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1))))))))) i(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) graph: j#(s(x1)) -> p#(p(s(s(i(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) j#(0(x1)) -> p#(p(s(s(0(p(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(p(p(s(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(p(s(s(s(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) i#(s(x1)) -> p#(p(s(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/576