CH01.TR1: The challenge you are offered is to automated much of what is detailed in this essay. CH02.TR1: In this challenge, you are asked to extend, modify, and adapt the material presented here whose goal is proof shortening to the goal of proof finding. CH03.TR1: As shorter and still shorter subproofs are found, you are challenged to identify properties of subproofs that strongly suggest progress is being made toward the goal of completing a shorter proof of the final result. CH04.TR1: You are challenged to solve a puzzle that asks you to explain why the following input file yields an 18- step proof of the dependence of A7 when the ratio strategy is used and when level saturation is not, whereas a 20-step proof is returned when the ratio strategy is avoided but level saturation is used. OQ01.TR1: In the BCSK logic, with the axiom set consisting of 1, 2, 4, 5, 8, and 9, does there exist a proof of length strictly less than 14 (applications of the two forms of condensed detachment) showing A3 to be dependent? OQ02.TR1: Does there exist a proof of length strictly less than 24 (applications of the two forms of condensed detachment for the BCSK logic) deriving thesis 1 from the system consisting of 1, 2 4, 5, 8, and 9? OQ03.TR1: With condensed detachment as the only inference rule, and with the only admissible targets for the completion of a proof one of the fourteen shortest single axioms (other than XCB) or the independent 2-basis consisting of symmetry and transitivity, does there exist a proof of length strictly less than 22 that establishes XCB to be a single axiom for EC?