| 0 | 0 | propositional calculus |
| 1 | 0 | propositional theory |
| 2 | 0 | axiom one |
| 3 | 0 | axiom two |
| 4 | 0 | axiom three |
| 5 | 0 | axiom four |
| 6 | 0 | axiom five |
| 7 | 0 | axiom mp |
| 8 | 0 | axiom gen |
| 9 | 0 | mendelson lemma one eight |
| 10 | 0 | mendelson corollary one ten a |
| 11 | 0 | mendelson corollary one ten b |
| 12 | 0 | mendelson lemma one eleven a |
| 13 | 0 | nani teta saka...:13 |
| 14 | 2 | * imply * |
The pyk compiler, version 0.grue.20050502+ by Klaus Grue,