No TPTP formula. May not be expressible in strict first order. 
Merge.kif 16851685 
The number 1 argument of attr is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
UXExperimentalTerms.kif 16971697 
The number 1 argument of TTFx is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 34613461 
The number 2 argument of closed on is an instance of 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 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 class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 566566 
The number 1 argument of disjoint decomposition is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 567567 
The number 2 argument of disjoint decomposition is an instance of 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 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 class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 35843584 
The number 2 argument of equivalence relation on is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 548548 
The number 1 argument of exhaustive decomposition is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 549549 
The number 2 argument of exhaustive decomposition is an instance of 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 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 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 class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 35083508 
The number 2 argument of irreflexive on is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 35273527 
The number 2 argument of partial ordering on is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 582582 
The number 1 argument of partition is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 583583 
The number 2 argument of partition is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 305305 
The number 2 argument of range is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 34903490 
The number 2 argument of reflexive on is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 129129 
The number 1 argument of subclass is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 130130 
The number 2 argument of subclass is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 84878487 
The number 1 argument of successorClass is an instance of class 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 84888488 
The number 2 argument of successorClass is an instance of class 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 