; PR-011: the universe is caused.  Independent cross-check in Z3, for both
; definitions of the universe.  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 Part (Thing Thing) Bool)    ; (Part p u): p is a part of u (physical or metaphysical)
(declare-const U Thing)                  ; the universe

(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 InU ((x Thing)) Bool (or (= x U) (Part x U)))

(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Part p A))
                                                      (forall ((p Thing)) (=> (Part p A) (not (Ess p)))))
                                                 (not (Ess A)))))
(define-fun OP006 () Bool (exists ((x Thing)) (and (InU x) (Poss x))))              ; broader definition
(define-fun OP007 () Bool (and (Ex U) (exists ((p Thing)) (Part p U))))            ; our definition
(define-fun Narrow () Bool (forall ((p Thing)) (=> (Part p U) (not (Ess p)))))    ; our definition of the universe

(echo "check 1: broader definition: MP-008 + OP-006 + nothing in the universe caused (expect unsat)")
(push) (assert MP008) (assert OP006) (assert (not (exists ((x Thing)) (and (InU x) (Poss x) (TA x))))) (check-sat) (pop)
(echo "check 2: our definition: MP-008 + MP-010 + definition + OP-007 + universe uncaused (expect unsat)")
(push) (assert MP008) (assert MP010) (assert Narrow) (assert OP007) (assert (not (TA U))) (check-sat) (pop)
(echo "check 3: broader definition without OP-006 (expect sat: OP-006 is needed)")
(push) (assert MP008) (assert (not (exists ((x Thing)) (and (InU x) (Poss x) (TA x))))) (check-sat) (pop)
(echo "check 4: our definition without OP-007 (expect sat: OP-007 is needed)")
(push) (assert MP008) (assert MP010) (assert Narrow) (assert (not (TA U))) (check-sat) (pop)
(echo "check 5: without MP-008, both definitions (expect sat: MP-008 is needed)")
(push) (assert MP010) (assert Narrow) (assert OP007) (assert OP006) (assert (not (TA U)))
  (assert (not (exists ((x Thing)) (and (InU x) (Poss x) (TA x))))) (check-sat) (pop)
(echo "check 6: broader definition, case 3 (a necessary part and a possible part) is consistent (expect sat)")
(push) (assert MP008) (assert OP006)
  (assert (exists ((n Thing) (p Thing)) (and (Part n U) (Part p U) (Ex n) (Ess n) (Poss p)))) (check-sat) (pop)