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

( ! [V__FORMULA,V__CONFIDENCE,V__EXPERIMENT] :
((s__instance(V__CONFIDENCE,s__RealNumber) =>
(((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE)
&
s__instance(V__EXPERIMENT,s__Experimenting) &
s__instance(V__FORMULA,s__Formula) &
s__patient(V__EXPERIMENT,V__FORMULA)
&
(V__CONFIDENCE = n__100))
=>
(s__truth(V__FORMULA,'$false__m')))))
)
)

UXExperimentalTerms.kif 682689 

( ! [V__P,V__H,V__PROP] :
(((s__instance(V__P,s__Agent) &
s__instance(V__PROP,s__Proposition) &
s__instance(V__PROP,s__Sentence))
=>
(((s__instance(V__H,s__Hallucination) &
s__experiencer(V__H,V__P))
=>
(( ? [V__PER] :
((s__instance(V__PER,s__Perception) &
s__experiencer(V__PER,V__P)
&
s__causes(V__H,V__PER)
&
s__containsInformation(V__PER,V__PROP)
&
s__truth(V__PROP,'$false__m'))))))))
)
)

Midlevelontology.kif 60516061 

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

( ! [V__FORMULA,V__EXPERIMENT,V__VALUE] :
((s__instance(V__VALUE,s__RealNumber) =>
(((s__pValue(V__EXPERIMENT,V__VALUE)
&
s__instance(V__EXPERIMENT,s__Experimenting) &
s__instance(V__FORMULA,s__Formula) &
s__patient(V__EXPERIMENT,V__FORMULA)
&
(V__VALUE = n__1))
=>
(s__truth(V__FORMULA,'$false__m')))))
)
)

UXExperimentalTerms.kif 723730 

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

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

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

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