| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1669-1669 | 子類 Abstract and Entity |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1942-1942 | 子類 流程任務 and Abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1694-1694 | 子類 Quantity and Abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1700-1700 | 子類 Attribute and Abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2128-2128 | 子類 SetOrClass and Abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2159-2159 | 子類 Relation and Abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2875-2875 | 子類 List and Abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3555-3555 | 子類 Proposition and Abstract |
|
|