$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 -T:60 universe_is_caused.smt2
check 1: broader definition: MP-008 + OP-006 + nothing in the universe caused (expect unsat)
unsat
check 2: our definition: MP-008 + MP-010 + definition + OP-007 + universe uncaused (expect unsat)
unsat
check 3: broader definition without OP-006 (expect sat: OP-006 is needed)
sat
check 4: our definition without OP-007 (expect sat: OP-007 is needed)
sat
check 5: without MP-008, both definitions (expect sat: MP-008 is needed)
sat
check 6: broader definition, case 3 (a necessary part and a possible part) is consistent (expect sat)
sat
exit code: 0
$ shasum -a 256 universe_is_caused.smt2
7d5be797ddd465aa8d38cabd34496ed08d649f94276aeb4bd8754b21eb7a2f94  universe_is_caused.smt2
checked: 2026-09-30