Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch009.
• GerverSofa.KernelOnly.PartE.Certificates.Batch024.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb518b98fbe.thetaAboveCell0110 : AngleCell

Subcell 0110 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.CertificateCellsb518b98fbe.thetaAboveCell0111 : AngleCell

Subcell 0111 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.CertificateCellsb518b98fbe.thetaAboveCell01103210 : AngleCell

Subcell 01103210 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.CertificateCellsb518b98fbe.thetaAboveCell01103211 : AngleCell

Subcell 01103211 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.CertificateCellsb518b98fbe.thetaAboveCell01103212 : AngleCell

Subcell 01103212 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.CertificateCellsb518b98fbe.thetaAboveCell01103213 : AngleCell

Subcell 01103213 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.CertificateCellsb518b98fbe.thetaAboveCell01103220 : AngleCell

Subcell 01103220 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.CertificateCellsb518b98fbe.thetaAboveCell01103221 : AngleCell

Subcell 01103221 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.CertificateCellsb518b98fbe.thetaAboveCell01103222 : AngleCell

Subcell 01103222 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.CertificateCellsb518b98fbe.thetaAboveCell01103223 : AngleCell

Subcell 01103223 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.CertificateCellsb518b98fbe.thetaAboveCell01103230 : AngleCell

Subcell 01103230 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.CertificateCellsb518b98fbe.thetaAboveCell01103231 : AngleCell

Subcell 01103231 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.CertificateCellsb518b98fbe.thetaAboveCell01103232 : AngleCell

Subcell 01103232 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.CertificateCellsb518b98fbe.thetaAboveCell01103233 : AngleCell

Subcell 01103233 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.CertificateCellsb518b98fbe.thetaAboveCell01103300 : AngleCell

Subcell 01103300 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.CertificateCellsb518b98fbe.thetaAboveCell01103301 : AngleCell

Subcell 01103301 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.CertificateCellsb518b98fbe.thetaAboveCell01103302 : AngleCell

Subcell 01103302 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.CertificateCellsb518b98fbe.thetaAboveCell01103303 : AngleCell

Subcell 01103303 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.CertificateCellsb518b98fbe.thetaAboveCell01103310 : AngleCell

Subcell 01103310 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.CertificateCellsb518b98fbe.thetaAboveCell01103311 : AngleCell

Subcell 01103311 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.CertificateCellsb518b98fbe.thetaAboveCell01103312 : AngleCell

Subcell 01103312 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.CertificateCellsb518b98fbe.thetaAboveCell01103313 : AngleCell

Subcell 01103313 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.CertificateCellsb518b98fbe.thetaAboveCell01103320 : AngleCell

Subcell 01103320 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.CertificateCellsb518b98fbe.thetaAboveCell01103321 : AngleCell

Subcell 01103321 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.CertificateCellsb518b98fbe.thetaAboveCell01103322 : AngleCell

Subcell 01103322 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.CertificateCellsb518b98fbe.thetaAboveCell01103323 : AngleCell

Subcell 01103323 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.CertificateCellsb518b98fbe.thetaAboveCell01103330 : AngleCell

Subcell 01103330 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.CertificateCellsb518b98fbe.thetaAboveCell01103331 : AngleCell

Subcell 01103331 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.CertificateCellsb518b98fbe.thetaAboveCell01103332 : AngleCell

Subcell 01103332 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.CertificateCellsb518b98fbe.thetaAboveCell01103333 : AngleCell

Subcell 01103333 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.CertificateCellsb518b98fbe.thetaAboveCell01112020 : AngleCell

Subcell 01112020 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.CertificateCellsb518b98fbe.thetaAboveCell01112021 : AngleCell

Subcell 01112021 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.CertificateCellsb518b98fbe.thetaAboveCell01112022 : AngleCell

Subcell 01112022 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.CertificateCellsb518b98fbe.thetaAboveCell01112023 : AngleCell

Subcell 01112023 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.CertificateCellsb518b98fbe.thetaAboveCell01112030 : AngleCell

Subcell 01112030 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.CertificateCellsb518b98fbe.thetaAboveCell01112031 : AngleCell

Subcell 01112031 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.CertificateCellsb518b98fbe.thetaAboveCell01112032 : AngleCell

Subcell 01112032 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.CertificateCellsb518b98fbe.thetaAboveCell01112033 : AngleCell

Subcell 01112033 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.CertificateCellsb518b98fbe.thetaAboveCell01112120 : AngleCell

Subcell 01112120 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.CertificateCellsb518b98fbe.thetaAboveCell01112121 : AngleCell

Subcell 01112121 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.CertificateCellsb518b98fbe.thetaAboveCell01112122 : AngleCell

Subcell 01112122 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.CertificateCellsb518b98fbe.thetaAboveCell01112123 : AngleCell

Subcell 01112123 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.CertificateCellsb518b98fbe.thetaAboveCell01112130 : AngleCell

Subcell 01112130 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.CertificateCellsb518b98fbe.thetaAboveCell01112131 : AngleCell

Subcell 01112131 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.CertificateCellsb518b98fbe.thetaAboveCell01112132 : AngleCell

Subcell 01112132 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.CertificateCellsb518b98fbe.thetaAboveCell01112133 : AngleCell

Subcell 01112133 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.CertificateCellsb518b98fbe.thetaAboveCell01112200 : AngleCell

Subcell 01112200 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.CertificateCellsb518b98fbe.thetaAboveCell01112201 : AngleCell

Subcell 01112201 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.CertificateCellsb518b98fbe.thetaAboveCell01112202 : AngleCell

Subcell 01112202 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.CertificateCellsb518b98fbe.thetaAboveCell01112203 : AngleCell

Subcell 01112203 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.CertificateCellsb518b98fbe.thetaAboveCell01112210 : AngleCell

Subcell 01112210 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.CertificateCellsb518b98fbe.thetaAboveCell01112211 : AngleCell

Subcell 01112211 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.CertificateCellsb518b98fbe.thetaAboveCell01112212 : AngleCell

Subcell 01112212 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.CertificateCellsb518b98fbe.thetaAboveCell01112213 : AngleCell

Subcell 01112213 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.CertificateCellsb518b98fbe.thetaAboveCell01112220 : AngleCell

Subcell 01112220 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.CertificateCellsb518b98fbe.thetaAboveCell01112221 : AngleCell

Subcell 01112221 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.CertificateCellsb518b98fbe.thetaAboveCell01112222 : AngleCell

Subcell 01112222 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.CertificateCellsb518b98fbe.thetaAboveCell01112223 : AngleCell

Subcell 01112223 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.CertificateCellsb518b98fbe.thetaAboveCell01112230 : AngleCell

Subcell 01112230 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.CertificateCellsb518b98fbe.thetaAboveCell01112231 : AngleCell

Subcell 01112231 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.CertificateCellsb518b98fbe.thetaAboveCell01112232 : AngleCell

Subcell 01112232 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.CertificateCellsb518b98fbe.thetaAboveCell01112233 : AngleCell

Subcell 01112233 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.CertificateCellsb518b98fbe.thetaAboveCell01112300 : AngleCell

Subcell 01112300 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.CertificateCellsb518b98fbe.thetaAboveCell01112301 : AngleCell

Subcell 01112301 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.CertificateCellsb518b98fbe.thetaAboveCell01112302 : AngleCell

Subcell 01112302 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.CertificateCellsb518b98fbe.thetaAboveCell01112303 : AngleCell

Subcell 01112303 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.CertificateCellsb518b98fbe.thetaAboveCell01112310 : AngleCell

Subcell 01112310 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.CertificateCellsb518b98fbe.thetaAboveCell01112311 : AngleCell

Subcell 01112311 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.CertificateCellsb518b98fbe.thetaAboveCell01112312 : AngleCell

Subcell 01112312 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.CertificateCellsb518b98fbe.thetaAboveCell01112313 : AngleCell

Subcell 01112313 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.CertificateCellsb518b98fbe.thetaAboveCell01112320 : AngleCell

Subcell 01112320 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.CertificateCellsb518b98fbe.thetaAboveCell01112321 : AngleCell

Subcell 01112321 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.CertificateCellsb518b98fbe.thetaAboveCell01112322 : AngleCell

Subcell 01112322 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.CertificateCellsb518b98fbe.thetaAboveCell01112323 : AngleCell

Subcell 01112323 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.CertificateCellsb518b98fbe.thetaAboveCell01112330 : AngleCell

Subcell 01112330 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.CertificateCellsb518b98fbe.thetaAboveCell01112331 : AngleCell

Subcell 01112331 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.CertificateCellsb518b98fbe.thetaAboveCell01112332 : AngleCell

Subcell 01112332 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.CertificateCellsb518b98fbe.thetaAboveCell01112333 : AngleCell

Subcell 01112333 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.CertificateCellsb518b98fbe.thetaAboveCell01113020 : AngleCell

Subcell 01113020 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.CertificateCellsb518b98fbe.thetaAboveCell01113021 : AngleCell

Subcell 01113021 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.CertificateCellsb518b98fbe.thetaAboveCell01113022 : AngleCell

Subcell 01113022 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.CertificateCellsb518b98fbe.thetaAboveCell01113023 : AngleCell

Subcell 01113023 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.CertificateCellsb518b98fbe.thetaAboveCell01113030 : AngleCell

Subcell 01113030 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.CertificateCellsb518b98fbe.thetaAboveCell01113031 : AngleCell

Subcell 01113031 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.CertificateCellsb518b98fbe.thetaAboveCell01113032 : AngleCell

Subcell 01113032 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.CertificateCellsb518b98fbe.thetaAboveCell01113033 : AngleCell

Subcell 01113033 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.CertificateCellsb518b98fbe.thetaAboveCell01113120 : AngleCell

Subcell 01113120 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.CertificateCellsb518b98fbe.thetaAboveCell01113121 : AngleCell

Subcell 01113121 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.CertificateCellsb518b98fbe.thetaAboveCell01113122 : AngleCell

Subcell 01113122 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.CertificateCellsb518b98fbe.thetaAboveCell01113123 : AngleCell

Subcell 01113123 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.CertificateCellsb518b98fbe.thetaAboveCell01113130 : AngleCell

Subcell 01113130 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.CertificateCellsb518b98fbe.thetaAboveCell01113131 : AngleCell

Subcell 01113131 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.CertificateCellsb518b98fbe.thetaAboveCell01113132 : AngleCell

Subcell 01113132 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.CertificateCellsb518b98fbe.thetaAboveCell01113133 : AngleCell

Subcell 01113133 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.CertificateCellsb518b98fbe.thetaAboveCell01113200 : AngleCell

Subcell 01113200 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.CertificateCellsb518b98fbe.thetaAboveCell01113201 : AngleCell

Subcell 01113201 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.CertificateCellsb518b98fbe.thetaAboveCell01113202 : AngleCell

Subcell 01113202 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.CertificateCells37514173c1.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.CertificateCells37514173c1.thetaAboveCell0100 : AngleCell

Subcell 0100 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.CertificateCells37514173c1.thetaBelowCell1110 : AngleCell

Subcell 1110 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell1111 : AngleCell

Subcell 1111 of the theta-below 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.CertificateCells37514173c1.thetaAboveCell00113310 : AngleCell

Subcell 00113310 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.CertificateCells37514173c1.thetaAboveCell00113311 : AngleCell

Subcell 00113311 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.CertificateCells37514173c1.thetaAboveCell00113312 : AngleCell

Subcell 00113312 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.CertificateCells37514173c1.thetaAboveCell00113313 : AngleCell

Subcell 00113313 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.CertificateCells37514173c1.thetaAboveCell01002200 : AngleCell

Subcell 01002200 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.CertificateCells37514173c1.thetaAboveCell01002201 : AngleCell

Subcell 01002201 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.CertificateCells37514173c1.thetaAboveCell01002202 : AngleCell

Subcell 01002202 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.CertificateCells37514173c1.thetaAboveCell01002203 : AngleCell

Subcell 01002203 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.CertificateCells37514173c1.thetaAboveCell01002210 : AngleCell

Subcell 01002210 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.CertificateCells37514173c1.thetaAboveCell01002211 : AngleCell

Subcell 01002211 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.CertificateCells37514173c1.thetaAboveCell01002212 : AngleCell

Subcell 01002212 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.CertificateCells37514173c1.thetaAboveCell01002213 : AngleCell

Subcell 01002213 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.CertificateCells37514173c1.thetaAboveCell01002300 : AngleCell

Subcell 01002300 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.CertificateCells37514173c1.thetaAboveCell01002301 : AngleCell

Subcell 01002301 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.CertificateCells37514173c1.thetaAboveCell01002302 : AngleCell

Subcell 01002302 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.CertificateCells37514173c1.thetaAboveCell01002303 : AngleCell

Subcell 01002303 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.CertificateCells37514173c1.thetaAboveCell01002310 : AngleCell

Subcell 01002310 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.CertificateCells37514173c1.thetaAboveCell01002311 : AngleCell

Subcell 01002311 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.CertificateCells37514173c1.thetaAboveCell01003200 : AngleCell

Subcell 01003200 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.CertificateCells37514173c1.thetaAboveCell01003201 : AngleCell

Subcell 01003201 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.CertificateCells37514173c1.thetaBelowCell11103022 : AngleCell

Subcell 11103022 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103023 : AngleCell

Subcell 11103023 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103031 : AngleCell

Subcell 11103031 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103032 : AngleCell

Subcell 11103032 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103033 : AngleCell

Subcell 11103033 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103120 : AngleCell

Subcell 11103120 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103122 : AngleCell

Subcell 11103122 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103123 : AngleCell

Subcell 11103123 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103132 : AngleCell

Subcell 11103132 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103133 : AngleCell

Subcell 11103133 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103210 : AngleCell

Subcell 11103210 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103211 : AngleCell

Subcell 11103211 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103300 : AngleCell

Subcell 11103300 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103301 : AngleCell

Subcell 11103301 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103310 : AngleCell

Subcell 11103310 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11103311 : AngleCell

Subcell 11103311 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112022 : AngleCell

Subcell 11112022 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112023 : AngleCell

Subcell 11112023 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112032 : AngleCell

Subcell 11112032 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112033 : AngleCell

Subcell 11112033 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112122 : AngleCell

Subcell 11112122 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112123 : AngleCell

Subcell 11112123 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112132 : AngleCell

Subcell 11112132 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112133 : AngleCell

Subcell 11112133 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112200 : AngleCell

Subcell 11112200 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112201 : AngleCell

Subcell 11112201 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112210 : AngleCell

Subcell 11112210 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112211 : AngleCell

Subcell 11112211 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112300 : AngleCell

Subcell 11112300 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112301 : AngleCell

Subcell 11112301 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112310 : AngleCell

Subcell 11112310 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11112311 : AngleCell

Subcell 11112311 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113022 : AngleCell

Subcell 11113022 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113023 : AngleCell

Subcell 11113023 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113032 : AngleCell

Subcell 11113032 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113033 : AngleCell

Subcell 11113033 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113122 : AngleCell

Subcell 11113122 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113123 : AngleCell

Subcell 11113123 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113132 : AngleCell

Subcell 11113132 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113133 : AngleCell

Subcell 11113133 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113200 : AngleCell

Subcell 11113200 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113201 : AngleCell

Subcell 11113201 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell11113210 : AngleCell

Subcell 11113210 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132010310 : AngleCell

Subcell 111132010310 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132010311 : AngleCell

Subcell 111132010311 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132010312 : AngleCell

Subcell 111132010312 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132010313 : AngleCell

Subcell 111132010313 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011120 : AngleCell

Subcell 111132011120 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011121 : AngleCell

Subcell 111132011121 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011122 : AngleCell

Subcell 111132011122 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011123 : AngleCell

Subcell 111132011123 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011130 : AngleCell

Subcell 111132011130 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011131 : AngleCell

Subcell 111132011131 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011132 : AngleCell

Subcell 111132011132 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011133 : AngleCell

Subcell 111132011133 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011200 : AngleCell

Subcell 111132011200 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011201 : AngleCell

Subcell 111132011201 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011202 : AngleCell

Subcell 111132011202 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011203 : AngleCell

Subcell 111132011203 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011210 : AngleCell

Subcell 111132011210 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011211 : AngleCell

Subcell 111132011211 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011212 : AngleCell

Subcell 111132011212 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011213 : AngleCell

Subcell 111132011213 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011300 : AngleCell

Subcell 111132011300 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011301 : AngleCell

Subcell 111132011301 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011302 : AngleCell

Subcell 111132011302 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011303 : AngleCell

Subcell 111132011303 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011310 : AngleCell

Subcell 111132011310 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011311 : AngleCell

Subcell 111132011311 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011312 : AngleCell

Subcell 111132011312 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011313 : AngleCell

Subcell 111132011313 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011320 : AngleCell

Subcell 111132011320 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011321 : AngleCell

Subcell 111132011321 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011322 : AngleCell

Subcell 111132011322 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011323 : AngleCell

Subcell 111132011323 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011330 : AngleCell

Subcell 111132011330 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011331 : AngleCell

Subcell 111132011331 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011332 : AngleCell

Subcell 111132011332 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132011333 : AngleCell

Subcell 111132011333 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100000 : AngleCell

Subcell 111132100000 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100001 : AngleCell

Subcell 111132100001 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100002 : AngleCell

Subcell 111132100002 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100003 : AngleCell

Subcell 111132100003 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100010 : AngleCell

Subcell 111132100010 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100011 : AngleCell

Subcell 111132100011 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100012 : AngleCell

Subcell 111132100012 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100013 : AngleCell

Subcell 111132100013 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100020 : AngleCell

Subcell 111132100020 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100021 : AngleCell

Subcell 111132100021 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100022 : AngleCell

Subcell 111132100022 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100023 : AngleCell

Subcell 111132100023 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100030 : AngleCell

Subcell 111132100030 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100031 : AngleCell

Subcell 111132100031 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100032 : AngleCell

Subcell 111132100032 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100033 : AngleCell

Subcell 111132100033 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100100 : AngleCell

Subcell 111132100100 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100101 : AngleCell

Subcell 111132100101 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100102 : AngleCell

Subcell 111132100102 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100103 : AngleCell

Subcell 111132100103 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100120 : AngleCell

Subcell 111132100120 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100121 : AngleCell

Subcell 111132100121 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100122 : AngleCell

Subcell 111132100122 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100123 : AngleCell

Subcell 111132100123 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100130 : AngleCell

Subcell 111132100130 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100131 : AngleCell

Subcell 111132100131 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100132 : AngleCell

Subcell 111132100132 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100133 : AngleCell

Subcell 111132100133 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100200 : AngleCell

Subcell 111132100200 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100201 : AngleCell

Subcell 111132100201 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100202 : AngleCell

Subcell 111132100202 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100203 : AngleCell

Subcell 111132100203 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100210 : AngleCell

Subcell 111132100210 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100211 : AngleCell

Subcell 111132100211 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100212 : AngleCell

Subcell 111132100212 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100213 : AngleCell

Subcell 111132100213 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100220 : AngleCell

Subcell 111132100220 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100221 : AngleCell

Subcell 111132100221 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100222 : AngleCell

Subcell 111132100222 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100223 : AngleCell

Subcell 111132100223 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100230 : AngleCell

Subcell 111132100230 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100231 : AngleCell

Subcell 111132100231 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100232 : AngleCell

Subcell 111132100232 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100233 : AngleCell

Subcell 111132100233 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100300 : AngleCell

Subcell 111132100300 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100301 : AngleCell

Subcell 111132100301 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100302 : AngleCell

Subcell 111132100302 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100303 : AngleCell

Subcell 111132100303 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100310 : AngleCell

Subcell 111132100310 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100311 : AngleCell

Subcell 111132100311 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100312 : AngleCell

Subcell 111132100312 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100313 : AngleCell

Subcell 111132100313 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100320 : AngleCell

Subcell 111132100320 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100321 : AngleCell

Subcell 111132100321 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100322 : AngleCell

Subcell 111132100322 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100323 : AngleCell

Subcell 111132100323 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100330 : AngleCell

Subcell 111132100330 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100331 : AngleCell

Subcell 111132100331 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100332 : AngleCell

Subcell 111132100332 of the theta-below 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.CertificateCells37514173c1.thetaBelowCell111132100333 : AngleCell

Subcell 111132100333 of the theta-below 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.CertificateCells00c658e5bf.thetaBelowCell1111 : AngleCell

Subcell 1111 of the theta-below 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.CertificateCells00c658e5bf.thetaBelowCell11113312 : AngleCell

Subcell 11113312 of the theta-below 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.CertificateCells00c658e5bf.thetaBelowCell11113313 : AngleCell

Subcell 11113313 of the theta-below 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.E24KC5TerminalBatchT307200009.

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032110 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032111 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110321333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032200 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032201 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032202 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032203 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032210 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032211 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032212 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032213 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103222 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103223 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032300 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032301 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032302 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032303 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032310 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032311 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032312 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011032313 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103232 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103233 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033000 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033001 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033010 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033011 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110330333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033100 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033101 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033110 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033111 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0110331333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01103313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033200 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033201 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033202 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033203 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033210 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033211 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033212 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033213 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103322 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103323 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033300 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033301 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033302 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033303 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033310 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033311 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033312 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011033313 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103332 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01103333 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01103333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011100 : adaptiveCoverCheck 13 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011101 : adaptiveCoverCheck 13 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011102 : adaptiveCoverCheck 13 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011103 : adaptiveCoverCheck 13 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011110 : adaptiveCoverCheck 13 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011111 : adaptiveCoverCheck 13 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011112 : adaptiveCoverCheck 13 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011113 : adaptiveCoverCheck 13 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111200 : adaptiveCoverCheck 12 (childLL (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111201 : adaptiveCoverCheck 12 (childLH (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112020 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112020 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112021 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112021 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112022 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112022 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112023 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112023 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112030 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112030 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112031 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112031 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112032 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112032 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112033 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112033 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111210 : adaptiveCoverCheck 12 (childLL (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111211 : adaptiveCoverCheck 12 (childLH (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112120 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112120 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112121 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112121 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112122 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112122 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112123 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112123 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112130 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112130 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112131 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112131 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112132 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112132 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112133 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112133 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122000 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122001 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122010 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122011 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111220333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122100 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122101 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122110 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122111 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111221333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122200 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122201 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122202 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122203 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122210 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122211 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122212 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122213 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112222 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112223 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122300 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122301 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122302 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122303 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122310 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122311 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122312 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011122313 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112232 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112233 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123000 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123001 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123010 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123011 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111230333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123100 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123101 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123110 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123111 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231220 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231221 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231222 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231223 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231230 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231231 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231232 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231233 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231320 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231321 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231322 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231323 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231330 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231331 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231332 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111231333 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01112313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123200 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123201 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123202 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123203 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123210 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123211 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123212 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123213 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112322 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112323 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123300 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123301 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123302 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123303 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123310 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123311 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123312 : adaptiveCoverCheck 10 (childHL CertificateCellsb518b98fbe.thetaAboveCell01112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011123313 : adaptiveCoverCheck 10 (childHH CertificateCellsb518b98fbe.thetaAboveCell01112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112332 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01112333 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01112333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111300 : adaptiveCoverCheck 12 (childLL (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111301 : adaptiveCoverCheck 12 (childLH (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113020 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113020 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113021 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113021 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113022 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113022 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113023 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113023 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113030 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113030 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113031 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113031 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113032 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113032 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113033 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113033 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111310 : adaptiveCoverCheck 12 (childLL (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111311 : adaptiveCoverCheck 12 (childLH (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell0111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113120 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113120 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113121 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113121 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113122 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113122 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113123 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113123 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113130 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113130 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113131 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113131 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113132 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113132 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf01113133 : adaptiveCoverCheck 11 CertificateCellsb518b98fbe.thetaAboveCell01113133 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011132000 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01113200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011132001 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01113200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01113200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011132010 : adaptiveCoverCheck 10 (childLL CertificateCellsb518b98fbe.thetaAboveCell01113201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf011132011 : adaptiveCoverCheck 10 (childLH CertificateCellsb518b98fbe.thetaAboveCell01113201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCellsb518b98fbe.thetaAboveCell01113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCellsb518b98fbe.thetaAboveCell01113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCellsb518b98fbe.thetaAboveCell01113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCellsb518b98fbe.thetaAboveCell01113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCellsb518b98fbe.thetaAboveCell01113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCellsb518b98fbe.thetaAboveCell01113202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0111320211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCellsb518b98fbe.thetaAboveCell01113202)) = true

Gerver sofa dependency batch

• KernelOnly.PartE.E24KC6ProofBatchA7de3be3b4ab1789.
• KernelOnly.PartE.E24KC6ProofBatchAad74ad127e30429.

E24KC6 explicit proof-producing certificate batch.

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell00113310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell00113310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell00113310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell00113310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell00113311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell00113311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell00113311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell00113311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell00113312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell00113312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell00113312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell00113312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell00113313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell00113313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell00113313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0011331311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell00113313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell01002202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell01002202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell01002202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell01002202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells37514173c1.thetaAboveCell01002202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells37514173c1.thetaAboveCell01002202)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100220313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells37514173c1.thetaAboveCell01002203)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell01002212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell01002212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells37514173c1.thetaAboveCell01002212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell01002212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell01002212)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell01002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell01002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell01002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100221311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell01002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell01002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell01002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell01002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell01002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells37514173c1.thetaAboveCell01002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells37514173c1.thetaAboveCell01002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells37514173c1.thetaAboveCell01002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100230311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells37514173c1.thetaAboveCell01002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100231133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells37514173c1.thetaAboveCell01003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells37514173c1.thetaAboveCell01003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells37514173c1.thetaAboveCell01003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0100320133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells37514173c1.thetaAboveCell01003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030223 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030232 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030233 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030312 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103031) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030313 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103031) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030320 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030321 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030322 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030323 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030330 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030331 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030332 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111030333 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031202 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103120) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031220 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031221 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031222 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031223 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031230 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031231 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031232 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031233 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031320 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031321 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031322 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031323 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031330 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031331 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031332 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11103133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111031333 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11103133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111032100 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103210) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111032101 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103210) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111032110 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103211) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111032111 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103211) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033000 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103300) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033001 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103300) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033010 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103301) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033011 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103301) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033100 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103310) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033101 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103310) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033110 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11103311) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111033111 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11103311) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120220 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120221 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120222 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120223 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120230 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120231 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120232 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120233 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120320 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120321 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120322 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120323 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120330 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120331 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120332 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111120333 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121220 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121221 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121222 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121223 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121230 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121231 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121232 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121233 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121322 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121323 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121332 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111121333 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122000 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112200) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122001 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112200) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122010 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112201) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122011 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112201) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122100 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112210) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122101 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112210) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122110 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112211) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122111 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112211) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111122113 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112211) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123000 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112300) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123001 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112300) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123002 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112300) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123003 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112300) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123010 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112301) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123011 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112301) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123012 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112301) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123013 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112301) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123100 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112310) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123101 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112310) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123102 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112310) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123103 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112310) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123110 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11112311) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123111 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11112311) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123112 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11112311) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111123113 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11112311) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130222 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130223 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113022) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130232 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130233 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113023) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130322 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130323 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113032) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130332 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111130333 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113033) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131222 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131223 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113122) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131232 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131233 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113123) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131322 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131323 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113132) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131332 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111131333 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113133) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132000 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11113200) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132001 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11113200) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132002 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113200) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132003 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113200) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132010 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11113201) = true

theorem GerverSofa.PartE.cover_subtree_b3391292f833 : adaptiveCoverCheck 8 (childLH (childLH CertificateCells37514173c1.thetaBelowCell11113201)) = true

theorem GerverSofa.PartE.cover_subtree_3e9c61b8ab9c : adaptiveCoverCheck 8 (childHL (childLH CertificateCells37514173c1.thetaBelowCell11113201)) = true

theorem GerverSofa.PartE.cover_subtree_466ff371217d : adaptiveCoverCheck 8 (childHH (childLH CertificateCells37514173c1.thetaBelowCell11113201)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132011 : adaptiveCoverCheck 9 (childLH CertificateCells37514173c1.thetaBelowCell11113201) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132012 : adaptiveCoverCheck 9 (childHL CertificateCells37514173c1.thetaBelowCell11113201) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132013 : adaptiveCoverCheck 9 (childHH CertificateCells37514173c1.thetaBelowCell11113201) = true

theorem GerverSofa.PartE.cover_subtree_7f4f4b92c5ab : adaptiveCoverCheck 8 (childLL (childLL CertificateCells37514173c1.thetaBelowCell11113210)) = true

theorem GerverSofa.PartE.cover_subtree_c689c5c4108b : adaptiveCoverCheck 8 (childLH (childLL CertificateCells37514173c1.thetaBelowCell11113210)) = true

theorem GerverSofa.PartE.cover_subtree_9df392f82d53 : adaptiveCoverCheck 8 (childHL (childLL CertificateCells37514173c1.thetaBelowCell11113210)) = true

theorem GerverSofa.PartE.cover_subtree_f50cdc547dbb : adaptiveCoverCheck 8 (childHH (childLL CertificateCells37514173c1.thetaBelowCell11113210)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111132100 : adaptiveCoverCheck 9 (childLL CertificateCells37514173c1.thetaBelowCell11113210) = true

E24KC6 explicit proof-producing certificate batch.

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111133120 : adaptiveCoverCheck 9 (childLL CertificateCells00c658e5bf.thetaBelowCell11113312) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111133121 : adaptiveCoverCheck 9 (childLH CertificateCells00c658e5bf.thetaBelowCell11113312) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111133130 : adaptiveCoverCheck 9 (childLL CertificateCells00c658e5bf.thetaBelowCell11113313) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf111133131 : adaptiveCoverCheck 9 (childLH CertificateCells00c658e5bf.thetaBelowCell11113313) = true