length parameter of formula | |
| | show the first 21 theorems | eliminate pairs of equal variables | |
| show substitution or formula | |
| | 1{p Epq,q EErqEpr,r s}, 1 | | | 4{r Epq,p Erq,q Epr}, 1 | | | | 7{p ErEqp,q EEpqr}, 8 | 2{s EEprEpq,r p,p r}, 9{q r,r Epq} | 5{r Epq,p EpEpq}, 10{r Epq} | | | 2{s EEpqr,r q,q Eqr}, 13{r Epq,q r,p q} | 7{p EpEqr,q EEpqr}, 14 | 9{p Erq,q p,r EpEqr}, 9{p r,r p} | 16{p EEprEqp}, 5{r p,q r,p q} | 16{p EEpqr,q r,r Eqp}, 9 | 10{r EEqrs,q EErqs}, 18{p q,q r,r s} | 10{r EEqrs,q EqErs}, 15{p q,q r,r s} | 7{p EpEEqrs,q EpEqErs}, 20 |
|
|
|
|