# QG-Ring Examples from R. Padmanabhan

I asked Padmanabhan for examples for the Milehigh Conference. Here is his response, into which I have inserted (shown in red) the Prover9 and Mace4 jobs he suggested.
```    From: Ranganathan Padmanabhan
Subject: Re: loops, quasigroups, nonassociative systems
Date: Fri, 17 Jun 2005
To: William McCune

On Jun 15, 2005, at 9:43 AM, William McCune wrote:

> RP,
>
> I'll be giving an invited talk on July 7 at the Denver conference
> on loops, quasigroups, and nonassociative systems.  See
>
>         http://www.math.du.edu/milehigh/
>
> This talk will be the official release of Prover9.  I plan to
> give several detailed example problems and proofs, though
> I haven't yet decided on the problems.
>
> Can you suggest some problems that would be of interest to that
> audience?  I'm looking for easy problems as well has medium
> and harder ones, and also counterexample problems for Mace4.

Hi Bill,

Here is a Problem on quasigroups which might be amenable for
treatment by Otter, Mace and Prover9.

A Sample Theorem (due to R.P. and Barry Wolk)

Let K be the set of all algebras of type (2) satisfying the four
identities given below.

1. (x * E) * x = x.
2. x* (x * y) = y.
3. (x * y) * (z * u) = (x * z) * (y * u).
4. ((x * x) * x) * x = ((y * y) * y) * y  (=E).

Then K satisfies all the identities valid in the ring model (Z[7]; 3x-
y). In other words, the variety K has a solvable word problem!
Also every model of K is imbeddable in a quasigroup.

Solution to the word problem is given like this: An identity f=g is a
consequence of {1,2,3,4} if and only if it is true in the ring model
mentioned above.

Applying MACE and OTTER to prove the above statements.

Step#1.
MACE. Get a ring model. A non-trivial one must be x*y = 3x - y (mod 7).
```

mace4 -f ring.in > ring.out ; ### ( ring.out.xml )

```    Step#2.
Use Otter to derive the two cancellation laws.
Right cancellation is obvious: x*y = x*z  => x*(x*y) = x*(x*z)  =>
y=z  by (2).
Left cancellation law: x*z = y*z => x=y also follows from the above
but not obvious and Otter will love proving this.
```

prover9 -f cancel1.in > cancel1.out ; ### ( cancel1.out.xml )
prover9 -f cancel2.in > cancel2.out ; ### ( cancel2.out.xml )

```    Step#3
Prove that E (defined in Id #4) is idempotent.
```

prover9 -f idempotent.in > idempotent.out ; ### ( idempotent.out.xml )

```    Human Steps.
By a result of M. Sholander, any cancellative medial groupoid with an
idempotent element is imbeddable in a medial quasigroup satisfying
the same identities of the original algebra. So any algebra belonging
to K is a sugroupoid of such a quasigroup. Finally, the classic
Toyoda-Bruck theorem asserts that every medial quasigroup is isotopic
to an abelian group i.e. a ring model. So x*y = ax + by and plugging
in the above four equations, one shows that 3x-y (mod 7) is the only
solution for this set of equations.

In particular, the identity ((x * y) * z) * u = ((u * y) * z) * x,
which is true in the ring model 3x-y (mod 7), must now be an
equational  consequence of the four identites. This creates new
problems for Otter, Prover9.
Prove this using Otter or Prover9.
Again, two methods.

Method I
Prove directly    {1,2,3,4} ==> ((x * y) * z) * u = ((u * y) * z) * x.
```

prover9 -f identity.in > identity.out ; ### ( identity.out.xml )

```    Method II.
Prove ((x * y) * z) * u = ((u * y) * z) * x from {1,2,3,4, quasigroup
property, skolemize i.e. type (2,2,2) with*,/,\ }.
```

prover9 -f identity2.in > identity2.out ; ### ( identity2.out.xml )

```    Obviously Method I is preferable.

Thus we have a very good example of a theorem differentiating the
"simplicity-and-elegance" of a human proof compared to the
"complexity-in-details" of a first order proof. Also, there is no
immediate first order human proof of
{1,2,3,4} ==> ((x * y) * z) * u = ((u * y) * z) * x.
But theorem-provers can do this.

Conjecture: This variety defined by the four identities above is one-
based.
If true, only machines can do this (using, of course, human designed
equational filters to eliminate "bad" guys).

Other (relatively easy) Problems:

Prove that x*(y*(y*x)) = y*x  implies y*(y*x) = x*y in quasigroups
```

prover9 -f qg1.in > qg1.out ; ### ( qg1.out.xml )

```    but not in cancellative groupoids.
```

prover9 -t 10 -f qg2.in > qg2.out ; ### ( qg2.out.xml )

(Mace4 cannot help, because it looks for finite models only.)

```    Prove that (xy)(zu) = (xz)(yu) implies (x(yz))((uv)w) = (x(uz))((yv)w)
in cancellation groupoids with an idempotent or under (gL)
but not in general.  (Prover9, Otter with gL), Mace).
```

prover9 -f cg1.in > cg1.out ; ### ( cg1.out.xml )

```    Good luck with your conference.

R. P.
```