; Dalil al-imkan: independent cross-check in Z3 of proof (a) (the aggregate
; route) and proof (b) (the short route through OP-001).
; "y gives existence to x, directly or through intermediaries" needs induction,
; which Z3 cannot express; it is represented by a relation UG that contains
; giving and is transitive, and the PROVED result of PR-003 (no circle of
; giving) is supplied as "nothing UG-gives to itself".  This is sound for
; unsat: any real counterexample extends to one here (take UG = the real
; chains of giving).  Z3 assumes non-empty domains; SP-001 supplies existence
; explicitly.  No time appears.

(declare-sort Thing 0)
(declare-fun Ex (Thing) Bool)            ; x exists
(declare-fun Ess (Thing) Bool)           ; x's existence is from its nature
(declare-fun Gives (Thing Thing) Bool)   ; (Gives y x): y gives existence to x
(declare-fun Mem (Thing Thing) Bool)     ; (Mem p A): p is a member of collection A
(declare-fun UG (Thing Thing) Bool)      ; y gives existence to x, directly or through intermediaries

(define-fun Nec ((x Thing)) Bool (and (Ex x) (Ess x)))
(define-fun Poss ((x Thing)) Bool (and (Ex x) (not (Ess x))))
(define-fun TA ((x Thing)) Bool (exists ((y Thing)) (Gives y x)))
(define-fun Agg ((A Thing)) Bool
  (and (forall ((p Thing)) (=> (not (= p A)) (= (Mem p A) (Poss p)))) (not (Mem A A))))

(define-fun UGdef () Bool (and (forall ((y Thing) (x Thing)) (=> (Gives y x) (UG y x)))
                               (forall ((x Thing) (y Thing) (z Thing)) (=> (and (UG x y) (UG y z)) (UG x z)))))
(define-fun PR003 () Bool (forall ((x Thing)) (not (UG x x))))                       ; proved: no circle of giving
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))
(define-fun MP009 () Bool (=> (exists ((p Thing)) (Poss p)) (exists ((A Thing)) (and (Agg A) (Ex A)))))
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Mem p A))
                                                      (forall ((p Thing)) (=> (Mem p A) (not (Ess p)))))
                                                 (not (Ess A)))))
(define-fun MP011 () Bool (forall ((c Thing) (A Thing) (p Thing)) (=> (and (Gives c A) (Mem p A)) (UG c p))))
(define-fun MP012 () Bool (forall ((y Thing) (x Thing)) (=> (Gives y x) (Ex y))))
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (and (Ex y) (not (TA y))))))
(define-fun SP001 () Bool (exists ((x Thing)) (Ex x)))
(define-fun Conclusion () Bool (exists ((n Thing)) (Nec n)))

(echo "check 1: proof (a): premises + SP-001 + conclusion denied (expect unsat)")
(push) (assert UGdef) (assert PR003) (assert MP008) (assert MP009) (assert MP010) (assert MP011) (assert MP012)
  (assert SP001) (assert (not Conclusion)) (check-sat) (pop)
(echo "check 2: proof (a): premises + SP-001 together (expect sat: consistent)")
(push) (assert UGdef) (assert PR003) (assert MP008) (assert MP009) (assert MP010) (assert MP011) (assert MP012)
  (assert SP001) (check-sat) (pop)
(echo "check 3: proof (a) without SP-001, conclusion denied (expect sat: SP-001 is needed)")
(push) (assert UGdef) (assert PR003) (assert MP008) (assert MP009) (assert MP010) (assert MP011) (assert MP012)
  (assert (not Conclusion)) (check-sat) (pop)
(echo "check 4: proof (b): MP-008 + OP-001 + SP-001 + conclusion denied (expect unsat)")
(push) (assert MP008) (assert OP001) (assert SP001) (assert (not Conclusion)) (check-sat) (pop)
(echo "check 5: proof (b) without OP-001, conclusion denied (expect sat: OP-001 is needed)")
(push) (assert MP008) (assert SP001) (assert (not Conclusion)) (check-sat) (pop)