Bob Veroff

May 2021

This page provides Web support for A Wos Challenge Met [2]. In particular, it includes the Prover9 [1] files used to work toward a solution to the challenge.

The Challenge

   x * rs(x,y) = y   # label("right solvable").
   rs(x, x * y) = y  # label("right solution is unique").
   ls(x,y) * y = x   # label("left solvable").
   ls(x * y, y) = x  # label("left solution is unique").

   1 * x = x         # label("left identity").
   x * 1 = x         # label("right identity").

   (x * y) * (z * x) = (x * (y * z)) * x # label("M1").
   ((x * y) * z) * y = x * (y * (z * y)) # label("M2").
   x * (y * (x * z)) = ((x * y) * x) * z # label("M3").
   x * ((y * z) * x) = (x * y) * (z * x) # label("M4").

Your challenge (in effect, four challenges) consists in finding four proofs. You might begin by seeking a proof that, from the basic axioms with the Moufang 1 adjoined, you can deduce Moufang 2, with no constraint. Let that be your first challenge.

For the next three challenges, find proofs of Moufang 3 from Moufang 2, Moufang 4 from Moufang 3, and Moufang 1 from Moufang 4, each proof with no constraint.

Then, for the more exciting set of challenges that are consistent with the questions that were open, find the given circle of proofs, but find pure proofs. In other words, the proof of the second from the first must avoid the use of Moufang 3 and Moufang 4 to be pure.

Depending on the program you use -- I had in mind that you would be using an automated reasoning program to meet the challenges -- the last line of each proof might be the so-called flip of the goal. In other words, rather than proving s = t, your program proves t = s. If such is the case, the further challenge -- and not trivial according to my research -- is to prove the various Moufang items as given.

If you have used a Knuth-Bendix approach, the final set of challenges asks for proofs that are free of demodulation and that are forward, rather than backward or bidirectional. If you succeed in finding the four proofs for the circle of pure proofs, you will discover, I feel rather sure, that their lengths differ sharply.

Meeting the Challenge

• M1 => M2
• M2 => M3
• M3 => M4
• M4 => M1

• Find an unconstrained proof that labels any of the undesired clauses that appear for easy identifcation.
• If not already pure, find a pure proof using the unconstrained proof as hints to help guide the search.
• Find a strictly-forward, demodulation-free (sfdf) proof using the pure proof as hints.
• If the derived goal is not equality ordered as specified in the challenge, use a syntactic trick to derive it in the desired order.

After each successful run of Prover9, we extract the resulting proof,

prooftrans -f file.out > file.pf

and hints for use in later runs.

prooftrans expand hints -f file.out > file.hints

M1 => M2

prover9 -f 1to2a.in > 1to2a.out

Extracted files: (pf, hints)

M4 (actually, its flip) appears in the proof (clause 29).

Pure:

prover9 -f 1to2b.in 1to2a.hints > 1to2b.out

Extracted files: (pf, hints)

SFDF:

prover9 -f 1to2c.in 1to2b.hints > 1to2c.out

Extracted files: (pf, hints)

M2 is derived and is equality ordered as specified in the problem statement, which completes M1 => M2.

M2 => M3

prover9 -f 2to3a.in > 2to3a.out

Extracted files: (pf, hints)

M4 (actually, its flip) appears in the proof (clause 20118).

Pure:

prover9 -f 2to3b.in 2to3a.hints > 2to3b.out

Extracted files: (pf, hints)

SFDF:

prover9 -f 2to3c.in 2to3b.hints > 2to3c.out

Extracted files: (pf, hints)

M3 is derived, but it is not equality ordered as specified in the problem statement. We resort to a bit of syntactic trickery to meet the challenge.

Ordered:

prover9 -f 2to3d.in 2to3c.hints > 2to3d.out

Extracted files: (pf, hints)

M3 => M4

For this case, it was helpful to include the additional directive

   set(para_from_small).

prover9 -f 3to4a.in > 3to4a.out

Extracted files: (pf, hints)

M1 appears in the proof (clause 22005).

Pure:

prover9 -f 3to4b.in 3to4a.hints > 3to4b.out

Extracted files: (pf, hints)

SFDF:

prover9 -f 3to4c.in 3to4b.hints > 3to4c.out

Extracted files: (pf, hints)

M4 is derived, but it is not equality ordered as specified in the problem statement.

Ordered:

prover9 -f 3to4d.in 3to4c.hints > 3to4d.out

Extracted files: (pf, hints)

M4 => M1

prover9 -f 4to1a.in > 4to1a.out

Extracted files: (pf, hints)

The resulting proof already is pure.

SFDF:

prover9 -f 4to1c.in 4to1b.hints > 4to1c.out

Extracted files: (pf, hints)

M1 is derived, but it is not equality ordered as specified in the problem statement.

Ordered:

prover9 -f 4to1d.in 4to1c.hints > 4to1d.out

Extracted files: (pf, hints)

Final Results

• M1 => M2
• M2 => M3
• M3 => M4
• M4 => M1

References

1. W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
2. R. Veroff. A Wos Challenge Met. In preparation.