Term Rewriting System R: [x] f(x) -> f(x) Termination of R to be shown. This program has no overlaps, so it is sufficient to show innermost termination. R contains the following Dependency Pairs: F(x) -> F(x) Furthermore, R contains one SCC. SCC1: F(x) -> F(x) Found an infinite P-chain over R: P = F(x) -> F(x) R = [] s = F(x') evaluates to t = F(x') Thus, s starts an infinite reduction. Non-Termination of R could be shown. Duration: 1.150 seconds.