if(Prover9).
assign(order, kbo).
end_if.

formulas(assumptions).

% loop axioms
1 * x = x. x * 1 = x.
x \ (x * y) = y. x * (x \ y) = y.
(x * y) / y = x. (x / y) * y = x.

% Osborn loops (equivalent identities)
((x * (y * x)) / x) * (z * x) = x * ((y * z) * x).
(x * y) * (x \ ((x * z) * x)) = (x * (y * z)) * x.

end_of_list.

formulas(goals).

% The goal is to show that the Osborn identities hold in all 
% (one-sided) isotopes. Either one would be sufficient.

% for right isotopes
%((x * (u \ (y * (u \ x)))) / (u \ x)) * (u \ (z * (u \ x))) = x * (u \ ((y * (u \ z)) * (u \ x))).
% shorter equivalent form:
(((u * x) * (u \ (y * x))) / x) * (u \ (z * x)) = (u * x) * (u \ ((y * (u \ z)) * x)).

% for left isotopes
%(((x / u) * z) / u) * ((x / u) \ ((((x / u) * y) / u) * x)) = (((x / u) * ((z / u) * y)) / u) * x.
% shorter equivalent form
((x * z) / u) * (x \ (((x * y) / u) * (x * u))) = ((x * ((z / u) * y)) / u) * (x * u).

end_of_list.

%BEGIN

1) It isn't known if the two goals are equivalent. 

2) Isotopy invariance of Osborn loops, if true, has structural implications.
In particular, if either of the goals are true, then these equivalent(!)
clauses hold:

% Q/N has the weak inverse property

(x * y) * (z * (u * ((z * u) \ 1))) = x * (y * (z * (u * ((z * u) \ 1)))).
(x * (z * (u * ((z * u) \ 1)))) * y = x * ((z * (u * ((z * u) \ 1))) * y).
(z * (u * ((z * u) \ 1))) * (x * y) = ((z * (u * ((z * u) \ 1))) * x) * y.

(x * y) * (((1 / (z * u)) * z) * u) = x * (y * (((1 / (z * u)) * z) * u)).
(x * (((1 / (z * u)) * z) * u)) * y = x * ((((1 / (z * u)) * z) * u) * y).
((((1 / (z * u)) * z) * u) * x) * y = (((1 / (z * u)) * z) * u) * (x * y).

  a) The equivalence of these six might be useful for proof sketches.

  b) For proof sketches, it might be useful to get proofs that each goal implies
  the immediately preceding six clauses.

  c) It would also be very interesting to *bypass* the goals and *directly*
  prove that Osborn loops satisfy the preceding clauses.

  d) Open: what about the converse? If the six clauses above are *assumed*, does
  that imply the goals? This would be interesting too!

  e) Obviously c) and d) together would settle the whole issue.

END%

%BEGIN

For reasons it would take a while to explain, it might be useful to find proofs
of these clauses for sketches. (It isn't known if they hold!)

x * (u \ ((y * (u \ (u / (u \ x)))) * (u \ x))) = (x * (u \ (y * (u \ x)))) / (u \ x).
(x * (u \ x)) / (u \ ((u * (y \ u)) * (u \ x))) = (x * (u \ (y * (u \ x)))) / (u \ x).

(((x / u) * ((((x / u) \ u) / u) * y)) / u) * x = (x / u) \ ((((x / u) * y) / u) * x).
(((x / u) * ((u / y) * u)) / u) \ ((x / u) * x) = (x / u) \ ((((x / u) * y) / u) * x).

END%

%BEGIN

There are a few 2-variable identities holding in Osborn loops which are of some
interest. To get proof sketches, it might be useful to show that these hold in
isotopes. (It isn't known if they do!)

(u / (u \ x)) * (u \ (x * y)) = x * (u \ ((u * (x \ u)) * y)).
((y * x) / u) * ((x / u) \ u) = ((y * ((u / x) * u)) / u) * x.

(y * (u \ (u / x))) * x = (y * x) * ((u * x) \ u).
x * (((x \ u) / u) * y) = (u / (x * u)) * (x * y).

(u / (u \ x)) * (u \ (x * (u \ ((y * (u \ x)) * (x \ u))))) = y.
(((((u / x) * ((x / u) * y)) / u) * x) / u) * ((x / u) \ u) = y.

END%

%BEGIN

What is quite maddening is that in *every* known proper subvariety of Osborn
loops, the goals hold! So in principle, it should be possible to get good
sketches from many different subvarieties!

% Case 1: Moufang (equivalent identities)
((x * y) * x) * z = x * (y * (x * z)).
((x * y) * z) * y = x * (y * (z * y)).
(x * y) * (z * x) = x * ((y * z) * x).
% this case is very easy, and is implied by even
% simpler equations such as (x * x) * y = x * (x * y), etc.

% Case 2: Conjugacy closed
((x * y) / x) * (x * z) = x * (y * z).
(z * x) * (x \ (y * x)) = (z * y) * x.
% an Osborn loop satisfying either of these satisfies the
% other one, so it might be useful to treat them separately

% Case 3: Generalized Moufang (Osborn with weak inverse property)
x * ((y * x) \ 1) = y \ 1.
(1 / (x * y)) * x = 1 / y.
% these identities are equivalent in Osborn loops

% Case 4: VD loops (VD = Valentin Danielovich)
(x \ (y * x)) * ((x \ (z * x)) * x) = (x \ ((y * z) * x)) * x.
(x * ((x * z) / x)) * ((x * y) / x) = x * ((x * (z * y)) / x).
% an Osborn loop satisfying either of these satisfies the
% other one, so it might be useful to treat them separately

% Case 5: Osborn with nuclear squares (equivalent identities)
(x * x) * (y * z) = ((x * x) * y) * z.
(x * (y * y)) * z = x * ((y * y) * z).
(x * y) * (z * z) = x * (y * (z * z)).

% Case 6: Generalized left and right Bol
(x * (y * x)) * ((1 / x) * (x * z)) = x * (y * (x * z)).
((z * x) * (x \ 1)) * ((x * y) * x) = ((z * x) * y) * x.
% an Osborn loop satisfying either of these satisfies the
% other one, so it might be useful to treat them separately

% By the way, I don't think it's known if cases 3 implies case 6.
% The converse is not true.

END%

%BEGIN

The desired result would still be of interest even in special cases.
It is not known if the goals hold for any of the following classes.

% Case 1: Power associative
(x * x) * x = x * (x * x).
1 / x = x \ 1.

% Case 2: Automorphic inverse property
(x \ 1) * (y \ 1) = (x * y) \ 1.
(1 / x) * (1 / y) = 1 / (x * y).

% Case 2a: Central cubes (implied by AIP)
(x * (x * x)) * y = y * (x * (x * x)).
((x * x) * x) * y = y * ((x * x) * x).
((x * (x * x)) * y) * z = (x * (x * x)) * (y * z).
(y * (x * (x * x))) * z = y * ((x * (x * x)) * z).
(y * z) * (x * (x * x)) = y * (z * (x * (x * x))).
(((x * x) * x) * y) * z = ((x * x) * x) * (y * z).
(y * ((x * x) * x)) * z = y * (((x * x) * x) * z).
(y * z) * ((x * x) * x) = y * (z * ((x * x) * x)).

END%

%BEGIN

Remarks on semantic guidance:

These two properties hold in all Osborn loops, but also
in other varieties, hence are not likely to be crucial
to a proof:

((1 / x) * (x * y)) * ((1 / x) * (x * z)) = (1 / x) * (x * (y * z)).
((y * x) * (x \ 1)) * ((z * x) * (x \ 1)) = ((y * z) * x) * (x \ 1).

In addition, it is very unlikely that any 2-variable consequence
of the Osborn identities will play a significant role in a proof,
because they all hold in many other other varieties as well.

Unfortunately, the smallest model in which the Osborn identities
are false but all the clauses just described are true is the Steiner
loop of order 10. (See below.) So an attack on this problem using
semantic guidance will require very careful memory management.

list(interpretations).
interpretation( 10, [number=1, seconds=2], [
        function(*(_,_), [
			   1, 0, 3, 2, 5, 4, 9, 8, 7, 6,
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
			   3, 2, 1, 0, 6, 8, 4, 9, 5, 7,
			   2, 3, 0, 1, 7, 9, 8, 4, 6, 5,
			   5, 4, 6, 7, 1, 0, 2, 3, 9, 8,
			   4, 5, 8, 9, 0, 1, 7, 6, 2, 3,
			   9, 6, 4, 8, 2, 7, 1, 5, 3, 0,
			   8, 7, 9, 4, 3, 6, 5, 1, 0, 2,
			   7, 8, 5, 6, 9, 2, 3, 0, 1, 4,
			   6, 9, 7, 5, 8, 3, 0, 2, 4, 1 ]),

        function(/(_,_), [
			   1, 0, 3, 2, 5, 4, 9, 8, 7, 6,
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
			   3, 2, 1, 0, 6, 8, 4, 9, 5, 7,
			   2, 3, 0, 1, 7, 9, 8, 4, 6, 5,
			   5, 4, 6, 7, 1, 0, 2, 3, 9, 8,
			   4, 5, 8, 9, 0, 1, 7, 6, 2, 3,
			   9, 6, 4, 8, 2, 7, 1, 5, 3, 0,
			   8, 7, 9, 4, 3, 6, 5, 1, 0, 2,
			   7, 8, 5, 6, 9, 2, 3, 0, 1, 4,
			   6, 9, 7, 5, 8, 3, 0, 2, 4, 1 ]),

        function(\(_,_), [
			   1, 0, 3, 2, 5, 4, 9, 8, 7, 6,
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
			   3, 2, 1, 0, 6, 8, 4, 9, 5, 7,
			   2, 3, 0, 1, 7, 9, 8, 4, 6, 5,
			   5, 4, 6, 7, 1, 0, 2, 3, 9, 8,
			   4, 5, 8, 9, 0, 1, 7, 6, 2, 3,
			   9, 6, 4, 8, 2, 7, 1, 5, 3, 0,
			   8, 7, 9, 4, 3, 6, 5, 1, 0, 2,
			   7, 8, 5, 6, 9, 2, 3, 0, 1, 4,
			   6, 9, 7, 5, 8, 3, 0, 2, 4, 1 ])
]).
end_of_list.

END%