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: Arctic Interpretation Processor: dimension: 1 interpretation: [j](x0) = 9x0, [p](x0) = x0, [s](x0) = x0, [i](x0) = 9x0, [0](x0) = 1x0 orientation: i(0(x1)) = 10x1 >= 1x1 = p(s(p(s(0(p(s(p(s(x1))))))))) i(s(x1)) = 9x1 >= 9x1 = p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1)))))))))))))))))) j(0(x1)) = 10x1 >= 1x1 = p(s(p(p(s(s(0(p(s(p(s(x1))))))))))) j(s(x1)) = 9x1 >= 9x1 = s(s(s(s(p(p(s(s(i(p(s(p(s(x1))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = 1x1 >= 1x1 = 0(s(s(s(s(s(s(s(s(x1))))))))) problem: 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)) -> 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))))))))) DP Processor: DPs: 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#(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(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(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#(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#(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(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(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))))) 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)) -> 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) EDG Processor: DPs: 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#(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(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(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#(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)))))))))))))))))) 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#(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#(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#(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(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(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) 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: 4/225