#### Problem

Deduce the formula
∀x∀y(∃z(r(z,z,x)&r(z,z,y))→∃w(r(x,x,w)&r(y,y,w))) from the
formulas

∀u∀v∀x∀y(∃z(r(x,z,y)&r(u,z,v))→∃w(r(v,x,w)&r(y,u,w))), ∀u∀x∀y∀z(r(x,u,y)&r(y,u,z)→r(x,u,z)).
**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.