Sext 100000 110000 5

Kernel-checked forced assignments and closed-interval exclusions.

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_0 : Certificates.ExcludedOn (model40.B 0 ++ [step40.q]) 9000000000000 (model40.caps 0) (model40.ord 0) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_2 : Certificates.ExcludedOn (model40.B 2 ++ [step40.q]) 9000000000000 (model40.caps 2) (model40.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_3 : Certificates.ExcludedOn (model40.B 3 ++ [step40.q]) 9000000000000 (model40.caps 3) (model40.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_4 : Certificates.ExcludedOn (model40.B 4 ++ [step40.q]) 9000000000000 (model40.caps 4) (model40.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_5 : Certificates.ExcludedOn (model40.B 5 ++ [step40.q]) 9000000000000 (model40.caps 5) (model40.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_6 : Certificates.ExcludedOn (model40.B 6 ++ [step40.q]) 9000000000000 (model40.caps 6) (model40.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_7 : Certificates.ExcludedOn (model40.B 7 ++ [step40.q]) 9000000000000 (model40.caps 7) (model40.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_8 : Certificates.ExcludedOn (model40.B 8 ++ [step40.q]) 9000000000000 (model40.caps 8) (model40.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded40_9 : Certificates.ExcludedOn (model40.B 9 ++ [step40.q]) 9000000000000 (model40.caps 9) (model40.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked40 : Certificates.StepValid model40 9000000000000 step40 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next40 : model40.insert step40 = model41

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_1 : Certificates.ExcludedOn (model41.B 1 ++ [step41.q]) 9000000000000 (model41.caps 1) (model41.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_2 : Certificates.ExcludedOn (model41.B 2 ++ [step41.q]) 9000000000000 (model41.caps 2) (model41.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_3 : Certificates.ExcludedOn (model41.B 3 ++ [step41.q]) 9000000000000 (model41.caps 3) (model41.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_4 : Certificates.ExcludedOn (model41.B 4 ++ [step41.q]) 9000000000000 (model41.caps 4) (model41.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_5 : Certificates.ExcludedOn (model41.B 5 ++ [step41.q]) 9000000000000 (model41.caps 5) (model41.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_6 : Certificates.ExcludedOn (model41.B 6 ++ [step41.q]) 9000000000000 (model41.caps 6) (model41.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_7 : Certificates.ExcludedOn (model41.B 7 ++ [step41.q]) 9000000000000 (model41.caps 7) (model41.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_8 : Certificates.ExcludedOn (model41.B 8 ++ [step41.q]) 9000000000000 (model41.caps 8) (model41.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded41_9 : Certificates.ExcludedOn (model41.B 9 ++ [step41.q]) 9000000000000 (model41.caps 9) (model41.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked41 : Certificates.StepValid model41 9000000000000 step41 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next41 : model41.insert step41 = model42