Troubleshooting. The symbols ", $ and ® in the above formulas are intended to be the universal quantifier, the existential quantifier and the implication sign, respectively (using the font "Symbol" characters with ASCII codes 34, 36 and 174). If some of these symbols look differently on your screen, you may browse also a Unicode version of this text that avoids using font "Symbol" characters.
Comments. The formulated logical problem seems to be appropriate for
testing the capabilities of proof search computer programs. It is a refined
formalized version of a statement proved in 1962 by Y. Tagamlitzki
(1917-1983). The straightforward formal presentation of the mentioned
statement in the First Order Predicate Calculus is somewhat more complicated
and makes use also of equality. The original Tagamlitzki's proof was
essentially not a first order one. A first order proof has been found
shortly afterwards by I. Prodanov (1935-1985). In fact, he proved a
statement that is slightly stronger than the original one and that is
expressible in the First Order Predicate Calculus without Equality. About the end of 1983 a corresponding version of the problem has been proposed to J. Siekmann (then in Karlsruhe) for a computer treatment by means of the Markgraf Karl Refutation Procedure (MKRP). Several months passed without a success of MKRP on
this task, therefore we suggested a certain decomposition of the problem on
the base of an easy reformulation. This turned out to be enough for MKRP to
find a solution in May 1984. We made an analysis of that solution and thus
obtained the present formulation of the problem. Although the result becomes
somewhat stronger when using this formulation, it seems that the problem is
less difficult for a computer proof search in the present form than in the
form successfully treated by MKRP. For example, we succeeded in 1998 to
solve the problem in its present form by using Prolog in an appropriate way.