( ! [V__Object,V__Seller,V__Money,V__Purchase,V__Buyer] :
(((s__instance(V__Object,s__Physical) &
s__instance(V__Seller,s__Object) &
s__instance(V__Money,s__CurrencyMeasure) &
s__instance(V__Purchase,s__Process) &
s__instance(V__Buyer,s__Agent))
=>
(((s__agent(V__Purchase,V__Buyer)
&
s__origin(V__Purchase,V__Seller)
&
s__patient(V__Purchase,V__Object)
&
s__monetaryValue(V__Object,V__Money))
=>
(( ? [V__Payment] :
((s__subProcess(V__Payment,V__Purchase)
&
s__instance(V__Payment,s__Payment) &
s__transactionAmount(V__Payment,V__Money)
&
s__origin(V__Payment,V__Buyer)
&
s__destination(V__Payment,V__Seller))))))))
)
)

FinancialOntology.kif 463475 

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

( ! [V__Period,V__Total,V__BondHolder,V__Date,V__Bond,V__Interest,V__Principal] :
(((s__instance(V__Period,s__TimeInterval) &
s__instance(V__Total,s__Number) &
s__instance(V__Total,s__CurrencyMeasure) &
s__instance(V__BondHolder,s__Agent) &
s__instance(V__Date,s__Day) &
s__instance(V__Interest,s__Interest) &
s__instance(V__Interest,s__Number) &
s__instance(V__Principal,s__Number) &
s__instance(V__Principal,s__CurrencyMeasure))
=>
(((s__instance(V__Bond,s__ZeroCouponBond) &
s__maturityDate(s__AccountFn(V__Bond)
,V__Date)
&
s__possesses(V__BondHolder,V__Bond)
&
s__principalAmount(s__AccountFn(V__Bond)
,V__Principal)
&
s__agreementPeriod(s__AccountFn(V__Bond)
,V__Period)
&
s__interestEarned(s__AccountFn(V__Bond)
,V__Interest,V__Period)
&
(V__Total = s__AdditionFn(V__Principal,V__Interest)))
=>
(( ? [V__Payment] :
((s__instance(V__Payment,s__Payment) &
s__destination(V__Payment,V__BondHolder)
&
s__origin(V__Payment,s__AccountFn(V__Bond))
&
s__transactionAmount(V__Payment,V__Total))))))))
)
)

FinancialOntology.kif 22822296 

( ! [V__REPAYMENT,V__REPAYMENT_ORIGIN,V__REPAYMENT_DESTINATION] :
(((s__instance(V__REPAYMENT,s__Repayment) &
s__instance(V__REPAYMENT_DESTINATION,s__Object) &
s__destination(V__REPAYMENT,V__REPAYMENT_DESTINATION)
&
s__instance(V__REPAYMENT_ORIGIN,s__Object) &
s__origin(V__REPAYMENT,V__REPAYMENT_ORIGIN))
=>
(( ? [V__PAYMENT, V__PAYMENT_ORIGIN, V__PAYMENT_DESTINATION] :
((s__instance(V__PAYMENT,s__Payment) &
s__instance(V__PAYMENT_ORIGIN,s__Object) &
s__instance(V__PAYMENT_DESTINATION,s__Object) &
~((V__PAYMENT = V__REPAYMENT))
&
s__destination(V__PAYMENT,V__PAYMENT_DESTINATION)
&
s__origin(V__PAYMENT,V__PAYMENT_ORIGIN)
&
(V__PAYMENT_ORIGIN = V__REPAYMENT_DESTINATION)
&
(V__PAYMENT_DESTINATION = V__REPAYMENT_ORIGIN))))))
)
)

UXExperimentalTerms.kif 20922109 

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

( ! [V__Amount,V__Period,V__Account] :
(((s__instance(V__Amount,s__CurrencyMeasure) &
s__instance(V__Period,s__TimeDuration) &
s__instance(V__Account,s__FinancialAccount))
=>
((s__periodicPayment(V__Account,V__Amount,V__Period)
=>
(( ? [V__Payment] :
((s__instance(V__Payment,s__Payment) &
s__origin(V__Payment,s__CurrencyFn(V__Account))
&
s__transactionAmount(V__Payment,V__Amount)
&
s__frequency(V__Payment,V__Period))))))))
)
)

FinancialOntology.kif 702709 
