; GraphAtlas proof IC-06
; Statement: For any capital resources and any requirement, what counts and what is left out add up to what is held, for a group that is not mutual and for a mutual. For a group that is not mutual, Tier 1 Limited counts up to 15 per cent of the requirement, Tier 2 up to 50 per cent and the basket up to 15 per cent, and none of the Non-Paid-Up capital counts. For a mutual, Tier 1 Limited counts up to 30 per cent, Non-Paid-Up up to 10 per cent, and Tier 1 Limited and Tier 2 together up to 60 per cent. What Tier 1 Limited has over its limit moves to Tier 2. What is left out is not below zero and what counts is not above what is held.
; About: qualifyingResources in src/kernel/ics.ts, with LIMIT_TEXT and BASKET_SHARE_TEXT as exact decimals. The basket enters as the sum of its three items at their shares, which are 50, 100 and 10 per cent. The group that is not mutual counts the smaller of Tier 1 Limited, 10 per cent of the requirement and what has a loss absorbency mechanism, and 15 per cent of the requirement. The mutual counts the smaller of Tier 1 Limited and 30 per cent, and its combined limit is 60 per cent less the Tier 1 Limited that counts. The excess of Tier 1 Limited, the basket that counts, the Non-Paid-Up that counts and Tier 2 make the pool that the Tier 2 limit applies to.
; Source: IAIS Insurance Capital Standard, Level 2 text of 5 December 2024, L2-122, L2-127 and L2-129
; Expected: unsat for each of the 20 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun requirement () Real)
(declare-fun tier_1_unlimited () Real)
(declare-fun tier_1_limited () Real)
(declare-fun tier_1_limited_with_mechanism () Real)
(declare-fun tier_2 () Real)
(declare-fun non_paid_up () Real)
(declare-fun pension_fund_asset () Real)
(declare-fun deferred_tax_asset_item () Real)
(declare-fun software_intangibles () Real)
(assert (>= requirement 0.0))
(assert (>= tier_1_unlimited 0.0))
(assert (>= tier_1_limited 0.0))
(assert (>= tier_1_limited_with_mechanism 0.0))
(assert (<= tier_1_limited_with_mechanism tier_1_limited))
(assert (>= tier_2 0.0))
(assert (>= non_paid_up 0.0))
(assert (>= pension_fund_asset 0.0))
(assert (>= deferred_tax_asset_item 0.0))
(assert (>= software_intangibles 0.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism))) (a!3 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement))) (a!4 (ite (<= a!3 (* (/ 3.0 20.0) requirement)) a!3 (* (/ 3.0 20.0) requirement)))) (let ((a!5 (ite (<= (+ tier_2 a!4 0.0 (- tier_1_limited a!2)) (* (/ 1.0 2.0) requirement)) (+ tier_2 a!4 0.0 (- tier_1_limited a!2)) (* (/ 1.0 2.0) requirement)))) (let ((a!6 (+ tier_1_unlimited a!2 a!5 (- a!3 a!4) (- non_paid_up 0.0) (- (+ tier_2 a!4 0.0 (- tier_1_limited a!2)) a!5)))) (= a!6 (+ tier_1_unlimited tier_1_limited tier_2 non_paid_up a!3))))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (* (/ 3.0 10.0) requirement)) tier_1_limited (* (/ 3.0 10.0) requirement))) (a!2 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles))) (a!4 (ite (<= non_paid_up (* (/ 1.0 10.0) requirement)) non_paid_up (* (/ 1.0 10.0) requirement)))) (let ((a!3 (ite (<= a!2 (* (/ 3.0 20.0) requirement)) a!2 (* (/ 3.0 20.0) requirement)))) (let ((a!5 (ite (<= (+ tier_2 a!3 a!4 (- tier_1_limited a!1)) (- (* (/ 3.0 5.0) requirement) a!1)) (+ tier_2 a!3 a!4 (- tier_1_limited a!1)) (- (* (/ 3.0 5.0) requirement) a!1)))) (let ((a!6 (+ tier_1_unlimited a!1 a!5 (- a!2 a!3) (- non_paid_up a!4) (- (+ tier_2 a!3 a!4 (- tier_1_limited a!1)) a!5)))) (= a!6 (+ tier_1_unlimited tier_1_limited tier_2 non_paid_up a!2))))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)))) (<= (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)) (* (/ 3.0 20.0) requirement)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles))) (a!2 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)))) (let ((a!3 (- tier_1_limited (ite (<= a!2 (* (/ 3.0 20.0) requirement)) a!2 (* (/ 3.0 20.0) requirement))))) (let ((a!4 (+ tier_2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)) 0.0 a!3))) (<= (ite (<= a!4 (* (/ 1.0 2.0) requirement)) a!4 (* (/ 1.0 2.0) requirement)) (* (/ 1.0 2.0) requirement)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (<= (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)) (* (/ 3.0 20.0) requirement)))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (<= (ite (<= tier_1_limited (* (/ 3.0 10.0) requirement)) tier_1_limited (* (/ 3.0 10.0) requirement)) (* (/ 3.0 10.0) requirement))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (<= (ite (<= non_paid_up (* (/ 1.0 10.0) requirement)) non_paid_up (* (/ 1.0 10.0) requirement)) (* (/ 1.0 10.0) requirement))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (* (/ 3.0 10.0) requirement)) tier_1_limited (* (/ 3.0 10.0) requirement))) (a!2 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!3 (+ tier_2 (ite (<= a!2 (* (/ 3.0 20.0) requirement)) a!2 (* (/ 3.0 20.0) requirement)) (ite (<= non_paid_up (* (/ 1.0 10.0) requirement)) non_paid_up (* (/ 1.0 10.0) requirement)) (- tier_1_limited a!1)))) (let ((a!4 (ite (<= a!3 (- (* (/ 3.0 5.0) requirement) a!1)) a!3 (- (* (/ 3.0 5.0) requirement) a!1)))) (<= (+ a!1 a!4) (* (/ 3.0 5.0) requirement)))))))
(check-sat)
(pop 1)

; Goal 9, negated
(push 1)
(assert (not (let ((a!1 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles))) (a!3 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement))) (a!4 (- tier_1_limited (ite (<= a!3 (* (/ 3.0 20.0) requirement)) a!3 (* (/ 3.0 20.0) requirement))))) (let ((a!5 (- (+ tier_2 a!2 0.0 a!4) (ite (<= (+ tier_2 a!2 0.0 a!4) (* (/ 1.0 2.0) requirement)) (+ tier_2 a!2 0.0 a!4) (* (/ 1.0 2.0) requirement))))) (>= (+ (- a!1 a!2) (- non_paid_up 0.0) a!5) non_paid_up))))))
(check-sat)
(pop 1)

; Goal 10, negated
(push 1)
(assert (not (let ((a!1 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles))) (a!3 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement))) (a!4 (- tier_1_limited (ite (<= a!3 (* (/ 3.0 20.0) requirement)) a!3 (* (/ 3.0 20.0) requirement))))) (let ((a!5 (- (+ tier_2 a!2 0.0 a!4) (ite (<= (+ tier_2 a!2 0.0 a!4) (* (/ 1.0 2.0) requirement)) (+ tier_2 a!2 0.0 a!4) (* (/ 1.0 2.0) requirement))))) (>= (+ (- a!1 a!2) (- non_paid_up 0.0) a!5) 0.0))))))
(check-sat)
(pop 1)

; Goal 11, negated
(push 1)
(assert (not (let ((a!1 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles))) (a!3 (ite (<= non_paid_up (* (/ 1.0 10.0) requirement)) non_paid_up (* (/ 1.0 10.0) requirement))) (a!4 (ite (<= tier_1_limited (* (/ 3.0 10.0) requirement)) tier_1_limited (* (/ 3.0 10.0) requirement)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)))) (let ((a!5 (ite (<= (+ tier_2 a!2 a!3 (- tier_1_limited a!4)) (- (* (/ 3.0 5.0) requirement) a!4)) (+ tier_2 a!2 a!3 (- tier_1_limited a!4)) (- (* (/ 3.0 5.0) requirement) a!4)))) (let ((a!6 (+ (- a!1 a!2) (- non_paid_up a!3) (- (+ tier_2 a!2 a!3 (- tier_1_limited a!4)) a!5)))) (>= a!6 0.0)))))))
(check-sat)
(pop 1)

; Goal 12, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism))) (a!3 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)))) (let ((a!4 (+ tier_2 (ite (<= a!3 (* (/ 3.0 20.0) requirement)) a!3 (* (/ 3.0 20.0) requirement)) 0.0 (- tier_1_limited a!2)))) (let ((a!5 (+ tier_1_unlimited a!2 (ite (<= a!4 (* (/ 1.0 2.0) requirement)) a!4 (* (/ 1.0 2.0) requirement))))) (<= a!5 (+ tier_1_unlimited tier_1_limited tier_2 non_paid_up a!3))))))))
(check-sat)
(pop 1)

; Goal 13, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (* (/ 3.0 10.0) requirement)) tier_1_limited (* (/ 3.0 10.0) requirement))) (a!2 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!3 (+ tier_2 (ite (<= a!2 (* (/ 3.0 20.0) requirement)) a!2 (* (/ 3.0 20.0) requirement)) (ite (<= non_paid_up (* (/ 1.0 10.0) requirement)) non_paid_up (* (/ 1.0 10.0) requirement)) (- tier_1_limited a!1)))) (let ((a!4 (ite (<= a!3 (- (* (/ 3.0 5.0) requirement) a!1)) a!3 (- (* (/ 3.0 5.0) requirement) a!1)))) (<= (+ tier_1_unlimited a!1 a!4) (+ tier_1_unlimited tier_1_limited tier_2 non_paid_up a!2)))))))
(check-sat)
(pop 1)

; Goal 14, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)))) (>= (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)) (ite (<= tier_1_limited (* (/ 1.0 10.0) requirement)) tier_1_limited (* (/ 1.0 10.0) requirement))))))
(check-sat)
(pop 1)

; Goal 15, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism))) (a!3 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement)))) (let ((a!4 (+ tier_2 (ite (<= a!3 (* (/ 3.0 20.0) requirement)) a!3 (* (/ 3.0 20.0) requirement)) 0.0 (- tier_1_limited a!2)))) (let ((a!5 (+ tier_1_unlimited a!2 (ite (<= a!4 (* (/ 1.0 2.0) requirement)) a!4 (* (/ 1.0 2.0) requirement))))) (>= a!5 tier_1_unlimited)))))))
(check-sat)
(pop 1)

; Goal 16, negated
(push 1)
(assert (not (=> (and (= deferred_tax_asset_item (to_real 0)) (= software_intangibles (to_real 0))) (= (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)) (* pension_fund_asset (/ 1.0 2.0))))))
(check-sat)
(pop 1)

; Goal 17, negated
(push 1)
(assert (not (=> (and (= pension_fund_asset (to_real 0)) (= software_intangibles (to_real 0))) (= (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)) deferred_tax_asset_item))))
(check-sat)
(pop 1)

; Goal 18, negated
(push 1)
(assert (not (=> (and (= pension_fund_asset (to_real 0)) (= deferred_tax_asset_item (to_real 0))) (= (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)) (* software_intangibles (/ 1.0 10.0))))))
(check-sat)
(pop 1)

; Goal 19, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism)) tier_1_limited (+ (* (/ 1.0 10.0) requirement) tier_1_limited_with_mechanism))) (a!3 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!2 (ite (<= a!1 (* (/ 3.0 20.0) requirement)) a!1 (* (/ 3.0 20.0) requirement))) (a!4 (+ tier_2 (ite (<= a!3 (* (/ 3.0 20.0) requirement)) a!3 (* (/ 3.0 20.0) requirement))))) (let ((a!5 (ite (<= (+ a!4 0.0 (- tier_1_limited a!2)) (* (/ 1.0 2.0) requirement)) (+ a!4 0.0 (- tier_1_limited a!2)) (* (/ 1.0 2.0) requirement))) (a!6 (+ (+ tier_1_unlimited a!2) (ite (<= a!4 (* (/ 1.0 2.0) requirement)) a!4 (* (/ 1.0 2.0) requirement))))) (>= (+ (+ tier_1_unlimited a!2) a!5) a!6))))))
(check-sat)
(pop 1)

; Goal 20, negated
(push 1)
(assert (not (let ((a!1 (ite (<= tier_1_limited (* (/ 3.0 10.0) requirement)) tier_1_limited (* (/ 3.0 10.0) requirement))) (a!2 (+ (* (/ 1.0 2.0) pension_fund_asset) (* 1.0 deferred_tax_asset_item) (* (/ 1.0 10.0) software_intangibles)))) (let ((a!3 (+ tier_2 (ite (<= a!2 (* (/ 3.0 20.0) requirement)) a!2 (* (/ 3.0 20.0) requirement)) (ite (<= non_paid_up (* (/ 1.0 10.0) requirement)) non_paid_up (* (/ 1.0 10.0) requirement)) (- tier_1_limited a!1)))) (let ((a!4 (ite (<= a!3 (- (* (/ 3.0 5.0) requirement) a!1)) a!3 (- (* (/ 3.0 5.0) requirement) a!1)))) (>= (+ (+ tier_1_unlimited a!1) a!4) (+ tier_1_unlimited a!1)))))))
(check-sat)
(pop 1)