Sigma KB Term Intersection

No TPTP formula. May not be expressible in strict first order.	Merge.kif 3005-3010	If the number a positive integer argument of a relation is a subclass of a class and the relation is an instance of predicate and the relation @ROW, then the positive integerth element of (@ROW) is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3339-3339	Predicate is a subclass of relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3340-3340	Predicate is a subclass of inheritable relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3478-3478	Binary predicate is a subclass of predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3489-3489	Ternary predicate is a subclass of predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3500-3500	Quaternary predicate is a subclass of predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3511-3511	Quintary predicate is a subclass of predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3550-3550	Logical operator is a subclass of predicate
No TPTP formula. May not be expressible in strict first order.	Merge.kif 18470-18470	ClosedWorldPredicate is a subclass of predicate