No TPTP formula. May not be expressible in strict first order. 
Merge.kif 47914791 
The number 2 argument of exponentiation is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 48194819 
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 49044904 
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 53015301 
The number 1 argument of predecessor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50675067 
The number 1 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50685068 
The number 2 argument of remainder is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 31383138 
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 31393139 
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 52685268 
The number 1 argument of successor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 85208520 
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 1827818278 
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 1826118261 
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 1829518295 
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 34873487 
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 1026610266 
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 52465246 
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 