( ! [V__Amount,V__Loan] :
(s__instance(V__Amount,s__Interest) =>
(( ? [V__Period] :
((s__instance(V__Period,s__TimeInterval) &
(s__instance(V__Loan,s__Loan) &
s__agreementPeriod(V__Loan,V__Period)
&
s__interestEarned(V__Loan,V__Amount,V__Period)))))
=>
s__loanInterest(V__Loan,V__Amount))
&
(s__loanInterest(V__Loan,V__Amount)
=>
( ? [V__Period] :
((s__instance(V__Period,s__TimeInterval) &
(s__instance(V__Loan,s__Loan) &
s__agreementPeriod(V__Loan,V__Period)
&
s__interestEarned(V__Loan,V__Amount,V__Period))))))
)
)

FinancialOntology.kif 37623768 
There exists a time interval such that a loan is an instance of loan and the time interval is an agreement period of the loan and the loan is interest earned an interest for the time interval if and only if the interest is a loan interest of the loan 
( ! [V__Lender,V__Period,V__Loan,V__Interest,V__Borrower] :
((s__instance(V__Lender,s__CognitiveAgent) &
s__instance(V__Period,s__TimeInterval) &
s__instance(V__Loan,s__Loan) &
s__instance(V__Interest,s__Interest) &
s__instance(V__Borrower,s__CognitiveAgent))
=>
(s__borrower(V__Loan,V__Borrower)
&
s__lender(V__Loan,V__Lender)
&
s__agreementPeriod(V__Loan,V__Period)
&
s__interestEarned(V__Loan,V__Interest,V__Period))
=>
( ? [V__Payment] :
((s__instance(V__Payment,s__FinancialTransaction) &
(s__origin(V__Payment,V__Borrower)
&
s__transactionAmount(V__Payment,V__Interest)
&
s__destination(V__Payment,V__Lender)))))
)
)

FinancialOntology.kif 12021212 

( ! [V__Period,V__Agent,V__Interest,V__Account,V__Organization] :
((s__instance(V__Period,s__TimeInterval) &
s__instance(V__Agent,s__CognitiveAgent) &
s__instance(V__Interest,s__Interest) &
s__instance(V__Organization,s__FinancialOrganization))
=>
(s__instance(V__Account,s__CreditAccount) &
s__accountAt(V__Account,V__Organization)
&
s__accountHolder(V__Account,V__Agent)
&
s__interestEarned(V__Account,V__Interest,V__Period))
=>
( ? [V__Payment] :
((s__instance(V__Payment,s__FinancialTransaction) &
(s__origin(V__Payment,V__Agent)
&
s__transactionAmount(V__Payment,V__Interest)
&
s__destination(V__Payment,V__Organization)))))
)
)

FinancialOntology.kif 11531163 

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

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

( ! [V__Period,V__Agent,V__Interest,V__Account] :
((s__instance(V__Period,s__TimeInterval) &
s__instance(V__Agent,s__CognitiveAgent) &
s__instance(V__Interest,s__Interest))
=>
(s__instance(V__Account,s__SavingsAccount) &
s__accountHolder(V__Account,V__Agent)
&
s__interestEarned(V__Account,V__Interest,V__Period))
=>
( ? [V__Payment] :
((s__instance(V__Payment,s__FinancialTransaction) &
(s__destination(V__Payment,s__CurrencyFn(V__Account))
&
s__transactionAmount(V__Payment,V__Interest)
&
s__destination(V__Payment,V__Agent)))))
)
)

FinancialOntology.kif 987996 

( ! [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__CurrencyMeasure) &
s__instance(V__BondHolder,s__Agent) &
s__instance(V__Date,s__Day) &
s__instance(V__Interest,s__Interest) &
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 22632277 

( ! [V__Period,V__Loan,V__Date,V__Interest,V__Principal] :
((s__instance(V__Period,s__TimeInterval) &
s__instance(V__Date,s__TimeInterval) &
s__instance(V__Interest,s__Interest) &
s__instance(V__Principal,s__CurrencyMeasure))
=>
(s__instance(V__Loan,s__InterestOnlyLoan) &
s__agreementPeriod(V__Loan,V__Period)
&
s__principalAmount(V__Loan,V__Principal)
&
s__interestEarned(V__Loan,V__Interest,V__Period))
=>
(s__amountDue(V__Loan,V__Principal,s__EndFn(V__Period))
&
s__amountDue(V__Loan,V__Interest,V__Date)
&
s__before(s__EndFn(V__Date)
,s__EndFn(V__Period)))
)
)

FinancialOntology.kif 15571566 
