\sorts {
	s;
}

\functions {
        s f(s);
        s a;
}

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