| No TPTP formula. May not be expressible in strict first order. | Government.kif 1692-1698 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3738-3742 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2617-2622 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1496-1518 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1556-1556 | 施事体 是 客体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1566-1566 | 有感知的主事 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14054-14054 | 地缘政治区域 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14355-14355 | 生物 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16173-16173 | 商业代理人 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16224-16224 | 群组 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16610-16610 | 机构 是 施事体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 1306-1306 | IT代理商 是 施事体 的 subclass |
|
|