diff --git a/ITP/encoding.tex b/ITP/encoding.tex
index 943e612..fdd8e1e 100644
--- a/ITP/encoding.tex
+++ b/ITP/encoding.tex
@@ -176,6 +176,17 @@
 This was done by verifying the unsatisfiability
 of another formula that took 20 seconds to solve.
 
+The artifact for this paper includes scripts to validate any individual subproblem,
+as well as the summary proof that the subproblems cover the search space.
+However, the unsatisfiability of $\phi_{30}$ depends on
+the unsatisfiability of \textit{all} (hundreds of thousands of) subproblems.
+A skeptical reader might wish to examine the proof files for all subproblems,
+but we estimated the total proof size to be tens or hundreds of terabytes,
+far too much to reasonably store and distribute.
+So, the skeptical reader must run the entire 3 CPU year computation.
+We believe this trust story can be somewhat improved,
+but leave such a challenge as future work.
+
 % file-local attic:
 
 % By using the triangulation lemma repeatedly,
diff --git a/ITP/main.bib b/ITP/main.bib
index bd34c0e..53681cd 100644
--- a/ITP/main.bib
+++ b/ITP/main.bib
@@ -671,3 +671,21 @@ @InProceedings{sbva
   IGNOREURN =		{urn:nbn:de:0030-drops-184736},
   doi =		{10.4230/LIPIcs.SAT.2023.11},
 }
+
+@InProceedings{cube_and_conquer,
+author="Heule, Marijn J. H.
+and Kullmann, Oliver
+and Wieringa, Siert
+and Biere, Armin",
+editor="Eder, Kerstin
+and Louren{\c{c}}o, Jo{\~a}o
+and Shehory, Onn",
+title="Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads",
+booktitle="Hardware and Software: Verification and Testing",
+year="2012",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="50--65",
+abstract="Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel.",
+isbn="978-3-642-34188-5"
+}