diff options
| author | krasimir <krasimir@chalmers.se> | 2010-02-17 12:21:41 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-02-17 12:21:41 +0000 |
| commit | d6627b5a5af6a82dd5316ac5d527790697615339 (patch) | |
| tree | 06c89e2cbb1212fe54c1c886ddb839e91383952f /examples/SUMO/TPTP/FinancialOntologyLemAx.p | |
| parent | 6690fbaf6ce1247165ce159683367982c28efeca (diff) | |
added TPTP for SUMO
Diffstat (limited to 'examples/SUMO/TPTP/FinancialOntologyLemAx.p')
| -rw-r--r-- | examples/SUMO/TPTP/FinancialOntologyLemAx.p | 1577 |
1 files changed, 1577 insertions, 0 deletions
diff --git a/examples/SUMO/TPTP/FinancialOntologyLemAx.p b/examples/SUMO/TPTP/FinancialOntologyLemAx.p new file mode 100644 index 000000000..a434a0d07 --- /dev/null +++ b/examples/SUMO/TPTP/FinancialOntologyLemAx.p @@ -0,0 +1,1577 @@ +fof(axFinancialLem0, axiom,
+ ( ! [Var_ASSET] :
+ (hasType(type_FinancialAsset, Var_ASSET) =>
+(( ? [Var_VALUE] :
+ (hasType(type_CurrencyMeasure, Var_VALUE) &
+(f_monetaryValue(Var_ASSET,Var_VALUE)))))))).
+
+fof(axFinancialLem1, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ? [Var_ORGANIZATION] :
+ (hasType(type_FinancialOrganization, Var_ORGANIZATION) &
+(f_accountAt(Var_ACCOUNT,Var_ORGANIZATION)))))))).
+
+fof(axFinancialLem2, axiom,
+ ( ! [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) =>
+(( ? [Var_VALUE] :
+ (hasType(type_CurrencyMeasure, Var_VALUE) &
+(f_monetaryValue(Var_CHECK,Var_VALUE)))))))).
+
+fof(axFinancialLem3, axiom,
+ ( ! [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) =>
+(( ? [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) &
+(f_checkAccount(Var_CHECK,Var_ACCOUNT)))))))).
+
+fof(axFinancialLem4, axiom,
+ ( ! [Var_PROCESSING] :
+ (hasType(type_ProcessingACheck, Var_PROCESSING) =>
+(( ! [Var_WITHDRAWALTIME] :
+ ((hasType(type_Entity, Var_WITHDRAWALTIME) & hasType(type_TimeInterval, Var_WITHDRAWALTIME)) =>
+(( ! [Var_PROCESSINGTIME] :
+ ((hasType(type_Entity, Var_PROCESSINGTIME) & hasType(type_TimeInterval, Var_PROCESSINGTIME)) =>
+(( ! [Var_ACCOUNT] :
+ ((hasType(type_FinancialAccount, Var_ACCOUNT) & hasType(type_Object, Var_ACCOUNT)) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_CHECK] :
+ ((hasType(type_Physical, Var_CHECK) & hasType(type_Check, Var_CHECK) & hasType(type_Entity, Var_CHECK) & hasType(type_Object, Var_CHECK)) =>
+(((((f_monetaryValue(Var_CHECK,Var_AMOUNT)) & (((f_checkAccount(Var_CHECK,Var_ACCOUNT)) & (((f_patient(Var_PROCESSING,Var_CHECK)) & (f_WhenFn(Var_PROCESSING) = Var_PROCESSINGTIME))))))) => (( ? [Var_WITHDRAWAL] :
+ (hasType(type_Withdrawal, Var_WITHDRAWAL) &
+(((f_instrument(Var_WITHDRAWAL,Var_CHECK)) & (((f_WhenFn(Var_WITHDRAWAL) = Var_WITHDRAWALTIME) & (((f_meetsTemporally(Var_PROCESSINGTIME,Var_WITHDRAWALTIME)) & (((f_transactionAmount(Var_WITHDRAWAL,Var_AMOUNT)) & (f_origin(Var_WITHDRAWAL,Var_ACCOUNT))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem5, axiom,
+ ( ! [Var_PROCESSING] :
+ (hasType(type_ProcessingACheck, Var_PROCESSING) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_DEPOSITTIME] :
+ ((hasType(type_Entity, Var_DEPOSITTIME) & hasType(type_TimeInterval, Var_DEPOSITTIME)) =>
+(( ! [Var_PROCESSINGTIME] :
+ ((hasType(type_Entity, Var_PROCESSINGTIME) & hasType(type_TimeInterval, Var_PROCESSINGTIME)) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_CHECK] :
+ ((hasType(type_Physical, Var_CHECK) & hasType(type_Entity, Var_CHECK) & hasType(type_Object, Var_CHECK)) =>
+(((((f_monetaryValue(Var_CHECK,Var_AMOUNT)) & (((f_patient(Var_PROCESSING,Var_CHECK)) & (((f_destination(Var_PROCESSING,f_CurrencyFn(Var_ACCOUNT))) & (f_WhenFn(Var_PROCESSING) = Var_PROCESSINGTIME))))))) => (( ? [Var_DEPOSIT] :
+ (hasType(type_Deposit, Var_DEPOSIT) &
+(((f_instrument(Var_DEPOSIT,Var_CHECK)) & (((f_WhenFn(Var_DEPOSIT) = Var_DEPOSITTIME) & (((f_meetsTemporally(Var_PROCESSINGTIME,Var_DEPOSITTIME)) & (((f_transactionAmount(Var_DEPOSIT,Var_AMOUNT)) & (f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT)))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem6, axiom,
+ ( ! [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) =>
+(( ! [Var_PROCESSING] :
+ (hasType(type_ProcessingACheck, Var_PROCESSING) =>
+(((f_patient(Var_PROCESSING,Var_CHECK)) => (( ? [Var_DEPOSITING] :
+ (hasType(type_DepositingACheck, Var_DEPOSITING) &
+(((f_patient(Var_DEPOSITING,Var_CHECK)) & (f_time(Var_DEPOSITING,f_ImmediatePastFn(f_WhenFn(Var_PROCESSING))))))))))))))))).
+
+fof(axFinancialLem7, axiom,
+ ( ! [Var_DEPOSITING] :
+ (hasType(type_DepositingACheck, Var_DEPOSITING) =>
+(( ! [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
+(((f_agent(Var_DEPOSITING,Var_AGENT)) => (f_signedBy(Var_CHECK,Var_AGENT))))))))))))).
+
+fof(axFinancialLem8, axiom,
+ ( ! [Var_DRAWING] :
+ (hasType(type_DrawingACheck, Var_DRAWING) =>
+(( ! [Var_PROCESSING] :
+ (hasType(type_ProcessingACheck, Var_PROCESSING) =>
+(( ! [Var_DURATION] :
+ (hasType(type_Quantity, Var_DURATION) =>
+(( ! [Var_DUATION] :
+ (hasType(type_TimeDuration, Var_DUATION) =>
+(( ! [Var_TIME] :
+ (hasType(type_TimeInterval, Var_TIME) =>
+(( ! [Var_PROCESSINGTIME] :
+ ((hasType(type_Entity, Var_PROCESSINGTIME) & hasType(type_TimeInterval, Var_PROCESSINGTIME)) =>
+(( ! [Var_PROCESING] :
+ (hasType(type_Physical, Var_PROCESING) =>
+(( ! [Var_DRAWINGTIME] :
+ ((hasType(type_Entity, Var_DRAWINGTIME) & hasType(type_TimeInterval, Var_DRAWINGTIME)) =>
+(( ! [Var_CHECK] :
+ (hasType(type_Entity, Var_CHECK) =>
+(((((f_patient(Var_DRAWING,Var_CHECK)) & (((f_patient(Var_PROCESSING,Var_CHECK)) & (((f_WhenFn(Var_DRAWING) = Var_DRAWINGTIME) & (((f_WhenFn(Var_PROCESING) = Var_PROCESSINGTIME) & (((f_meetsTemporally(Var_DRAWINGTIME,Var_TIME)) & (((f_meetsTemporally(Var_TIME,Var_PROCESSINGTIME)) & (f_duration(Var_TIME,Var_DUATION)))))))))))))) => (f_lessThan(Var_DURATION,f_MeasureFn(6,inst_MonthDuration)))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem9, axiom,
+ ( ! [Var_CHECK] :
+ (hasType(type_PayCheck, Var_CHECK) =>
+(( ! [Var_GIVE] :
+ (hasType(type_Giving, Var_GIVE) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Entity, Var_AGENT) & hasType(type_Organization, Var_AGENT)) =>
+(( ! [Var_ORGANIZATION] :
+ (hasType(type_CognitiveAgent, Var_ORGANIZATION) =>
+(((((f_issuedBy(Var_CHECK,Var_ORGANIZATION)) & (f_destination(Var_GIVE,Var_AGENT)))) => (f_employs(Var_AGENT,Var_ORGANIZATION)))))))))))))))).
+
+fof(axFinancialLem10, axiom,
+ ( ! [Var_CARD] :
+ (hasType(type_BankCard, Var_CARD) =>
+(( ? [Var_ORGANIZATION] :
+ (hasType(type_CognitiveAgent, Var_ORGANIZATION) &
+(f_issuedBy(Var_CARD,Var_ORGANIZATION)))))))).
+
+fof(axFinancialLem11, axiom,
+ ( ! [Var_CARD] :
+ (hasType(type_BankCard, Var_CARD) =>
+(( ! [Var_BANK] :
+ ((hasType(type_CognitiveAgent, Var_BANK) & hasType(type_FinancialOrganization, Var_BANK)) =>
+(((f_issuedBy(Var_CARD,Var_BANK)) => (( ? [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) &
+(((f_cardAccount(Var_CARD,Var_ACCOUNT)) & (f_accountAt(Var_ACCOUNT,Var_BANK))))))))))))))).
+
+fof(axFinancialLem12, axiom,
+ ( ! [Var_CARD] :
+ (hasType(type_DebitCard, Var_CARD) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
+(((f_possesses(Var_AGENT,Var_CARD)) => (( ? [Var_ACCOUNT] :
+ (hasType(type_DepositAccount, Var_ACCOUNT) &
+(((f_cardAccount(Var_CARD,Var_ACCOUNT)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT))))))))))))))).
+
+fof(axFinancialLem13, axiom,
+ ( ! [Var_CARD] :
+ (hasType(type_CreditCard, Var_CARD) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
+(((f_possesses(Var_AGENT,Var_CARD)) => (( ? [Var_ACCOUNT] :
+ (hasType(type_CreditCardAccount, Var_ACCOUNT) &
+(((f_cardAccount(Var_CARD,Var_ACCOUNT)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT))))))))))))))).
+
+fof(axFinancialLem14, axiom,
+ ( ! [Var_OPENING] :
+ (hasType(type_OpeningAnAccount, Var_OPENING) =>
+(( ! [Var_BANK] :
+ (hasType(type_FinancialOrganization, Var_BANK) =>
+(( ! [Var_OPENINGTIME] :
+ ((hasType(type_Entity, Var_OPENINGTIME) & hasType(type_TimeInterval, Var_OPENINGTIME)) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
+(((((f_located(Var_OPENING,Var_BANK)) & (((f_agent(Var_OPENING,Var_AGENT)) & (f_WhenFn(Var_OPENING) = Var_OPENINGTIME))))) => (( ? [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) &
+(( ? [Var_ACCOUNTPERIOD] :
+ (hasType(type_TimeInterval, Var_ACCOUNTPERIOD) &
+(((f_agreementPeriod(Var_ACCOUNT,Var_ACCOUNTPERIOD)) & (((f_meetsTemporally(Var_OPENINGTIME,Var_ACCOUNTPERIOD)) & (((f_accountAt(Var_ACCOUNT,Var_BANK)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT)))))))))))))))))))))))))))).
+
+fof(axFinancialLem15, axiom,
+ ( ! [Var_USING] :
+ (hasType(type_UsingAnAccount, Var_USING) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
+(( ! [Var_ACCOUNT] :
+ ((hasType(type_Entity, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
+(((((f_patient(Var_USING,Var_ACCOUNT)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT)))) => (f_agent(Var_USING,Var_AGENT))))))))))))).
+
+fof(axFinancialLem16, axiom,
+ ( ! [Var_DRAWING] :
+ (hasType(type_DrawingACheck, Var_DRAWING) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
+(( ! [Var_CHECK] :
+ ((hasType(type_Entity, Var_CHECK) & hasType(type_Check, Var_CHECK)) =>
+(((((f_patient(Var_DRAWING,Var_CHECK)) & (((f_agent(Var_DRAWING,Var_AGENT)) & (f_checkAccount(Var_CHECK,Var_ACCOUNT)))))) => (f_accountHolder(Var_ACCOUNT,Var_AGENT)))))))))))))))).
+
+fof(axFinancialLem17, axiom,
+ ( ! [Var_DEPOSITING] :
+ (hasType(type_DepositingACheck, Var_DEPOSITING) =>
+(( ? [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) &
+(f_patient(Var_DEPOSITING,Var_CHECK)))))))).
+
+fof(axFinancialLem18, axiom,
+ ( ! [Var_DEPOSITING] :
+ (hasType(type_DepositingACheck, Var_DEPOSITING) =>
+(( ! [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_patient(Var_DEPOSITING,Var_CHECK)) & (((f_checkAccount(Var_CHECK,Var_ACCOUNT)) & (f_monetaryValue(Var_CHECK,Var_AMOUNT)))))) => (( ? [Var_DEPOSIT] :
+ (hasType(type_Deposit, Var_DEPOSIT) &
+(((f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT))) & (f_transactionAmount(Var_DEPOSIT,Var_AMOUNT))))))))))))))))))))).
+
+fof(axFinancialLem19, axiom,
+ ( ! [Var_CONTROLLING] :
+ (hasType(type_ControllingAnAccount, Var_CONTROLLING) =>
+(( ! [Var_BANK] :
+ ((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_Agent, Var_BANK)) =>
+(( ! [Var_ACCOUNT] :
+ ((hasType(type_Entity, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
+(((((f_patient(Var_CONTROLLING,Var_ACCOUNT)) & (f_accountAt(Var_ACCOUNT,Var_BANK)))) => (f_agent(Var_CONTROLLING,Var_BANK))))))))))))).
+
+fof(axFinancialLem20, axiom,
+ ( ! [Var_PROCESSING] :
+ (hasType(type_ProcessingACheck, Var_PROCESSING) =>
+(( ! [Var_PROCESING] :
+ (hasType(type_Process, Var_PROCESING) =>
+(( ? [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) &
+(f_patient(Var_PROCESING,Var_CHECK))))))))))).
+
+fof(axFinancialLem21, axiom,
+ ( ! [Var_PROCESSING] :
+ (hasType(type_ProcessingACheck, Var_PROCESSING) =>
+(( ? [Var_AUTHORIZATION] :
+ (hasType(type_AuthorizationOfTransaction, Var_AUTHORIZATION) &
+(f_subProcess(Var_AUTHORIZATION,Var_PROCESSING)))))))).
+
+fof(axFinancialLem22, axiom,
+ ( ! [Var_PAYMENT] :
+ (hasType(type_Payment, Var_PAYMENT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_BALANCE2] :
+ ((hasType(type_Entity, Var_BALANCE2) & hasType(type_CurrencyMeasure, Var_BALANCE2)) =>
+(( ! [Var_BALANCE1] :
+ ((hasType(type_CurrencyMeasure, Var_BALANCE1) & hasType(type_Quantity, Var_BALANCE1)) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
+(((((f_origin(Var_PAYMENT,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_PAYMENT,Var_AMOUNT)) & (((f_currentAccountBalance(Var_ACCOUNT,f_ImmediatePastFn(f_WhenFn(Var_PAYMENT)),Var_BALANCE1)) & (Var_BALANCE2 = f_SubtractionFn(Var_BALANCE1,Var_AMOUNT)))))))) => (f_currentAccountBalance(Var_ACCOUNT,f_ImmediateFutureFn(f_WhenFn(Var_PAYMENT)),Var_BALANCE2))))))))))))))))))).
+
+fof(axFinancialLem23, axiom,
+ ( ! [Var_DEPOSIT] :
+ (hasType(type_Deposit, Var_DEPOSIT) =>
+(( ? [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) &
+(f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT))))))))).
+
+fof(axFinancialLem24, axiom,
+ ( ! [Var_DEPOSIT] :
+ (hasType(type_Deposit, Var_DEPOSIT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_BALANCE2] :
+ ((hasType(type_Entity, Var_BALANCE2) & hasType(type_CurrencyMeasure, Var_BALANCE2)) =>
+(( ! [Var_BALANCE1] :
+ ((hasType(type_CurrencyMeasure, Var_BALANCE1) & hasType(type_Quantity, Var_BALANCE1)) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
+(( ! [Var_TIMEOFDEPOSIT] :
+ (hasType(type_TimePosition, Var_TIMEOFDEPOSIT) =>
+(((((f_time(Var_DEPOSIT,Var_TIMEOFDEPOSIT)) & (((f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_DEPOSIT,Var_AMOUNT)) & (((f_currentAccountBalance(Var_ACCOUNT,f_ImmediatePastFn(f_WhenFn(Var_DEPOSIT)),Var_BALANCE1)) & (Var_BALANCE2 = f_AdditionFn(Var_BALANCE1,Var_AMOUNT)))))))))) => (f_currentAccountBalance(Var_ACCOUNT,f_ImmediateFutureFn(f_FutureFn(Var_DEPOSIT)),Var_BALANCE2)))))))))))))))))))))).
+
+fof(axFinancialLem25, axiom,
+ ( ! [Var_WITHDRAWAL] :
+ (hasType(type_Withdrawal, Var_WITHDRAWAL) =>
+(( ? [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) &
+(f_origin(Var_WITHDRAWAL,f_CurrencyFn(Var_ACCOUNT))))))))).
+
+fof(axFinancialLem26, axiom,
+ ( ! [Var_WITHDRAWAL] :
+ (hasType(type_Withdrawal, Var_WITHDRAWAL) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_BALANCE2] :
+ ((hasType(type_Entity, Var_BALANCE2) & hasType(type_CurrencyMeasure, Var_BALANCE2)) =>
+(( ! [Var_BALANCE1] :
+ ((hasType(type_CurrencyMeasure, Var_BALANCE1) & hasType(type_Quantity, Var_BALANCE1)) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
+(( ! [Var_TIMEOFWITHDRAWAL] :
+ (hasType(type_TimePosition, Var_TIMEOFWITHDRAWAL) =>
+(((((f_time(Var_WITHDRAWAL,Var_TIMEOFWITHDRAWAL)) & (((f_origin(Var_WITHDRAWAL,Var_ACCOUNT)) & (((f_transactionAmount(Var_WITHDRAWAL,Var_AMOUNT)) & (((f_currentAccountBalance(Var_ACCOUNT,f_ImmediatePastFn(f_WhenFn(Var_WITHDRAWAL)),Var_BALANCE1)) & (Var_BALANCE2 = f_SubtractionFn(Var_BALANCE1,Var_AMOUNT)))))))))) => (f_currentAccountBalance(Var_ACCOUNT,f_ImmediateFutureFn(f_FutureFn(Var_WITHDRAWAL)),Var_BALANCE2)))))))))))))))))))))).
+
+fof(axFinancialLem27, axiom,
+ ( ! [Var_MONEY] :
+ (hasType(type_CurrencyMeasure, Var_MONEY) =>
+(( ! [Var_OBJECT] :
+ ((hasType(type_Entity, Var_OBJECT) & hasType(type_Physical, Var_OBJECT)) =>
+(( ! [Var_SELLER] :
+ ((hasType(type_Object, Var_SELLER) & hasType(type_Entity, Var_SELLER)) =>
+(( ! [Var_BUYER] :
+ (hasType(type_Agent, Var_BUYER) =>
+(( ! [Var_PURCHASE] :
+ (hasType(type_Process, Var_PURCHASE) =>
+(((((f_agent(Var_PURCHASE,Var_BUYER)) & (((f_origin(Var_PURCHASE,Var_SELLER)) & (((f_patient(Var_PURCHASE,Var_OBJECT)) & (f_monetaryValue(Var_OBJECT,Var_MONEY)))))))) => (( ? [Var_PAYMENT] :
+ (hasType(type_Payment, Var_PAYMENT) &
+(((f_subProcess(Var_PAYMENT,Var_PURCHASE)) & (((f_transactionAmount(Var_PAYMENT,Var_MONEY)) & (f_destination(Var_PAYMENT,Var_SELLER)))))))))))))))))))))))))).
+
+fof(axFinancialLem28, axiom,
+ ( ! [Var_RATE_DECIMAL] :
+ ((hasType(type_Entity, Var_RATE_DECIMAL) & hasType(type_Quantity, Var_RATE_DECIMAL)) =>
+(( ! [Var_PERIOD] :
+ ((hasType(type_TimeInterval, Var_PERIOD) & hasType(type_PhysicalQuantity, Var_PERIOD)) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_Interest, Var_AMOUNT) & hasType(type_Entity, Var_AMOUNT)) =>
+(( ! [Var_RATE] :
+ ((hasType(type_InterestRate, Var_RATE) & hasType(type_PhysicalQuantity, Var_RATE)) =>
+(( ! [Var_BALANCE] :
+ ((hasType(type_CurrencyMeasure, Var_BALANCE) & hasType(type_Quantity, Var_BALANCE)) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_principalAmount(Var_ACCOUNT,Var_BALANCE)) & (((f_fixedInterestRate(Var_ACCOUNT,Var_RATE)) & (((f_simpleInterest(Var_ACCOUNT,Var_AMOUNT,Var_PERIOD)) & (Var_RATE_DECIMAL = f_DivisionFn(f_MagnitudeFn(Var_RATE),100)))))))) => (Var_AMOUNT = f_MultiplicationFn(f_MultiplicationFn(f_MagnitudeFn(Var_PERIOD),Var_BALANCE),Var_RATE_DECIMAL)))))))))))))))))))))).
+
+fof(axFinancialLem29, axiom,
+ ( ! [Var_MULTIPLY] :
+ ((hasType(type_Entity, Var_MULTIPLY) & hasType(type_Quantity, Var_MULTIPLY)) =>
+(( ! [Var_EXPONENT] :
+ ((hasType(type_Entity, Var_EXPONENT) & hasType(type_Quantity, Var_EXPONENT)) =>
+(( ! [Var_ADD] :
+ ((hasType(type_Entity, Var_ADD) & hasType(type_Quantity, Var_ADD)) =>
+(( ! [Var_RATE_DECIMAL] :
+ ((hasType(type_Entity, Var_RATE_DECIMAL) & hasType(type_Quantity, Var_RATE_DECIMAL)) =>
+(( ! [Var_PERIOD] :
+ ((hasType(type_TimeInterval, Var_PERIOD) & hasType(type_PhysicalQuantity, Var_PERIOD)) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_Entity, Var_INTEREST)) =>
+(( ! [Var_RATE] :
+ ((hasType(type_InterestRate, Var_RATE) & hasType(type_Quantity, Var_RATE)) =>
+(( ! [Var_BALANCE] :
+ ((hasType(type_CurrencyMeasure, Var_BALANCE) & hasType(type_Quantity, Var_BALANCE)) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_principalAmount(Var_ACCOUNT,Var_BALANCE)) & (((f_fixedInterestRate(Var_ACCOUNT,Var_RATE)) & (((f_compoundInterest(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)) & (((Var_RATE_DECIMAL = f_DivisionFn(Var_RATE,100)) & (((Var_ADD = f_AdditionFn(1,Var_RATE_DECIMAL)) & (((Var_EXPONENT = f_ExponentiationFn(Var_ADD,f_MagnitudeFn(Var_PERIOD))) & (Var_MULTIPLY = f_MultiplicationFn(Var_EXPONENT,Var_BALANCE)))))))))))))) => (Var_INTEREST = f_SubtractionFn(Var_MULTIPLY,Var_BALANCE))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem30, axiom,
+ ( ! [Var_RATE] :
+ ((hasType(type_Entity, Var_RATE) & hasType(type_InterestRate, Var_RATE)) =>
+(( ! [Var_RATE_DECIMAL] :
+ ((hasType(type_Entity, Var_RATE_DECIMAL) & hasType(type_Quantity, Var_RATE_DECIMAL)) =>
+(( ! [Var_PRINCIPAL] :
+ ((hasType(type_CurrencyMeasure, Var_PRINCIPAL) & hasType(type_Quantity, Var_PRINCIPAL)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_Quantity, Var_INTEREST)) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_simpleInterest(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)) & (((f_principalAmount(Var_ACCOUNT,Var_PRINCIPAL)) & (((Var_RATE_DECIMAL = f_DivisionFn(Var_INTEREST,Var_PRINCIPAL)) & (Var_RATE = f_MultiplicationFn(Var_RATE_DECIMAL,100)))))))) => (f_interestRatePerPeriod(Var_ACCOUNT,Var_RATE,Var_PERIOD)))))))))))))))))))))).
+
+fof(axFinancialLem31, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_PersonalAccount, Var_ACCOUNT) =>
+(( ! [Var_PRIMERATE] :
+ ((hasType(type_InterestRate, Var_PRIMERATE) & hasType(type_Quantity, Var_PRIMERATE)) =>
+(( ! [Var_RATE] :
+ ((hasType(type_InterestRate, Var_RATE) & hasType(type_Quantity, Var_RATE)) =>
+(( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(((((f_currentInterestRate(Var_ACCOUNT,Var_DATE,Var_RATE)) & (f_primeInterestRate(Var_DATE,Var_PRIMERATE)))) => (f_greaterThan(Var_RATE,Var_PRIMERATE)))))))))))))))).
+
+fof(axFinancialLem32, axiom,
+ ( ! [Var_DATE] :
+ ((hasType(type_TimeInterval, Var_DATE) & hasType(type_TimePosition, Var_DATE)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_AGREEMENT] :
+ (hasType(type_Contract, Var_AGREEMENT) =>
+(((((f_agreementPeriod(Var_AGREEMENT,Var_PERIOD)) & (f_overlapsTemporally(Var_DATE,Var_PERIOD)))) <=> (f_agreementActive(Var_AGREEMENT,Var_DATE))))))))))))).
+
+fof(axFinancialLem33, axiom,
+ ( ! [Var_PRINCIPAL] :
+ (hasType(type_CurrencyMeasure, Var_PRINCIPAL) =>
+(( ! [Var_DATE] :
+ ((hasType(type_Day, Var_DATE) & hasType(type_TimePosition, Var_DATE)) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_maturityDate(Var_ACCOUNT,Var_DATE)) & (f_principalAmount(Var_ACCOUNT,Var_PRINCIPAL)))) => (f_amountDue(Var_ACCOUNT,Var_PRINCIPAL,Var_DATE))))))))))))).
+
+fof(axFinancialLem34, axiom,
+ ( ! [Var_END] :
+ ((hasType(type_TimeInterval, Var_END) & hasType(type_Day, Var_END)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_ACCOUNT] :
+ ((hasType(type_Contract, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
+(((((f_agreementPeriod(Var_ACCOUNT,Var_PERIOD)) & (f_finishes(Var_END,Var_PERIOD)))) <=> (f_maturityDate(Var_ACCOUNT,Var_END))))))))))))).
+
+fof(axFinancialLem35, axiom,
+ ( ! [Var_BALANCE] :
+ (hasType(type_CurrencyMeasure, Var_BALANCE) =>
+(( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(( ! [Var_ACCOUNT] :
+ ((hasType(type_Contract, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
+(((((f_effectiveDate(Var_ACCOUNT,Var_DATE)) & (f_currentAccountBalance(Var_ACCOUNT,Var_DATE,Var_BALANCE)))) => (f_originalBalance(Var_ACCOUNT,Var_BALANCE))))))))))))).
+
+fof(axFinancialLem36, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_LiabilityAccount, Var_ACCOUNT) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
+(( ! [Var_MINPAYMENT] :
+ ((hasType(type_CurrencyMeasure, Var_MINPAYMENT) & hasType(type_Quantity, Var_MINPAYMENT)) =>
+(((((f_minimumPayment(Var_ACCOUNT,Var_MINPAYMENT,inst_MonthDuration)) & (( ? [Var_MONTH] :
+ (hasType(type_Month, Var_MONTH) &
+(( ? [Var_PAYMENT] :
+ (hasType(type_Process, Var_PAYMENT) &
+(((f_destination(Var_PAYMENT,f_CurrencyFn(Var_ACCOUNT))) & (((f_paymentsPerPeriod(Var_ACCOUNT,Var_AMOUNT,Var_MONTH)) & (f_lessThan(Var_AMOUNT,Var_MINPAYMENT)))))))))))))) => (( ? [Var_PENALTY] :
+ (hasType(type_Penalty, Var_PENALTY) &
+(f_destination(Var_PENALTY,f_CurrencyFn(Var_ACCOUNT))))))))))))))))).
+
+fof(axFinancialLem37, axiom,
+ ( ! [Var_OVERDRAFT] :
+ ((hasType(type_Entity, Var_OVERDRAFT) & hasType(type_RealNumber, Var_OVERDRAFT)) =>
+(( ! [Var_BALANCE] :
+ ((hasType(type_RealNumber, Var_BALANCE) & hasType(type_Quantity, Var_BALANCE)) =>
+(( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_currentAccountBalance(Var_ACCOUNT,Var_DATE,f_MeasureFn(Var_BALANCE,inst_UnitedStatesDollar))) & (((f_lessThan(Var_BALANCE,0)) & (Var_OVERDRAFT = f_SubtractionFn(0,Var_BALANCE)))))) => (f_overdraft(Var_ACCOUNT,f_MeasureFn(Var_OVERDRAFT,inst_UnitedStatesDollar),Var_DATE)))))))))))))))).
+
+fof(axFinancialLem38, axiom,
+ ( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_LOAN] :
+ ((hasType(type_Loan, Var_LOAN) & hasType(type_Contract, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
+(((((f_downPayment(Var_LOAN,Var_AMOUNT)) & (f_effectiveDate(Var_LOAN,Var_DATE)))) => (( ? [Var_PAYMENT] :
+ ((hasType(type_FinancialTransaction, Var_PAYMENT) & hasType(type_Physical, Var_PAYMENT) & hasType(type_Process, Var_PAYMENT)) &
+(((f_transactionAmount(Var_PAYMENT,Var_AMOUNT)) & (((f_date(Var_PAYMENT,Var_DATE)) & (f_destination(Var_PAYMENT,f_CurrencyFn(Var_LOAN))))))))))))))))))))).
+
+fof(axFinancialLem39, axiom,
+ ( ! [Var_BALANCE] :
+ ((hasType(type_Entity, Var_BALANCE) & hasType(type_CurrencyMeasure, Var_BALANCE)) =>
+(( ! [Var_VALUE] :
+ ((hasType(type_CurrencyMeasure, Var_VALUE) & hasType(type_Quantity, Var_VALUE)) =>
+(( ! [Var_PURCHASE] :
+ ((hasType(type_Object, Var_PURCHASE) & hasType(type_Physical, Var_PURCHASE)) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
+(( ! [Var_LOAN] :
+ ((hasType(type_Loan, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
+(((((f_downPayment(Var_LOAN,Var_AMOUNT)) & (((f_loanForPurchase(Var_LOAN,Var_PURCHASE)) & (((f_monetaryValue(Var_PURCHASE,Var_VALUE)) & (Var_BALANCE = f_SubtractionFn(Var_VALUE,Var_AMOUNT)))))))) => (f_originalBalance(Var_LOAN,Var_BALANCE))))))))))))))))))).
+
+fof(axFinancialLem40, axiom,
+ ( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_ACTION] :
+ ((hasType(type_FinancialTransaction, Var_ACTION) & hasType(type_Process, Var_ACTION)) =>
+(( ! [Var_BANK] :
+ ((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_Agent, Var_BANK)) =>
+(((f_serviceFee(Var_BANK,Var_ACTION,Var_AMOUNT)) => (( ? [Var_FEE] :
+ (hasType(type_ChargingAFee, Var_FEE) &
+(((f_agent(Var_FEE,Var_BANK)) & (((f_causes(Var_ACTION,Var_FEE)) & (f_amountCharged(Var_FEE,Var_AMOUNT)))))))))))))))))))).
+
+fof(axFinancialLem41, axiom,
+ ( ! [Var_TAX] :
+ (hasType(type_Tax, Var_TAX) =>
+(( ? [Var_ORG] :
+ (hasType(type_Government, Var_ORG) &
+(f_agent(Var_TAX,Var_ORG)))))))).
+
+fof(axFinancialLem42, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_InterestBearingAccount, Var_ACCOUNT) =>
+(( ? [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) &
+(( ? [Var_RATE] :
+ (hasType(type_InterestRate, Var_RATE) &
+(f_interestRatePerPeriod(Var_ACCOUNT,Var_RATE,Var_PERIOD))))))))))).
+
+fof(axFinancialLem43, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_PersonalAccount, Var_ACCOUNT) =>
+(( ! [Var_AGENT] :
+ (hasType(type_Human, Var_AGENT) =>
+(f_accountHolder(Var_ACCOUNT,Var_AGENT)))))))).
+
+fof(axFinancialLem44, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_SavingsAccount, Var_ACCOUNT) =>
+(( ! [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) =>
+(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) => (( ? [Var_AUTHORIZATION] :
+ (hasType(type_AuthorizationOfTransaction, Var_AUTHORIZATION) &
+(f_subProcess(Var_AUTHORIZATION,Var_TRANSACTION))))))))))))).
+
+fof(axFinancialLem45, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_SavingsAccount, Var_ACCOUNT) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) =>
+(((((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_interestEarned(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)))) => (( ? [Var_PAYMENT] :
+ ((hasType(type_Process, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
+(((f_destination(Var_PAYMENT,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_PAYMENT,Var_INTEREST)) & (f_destination(Var_PAYMENT,Var_AGENT))))))))))))))))))))))).
+
+fof(axFinancialLem46, axiom,
+ ( ! [Var_CD] :
+ (hasType(type_CertificateOfDeposit, Var_CD) =>
+(( ? [Var_DATE] :
+ (hasType(type_Day, Var_DATE) &
+(f_maturityDate(Var_CD,Var_DATE)))))))).
+
+fof(axFinancialLem47, axiom,
+ ( ! [Var_CD] :
+ (hasType(type_CertificateOfDeposit, Var_CD) =>
+(( ! [Var_WITHDRAWAL] :
+ (hasType(type_Withdrawal, Var_WITHDRAWAL) =>
+(( ! [Var_DATEOFWITHDRAWAL] :
+ ((hasType(type_Day, Var_DATEOFWITHDRAWAL) & hasType(type_TimeInterval, Var_DATEOFWITHDRAWAL)) =>
+(( ! [Var_MATURITYDATE] :
+ ((hasType(type_Day, Var_MATURITYDATE) & hasType(type_TimeInterval, Var_MATURITYDATE)) =>
+(((((f_maturityDate(Var_CD,Var_MATURITYDATE)) & (((f_origin(Var_WITHDRAWAL,f_CurrencyFn(Var_CD))) & (((f_date(Var_WITHDRAWAL,Var_DATEOFWITHDRAWAL)) & (f_before(f_EndFn(Var_DATEOFWITHDRAWAL),f_BeginFn(Var_MATURITYDATE))))))))) => (( ? [Var_PENALTY] :
+ (hasType(type_Penalty, Var_PENALTY) &
+(((f_destination(Var_PENALTY,f_CurrencyFn(Var_CD))) & (f_causes(Var_WITHDRAWAL,Var_PENALTY))))))))))))))))))))).
+
+fof(axFinancialLem48, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_TraditionalSavingsAccount, Var_ACCOUNT) =>
+(( ~ ( ? [Var_DATE] :
+ (hasType(type_Day, Var_DATE) &
+(f_maturityDate(Var_ACCOUNT,Var_DATE))))))))).
+
+fof(axFinancialLem49, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_TraditionalSavingsAccount, Var_ACCOUNT) =>
+(( ! [Var_WITHDRAWAL] :
+ (hasType(type_Withdrawal, Var_WITHDRAWAL) =>
+(((f_origin(Var_WITHDRAWAL,f_CurrencyFn(Var_ACCOUNT))) => (( ? [Var_PENALTY] :
+ (hasType(type_Penalty, Var_PENALTY) &
+(((f_destination(Var_PENALTY,f_CurrencyFn(Var_ACCOUNT))) & (f_causes(Var_WITHDRAWAL,Var_PENALTY))))))))))))))).
+
+fof(axFinancialLem50, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_CheckingAccount, Var_ACCOUNT) =>
+(( ! [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) =>
+(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) => (((( ? [Var_CHECK] :
+ (hasType(type_Check, Var_CHECK) &
+(f_instrument(Var_TRANSACTION,Var_CHECK))))) | (( ? [Var_DEBITCARD] :
+ (hasType(type_DebitCard, Var_DEBITCARD) &
+(f_instrument(Var_TRANSACTION,Var_DEBITCARD))))))))))))))).
+
+fof(axFinancialLem51, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_LiabilityAccount, Var_ACCOUNT) =>
+(( ! [Var_BANK] :
+ ((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_CognitiveAgent, Var_BANK)) =>
+(( ! [Var_AGENT] :
+ (hasType(type_CognitiveAgent, Var_AGENT) =>
+(((((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_accountAt(Var_ACCOUNT,Var_BANK)))) => (( ? [Var_DEBT] :
+ (hasType(type_Liability, Var_DEBT) &
+(((f_agreementMember(Var_DEBT,Var_AGENT)) & (f_agreementMember(Var_DEBT,Var_BANK)))))))))))))))))).
+
+fof(axFinancialLem52, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_CreditAccount, Var_ACCOUNT) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Object, Var_AGENT)) =>
+(( ! [Var_ORGANIZATION] :
+ ((hasType(type_FinancialOrganization, Var_ORGANIZATION) & hasType(type_Entity, Var_ORGANIZATION)) =>
+(((((f_accountAt(Var_ACCOUNT,Var_ORGANIZATION)) & (((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_interestEarned(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)))))) => (( ? [Var_PAYMENT] :
+ ((hasType(type_Process, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
+(((f_origin(Var_PAYMENT,Var_AGENT)) & (((f_transactionAmount(Var_PAYMENT,Var_INTEREST)) & (f_destination(Var_PAYMENT,Var_ORGANIZATION)))))))))))))))))))))))))).
+
+fof(axFinancialLem53, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_CreditCardAccount, Var_ACCOUNT) =>
+(( ! [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) =>
+(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) => (( ? [Var_CARD] :
+ (hasType(type_CreditCard, Var_CARD) &
+(f_instrument(Var_TRANSACTION,Var_CARD))))))))))))).
+
+fof(axFinancialLem54, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) =>
+(( ? [Var_LENDER] :
+ (hasType(type_CognitiveAgent, Var_LENDER) &
+(( ? [Var_BORROWER] :
+ (hasType(type_CognitiveAgent, Var_BORROWER) &
+(((f_borrower(Var_LOAN,Var_BORROWER)) & (f_lender(Var_LOAN,Var_LENDER))))))))))))).
+
+fof(axFinancialLem55, axiom,
+ ( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_LENDER] :
+ ((hasType(type_CognitiveAgent, Var_LENDER) & hasType(type_Entity, Var_LENDER)) =>
+(( ! [Var_BORROWER] :
+ ((hasType(type_CognitiveAgent, Var_BORROWER) & hasType(type_Object, Var_BORROWER)) =>
+(( ! [Var_LOAN] :
+ ((hasType(type_Loan, Var_LOAN) & hasType(type_Contract, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
+(((((f_borrower(Var_LOAN,Var_BORROWER)) & (((f_lender(Var_LOAN,Var_LENDER)) & (((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_interestEarned(Var_LOAN,Var_INTEREST,Var_PERIOD)))))))) => (( ? [Var_PAYMENT] :
+ ((hasType(type_Process, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
+(((f_origin(Var_PAYMENT,Var_BORROWER)) & (((f_transactionAmount(Var_PAYMENT,Var_INTEREST)) & (f_destination(Var_PAYMENT,Var_LENDER)))))))))))))))))))))))))).
+
+fof(axFinancialLem56, axiom,
+ ( ! [Var_AGENT] :
+ ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
+(( ! [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) =>
+(((f_lender(Var_LOAN,Var_AGENT)) => (( ? [Var_LENDING] :
+ (hasType(type_Lending, Var_LENDING) &
+(f_agent(Var_LENDING,Var_AGENT))))))))))))).
+
+fof(axFinancialLem57, axiom,
+ ( ! [Var_AGENT] :
+ ((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
+(( ! [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) =>
+(((f_borrower(Var_LOAN,Var_AGENT)) => (( ? [Var_BORROWING] :
+ (hasType(type_Borrowing, Var_BORROWING) &
+(f_agent(Var_BORROWING,Var_AGENT))))))))))))).
+
+fof(axFinancialLem58, axiom,
+ ( ! [Var_COLLATERAL] :
+ (hasType(type_Collateral, Var_COLLATERAL) =>
+(( ? [Var_LOAN] :
+ (hasType(type_SecuredLoan, Var_LOAN) &
+(f_securedBy(Var_LOAN,Var_COLLATERAL)))))))).
+
+fof(axFinancialLem59, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) =>
+(( ! [Var_DEFAULT] :
+ (hasType(type_FinancialDefault, Var_DEFAULT) =>
+(( ! [Var_BANK] :
+ ((hasType(type_CognitiveAgent, Var_BANK) & hasType(type_Agent, Var_BANK)) =>
+(( ! [Var_SECURITY] :
+ ((hasType(type_Collateral, Var_SECURITY) & hasType(type_Object, Var_SECURITY)) =>
+(((((f_securedBy(Var_LOAN,Var_SECURITY)) & (((f_lender(Var_LOAN,Var_BANK)) & (f_patient(Var_DEFAULT,Var_LOAN)))))) => (f_holdsDuring(f_ImmediateFutureFn(f_WhenFn(Var_DEFAULT)),possesses(Var_BANK,Var_SECURITY))))))))))))))))).
+
+fof(axFinancialLem60, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_SecuredLoan, Var_LOAN) =>
+(( ? [Var_SECURITY] :
+ (hasType(type_Collateral, Var_SECURITY) &
+(f_securedBy(Var_LOAN,Var_SECURITY)))))))).
+
+fof(axFinancialLem61, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_Mortgage, Var_LOAN) =>
+(( ? [Var_ESTATE] :
+ (hasType(type_RealEstate, Var_ESTATE) &
+(f_loanForPurchase(Var_LOAN,Var_ESTATE)))))))).
+
+fof(axFinancialLem62, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_Mortgage, Var_LOAN) =>
+(( ! [Var_REALESTATE] :
+ ((hasType(type_Object, Var_REALESTATE) & hasType(type_Collateral, Var_REALESTATE)) =>
+(((f_loanForPurchase(Var_LOAN,Var_REALESTATE)) => (f_securedBy(Var_LOAN,Var_REALESTATE)))))))))).
+
+fof(axFinancialLem63, axiom,
+ ( ! [Var_REFINANCING] :
+ (hasType(type_Refinancing, Var_REFINANCING) =>
+(( ! [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(( ! [Var_BORROWER] :
+ (hasType(type_CognitiveAgent, Var_BORROWER) =>
+(( ! [Var_COLLATERAL] :
+ (hasType(type_Collateral, Var_COLLATERAL) =>
+(( ! [Var_TIME] :
+ (hasType(type_TimePosition, Var_TIME) =>
+(((((f_time(Var_REFINANCING,Var_TIME)) & (((f_securedBy(Var_LOAN,Var_COLLATERAL)) & (((f_borrower(Var_LOAN,Var_BORROWER)) & (((f_currentAccountBalance(Var_LOAN,Var_DATE,Var_AMOUNT)) & (f_patient(Var_REFINANCING,Var_LOAN)))))))))) => (( ? [Var_NEWLOAN] :
+ (hasType(type_Loan, Var_NEWLOAN) &
+(( ? [Var_PAYMENT] :
+ ((hasType(type_Process, Var_PAYMENT) & hasType(type_Physical, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
+(((f_borrower(Var_NEWLOAN,Var_BORROWER)) & (((f_securedBy(Var_LOAN,Var_COLLATERAL)) & (((f_destination(Var_PAYMENT,f_CurrencyFn(Var_LOAN))) & (((f_time(Var_PAYMENT,Var_TIME)) & (((f_origin(Var_PAYMENT,f_CurrencyFn(Var_NEWLOAN))) & (f_transactionAmount(Var_PAYMENT,Var_AMOUNT))))))))))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem64, axiom,
+ ( ! [Var_COMMITMENT] :
+ (hasType(type_LoanCommitment, Var_COMMITMENT) =>
+(( ? [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) &
+(( ? [Var_BORROWER] :
+ (hasType(type_CognitiveAgent, Var_BORROWER) &
+(( ? [Var_LENDER] :
+ (hasType(type_CognitiveAgent, Var_LENDER) &
+(((f_lender(Var_LOAN,Var_LENDER)) & (((f_borrower(Var_LOAN,Var_BORROWER)) & (((f_agreementMember(Var_COMMITMENT,Var_LENDER)) & (f_agreementMember(Var_COMMITMENT,Var_BORROWER)))))))))))))))))))).
+
+fof(axFinancialLem65, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_BankTermLoan, Var_LOAN) =>
+(( ! [Var_DURATION] :
+ ((hasType(type_RealNumber, Var_DURATION) & hasType(type_Quantity, Var_DURATION)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_duration(Var_PERIOD,f_MeasureFn(Var_DURATION,inst_YearDuration))))) => (f_greaterThanOrEqualTo(Var_DURATION,1))))))))))))).
+
+fof(axFinancialLem66, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_ConsolidationLoan, Var_LOAN) =>
+(( ? [Var_LOAN1] :
+ (hasType(type_Loan, Var_LOAN1) &
+(( ? [Var_LOAN2] :
+ (hasType(type_Loan, Var_LOAN2) &
+(( ? [Var_PAYMENT2] :
+ (hasType(type_Process, Var_PAYMENT2) &
+(( ? [Var_PAYMENT1] :
+ (hasType(type_Process, Var_PAYMENT1) &
+(((f_destination(Var_PAYMENT1,f_CurrencyFn(Var_LOAN1))) & (((f_destination(Var_PAYMENT2,f_CurrencyFn(Var_LOAN2))) & (((f_origin(Var_PAYMENT1,f_CurrencyFn(Var_LOAN))) & (f_origin(Var_PAYMENT2,f_CurrencyFn(Var_LOAN)))))))))))))))))))))))).
+
+fof(axFinancialLem67, axiom,
+ ( ! [Var_MORTGAGE] :
+ (hasType(type_ConventionalMortgage, Var_MORTGAGE) =>
+(( ? [Var_GOVERNMENT] :
+ (hasType(type_Government, Var_GOVERNMENT) &
+(f_insured(Var_MORTGAGE,Var_GOVERNMENT)))))))).
+
+fof(axFinancialLem68, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_DayLoan, Var_LOAN) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_duration(Var_PERIOD,f_MeasureFn(1,inst_DayDuration))))))))))).
+
+fof(axFinancialLem69, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_SinglePaymentLoan, Var_LOAN) =>
+(( ! [Var_MATURITY] :
+ ((hasType(type_Day, Var_MATURITY) & hasType(type_TimePosition, Var_MATURITY)) =>
+(( ! [Var_PRINCIPAL] :
+ (hasType(type_CurrencyMeasure, Var_PRINCIPAL) =>
+(((((f_principalAmount(Var_LOAN,Var_PRINCIPAL)) & (f_maturityDate(Var_LOAN,Var_MATURITY)))) => (f_amountDue(Var_LOAN,Var_PRINCIPAL,Var_MATURITY))))))))))))).
+
+fof(axFinancialLem70, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_InterestOnlyLoan, Var_LOAN) =>
+(( ! [Var_DATE] :
+ ((hasType(type_TimePosition, Var_DATE) & hasType(type_TimeInterval, Var_DATE)) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
+(( ! [Var_PRINCIPAL] :
+ (hasType(type_CurrencyMeasure, Var_PRINCIPAL) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (((f_principalAmount(Var_LOAN,Var_PRINCIPAL)) & (f_interestEarned(Var_LOAN,Var_INTEREST,Var_PERIOD)))))) => (((f_amountDue(Var_LOAN,Var_PRINCIPAL,f_EndFn(Var_PERIOD))) & (((f_amountDue(Var_LOAN,Var_INTEREST,Var_DATE)) & (f_before(f_EndFn(Var_DATE),f_EndFn(Var_PERIOD)))))))))))))))))))))))).
+
+fof(axFinancialLem71, axiom,
+ ( ! [Var_INDEX] :
+ (hasType(type_Index, Var_INDEX) =>
+(( ? [Var_PERFORMANCE] :
+ (hasType(type_EconomicIndicator, Var_PERFORMANCE) &
+(f_benchmark(Var_PERFORMANCE,Var_INDEX)))))))).
+
+fof(axFinancialLem72, axiom,
+ ( ! [Var_INFLATION] :
+ (hasType(type_Inflation, Var_INFLATION) =>
+(( ! [Var_CPI] :
+ (hasType(type_ConsumerPriceIndex, Var_CPI) =>
+(( ! [Var_PPI] :
+ (hasType(type_ProducerPriceIndex, Var_PPI) =>
+(((f_benchmark(Var_INFLATION,Var_CPI)) | (f_benchmark(Var_INFLATION,Var_PPI))))))))))))).
+
+fof(axFinancialLem73, axiom,
+ ( ! [Var_INDEX] :
+ (hasType(type_InflationIndex, Var_INDEX) =>
+(( ? [Var_INFLATION] :
+ (hasType(type_Inflation, Var_INFLATION) &
+(f_benchmark(Var_INFLATION,Var_INDEX)))))))).
+
+fof(axFinancialLem74, axiom,
+ ( ! [Var_R] :
+ (hasType(type_RealNumber, Var_R) =>
+(( ! [Var_N] :
+ ((hasType(type_Nation, Var_N) & hasType(type_Entity, Var_N)) =>
+(((f_inflationRateInCountry(Var_N,Var_R)) => (( ? [Var_I] :
+ (hasType(type_Inflation, Var_I) &
+(((f_duration(f_WhenFn(Var_I),inst_YearDuration)) & (((f_experiencer(Var_I,Var_N)) & (f_inflationRate(Var_I,Var_R))))))))))))))))).
+
+fof(axFinancialLem75, axiom,
+ ( ! [Var_INDEX] :
+ (hasType(type_StockIndex, Var_INDEX) =>
+(( ? [Var_STOCK] :
+ (hasType(type_Stock, Var_STOCK) &
+(f_benchmark(Var_INDEX,Var_STOCK)))))))).
+
+fof(axFinancialLem76, axiom,
+ ( ! [Var_INVESTMENT] :
+ (hasType(type_Investment, Var_INVESTMENT) =>
+(( ? [Var_AGENT] :
+ (hasType(type_Agent, Var_AGENT) &
+(( ? [Var_INVESTING] :
+ (hasType(type_Process, Var_INVESTING) &
+(((f_agent(Var_INVESTING,Var_AGENT)) & (f_possesses(Var_AGENT,Var_INVESTMENT))))))))))))).
+
+fof(axFinancialLem77, axiom,
+ ( ! [Var_ATTRIBUTE] :
+ (hasType(type_InvestmentAttribute, Var_ATTRIBUTE) =>
+(( ? [Var_ACCOUNT] :
+ (hasType(type_InvestmentAccount, Var_ACCOUNT) &
+(f_attribute(Var_ACCOUNT,Var_ATTRIBUTE)))))))).
+
+fof(axFinancialLem78, axiom,
+ ( ! [Var_AGENT] :
+ (hasType(type_Agent, Var_AGENT) =>
+(( ! [Var_MONEY] :
+ (hasType(type_CurrencyMeasure, Var_MONEY) =>
+(( ! [Var_OBJ] :
+ ((hasType(type_Physical, Var_OBJ) & hasType(type_Entity, Var_OBJ)) =>
+(((f_price(Var_OBJ,Var_MONEY,Var_AGENT)) => (( ? [Var_BUYING] :
+ (hasType(type_Buying, Var_BUYING) &
+(((f_agent(Var_BUYING,Var_AGENT)) & (((f_patient(Var_BUYING,Var_OBJ)) & (f_transactionAmount(Var_BUYING,Var_MONEY)))))))))))))))))))).
+
+fof(axFinancialLem79, axiom,
+ ( ! [Var_PLACE] :
+ (hasType(type_PlacingAnOrder, Var_PLACE) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Entity, Var_TIME) & hasType(type_TimeInterval, Var_TIME)) =>
+(((f_WhenFn(Var_PLACE) = Var_TIME) => (( ? [Var_PERIOD] :
+ ((hasType(type_Entity, Var_PERIOD) & hasType(type_TimeInterval, Var_PERIOD)) &
+(( ? [Var_ORDER] :
+ (hasType(type_Physical, Var_ORDER) &
+(((f_WhenFn(Var_ORDER) = Var_PERIOD) & (f_meetsTemporally(Var_TIME,Var_PERIOD)))))))))))))))))).
+
+fof(axFinancialLem80, axiom,
+ ( ! [Var_ORDER] :
+ (hasType(type_LimitOrder, Var_ORDER) =>
+(( ? [Var_PRICE] :
+ (hasType(type_CurrencyMeasure, Var_PRICE) &
+(f_limitPrice(Var_ORDER,Var_PRICE)))))))).
+
+fof(axFinancialLem81, axiom,
+ ( ! [Var_BROKER] :
+ (hasType(type_Broker, Var_BROKER) =>
+(( ? [Var_CONTRACT] :
+ (hasType(type_ServiceContract, Var_CONTRACT) &
+(f_agreementMember(Var_CONTRACT,Var_BROKER)))))))).
+
+fof(axFinancialLem82, axiom,
+ ( ! [Var_INVESTMENT] :
+ (hasType(type_TaxFreeInvestment, Var_INVESTMENT) =>
+(( ? [Var_TAX] :
+ (hasType(type_Tax, Var_TAX) &
+(f_origin(Var_TAX,Var_INVESTMENT)))))))).
+
+fof(axFinancialLem83, axiom,
+ ( ! [Var_INVESTMENT] :
+ (hasType(type_TaxableInvestment, Var_INVESTMENT) =>
+(( ? [Var_TAX] :
+ (hasType(type_Tax, Var_TAX) &
+(f_origin(Var_TAX,Var_INVESTMENT)))))))).
+
+fof(axFinancialLem84, axiom,
+ ( ! [Var_STOCK] :
+ (hasType(type_PreferredStock, Var_STOCK) =>
+(( ? [Var_DIVIDEND] :
+ (hasType(type_Dividend, Var_DIVIDEND) &
+(( ? [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) &
+(f_transactionAmount(Var_DIVIDEND,Var_AMOUNT))))))))))).
+
+fof(axFinancialLem85, axiom,
+ ( ! [Var_STOCK] :
+ (hasType(type_PennyStock, Var_STOCK) =>
+(( ! [Var_DATE] :
+ (hasType(type_Agent, Var_DATE) =>
+(( ! [Var_PRICE] :
+ ((hasType(type_RealNumber, Var_PRICE) & hasType(type_Quantity, Var_PRICE)) =>
+(((f_askPrice(Var_STOCK,f_MeasureFn(Var_PRICE,inst_UnitedStatesDollar),Var_DATE)) => (f_lessThan(Var_PRICE,5))))))))))))).
+
+fof(axFinancialLem86, axiom,
+ ( ! [Var_TIMEAFTERSPLIT] :
+ ((hasType(type_Agent, Var_TIMEAFTERSPLIT) & hasType(type_TimeInterval, Var_TIMEAFTERSPLIT)) =>
+(( ! [Var_NEWNUMBER] :
+ ((hasType(type_Entity, Var_NEWNUMBER) & hasType(type_RealNumber, Var_NEWNUMBER)) =>
+(( ! [Var_N3] :
+ ((hasType(type_Entity, Var_N3) & hasType(type_Quantity, Var_N3)) =>
+(( ! [Var_TIMEOFSPLIT] :
+ ((hasType(type_Entity, Var_TIMEOFSPLIT) & hasType(type_TimeInterval, Var_TIMEOFSPLIT)) =>
+(( ! [Var_N2] :
+ ((hasType(type_Integer, Var_N2) & hasType(type_Quantity, Var_N2)) =>
+(( ! [Var_N1] :
+ ((hasType(type_Integer, Var_N1) & hasType(type_Quantity, Var_N1)) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Agent, Var_TIME) & hasType(type_TimeInterval, Var_TIME)) =>
+(( ! [Var_NUMBER] :
+ ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) =>
+(( ! [Var_STOCKS] :
+ (hasType(type_Physical, Var_STOCKS) =>
+(((((f_price(Var_STOCKS,f_MeasureFn(Var_NUMBER,inst_UnitedStatesDollar),Var_TIME)) & (( ? [Var_EVENT] :
+ ((hasType(type_StockSplit, Var_EVENT) & hasType(type_Physical, Var_EVENT)) &
+(((f_splitFor(Var_EVENT,Var_N1,Var_N2)) & (f_WhenFn(Var_EVENT) = Var_TIMEOFSPLIT)))))))) => (((Var_N3 = f_MultiplicationFn(Var_NUMBER,Var_N1)) & (((Var_NEWNUMBER = f_DivisionFn(Var_N3,Var_N2)) & (((f_price(Var_STOCKS,f_MeasureFn(Var_NEWNUMBER,inst_UnitedStatesDollar),Var_TIMEAFTERSPLIT)) & (((f_meetsTemporally(Var_TIME,Var_TIMEOFSPLIT)) & (f_meetsTemporally(Var_TIMEOFSPLIT,Var_TIMEAFTERSPLIT))))))))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem87, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_Bond, Var_BOND) =>
+(( ? [Var_DATE] :
+ (hasType(type_Day, Var_DATE) &
+(f_maturityDate(Var_BOND,Var_DATE)))))))).
+
+fof(axFinancialLem88, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_Bond, Var_BOND) =>
+(( ! [Var_BONDHOLDER] :
+ ((hasType(type_Agent, Var_BONDHOLDER) & hasType(type_Entity, Var_BONDHOLDER)) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
+(((((f_couponInterest(Var_BOND,Var_INTEREST)) & (f_possesses(Var_BONDHOLDER,Var_BOND)))) => (( ? [Var_PAYMENT] :
+ (hasType(type_Process, Var_PAYMENT) &
+(( ? [Var_PERIOD] :
+ (hasType(type_TimeDuration, Var_PERIOD) &
+(((f_periodicPayment(f_AccountFn(Var_BOND),Var_INTEREST,Var_PERIOD)) & (f_destination(Var_PAYMENT,Var_BONDHOLDER))))))))))))))))))))).
+
+fof(axFinancialLem89, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_ASSET] :
+ ((hasType(type_Object, Var_ASSET) & hasType(type_FinancialAsset, Var_ASSET)) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
+(((((f_possesses(Var_AGENT,Var_ASSET)) & (Var_ACCOUNT = f_AccountFn(Var_ASSET)))) <=> (f_accountHolder(Var_ACCOUNT,Var_AGENT))))))))))))).
+
+fof(axFinancialLem90, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_ZeroCouponBond, Var_BOND) =>
+(( ! [Var_BONDACCOUNT] :
+ (hasType(type_FinancialAccount, Var_BONDACCOUNT) =>
+(( ! [Var_TOTAL] :
+ ((hasType(type_Entity, Var_TOTAL) & hasType(type_CurrencyMeasure, Var_TOTAL)) =>
+(( ! [Var_INTEREST] :
+ ((hasType(type_Interest, Var_INTEREST) & hasType(type_Quantity, Var_INTEREST)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_PRINCIPAL] :
+ ((hasType(type_CurrencyMeasure, Var_PRINCIPAL) & hasType(type_Quantity, Var_PRINCIPAL)) =>
+(( ! [Var_BONDHOLDER] :
+ ((hasType(type_Agent, Var_BONDHOLDER) & hasType(type_Entity, Var_BONDHOLDER)) =>
+(( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(((((f_maturityDate(f_AccountFn(Var_BOND),Var_DATE)) & (((f_possesses(Var_BONDHOLDER,Var_BOND)) & (((f_principalAmount(f_AccountFn(Var_BOND),Var_PRINCIPAL)) & (((f_agreementPeriod(f_AccountFn(Var_BOND),Var_PERIOD)) & (((f_interestEarned(f_AccountFn(Var_BOND),Var_INTEREST,Var_PERIOD)) & (Var_TOTAL = f_AdditionFn(Var_PRINCIPAL,Var_INTEREST)))))))))))) => (( ? [Var_PAYMENT] :
+ (hasType(type_Payment, Var_PAYMENT) &
+(((f_destination(Var_PAYMENT,Var_BONDHOLDER)) & (((f_origin(Var_PAYMENT,f_CurrencyFn(Var_BONDACCOUNT))) & (f_transactionAmount(Var_PAYMENT,Var_TOTAL))))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem91, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_MunicipalBond, Var_BOND) =>
+(( ? [Var_AGENT] :
+ (hasType(type_Government, Var_AGENT) &
+(f_issuedBy(Var_BOND,Var_AGENT)))))))).
+
+fof(axFinancialLem92, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_CorporateBond, Var_BOND) =>
+(( ? [Var_AGENT] :
+ (hasType(type_Corporation, Var_AGENT) &
+(f_issuedBy(Var_BOND,Var_AGENT)))))))).
+
+fof(axFinancialLem93, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_SecuredBond, Var_BOND) =>
+(( ? [Var_SECURITY] :
+ (hasType(type_Collateral, Var_SECURITY) &
+(f_securedBy(Var_BOND,Var_SECURITY)))))))).
+
+fof(axFinancialLem94, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_SecuredBond, Var_BOND) =>
+(( ! [Var_DEFAULT] :
+ (hasType(type_FinancialDefault, Var_DEFAULT) =>
+(( ! [Var_AGENT] :
+ (hasType(type_Agent, Var_AGENT) =>
+(( ! [Var_SECURITY] :
+ ((hasType(type_Collateral, Var_SECURITY) & hasType(type_Object, Var_SECURITY)) =>
+(((((f_securedBy(Var_BOND,Var_SECURITY)) & (((f_possesses(Var_AGENT,Var_BOND)) & (f_patient(Var_DEFAULT,Var_BOND)))))) => (f_holdsDuring(f_ImmediateFutureFn(f_WhenFn(Var_DEFAULT)),possesses(Var_AGENT,Var_SECURITY))))))))))))))))).
+
+fof(axFinancialLem95, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_TreasuryBond, Var_BOND) =>
+(( ? [Var_AGENT] :
+ (hasType(type_Government, Var_AGENT) &
+(f_issuedBy(Var_BOND,Var_AGENT)))))))).
+
+fof(axFinancialLem96, axiom,
+ ( ! [Var_BOND] :
+ (hasType(type_CallableBond, Var_BOND) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_DATE] :
+ ((hasType(type_Day, Var_DATE) & hasType(type_TimePosition, Var_DATE)) =>
+(((((f_currentAccountBalance(f_AccountFn(Var_BOND),Var_DATE,Var_AMOUNT)) & (f_callDate(Var_BOND,Var_DATE)))) => (f_amountDue(f_AccountFn(Var_BOND),Var_AMOUNT,Var_DATE))))))))))))).
+
+fof(axFinancialLem97, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_ConventionalOption, Var_OPTION) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ? [Var_NUMBER] :
+ ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) &
+(((f_agreementPeriod(Var_OPTION,Var_PERIOD)) & (((f_duration(Var_PERIOD,f_MeasureFn(Var_NUMBER,inst_MonthDuration))) & (f_lessThan(Var_NUMBER,9))))))))))))))).
+
+fof(axFinancialLem98, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_ConventionalOption, Var_OPTION) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ? [Var_NUMBER] :
+ ((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) &
+(((f_agreementPeriod(Var_OPTION,Var_PERIOD)) & (((f_duration(Var_PERIOD,f_MeasureFn(Var_NUMBER,inst_MonthDuration))) & (f_lessThan(Var_NUMBER,39))))))))))))))).
+
+fof(axFinancialLem99, axiom,
+ ( ! [Var_DATE] :
+ ((hasType(type_Day, Var_DATE) & hasType(type_TimeInterval, Var_DATE)) =>
+(( ! [Var_CONTRACT] :
+ (hasType(type_Contract, Var_CONTRACT) =>
+(((f_expirationDate(Var_CONTRACT,Var_DATE)) => (( ? [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) &
+(((f_agreementPeriod(Var_CONTRACT,Var_PERIOD)) & (f_finishes(Var_DATE,Var_PERIOD))))))))))))))).
+
+fof(axFinancialLem100, axiom,
+ ( ! [Var_AGENT] :
+ (hasType(type_CognitiveAgent, Var_AGENT) =>
+(( ! [Var_PREMIUM] :
+ (hasType(type_CurrencyMeasure, Var_PREMIUM) =>
+(( ! [Var_OPTION] :
+ ((hasType(type_Option, Var_OPTION) & hasType(type_Investment, Var_OPTION)) =>
+(((((f_premium(Var_OPTION,Var_PREMIUM)) & (f_optionHolder(Var_OPTION,Var_AGENT)))) => (f_potentialLoss(Var_AGENT,Var_OPTION,Var_PREMIUM))))))))))))).
+
+fof(axFinancialLem101, axiom,
+ ( ! [Var_KILL] :
+ (hasType(type_CancellingAnOrder, Var_KILL) =>
+(( ! [Var_ORDER] :
+ ((hasType(type_Entity, Var_ORDER) & hasType(type_Contract, Var_ORDER)) =>
+(((f_patient(Var_KILL,Var_ORDER)) => (( ~ (f_agreementActive(Var_ORDER,f_ImmediateFutureFn(f_WhenFn(Var_KILL)))))))))))))).
+
+fof(axFinancialLem102, axiom,
+ ( ! [Var_ORDER] :
+ (hasType(type_IOCOrder, Var_ORDER) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) => (((( ? [Var_FILL] :
+ (hasType(type_FillingAnOrder, Var_FILL) &
+(( ? [Var_TIME1] :
+ ((hasType(type_Entity, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) &
+(((f_patient(Var_FILL,Var_ORDER)) & (((f_WhenFn(Var_FILL) = Var_TIME1) & (f_starts(Var_TIME1,Var_PERIOD)))))))))))) | (( ? [Var_KILL] :
+ (hasType(type_CancellingAnOrder, Var_KILL) &
+(( ? [Var_TIME2] :
+ ((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2)) &
+(((f_patient(Var_KILL,Var_ORDER)) & (((f_WhenFn(Var_KILL) = Var_TIME2) & (f_starts(Var_TIME2,Var_PERIOD)))))))))))))))))))))).
+
+fof(axFinancialLem103, axiom,
+ ( ! [Var_ORDER] :
+ (hasType(type_FOKOrder, Var_ORDER) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) => (((( ? [Var_FILL] :
+ (hasType(type_FillingAnOrder, Var_FILL) &
+(( ? [Var_TIME1] :
+ ((hasType(type_Entity, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) &
+(((f_patient(Var_FILL,Var_ORDER)) & (((f_WhenFn(Var_FILL) = Var_TIME1) & (f_starts(Var_TIME1,Var_PERIOD)))))))))))) | (( ? [Var_KILL] :
+ (hasType(type_CancellingAnOrder, Var_KILL) &
+(( ? [Var_TIME2] :
+ ((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2)) &
+(((f_patient(Var_KILL,Var_ORDER)) & (((f_WhenFn(Var_KILL) = Var_TIME2) & (f_starts(Var_TIME2,Var_PERIOD)))))))))))))))))))))).
+
+fof(axFinancialLem104, axiom,
+ ( ! [Var_ORDER] :
+ (hasType(type_GTCOrder, Var_ORDER) =>
+(( ! [Var_END] :
+ ((hasType(type_Entity, Var_END) & hasType(type_TimeInterval, Var_END)) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Entity, Var_TIME) & hasType(type_TimeInterval, Var_TIME)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) => (((( ? [Var_EXECUTE] :
+ (hasType(type_FillingAnOrder, Var_EXECUTE) &
+(((f_patient(Var_EXECUTE,Var_ORDER)) & (((f_WhenFn(Var_EXECUTE) = Var_TIME) & (f_overlapsTemporally(Var_TIME,Var_PERIOD))))))))) | (( ? [Var_CANCEL] :
+ (hasType(type_CancellingAnOrder, Var_CANCEL) &
+(((f_patient(Var_CANCEL,Var_ORDER)) & (((f_WhenFn(Var_CANCEL) = Var_END) & (f_finishes(Var_END,Var_PERIOD))))))))))))))))))))))))).
+
+fof(axFinancialLem105, axiom,
+ ( ! [Var_ORDER] :
+ (hasType(type_DayOrder, Var_ORDER) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) & (f_duration(Var_PERIOD,f_MeasureFn(1,inst_DayDuration))))))))))).
+
+fof(axFinancialLem106, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_CallOption, Var_OPTION) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
+(((( ? [Var_STRIKEPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
+(( ? [Var_STOCKPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
+(( ? [Var_STOCK] :
+ ((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
+(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STRIKEPRICE,Var_STOCKPRICE))))))))))))))))) <=> (f_inTheMoney(Var_OPTION,Var_TIME)))))))))).
+
+fof(axFinancialLem107, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_PutOption, Var_OPTION) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
+(((( ? [Var_STRIKEPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
+(( ? [Var_STOCKPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
+(( ? [Var_STOCK] :
+ ((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
+(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STOCKPRICE,Var_STRIKEPRICE))))))))))))))))) <=> (f_inTheMoney(Var_OPTION,Var_TIME)))))))))).
+
+fof(axFinancialLem108, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_Option, Var_OPTION) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
+(((( ? [Var_STRIKEPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Entity, Var_STRIKEPRICE)) &
+(( ? [Var_STOCKPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Entity, Var_STOCKPRICE)) &
+(( ? [Var_STOCK] :
+ ((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
+(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (Var_STOCKPRICE = Var_STRIKEPRICE)))))))))))))))) <=> (f_atTheMoney(Var_OPTION,Var_TIME)))))))))).
+
+fof(axFinancialLem109, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_CallOption, Var_OPTION) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
+(((( ? [Var_STRIKEPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
+(( ? [Var_STOCKPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
+(( ? [Var_STOCK] :
+ ((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
+(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STOCKPRICE,Var_STRIKEPRICE))))))))))))))))) <=> (f_outOfTheMoney(Var_OPTION,Var_TIME)))))))))).
+
+fof(axFinancialLem110, axiom,
+ ( ! [Var_OPTION] :
+ (hasType(type_PutOption, Var_OPTION) =>
+(( ! [Var_TIME] :
+ ((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
+(((( ? [Var_STRIKEPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
+(( ? [Var_STOCKPRICE] :
+ ((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
+(( ? [Var_STOCK] :
+ ((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
+(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STRIKEPRICE,Var_STOCKPRICE))))))))))))))))) <=> (f_outOfTheMoney(Var_OPTION,Var_TIME)))))))))).
+
+fof(axFinancialLem111, axiom,
+ ( ! [Var_SPREAD] :
+ (hasType(type_SpreadOption, Var_SPREAD) =>
+(( ? [Var_OPTION1] :
+ (hasType(type_Option, Var_OPTION1) &
+(( ? [Var_OPTION2] :
+ (hasType(type_Option, Var_OPTION2) &
+(( ? [Var_BUY] :
+ (hasType(type_Buying, Var_BUY) &
+(( ? [Var_SELL] :
+ (hasType(type_Selling, Var_SELL) &
+(( ? [Var_TIME] :
+ (hasType(type_TimePosition, Var_TIME) &
+(((f_patient(Var_BUY,Var_OPTION1)) & (((f_patient(Var_SELL,Var_OPTION2)) & (((f_time(Var_BUY,Var_TIME)) & (f_time(Var_SELL,Var_TIME)))))))))))))))))))))))))).
+
+fof(axFinancialLem112, axiom,
+ ( ! [Var_SPREAD] :
+ (hasType(type_ButterflySpread, Var_SPREAD) =>
+(( ? [Var_CALL1] :
+ (hasType(type_CallOption, Var_CALL1) &
+(( ? [Var_CALL2] :
+ (hasType(type_CallOption, Var_CALL2) &
+(( ? [Var_CALL3] :
+ (hasType(type_CallOption, Var_CALL3) &
+(( ? [Var_CALL4] :
+ (hasType(type_CallOption, Var_CALL4) &
+(( ? [Var_PRICE4] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE4) & hasType(type_Quantity, Var_PRICE4)) &
+(( ? [Var_PRICE3] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE3) & hasType(type_Quantity, Var_PRICE3)) &
+(( ? [Var_PRICE2] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) &
+(( ? [Var_PRICE1] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) &
+(((f_strikePrice(Var_CALL1,Var_PRICE1)) & (((f_strikePrice(Var_CALL2,Var_PRICE2)) & (((f_strikePrice(Var_CALL3,Var_PRICE3)) & (((f_strikePrice(Var_CALL4,Var_PRICE4)) & (((f_lessThan(Var_PRICE1,Var_PRICE2)) & (((f_lessThan(Var_PRICE1,Var_PRICE3)) & (((f_greaterThan(Var_PRICE4,Var_PRICE2)) & (f_greaterThan(Var_PRICE4,Var_PRICE2))))))))))))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem113, axiom,
+ ( ! [Var_TRANSACTION] :
+ (hasType(type_StockMarketTransaction, Var_TRANSACTION) =>
+(( ? [Var_MARKET] :
+ (hasType(type_StockMarket, Var_MARKET) &
+(f_located(Var_TRANSACTION,Var_MARKET)))))))).
+
+fof(axFinancialLem114, axiom,
+ ( ! [Var_UPTICK] :
+ (hasType(type_Uptick, Var_UPTICK) =>
+(( ! [Var_PRICE2] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) =>
+(( ! [Var_PRICE1] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) =>
+(( ! [Var_TIME1] :
+ ((hasType(type_Entity, Var_TIME1) & hasType(type_Agent, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) =>
+(( ! [Var_STOCK] :
+ ((hasType(type_Entity, Var_STOCK) & hasType(type_Physical, Var_STOCK)) =>
+(((((f_patient(Var_UPTICK,Var_STOCK)) & (((f_WhenFn(Var_UPTICK) = Var_TIME1) & (f_price(Var_STOCK,Var_PRICE1,Var_TIME1)))))) => (( ? [Var_TRANSACTION] :
+ (hasType(type_StockMarketTransaction, Var_TRANSACTION) &
+(( ? [Var_TIME2] :
+ ((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2) & hasType(type_Agent, Var_TIME2)) &
+(((f_patient(Var_TRANSACTION,Var_STOCK)) & (((f_WhenFn(Var_TRANSACTION) = Var_TIME2) & (((f_meetsTemporally(Var_TIME2,Var_TIME1)) & (((f_price(Var_STOCK,Var_PRICE2,Var_TIME2)) & (f_lessThan(Var_PRICE2,Var_PRICE1))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem115, axiom,
+ ( ! [Var_DOWNTICK] :
+ (hasType(type_Downtick, Var_DOWNTICK) =>
+(( ! [Var_PRICE2] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) =>
+(( ! [Var_PRICE1] :
+ ((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) =>
+(( ! [Var_TIME1] :
+ ((hasType(type_Entity, Var_TIME1) & hasType(type_Agent, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) =>
+(( ! [Var_STOCK] :
+ ((hasType(type_Entity, Var_STOCK) & hasType(type_Physical, Var_STOCK)) =>
+(((((f_patient(Var_DOWNTICK,Var_STOCK)) & (((f_WhenFn(Var_DOWNTICK) = Var_TIME1) & (f_price(Var_STOCK,Var_PRICE1,Var_TIME1)))))) => (( ? [Var_TRANSACTION] :
+ (hasType(type_StockMarketTransaction, Var_TRANSACTION) &
+(( ? [Var_TIME2] :
+ ((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2) & hasType(type_Agent, Var_TIME2)) &
+(((f_patient(Var_TRANSACTION,Var_STOCK)) & (((f_WhenFn(Var_TRANSACTION) = Var_TIME2) & (((f_meetsTemporally(Var_TIME2,Var_TIME1)) & (((f_price(Var_STOCK,Var_PRICE2,Var_TIME2)) & (f_greaterThan(Var_PRICE2,Var_PRICE1))))))))))))))))))))))))))))))))).
+
+fof(axFinancialLem116, axiom,
+ ( ! [Var_AGENT] :
+ (hasType(type_CognitiveAgent, Var_AGENT) =>
+(( ! [Var_ORG] :
+ ((hasType(type_Organization, Var_ORG) & hasType(type_CognitiveAgent, Var_ORG)) =>
+(((f_employs(Var_ORG,Var_AGENT)) <=> (( ? [Var_EMPLOYMENT] :
+ (hasType(type_Employment, Var_EMPLOYMENT) &
+(((f_agreementMember(Var_EMPLOYMENT,Var_ORG)) & (f_agreementMember(Var_EMPLOYMENT,Var_AGENT))))))))))))))).
+
+fof(axFinancialLem117, axiom,
+ ( ! [Var_MONEY] :
+ (hasType(type_CurrencyMeasure, Var_MONEY) =>
+(( ! [Var_AGENT] :
+ (hasType(type_Human, Var_AGENT) =>
+(((f_monthlyIncome(Var_AGENT,Var_MONEY)) <=> (( ? [Var_MONTH] :
+ (hasType(type_Month, Var_MONTH) &
+(f_income(Var_AGENT,Var_MONEY,Var_MONTH))))))))))))).
+
+fof(axFinancialLem118, axiom,
+ ( ! [Var_ACTIVITY] :
+ ((hasType(type_OrganizationalProcess, Var_ACTIVITY) & hasType(type_Process, Var_ACTIVITY)) =>
+(( ! [Var_MONEY] :
+ (hasType(type_CurrencyMeasure, Var_MONEY) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Human, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
+(((f_incomeEarned(Var_AGENT,Var_MONEY,Var_ACTIVITY)) => (f_agent(Var_ACTIVITY,Var_AGENT))))))))))))).
+
+fof(axFinancialLem119, axiom,
+ ( ! [Var_TIME] :
+ (hasType(type_TimePosition, Var_TIME) =>
+(( ! [Var_ACTIVITY] :
+ ((hasType(type_OrganizationalProcess, Var_ACTIVITY) & hasType(type_Physical, Var_ACTIVITY) & hasType(type_Process, Var_ACTIVITY)) =>
+(( ! [Var_INCOME] :
+ (hasType(type_CurrencyMeasure, Var_INCOME) =>
+(( ! [Var_AGENT] :
+ (hasType(type_Human, Var_AGENT) =>
+(((((f_taxDeferredIncome(Var_AGENT,Var_INCOME,Var_ACTIVITY)) & (f_time(Var_ACTIVITY,Var_TIME)))) => (( ? [Var_TAX] :
+ (hasType(type_Tax, Var_TAX) &
+(((f_causes(Var_ACTIVITY,Var_TAX)) & (f_time(Var_TAX,Var_TIME))))))))))))))))))))).
+
+fof(axFinancialLem120, axiom,
+ ( ! [Var_ATINCOME] :
+ ((hasType(type_Entity, Var_ATINCOME) & hasType(type_OrganizationalProcess, Var_ATINCOME)) =>
+(( ! [Var_ACTIVITY] :
+ ((hasType(type_OrganizationalProcess, Var_ACTIVITY) & hasType(type_Process, Var_ACTIVITY) & hasType(type_CurrencyMeasure, Var_ACTIVITY)) =>
+(( ! [Var_AGENT] :
+ (hasType(type_Human, Var_AGENT) =>
+(((( ? [Var_TAXAMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_TAXAMOUNT) & hasType(type_Quantity, Var_TAXAMOUNT)) &
+(( ? [Var_TAX] :
+ ((hasType(type_ChargingAFee, Var_TAX) & hasType(type_Process, Var_TAX)) &
+(( ? [Var_INCOME] :
+ ((hasType(type_CurrencyMeasure, Var_INCOME) & hasType(type_Quantity, Var_INCOME)) &
+(((f_incomeEarned(Var_AGENT,Var_INCOME,Var_ACTIVITY)) & (((f_amountCharged(Var_TAX,Var_TAXAMOUNT)) & (((f_causes(Var_ACTIVITY,Var_TAX)) & (Var_ATINCOME = f_SubtractionFn(Var_INCOME,Var_TAXAMOUNT))))))))))))))))) <=> (f_afterTaxIncome(Var_AGENT,Var_ACTIVITY,Var_ATINCOME))))))))))))).
+
+fof(axFinancialLem121, axiom,
+ ( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_MONEY] :
+ (hasType(type_CurrencyMeasure, Var_MONEY) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Human, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) =>
+(((f_employeeContribution(Var_AGENT,Var_MONEY,Var_PERIOD)) => (( ? [Var_PLAN] :
+ (hasType(type_PensionPlan, Var_PLAN) &
+(( ? [Var_ORG] :
+ ((hasType(type_Organization, Var_ORG) & hasType(type_Agent, Var_ORG)) &
+(((f_employs(Var_ORG,Var_AGENT)) & (((f_agent(Var_PLAN,Var_ORG)) & (f_destination(Var_PLAN,Var_AGENT))))))))))))))))))))))).
+
+fof(axFinancialLem122, axiom,
+ ( ! [Var_PERIOD] :
+ ((hasType(type_TimePosition, Var_PERIOD) & hasType(type_Entity, Var_PERIOD)) =>
+(( ! [Var_MONEY] :
+ (hasType(type_CurrencyMeasure, Var_MONEY) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Human, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
+(((f_compensationPackage(Var_AGENT,Var_MONEY,Var_PERIOD)) => (( ? [Var_ACTIVITY] :
+ (hasType(type_Working, Var_ACTIVITY) &
+(((f_agent(Var_ACTIVITY,Var_AGENT)) & (((Var_PERIOD = f_WhenFn(Var_ACTIVITY)) & (f_incomeEarned(Var_AGENT,Var_MONEY,Var_ACTIVITY)))))))))))))))))))).
+
+fof(axFinancialLem123, axiom,
+ ( ! [Var_STARTDATE] :
+ ((hasType(type_Day, Var_STARTDATE) & hasType(type_TimeInterval, Var_STARTDATE)) =>
+(( ! [Var_AGREEMENT] :
+ (hasType(type_Contract, Var_AGREEMENT) =>
+(((f_effectiveDate(Var_AGREEMENT,Var_STARTDATE)) <=> (( ? [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) &
+(((f_agreementPeriod(Var_AGREEMENT,Var_PERIOD)) & (f_starts(Var_STARTDATE,Var_PERIOD))))))))))))))).
+
+fof(axFinancialLem124, axiom,
+ ( ! [Var_CASH] :
+ (hasType(type_Cash, Var_CASH) =>
+(( ? [Var_VALUE] :
+ (hasType(type_CurrencyMeasure, Var_VALUE) &
+(f_monetaryValue(Var_CASH,Var_VALUE)))))))).
+
+fof(axFinancialLem125, axiom,
+ ( ! [Var_INVESTMENT] :
+ (hasType(type_Investment, Var_INVESTMENT) =>
+(( ! [Var_LEVEL] :
+ (hasType(type_RiskAttribute, Var_LEVEL) =>
+(( ! [Var_AGENT] :
+ ((hasType(type_Investor, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
+(((((f_riskTolerance(Var_AGENT,Var_LEVEL)) & (f_possesses(Var_AGENT,Var_INVESTMENT)))) => (f_riskLevel(Var_INVESTMENT,Var_LEVEL))))))))))))).
+
+fof(axFinancialLem126, axiom,
+ ( ! [Var_ACCOUNT] :
+ ((hasType(type_FinancialAccount, Var_ACCOUNT) & hasType(type_Entity, Var_ACCOUNT)) =>
+(( ! [Var_CARD] :
+ (hasType(type_BankCard, Var_CARD) =>
+(( ! [Var_CODE] :
+ (hasType(type_ContentBearingObject, Var_CODE) =>
+(((((f_cardCode(Var_CODE,Var_CARD)) & (f_cardAccount(Var_CARD,Var_ACCOUNT)))) => (( ? [Var_ENCODING] :
+ (hasType(type_Encoding, Var_ENCODING) &
+(f_patient(Var_ENCODING,Var_ACCOUNT)))))))))))))))).
+
+fof(axFinancialLem127, axiom,
+ ( ! [Var_CARD] :
+ (hasType(type_DebitCard, Var_CARD) =>
+(( ! [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) =>
+(( ! [Var_AGENT] :
+ (hasType(type_Agent, Var_AGENT) =>
+(((((f_possesses(Var_AGENT,Var_CARD)) & (f_instrument(Var_TRANSACTION,Var_CARD)))) => (( ? [Var_ENTER] :
+ (hasType(type_EnteringAPin, Var_ENTER) &
+(( ? [Var_PIN] :
+ ((hasType(type_SymbolicString, Var_PIN) & hasType(type_Entity, Var_PIN)) &
+(((f_pin(Var_PIN,Var_CARD)) & (((f_patient(Var_ENTER,Var_PIN)) & (f_agent(Var_ENTER,Var_AGENT))))))))))))))))))))))).
+
+fof(axFinancialLem128, axiom,
+ ( ! [Var_ENTER] :
+ (hasType(type_EnteringAPin, Var_ENTER) =>
+(( ? [Var_CARD] :
+ (hasType(type_BankCard, Var_CARD) &
+(( ? [Var_PIN] :
+ ((hasType(type_SymbolicString, Var_PIN) & hasType(type_Entity, Var_PIN)) &
+(((f_pin(Var_PIN,Var_CARD)) & (f_patient(Var_ENTER,Var_PIN))))))))))))).
+
+fof(axFinancialLem129, axiom,
+ ( ! [Var_CHECK] :
+ (hasType(type_VerifyingCardCode, Var_CHECK) =>
+(( ! [Var_CARD] :
+ (hasType(type_BankCard, Var_CARD) =>
+(( ! [Var_CODE] :
+ ((hasType(type_Entity, Var_CODE) & hasType(type_ContentBearingObject, Var_CODE)) =>
+(((((f_patient(Var_CHECK,Var_CODE)) & (f_cardCode(Var_CODE,Var_CARD)))) => (( ? [Var_DECODE] :
+ (hasType(type_Decoding, Var_DECODE) &
+(((f_subProcess(Var_DECODE,Var_CHECK)) & (f_patient(Var_DECODE,Var_CODE)))))))))))))))))).
+
+fof(axFinancialLem130, axiom,
+ ( ! [Var_AGENT2] :
+ ((hasType(type_CognitiveAgent, Var_AGENT2) & hasType(type_Agent, Var_AGENT2)) =>
+(( ! [Var_AGENT1] :
+ ((hasType(type_CognitiveAgent, Var_AGENT1) & hasType(type_Entity, Var_AGENT1)) =>
+(((f_customer(Var_AGENT1,Var_AGENT2)) <=> (( ? [Var_SERVICE] :
+ (hasType(type_FinancialTransaction, Var_SERVICE) &
+(((f_agent(Var_SERVICE,Var_AGENT2)) & (f_destination(Var_SERVICE,Var_AGENT1))))))))))))))).
+
+fof(axFinancialLem131, axiom,
+ ( ! [Var_BANK] :
+ ((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_CognitiveAgent, Var_BANK)) =>
+(( ! [Var_AGENT] :
+ (hasType(type_CognitiveAgent, Var_AGENT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_accountAt(Var_ACCOUNT,Var_BANK)))) => (f_customer(Var_AGENT,Var_BANK))))))))))))).
+
+fof(axFinancialLem132, axiom,
+ ( ! [Var_ORG] :
+ (hasType(type_Organization, Var_ORG) =>
+(( ! [Var_PERSON2] :
+ ((hasType(type_CognitiveAgent, Var_PERSON2) & hasType(type_Entity, Var_PERSON2)) =>
+(( ! [Var_PERSON1] :
+ ((hasType(type_CognitiveAgent, Var_PERSON1) & hasType(type_Agent, Var_PERSON1)) =>
+(((f_customerRepresentative(Var_PERSON1,Var_PERSON2,Var_ORG)) <=> (( ? [Var_SERVICE] :
+ (hasType(type_FinancialTransaction, Var_SERVICE) &
+(((f_employs(Var_ORG,Var_PERSON1)) & (((f_agent(Var_SERVICE,Var_PERSON1)) & (f_destination(Var_SERVICE,Var_PERSON2)))))))))))))))))))).
+
+fof(axFinancialLem133, axiom,
+ ( ! [Var_SLOT] :
+ (hasType(type_ATMSlot, Var_SLOT) =>
+(( ? [Var_ATM] :
+ (hasType(type_ATMMachine, Var_ATM) &
+(f_hole(Var_SLOT,Var_ATM)))))))).
+
+fof(axFinancialLem134, axiom,
+ ( ! [Var_SLOT] :
+ (hasType(type_ATMSlot, Var_SLOT) =>
+(( ? [Var_INSERT] :
+ (hasType(type_Putting, Var_INSERT) &
+(( ? [Var_CARD] :
+ (hasType(type_BankCard, Var_CARD) &
+(((f_patient(Var_INSERT,Var_CARD)) & (f_destination(Var_INSERT,Var_SLOT))))))))))))).
+
+fof(axFinancialLem135, axiom,
+ ( ! [Var_FAX] :
+ (hasType(type_Fax, Var_FAX) =>
+(( ? [Var_FAXMACHINE] :
+ (hasType(type_FaxMachine, Var_FAXMACHINE) &
+(f_instrument(Var_FAX,Var_FAXMACHINE)))))))).
+
+fof(axFinancialLem136, axiom,
+ ( ! [Var_AMOUNT1] :
+ (hasType(type_Quantity, Var_AMOUNT1) =>
+(( ! [Var_DAY] :
+ (hasType(type_Day, Var_DAY) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((( ? [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) &
+(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_TRANSACTION,Var_AMOUNT)) & (f_date(Var_TRANSACTION,Var_DAY))))))))) => (( ? [Var_AMOUNT2] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) &
+(((f_availableBalance(Var_ACCOUNT,Var_DAY,Var_AMOUNT2)) & (f_greaterThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2))))))))))))))))))))).
+
+fof(axFinancialLem137, axiom,
+ ( ! [Var_CASH] :
+ (hasType(type_Cash, Var_CASH) =>
+(( ! [Var_AMOUNT1] :
+ (hasType(type_Quantity, Var_AMOUNT1) =>
+(( ! [Var_DAY] :
+ (hasType(type_Day, Var_DAY) =>
+(( ! [Var_AMOUNT] :
+ (hasType(type_CurrencyMeasure, Var_AMOUNT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((( ? [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) &
+(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_TRANSACTION,Var_AMOUNT)) & (((f_instrument(Var_TRANSACTION,Var_CASH)) & (f_date(Var_TRANSACTION,Var_DAY))))))))))) => (( ? [Var_AMOUNT2] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) &
+(((f_availableCash(Var_ACCOUNT,Var_DAY,Var_AMOUNT2)) & (f_greaterThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2)))))))))))))))))))))))).
+
+fof(axFinancialLem138, axiom,
+ ( ! [Var_STATEMENT] :
+ (hasType(type_BankStatement, Var_STATEMENT) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((f_statementAccount(Var_STATEMENT,Var_ACCOUNT)) => (( ? [Var_TRANSACTION] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION) &
+(((((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) | (f_destination(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))))) & (f_realization(Var_STATEMENT,Var_TRANSACTION))))))))))))))).
+
+fof(axFinancialLem139, axiom,
+ ( ! [Var_TRANSACTION1] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION1) =>
+(( ! [Var_TRANSACTION2] :
+ (hasType(type_FinancialTransaction, Var_TRANSACTION2) =>
+(( ! [Var_STATEMENT] :
+ ((hasType(type_BankStatement, Var_STATEMENT) & hasType(type_Process, Var_STATEMENT)) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((((f_lastStatement(Var_ACCOUNT,Var_STATEMENT)) & (((( ~ (f_realization(Var_STATEMENT,Var_TRANSACTION1)))) & (f_realization(Var_STATEMENT,Var_TRANSACTION2)))))) => (f_earlier(f_WhenFn(Var_TRANSACTION2),f_WhenFn(Var_TRANSACTION1))))))))))))))))).
+
+fof(axFinancialLem140, axiom,
+ ( ! [Var_LOAN] :
+ (hasType(type_Loan, Var_LOAN) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_Interest, Var_AMOUNT) & hasType(type_CurrencyMeasure, Var_AMOUNT)) =>
+(((( ? [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) &
+(((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_interestEarned(Var_LOAN,Var_AMOUNT,Var_PERIOD))))))) <=> (f_loanInterest(Var_LOAN,Var_AMOUNT)))))))))).
+
+fof(axFinancialLem141, axiom,
+ ( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(( ! [Var_STATEMENT] :
+ ((hasType(type_BankStatement, Var_STATEMENT) & hasType(type_Proposition, Var_STATEMENT)) =>
+(((f_dateOfStatement(Var_STATEMENT,Var_DATE)) => (( ? [Var_COPY] :
+ ((hasType(type_ContentBearingPhysical, Var_COPY) & hasType(type_Physical, Var_COPY)) &
+(((f_containsInformation(Var_COPY,Var_STATEMENT)) & (f_date(Var_COPY,Var_DATE))))))))))))))).
+
+fof(axFinancialLem142, axiom,
+ ( ! [Var_DATE] :
+ (hasType(type_Day, Var_DATE) =>
+(( ! [Var_BALANCE] :
+ (hasType(type_CurrencyMeasure, Var_BALANCE) =>
+(( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(((f_lastStatementBalance(Var_ACCOUNT,Var_BALANCE)) => (( ? [Var_STATEMENT] :
+ (hasType(type_BankStatement, Var_STATEMENT) &
+(((f_lastStatement(Var_ACCOUNT,Var_STATEMENT)) & (((f_dateOfStatement(Var_STATEMENT,Var_DATE)) & (f_currentAccountBalance(Var_ACCOUNT,Var_DATE,Var_ACCOUNT)))))))))))))))))))).
+
+fof(axFinancialLem143, axiom,
+ ( ! [Var_DURATION] :
+ ((hasType(type_TimeDuration, Var_DURATION) & hasType(type_Entity, Var_DURATION)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_STATEMENT] :
+ (hasType(type_BankStatement, Var_STATEMENT) =>
+(((((f_statementPeriod(Var_STATEMENT,Var_PERIOD)) & (f_duration(Var_PERIOD,Var_DURATION)))) => (Var_DURATION = inst_MonthDuration)))))))))))).
+
+fof(axFinancialLem144, axiom,
+ ( ! [Var_DATE] :
+ ((hasType(type_Day, Var_DATE) & hasType(type_TimeInterval, Var_DATE)) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_STATEMENT] :
+ (hasType(type_BankStatement, Var_STATEMENT) =>
+(((((f_statementPeriod(Var_STATEMENT,Var_PERIOD)) & (f_dateOfStatement(Var_STATEMENT,Var_DATE)))) => (f_finishes(Var_DATE,Var_PERIOD))))))))))))).
+
+fof(axFinancialLem145, axiom,
+ ( ! [Var_ACCOUNT] :
+ (hasType(type_FinancialAccount, Var_ACCOUNT) =>
+(( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_INTEREST] :
+ (hasType(type_CurrencyMeasure, Var_INTEREST) =>
+(( ! [Var_STATEMENT] :
+ (hasType(type_BankStatement, Var_STATEMENT) =>
+(((((f_statementInterest(Var_STATEMENT,Var_INTEREST)) & (((f_statementPeriod(Var_STATEMENT,Var_PERIOD)) & (f_statementAccount(Var_STATEMENT,Var_ACCOUNT)))))) => (( ? [Var_AMOUNT] :
+ (hasType(type_Interest, Var_AMOUNT) &
+(f_interestEarned(Var_ACCOUNT,Var_AMOUNT,Var_PERIOD))))))))))))))))))).
+
+fof(axFinancialLem146, axiom,
+ ( ! [Var_TRANSFER] :
+ (hasType(type_ExternalTransfer, Var_TRANSFER) =>
+(( ! [Var_ORGANIZATION1] :
+ (hasType(type_FinancialOrganization, Var_ORGANIZATION1) =>
+(( ! [Var_ORGANIZATION2] :
+ (hasType(type_FinancialOrganization, Var_ORGANIZATION2) =>
+(((((f_origin(Var_TRANSFER,Var_ORGANIZATION1)) & (f_destination(Var_TRANSFER,Var_ORGANIZATION2)))) => (Var_ORGANIZATION1 != Var_ORGANIZATION2)))))))))))).
+
+fof(axFinancialLem147, axiom,
+ ( ! [Var_TRANSFER] :
+ (hasType(type_ExternalTransfer, Var_TRANSFER) =>
+(( ! [Var_ORGANIZATION1] :
+ (hasType(type_FinancialOrganization, Var_ORGANIZATION1) =>
+(( ! [Var_ORGANIZATION2] :
+ (hasType(type_FinancialOrganization, Var_ORGANIZATION2) =>
+(( ! [Var_ORGANIZATION2] :
+ (hasType(type_Entity, Var_ORGANIZATION2) =>
+(((((f_origin(Var_TRANSFER,Var_ORGANIZATION1)) & (f_destination(Var_TRANSFER,Var_ORGANIZATION2)))) => (Var_ORGANIZATION1 = Var_ORGANIZATION2))))))))))))))).
+
+fof(axFinancialLem148, axiom,
+ ( ! [Var_PERIOD] :
+ (hasType(type_TimeInterval, Var_PERIOD) =>
+(( ! [Var_AMOUNT] :
+ ((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Interest, Var_AMOUNT)) =>
+(( ! [Var_LOAN] :
+ ((hasType(type_Loan, Var_LOAN) & hasType(type_Contract, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
+(((((f_loanFeeAmount(Var_LOAN,Var_AMOUNT)) & (f_agreementPeriod(Var_LOAN,Var_PERIOD)))) => (f_interestEarned(Var_LOAN,Var_AMOUNT,Var_PERIOD))))))))))))).
+
|