Five rows of a 60-row project schedule are an irreducible infeasible subsystem

Identifier: F:schedule-deadline-iis
Proof route: search-certificate
External status: Not recorded
Axiom footprint: smtlib2-linear-arithmetic-semantics, axeyum-smtlib.parser-faithfulness-of-the-committed-instance, axeyum-ir.ground-evaluator-model-replay-semantics, axeyum-solver.farkas-certificate-checker

Recorded description

The project schedule in artifacts/instances/infeasibility/schedule-deadline.smt2 -- 20 tasks, continuous start times, 60 constraint rows -- admits no feasible schedule, and the five rows material_t03, prec_t03_t06, prec_t06_t09, prec_t09_t12 and deadline_delivery are an IRREDUCIBLE infeasible subsystem: jointly unsatisfiable, and dropping any single one leaves a satisfiable set. The other 55 rows are jointly satisfiable. The explanation is a critical chain -- the long-lead material for t03 lands day 6, and 14 days of chained work plus a 4-day final task cannot fit inside a 20-day delivery promise.

Formal statement

(assert (and (not (exists ((s_t03 Real) (s_t06 Real) (s_t09 Real) (s_t12 Real)) (and (>= s_t03 6.0) (>= s_t06 (+ s_t03 5.0)) (>= s_t09 (+ s_t06 6.0)) (>= s_t12 (+ s_t09 3.0)) (<= (+ s_t12 4.0) 20.0)))) (exists ((s_t03 Real) (s_t06 Real) (s_t09 Real) (s_t12 Real)) (and (>= s_t06 (+ s_t03 5.0)) (>= s_t09 (+ s_t06 6.0)) (>= s_t12 (+ s_t09 3.0)) (<= (+ s_t12 4.0) 20.0))) (exists ((s_t03 Real) (s_t06 Real) (s_t09 Real) (s_t12 Real)) (and (>= s_t03 6.0) (>= s_t09 (+ s_t06 6.0)) (>= s_t12 (+ s_t09 3.0)) (<= (+ s_t12 4.0) 20.0))) (exists ((s_t03 Real) (s_t06 Real) (s_t09 Real) (s_t12 Real)) (and (>= s_t03 6.0) (>= s_t06 (+ s_t03 5.0)) (>= s_t12 (+ s_t09 3.0)) (<= (+ s_t12 4.0) 20.0))) (exists ((s_t03 Real) (s_t06 Real) (s_t09 Real) (s_t12 Real)) (and (>= s_t03 6.0) (>= s_t06 (+ s_t03 5.0)) (>= s_t09 (+ s_t06 6.0)) (<= (+ s_t12 4.0) 20.0))) (exists ((s_t03 Real) (s_t06 Real) (s_t09 Real) (s_t12 Real)) (and (>= s_t03 6.0) (>= s_t06 (+ s_t03 5.0)) (>= s_t09 (+ s_t06 6.0)) (>= s_t12 (+ s_t09 3.0))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 0 direct dependents

Evidence

schedule-core-refutation

Kind: unsat-certificate
Status: checked

Supports: The five named rows are jointly unsatisfiable.

Checker command

cargo run --release -q -p axeyum-solver --features full --example infeasibility_iis -- artifacts/instances/infeasibility/schedule-deadline.smt2 --expect-rows 60 --expect-core 5

Evidence notes

Ran 2026-08-14 in 0.11s. `produce_evidence` on the five reports `Evidence::UnsatFarkas` with `check_outcome` = `verified` and trust step `farkas` CERTIFIED THIS RUN. z3 4.13.3 returns the same five names. This half is strictly stronger than the two integer facts' and is recorded separately as F:schedule-critical-chain-infeasible, which carries the kernel-checked Lean proof term on proof_route `kernel-lean`.

schedule-leave-one-out-witnesses

Kind: witness-replay
Status: checked

Supports: Dropping any single one of the five leaves a satisfiable set -- the core is irreducible.

Checker command

cargo run --release -q -p axeyum-solver --features full --example infeasibility_iis -- artifacts/instances/infeasibility/schedule-deadline.smt2 --expect-rows 60 --expect-core 5

Evidence notes

All five leave-one-out subsets re-solved to `sat` with each model replayed against its own subset by the IR ground evaluator; the instance minus the core is `sat` with a replayed model. z3 agrees on all five. Note that the core does NOT include start_t01 or prec_t01_t03: the chain from the project start would also overrun (0+4+5+6+3+4 = 22 > 20), so a six-row core exists, but the material release at day 6 dominates the day-4 earliest start and the minimizer correctly returns the shorter, more informative explanation. Two different irreducible cores, and the one you get is the one you can act on.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum lane `infeasibility`, 2026-08-14: crates/axeyum-solver/examples/infeasibility_iis.rs over the committed instance",
  "source": "instance authored by this lane (scripts/gen-infeasibility-instances.py); not extracted from any corpus"
}