Sint 160000 170000 6

Kernel-checked forced assignments and closed-interval exclusions.

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_1 : Certificates.ExcludedOn (model48.B 1 ++ [step48.q]) 9000000000000 (model48.caps 1) (model48.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_2 : Certificates.ExcludedOn (model48.B 2 ++ [step48.q]) 9000000000000 (model48.caps 2) (model48.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_3 : Certificates.ExcludedOn (model48.B 3 ++ [step48.q]) 9000000000000 (model48.caps 3) (model48.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_4 : Certificates.ExcludedOn (model48.B 4 ++ [step48.q]) 9000000000000 (model48.caps 4) (model48.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_5 : Certificates.ExcludedOn (model48.B 5 ++ [step48.q]) 9000000000000 (model48.caps 5) (model48.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_6 : Certificates.ExcludedOn (model48.B 6 ++ [step48.q]) 9000000000000 (model48.caps 6) (model48.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_7 : Certificates.ExcludedOn (model48.B 7 ++ [step48.q]) 9000000000000 (model48.caps 7) (model48.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_8 : Certificates.ExcludedOn (model48.B 8 ++ [step48.q]) 9000000000000 (model48.caps 8) (model48.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.excluded48_9 : Certificates.ExcludedOn (model48.B 9 ++ [step48.q]) 9000000000000 (model48.caps 9) (model48.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.checked48 : Certificates.StepValid model48 9000000000000 step48 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Sint160000170000.next48 : model48.insert step48 = model49