Conclusion

Contributions

• Different proofs are good proofs
  (at least in the TSTP solution library)
• Consideration of artifacts to measure and evaluate
• Clustering coefficient C_sw

Current Work

• Proof combinations
• Unclustered sets expected to produce different proofs
• Difference can be quantified by Jaccard distance or C_sw