| SetOrClass | |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1804-1805 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2127-2129 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 419-420 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2125-2125 | 劃分 SetOrClass, Set and Class |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2124-2124 | 子類 SetOrClass and Abstract |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5488-5488 | 範圍 補充 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5509-5509 | 範圍 一般化交叉口 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5498-5498 | 範圍 一般化聯盟 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5467-5467 | 範圍 路口 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5478-5478 | 範圍 相對補充 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5441-5441 | 範圍 聯盟 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 791-791 | 範圍子類 電源組 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2132-2132 | 子類 Class and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2144-2144 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 885-885 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 972-972 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 561-561 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 91-91 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 94-94 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2246-2246 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 513-513 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 128-128 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 387-387 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 582-582 | 子類 Set and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 95-95 | 子類 Set and SetOrClass |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5518-5518 | 域 基數, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5487-5487 | 域 補充, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5465-5465 | 域 路口, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5466-5466 | 域 路口, 2 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 790-790 | 域 電源組, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5476-5476 | 域 相對補充, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5477-5477 | 域 相對補充, 2 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5439-5439 | 域 聯盟, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5440-5440 | 域 聯盟, 2 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 945-945 | 域 adjacentOrientation, 2 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 400-400 | 域 基數, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 39-39 | 域 詞庫, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5508-5508 | 域子類 一般化交叉口, 1 and SetOrClass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5497-5497 | 域子類 一般化聯盟, 1 and SetOrClass |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Government.kif 410-414 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2139-2152 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2212-2225 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2176-2189 |
|
|
|