$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 no_circular_creation.smt2
check 1: MP-001..003 + circle of 2 (expect unsat)
unsat
check 2: MP-001..003 + circle of 3 (expect unsat)
unsat
check 3: MP-001..003 + circle of 4 (expect unsat)
unsat
check 4: MP-001..003 + circle of 5 (expect unsat)
unsat
check 5: circle of 3 without MP-003 (expect sat: MP-003 is needed)
sat
check 6: circle of 3 without MP-001 (expect sat: MP-001 is needed)
sat
check 7: circle of 3 without MP-002 (expect sat: MP-002 is needed)
sat
check 8: MP-001..003 + straight chain c gives b gives a (expect sat: postulates allow chains)
sat
exit code: 0
$ shasum -a 256 no_circular_creation.smt2
a9393b5e507742e51e174f8c4a827f5328e190c7736c2ff2d9c40b13b79131ad  no_circular_creation.smt2
checked: 2026-09-29