Across 117500 122500 0

Kernel-checked forced assignments and closed-interval exclusions.

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_1 : Certificates.ExcludedOn (model0.B 1 ++ [step0.q]) 9000000000000 (model0.caps 1) (model0.ord 1) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_2 : Certificates.ExcludedOn (model0.B 2 ++ [step0.q]) 9000000000000 (model0.caps 2) (model0.ord 2) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_3 : Certificates.ExcludedOn (model0.B 3 ++ [step0.q]) 9000000000000 (model0.caps 3) (model0.ord 3) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_4 : Certificates.ExcludedOn (model0.B 4 ++ [step0.q]) 9000000000000 (model0.caps 4) (model0.ord 4) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_5 : Certificates.ExcludedOn (model0.B 5 ++ [step0.q]) 9000000000000 (model0.caps 5) (model0.ord 5) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_6 : Certificates.ExcludedOn (model0.B 6 ++ [step0.q]) 9000000000000 (model0.caps 6) (model0.ord 6) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_7 : Certificates.ExcludedOn (model0.B 7 ++ [step0.q]) 9000000000000 (model0.caps 7) (model0.ord 7) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_8 : Certificates.ExcludedOn (model0.B 8 ++ [step0.q]) 9000000000000 (model0.caps 8) (model0.ord 8) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.excluded0_9 : Certificates.ExcludedOn (model0.B 9 ++ [step0.q]) 9000000000000 (model0.caps 9) (model0.ord 9) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.checked0 : Certificates.StepValid model0 9000000000000 step0 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across117500122500.next0 : model0.insert step0 = model1