Class(class) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9035-9035 | The number 1 argument of successor class is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9036-9036 | The number 2 argument of successor class is an instance of class |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4531-4531 | The number 1 argument of total is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1214-1214 | The number 2 argument of total facility type in area is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3660-3660 | The number 2 argument of total ordering on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3682-3682 | The number 2 argument of trichotomizing on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 335-335 | The number 2 argument of range subclass is a subclass of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2129-2129 | Set or class is exhaustively partitioned into set and class |