Proof Dependence

Avoiding A3 and A6

• Avoid formulae by demodulating to junk
• A3 avoided in proofs of T1 and A6
• A6 seemed necessary for proof of T1
  • A6 used only once in a proof
  • Add preceding deduced formula as axioms
  • BFS for child of A6, avoiding A6, succeeded
• A3 and A6 avoided in proof of T1, using resonators
• A3 and A6 are proof dependent for T1

Avoiding A7

• A3 and A6 proved without A7
• A7 avoided in proof of T1
• A7 is proof dependent for T1