No TPTP formula. May not be expressible in strict first order. 
Merge.kif 21162133 
A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 179183 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 32873289 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 33493351 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 33383340 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 32483250 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 33663368 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 33883390 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 33993401 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 33773379 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 34083412 
