; Dalil al-kalima, the conclusion: independent cross-check in Z3.
; Z3 assumes a non-empty domain.  Here the universe u is named explicitly,
; so that assumption does no work.  No time appears.

(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)    ; (Gives y x): y gives existence to x
(declare-fun Through (Thing Thing) Bool)  ; (Through x y): x has its existence through y
(declare-fun Exists (Thing) Bool)         ; (Exists x): x exists
(declare-const u Thing)                   ; the universe

(define-fun MP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool (forall ((x Thing) (y Thing) (z Thing))
                            (=> (and (Through x y) (Through y z)) (Through x z))))
(define-fun Necessary ((x Thing)) Bool
  (and (Exists x) (not (exists ((z Thing)) (Gives z x)))))
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Necessary y))))
(define-fun UniverseIsCaused () Bool (exists ((y Thing)) (Gives y u)))   ; the antecedent: the universe is caused

; The conclusion: something necessary gives existence to the universe.
(define-fun Conclusion () Bool (exists ((b Thing)) (and (Gives b u) (Necessary b))))

(echo "check 1: premises + universe caused + conclusion denied (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert UniverseIsCaused)
  (assert (not Conclusion)) (check-sat) (pop)

(echo "check 2: premises + universe caused together (expect sat: consistent)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert UniverseIsCaused) (check-sat) (pop)

(echo "check 3: without OP-001, conclusion denied (expect sat: OP-001 is needed)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert UniverseIsCaused)
  (assert (not Conclusion)) (check-sat) (pop)

(echo "check 4: universe not assumed caused, conclusion denied (expect sat: the conclusion is conditional)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001)
  (assert (not Conclusion)) (check-sat) (pop)