No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18101810 
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 55435543 
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 55175517 
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 55185518 
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 819819 
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 55305530 
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 55315531 
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 54895489 
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 54905490 
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 36673667 
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 438438 
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 439439 
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 229229 
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 258258 
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 38003800 
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 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 37163716 
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 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2013220132 
The number 2 argument of member type is an instance of set or class 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2014620146 
The number 2 argument of member type count is an instance of set or class 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 