No TPTP formula. May not be expressible in strict first order. 
ComputerInput.kif 295295 
Arrow key is disjoint from enter key 
No TPTP formula. May not be expressible in strict first order. 
ComputerInput.kif 334334 
Multi keypress key is disjoint from enter key 
No TPTP formula. May not be expressible in strict first order. 
ComputerInput.kif 324324 
Numbered function key is disjoint from enter key 
No TPTP formula. May not be expressible in strict first order. 
domainEnglishFormat.kif 6482564825 
