Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch005.
• GerverSofa.KernelOnly.PartE.Certificates.Batch027.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell0133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiAboveCell1133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiBelowCell3221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiBelowCell3222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiBelowCell3223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiBelowCell3310 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiBelowCell3311 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.phiBelowCell3313 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.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.CertificateCells0d991a929b.thetaAboveCell00002020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002200 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002201 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002202 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002203 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.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.CertificateCells0d991a929b.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.CertificateCells0d991a929b.thetaAboveCell00002212 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002213 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.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.CertificateCells0d991a929b.thetaAboveCell00002301 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002302 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002303 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002310 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002311 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002312 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002313 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00002333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells0d991a929b.thetaAboveCell00003120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.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.CertificateCells802ef10e9d.thetaAboveCell00002310 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell00002311 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell00003200 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell00003201 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023102133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023103133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023110333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023111333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023112133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000023113133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000230 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000231 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000232 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000233 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000320 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000321 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000322 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000323 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000330 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000331 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000332 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032000333 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032001220 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032001221 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032001222 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032001223 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032002133 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003000 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003001 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003002 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003003 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003010 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003011 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003012 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003013 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003020 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003021 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003022 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003023 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003030 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003031 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003032 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003033 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003100 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003101 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003102 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003103 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003110 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003111 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003112 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003113 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003120 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003121 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003122 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003123 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003130 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003131 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003132 : AngleCell

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

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells802ef10e9d.thetaAboveCell000032003133 : AngleCell

Subcell 000032003133 of the 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.E24KC5TerminalBatchT000001.

E24KC5 checkpoint-aware kernel batch.

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00000 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell0000) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00001 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell0000) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00002 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0000) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00003 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0000) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00010 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell0001) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00011 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell0001) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00012 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0001) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00013 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0001) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0002 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0002 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0003 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0003 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00100 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell0010) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00101 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell0010) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00102 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0010) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00103 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0010) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00110 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell0011) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00111 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell0011) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00112 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0011) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf00113 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0011) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0012 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0012 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0013 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0013 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf002 : adaptiveCoverCheck 13 (childHL (childLL (childLL e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0030 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0030 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0031 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0031 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0032 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0032 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0033 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0033 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01000 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell0100) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01001 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell0100) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01002 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0100) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01003 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0100) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01010 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell0101) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf010110 : adaptiveCoverCheck 10 (childLL (childLH CertificateCells0d991a929b.phiAboveCell0101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf010111 : adaptiveCoverCheck 10 (childLH (childLH CertificateCells0d991a929b.phiAboveCell0101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf010112 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell0101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf010113 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell0101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01012 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0101) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01013 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0101) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0102 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0102 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0103 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0103 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011000 : adaptiveCoverCheck 10 (childLL (childLL CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011001 : adaptiveCoverCheck 10 (childLH (childLL CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011002 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011003 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011010 : adaptiveCoverCheck 10 (childLL (childLH CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011011 : adaptiveCoverCheck 10 (childLH (childLH CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011012 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011013 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell0110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01102 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0110) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01103 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0110) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011100 : adaptiveCoverCheck 10 (childLL (childLL CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011101 : adaptiveCoverCheck 10 (childLH (childLL CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011102 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011103 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011110 : adaptiveCoverCheck 10 (childLL (childLH CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011111 : adaptiveCoverCheck 10 (childLH (childLH CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011112 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf011113 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell0111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01112 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell0111) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf01113 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell0111) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0112 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0112 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0113 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0113 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0120 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0120 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0121 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0121 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0122 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0122 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0123 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0123 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0130 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0130 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0131 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0131 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0132 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0132 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf0133 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell0133 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf02 : adaptiveCoverCheck 14 (childHL (childLL e24PhiAboveRoot)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf030 : adaptiveCoverCheck 13 (childLL (childHH (childLL e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf031 : adaptiveCoverCheck 13 (childLH (childHH (childLL e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf032 : adaptiveCoverCheck 13 (childHL (childHH (childLL e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf033 : adaptiveCoverCheck 13 (childHH (childHH (childLL e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100000 : adaptiveCoverCheck 10 (childLL (childLL CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100001 : adaptiveCoverCheck 10 (childLH (childLL CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100002 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100003 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100010 : adaptiveCoverCheck 10 (childLL (childLH CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100011 : adaptiveCoverCheck 10 (childLH (childLH CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100012 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100013 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell1000)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10002 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1000) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10003 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1000) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100100 : adaptiveCoverCheck 10 (childLL (childLL CertificateCells0d991a929b.phiAboveCell1001)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001010 : adaptiveCoverCheck 9 (childLL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001011 : adaptiveCoverCheck 9 (childLH (childLH (childLL CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001012 : adaptiveCoverCheck 9 (childHL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001013 : adaptiveCoverCheck 9 (childHH (childLH (childLL CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100102 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell1001)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100103 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell1001)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001100 : adaptiveCoverCheck 9 (childLL (childLL (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001101 : adaptiveCoverCheck 9 (childLH (childLL (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001102 : adaptiveCoverCheck 9 (childHL (childLL (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001103 : adaptiveCoverCheck 9 (childHH (childLL (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001110 : adaptiveCoverCheck 9 (childLL (childLH (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001111 : adaptiveCoverCheck 9 (childLH (childLH (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001112 : adaptiveCoverCheck 9 (childHL (childLH (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1001113 : adaptiveCoverCheck 9 (childHH (childLH (childLH CertificateCells0d991a929b.phiAboveCell1001))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100112 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell1001)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf100113 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell1001)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10012 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1001) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10013 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1001) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10020 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1002) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10021 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1002) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10022 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1002) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10023 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1002) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10030 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1003) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10031 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1003) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10032 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1003) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10033 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1003) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010000 : adaptiveCoverCheck 9 (childLL (childLL (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010001 : adaptiveCoverCheck 9 (childLH (childLL (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010002 : adaptiveCoverCheck 9 (childHL (childLL (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010003 : adaptiveCoverCheck 9 (childHH (childLL (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010010 : adaptiveCoverCheck 9 (childLL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010011 : adaptiveCoverCheck 9 (childLH (childLH (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010012 : adaptiveCoverCheck 9 (childHL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010013 : adaptiveCoverCheck 9 (childHH (childLH (childLL CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101002 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell1010)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101003 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell1010)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010100 : adaptiveCoverCheck 9 (childLL (childLL (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010101 : adaptiveCoverCheck 9 (childLH (childLL (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010102 : adaptiveCoverCheck 9 (childHL (childLL (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010103 : adaptiveCoverCheck 9 (childHH (childLL (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010110 : adaptiveCoverCheck 9 (childLL (childLH (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010111 : adaptiveCoverCheck 9 (childLH (childLH (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010112 : adaptiveCoverCheck 9 (childHL (childLH (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1010113 : adaptiveCoverCheck 9 (childHH (childLH (childLH CertificateCells0d991a929b.phiAboveCell1010))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101012 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell1010)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101013 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell1010)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10102 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1010) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10103 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1010) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011000 : adaptiveCoverCheck 9 (childLL (childLL (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011001 : adaptiveCoverCheck 9 (childLH (childLL (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011002 : adaptiveCoverCheck 9 (childHL (childLL (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011003 : adaptiveCoverCheck 9 (childHH (childLL (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011010 : adaptiveCoverCheck 9 (childLL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011012 : adaptiveCoverCheck 9 (childHL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011013 : adaptiveCoverCheck 9 (childHH (childLH (childLL CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101102 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101103 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011102 : adaptiveCoverCheck 9 (childHL (childLL (childLH CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011103 : adaptiveCoverCheck 9 (childHH (childLL (childLH CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011112 : adaptiveCoverCheck 9 (childHL (childLH (childLH CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1011113 : adaptiveCoverCheck 9 (childHH (childLH (childLH CertificateCells0d991a929b.phiAboveCell1011))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101112 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101113 : adaptiveCoverCheck 10 (childHH (childLH CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10112 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1011) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101130 : adaptiveCoverCheck 10 (childLL (childHH CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101131 : adaptiveCoverCheck 10 (childLH (childHH CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101132 : adaptiveCoverCheck 10 (childHL (childHH CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf101133 : adaptiveCoverCheck 10 (childHH (childHH CertificateCells0d991a929b.phiAboveCell1011)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10120 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1012) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10121 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1012) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10122 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1012) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10123 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1012) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10130 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1013) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10131 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1013) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10132 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1013) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf10133 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1013) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1020 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1020 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1021 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1021 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1022 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1022 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1023 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1023 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1030 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1030 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1031 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1031 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1032 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1032 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1033 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1033 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100002 : adaptiveCoverCheck 9 (childHL (childLL (childLL CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100003 : adaptiveCoverCheck 9 (childHH (childLL (childLL CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100012 : adaptiveCoverCheck 9 (childHL (childLH (childLL CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100013 : adaptiveCoverCheck 9 (childHH (childLH (childLL CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110002 : adaptiveCoverCheck 10 (childHL (childLL CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110003 : adaptiveCoverCheck 10 (childHH (childLL CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100102 : adaptiveCoverCheck 9 (childHL (childLL (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100103 : adaptiveCoverCheck 9 (childHH (childLL (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100112 : adaptiveCoverCheck 9 (childHL (childLH (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100113 : adaptiveCoverCheck 9 (childHH (childLH (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110012 : adaptiveCoverCheck 10 (childHL (childLH CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100130 : adaptiveCoverCheck 9 (childLL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100131 : adaptiveCoverCheck 9 (childLH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100132 : adaptiveCoverCheck 9 (childHL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1100133 : adaptiveCoverCheck 9 (childHH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1100))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110020 : adaptiveCoverCheck 10 (childLL (childHL CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110021 : adaptiveCoverCheck 10 (childLH (childHL CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110022 : adaptiveCoverCheck 10 (childHL (childHL CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110023 : adaptiveCoverCheck 10 (childHH (childHL CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110030 : adaptiveCoverCheck 10 (childLL (childHH CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110031 : adaptiveCoverCheck 10 (childLH (childHH CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110032 : adaptiveCoverCheck 10 (childHL (childHH CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110033 : adaptiveCoverCheck 10 (childHH (childHH CertificateCells0d991a929b.phiAboveCell1100)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101002 : adaptiveCoverCheck 9 (childHL (childLL (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101003 : adaptiveCoverCheck 9 (childHH (childLL (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101020 : adaptiveCoverCheck 9 (childLL (childHL (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101021 : adaptiveCoverCheck 9 (childLH (childHL (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101022 : adaptiveCoverCheck 9 (childHL (childHL (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101023 : adaptiveCoverCheck 9 (childHH (childHL (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101030 : adaptiveCoverCheck 9 (childLL (childHH (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101031 : adaptiveCoverCheck 9 (childLH (childHH (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101032 : adaptiveCoverCheck 9 (childHL (childHH (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101033 : adaptiveCoverCheck 9 (childHH (childHH (childLL CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101120 : adaptiveCoverCheck 9 (childLL (childHL (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101121 : adaptiveCoverCheck 9 (childLH (childHL (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101122 : adaptiveCoverCheck 9 (childHL (childHL (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101123 : adaptiveCoverCheck 9 (childHH (childHL (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101130 : adaptiveCoverCheck 9 (childLL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101131 : adaptiveCoverCheck 9 (childLH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101132 : adaptiveCoverCheck 9 (childHL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101133 : adaptiveCoverCheck 9 (childHH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1101))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110120 : adaptiveCoverCheck 10 (childLL (childHL CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110121 : adaptiveCoverCheck 10 (childLH (childHL CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110122 : adaptiveCoverCheck 10 (childHL (childHL CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110123 : adaptiveCoverCheck 10 (childHH (childHL CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110130 : adaptiveCoverCheck 10 (childLL (childHH CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110131 : adaptiveCoverCheck 10 (childLH (childHH CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110132 : adaptiveCoverCheck 10 (childHL (childHH CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf110133 : adaptiveCoverCheck 10 (childHH (childHH CertificateCells0d991a929b.phiAboveCell1101)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11020 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1102) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11021 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1102) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11022 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1102) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11023 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1102) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11030 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1103) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11031 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1103) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11032 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1103) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11033 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1103) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110020 : adaptiveCoverCheck 9 (childLL (childHL (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110021 : adaptiveCoverCheck 9 (childLH (childHL (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110022 : adaptiveCoverCheck 9 (childHL (childHL (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110023 : adaptiveCoverCheck 9 (childHH (childHL (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110030 : adaptiveCoverCheck 9 (childLL (childHH (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110031 : adaptiveCoverCheck 9 (childLH (childHH (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110032 : adaptiveCoverCheck 9 (childHL (childHH (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110033 : adaptiveCoverCheck 9 (childHH (childHH (childLL CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110120 : adaptiveCoverCheck 9 (childLL (childHL (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110121 : adaptiveCoverCheck 9 (childLH (childHL (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110122 : adaptiveCoverCheck 9 (childHL (childHL (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110123 : adaptiveCoverCheck 9 (childHH (childHL (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110130 : adaptiveCoverCheck 9 (childLL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110131 : adaptiveCoverCheck 9 (childLH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110132 : adaptiveCoverCheck 9 (childHL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110133 : adaptiveCoverCheck 9 (childHH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1110))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111020 : adaptiveCoverCheck 10 (childLL (childHL CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111021 : adaptiveCoverCheck 10 (childLH (childHL CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111022 : adaptiveCoverCheck 10 (childHL (childHL CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111023 : adaptiveCoverCheck 10 (childHH (childHL CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111030 : adaptiveCoverCheck 10 (childLL (childHH CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111031 : adaptiveCoverCheck 10 (childLH (childHH CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111032 : adaptiveCoverCheck 10 (childHL (childHH CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111033 : adaptiveCoverCheck 10 (childHH (childHH CertificateCells0d991a929b.phiAboveCell1110)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111020 : adaptiveCoverCheck 9 (childLL (childHL (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111021 : adaptiveCoverCheck 9 (childLH (childHL (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111022 : adaptiveCoverCheck 9 (childHL (childHL (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111023 : adaptiveCoverCheck 9 (childHH (childHL (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111030 : adaptiveCoverCheck 9 (childLL (childHH (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111031 : adaptiveCoverCheck 9 (childLH (childHH (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111032 : adaptiveCoverCheck 9 (childHL (childHH (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111033 : adaptiveCoverCheck 9 (childHH (childHH (childLL CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111120 : adaptiveCoverCheck 9 (childLL (childHL (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111121 : adaptiveCoverCheck 9 (childLH (childHL (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111122 : adaptiveCoverCheck 9 (childHL (childHL (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111123 : adaptiveCoverCheck 9 (childHH (childHL (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111130 : adaptiveCoverCheck 9 (childLL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111132 : adaptiveCoverCheck 9 (childHL (childHH (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1111133 : adaptiveCoverCheck 9 (childHH (childHH (childLH CertificateCells0d991a929b.phiAboveCell1111))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111120 : adaptiveCoverCheck 10 (childLL (childHL CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111121 : adaptiveCoverCheck 10 (childLH (childHL CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111122 : adaptiveCoverCheck 10 (childHL (childHL CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111123 : adaptiveCoverCheck 10 (childHH (childHL CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111130 : adaptiveCoverCheck 10 (childLL (childHH CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111131 : adaptiveCoverCheck 10 (childLH (childHH CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111132 : adaptiveCoverCheck 10 (childHL (childHH CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf111133 : adaptiveCoverCheck 10 (childHH (childHH CertificateCells0d991a929b.phiAboveCell1111)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11120 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1112) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11121 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1112) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11122 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1112) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11123 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1112) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11130 : adaptiveCoverCheck 11 (childLL CertificateCells0d991a929b.phiAboveCell1113) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11131 : adaptiveCoverCheck 11 (childLH CertificateCells0d991a929b.phiAboveCell1113) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11132 : adaptiveCoverCheck 11 (childHL CertificateCells0d991a929b.phiAboveCell1113) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf11133 : adaptiveCoverCheck 11 (childHH CertificateCells0d991a929b.phiAboveCell1113) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1120 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1120 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1121 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1121 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1122 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1122 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1123 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1123 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1130 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1130 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1131 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1131 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1132 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1132 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1133 : adaptiveCoverCheck 12 CertificateCells0d991a929b.phiAboveCell1133 = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf120 : adaptiveCoverCheck 13 (childLL (childHL (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf121 : adaptiveCoverCheck 13 (childLH (childHL (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf122 : adaptiveCoverCheck 13 (childHL (childHL (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf123 : adaptiveCoverCheck 13 (childHH (childHL (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf130 : adaptiveCoverCheck 13 (childLL (childHH (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf131 : adaptiveCoverCheck 13 (childLH (childHH (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf132 : adaptiveCoverCheck 13 (childHL (childHH (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf133 : adaptiveCoverCheck 13 (childHH (childHH (childLH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf2 : adaptiveCoverCheck 15 (childHL e24PhiAboveRoot) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf300 : adaptiveCoverCheck 13 (childLL (childLL (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf301 : adaptiveCoverCheck 13 (childLH (childLL (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf302 : adaptiveCoverCheck 13 (childHL (childLL (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf303 : adaptiveCoverCheck 13 (childHH (childLL (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf310 : adaptiveCoverCheck 13 (childLL (childLH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf311 : adaptiveCoverCheck 13 (childLH (childLH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf312 : adaptiveCoverCheck 13 (childHL (childLH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf313 : adaptiveCoverCheck 13 (childHH (childLH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf32 : adaptiveCoverCheck 14 (childHL (childHH e24PhiAboveRoot)) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf330 : adaptiveCoverCheck 13 (childLL (childHH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf331 : adaptiveCoverCheck 13 (childLH (childHH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf332 : adaptiveCoverCheck 13 (childHL (childHH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf333 : adaptiveCoverCheck 13 (childHH (childHH (childHH e24PhiAboveRoot))) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32212 : adaptiveCoverCheck 9 (childHL CertificateCells0d991a929b.phiBelowCell3221) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32220 : adaptiveCoverCheck 9 (childLL CertificateCells0d991a929b.phiBelowCell3222) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32221 : adaptiveCoverCheck 9 (childLH CertificateCells0d991a929b.phiBelowCell3222) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32222 : adaptiveCoverCheck 9 (childHL CertificateCells0d991a929b.phiBelowCell3222) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32223 : adaptiveCoverCheck 9 (childHH CertificateCells0d991a929b.phiBelowCell3222) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32230 : adaptiveCoverCheck 9 (childLL CertificateCells0d991a929b.phiBelowCell3223) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32232 : adaptiveCoverCheck 9 (childHL CertificateCells0d991a929b.phiBelowCell3223) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf32233 : adaptiveCoverCheck 9 (childHH CertificateCells0d991a929b.phiBelowCell3223) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33100 : adaptiveCoverCheck 9 (childLL CertificateCells0d991a929b.phiBelowCell3310) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33101 : adaptiveCoverCheck 9 (childLH CertificateCells0d991a929b.phiBelowCell3310) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33103 : adaptiveCoverCheck 9 (childHH CertificateCells0d991a929b.phiBelowCell3310) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33110 : adaptiveCoverCheck 9 (childLL CertificateCells0d991a929b.phiBelowCell3311) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33111 : adaptiveCoverCheck 9 (childLH CertificateCells0d991a929b.phiBelowCell3311) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33112 : adaptiveCoverCheck 9 (childHL CertificateCells0d991a929b.phiBelowCell3311) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33113 : adaptiveCoverCheck 9 (childHH CertificateCells0d991a929b.phiBelowCell3311) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33130 : adaptiveCoverCheck 9 (childLL CertificateCells0d991a929b.phiBelowCell3313) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33131 : adaptiveCoverCheck 9 (childLH CertificateCells0d991a929b.phiBelowCell3313) = true

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33133 : adaptiveCoverCheck 9 (childHH CertificateCells0d991a929b.phiBelowCell3313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000000 : adaptiveCoverCheck 13 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000001 : adaptiveCoverCheck 13 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000002 : adaptiveCoverCheck 13 (childHL (childLL CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000003 : adaptiveCoverCheck 13 (childHH (childLL CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000010 : adaptiveCoverCheck 13 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000011 : adaptiveCoverCheck 13 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000012 : adaptiveCoverCheck 13 (childHL (childLH CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000013 : adaptiveCoverCheck 13 (childHH (childLH CertificateCells0d991a929b.thetaAboveCell0000)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000200 : adaptiveCoverCheck 12 (childLL (childLL (childHL CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000201 : adaptiveCoverCheck 12 (childLH (childLL (childHL CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002020 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002020 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002021 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002021 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020220 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020221 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020222 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020223 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020230 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020231 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020232 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020233 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002030 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002030 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002031 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002031 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020320 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020321 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020322 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020323 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020330 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020331 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020332 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000020333 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000210 : adaptiveCoverCheck 12 (childLL (childLH (childHL CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000211 : adaptiveCoverCheck 12 (childLH (childLH (childHL CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002120 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002120 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002121 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002121 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021220 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002122) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021221 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002122) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021222 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002122) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021223 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002122) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021230 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002123) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021231 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002123) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021232 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002123) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021233 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002123) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002130 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002130 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002131 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002131 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021320 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002132) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021321 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002132) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021322 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002132) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021323 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002132) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021330 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002133) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021331 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002133) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021332 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002133) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000021333 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002133) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220000 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220001 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220010 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220011 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220100 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220101 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220110 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220111 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022020 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022021 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022022 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022023 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002202) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022030 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022031 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022032 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022033 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002203) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221000 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221001 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221010 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221011 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002210)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221100 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221101 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221110 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221111 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002211)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022120 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022121 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022122 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022123 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002212) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022130 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells0d991a929b.thetaAboveCell00002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000221313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells0d991a929b.thetaAboveCell00002213)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022132 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000022133 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002213) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002220 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002220 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002221 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002221 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002222 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002222 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002223 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002223 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002230 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002230 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002231 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002231 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002232 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002232 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002233 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002233 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230000 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230001 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230010 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230011 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002300)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230100 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230101 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230110 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230111 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002301)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells0d991a929b.thetaAboveCell00002302)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023022 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023023 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002302) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000230313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells0d991a929b.thetaAboveCell00002303)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023032 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023033 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002303) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231000 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231001 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231010 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231011 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231100 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231101 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231110 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231111 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231200 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231201 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231202 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231203 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231210 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231211 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231212 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231213 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells0d991a929b.thetaAboveCell00002312)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023122 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023123 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002312) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231300 : adaptiveCoverCheck 9 (childLL (childLL CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231301 : adaptiveCoverCheck 9 (childLH (childLL CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231302 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231303 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231310 : adaptiveCoverCheck 9 (childLL (childLH CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231311 : adaptiveCoverCheck 9 (childLH (childLH CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231312 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231313 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells0d991a929b.thetaAboveCell00002313)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023132 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00002313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000023133 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00002313) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002320 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002320 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002321 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002321 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002322 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002322 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002323 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002323 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002330 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002330 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002331 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002331 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002332 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002332 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00002333 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00002333 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000300 : adaptiveCoverCheck 12 (childLL (childLL (childHH CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000301 : adaptiveCoverCheck 12 (childLH (childLL (childHH CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00003020 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00003020 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00003021 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00003021 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030220 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00003022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030221 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00003022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030222 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00003022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030223 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00003022) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030230 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00003023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030231 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00003023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030232 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00003023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030233 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00003023) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00003030 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00003030 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00003031 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00003031 = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030320 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00003032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030321 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00003032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030322 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00003032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030323 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00003032) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030330 : adaptiveCoverCheck 10 (childLL CertificateCells0d991a929b.thetaAboveCell00003033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030331 : adaptiveCoverCheck 10 (childLH CertificateCells0d991a929b.thetaAboveCell00003033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030332 : adaptiveCoverCheck 10 (childHL CertificateCells0d991a929b.thetaAboveCell00003033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf000030333 : adaptiveCoverCheck 10 (childHH CertificateCells0d991a929b.thetaAboveCell00003033) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000310 : adaptiveCoverCheck 12 (childLL (childLH (childHH CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000311 : adaptiveCoverCheck 12 (childLH (childLH (childHH CertificateCells0d991a929b.thetaAboveCell0000))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf00003120 : adaptiveCoverCheck 11 CertificateCells0d991a929b.thetaAboveCell00003120 = true

Gerver sofa dependency batch

• KernelOnly.PartE.E24KC6ProofBatchB39d17cf54d27511.

E24KC6 explicit proof-producing certificate batch.

theorem GerverSofa.PartE.cover_subtree_f27aed8d7652 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102000 = true

theorem GerverSofa.PartE.cover_subtree_005f989c43cb : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102001 = true

theorem GerverSofa.PartE.cover_subtree_9ea21eaf3506 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102002 = true

theorem GerverSofa.PartE.cover_subtree_aecd625dd7fb : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102003 = true

theorem GerverSofa.PartE.cover_subtree_77a434675cac : adaptiveCoverCheck 8 (childLL (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_422f11b7507e : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102010 = true

theorem GerverSofa.PartE.cover_subtree_9333e7948d29 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102011 = true

theorem GerverSofa.PartE.cover_subtree_0e2f446f3080 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102012 = true

theorem GerverSofa.PartE.cover_subtree_07cb153dceed : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102013 = true

theorem GerverSofa.PartE.cover_subtree_334813029f45 : adaptiveCoverCheck 8 (childLH (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_c82ade123eba : adaptiveCoverCheck 8 (childHL (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_b2c2dad45076 : adaptiveCoverCheck 8 (childHH (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.cover_subtree_d0ee7bfc8527 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102100 = true

theorem GerverSofa.PartE.cover_subtree_58a66e346033 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102101 = true

theorem GerverSofa.PartE.cover_subtree_c17867007896 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102102 = true

theorem GerverSofa.PartE.cover_subtree_70f834eb3976 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102103 = true

theorem GerverSofa.PartE.cover_subtree_a226aa051b7b : adaptiveCoverCheck 8 (childLL (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_71a49837eadf : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102112 = true

theorem GerverSofa.PartE.cover_subtree_5a86501aa891 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023102113 = true

theorem GerverSofa.PartE.cover_subtree_1d4344731b0b : adaptiveCoverCheck 8 (childLH (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_3bdba90bbb0c : adaptiveCoverCheck 8 (childHL (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_f8da85ca8892 : adaptiveCoverCheck 8 (childHH (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.cover_subtree_786f313d71e4 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103002 = true

theorem GerverSofa.PartE.cover_subtree_7c7cbd1b1de9 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103003 = true

theorem GerverSofa.PartE.cover_subtree_e95dc4fe2400 : adaptiveCoverCheck 8 (childLL (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_d1ef0fda9310 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103012 = true

theorem GerverSofa.PartE.cover_subtree_334bbbdc1a85 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103013 = true

theorem GerverSofa.PartE.cover_subtree_1b4b2c805488 : adaptiveCoverCheck 8 (childLH (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_d023ef13133b : adaptiveCoverCheck 8 (childHL (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_8107f33bf217 : adaptiveCoverCheck 8 (childHH (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.cover_subtree_e7898c3dadb7 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103102 = true

theorem GerverSofa.PartE.cover_subtree_76677b2fe65f : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103103 = true

theorem GerverSofa.PartE.cover_subtree_b293a3c8540f : adaptiveCoverCheck 8 (childLL (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_a17e19b0274e : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103112 = true

theorem GerverSofa.PartE.cover_subtree_e650c47410b7 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023103113 = true

theorem GerverSofa.PartE.cover_subtree_d40c83c06c06 : adaptiveCoverCheck 8 (childLH (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_759d6e2f1f21 : adaptiveCoverCheck 8 (childHL (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.cover_subtree_695ff4e0f9a2 : adaptiveCoverCheck 8 (childHH (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002310))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells802ef10e9d.thetaAboveCell00002310)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231102 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231103 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231112 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231113 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.cover_subtree_b3ebd2cd2770 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112002 = true

theorem GerverSofa.PartE.cover_subtree_f788d0e2a5ae : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112003 = true

theorem GerverSofa.PartE.cover_subtree_7f7afb8d0a4d : adaptiveCoverCheck 8 (childLL (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_074cd1f5f52c : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112012 = true

theorem GerverSofa.PartE.cover_subtree_dfbe90b65883 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112013 = true

theorem GerverSofa.PartE.cover_subtree_20dd499bd364 : adaptiveCoverCheck 8 (childLH (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_97430f27dc25 : adaptiveCoverCheck 8 (childHL (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_8ea35ca64562 : adaptiveCoverCheck 8 (childHH (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231120 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.cover_subtree_bb7934ab6a6d : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112102 = true

theorem GerverSofa.PartE.cover_subtree_f960ce5080b6 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112103 = true

theorem GerverSofa.PartE.cover_subtree_be8b495598ef : adaptiveCoverCheck 8 (childLL (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_c24cbad7c860 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112112 = true

theorem GerverSofa.PartE.cover_subtree_5030364bf316 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023112113 = true

theorem GerverSofa.PartE.cover_subtree_b9cce4a71b20 : adaptiveCoverCheck 8 (childLH (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_f376dd8d0235 : adaptiveCoverCheck 8 (childHL (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_a9dfb54a5534 : adaptiveCoverCheck 8 (childHH (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231121 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231122 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231123 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.cover_subtree_d1cb21971feb : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113002 = true

theorem GerverSofa.PartE.cover_subtree_3efb79a6f9e0 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113003 = true

theorem GerverSofa.PartE.cover_subtree_f6e1fff83561 : adaptiveCoverCheck 8 (childLL (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_4cb56c792c1b : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113012 = true

theorem GerverSofa.PartE.cover_subtree_d84633da1a8a : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113013 = true

theorem GerverSofa.PartE.cover_subtree_5c601c4361a5 : adaptiveCoverCheck 8 (childLH (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_7c8020e781ad : adaptiveCoverCheck 8 (childHL (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_01c951b510fe : adaptiveCoverCheck 8 (childHH (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231130 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.cover_subtree_195c372ae99b : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113102 = true

theorem GerverSofa.PartE.cover_subtree_d1cce1dbdb65 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113103 = true

theorem GerverSofa.PartE.cover_subtree_f77ed6807865 : adaptiveCoverCheck 8 (childLL (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_93cb889e1841 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113112 = true

theorem GerverSofa.PartE.cover_subtree_dd2e8b0050d0 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000023113113 = true

theorem GerverSofa.PartE.cover_subtree_9bd401d941dd : adaptiveCoverCheck 8 (childLH (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_17ce5f0eb4e5 : adaptiveCoverCheck 8 (childHL (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.cover_subtree_167fbbc5bd30 : adaptiveCoverCheck 8 (childHH (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002311))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231131 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231132 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000231133 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells802ef10e9d.thetaAboveCell00002311)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320002 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320003 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320012 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320013 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.cover_subtree_dc923db2d444 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000032002002 = true

theorem GerverSofa.PartE.cover_subtree_3d16a69d20d7 : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000032002003 = true

theorem GerverSofa.PartE.cover_subtree_80a354cc93c8 : adaptiveCoverCheck 8 (childLL (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_0a679df94e2d : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000032002012 = true

theorem GerverSofa.PartE.cover_subtree_a9518d4839ee : adaptiveCoverCheck 7 CertificateCells802ef10e9d.thetaAboveCell000032002013 = true

theorem GerverSofa.PartE.cover_subtree_69eb32740a9f : adaptiveCoverCheck 8 (childLH (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_0afe6e641e2b : adaptiveCoverCheck 8 (childHL (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_13f8c37ba985 : adaptiveCoverCheck 8 (childHH (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320020 : adaptiveCoverCheck 9 (childLL (childHL CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.cover_subtree_6185ee76a9ce : adaptiveCoverCheck 8 (childLL (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_d6e21884e5c8 : adaptiveCoverCheck 8 (childLH (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_d4ae0081215d : adaptiveCoverCheck 8 (childHL (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_14b21c11f4bb : adaptiveCoverCheck 8 (childHH (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320021 : adaptiveCoverCheck 9 (childLH (childHL CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320022 : adaptiveCoverCheck 9 (childHL (childHL CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320023 : adaptiveCoverCheck 9 (childHH (childHL CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.cover_subtree_0c3f9f5d2a22 : adaptiveCoverCheck 8 (childLL (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_e68bbaf0142c : adaptiveCoverCheck 8 (childLH (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_80b59cc08427 : adaptiveCoverCheck 8 (childHL (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_45a4c3e7665d : adaptiveCoverCheck 8 (childHH (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320030 : adaptiveCoverCheck 9 (childLL (childHH CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.cover_subtree_cabec6ebeaec : adaptiveCoverCheck 8 (childLL (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_f94fc5a27c16 : adaptiveCoverCheck 8 (childLH (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_5a58662c5bc0 : adaptiveCoverCheck 8 (childHL (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.cover_subtree_38aaf5d7c82e : adaptiveCoverCheck 8 (childHH (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00003200))) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320031 : adaptiveCoverCheck 9 (childLH (childHH CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320032 : adaptiveCoverCheck 9 (childHL (childHH CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320033 : adaptiveCoverCheck 9 (childHH (childHH CertificateCells802ef10e9d.thetaAboveCell00003200)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320102 : adaptiveCoverCheck 9 (childHL (childLL CertificateCells802ef10e9d.thetaAboveCell00003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320103 : adaptiveCoverCheck 9 (childHH (childLL CertificateCells802ef10e9d.thetaAboveCell00003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320112 : adaptiveCoverCheck 9 (childHL (childLH CertificateCells802ef10e9d.thetaAboveCell00003201)) = true

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000320113 : adaptiveCoverCheck 9 (childHH (childLH CertificateCells802ef10e9d.thetaAboveCell00003201)) = true