Install requirements.txt in a virtual environment. Run python cycle_type.py to validate composition and reproduce N12 and N14 one-fixed-point tests (solver timeouts depend on hardware). For the N14 two-fixed-point test run: from cycle_type import run; run(14,"has2",fixed=2); run(14,"no2",fixed=2). Each UNSAT trace is separately RUP-checked. Existing N12 proof can be checked with certificates.check using the supplied CNF and DRUP files. Historical rectangle-count exclusions are not re-proved by this supplement. General configurations; relaxed witnesses are NOT NTIL. See session29/report.txt.
