No TPTP formula. May not be expressible in strict first order. 
Merge.kif 49474947 
The number 2 argument of exponentiation is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 53915391 
The number 1 argument of predecessor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 53575357 
The number 1 argument of successor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 86148614 
The number 1 argument of year is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 757757 
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 31253125 
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 1869018690 
The number 2 argument of defaultMaxValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1867618676 
The number 2 argument of defaultMinValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1870418704 
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 40554055 
The number 2 argument of Fleet Size 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 450450 
The number 2 argument of maximum capacity is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1866118661 
The number 2 argument of maxValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2011020110 
The number 2 argument of member count is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 21542154 
The number 2 argument of minCardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 21552155 
The number 3 argument of minCardinality is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1864718647 
The number 2 argument of minValue is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Cars.kif 18051805 
The number 2 argument of molecularRatio is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50165016 
The number 1 argument of multiplicative factor is an instance of integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50175017 
The number 2 argument of multiplicative factor is an instance of integer 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 