$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 recursion_worlds.smt2
check 1: no base, World A (all exist) respects dependence (expect sat)
sat
check 2: no base, World B (none exist) respects dependence (expect sat)
sat
check 3: with base u10 existing, World B is impossible (expect unsat)
unsat
check 4: no base, the recurrence allows f12 = 0 (expect sat)
sat
check 5: no base, the recurrence also allows f12 = 144 (expect sat)
sat
check 6: with base f0 = 0, f1 = 1, f12 can only be 144 (expect unsat)
unsat
exit code: 0
$ shasum -a 256 recursion_worlds.smt2
568456bfa03aa65fc486eefca25661da7184e8ee5366949da1a37fcfc2b79331  recursion_worlds.smt2
checked: 2026-09-29