No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1304113048 
The statement a formula has the modal force of legal if and only if there doesn't exist another formula such that the statement the other formula has the modal force of law and the other formula is not a consistent of the formula 
( ! [V__CONTENT,V__NATION,V__LAW,V__CAO] :
(((s__instance(V__CONTENT,s__Proposition) &
s__instance(V__LAW,s__Proposition))
=>
(((s__instance(V__CAO,s__CivilAffairsOperation) &
s__located(V__CAO,V__NATION)
&
s__instance(V__NATION,s__Nation) &
s__instance(V__LAW,s__RegionalLawFn(V__NATION))
&
s__realization(V__CAO,V__CONTENT))
=>
(s__consistent(V__LAW,V__CONTENT)))))
)
)

MilitaryProcesses.kif 22242232 

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

( ! [V__C] :
((s__instance(V__C,s__Correcting) =>
(( ? [V__D, V__S, V__SP, V__CP] :
((s__instance(V__SP,s__Proposition) &
s__instance(V__CP,s__Proposition) &
(s__instance(V__D,s__Disagreeing) &
s__subProcess(V__C,V__D)
&
s__instance(V__S,s__Stating) &
s__subProcess(V__S,V__D)
&
s__containsInformation(V__S,V__SP)
&
s__containsInformation(V__C,V__CP)
&
s__refers(V__CP,V__SP)
&
~(s__consistent(V__CP,V__SP))))))))
)
)

Midlevelontology.kif 2874928761 

( ! [V__DIS] :
((s__instance(V__DIS,s__Disagreeing) =>
(( ? [V__A1, V__A2, V__STATE1, V__STATE2, V__STMT1, V__STMT2] :
((s__instance(V__A1,s__Agent) &
s__instance(V__A2,s__Agent) &
s__instance(V__STATE1,s__Process) &
s__instance(V__STATE1,s__ContentBearingPhysical) &
s__instance(V__STATE2,s__Process) &
s__instance(V__STATE2,s__ContentBearingPhysical) &
s__instance(V__STMT1,s__Proposition) &
s__instance(V__STMT2,s__Proposition) &
(s__subProcess(V__STATE1,V__DIS)
&
s__subProcess(V__STATE2,V__DIS)
&
s__agent(V__STATE1,V__A1)
&
s__agent(V__STATE2,V__A2)
&
~((V__A1 = V__A2))
&
s__containsInformation(V__STATE1,V__STMT1)
&
s__containsInformation(V__STATE2,V__STMT2)
&
~(s__consistent(V__STMT1,V__STMT2))))))))
)
)

Merge.kif 1253412547 
 If a process is an instance of disagreeing,
 then there exist an agent, another agent,, , another process,, , a third process,, , a proposition and another proposition such that the other process is a subprocess of the process and the third process is a subprocess of the process and the agent is an agent of the other process and the other agent is an agent of the third process and the agent is not equal to the other agent and the other process contains information the proposition and the third process contains information the other proposition and the other proposition is not a consistent of the proposition
