| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2147-2148 | Relation is disjointly decomposed into binary relation, ternary relation, quaternary relation, quintary relation, and variable arity relation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1816-1819 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2152-2156 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 434-437 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2149-2149 | Relation is exhaustively partitioned into predicate and function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2150-2150 | Relation is exhaustively partitioned into total valued relation and partial valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2146-2146 | Relation is a subclass of abstract |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2219-2219 | Binary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2545-2545 | Inheritable relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2658-2658 | Intentional relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 965-965 | PPP based economic valuation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2210-2210 | Partial valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3326-3326 | Predicate is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2551-2551 | Probability relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2848-2848 | Quaternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2855-2855 | Quintary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3520-3520 | Relation extended to quantities is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2163-2163 | Single valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2643-2643 | Spatial relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2650-2650 | Temporal relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2841-2841 | Ternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2181-2181 | Total valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3509-3509 | Variable arity relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 888-888 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 978-978 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 564-564 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 94-94 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 95-95 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2249-2249 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 516-516 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 99-99 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31482-31482 | The number 2 argument of applicable relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 412-412 | The number 1 argument of disjoint relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 413-413 | The number 2 argument of disjoint relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 208-208 | The number 1 argument of domain is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 230-230 | The number 1 argument of domain subclass is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2069-2069 | The number 1 argument of exact cardinality is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2193-2193 | The number 1 argument of max cardinality is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2156-2156 | The number 1 argument of min cardinality is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 171-171 | The number 1 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 172-172 | The number 2 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 361-361 | The number 1 argument of valence is an instance of relation |
| appearance as argument number 4 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1657-1657 | Abstract is disjointly decomposed into quantity, attribute, relation, proposition, and list |
|
|
|