No TPTP formula. May not be expressible in strict first order. 
Merge.kif 16861686 
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 51955195 
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 51735173 
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 51745174 
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 763763 
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 51845184 
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 51855185 
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 51475147 
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 51485148 
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 34563456 
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 395395 
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 396396 
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 209209 
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 231231 
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 35793579 
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 152152 
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 153153 
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 35033503 
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 