No TPTP formula. May not be expressible in strict first order. 
Merge.kif 46534653 
The number 2 argument of exponentiation is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 46814681 
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 47544754 
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 51065106 
The number 1 argument of predecessor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 49064906 
The number 1 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 49074907 
The number 2 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 30583058 
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 30593059 
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 50735073 
The number 1 argument of successor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 82308230 
The number 1 argument of year is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 767767 
The number 3 argument of capacity by arrangement is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Cars.kif 31133113 
The number 2 argument of coilCount 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 642642 
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 1780517805 
The number 2 argument of defaultMaxValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1778817788 
The number 2 argument of defaultMinValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1782217822 
The number 2 argument of defaultValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 20722072 
The number 2 argument of exactCardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 20732073 
The number 3 argument of exactCardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 34553455 
The number 2 argument of Fleet Size is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 98799879 
The number 3 argument of heartRate is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50515051 
The number 2 argument of identity element is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 21902190 
The number 2 argument of maxCardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 21912191 
The number 3 argument of maxCardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 457457 
The number 2 argument of maximum capacity is an instance of integer 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 