No TPTP formula. May not be expressible in strict first order. 
Merge.kif 48064806 
The number 2 argument of exponentiation is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 48344834 
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 49194919 
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 53205320 
The number 1 argument of predecessor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50825082 
The number 1 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50835083 
The number 2 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 31483148 
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 31493149 
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 52875287 
The number 1 argument of successor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 85398539 
The number 1 argument of year 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. 
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 1832218322 
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 1830518305 
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 1833918339 
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. 
Midlevelontology.kif 1028910289 
The number 3 argument of heart rate is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 52655265 
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 21942194 
The number 2 argument of max cardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 21952195 
The number 3 argument of max cardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 477477 
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 