Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch035.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells9e0a1773d8.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.CertificateCells9e0a1773d8.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells5867c25b03.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.CertificateCells5867c25b03.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsca01649193.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.CertificateCellsca01649193.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells469c6912b9.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.CertificateCells469c6912b9.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellscf0a854a36.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.CertificateCellscf0a854a36.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellscf0a854a36.phiAboveCell110110100100 : AngleCell

Subcell 110110100100 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.CertificateCellseb0fd3147a.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.CertificateCellseb0fd3147a.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellseb0fd3147a.phiAboveCell110110100101 : AngleCell

Subcell 110110100101 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.CertificateCellsa5ae349f6a.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.CertificateCellsa5ae349f6a.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsa5ae349f6a.phiAboveCell110110100102 : AngleCell

Subcell 110110100102 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.CertificateCellsed6c91cc2c.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.CertificateCellsed6c91cc2c.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsed6c91cc2c.phiAboveCell110110100103 : AngleCell

Subcell 110110100103 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.CertificateCellsd58d6f2902.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.CertificateCellsd58d6f2902.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsd58d6f2902.phiAboveCell110110100110 : AngleCell

Subcell 110110100110 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.CertificateCellsaa730af275.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.CertificateCellsaa730af275.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsaa730af275.phiAboveCell110110100111 : AngleCell

Subcell 110110100111 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.CertificateCellse47b06e09b.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.CertificateCellse47b06e09b.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellse47b06e09b.phiAboveCell110110100112 : AngleCell

Subcell 110110100112 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.CertificateCells6d37377041.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.CertificateCells6d37377041.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells6d37377041.phiAboveCell110110100113 : AngleCell

Subcell 110110100113 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.CertificateCellse508f838c4.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.CertificateCellse508f838c4.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells1cda533a6e.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.CertificateCells1cda533a6e.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells3babcd7448.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.CertificateCells3babcd7448.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsbbdc1f9510.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.CertificateCellsbbdc1f9510.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells44a650755e.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.CertificateCells44a650755e.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells44a650755e.phiAboveCell110110101000 : AngleCell

Subcell 110110101000 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.CertificateCells9dff8fd68c.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.CertificateCells9dff8fd68c.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells9dff8fd68c.phiAboveCell110110101001 : AngleCell

Subcell 110110101001 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.CertificateCells0eb9c7dd4e.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.CertificateCells0eb9c7dd4e.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells0eb9c7dd4e.phiAboveCell110110101002 : AngleCell

Subcell 110110101002 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.CertificateCellsa1f8281244.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.CertificateCellsa1f8281244.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsa1f8281244.phiAboveCell110110101003 : AngleCell

Subcell 110110101003 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.CertificateCellsa31bfb0e48.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.CertificateCellsa31bfb0e48.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsa31bfb0e48.phiAboveCell110110101010 : AngleCell

Subcell 110110101010 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.CertificateCellsba54477f25.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.CertificateCellsba54477f25.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsba54477f25.phiAboveCell110110101011 : AngleCell

Subcell 110110101011 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.CertificateCells40378f08af.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.CertificateCells40378f08af.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells40378f08af.phiAboveCell110110101012 : AngleCell

Subcell 110110101012 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.CertificateCellsbef31c9887.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.CertificateCellsbef31c9887.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsbef31c9887.phiAboveCell110110101013 : AngleCell

Subcell 110110101013 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.CertificateCells6837eba069.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.CertificateCells6837eba069.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells21829695a9.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.CertificateCells21829695a9.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsd170a2bed6.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.CertificateCellsd170a2bed6.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells3fed941c0c.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.CertificateCells3fed941c0c.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsb780467ddc.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.CertificateCellsb780467ddc.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellse5752d8306.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.CertificateCellse5752d8306.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells18ee7077e5.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.CertificateCells18ee7077e5.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells481c5d2cb5.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.CertificateCells481c5d2cb5.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCellsc1762ca3ac.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.CertificateCellsc1762ca3ac.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells105558b317.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.CertificateCells105558b317.phiAboveCell11011010 : AngleCell

Subcell 11011010 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.CertificateCells411895cea3.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.CertificateCells411895cea3.phiAboveCell11011011 : AngleCell

Subcell 11011011 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.

Gerver sofa dependency batch

• KernelOnly.PartE.PhiAbove.Leaf00025.
• KernelOnly.PartE.PhiAbove.Leaf00026.
• KernelOnly.PartE.PhiAbove.Leaf00027.
• KernelOnly.PartE.PhiAbove.Leaf00028.
• KernelOnly.PartE.PhiAbove.Leaf00032.
• KernelOnly.PartE.PhiAbove.Leaf00033.
• KernelOnly.PartE.PhiAbove.Leaf00034.
• KernelOnly.PartE.PhiAbove.Leaf00035.
• KernelOnly.PartE.PhiAbove.Leaf00038.
• KernelOnly.PartE.PhiAbove.Leaf00039.
• KernelOnly.PartE.PhiAbove.Leaf00040.
• KernelOnly.PartE.PhiAbove.Leaf00041.
• KernelOnly.PartE.PhiAbove.Leaf00043.
• KernelOnly.PartE.PhiAbove.Leaf00044.
• KernelOnly.PartE.PhiAbove.Leaf00046.
• KernelOnly.PartE.PhiAbove.Leaf00047.
• KernelOnly.PartE.PhiAbove.Leaf00052.
• KernelOnly.PartE.PhiAbove.Leaf00053.
• KernelOnly.PartE.PhiAbove.Leaf00054.
• KernelOnly.PartE.PhiAbove.Leaf00055.
• KernelOnly.PartE.PhiAbove.Leaf00058.
• KernelOnly.PartE.PhiAbove.Leaf00059.
• KernelOnly.PartE.PhiAbove.Leaf00060.
• KernelOnly.PartE.PhiAbove.Leaf00061.
• KernelOnly.PartE.PhiAbove.Leaf00063.
• KernelOnly.PartE.PhiAbove.Leaf00064.
• KernelOnly.PartE.PhiAbove.Leaf00067.
• KernelOnly.PartE.PhiAbove.Leaf00068.
• KernelOnly.PartE.PhiAbove.Leaf00069.
• KernelOnly.PartE.PhiAbove.Leaf00070.
• KernelOnly.PartE.PhiAbove.Leaf00072.
• KernelOnly.PartE.PhiAbove.Leaf00073.
• KernelOnly.PartE.PhiAbove.Leaf00075.
• KernelOnly.PartE.PhiAbove.Leaf00076.
• KernelOnly.PartE.PhiAbove.Leaf00081.

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c0_c0_5_00025

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c0_c0 : adaptiveCoverCheck 5 (childLL (childLL (childLL CertificateCells9e0a1773d8.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c0_c1_5_00026

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c0_c1 : adaptiveCoverCheck 5 (childLH (childLL (childLL CertificateCells5867c25b03.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c0_c2_5_00027

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c0_c2 : adaptiveCoverCheck 5 (childHL (childLL (childLL CertificateCellsca01649193.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c0_c3_5_00028

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c0_c3 : adaptiveCoverCheck 5 (childHH (childLL (childLL CertificateCells469c6912b9.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c0_c0_4_00032

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c0_c0 : adaptiveCoverCheck 4 CertificateCellscf0a854a36.phiAboveCell110110100100 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c0_c1_4_00033

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c0_c1 : adaptiveCoverCheck 4 CertificateCellseb0fd3147a.phiAboveCell110110100101 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c0_c2_4_00034

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c0_c2 : adaptiveCoverCheck 4 CertificateCellsa5ae349f6a.phiAboveCell110110100102 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c0_c3_4_00035

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c0_c3 : adaptiveCoverCheck 4 CertificateCellsed6c91cc2c.phiAboveCell110110100103 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c1_c0_4_00038

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c1_c0 : adaptiveCoverCheck 4 CertificateCellsd58d6f2902.phiAboveCell110110100110 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c1_c1_4_00039

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c1_c1 : adaptiveCoverCheck 4 CertificateCellsaa730af275.phiAboveCell110110100111 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c1_c2_4_00040

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c1_c2 : adaptiveCoverCheck 4 CertificateCellse47b06e09b.phiAboveCell110110100112 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c0_c1_c1_c3_4_00041

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c1_c3 : adaptiveCoverCheck 4 CertificateCells6d37377041.phiAboveCell110110100113 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c1_c2_5_00043

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c2 : adaptiveCoverCheck 5 (childHL (childLH (childLL CertificateCellse508f838c4.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c1_c3_5_00044

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c1_c3 : adaptiveCoverCheck 5 (childHH (childLH (childLL CertificateCells1cda533a6e.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c2_6_00046

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c2 : adaptiveCoverCheck 6 (childHL (childLL CertificateCells3babcd7448.phiAboveCell11011010)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c0_c3_6_00047

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c0_c3 : adaptiveCoverCheck 6 (childHH (childLL CertificateCellsbbdc1f9510.phiAboveCell11011010)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c0_c0_4_00052

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c0_c0 : adaptiveCoverCheck 4 CertificateCells44a650755e.phiAboveCell110110101000 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c0_c1_4_00053

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c0_c1 : adaptiveCoverCheck 4 CertificateCells9dff8fd68c.phiAboveCell110110101001 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c0_c2_4_00054

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c0_c2 : adaptiveCoverCheck 4 CertificateCells0eb9c7dd4e.phiAboveCell110110101002 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c0_c3_4_00055

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c0_c3 : adaptiveCoverCheck 4 CertificateCellsa1f8281244.phiAboveCell110110101003 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c1_c0_4_00058

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c1_c0 : adaptiveCoverCheck 4 CertificateCellsa31bfb0e48.phiAboveCell110110101010 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c1_c1_4_00059

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c1_c1 : adaptiveCoverCheck 4 CertificateCellsba54477f25.phiAboveCell110110101011 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c1_c2_4_00060

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c1_c2 : adaptiveCoverCheck 4 CertificateCells40378f08af.phiAboveCell110110101012 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above

Leaf1101101_c0_c1_c0_c1_c3_4_00061

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c1_c3 : adaptiveCoverCheck 4 CertificateCellsbef31c9887.phiAboveCell110110101013 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c0_c2_5_00063

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c2 : adaptiveCoverCheck 5 (childHL (childLL (childLH CertificateCells6837eba069.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c0_c3_5_00064

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c0_c3 : adaptiveCoverCheck 5 (childHH (childLL (childLH CertificateCells21829695a9.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c1_c0_5_00067

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c1_c0 : adaptiveCoverCheck 5 (childLL (childLH (childLH CertificateCellsd170a2bed6.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c1_c1_5_00068

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c1_c1 : adaptiveCoverCheck 5 (childLH (childLH (childLH CertificateCells3fed941c0c.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c1_c2_5_00069

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c1_c2 : adaptiveCoverCheck 5 (childHL (childLH (childLH CertificateCellsb780467ddc.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c1_c3_5_00070

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c1_c3 : adaptiveCoverCheck 5 (childHH (childLH (childLH CertificateCellse5752d8306.phiAboveCell11011010))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c2_6_00072

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c2 : adaptiveCoverCheck 6 (childHL (childLH CertificateCells18ee7077e5.phiAboveCell11011010)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c1_c3_6_00073

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c1_c3 : adaptiveCoverCheck 6 (childHH (childLH CertificateCells481c5d2cb5.phiAboveCell11011010)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c2_7_00075

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c2 : adaptiveCoverCheck 7 (childHL CertificateCellsc1762ca3ac.phiAboveCell11011010) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c0_c3_7_00076

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c0_c3 : adaptiveCoverCheck 7 (childHH CertificateCells105558b317.phiAboveCell11011010) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c0_c0_5_00081

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c0_c0 : adaptiveCoverCheck 5 (childLL (childLL (childLL CertificateCells411895cea3.phiAboveCell11011011))) = true