TreeView Knowledge Base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 2282-2283
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5237-5238
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5234-5234	The number 1 argument of predecessor is an instance of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5233-5233	Predecessor is an instance of total valued relation
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5232-5232	Predecessor is an instance of unary function
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5235-5235	The range of predecessor is an instance of integer

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 736-736
No TPTP formula. May not be expressible in strict first order.	english_format.kif 738-738
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 47139-47139
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 737-737
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 47138-47138
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 47137-47137

antecedent

No TPTP formula. May not be expressible in strict first order.

Merge.kif 5240-5242

consequent

No TPTP formula. May not be expressible in strict first order.	Merge.kif 5228-5230	If an integer is an instance of integer, then the integer is equal to ((the integer+1)+2)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5224-5226	If an integer is an instance of integer, then the integer is equal to ((the integer+2)+1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5244-5246	If an integer is an instance of integer, then the integer is greater than (the integer+2)

statement

No TPTP formula. May not be expressible in strict first order.

Merge.kif 4640-4641