Hoops Problem

December 2014

Here is a Prover9 proof for a hoops problem posed by Rob Arthan and Paulo Oliva.

The proof is a strictly-forward demodulation-free derivation of the main conjecture. This essentially is a proof-checking run, since it includes steps from a previously found proof as hints. The original proof was found using the method of proof sketches.

Proof. (in, out, pf, xml)

Update (January 2015)

The previous proof is for a formulation of the problem that includes a predicate for a partial order relation and non-unit Horn clauses. After this was posted, Michael Kinyon used Waldmeister to get a proof for a strict equality formulation of the problem. Using that and hints from the above proof, he was able to get a Prover9 proof.

Proof. (in, out, pf, xml)