No TPTP formula. May not be expressible in strict first order. 
Merge.kif 48204820 
The number 2 argument of exponentiation is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 48484848 
The number 1 argument of greatest common divisor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 49334933 
The number 1 argument of least common multiple is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 53345334 
The number 1 argument of predecessor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50965096 
The number 1 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50975097 
The number 2 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 31613161 
The number 1 argument of sublist function is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 31623162 
The number 2 argument of sublist function is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 53015301 
The number 1 argument of successor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 85558555 
The number 1 argument of year is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1035110351 
The number 3 argument of breathingRate is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 788788 
The number 3 argument of capacity by arrangement is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
VirusProteinAndCellPart.kif 699699 
The number 2 argument of chromosome number is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
VirusProteinAndCellPart.kif 825825 
The number 3 argument of chromosome set count is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Cars.kif 31133113 
The number 2 argument of coil count is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Communications.kif 135135 
The number 3 argument of communication satellite for area is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
QoSontology.kif 644644 
The number 2 argument of criticality level is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1841118411 
The number 2 argument of default max value is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1839418394 
The number 2 argument of default min value is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1842818428 
The number 2 argument of default value is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 20702070 
The number 2 argument of exact cardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 20712071 
The number 3 argument of exact cardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 34943494 
The number 2 argument of Fleet Size is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
VirusProteinAndCellPart.kif 790790 
The number 2 argument of haploid number is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1030910309 
The number 3 argument of heart rate is an instance of integer 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 