Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch022.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell0010 : AngleCell

Subcell 0010 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell0011 : AngleCell

Subcell 0011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102211 : AngleCell

Subcell 00102211 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102212 : AngleCell

Subcell 00102212 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102213 : AngleCell

Subcell 00102213 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102300 : AngleCell

Subcell 00102300 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102301 : AngleCell

Subcell 00102301 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102302 : AngleCell

Subcell 00102302 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102303 : AngleCell

Subcell 00102303 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102310 : AngleCell

Subcell 00102310 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102311 : AngleCell

Subcell 00102311 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102312 : AngleCell

Subcell 00102312 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00102313 : AngleCell

Subcell 00102313 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103200 : AngleCell

Subcell 00103200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103201 : AngleCell

Subcell 00103201 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103202 : AngleCell

Subcell 00103202 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103203 : AngleCell

Subcell 00103203 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103210 : AngleCell

Subcell 00103210 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103211 : AngleCell

Subcell 00103211 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103212 : AngleCell

Subcell 00103212 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103213 : AngleCell

Subcell 00103213 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103300 : AngleCell

Subcell 00103300 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103301 : AngleCell

Subcell 00103301 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103302 : AngleCell

Subcell 00103302 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103303 : AngleCell

Subcell 00103303 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103310 : AngleCell

Subcell 00103310 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103311 : AngleCell

Subcell 00103311 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103312 : AngleCell

Subcell 00103312 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00103313 : AngleCell

Subcell 00103313 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112200 : AngleCell

Subcell 00112200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112201 : AngleCell

Subcell 00112201 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112202 : AngleCell

Subcell 00112202 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112203 : AngleCell

Subcell 00112203 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112210 : AngleCell

Subcell 00112210 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112211 : AngleCell

Subcell 00112211 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112212 : AngleCell

Subcell 00112212 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112213 : AngleCell

Subcell 00112213 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112300 : AngleCell

Subcell 00112300 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112301 : AngleCell

Subcell 00112301 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112302 : AngleCell

Subcell 00112302 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112303 : AngleCell

Subcell 00112303 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112310 : AngleCell

Subcell 00112310 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112311 : AngleCell

Subcell 00112311 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112312 : AngleCell

Subcell 00112312 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00112313 : AngleCell

Subcell 00112313 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113200 : AngleCell

Subcell 00113200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113201 : AngleCell

Subcell 00113201 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113202 : AngleCell

Subcell 00113202 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113203 : AngleCell

Subcell 00113203 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113210 : AngleCell

Subcell 00113210 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113211 : AngleCell

Subcell 00113211 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113212 : AngleCell

Subcell 00113212 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113213 : AngleCell

Subcell 00113213 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113300 : AngleCell

Subcell 00113300 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113301 : AngleCell

Subcell 00113301 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113302 : AngleCell

Subcell 00113302 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9faa13f35d.thetaAboveCell00113303 : AngleCell

Subcell 00113303 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

• One or more equations did not get rendered due to their size.

Gerver sofa dependency batch

• KernelOnly.PartE.E24KC6ProofBatch3b6d17fd8ecf6129.

E24KC6 explicit proof-producing certificate batch.

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00102211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00102212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00102212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00102212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00102212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00102213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00102213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00102213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010221311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00102213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00102300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00102301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00102302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00102302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00102302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00102302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00102303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00102303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00102303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010230311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00102303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00102310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00102311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00102312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00102312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00102312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00102312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00102313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00102313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00102313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010231311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00102313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010320311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010321311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010330311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0010331311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011220311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011221311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011230311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells9faa13f35d.thetaAboveCell00112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011231311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00113203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00113203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00113203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011320311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00113203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00113210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00113210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00113210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00113210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00113211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00113211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00113211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00113211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00113212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00113212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00113212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00113212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00113213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00113213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00113213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011321311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00113213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00113300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00113300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00113300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00113300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells9faa13f35d.thetaAboveCell00113301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells9faa13f35d.thetaAboveCell00113301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells9faa13f35d.thetaAboveCell00113301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells9faa13f35d.thetaAboveCell00113301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00113302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00113302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00113302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00113302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells9faa13f35d.thetaAboveCell00113303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells9faa13f35d.thetaAboveCell00113303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells9faa13f35d.thetaAboveCell00113303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011330311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells9faa13f35d.thetaAboveCell00113303)) = true