Aown 330000 340000 1

Kernel-checked forced assignments and closed-interval exclusions.

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_0 : Certificates.ExcludedOn (model8.B 0 ++ [step8.q]) 9000000000000 (model8.caps 0) (model8.ord 0) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_2 : Certificates.ExcludedOn (model8.B 2 ++ [step8.q]) 9000000000000 (model8.caps 2) (model8.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_3 : Certificates.ExcludedOn (model8.B 3 ++ [step8.q]) 9000000000000 (model8.caps 3) (model8.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_4 : Certificates.ExcludedOn (model8.B 4 ++ [step8.q]) 9000000000000 (model8.caps 4) (model8.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_5 : Certificates.ExcludedOn (model8.B 5 ++ [step8.q]) 9000000000000 (model8.caps 5) (model8.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_6 : Certificates.ExcludedOn (model8.B 6 ++ [step8.q]) 9000000000000 (model8.caps 6) (model8.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_7 : Certificates.ExcludedOn (model8.B 7 ++ [step8.q]) 9000000000000 (model8.caps 7) (model8.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_8 : Certificates.ExcludedOn (model8.B 8 ++ [step8.q]) 9000000000000 (model8.caps 8) (model8.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded8_9 : Certificates.ExcludedOn (model8.B 9 ++ [step8.q]) 9000000000000 (model8.caps 9) (model8.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.checked8 : Certificates.StepValid model8 9000000000000 step8 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.next8 : model8.insert step8 = model9

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_0 : Certificates.ExcludedOn (model9.B 0 ++ [step9.q]) 9000000000000 (model9.caps 0) (model9.ord 0) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_1 : Certificates.ExcludedOn (model9.B 1 ++ [step9.q]) 9000000000000 (model9.caps 1) (model9.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_2 : Certificates.ExcludedOn (model9.B 2 ++ [step9.q]) 9000000000000 (model9.caps 2) (model9.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_3 : Certificates.ExcludedOn (model9.B 3 ++ [step9.q]) 9000000000000 (model9.caps 3) (model9.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_4 : Certificates.ExcludedOn (model9.B 4 ++ [step9.q]) 9000000000000 (model9.caps 4) (model9.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_5 : Certificates.ExcludedOn (model9.B 5 ++ [step9.q]) 9000000000000 (model9.caps 5) (model9.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_6 : Certificates.ExcludedOn (model9.B 6 ++ [step9.q]) 9000000000000 (model9.caps 6) (model9.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_8 : Certificates.ExcludedOn (model9.B 8 ++ [step9.q]) 9000000000000 (model9.caps 8) (model9.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded9_9 : Certificates.ExcludedOn (model9.B 9 ++ [step9.q]) 9000000000000 (model9.caps 9) (model9.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.checked9 : Certificates.StepValid model9 9000000000000 step9 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.next9 : model9.insert step9 = model10

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_1 : Certificates.ExcludedOn (model10.B 1 ++ [step10.q]) 9000000000000 (model10.caps 1) (model10.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_2 : Certificates.ExcludedOn (model10.B 2 ++ [step10.q]) 9000000000000 (model10.caps 2) (model10.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_3 : Certificates.ExcludedOn (model10.B 3 ++ [step10.q]) 9000000000000 (model10.caps 3) (model10.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_4 : Certificates.ExcludedOn (model10.B 4 ++ [step10.q]) 9000000000000 (model10.caps 4) (model10.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_5 : Certificates.ExcludedOn (model10.B 5 ++ [step10.q]) 9000000000000 (model10.caps 5) (model10.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_6 : Certificates.ExcludedOn (model10.B 6 ++ [step10.q]) 9000000000000 (model10.caps 6) (model10.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_7 : Certificates.ExcludedOn (model10.B 7 ++ [step10.q]) 9000000000000 (model10.caps 7) (model10.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_8 : Certificates.ExcludedOn (model10.B 8 ++ [step10.q]) 9000000000000 (model10.caps 8) (model10.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded10_9 : Certificates.ExcludedOn (model10.B 9 ++ [step10.q]) 9000000000000 (model10.caps 9) (model10.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.checked10 : Certificates.StepValid model10 9000000000000 step10 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.next10 : model10.insert step10 = model11

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_1 : Certificates.ExcludedOn (model11.B 1 ++ [step11.q]) 9000000000000 (model11.caps 1) (model11.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_2 : Certificates.ExcludedOn (model11.B 2 ++ [step11.q]) 9000000000000 (model11.caps 2) (model11.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_3 : Certificates.ExcludedOn (model11.B 3 ++ [step11.q]) 9000000000000 (model11.caps 3) (model11.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_4 : Certificates.ExcludedOn (model11.B 4 ++ [step11.q]) 9000000000000 (model11.caps 4) (model11.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_5 : Certificates.ExcludedOn (model11.B 5 ++ [step11.q]) 9000000000000 (model11.caps 5) (model11.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_6 : Certificates.ExcludedOn (model11.B 6 ++ [step11.q]) 9000000000000 (model11.caps 6) (model11.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_7 : Certificates.ExcludedOn (model11.B 7 ++ [step11.q]) 9000000000000 (model11.caps 7) (model11.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_8 : Certificates.ExcludedOn (model11.B 8 ++ [step11.q]) 9000000000000 (model11.caps 8) (model11.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded11_9 : Certificates.ExcludedOn (model11.B 9 ++ [step11.q]) 9000000000000 (model11.caps 9) (model11.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.checked11 : Certificates.StepValid model11 9000000000000 step11 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.next11 : model11.insert step11 = model12

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_0 : Certificates.ExcludedOn (model12.B 0 ++ [step12.q]) 9000000000000 (model12.caps 0) (model12.ord 0) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_1 : Certificates.ExcludedOn (model12.B 1 ++ [step12.q]) 9000000000000 (model12.caps 1) (model12.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_3 : Certificates.ExcludedOn (model12.B 3 ++ [step12.q]) 9000000000000 (model12.caps 3) (model12.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_4 : Certificates.ExcludedOn (model12.B 4 ++ [step12.q]) 9000000000000 (model12.caps 4) (model12.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_5 : Certificates.ExcludedOn (model12.B 5 ++ [step12.q]) 9000000000000 (model12.caps 5) (model12.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_6 : Certificates.ExcludedOn (model12.B 6 ++ [step12.q]) 9000000000000 (model12.caps 6) (model12.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_7 : Certificates.ExcludedOn (model12.B 7 ++ [step12.q]) 9000000000000 (model12.caps 7) (model12.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_8 : Certificates.ExcludedOn (model12.B 8 ++ [step12.q]) 9000000000000 (model12.caps 8) (model12.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded12_9 : Certificates.ExcludedOn (model12.B 9 ++ [step12.q]) 9000000000000 (model12.caps 9) (model12.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.checked12 : Certificates.StepValid model12 9000000000000 step12 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.next12 : model12.insert step12 = model13

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_1 : Certificates.ExcludedOn (model13.B 1 ++ [step13.q]) 9000000000000 (model13.caps 1) (model13.ord 1) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_2 : Certificates.ExcludedOn (model13.B 2 ++ [step13.q]) 9000000000000 (model13.caps 2) (model13.ord 2) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_3 : Certificates.ExcludedOn (model13.B 3 ++ [step13.q]) 9000000000000 (model13.caps 3) (model13.ord 3) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_4 : Certificates.ExcludedOn (model13.B 4 ++ [step13.q]) 9000000000000 (model13.caps 4) (model13.ord 4) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_5 : Certificates.ExcludedOn (model13.B 5 ++ [step13.q]) 9000000000000 (model13.caps 5) (model13.ord 5) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_6 : Certificates.ExcludedOn (model13.B 6 ++ [step13.q]) 9000000000000 (model13.caps 6) (model13.ord 6) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_7 : Certificates.ExcludedOn (model13.B 7 ++ [step13.q]) 9000000000000 (model13.caps 7) (model13.ord 7) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_8 : Certificates.ExcludedOn (model13.B 8 ++ [step13.q]) 9000000000000 (model13.caps 8) (model13.ord 8) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded13_9 : Certificates.ExcludedOn (model13.B 9 ++ [step13.q]) 9000000000000 (model13.caps 9) (model13.ord 9) 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.checked13 : Certificates.StepValid model13 9000000000000 step13 0 1 100

theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.next13 : model13.insert step13 = model14