Aown 240000 250000 3

Kernel-checked forced assignments and closed-interval exclusions.

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_1 : Certificates.ExcludedOn (model24.B 1 ++ [step24.q]) 9000000000000 (model24.caps 1) (model24.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_2 : Certificates.ExcludedOn (model24.B 2 ++ [step24.q]) 9000000000000 (model24.caps 2) (model24.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_3 : Certificates.ExcludedOn (model24.B 3 ++ [step24.q]) 9000000000000 (model24.caps 3) (model24.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_4 : Certificates.ExcludedOn (model24.B 4 ++ [step24.q]) 9000000000000 (model24.caps 4) (model24.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_5 : Certificates.ExcludedOn (model24.B 5 ++ [step24.q]) 9000000000000 (model24.caps 5) (model24.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_6 : Certificates.ExcludedOn (model24.B 6 ++ [step24.q]) 9000000000000 (model24.caps 6) (model24.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_7 : Certificates.ExcludedOn (model24.B 7 ++ [step24.q]) 9000000000000 (model24.caps 7) (model24.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_8 : Certificates.ExcludedOn (model24.B 8 ++ [step24.q]) 9000000000000 (model24.caps 8) (model24.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded24_9 : Certificates.ExcludedOn (model24.B 9 ++ [step24.q]) 9000000000000 (model24.caps 9) (model24.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.checked24 : Certificates.StepValid model24 9000000000000 step24 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.next24 : model24.insert step24 = model25

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_1 : Certificates.ExcludedOn (model25.B 1 ++ [step25.q]) 9000000000000 (model25.caps 1) (model25.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_2 : Certificates.ExcludedOn (model25.B 2 ++ [step25.q]) 9000000000000 (model25.caps 2) (model25.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_3 : Certificates.ExcludedOn (model25.B 3 ++ [step25.q]) 9000000000000 (model25.caps 3) (model25.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_4 : Certificates.ExcludedOn (model25.B 4 ++ [step25.q]) 9000000000000 (model25.caps 4) (model25.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_5 : Certificates.ExcludedOn (model25.B 5 ++ [step25.q]) 9000000000000 (model25.caps 5) (model25.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_6 : Certificates.ExcludedOn (model25.B 6 ++ [step25.q]) 9000000000000 (model25.caps 6) (model25.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_7 : Certificates.ExcludedOn (model25.B 7 ++ [step25.q]) 9000000000000 (model25.caps 7) (model25.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_8 : Certificates.ExcludedOn (model25.B 8 ++ [step25.q]) 9000000000000 (model25.caps 8) (model25.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.excluded25_9 : Certificates.ExcludedOn (model25.B 9 ++ [step25.q]) 9000000000000 (model25.caps 9) (model25.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.checked25 : Certificates.StepValid model25 9000000000000 step25 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown240000250000.next25 : model25.insert step25 = model26