$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 no_self_creation.smt2
check 1: MP-001 + MP-002 + something gives existence to itself (expect unsat)
unsat
check 2: MP-002 only + self-giver (expect sat: MP-001 is needed)
sat
check 3: MP-001 only + self-giver (expect sat: MP-002 is needed)
sat
check 4: MP-001 + MP-002 + a gives existence to b (expect sat: postulates allow giving)
sat
exit code: 0
$ shasum -a 256 no_self_creation.smt2
11b1cac0e058966968353c60d581ad915abb7359ea073741d7d28ea4d1328e1a  no_self_creation.smt2
checked: 2026-09-29