$ z3 --version
Z3 version 4.13.3 - 64 bit
$ z3 kalima_conclusion.smt2
check 1: premises + universe caused + conclusion denied (expect unsat)
unsat
check 2: premises + universe caused together (expect sat: consistent)
sat
check 3: without OP-001, conclusion denied (expect sat: OP-001 is needed)
sat
check 4: universe not assumed caused, conclusion denied (expect sat: the conclusion is conditional)
sat
exit code: 0
$ shasum -a 256 kalima_conclusion.smt2
33a16015f3fd8f0793547588bfd4de9dd0b366bf9f6ae654996f6a47b634ff51  kalima_conclusion.smt2
checked: 2026-09-29