| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2160-2161 | 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 2165-2169 | |
| 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 2162-2162 | Relation is exhaustively partitioned into predicate and function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2163-2163 | 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 2159-2159 | Relation is a subclass of abstract |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2232-2232 | Binary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2558-2558 | Inheritable relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2671-2671 | 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 2223-2223 | Partial valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3339-3339 | Predicate is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2564-2564 | Probability relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2861-2861 | Quaternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2868-2868 | Quintary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3533-3533 | Relation extended to quantities is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2176-2176 | Single valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2656-2656 | Spatial relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2663-2663 | Temporal relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2854-2854 | Ternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2194-2194 | Total valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3522-3522 | 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 97-97 | |
| 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 31294-31294 | 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 1670-1670 | Abstract is disjointly decomposed into quantity, attribute, relation, proposition, and list |
|
|
|