All4x4Tables: Integrate straggler counterexamples (#324)

Expands the number of finite magmas in All4x4Tables by integrating a
couple of finite magmas which were previously used in counterexamples
elsewhere.

**Benefits:**

* For all these examples, each satisfied and refuted equation was
determined,
      which settled 236 previously unknown anti-implications.
* These examples were put through the proof planner, meaning that while
the
number of magmas serving as counterexamples increased greatly (from 543
to 740) the number of checks the
kernel has to perform remains about the same. The `generate_lean.py`
script can
also prune them using transitive closure whenever new implications are
proven.
    
**The newly added sources:**

* Magmas constructed by the Vampire theorem prover gathered from #276.
     * Two magmas constructed by the Z3 solver gathered from #308.
     * A 5x5 magma manually constructed by Pace Nielsen.

With the importation of the straggler examples, the current set of
Vampire disproofs become redundant, so these are removed. The commit
changes the VampireProven documentation with a bit of explanation about
how Vampire `Disproof*.lean` files will appear when Vampire disproofs
are generated. It also updates the blueprint with more sources of
counterexamples.

Unknowns at 21679.

blueprint/src/chapter/counterexamples.tex

@@ -20,5 +20,7 @@ \chapter{Selected magmas}
   \item The set of strings with $x \circ y$ equal to $y$ when $x=y$ or when $x$ ends with $yyy$, or $xy$ otherwise (see \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/3102.20does.20not.20imply.203176}{this Zulip thread}).
   \item Vector spaces ${\mathbb F}_2^n$ over ${\mathbb F}_2$, which obey Definition \ref{eq1571} (and hence all the subsequent laws mentioned in Theorem \ref{1571_impl}).
   \item Knuth's construction \cite{knuth} of a central groupoid (Definition \ref{eq168}) as follows.  Let $S$ be a (finite) set with a distinguished element $0$, and a binary operation $*$ such that $x*0=0$ and $0*x=x$   for all $x$, and for each $x,y$ there is a unique $z$ with $x*z=y$.  One can then define a central groupoid on $S \times S$ by defining $(a,b) \op (c,d)$ to equal $(b,c)$ if $c,d \neq 0$; $(b,e)$ if $b*e=c$ is non-zero and $d=0$; and $(a*b,0)$ if $c=0$.  One such example in \cite{knuth} is when $S = \{0,1,2\}$ with $1*1=2*1=2$ and $1*2=2*2=1$.
-  \item A magma of cardinality $8$ was \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/using.20z3}{constructed by Z3} to refute an implication.
+  \item Cancellative magmas of orders 7 to 9, found by hand-guided search using various solvers.
+  \item Two magmas of cardinality $8$ were \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/using.20z3}{constructed by Z3}.
+  \item A large number of ad-hoc finite magmas were constructed using the Vampire theorem prover.
 \end{itemize}

equational_theories/Generated/All4x4Tables/README.md

@@ -3,14 +3,16 @@
 The Lean proofs here refute every false implication between two equations that
 has a counterexample in one of the following kinds of structures:
 
-* any `2x2`, `3x3` or `4x4` magma,
-* any cancellative `5x5` magma,
-* one of the 34 cancellative `7x7-9x9` magmas listed in `data/cancellative-manual.txt`.
+* every `2x2`, `3x3` or `4x4` magma,
+* every cancellative `5x5` magma,
+* a motley crew of other `5x5-9x9` finite magmas listed in `data/*.txt`.
 
-The proofs are generated by the following tools:
+Automated tools used to find these counterexamples include:
 
 1. The `2x2-4x4` magmas are brute-forced by a C program and pruned by Python scripts.
-2. The `5x5` magmas are generated using Mace4 and pruned using some Haskell tools.
+2. The `5x5` cancellative magmas are generated using Mace4 and pruned using some Haskell tools.
+3. Some magmas constructed by the Z3 solver, gathered from #308.
+4. A number of magmas constructed by the Vampire theorem prover, gathered from #276.
 
 # 2x2-4x4 magmas (brute-forcing)
 
@@ -50,23 +52,23 @@ and the script re-run to further reduce the size of the theorems.
 The brute-forcing takes a couple hundred CPU hours.
 
 
-# 5x5 cancellative magmas
+# 5x5 and above
 
 Once the 4x4 and smaller magmas have been brute-forced and `refutationsNxN.txt`
-generated, running the following bash scripts:
+generated, run the following bash scripts:
 ```
-MACE4HOME=/path/to/mace4 ./generate_5x5_refutations.sh
+MACE4HOME=/path/to/mace4 ./generate_combined_refutations.sh
 python3 generate_lean.py
 ```
 
 These scripts do the following:
 
 **1.** Use Mace4 to generate a list of all 5x5 cancellative magmas up to isomorphism.
 
-**2.** Take the `refutations.txt` obtained by enumerating 4x4 magmas, combines it with
-the 5x5 cancellative magmas and a hand-curated list of larger cancellative magmas,
-then uses the Haskell tools in `finite_magma_tools` to combine them into a shortlist
-of finite magma refutations which optimally cover the same set of counterexamples
+**2.** Take the `refutationsNxN.txt` files obtained by brute-forcing, combine it with
+the 5x5 cancellative magmas and a hand-curated list of other magmas, then use the
+Haskell tools in `finite_magma_tools` to combine them into a shortlist of finite
+magma refutations which optimally cover the same set of counterexamples
 as all of these. These proofs are output into the `raw_lean_output/` directory.
 
 **3.** Further prune the required `Fact`s using the known positive implications taken