(VAR x1 ) (RULES p(0(x1)) -> s(s(0(s(s(p(x1)))))) p(s(0(x1))) -> 0(x1) p(s(s(x1))) -> s(p(s(x1))) f(s(x1)) -> g(q(i(x1))) g(x1) -> f(p(p(x1))) q(i(x1)) -> q(s(x1)) q(s(x1)) -> s(s(x1)) i(x1) -> s(x1) )