Short Proofs

Short Proofs of ...

• T1, (T2 & T3), A3, A6
• From A1, A2, A4, A5, A8, A9
• Avoiding A3, A6, A7

Technique

• Start with an existing proof
• Demodulate formulae in proof to junk
• Search forced into a new direction

Results

• 24 step proof of T1 (down from 42)
• 43 step proof of (T2 & T3) (down from 80)
• 20 step proof of A3