No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18331833 
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 55775577 
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 55515551 
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 55525552 
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 833833 
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 55645564 
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 55655565 
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 55235523 
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 55245524 
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 903903 
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 6767 
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 6868 
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 6969 
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 36903690 
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 440440 
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 441441 
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 231231 
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 260260 
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 38233823 
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 165165 
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 166166 
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 8383 
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 37393739 
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 