Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch015.
• GerverSofa.KernelOnly.PartE.Certificates.Batch019.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell1133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell0133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell1022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11112331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11112332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11112333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113200 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113201 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113202 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113203 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113210 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113211 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113212 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113213 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113300 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113301 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113302 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113303 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113310 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113311 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113312 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113313 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaAboveCell11113333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2f4f8ea4fc.thetaBelowCell10113133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell0000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell00002210 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell00002211 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell00002300 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022103133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022110333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022111333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022112133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000022113133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023000333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2d2385ed48.thetaAboveCell000023001333 : AngleCell

Subcell 000023001333 of the 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.E24KC5TerminalBatchT614400015.

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123311 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123312 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123313 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11112331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123320 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11112332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123321 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11112332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123322 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11112332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123323 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11112332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123330 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11112333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123331 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11112333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123332 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11112333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111123333 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11112333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111300 : adaptiveCoverCheck 12 (childLL (childLL (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111301 : adaptiveCoverCheck 12 (childLH (childLL (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111302 : adaptiveCoverCheck 12 (childHL (childLL (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111303 : adaptiveCoverCheck 12 (childHH (childLL (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111310 : adaptiveCoverCheck 12 (childLL (childLH (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111311 : adaptiveCoverCheck 12 (childLH (childLH (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111312 : adaptiveCoverCheck 12 (childHL (childLH (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1111313 : adaptiveCoverCheck 12 (childHH (childLH (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113200 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113200 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113201 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113201 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132020 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132021 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132022 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132023 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132030 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132031 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132032 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132033 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113210 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113210 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113211 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113211 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132120 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132121 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132122 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132123 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132130 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132131 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132132 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132133 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132200 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132201 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132202 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132203 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113220) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132210 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132211 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132212 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132213 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113221) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132220 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113222) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132221 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113222) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132222 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113222) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132223 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113222) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132230 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113223) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132231 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113223) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132232 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113223) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132233 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113223) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132300 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132301 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132302 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132303 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113230) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132310 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132311 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132312 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132313 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113231) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132320 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113232) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132321 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113232) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132322 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113232) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132323 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113232) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132330 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113233) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132331 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113233) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132332 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113233) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111132333 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113233) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113300 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113300 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113301 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113301 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133020 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133021 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133022 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133023 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133030 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133031 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133032 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133033 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113310 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113310 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11113311 : adaptiveCoverCheck 11 CertificateCells2f4f8ea4fc.thetaAboveCell11113311 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133120 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133121 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133122 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133123 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133130 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133131 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133132 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133133 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133200 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133201 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133202 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133203 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113320) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133210 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133211 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133212 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133213 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113321) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133220 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113322) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133221 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113322) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133222 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113322) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133223 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113322) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133230 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113323) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133231 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113323) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133232 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113323) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133233 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113323) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133300 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133301 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133302 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133303 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113330) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133310 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133311 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133312 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133313 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113331) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133320 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133321 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133322 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133323 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113332) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133330 : adaptiveCoverCheck 10 (childLL CertificateCells2f4f8ea4fc.thetaAboveCell11113333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133331 : adaptiveCoverCheck 10 (childLH CertificateCells2f4f8ea4fc.thetaAboveCell11113333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133332 : adaptiveCoverCheck 10 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell11113333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111133333 : adaptiveCoverCheck 10 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell11113333) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112000 : adaptiveCoverCheck 12 (childLL (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112001 : adaptiveCoverCheck 12 (childLH (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112002 : adaptiveCoverCheck 12 (childHL (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112003 : adaptiveCoverCheck 12 (childHH (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112010 : adaptiveCoverCheck 12 (childLL (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112011 : adaptiveCoverCheck 12 (childLH (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112012 : adaptiveCoverCheck 12 (childHL (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112013 : adaptiveCoverCheck 12 (childHH (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111202 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111203 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1112)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112100 : adaptiveCoverCheck 12 (childLL (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112101 : adaptiveCoverCheck 12 (childLH (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112102 : adaptiveCoverCheck 12 (childHL (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112103 : adaptiveCoverCheck 12 (childHH (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112110 : adaptiveCoverCheck 12 (childLL (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112111 : adaptiveCoverCheck 12 (childLH (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112112 : adaptiveCoverCheck 12 (childHL (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1112113 : adaptiveCoverCheck 12 (childHH (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111212 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111213 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1112)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11122 : adaptiveCoverCheck 14 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell1112) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11123 : adaptiveCoverCheck 14 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1112) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113000 : adaptiveCoverCheck 12 (childLL (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113001 : adaptiveCoverCheck 12 (childLH (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113002 : adaptiveCoverCheck 12 (childHL (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113003 : adaptiveCoverCheck 12 (childHH (childLL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113010 : adaptiveCoverCheck 12 (childLL (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113011 : adaptiveCoverCheck 12 (childLH (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113012 : adaptiveCoverCheck 12 (childHL (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113013 : adaptiveCoverCheck 12 (childHH (childLH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111302 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111303 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells2f4f8ea4fc.thetaAboveCell1113)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113100 : adaptiveCoverCheck 12 (childLL (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113101 : adaptiveCoverCheck 12 (childLH (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113102 : adaptiveCoverCheck 12 (childHL (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113103 : adaptiveCoverCheck 12 (childHH (childLL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113110 : adaptiveCoverCheck 12 (childLL (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113111 : adaptiveCoverCheck 12 (childLH (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113112 : adaptiveCoverCheck 12 (childHL (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1113113 : adaptiveCoverCheck 12 (childHH (childLH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111312 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf111313 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells2f4f8ea4fc.thetaAboveCell1113)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11132 : adaptiveCoverCheck 14 (childHL CertificateCells2f4f8ea4fc.thetaAboveCell1113) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf11133 : adaptiveCoverCheck 14 (childHH CertificateCells2f4f8ea4fc.thetaAboveCell1113) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1120 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1120 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1121 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1121 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1122 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1122 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1123 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1123 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1130 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1130 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1131 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1131 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1132 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1132 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf1133 : adaptiveCoverCheck 15 CertificateCells2f4f8ea4fc.thetaAboveCell1133 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf120 : adaptiveCoverCheck 16 (childLL (childHL (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf121 : adaptiveCoverCheck 16 (childLH (childHL (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf122 : adaptiveCoverCheck 16 (childHL (childHL (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf123 : adaptiveCoverCheck 16 (childHH (childHL (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf130 : adaptiveCoverCheck 16 (childLL (childHH (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf131 : adaptiveCoverCheck 16 (childLH (childHH (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf132 : adaptiveCoverCheck 16 (childHL (childHH (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf133 : adaptiveCoverCheck 16 (childHH (childHH (childLH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf200 : adaptiveCoverCheck 16 (childLL (childLL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf201 : adaptiveCoverCheck 16 (childLH (childLL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf202 : adaptiveCoverCheck 16 (childHL (childLL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf203 : adaptiveCoverCheck 16 (childHH (childLL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf210 : adaptiveCoverCheck 16 (childLL (childLH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf211 : adaptiveCoverCheck 16 (childLH (childLH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf212 : adaptiveCoverCheck 16 (childHL (childLH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf213 : adaptiveCoverCheck 16 (childHH (childLH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf220 : adaptiveCoverCheck 16 (childLL (childHL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf221 : adaptiveCoverCheck 16 (childLH (childHL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf222 : adaptiveCoverCheck 16 (childHL (childHL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf223 : adaptiveCoverCheck 16 (childHH (childHL (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf230 : adaptiveCoverCheck 16 (childLL (childHH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf231 : adaptiveCoverCheck 16 (childLH (childHH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf232 : adaptiveCoverCheck 16 (childHL (childHH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf233 : adaptiveCoverCheck 16 (childHH (childHH (childHL e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf300 : adaptiveCoverCheck 16 (childLL (childLL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf301 : adaptiveCoverCheck 16 (childLH (childLL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf302 : adaptiveCoverCheck 16 (childHL (childLL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf303 : adaptiveCoverCheck 16 (childHH (childLL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf310 : adaptiveCoverCheck 16 (childLL (childLH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf311 : adaptiveCoverCheck 16 (childLH (childLH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf312 : adaptiveCoverCheck 16 (childHL (childLH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf313 : adaptiveCoverCheck 16 (childHH (childLH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf320 : adaptiveCoverCheck 16 (childLL (childHL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf321 : adaptiveCoverCheck 16 (childLH (childHL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf322 : adaptiveCoverCheck 16 (childHL (childHL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf323 : adaptiveCoverCheck 16 (childHH (childHL (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf330 : adaptiveCoverCheck 16 (childLL (childHH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf331 : adaptiveCoverCheck 16 (childLH (childHH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf332 : adaptiveCoverCheck 16 (childHL (childHH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf333 : adaptiveCoverCheck 16 (childHH (childHH (childHH e24ThetaAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0000 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0000 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0001 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0001 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0002 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0002 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00030 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00031 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00032 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00033 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00100 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0010) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00101 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0010) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00102 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0010) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00103 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0010) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00110 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0011) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00111 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0011) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00112 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0011) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00113 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0011) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00120 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0012) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00121 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0012) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00122 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0012) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00123 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0012) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00130 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0013) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00131 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0013) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00132 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0013) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf00133 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0013) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf002 : adaptiveCoverCheck 15 (childHL (childLL (childLL e24ThetaBelowRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0030 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0030 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0031 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0031 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0032 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0032 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0033 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0033 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01000 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0100) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01001 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0100) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01002 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0100) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01003 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0100) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01010 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0101) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01011 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0101) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01012 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0101) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf010130 : adaptiveCoverCheck 12 (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0101)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf010131 : adaptiveCoverCheck 12 (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0101)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf010132 : adaptiveCoverCheck 12 (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0101)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf010133 : adaptiveCoverCheck 12 (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0101)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01020 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0102) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01021 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0102) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01022 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0102) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01023 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0102) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01030 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0103) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01031 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0103) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01032 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0103) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01033 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0103) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01100 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0110) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011010 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011011 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011012 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011013 : adaptiveCoverCheck 12 (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011020 : adaptiveCoverCheck 12 (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011021 : adaptiveCoverCheck 12 (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011022 : adaptiveCoverCheck 12 (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011023 : adaptiveCoverCheck 12 (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011030 : adaptiveCoverCheck 12 (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011031 : adaptiveCoverCheck 12 (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011032 : adaptiveCoverCheck 12 (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011033 : adaptiveCoverCheck 12 (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0110)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011100 : adaptiveCoverCheck 12 (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011101 : adaptiveCoverCheck 12 (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011102 : adaptiveCoverCheck 12 (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011103 : adaptiveCoverCheck 12 (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011110 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011111 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011112 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011113 : adaptiveCoverCheck 12 (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011120 : adaptiveCoverCheck 12 (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011121 : adaptiveCoverCheck 12 (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011122 : adaptiveCoverCheck 12 (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011123 : adaptiveCoverCheck 12 (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011130 : adaptiveCoverCheck 12 (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011131 : adaptiveCoverCheck 12 (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011132 : adaptiveCoverCheck 12 (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf011133 : adaptiveCoverCheck 12 (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0111)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01120 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0112) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01121 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0112) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01122 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0112) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01123 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0112) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01130 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell0113) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01131 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell0113) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01132 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell0113) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf01133 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell0113) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0120 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0120 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0121 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0121 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0122 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0122 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0123 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0123 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0130 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0130 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0131 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0131 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0132 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0132 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf0133 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell0133 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf02 : adaptiveCoverCheck 16 (childHL (childLL e24ThetaBelowRoot)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf030 : adaptiveCoverCheck 15 (childLL (childHH (childLL e24ThetaBelowRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf031 : adaptiveCoverCheck 15 (childLH (childHH (childLL e24ThetaBelowRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf032 : adaptiveCoverCheck 15 (childHL (childHH (childLL e24ThetaBelowRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf033 : adaptiveCoverCheck 15 (childHH (childHH (childLL e24ThetaBelowRoot))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100000 : adaptiveCoverCheck 12 (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100001 : adaptiveCoverCheck 12 (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100002 : adaptiveCoverCheck 12 (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100003 : adaptiveCoverCheck 12 (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100010 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100011 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100012 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100013 : adaptiveCoverCheck 12 (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100020 : adaptiveCoverCheck 12 (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100021 : adaptiveCoverCheck 12 (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100022 : adaptiveCoverCheck 12 (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100023 : adaptiveCoverCheck 12 (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100030 : adaptiveCoverCheck 12 (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100031 : adaptiveCoverCheck 12 (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100032 : adaptiveCoverCheck 12 (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100033 : adaptiveCoverCheck 12 (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1000)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100100 : adaptiveCoverCheck 12 (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100101 : adaptiveCoverCheck 12 (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100102 : adaptiveCoverCheck 12 (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100103 : adaptiveCoverCheck 12 (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100110 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100111 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100112 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001130 : adaptiveCoverCheck 11 (childLL (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001131 : adaptiveCoverCheck 11 (childLH (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001132 : adaptiveCoverCheck 11 (childHL (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001133 : adaptiveCoverCheck 11 (childHH (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100120 : adaptiveCoverCheck 12 (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001210 : adaptiveCoverCheck 11 (childLL (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001211 : adaptiveCoverCheck 11 (childLH (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001212 : adaptiveCoverCheck 11 (childHL (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001213 : adaptiveCoverCheck 11 (childHH (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100122 : adaptiveCoverCheck 12 (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100123 : adaptiveCoverCheck 12 (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001300 : adaptiveCoverCheck 11 (childLL (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001301 : adaptiveCoverCheck 11 (childLH (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001302 : adaptiveCoverCheck 11 (childHL (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001303 : adaptiveCoverCheck 11 (childHH (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001310 : adaptiveCoverCheck 11 (childLL (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001311 : adaptiveCoverCheck 11 (childLH (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001312 : adaptiveCoverCheck 11 (childHL (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1001313 : adaptiveCoverCheck 11 (childHH (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100132 : adaptiveCoverCheck 12 (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100133 : adaptiveCoverCheck 12 (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1001)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10020 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1002) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10021 : adaptiveCoverCheck 13 (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1002) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10022 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1002) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10023 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1002) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10030 : adaptiveCoverCheck 13 (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100310 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1003)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100311 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1003)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100312 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1003)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf100313 : adaptiveCoverCheck 12 (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1003)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10032 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10033 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1003) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101000 : adaptiveCoverCheck 12 (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010010 : adaptiveCoverCheck 11 (childLL (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010011 : adaptiveCoverCheck 11 (childLH (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010012 : adaptiveCoverCheck 11 (childHL (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010013 : adaptiveCoverCheck 11 (childHH (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010020 : adaptiveCoverCheck 11 (childLL (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010021 : adaptiveCoverCheck 11 (childLH (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010022 : adaptiveCoverCheck 11 (childHL (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010023 : adaptiveCoverCheck 11 (childHH (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010030 : adaptiveCoverCheck 11 (childLL (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010031 : adaptiveCoverCheck 11 (childLH (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010032 : adaptiveCoverCheck 11 (childHL (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010033 : adaptiveCoverCheck 11 (childHH (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010100 : adaptiveCoverCheck 11 (childLL (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010101 : adaptiveCoverCheck 11 (childLH (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010102 : adaptiveCoverCheck 11 (childHL (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010103 : adaptiveCoverCheck 11 (childHH (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010110 : adaptiveCoverCheck 11 (childLL (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010111 : adaptiveCoverCheck 11 (childLH (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010112 : adaptiveCoverCheck 11 (childHL (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010113 : adaptiveCoverCheck 11 (childHH (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010120 : adaptiveCoverCheck 11 (childLL (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010121 : adaptiveCoverCheck 11 (childLH (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010122 : adaptiveCoverCheck 11 (childHL (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010123 : adaptiveCoverCheck 11 (childHH (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010130 : adaptiveCoverCheck 11 (childLL (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010131 : adaptiveCoverCheck 11 (childLH (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010132 : adaptiveCoverCheck 11 (childHL (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010133 : adaptiveCoverCheck 11 (childHH (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010200 : adaptiveCoverCheck 11 (childLL (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010201 : adaptiveCoverCheck 11 (childLH (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010202 : adaptiveCoverCheck 11 (childHL (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010203 : adaptiveCoverCheck 11 (childHH (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010210 : adaptiveCoverCheck 11 (childLL (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010211 : adaptiveCoverCheck 11 (childLH (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010212 : adaptiveCoverCheck 11 (childHL (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010213 : adaptiveCoverCheck 11 (childHH (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101022 : adaptiveCoverCheck 12 (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101023 : adaptiveCoverCheck 12 (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1010)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010300 : adaptiveCoverCheck 11 (childLL (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010301 : adaptiveCoverCheck 11 (childLH (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010302 : adaptiveCoverCheck 11 (childHL (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010303 : adaptiveCoverCheck 11 (childHH (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010310 : adaptiveCoverCheck 11 (childLL (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010311 : adaptiveCoverCheck 11 (childLH (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010312 : adaptiveCoverCheck 11 (childHL (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010313 : adaptiveCoverCheck 11 (childHH (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010320 : adaptiveCoverCheck 11 (childLL (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010321 : adaptiveCoverCheck 11 (childLH (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010322 : adaptiveCoverCheck 11 (childHL (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010323 : adaptiveCoverCheck 11 (childHH (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010330 : adaptiveCoverCheck 11 (childLL (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010331 : adaptiveCoverCheck 11 (childLH (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010332 : adaptiveCoverCheck 11 (childHL (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1010333 : adaptiveCoverCheck 11 (childHH (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1010))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011000 : adaptiveCoverCheck 11 (childLL (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011001 : adaptiveCoverCheck 11 (childLH (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011002 : adaptiveCoverCheck 11 (childHL (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011003 : adaptiveCoverCheck 11 (childHH (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101101 : adaptiveCoverCheck 12 (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011020 : adaptiveCoverCheck 11 (childLL (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011021 : adaptiveCoverCheck 11 (childLH (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011022 : adaptiveCoverCheck 11 (childHL (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011023 : adaptiveCoverCheck 11 (childHH (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011030 : adaptiveCoverCheck 11 (childLL (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011031 : adaptiveCoverCheck 11 (childLH (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011032 : adaptiveCoverCheck 11 (childHL (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011033 : adaptiveCoverCheck 11 (childHH (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101110 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101111 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011120 : adaptiveCoverCheck 11 (childLL (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011121 : adaptiveCoverCheck 11 (childLH (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011122 : adaptiveCoverCheck 11 (childHL (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011123 : adaptiveCoverCheck 11 (childHH (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011130 : adaptiveCoverCheck 11 (childLL (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011131 : adaptiveCoverCheck 11 (childLH (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011132 : adaptiveCoverCheck 11 (childHL (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011133 : adaptiveCoverCheck 11 (childHH (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011200 : adaptiveCoverCheck 11 (childLL (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011201 : adaptiveCoverCheck 11 (childLH (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011202 : adaptiveCoverCheck 11 (childHL (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011203 : adaptiveCoverCheck 11 (childHH (childLL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011210 : adaptiveCoverCheck 11 (childLL (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011211 : adaptiveCoverCheck 11 (childLH (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011212 : adaptiveCoverCheck 11 (childHL (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011213 : adaptiveCoverCheck 11 (childHH (childLH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011220 : adaptiveCoverCheck 11 (childLL (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011221 : adaptiveCoverCheck 11 (childLH (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011222 : adaptiveCoverCheck 11 (childHL (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011223 : adaptiveCoverCheck 11 (childHH (childHL (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011230 : adaptiveCoverCheck 11 (childLL (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011231 : adaptiveCoverCheck 11 (childLH (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011232 : adaptiveCoverCheck 11 (childHL (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011233 : adaptiveCoverCheck 11 (childHH (childHH (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011300 : adaptiveCoverCheck 11 (childLL (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011301 : adaptiveCoverCheck 11 (childLH (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011302 : adaptiveCoverCheck 11 (childHL (childLL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113030 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113030 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113031 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113031 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113032 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113032 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113033 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113033 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011310 : adaptiveCoverCheck 11 (childLL (childLH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113110 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113110 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113111 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113111 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113112 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113112 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113113 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113113 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113120 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113120 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113121 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113121 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113122 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113122 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113123 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113123 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113130 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113130 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113131 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113131 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113132 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113132 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10113133 : adaptiveCoverCheck 10 CertificateCells2f4f8ea4fc.thetaBelowCell10113133 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011320 : adaptiveCoverCheck 11 (childLL (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011321 : adaptiveCoverCheck 11 (childLH (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011322 : adaptiveCoverCheck 11 (childHL (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011323 : adaptiveCoverCheck 11 (childHH (childHL (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011330 : adaptiveCoverCheck 11 (childLL (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011331 : adaptiveCoverCheck 11 (childLH (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011332 : adaptiveCoverCheck 11 (childHL (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1011333 : adaptiveCoverCheck 11 (childHH (childHH (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1011))) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101200 : adaptiveCoverCheck 12 (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101201 : adaptiveCoverCheck 12 (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101202 : adaptiveCoverCheck 12 (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101203 : adaptiveCoverCheck 12 (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101210 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101211 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101212 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101213 : adaptiveCoverCheck 12 (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1012)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10122 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1012) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10123 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1012) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101300 : adaptiveCoverCheck 12 (childLL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101301 : adaptiveCoverCheck 12 (childLH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101302 : adaptiveCoverCheck 12 (childHL (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101303 : adaptiveCoverCheck 12 (childHH (childLL CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101310 : adaptiveCoverCheck 12 (childLL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101311 : adaptiveCoverCheck 12 (childLH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101312 : adaptiveCoverCheck 12 (childHL (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf101313 : adaptiveCoverCheck 12 (childHH (childLH CertificateCells2f4f8ea4fc.thetaBelowCell1013)) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10132 : adaptiveCoverCheck 13 (childHL CertificateCells2f4f8ea4fc.thetaBelowCell1013) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf10133 : adaptiveCoverCheck 13 (childHH CertificateCells2f4f8ea4fc.thetaBelowCell1013) = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1020 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell1020 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1021 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell1021 = true

theorem GerverSofa.PartE.e24KC2ThetaBelowLeaf1022 : adaptiveCoverCheck 14 CertificateCells2f4f8ea4fc.thetaBelowCell1022 = true

Gerver sofa dependency batch

• KernelOnly.PartE.E24KC6ProofBatch11b2bedf1dcd3516.

E24KC6 explicit proof-producing certificate batch.

theorem GerverSofa.PartE.cover_subtree_edb64f01a0c6 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022103100) = true

theorem GerverSofa.PartE.cover_subtree_a40a1df9b3a1 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022103100) = true

theorem GerverSofa.PartE.cover_subtree_e870c75d402b : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103100 = true

theorem GerverSofa.PartE.cover_subtree_5efea1d56268 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022103101) = true

theorem GerverSofa.PartE.cover_subtree_d2aa99fffe31 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022103101) = true

theorem GerverSofa.PartE.cover_subtree_0abbf33fdebf : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103101 = true

theorem GerverSofa.PartE.cover_subtree_1d0945e98034 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022103102) = true

theorem GerverSofa.PartE.cover_subtree_e19e97fa44f4 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022103102) = true

theorem GerverSofa.PartE.cover_subtree_92cf9ed4da50 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103102 = true

theorem GerverSofa.PartE.cover_subtree_637f019f84f2 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022103103) = true

theorem GerverSofa.PartE.cover_subtree_2f9a3a39c9a5 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022103103) = true

theorem GerverSofa.PartE.cover_subtree_30350e948f84 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103103 = true

theorem GerverSofa.PartE.cover_subtree_4a228fe99e26 : adaptiveCoverCheck 8 (childLL (childLH (childHH CertificateCells2d2385ed48.thetaAboveCell00002210))) = true

theorem GerverSofa.PartE.cover_subtree_dec56845b136 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022103110) = true

theorem GerverSofa.PartE.cover_subtree_6de59f8bb098 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022103110) = true

theorem GerverSofa.PartE.cover_subtree_ab36c8726f5a : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103110 = true

theorem GerverSofa.PartE.cover_subtree_59e28493c6fc : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022103111) = true

theorem GerverSofa.PartE.cover_subtree_de44712e43a7 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022103111) = true

theorem GerverSofa.PartE.cover_subtree_526ec4bd5c8b : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103111 = true

theorem GerverSofa.PartE.cover_subtree_f14f28c14e3c : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022103112) = true

theorem GerverSofa.PartE.cover_subtree_2e18124844df : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022103112) = true

theorem GerverSofa.PartE.cover_subtree_f0199f1a57d7 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103112 = true

theorem GerverSofa.PartE.cover_subtree_48a3af012806 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022103113) = true

theorem GerverSofa.PartE.cover_subtree_e9c96ebadfa8 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022103113) = true

theorem GerverSofa.PartE.cover_subtree_88cc51539fac : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022103113 = true

theorem GerverSofa.PartE.cover_subtree_a1d8aa321d27 : adaptiveCoverCheck 8 (childLH (childLH (childHH CertificateCells2d2385ed48.thetaAboveCell00002210))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells2d2385ed48.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells2d2385ed48.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells2d2385ed48.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221102 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221103 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221112 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221113 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.cover_subtree_43fd6107c581 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112000) = true

theorem GerverSofa.PartE.cover_subtree_2f5d0def195d : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112000) = true

theorem GerverSofa.PartE.cover_subtree_b847b0feac2d : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112000 = true

theorem GerverSofa.PartE.cover_subtree_4950fac9bab9 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112001) = true

theorem GerverSofa.PartE.cover_subtree_0e72524614ed : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112001) = true

theorem GerverSofa.PartE.cover_subtree_b10e2b341d50 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112001 = true

theorem GerverSofa.PartE.cover_subtree_76b490d87a4e : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112002) = true

theorem GerverSofa.PartE.cover_subtree_4b9c90d07695 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112002) = true

theorem GerverSofa.PartE.cover_subtree_b7dd7162f0b9 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112002 = true

theorem GerverSofa.PartE.cover_subtree_de29b5c5a11d : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112003) = true

theorem GerverSofa.PartE.cover_subtree_31f4d5809705 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112003) = true

theorem GerverSofa.PartE.cover_subtree_c9c566e964a9 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112003 = true

theorem GerverSofa.PartE.cover_subtree_da67754fe633 : adaptiveCoverCheck 8 (childLL (childLL (childHL CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.cover_subtree_95f6e6d97c24 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112010) = true

theorem GerverSofa.PartE.cover_subtree_9c844972ea1f : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112010) = true

theorem GerverSofa.PartE.cover_subtree_04ff1f51c7c8 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112010 = true

theorem GerverSofa.PartE.cover_subtree_754b681a3e26 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112011) = true

theorem GerverSofa.PartE.cover_subtree_497a7c55810a : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112011) = true

theorem GerverSofa.PartE.cover_subtree_92922a2edd2b : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112011 = true

theorem GerverSofa.PartE.cover_subtree_bfdd630a1f02 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112012) = true

theorem GerverSofa.PartE.cover_subtree_d41a2b9225dd : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112012) = true

theorem GerverSofa.PartE.cover_subtree_b54fc51b3ec8 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112012 = true

theorem GerverSofa.PartE.cover_subtree_1ae8b8609603 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112013) = true

theorem GerverSofa.PartE.cover_subtree_254e7d6a1a8d : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112013) = true

theorem GerverSofa.PartE.cover_subtree_316108a366aa : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112013 = true

theorem GerverSofa.PartE.cover_subtree_23a35d53c9e2 : adaptiveCoverCheck 8 (childLH (childLL (childHL CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.cover_subtree_021e44d85b50 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112100) = true

theorem GerverSofa.PartE.cover_subtree_62fa6c2e1429 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112100) = true

theorem GerverSofa.PartE.cover_subtree_ff28352fdcbd : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112100 = true

theorem GerverSofa.PartE.cover_subtree_4284ed2ee8d6 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112101) = true

theorem GerverSofa.PartE.cover_subtree_21c449726701 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112101) = true

theorem GerverSofa.PartE.cover_subtree_ecd8fe40a0e6 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112101 = true

theorem GerverSofa.PartE.cover_subtree_4e862092a132 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112102) = true

theorem GerverSofa.PartE.cover_subtree_aa7a39051514 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112102) = true

theorem GerverSofa.PartE.cover_subtree_bcfbc1ac2009 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112102 = true

theorem GerverSofa.PartE.cover_subtree_340b36315559 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112103) = true

theorem GerverSofa.PartE.cover_subtree_3ea1443179e3 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112103) = true

theorem GerverSofa.PartE.cover_subtree_333ca6341b52 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112103 = true

theorem GerverSofa.PartE.cover_subtree_0a317c2968a3 : adaptiveCoverCheck 8 (childLL (childLH (childHL CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.cover_subtree_0f6a5316da7f : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112110) = true

theorem GerverSofa.PartE.cover_subtree_8b21324e2245 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112110) = true

theorem GerverSofa.PartE.cover_subtree_2b3d980fd10a : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112110 = true

theorem GerverSofa.PartE.cover_subtree_3d8086490270 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022112111) = true

theorem GerverSofa.PartE.cover_subtree_13b36b31ee50 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022112111) = true

theorem GerverSofa.PartE.cover_subtree_fe061292783d : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112111 = true

theorem GerverSofa.PartE.cover_subtree_acdbdc38c196 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112112) = true

theorem GerverSofa.PartE.cover_subtree_f4b1386a9f86 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112112) = true

theorem GerverSofa.PartE.cover_subtree_280eb01136d6 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112112 = true

theorem GerverSofa.PartE.cover_subtree_3add30d6277d : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022112113) = true

theorem GerverSofa.PartE.cover_subtree_4b342ee841c3 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022112113) = true

theorem GerverSofa.PartE.cover_subtree_95d32084082d : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022112113 = true

theorem GerverSofa.PartE.cover_subtree_9112d0843a89 : adaptiveCoverCheck 8 (childLH (childLH (childHL CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.cover_subtree_c69725c188d3 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113000) = true

theorem GerverSofa.PartE.cover_subtree_a8d579475d23 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113000) = true

theorem GerverSofa.PartE.cover_subtree_560b815bd286 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113000 = true

theorem GerverSofa.PartE.cover_subtree_995ab0851a0f : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113001) = true

theorem GerverSofa.PartE.cover_subtree_f5e3b9ffae68 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113001) = true

theorem GerverSofa.PartE.cover_subtree_e2b5567129eb : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113001 = true

theorem GerverSofa.PartE.cover_subtree_2a8071ef107e : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022113002) = true

theorem GerverSofa.PartE.cover_subtree_1f4e667d89aa : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022113002) = true

theorem GerverSofa.PartE.cover_subtree_cf43677b186a : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113002 = true

theorem GerverSofa.PartE.cover_subtree_e06c4b38ee49 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022113003) = true

theorem GerverSofa.PartE.cover_subtree_5735fc3146a5 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022113003) = true

theorem GerverSofa.PartE.cover_subtree_b9715c0ddc62 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113003 = true

theorem GerverSofa.PartE.cover_subtree_0338ef548092 : adaptiveCoverCheck 8 (childLL (childLL (childHH CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.cover_subtree_8babef05283e : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113010) = true

theorem GerverSofa.PartE.cover_subtree_453a26c2a0ce : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113010) = true

theorem GerverSofa.PartE.cover_subtree_9a8d1e8ff5df : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113010 = true

theorem GerverSofa.PartE.cover_subtree_d4f84dde625a : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113011) = true

theorem GerverSofa.PartE.cover_subtree_a97cdaa163bd : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113011) = true

theorem GerverSofa.PartE.cover_subtree_caad7b9ebe18 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113011 = true

theorem GerverSofa.PartE.cover_subtree_fbb8d3b85bf4 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022113012) = true

theorem GerverSofa.PartE.cover_subtree_f025663eb4cc : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022113012) = true

theorem GerverSofa.PartE.cover_subtree_6d9b8f942e07 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113012 = true

theorem GerverSofa.PartE.cover_subtree_c85e1b57b2c5 : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022113013) = true

theorem GerverSofa.PartE.cover_subtree_a12be2bf4817 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022113013) = true

theorem GerverSofa.PartE.cover_subtree_d1382a844a10 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113013 = true

theorem GerverSofa.PartE.cover_subtree_d4d29d86cd96 : adaptiveCoverCheck 8 (childLH (childLL (childHH CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.cover_subtree_836d962e65ac : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113100) = true

theorem GerverSofa.PartE.cover_subtree_ecf6c7f90571 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113100) = true

theorem GerverSofa.PartE.cover_subtree_fa2b1e57d306 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113100 = true

theorem GerverSofa.PartE.cover_subtree_2c032bc482bc : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113101) = true

theorem GerverSofa.PartE.cover_subtree_3eddb0efc253 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113101) = true

theorem GerverSofa.PartE.cover_subtree_cbdd15c92455 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113101 = true

theorem GerverSofa.PartE.cover_subtree_e867c54455aa : adaptiveCoverCheck 6 (childLL CertificateCells2d2385ed48.thetaAboveCell000022113102) = true

theorem GerverSofa.PartE.cover_subtree_d8e5977bc823 : adaptiveCoverCheck 6 (childLH CertificateCells2d2385ed48.thetaAboveCell000022113102) = true

theorem GerverSofa.PartE.cover_subtree_81e578425a2e : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113102 = true

theorem GerverSofa.PartE.cover_subtree_6af7504512c8 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113103 = true

theorem GerverSofa.PartE.cover_subtree_dc05a5cb4d61 : adaptiveCoverCheck 8 (childLL (childLH (childHH CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.cover_subtree_fcbdf3a9e595 : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113110) = true

theorem GerverSofa.PartE.cover_subtree_2828e56e478f : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113110) = true

theorem GerverSofa.PartE.cover_subtree_15fb86545eea : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113110 = true

theorem GerverSofa.PartE.cover_subtree_0f38c8258b2e : adaptiveCoverCheck 6 (childHL CertificateCells2d2385ed48.thetaAboveCell000022113111) = true

theorem GerverSofa.PartE.cover_subtree_13fc46665967 : adaptiveCoverCheck 6 (childHH CertificateCells2d2385ed48.thetaAboveCell000022113111) = true

theorem GerverSofa.PartE.cover_subtree_83c447d13cd0 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113111 = true

theorem GerverSofa.PartE.cover_subtree_02c32f65c578 : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113112 = true

theorem GerverSofa.PartE.cover_subtree_74079318656f : adaptiveCoverCheck 7 CertificateCells2d2385ed48.thetaAboveCell000022113113 = true

theorem GerverSofa.PartE.cover_subtree_6a41f1f44284 : adaptiveCoverCheck 8 (childLH (childLH (childHH CertificateCells2d2385ed48.thetaAboveCell00002211))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells2d2385ed48.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230002 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells2d2385ed48.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230003 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells2d2385ed48.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230012 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells2d2385ed48.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230013 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells2d2385ed48.thetaAboveCell00002300)) = true