\sorts {
	s;
}

\functions {
        s f(s);
}

\problem {
\forall s x; f(f(x)) = f(x) -> \forall s y; f(y) = f(f(f(y)))
}