Inference Steps

Comparing the Artifacts

• Steps in FOF-to-CNF not very interesting
• CNF inference steps (sometimes that's all you get)
  • Subsets not interesting (see No Counting)
  • Interesting for same CNF leaves

Comparing the Proofs

• Measure Jaccard distance between sets
  (larger distance ≡ more different proofs)
• CNF set intersection (same CNF leaves)