A Survey of Failures
Bob Veroff

In this talk, I will describe three problems that appear to me to be
especially difficult for Prover9.  Each has syntactic properties that
make it different than problems I typically work on, and I'm interested
in developing new strategies that will be effective for problems having
these properties.

The first problem consists of equality units and a single clause with
four positive equality literals that appears to play a key role in any
proof.  The second problem tends to generate clauses that are ground or
nearly ground.  The third problem has a large number of axioms, defining
a relatively large number of functions and predicates.

The first problem is not open, but I have not seen a known proof and have
resisted looking at one for guidance.  The second and third problems are
open and may not have proofs.