  We describe a large-scale project in applied automated deduction concerned
with the following problem of considerable interest in loop theory: If $Q$ is a
loop with commuting inner mappings, does it follow that $Q$ modulo its center
is a group and $Q$ modulo its nucleus is an abelian group? This problem has
been answered affirmatively in several varieties of loops. The solution usually
involves sophisticated techniques of automated deduction, and the resulting
derivations are very long, often with no higher-level human proofs available.
