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.