No TPTP formula. May not be expressible in strict first order. 
Merge.kif 16811681 
The number 1 argument of attr is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51885188 
The number 1 argument of complement is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51665166 
The number 1 argument of intersection is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51675167 
The number 2 argument of intersection is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 762762 
The number 1 argument of power set is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51775177 
The number 1 argument of relative complement is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51785178 
The number 2 argument of relative complement is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51405140 
The number 1 argument of union is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51415141 
The number 2 argument of union is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 907907 
The number 2 argument of adjacent orientation is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Government.kif 425425 
The number 1 argument of cardinality is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
ComputerInput.kif 6868 
The number 1 argument of classIntersection is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
ComputerInput.kif 6969 
The number 2 argument of classIntersection is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
ComputerInput.kif 7070 
The number 3 argument of classIntersection is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 34513451 
The number 2 argument of closed on is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 394394 
The number 1 argument of disjoint is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 395395 
The number 2 argument of disjoint is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 208208 
The number 3 argument of domain is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 230230 
The number 3 argument of domain subclass is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 35743574 
The number 2 argument of equivalence relation on is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 151151 
The number 1 argument of immediate subclass is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 152152 
The number 2 argument of immediate subclass is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 8282 
The number 2 argument of instance is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 34983498 
The number 2 argument of irreflexive on is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
engineering.kif 3939 
The number 1 argument of lexicon is an instance of set or class 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 