$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 -T:60 imkan.smt2
check 1: proof (a): premises + SP-001 + conclusion denied (expect unsat)
unsat
check 2: proof (a): premises + SP-001 together (expect sat: consistent)
sat
check 3: proof (a) without SP-001, conclusion denied (expect sat: SP-001 is needed)
sat
check 4: proof (b): MP-008 + OP-001 + SP-001 + conclusion denied (expect unsat)
unsat
check 5: proof (b) without OP-001, conclusion denied (expect sat: OP-001 is needed)
sat
exit code: 0
$ shasum -a 256 imkan.smt2
ca4c5b3cfd4113889f86c2d262b845927b6bc13d43ef4205ccf32a0c3ff06091  imkan.smt2
checked: 2026-09-30