; GraphAtlas proof SI-01
; Statement: For any non-negative module charges, the basic SCR is never above the plain sum of the charges and never below the largest single charge.
; About: The quadratic form behind aggregate in src/kernel/aggregate.ts with the matrix in BSCR_CORRELATION_TEXT, taken as exact decimals. The solver proves the form lies between the square of the largest charge and the square of the sum. The SCR is its square root, which is increasing.
; Source: Directive 2009/138/EC, Article 104(1) and Annex IV, point 1
; Expected: unsat for each of the 6 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun scr_market () Real)
(declare-fun scr_default () Real)
(declare-fun scr_life () Real)
(declare-fun scr_health () Real)
(declare-fun scr_nonlife () Real)
(assert (>= scr_market 0.0))
(assert (>= scr_default 0.0))
(assert (>= scr_life 0.0))
(assert (>= scr_health 0.0))
(assert (>= scr_nonlife 0.0))

; Goal 1, negated
(push 1)
(assert (not (<= (+ 0.0 (* 1.0 scr_market scr_market) (* (* (/ 1.0 4.0) scr_market) scr_default) (* (* (/ 1.0 4.0) scr_market) scr_life) (* (* (/ 1.0 4.0) scr_market) scr_health) (* (* (/ 1.0 4.0) scr_market) scr_nonlife) (* (* (/ 1.0 4.0) scr_default) scr_market) (* 1.0 scr_default scr_default) (* (* (/ 1.0 4.0) scr_default) scr_life) (* (* (/ 1.0 4.0) scr_default) scr_health) (* (/ 1.0 2.0) scr_default scr_nonlife) (* (* (/ 1.0 4.0) scr_life) scr_market) (* (* (/ 1.0 4.0) scr_life) scr_default) (* 1.0 scr_life scr_life) (* (* (/ 1.0 4.0) scr_life) scr_health) (* 0.0 scr_life scr_nonlife) (* (* (/ 1.0 4.0) scr_health) scr_market) (* (* (/ 1.0 4.0) scr_health) scr_default) (* (* (/ 1.0 4.0) scr_health) scr_life) (* 1.0 scr_health scr_health) (* 0.0 scr_health scr_nonlife) (* (/ 1.0 4.0) scr_nonlife scr_market) (* (/ 1.0 2.0) scr_nonlife scr_default) (* (* 0.0 scr_nonlife) scr_life) (* (* 0.0 scr_nonlife) scr_health) (* 1.0 scr_nonlife scr_nonlife)) (* (+ 0.0 scr_market scr_default scr_life scr_health scr_nonlife) (+ 0.0 scr_market scr_default scr_life scr_health scr_nonlife)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (>= (+ 0.0 (* 1.0 scr_market scr_market) (* (* (/ 1.0 4.0) scr_market) scr_default) (* (* (/ 1.0 4.0) scr_market) scr_life) (* (* (/ 1.0 4.0) scr_market) scr_health) (* (* (/ 1.0 4.0) scr_market) scr_nonlife) (* (* (/ 1.0 4.0) scr_default) scr_market) (* 1.0 scr_default scr_default) (* (* (/ 1.0 4.0) scr_default) scr_life) (* (* (/ 1.0 4.0) scr_default) scr_health) (* (/ 1.0 2.0) scr_default scr_nonlife) (* (* (/ 1.0 4.0) scr_life) scr_market) (* (* (/ 1.0 4.0) scr_life) scr_default) (* 1.0 scr_life scr_life) (* (* (/ 1.0 4.0) scr_life) scr_health) (* 0.0 scr_life scr_nonlife) (* (* (/ 1.0 4.0) scr_health) scr_market) (* (* (/ 1.0 4.0) scr_health) scr_default) (* (* (/ 1.0 4.0) scr_health) scr_life) (* 1.0 scr_health scr_health) (* 0.0 scr_health scr_nonlife) (* (/ 1.0 4.0) scr_nonlife scr_market) (* (/ 1.0 2.0) scr_nonlife scr_default) (* (* 0.0 scr_nonlife) scr_life) (* (* 0.0 scr_nonlife) scr_health) (* 1.0 scr_nonlife scr_nonlife)) (* scr_market scr_market))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (>= (+ 0.0 (* 1.0 scr_market scr_market) (* (* (/ 1.0 4.0) scr_market) scr_default) (* (* (/ 1.0 4.0) scr_market) scr_life) (* (* (/ 1.0 4.0) scr_market) scr_health) (* (* (/ 1.0 4.0) scr_market) scr_nonlife) (* (* (/ 1.0 4.0) scr_default) scr_market) (* 1.0 scr_default scr_default) (* (* (/ 1.0 4.0) scr_default) scr_life) (* (* (/ 1.0 4.0) scr_default) scr_health) (* (/ 1.0 2.0) scr_default scr_nonlife) (* (* (/ 1.0 4.0) scr_life) scr_market) (* (* (/ 1.0 4.0) scr_life) scr_default) (* 1.0 scr_life scr_life) (* (* (/ 1.0 4.0) scr_life) scr_health) (* 0.0 scr_life scr_nonlife) (* (* (/ 1.0 4.0) scr_health) scr_market) (* (* (/ 1.0 4.0) scr_health) scr_default) (* (* (/ 1.0 4.0) scr_health) scr_life) (* 1.0 scr_health scr_health) (* 0.0 scr_health scr_nonlife) (* (/ 1.0 4.0) scr_nonlife scr_market) (* (/ 1.0 2.0) scr_nonlife scr_default) (* (* 0.0 scr_nonlife) scr_life) (* (* 0.0 scr_nonlife) scr_health) (* 1.0 scr_nonlife scr_nonlife)) (* scr_default scr_default))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (>= (+ 0.0 (* 1.0 scr_market scr_market) (* (* (/ 1.0 4.0) scr_market) scr_default) (* (* (/ 1.0 4.0) scr_market) scr_life) (* (* (/ 1.0 4.0) scr_market) scr_health) (* (* (/ 1.0 4.0) scr_market) scr_nonlife) (* (* (/ 1.0 4.0) scr_default) scr_market) (* 1.0 scr_default scr_default) (* (* (/ 1.0 4.0) scr_default) scr_life) (* (* (/ 1.0 4.0) scr_default) scr_health) (* (/ 1.0 2.0) scr_default scr_nonlife) (* (* (/ 1.0 4.0) scr_life) scr_market) (* (* (/ 1.0 4.0) scr_life) scr_default) (* 1.0 scr_life scr_life) (* (* (/ 1.0 4.0) scr_life) scr_health) (* 0.0 scr_life scr_nonlife) (* (* (/ 1.0 4.0) scr_health) scr_market) (* (* (/ 1.0 4.0) scr_health) scr_default) (* (* (/ 1.0 4.0) scr_health) scr_life) (* 1.0 scr_health scr_health) (* 0.0 scr_health scr_nonlife) (* (/ 1.0 4.0) scr_nonlife scr_market) (* (/ 1.0 2.0) scr_nonlife scr_default) (* (* 0.0 scr_nonlife) scr_life) (* (* 0.0 scr_nonlife) scr_health) (* 1.0 scr_nonlife scr_nonlife)) (* scr_life scr_life))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (>= (+ 0.0 (* 1.0 scr_market scr_market) (* (* (/ 1.0 4.0) scr_market) scr_default) (* (* (/ 1.0 4.0) scr_market) scr_life) (* (* (/ 1.0 4.0) scr_market) scr_health) (* (* (/ 1.0 4.0) scr_market) scr_nonlife) (* (* (/ 1.0 4.0) scr_default) scr_market) (* 1.0 scr_default scr_default) (* (* (/ 1.0 4.0) scr_default) scr_life) (* (* (/ 1.0 4.0) scr_default) scr_health) (* (/ 1.0 2.0) scr_default scr_nonlife) (* (* (/ 1.0 4.0) scr_life) scr_market) (* (* (/ 1.0 4.0) scr_life) scr_default) (* 1.0 scr_life scr_life) (* (* (/ 1.0 4.0) scr_life) scr_health) (* 0.0 scr_life scr_nonlife) (* (* (/ 1.0 4.0) scr_health) scr_market) (* (* (/ 1.0 4.0) scr_health) scr_default) (* (* (/ 1.0 4.0) scr_health) scr_life) (* 1.0 scr_health scr_health) (* 0.0 scr_health scr_nonlife) (* (/ 1.0 4.0) scr_nonlife scr_market) (* (/ 1.0 2.0) scr_nonlife scr_default) (* (* 0.0 scr_nonlife) scr_life) (* (* 0.0 scr_nonlife) scr_health) (* 1.0 scr_nonlife scr_nonlife)) (* scr_health scr_health))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (>= (+ 0.0 (* 1.0 scr_market scr_market) (* (* (/ 1.0 4.0) scr_market) scr_default) (* (* (/ 1.0 4.0) scr_market) scr_life) (* (* (/ 1.0 4.0) scr_market) scr_health) (* (* (/ 1.0 4.0) scr_market) scr_nonlife) (* (* (/ 1.0 4.0) scr_default) scr_market) (* 1.0 scr_default scr_default) (* (* (/ 1.0 4.0) scr_default) scr_life) (* (* (/ 1.0 4.0) scr_default) scr_health) (* (/ 1.0 2.0) scr_default scr_nonlife) (* (* (/ 1.0 4.0) scr_life) scr_market) (* (* (/ 1.0 4.0) scr_life) scr_default) (* 1.0 scr_life scr_life) (* (* (/ 1.0 4.0) scr_life) scr_health) (* 0.0 scr_life scr_nonlife) (* (* (/ 1.0 4.0) scr_health) scr_market) (* (* (/ 1.0 4.0) scr_health) scr_default) (* (* (/ 1.0 4.0) scr_health) scr_life) (* 1.0 scr_health scr_health) (* 0.0 scr_health scr_nonlife) (* (/ 1.0 4.0) scr_nonlife scr_market) (* (/ 1.0 2.0) scr_nonlife scr_default) (* (* 0.0 scr_nonlife) scr_life) (* (* 0.0 scr_nonlife) scr_health) (* 1.0 scr_nonlife scr_nonlife)) (* scr_nonlife scr_nonlife))))
(check-sat)
(pop 1)