No TPTP formula. May not be expressible in strict first order. 
Merge.kif 85538553 
The number 1 argument of day is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1535915359 
The number 2 argument of edition is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 29552955 
The number 2 argument of list order is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 49474947 
The number 2 argument of log is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1451014510 
The number 2 argument of periodical issue is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 89338933 
The number 1 argument of quarter fn is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 86318631 
The number 1 argument of second is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1446514465 
The number 2 argument of series volume is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 89158915 
The number 1 argument of week fn is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
FinancialOntology.kif 34533453 
The number 2 argument of account number is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 22542254 
The number 3 argument of agricultural product type by rank is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1363213632 
The number 2 argument of atomic number is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
FinancialOntology.kif 34703470 
The number 2 argument of check number is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
QoSontology.kif 12091209 
The number 2 argument of data stream slack is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 209209 
The number 2 argument of domain is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 231231 
The number 2 argument of domain subclass is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2165821658 
The number 2 argument of electron number is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 23352335 
The number 3 argument of export commodity type by rank is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 25142514 
The number 3 argument of export partner by rank is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 25022502 
The number 3 argument of export partner by rank in period is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 66606660 
The number 2 argument of human capacity is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 26312631 
The number 3 argument of import commodity type by rank is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 27072707 
The number 3 argument of import partner by rank is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 26952695 
The number 3 argument of import partner by rank in period is an instance of positive integer 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 15991599 
The number 3 argument of industry rank by output is an instance of positive integer 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 