A Case Study

Encoding of general education requirements at UM ... Composition, Humanities, Science, Mathematics, Social science, Second language, Writing
Conjecture to prove it's possible to complete the requirements
There are alternative ways, i.e., alternative proofs
Three proofs, two by EP and one by Metis
Formula equivalence modulo obvious properties of connectives, variable renaming and reordering, Skolem symbol renaming

Initial target EP1: Art, Biology, Computer Science, Anthropology, Arabic, Philosophy
13 initial self-combining steps, then 5 non-self-combining and 28 more self-combining
- Self-combining steps collapse sequences of equivalent formulae
- 1st non-self-combining step replaces EP1 proof by EP2
- 2nd and 3rd non-self-combining steps bring in EP1 and Metis components
- 4th and 5th non-self-combining steps change inference orders
Final combined proof: Art History (Metis), Biology (EP1), Statistics (EP2), Psychology (EP2), Japanese (EP2), SpecialWriting (EP2)