|
|
   EvenInteger
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1749-1749 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1902-1903 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1900-1900 | Even integer is a subclass of integer |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 867-867 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 936-936 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1895-1895 | Integer is exhaustively partitioned into odd integer and even integer |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5044-5047 |
|
|
|
|