Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch003.
• GerverSofa.KernelOnly.PartE.Certificates.Batch012.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells976ad3f816.phiAboveCell1111 : AngleCell

Subcell 1111 of the phi-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.CertificateCells83c065d08f.phiBelowCell3221 : AngleCell

Subcell 3221 of the phi-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.CertificateCells83c065d08f.phiBelowCell3223 : AngleCell

Subcell 3223 of the phi-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.CertificateCells83c065d08f.phiBelowCell3230 : AngleCell

Subcell 3230 of the phi-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.CertificateCells83c065d08f.phiBelowCell3231 : AngleCell

Subcell 3231 of the phi-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.CertificateCells9044f599c8.phiBelowCell3231 : AngleCell

Subcell 3231 of the phi-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.CertificateCells9044f599c8.phiBelowCell3232 : AngleCell

Subcell 3232 of the phi-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.CertificateCells9044f599c8.phiBelowCell3233 : AngleCell

Subcell 3233 of the phi-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.CertificateCellse87459d2a7.phiBelowCell3233 : AngleCell

Subcell 3233 of the phi-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.CertificateCellse87459d2a7.phiBelowCell3300 : AngleCell

Subcell 3300 of the phi-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.CertificateCellse87459d2a7.phiBelowCell3301 : AngleCell

Subcell 3301 of the phi-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.CertificateCells5c2e184d25.phiBelowCell3301 : AngleCell

Subcell 3301 of the phi-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.CertificateCells5c2e184d25.phiBelowCell3302 : AngleCell

Subcell 3302 of the phi-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.CertificateCells5c2e184d25.phiBelowCell3303 : AngleCell

Subcell 3303 of the phi-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.CertificateCells32f77991dd.phiBelowCell3303 : AngleCell

Subcell 3303 of the phi-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.CertificateCells32f77991dd.phiBelowCell3310 : AngleCell

Subcell 3310 of the phi-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.CertificateCells32f77991dd.phiBelowCell3312 : AngleCell

Subcell 3312 of the phi-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.CertificateCells6c9e156424.phiBelowCell3313 : AngleCell

Subcell 3313 of the phi-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.CertificateCells6c9e156424.phiBelowCell3320 : AngleCell

Subcell 3320 of the phi-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.CertificateCells613b88d08f.phiBelowCell3320 : AngleCell

Subcell 3320 of the phi-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.CertificateCells14a7ef0a1a.phiBelowCell3320 : AngleCell

Subcell 3320 of the phi-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.CertificateCells756d9e6827.phiBelowCell3321 : AngleCell

Subcell 3321 of the phi-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.CertificateCells9052ca8de4.phiBelowCell3321 : AngleCell

Subcell 3321 of the phi-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.CertificateCells8466e30288.phiBelowCell3321 : AngleCell

Subcell 3321 of the phi-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.CertificateCells960370a0be.phiBelowCell3321 : AngleCell

Subcell 3321 of the phi-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.CertificateCells960370a0be.phiBelowCell3322 : AngleCell

Subcell 3322 of the phi-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.CertificateCellsd434aeb685.phiBelowCell3322 : AngleCell

Subcell 3322 of the phi-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.CertificateCells720ec0d149.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-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.CertificateCells9005545168.phiAboveCell1110 : AngleCell

Subcell 1110 of the phi-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.CertificateCellse586487728.phiAboveCell1110 : AngleCell

Subcell 1110 of the phi-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.CertificateCellsce87a9d03d.phiAboveCell1110 : AngleCell

Subcell 1110 of the phi-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.CertificateCellsce3c5151af.phiAboveCell1110 : AngleCell

Subcell 1110 of the phi-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.CertificateCells7c64a780f8.phiBelowCell3330 : AngleCell

Subcell 3330 of the phi-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.CertificateCells168aeb56e4.thetaAboveCell1010 : AngleCell

Subcell 1010 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.CertificateCells168aeb56e4.thetaAboveCell1011 : AngleCell

Subcell 1011 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.CertificateCells168aeb56e4.thetaAboveCell1012 : AngleCell

Subcell 1012 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.CertificateCells168aeb56e4.thetaAboveCell1013 : AngleCell

Subcell 1013 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.CertificateCells168aeb56e4.thetaAboveCell1020 : AngleCell

Subcell 1020 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.CertificateCells168aeb56e4.thetaAboveCell1021 : AngleCell

Subcell 1021 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.CertificateCells168aeb56e4.thetaAboveCell1022 : AngleCell

Subcell 1022 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.CertificateCells168aeb56e4.thetaAboveCell1023 : AngleCell

Subcell 1023 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.CertificateCells168aeb56e4.thetaAboveCell1030 : AngleCell

Subcell 1030 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.CertificateCells168aeb56e4.thetaAboveCell1031 : AngleCell

Subcell 1031 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.CertificateCells168aeb56e4.thetaAboveCell1032 : AngleCell

Subcell 1032 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.CertificateCells168aeb56e4.thetaAboveCell1033 : AngleCell

Subcell 1033 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.CertificateCells168aeb56e4.thetaAboveCell1100 : AngleCell

Subcell 1100 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.CertificateCells168aeb56e4.thetaAboveCell10103300 : AngleCell

Subcell 10103300 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.CertificateCells168aeb56e4.thetaAboveCell10103301 : AngleCell

Subcell 10103301 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.CertificateCells168aeb56e4.thetaAboveCell10103302 : AngleCell

Subcell 10103302 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.CertificateCells168aeb56e4.thetaAboveCell10103303 : AngleCell

Subcell 10103303 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.CertificateCells168aeb56e4.thetaAboveCell10103310 : AngleCell

Subcell 10103310 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.CertificateCells168aeb56e4.thetaAboveCell10103311 : AngleCell

Subcell 10103311 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.CertificateCells168aeb56e4.thetaAboveCell10103312 : AngleCell

Subcell 10103312 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.CertificateCells168aeb56e4.thetaAboveCell10103313 : AngleCell

Subcell 10103313 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.CertificateCells168aeb56e4.thetaAboveCell10103320 : AngleCell

Subcell 10103320 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.CertificateCells168aeb56e4.thetaAboveCell10103321 : AngleCell

Subcell 10103321 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.CertificateCells168aeb56e4.thetaAboveCell10103322 : AngleCell

Subcell 10103322 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.CertificateCells168aeb56e4.thetaAboveCell10103323 : AngleCell

Subcell 10103323 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.CertificateCells168aeb56e4.thetaAboveCell10103330 : AngleCell

Subcell 10103330 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.CertificateCells168aeb56e4.thetaAboveCell10103331 : AngleCell

Subcell 10103331 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.CertificateCells168aeb56e4.thetaAboveCell10103332 : AngleCell

Subcell 10103332 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.CertificateCells168aeb56e4.thetaAboveCell10103333 : AngleCell

Subcell 10103333 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.CertificateCells168aeb56e4.thetaAboveCell10112200 : AngleCell

Subcell 10112200 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.CertificateCells168aeb56e4.thetaAboveCell10112201 : AngleCell

Subcell 10112201 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.CertificateCells168aeb56e4.thetaAboveCell10112202 : AngleCell

Subcell 10112202 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.CertificateCells168aeb56e4.thetaAboveCell10112203 : AngleCell

Subcell 10112203 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.CertificateCells168aeb56e4.thetaAboveCell10112210 : AngleCell

Subcell 10112210 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.CertificateCells168aeb56e4.thetaAboveCell10112211 : AngleCell

Subcell 10112211 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.CertificateCells168aeb56e4.thetaAboveCell10112212 : AngleCell

Subcell 10112212 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.CertificateCells168aeb56e4.thetaAboveCell10112213 : AngleCell

Subcell 10112213 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.CertificateCells168aeb56e4.thetaAboveCell10112220 : AngleCell

Subcell 10112220 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.CertificateCells168aeb56e4.thetaAboveCell10112221 : AngleCell

Subcell 10112221 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.CertificateCells168aeb56e4.thetaAboveCell10112222 : AngleCell

Subcell 10112222 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.CertificateCells168aeb56e4.thetaAboveCell10112223 : AngleCell

Subcell 10112223 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.CertificateCells168aeb56e4.thetaAboveCell10112230 : AngleCell

Subcell 10112230 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.CertificateCells168aeb56e4.thetaAboveCell10112231 : AngleCell

Subcell 10112231 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.CertificateCells168aeb56e4.thetaAboveCell10112232 : AngleCell

Subcell 10112232 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.CertificateCells168aeb56e4.thetaAboveCell10112233 : AngleCell

Subcell 10112233 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.CertificateCells168aeb56e4.thetaAboveCell10112300 : AngleCell

Subcell 10112300 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.CertificateCells168aeb56e4.thetaAboveCell10112301 : AngleCell

Subcell 10112301 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.CertificateCells168aeb56e4.thetaAboveCell10112302 : AngleCell

Subcell 10112302 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.CertificateCells168aeb56e4.thetaAboveCell10112303 : AngleCell

Subcell 10112303 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.CertificateCells168aeb56e4.thetaAboveCell10112310 : AngleCell

Subcell 10112310 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.CertificateCells168aeb56e4.thetaAboveCell10112311 : AngleCell

Subcell 10112311 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.CertificateCells168aeb56e4.thetaAboveCell10112312 : AngleCell

Subcell 10112312 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.CertificateCells168aeb56e4.thetaAboveCell10112313 : AngleCell

Subcell 10112313 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.CertificateCells168aeb56e4.thetaAboveCell10112320 : AngleCell

Subcell 10112320 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.CertificateCells168aeb56e4.thetaAboveCell10112321 : AngleCell

Subcell 10112321 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.CertificateCells168aeb56e4.thetaAboveCell10112322 : AngleCell

Subcell 10112322 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.CertificateCells168aeb56e4.thetaAboveCell10112323 : AngleCell

Subcell 10112323 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.CertificateCells168aeb56e4.thetaAboveCell10112330 : AngleCell

Subcell 10112330 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.CertificateCells168aeb56e4.thetaAboveCell10112331 : AngleCell

Subcell 10112331 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.CertificateCells168aeb56e4.thetaAboveCell10112332 : AngleCell

Subcell 10112332 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.CertificateCells168aeb56e4.thetaAboveCell10112333 : AngleCell

Subcell 10112333 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.CertificateCells168aeb56e4.thetaAboveCell10113200 : AngleCell

Subcell 10113200 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.CertificateCells168aeb56e4.thetaAboveCell10113201 : AngleCell

Subcell 10113201 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.CertificateCells168aeb56e4.thetaAboveCell10113202 : AngleCell

Subcell 10113202 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.CertificateCells168aeb56e4.thetaAboveCell10113203 : AngleCell

Subcell 10113203 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.CertificateCells168aeb56e4.thetaAboveCell10113210 : AngleCell

Subcell 10113210 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.CertificateCells168aeb56e4.thetaAboveCell10113211 : AngleCell

Subcell 10113211 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.CertificateCells168aeb56e4.thetaAboveCell10113212 : AngleCell

Subcell 10113212 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.CertificateCells168aeb56e4.thetaAboveCell10113213 : AngleCell

Subcell 10113213 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.CertificateCells168aeb56e4.thetaAboveCell10113220 : AngleCell

Subcell 10113220 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.CertificateCells168aeb56e4.thetaAboveCell10113221 : AngleCell

Subcell 10113221 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.CertificateCells168aeb56e4.thetaAboveCell10113222 : AngleCell

Subcell 10113222 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.CertificateCells168aeb56e4.thetaAboveCell10113223 : AngleCell

Subcell 10113223 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.CertificateCells168aeb56e4.thetaAboveCell10113230 : AngleCell

Subcell 10113230 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.CertificateCells168aeb56e4.thetaAboveCell10113231 : AngleCell

Subcell 10113231 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.CertificateCells168aeb56e4.thetaAboveCell10113232 : AngleCell

Subcell 10113232 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.CertificateCells168aeb56e4.thetaAboveCell10113233 : AngleCell

Subcell 10113233 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.CertificateCells168aeb56e4.thetaAboveCell10113300 : AngleCell

Subcell 10113300 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.CertificateCells168aeb56e4.thetaAboveCell10113301 : AngleCell

Subcell 10113301 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.CertificateCells168aeb56e4.thetaAboveCell10113302 : AngleCell

Subcell 10113302 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.CertificateCells168aeb56e4.thetaAboveCell10113303 : AngleCell

Subcell 10113303 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.CertificateCells168aeb56e4.thetaAboveCell10113310 : AngleCell

Subcell 10113310 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.CertificateCells168aeb56e4.thetaAboveCell10113311 : AngleCell

Subcell 10113311 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.CertificateCells168aeb56e4.thetaAboveCell10113312 : AngleCell

Subcell 10113312 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.CertificateCells168aeb56e4.thetaAboveCell10113313 : AngleCell

Subcell 10113313 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.CertificateCells168aeb56e4.thetaAboveCell10113320 : AngleCell

Subcell 10113320 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.CertificateCells168aeb56e4.thetaAboveCell10113321 : AngleCell

Subcell 10113321 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.CertificateCells168aeb56e4.thetaAboveCell10113322 : AngleCell

Subcell 10113322 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.CertificateCells168aeb56e4.thetaAboveCell10113323 : AngleCell

Subcell 10113323 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.CertificateCells168aeb56e4.thetaAboveCell10113330 : AngleCell

Subcell 10113330 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.CertificateCells168aeb56e4.thetaAboveCell10113331 : AngleCell

Subcell 10113331 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.CertificateCells168aeb56e4.thetaAboveCell10113332 : AngleCell

Subcell 10113332 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.CertificateCells168aeb56e4.thetaAboveCell10113333 : AngleCell

Subcell 10113333 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.CertificateCells168aeb56e4.thetaAboveCell11002200 : AngleCell

Subcell 11002200 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.CertificateCells168aeb56e4.thetaAboveCell11002201 : AngleCell

Subcell 11002201 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.CertificateCells168aeb56e4.thetaAboveCell11002202 : AngleCell

Subcell 11002202 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.CertificateCells168aeb56e4.thetaAboveCell11002203 : AngleCell

Subcell 11002203 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.CertificateCells168aeb56e4.thetaAboveCell11002210 : AngleCell

Subcell 11002210 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.CertificateCells168aeb56e4.thetaAboveCell11002211 : AngleCell

Subcell 11002211 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.CertificateCells168aeb56e4.thetaAboveCell11002212 : AngleCell

Subcell 11002212 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.CertificateCells168aeb56e4.thetaAboveCell11002213 : AngleCell

Subcell 11002213 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.CertificateCells168aeb56e4.thetaAboveCell11002220 : AngleCell

Subcell 11002220 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.CertificateCells168aeb56e4.thetaAboveCell11002221 : AngleCell

Subcell 11002221 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.CertificateCells168aeb56e4.thetaAboveCell11002222 : AngleCell

Subcell 11002222 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.CertificateCells168aeb56e4.thetaAboveCell11002223 : AngleCell

Subcell 11002223 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.CertificateCells168aeb56e4.thetaAboveCell11002230 : AngleCell

Subcell 11002230 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.CertificateCells168aeb56e4.thetaAboveCell11002231 : AngleCell

Subcell 11002231 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.CertificateCells168aeb56e4.thetaAboveCell11002232 : AngleCell

Subcell 11002232 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.CertificateCells168aeb56e4.thetaAboveCell11002233 : AngleCell

Subcell 11002233 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.CertificateCells168aeb56e4.thetaAboveCell11002300 : AngleCell

Subcell 11002300 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.CertificateCells168aeb56e4.thetaAboveCell11002301 : AngleCell

Subcell 11002301 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.CertificateCells168aeb56e4.thetaAboveCell11002302 : AngleCell

Subcell 11002302 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.CertificateCells168aeb56e4.thetaAboveCell11002303 : AngleCell

Subcell 11002303 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.CertificateCells168aeb56e4.thetaAboveCell11002310 : AngleCell

Subcell 11002310 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.CertificateCells168aeb56e4.thetaAboveCell11002311 : AngleCell

Subcell 11002311 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.CertificateCells168aeb56e4.thetaAboveCell11002312 : AngleCell

Subcell 11002312 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.CertificateCells168aeb56e4.thetaAboveCell11002313 : AngleCell

Subcell 11002313 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.CertificateCells168aeb56e4.thetaAboveCell11002320 : AngleCell

Subcell 11002320 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.CertificateCells168aeb56e4.thetaAboveCell11002321 : AngleCell

Subcell 11002321 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.CertificateCells168aeb56e4.thetaAboveCell11002322 : AngleCell

Subcell 11002322 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.CertificateCells168aeb56e4.thetaAboveCell11002323 : AngleCell

Subcell 11002323 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.CertificateCells168aeb56e4.thetaAboveCell11002330 : AngleCell

Subcell 11002330 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.CertificateCells168aeb56e4.thetaAboveCell11002331 : AngleCell

Subcell 11002331 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.CertificateCells168aeb56e4.thetaAboveCell11002332 : AngleCell

Subcell 11002332 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.CertificateCells168aeb56e4.thetaAboveCell11002333 : AngleCell

Subcell 11002333 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.CertificateCells168aeb56e4.thetaAboveCell11003200 : AngleCell

Subcell 11003200 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.CertificateCells168aeb56e4.thetaAboveCell11003201 : AngleCell

Subcell 11003201 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.CertificateCells168aeb56e4.thetaAboveCell11003202 : AngleCell

Subcell 11003202 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.CertificateCells168aeb56e4.thetaAboveCell11003203 : AngleCell

Subcell 11003203 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.CertificateCells168aeb56e4.thetaAboveCell11003210 : AngleCell

Subcell 11003210 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.CertificateCells168aeb56e4.thetaAboveCell11003211 : AngleCell

Subcell 11003211 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.CertificateCells168aeb56e4.thetaAboveCell11003212 : AngleCell

Subcell 11003212 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.CertificateCells168aeb56e4.thetaAboveCell11003213 : AngleCell

Subcell 11003213 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.CertificateCells168aeb56e4.thetaAboveCell11003220 : AngleCell

Subcell 11003220 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.CertificateCells168aeb56e4.thetaAboveCell11003221 : AngleCell

Subcell 11003221 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.CertificateCells168aeb56e4.thetaAboveCell11003222 : AngleCell

Subcell 11003222 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.CertificateCells168aeb56e4.thetaAboveCell11003223 : AngleCell

Subcell 11003223 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.CertificateCells168aeb56e4.thetaAboveCell11003230 : AngleCell

Subcell 11003230 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.CertificateCells168aeb56e4.thetaAboveCell11003231 : AngleCell

Subcell 11003231 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.CertificateCells168aeb56e4.thetaAboveCell11003232 : AngleCell

Subcell 11003232 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.CertificateCells168aeb56e4.thetaAboveCell11003233 : AngleCell

Subcell 11003233 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.CertificateCells168aeb56e4.thetaAboveCell11003300 : AngleCell

Subcell 11003300 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.CertificateCells168aeb56e4.thetaAboveCell11003301 : AngleCell

Subcell 11003301 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.CertificateCells168aeb56e4.thetaAboveCell11003302 : AngleCell

Subcell 11003302 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.CertificateCells168aeb56e4.thetaAboveCell11003303 : AngleCell

Subcell 11003303 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.CertificateCells168aeb56e4.thetaAboveCell11003310 : AngleCell

Subcell 11003310 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.CertificateCells168aeb56e4.thetaAboveCell11003311 : AngleCell

Subcell 11003311 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.CertificateCells168aeb56e4.thetaAboveCell11003312 : AngleCell

Subcell 11003312 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.CertificateCells168aeb56e4.thetaAboveCell11003313 : AngleCell

Subcell 11003313 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.CertificateCells168aeb56e4.thetaAboveCell11003320 : AngleCell

Subcell 11003320 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.CertificateCells168aeb56e4.thetaAboveCell11003321 : AngleCell

Subcell 11003321 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.CertificateCells168aeb56e4.thetaAboveCell11003322 : AngleCell

Subcell 11003322 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.CertificateCells168aeb56e4.thetaAboveCell11003323 : AngleCell

Subcell 11003323 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.CertificateCells168aeb56e4.thetaAboveCell11003330 : AngleCell

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

Equations

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

Gerver sofa dependency batch

• KernelOnly.PartE.E24KC5FrontierBatchF3200227.
• KernelOnly.PartE.E24KC5FrontierBatchF4000228.
• KernelOnly.PartE.E24KC5FrontierBatchF4800229.
• KernelOnly.PartE.E24KC5FrontierBatchF5600230.
• KernelOnly.PartE.E24KC5FrontierBatchF6400231.
• KernelOnly.PartE.E24KC5FrontierBatchF7200232.
• KernelOnly.PartE.E24KC5FrontierBatchF80LL00235.
• KernelOnly.PartE.E24KC5FrontierBatchF80LRL00237.
• KernelOnly.PartE.E24KC5FrontierBatchF80LRR00238.
• KernelOnly.PartE.E24KC5FrontierBatchF80RLR00247.
• KernelOnly.PartE.E24KC5FrontierBatchF80RRL00249.
• KernelOnly.PartE.E24KC5FrontierBatchF80RRR00250.
• KernelOnly.PartE.E24KC5FrontierBatchF88LL00253.
• KernelOnly.PartE.E24KC5FrontierBatchF88LRR00261.
• KernelOnly.PartE.E24KC5FrontierBatchF88RRL00287.
• KernelOnly.PartE.E24KC5FrontierBatchF8LLR00192.
• KernelOnly.PartE.E24KC5FrontierBatchF8LRL00194.
• KernelOnly.PartE.E24KC5FrontierBatchF8RLR00209.
• KernelOnly.PartE.E24KC5FrontierBatchF8RR00210.
• KernelOnly.PartE.E24KC5FrontierBatchF96LLR00463.

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111101 : adaptiveCoverCheck 9 (childLH (childLL (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111102 : adaptiveCoverCheck 9 (childHL (childLL (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111103 : adaptiveCoverCheck 9 (childHH (childLL (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111110 : adaptiveCoverCheck 9 (childLL (childLH (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111111 : adaptiveCoverCheck 9 (childLH (childLH (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111112 : adaptiveCoverCheck 9 (childHL (childLH (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111113 : adaptiveCoverCheck 9 (childHH (childLH (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111131 : adaptiveCoverCheck 9 (childLH (childHH (childLH CertificateCells976ad3f816.phiAboveCell1111))) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32211 : adaptiveCoverCheck 9 (childLH CertificateCells83c065d08f.phiBelowCell3221) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32213 : adaptiveCoverCheck 9 (childHH CertificateCells83c065d08f.phiBelowCell3221) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32231 : adaptiveCoverCheck 9 (childLH CertificateCells83c065d08f.phiBelowCell3223) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32300 : adaptiveCoverCheck 9 (childLL CertificateCells83c065d08f.phiBelowCell3230) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32301 : adaptiveCoverCheck 9 (childLH CertificateCells83c065d08f.phiBelowCell3230) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32302 : adaptiveCoverCheck 9 (childHL CertificateCells83c065d08f.phiBelowCell3230) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32303 : adaptiveCoverCheck 9 (childHH CertificateCells83c065d08f.phiBelowCell3230) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32310 : adaptiveCoverCheck 9 (childLL CertificateCells83c065d08f.phiBelowCell3231) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32311 : adaptiveCoverCheck 9 (childLH CertificateCells9044f599c8.phiBelowCell3231) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32312 : adaptiveCoverCheck 9 (childHL CertificateCells9044f599c8.phiBelowCell3231) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32313 : adaptiveCoverCheck 9 (childHH CertificateCells9044f599c8.phiBelowCell3231) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32320 : adaptiveCoverCheck 9 (childLL CertificateCells9044f599c8.phiBelowCell3232) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32321 : adaptiveCoverCheck 9 (childLH CertificateCells9044f599c8.phiBelowCell3232) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32322 : adaptiveCoverCheck 9 (childHL CertificateCells9044f599c8.phiBelowCell3232) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32323 : adaptiveCoverCheck 9 (childHH CertificateCells9044f599c8.phiBelowCell3232) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32330 : adaptiveCoverCheck 9 (childLL CertificateCells9044f599c8.phiBelowCell3233) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32331 : adaptiveCoverCheck 9 (childLH CertificateCellse87459d2a7.phiBelowCell3233) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32332 : adaptiveCoverCheck 9 (childHL CertificateCellse87459d2a7.phiBelowCell3233) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32333 : adaptiveCoverCheck 9 (childHH CertificateCellse87459d2a7.phiBelowCell3233) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33000 : adaptiveCoverCheck 9 (childLL CertificateCellse87459d2a7.phiBelowCell3300) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33001 : adaptiveCoverCheck 9 (childLH CertificateCellse87459d2a7.phiBelowCell3300) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33002 : adaptiveCoverCheck 9 (childHL CertificateCellse87459d2a7.phiBelowCell3300) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33003 : adaptiveCoverCheck 9 (childHH CertificateCellse87459d2a7.phiBelowCell3300) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33010 : adaptiveCoverCheck 9 (childLL CertificateCellse87459d2a7.phiBelowCell3301) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33011 : adaptiveCoverCheck 9 (childLH CertificateCells5c2e184d25.phiBelowCell3301) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33012 : adaptiveCoverCheck 9 (childHL CertificateCells5c2e184d25.phiBelowCell3301) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33013 : adaptiveCoverCheck 9 (childHH CertificateCells5c2e184d25.phiBelowCell3301) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33020 : adaptiveCoverCheck 9 (childLL CertificateCells5c2e184d25.phiBelowCell3302) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33021 : adaptiveCoverCheck 9 (childLH CertificateCells5c2e184d25.phiBelowCell3302) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33022 : adaptiveCoverCheck 9 (childHL CertificateCells5c2e184d25.phiBelowCell3302) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33023 : adaptiveCoverCheck 9 (childHH CertificateCells5c2e184d25.phiBelowCell3302) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33030 : adaptiveCoverCheck 9 (childLL CertificateCells5c2e184d25.phiBelowCell3303) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33031 : adaptiveCoverCheck 9 (childLH CertificateCells32f77991dd.phiBelowCell3303) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33032 : adaptiveCoverCheck 9 (childHL CertificateCells32f77991dd.phiBelowCell3303) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33033 : adaptiveCoverCheck 9 (childHH CertificateCells32f77991dd.phiBelowCell3303) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33102 : adaptiveCoverCheck 9 (childHL CertificateCells32f77991dd.phiBelowCell3310) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33120 : adaptiveCoverCheck 9 (childLL CertificateCells32f77991dd.phiBelowCell3312) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33121 : adaptiveCoverCheck 9 (childLH CertificateCells32f77991dd.phiBelowCell3312) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33122 : adaptiveCoverCheck 9 (childHL CertificateCells32f77991dd.phiBelowCell3312) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33123 : adaptiveCoverCheck 9 (childHH CertificateCells32f77991dd.phiBelowCell3312) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33132 : adaptiveCoverCheck 9 (childHL CertificateCells6c9e156424.phiBelowCell3313) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33200 : adaptiveCoverCheck 9 (childLL CertificateCells6c9e156424.phiBelowCell3320) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33201 : adaptiveCoverCheck 9 (childLH CertificateCells613b88d08f.phiBelowCell3320) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33202 : adaptiveCoverCheck 9 (childHL CertificateCells14a7ef0a1a.phiBelowCell3320) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33210 : adaptiveCoverCheck 9 (childLL CertificateCells756d9e6827.phiBelowCell3321) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33211 : adaptiveCoverCheck 9 (childLH CertificateCells9052ca8de4.phiBelowCell3321) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33212 : adaptiveCoverCheck 9 (childHL CertificateCells8466e30288.phiBelowCell3321) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33213 : adaptiveCoverCheck 9 (childHH CertificateCells960370a0be.phiBelowCell3321) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33220 : adaptiveCoverCheck 9 (childLL CertificateCells960370a0be.phiBelowCell3322) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33222 : adaptiveCoverCheck 9 (childHL CertificateCellsd434aeb685.phiBelowCell3322) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33231 : adaptiveCoverCheck 9 (childLH CertificateCells720ec0d149.phiBelowCell3323) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110002 : adaptiveCoverCheck 9 (childHL (childLL (childLL CertificateCells9005545168.phiAboveCell1110))) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110003 : adaptiveCoverCheck 9 (childHH (childLL (childLL CertificateCellse586487728.phiAboveCell1110))) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110012 : adaptiveCoverCheck 9 (childHL (childLH (childLL CertificateCellsce87a9d03d.phiAboveCell1110))) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110013 : adaptiveCoverCheck 9 (childHH (childLH (childLL CertificateCellsce3c5151af.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110100 : adaptiveCoverCheck 9 (childLL (childLL (childLH CertificateCellsce3c5151af.phiAboveCell1110))) = true

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33300 : adaptiveCoverCheck 9 (childLL CertificateCells7c64a780f8.phiBelowCell3330) = true

Gerver sofa dependency batch

• KernelOnly.PartE.E24KC5TerminalBatchT512000013.

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033002 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033003 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033010 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033011 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033012 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033013 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1010330200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell10103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1010330201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell10103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1010330202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells168aeb56e4.thetaAboveCell10103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1010330203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells168aeb56e4.thetaAboveCell10103302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033100 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033101 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033102 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033103 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033110 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033111 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033112 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033113 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10103322 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10103322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10103323 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10103323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101033313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10103331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10103332 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10103332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10103333 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10103333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101100 : adaptiveCoverCheck 13 (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101101 : adaptiveCoverCheck 13 (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101102 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101103 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101110 : adaptiveCoverCheck 13 (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101111 : adaptiveCoverCheck 13 (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101112 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101113 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells168aeb56e4.thetaAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011200 : adaptiveCoverCheck 12 (childLL (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011201 : adaptiveCoverCheck 12 (childLH (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011202 : adaptiveCoverCheck 12 (childHL (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011203 : adaptiveCoverCheck 12 (childHH (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011210 : adaptiveCoverCheck 12 (childLL (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011211 : adaptiveCoverCheck 12 (childLH (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011212 : adaptiveCoverCheck 12 (childHL (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011213 : adaptiveCoverCheck 12 (childHH (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122000 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122001 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122002 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122003 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122010 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122011 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122012 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122013 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122100 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122101 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122102 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122103 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122110 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122111 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122112 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122113 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112222 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112223 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101122313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112232 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112233 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123000 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123001 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123002 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123003 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123010 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123011 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123012 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123013 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123100 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123101 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123102 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123103 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123110 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123111 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123112 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123113 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112322 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112323 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101123313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112332 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10112333 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10112333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011300 : adaptiveCoverCheck 12 (childLL (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011301 : adaptiveCoverCheck 12 (childLH (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011302 : adaptiveCoverCheck 12 (childHL (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011303 : adaptiveCoverCheck 12 (childHH (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011310 : adaptiveCoverCheck 12 (childLL (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011311 : adaptiveCoverCheck 12 (childLH (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011312 : adaptiveCoverCheck 12 (childHL (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1011313 : adaptiveCoverCheck 12 (childHH (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132000 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132001 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132002 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132003 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113200) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132010 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132011 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132012 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132013 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113201) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132100 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132101 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132102 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132103 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113210) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132110 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132111 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132112 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132113 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113211) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113222 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113223 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101132313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113232 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113233 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133000 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133001 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133002 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133003 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113300) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133010 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133011 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133012 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133013 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113301) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133100 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133101 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133102 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133103 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113310) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133110 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133111 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133112 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133113 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113311) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113322 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113323 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell10113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell10113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell10113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101133313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell10113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113332 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10113333 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell10113333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012000 : adaptiveCoverCheck 12 (childLL (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012001 : adaptiveCoverCheck 12 (childLH (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012002 : adaptiveCoverCheck 12 (childHL (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012003 : adaptiveCoverCheck 12 (childHH (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012010 : adaptiveCoverCheck 12 (childLL (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012011 : adaptiveCoverCheck 12 (childLH (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012012 : adaptiveCoverCheck 12 (childHL (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012013 : adaptiveCoverCheck 12 (childHH (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101202 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells168aeb56e4.thetaAboveCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101203 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells168aeb56e4.thetaAboveCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012100 : adaptiveCoverCheck 12 (childLL (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012101 : adaptiveCoverCheck 12 (childLH (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012102 : adaptiveCoverCheck 12 (childHL (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012103 : adaptiveCoverCheck 12 (childHH (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012110 : adaptiveCoverCheck 12 (childLL (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012111 : adaptiveCoverCheck 12 (childLH (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012112 : adaptiveCoverCheck 12 (childHL (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1012113 : adaptiveCoverCheck 12 (childHH (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1012))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101212 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells168aeb56e4.thetaAboveCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101213 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells168aeb56e4.thetaAboveCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10122 : adaptiveCoverCheck 14 (childHL CertificateCells168aeb56e4.thetaAboveCell1012) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10123 : adaptiveCoverCheck 14 (childHH CertificateCells168aeb56e4.thetaAboveCell1012) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013000 : adaptiveCoverCheck 12 (childLL (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013001 : adaptiveCoverCheck 12 (childLH (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013002 : adaptiveCoverCheck 12 (childHL (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013003 : adaptiveCoverCheck 12 (childHH (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013010 : adaptiveCoverCheck 12 (childLL (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013011 : adaptiveCoverCheck 12 (childLH (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013012 : adaptiveCoverCheck 12 (childHL (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013013 : adaptiveCoverCheck 12 (childHH (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101302 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells168aeb56e4.thetaAboveCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101303 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells168aeb56e4.thetaAboveCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013100 : adaptiveCoverCheck 12 (childLL (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013101 : adaptiveCoverCheck 12 (childLH (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013102 : adaptiveCoverCheck 12 (childHL (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013103 : adaptiveCoverCheck 12 (childHH (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013110 : adaptiveCoverCheck 12 (childLL (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013111 : adaptiveCoverCheck 12 (childLH (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013112 : adaptiveCoverCheck 12 (childHL (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1013113 : adaptiveCoverCheck 12 (childHH (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1013))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101312 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells168aeb56e4.thetaAboveCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf101313 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells168aeb56e4.thetaAboveCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10132 : adaptiveCoverCheck 14 (childHL CertificateCells168aeb56e4.thetaAboveCell1013) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf10133 : adaptiveCoverCheck 14 (childHH CertificateCells168aeb56e4.thetaAboveCell1013) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1020 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1020 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1021 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1021 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1022 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1022 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1023 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1023 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1030 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1030 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1031 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1031 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1032 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1032 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1033 : adaptiveCoverCheck 15 CertificateCells168aeb56e4.thetaAboveCell1033 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110000 : adaptiveCoverCheck 13 (childLL (childLL CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110001 : adaptiveCoverCheck 13 (childLH (childLL CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110002 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110003 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110010 : adaptiveCoverCheck 13 (childLL (childLH CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110011 : adaptiveCoverCheck 13 (childLH (childLH CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110012 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110013 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells168aeb56e4.thetaAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100200 : adaptiveCoverCheck 12 (childLL (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100201 : adaptiveCoverCheck 12 (childLH (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100202 : adaptiveCoverCheck 12 (childHL (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100203 : adaptiveCoverCheck 12 (childHH (childLL (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100210 : adaptiveCoverCheck 12 (childLL (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100211 : adaptiveCoverCheck 12 (childLH (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100212 : adaptiveCoverCheck 12 (childHL (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100213 : adaptiveCoverCheck 12 (childHH (childLH (childHL CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002200 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002200 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002201 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002201 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002210 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002210 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002211 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002211 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002222 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002223 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110022313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002232 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002233 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002300 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002300 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002301 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002301 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002310 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002310 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002311 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002311 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002322 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002323 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11002331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11002331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11002331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110023313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11002331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002332 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11002333 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11002333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100300 : adaptiveCoverCheck 12 (childLL (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100301 : adaptiveCoverCheck 12 (childLH (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100302 : adaptiveCoverCheck 12 (childHL (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100303 : adaptiveCoverCheck 12 (childHH (childLL (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100310 : adaptiveCoverCheck 12 (childLL (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100311 : adaptiveCoverCheck 12 (childLH (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100312 : adaptiveCoverCheck 12 (childHL (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1100313 : adaptiveCoverCheck 12 (childHH (childLH (childHH CertificateCells168aeb56e4.thetaAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003200 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003200 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003201 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003201 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003210 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003210 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003211 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003211 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003222 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003223 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032301 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032302 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032303 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032310 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032311 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032312 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110032313 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003232 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003233 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003300 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003300 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003301 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003301 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033020 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033021 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033022 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033023 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033030 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033031 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033032 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033033 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003310 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003310 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003311 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003311 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033120 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033121 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033122 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033123 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033130 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033131 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033132 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033133 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033200 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033201 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033202 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033203 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033210 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033211 : adaptiveCoverCheck 10 (childLH CertificateCells168aeb56e4.thetaAboveCell11003321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033212 : adaptiveCoverCheck 10 (childHL CertificateCells168aeb56e4.thetaAboveCell11003321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033213 : adaptiveCoverCheck 10 (childHH CertificateCells168aeb56e4.thetaAboveCell11003321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003322 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11003323 : adaptiveCoverCheck 11 CertificateCells168aeb56e4.thetaAboveCell11003323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf110033300 : adaptiveCoverCheck 10 (childLL CertificateCells168aeb56e4.thetaAboveCell11003330) = true