Independent generated check. The main row-14 proof is the readable GenusFiveRow14 construction via ConfigurationBananaTail; this module gives an additional exact replay.

Generated exact replay of the fixed AR row-14 divisor. cells_check and tree_check replay every arithmetic obligation in the kernel.

def AtanasovRanganathan.GenusFiveRow14FixedCover.aff (data : List ℤ) : Utilities.Certificate.ExplicitPotential.AffineForm 12

Decode an integer coefficient list as a twelve-variable affine form: the first entry is the constant and missing entries are zero.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.aff data = { fixedValue := data.getD 0 0, coefficient := fun (coordinate : Fin 12) => data.getD (↑coordinate + 1) 0 }

def AtanasovRanganathan.GenusFiveRow14FixedCover.rowDivisor : Fin 8 → ℤ

The fixed degree-four row-14 divisor, with one chip at each of vertices zero, three, five, and seven.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.rowDivisor vertex = [1, 0, 0, 1, 0, 1, 0, 1].getD (↑vertex) 0

def AtanasovRanganathan.GenusFiveRow14FixedCover.defaultWitness : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

The zero endpoint slopes and zero core potential used for an out-of-range witness-table lookup.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.defaultWitness = { alpha := fun (x : Fin 12) => 0, beta := fun (x : Fin 12) => 0, potential := fun (x : Fin 8) => 0 }

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness0 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 0 for the row-14 closed cover: alpha is zero. beta is zero. The affine potential is zero.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness1 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 1 for the row-14 closed cover: alpha is -1 at slots 0, 6; 1 at slots 7, and zero elsewhere. beta is -1 at slots 7, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness2 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 2 for the row-14 closed cover: alpha is -1 at slots 4; 1 at slots 10, and zero elsewhere. beta is -1 at slots 5, 10, and zero elsewhere. The nonzero affine potentials occur at vertices 2.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness3 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 3 for the row-14 closed cover: alpha is -1 at slots 8, 11, and zero elsewhere. beta is -1 at slots 9; 1 at slots 11, and zero elsewhere. The nonzero affine potentials occur at vertices 4.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness4 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 4 for the row-14 closed cover: alpha is -1 at slots 0, 1, 6; 1 at slots 7, and zero elsewhere. beta is -1 at slots 7; 1 at slots 0, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness5 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 5 for the row-14 closed cover: alpha is -1 at slots 8, 11, and zero elsewhere. beta is -1 at slots 9; 1 at slots 8, and zero elsewhere. The nonzero affine potentials occur at vertices 4.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness6 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 6 for the row-14 closed cover: alpha is -1 at slots 4; 1 at slots 5, and zero elsewhere. beta is -1 at slots 5, 10, and zero elsewhere. The nonzero affine potentials occur at vertices 2.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness7 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 7 for the row-14 closed cover: alpha is -1 at slots 0, 6; 1 at slots 7, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 0, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness8 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 8 for the row-14 closed cover: alpha is -1 at slots 0, 2, 3, 6; 1 at slots 1, 7, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 3, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness9 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 9 for the row-14 closed cover: alpha is -1 at slots 0, 2, 3, 6; 1 at slots 1, 7, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 0, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness10 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 10 for the row-14 closed cover: alpha is -1 at slots 0, 2, 3, 6; 1 at slots 1, 7, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 2, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness11 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 11 for the row-14 closed cover: alpha is -1 at slots 1, 6; 1 at slots 7, and zero elsewhere. beta is -1 at slots 7, and zero elsewhere. The nonzero affine potentials occur at vertices 1.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness12 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 12 for the row-14 closed cover: alpha is -1 at slots 1, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 1, and zero elsewhere. The nonzero affine potentials occur at vertices 1.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness13 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 13 for the row-14 closed cover: alpha is -1 at slots 0, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 0, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness14 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 14 for the row-14 closed cover: alpha is -1 at slots 4, and zero elsewhere. beta is -1 at slots 5, 10; 1 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 2.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness15 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 15 for the row-14 closed cover: alpha is -1 at slots 0, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness16 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 16 for the row-14 closed cover: alpha is -1 at slots 0, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 0, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness17 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 17 for the row-14 closed cover: alpha is -1 at slots 0, 6, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 0, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness18 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 18 for the row-14 closed cover: alpha is -1 at slots 0, 2, 3, 6; 1 at slots 1, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 3, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness19 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 19 for the row-14 closed cover: alpha is -1 at slots 0, 2, 3, 6; 1 at slots 1, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 2, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness20 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 20 for the row-14 closed cover: alpha is -1 at slots 0, 2, 3, 6; 1 at slots 1, and zero elsewhere. beta is -1 at slots 1, 7; 1 at slots 0, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness21 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 21 for the row-14 closed cover: alpha is -1 at slots 1, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness22 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 22 for the row-14 closed cover: alpha is -1 at slots 0, 1, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 0, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness23 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 23 for the row-14 closed cover: alpha is -1 at slots 0, 1, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 0, 1, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witness24 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 24 for the row-14 closed cover: alpha is -1 at slots 8, 11; 1 at slots 9, and zero elsewhere. beta is -1 at slots 9, and zero elsewhere. The nonzero affine potentials occur at vertices 4.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.witnesses : List (Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12)

The twenty-five endpoint-slope and affine-potential witnesses shared by the row-14 closed-cover cells.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell0 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 0 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 3, 0, 4, 0]; cell0_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell0_check : cell0.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell1 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 1 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 5, 0, 4, 0]; cell1_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell1_check : cell1.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell2 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 2 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 3, 0, 4, 0]; cell2_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell2_check : cell2.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell3 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 3 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 5, 0, 4, 0]; cell3_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell3_check : cell3.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell4 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 4 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 3, 0, 7, 0]; cell4_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell4_check : cell4.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell5 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 5 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 5, 0, 7, 0]; cell5_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell5_check : cell5.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell6 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 6 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 3, 0, 7, 0]; cell6_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell6_check : cell6.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell7 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 7 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 5, 0, 7, 0]; cell7_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell7_check : cell7.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell8 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 8 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 3, 0, 8, 0]; cell8_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell8_check : cell8.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell9 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 9 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 3, 0, 9, 0]; cell9_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell9_check : cell9.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell10 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 10 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 3, 0, 10, 0]; cell10_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell10_check : cell10.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell11 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 11 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 5, 0, 8, 0]; cell11_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell11_check : cell11.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell12 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 12 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 5, 0, 10, 0]; cell12_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell12_check : cell12.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell13 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 13 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 5, 0, 9, 0]; cell13_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell13_check : cell13.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell14 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 14 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 3, 0, 8, 0]; cell14_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell14_check : cell14.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell15 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 15 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 3, 0, 9, 0]; cell15_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell15_check : cell15.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell16 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 16 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 5, 0, 8, 0]; cell16_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell16_check : cell16.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell17 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 17 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 5, 0, 9, 0]; cell17_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell17_check : cell17.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell18 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 18 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 3, 0, 10, 0]; cell18_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell18_check : cell18.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell19 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 19 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 5, 0, 10, 0]; cell19_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell19_check : cell19.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell20 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 20 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 2, 0, 3, 0, 4, 0]; cell20_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell20_check : cell20.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell21 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 21 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 2, 0, 5, 0, 4, 0]; cell21_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell21_check : cell21.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell22 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 22 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 6, 0, 3, 0, 4, 0]; cell22_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell22_check : cell22.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell23 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 23 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 6, 0, 5, 0, 4, 0]; cell23_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell23_check : cell23.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell24 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 24 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 2, 0, 3, 0, 13, 0]; cell24_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell24_check : cell24.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell25 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 25 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 2, 0, 5, 0, 13, 0]; cell25_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell25_check : cell25.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell26 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 26 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 6, 0, 3, 0, 13, 0]; cell26_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell26_check : cell26.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell27 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 27 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 6, 0, 5, 0, 13, 0]; cell27_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell27_check : cell27.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell28 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 28 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 3, 0, 4, 0]; cell28_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell28_check : cell28.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell29 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 29 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 5, 0, 4, 0]; cell29_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell29_check : cell29.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell30 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 30 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 3, 0, 7, 0]; cell30_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell30_check : cell30.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell31 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 31 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 5, 0, 7, 0]; cell31_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell31_check : cell31.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell32 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 32 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 3, 0, 8, 0]; cell32_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell32_check : cell32.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell33 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 33 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 3, 0, 9, 0]; cell33_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell33_check : cell33.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell34 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 34 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 5, 0, 8, 0]; cell34_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell34_check : cell34.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell35 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 35 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 5, 0, 9, 0]; cell35_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell35_check : cell35.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell36 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 36 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 3, 0, 10, 0]; cell36_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell36_check : cell36.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell37 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 37 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 5, 0, 10, 0]; cell37_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell37_check : cell37.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell38 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 38 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 14, 0, 3, 0, 4, 0]; cell38_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell38_check : cell38.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell39 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 39 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 14, 0, 5, 0, 4, 0]; cell39_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell39_check : cell39.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell40 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 40 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 14, 0, 3, 0, 13, 0]; cell40_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell40_check : cell40.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell41 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 41 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 14, 0, 5, 0, 13, 0]; cell41_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell41_check : cell41.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell42 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 42 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 3, 0, 16, 0]; cell42_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell42_check : cell42.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell43 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 43 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 3, 0, 16, 0]; cell43_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell43_check : cell43.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell44 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 44 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 3, 0, 16, 0]; cell44_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell44_check : cell44.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell45 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 45 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 3, 0, 17, 0]; cell45_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell45_check : cell45.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell46 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 46 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 3, 0, 17, 0]; cell46_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell46_check : cell46.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell47 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 47 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 3, 0, 17, 0]; cell47_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell47_check : cell47.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell48 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 48 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 3, 0, 18, 0]; cell48_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell48_check : cell48.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell49 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 49 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 3, 0, 18, 0]; cell49_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell49_check : cell49.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell50 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 50 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 3, 0, 18, 0]; cell50_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell50_check : cell50.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell51 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 51 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 3, 0, 19, 0]; cell51_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell51_check : cell51.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell52 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 52 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 3, 0, 19, 0]; cell52_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell52_check : cell52.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell53 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 53 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 3, 0, 19, 0]; cell53_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell53_check : cell53.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell54 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 54 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 3, 0, 20, 0]; cell54_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell54_check : cell54.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell55 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 55 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 3, 0, 20, 0]; cell55_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell55_check : cell55.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell56 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 56 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 3, 0, 20, 0]; cell56_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell56_check : cell56.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell57 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 57 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 2, 0, 3, 0, 22, 0]; cell57_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell57_check : cell57.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell58 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 58 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 6, 0, 3, 0, 22, 0]; cell58_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell58_check : cell58.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell59 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 59 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 14, 0, 3, 0, 22, 0]; cell59_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell59_check : cell59.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell60 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 60 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 23, 0]; cell60_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell60_check : cell60.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell61 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 61 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 13, 0]; cell61_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell61_check : cell61.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell62 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 62 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 17, 0]; cell62_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell62_check : cell62.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell63 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 63 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 18, 0]; cell63_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell63_check : cell63.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell64 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 64 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 19, 0]; cell64_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell64_check : cell64.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell65 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 65 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 20, 0]; cell65_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell65_check : cell65.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell66 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 66 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 23, 0]; cell66_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell66_check : cell66.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell67 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 67 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 13, 0]; cell67_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell67_check : cell67.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell68 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 68 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 17, 0]; cell68_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell68_check : cell68.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell69 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 69 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 18, 0]; cell69_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell69_check : cell69.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell70 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 70 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 19, 0]; cell70_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell70_check : cell70.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell71 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 71 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 20, 0]; cell71_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell71_check : cell71.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell72 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 72 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 2, 0, 5, 0, 13, 0]; cell72_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell72_check : cell72.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell73 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 73 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 14, 0, 5, 0, 13, 0]; cell73_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell73_check : cell73.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell74 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 74 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 23, 0]; cell74_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell74_check : cell74.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell75 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 75 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 13, 0]; cell75_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell75_check : cell75.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell76 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 76 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 17, 0]; cell76_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell76_check : cell76.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell77 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 77 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 18, 0]; cell77_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell77_check : cell77.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell78 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 78 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 19, 0]; cell78_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell78_check : cell78.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell79 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 79 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 20, 0]; cell79_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell79_check : cell79.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell80 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 80 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 6, 0, 5, 0, 13, 0]; cell80_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell80_check : cell80.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell81 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 81 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 5, 0, 16, 0]; cell81_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell81_check : cell81.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell82 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 82 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 5, 0, 16, 0]; cell82_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell82_check : cell82.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell83 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 83 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 2, 0, 5, 0, 22, 0]; cell83_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell83_check : cell83.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell84 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 84 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 6, 0, 5, 0, 22, 0]; cell84_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell84_check : cell84.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell85 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 85 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 5, 0, 16, 0]; cell85_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell85_check : cell85.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell86 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 86 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 14, 0, 5, 0, 22, 0]; cell86_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell86_check : cell86.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell87 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 87 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 24, 0, 4, 0]; cell87_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell87_check : cell87.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell88 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 88 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 24, 0, 7, 0]; cell88_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell88_check : cell88.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell89 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 89 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 24, 0, 8, 0]; cell89_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell89_check : cell89.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell90 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 90 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 24, 0, 9, 0]; cell90_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell90_check : cell90.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell91 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 91 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 2, 0, 24, 0, 10, 0]; cell91_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell91_check : cell91.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell92 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 92 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 2, 0, 24, 0, 4, 0]; cell92_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell92_check : cell92.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell93 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 93 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 2, 0, 24, 0, 13, 0]; cell93_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell93_check : cell93.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell94 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 94 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 24, 0, 4, 0]; cell94_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell94_check : cell94.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell95 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 95 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 24, 0, 7, 0]; cell95_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell95_check : cell95.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell96 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 96 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 24, 0, 8, 0]; cell96_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell96_check : cell96.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell97 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 97 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 24, 0, 9, 0]; cell97_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell97_check : cell97.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell98 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 98 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 14, 0, 24, 0, 10, 0]; cell98_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell98_check : cell98.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell99 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 99 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 14, 0, 24, 0, 13, 0]; cell99_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell99_check : cell99.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell100 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 100 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 14, 0, 24, 0, 13, 0]; cell100_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell100_check : cell100.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell101 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 101 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 14, 0, 5, 0, 13, 0]; cell101_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell101_check : cell101.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell102 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 102 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 24, 0, 4, 0]; cell102_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell102_check : cell102.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell103 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 103 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 24, 0, 7, 0]; cell103_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell103_check : cell103.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell104 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 104 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 24, 0, 8, 0]; cell104_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell104_check : cell104.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell105 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 105 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 24, 0, 9, 0]; cell105_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell105_check : cell105.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell106 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 106 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 6, 0, 24, 0, 10, 0]; cell106_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell106_check : cell106.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell107 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 107 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 6, 0, 24, 0, 4, 0]; cell107_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell107_check : cell107.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell108 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 108 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 14, 0, 24, 0, 4, 0]; cell108_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell108_check : cell108.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell109 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 109 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 12, 6, 0, 24, 0, 13, 0]; cell109_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell109_check : cell109.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell110 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 110 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 6, 0, 5, 0, 13, 0]; cell110_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell110_check : cell110.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell111 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 111 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 23, 0]; cell111_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell111_check : cell111.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell112 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 112 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 13, 0]; cell112_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell112_check : cell112.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell113 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 113 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 17, 0]; cell113_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell113_check : cell113.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell114 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 114 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 18, 0]; cell114_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell114_check : cell114.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell115 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 115 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 19, 0]; cell115_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell115_check : cell115.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell116 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 116 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 20, 0]; cell116_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell116_check : cell116.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell117 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 117 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 2, 0, 24, 0, 13, 0]; cell117_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell117_check : cell117.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell118 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 118 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 2, 0, 24, 0, 16, 0]; cell118_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell118_check : cell118.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell119 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 119 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 24, 0, 16, 0]; cell119_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell119_check : cell119.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell120 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 120 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 24, 0, 17, 0]; cell120_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell120_check : cell120.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell121 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 121 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 24, 0, 18, 0]; cell121_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell121_check : cell121.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell122 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 122 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 24, 0, 19, 0]; cell122_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell122_check : cell122.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell123 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 123 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 6, 0, 24, 0, 20, 0]; cell123_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell123_check : cell123.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell124 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 124 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 6, 0, 24, 0, 22, 0]; cell124_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell124_check : cell124.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell125 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 125 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 24, 0, 16, 0]; cell125_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell125_check : cell125.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell126 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 126 for the fixed row-14 divisor, with 19 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 24, 0, 17, 0]; cell126_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell126_check : cell126.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell127 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 127 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 24, 0, 18, 0]; cell127_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell127_check : cell127.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell128 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 128 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 24, 0, 19, 0]; cell128_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell128_check : cell128.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell129 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 129 for the fixed row-14 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 14, 0, 24, 0, 20, 0]; cell129_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell129_check : cell129.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cell130 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core

Closed-cover cell 130 for the fixed row-14 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 21, 14, 0, 24, 0, 22, 0]; cell130_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cell130_check : cell130.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.cells : List (GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core)

The 131 row-14 closed-cover cells in global index order, covering the full cone of nonnegative edge lengths.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.base : List (Utilities.Certificate.ExplicitPotential.AffineForm 12)

The twelve coordinate forms imposing nonnegativity of every edge length, which define the full domain of the row-14 cover.

Equations

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

def AtanasovRanganathan.GenusFiveRow14FixedCover.splitForms : List (Utilities.Certificate.ExplicitPotential.AffineForm 12)

The 34 homogeneous affine forms whose signs determine branches of the row-14 decision tree; coefficients are indexed by the twelve edge lengths.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm0 : splitForms.getD 0 0 = aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm1 : splitForms.getD 1 0 = aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm2 : splitForms.getD 2 0 = aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm3 : splitForms.getD 3 0 = aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm4 : splitForms.getD 4 0 = aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm5 : splitForms.getD 5 0 = aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm6 : splitForms.getD 6 0 = aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm7 : splitForms.getD 7 0 = aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm8 : splitForms.getD 8 0 = aff [0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm9 : splitForms.getD 9 0 = aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm10 : splitForms.getD 10 0 = aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm11 : splitForms.getD 11 0 = aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm12 : splitForms.getD 12 0 = aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm13 : splitForms.getD 13 0 = aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm14 : splitForms.getD 14 0 = aff [0, 1, -1, 0, -1, 0, 0, -1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm15 : splitForms.getD 15 0 = aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm16 : splitForms.getD 16 0 = aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm17 : splitForms.getD 17 0 = aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm18 : splitForms.getD 18 0 = aff [0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 1]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm19 : splitForms.getD 19 0 = aff [0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 1, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm20 : splitForms.getD 20 0 = aff [0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 1, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm21 : splitForms.getD 21 0 = aff [0, 1, -1, 0, -1, 0, 0, 0, -1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm22 : splitForms.getD 22 0 = aff [0, -1, 1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm23 : splitForms.getD 23 0 = aff [0, 1, -1, -1, 0, 0, 0, 0, -1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm24 : splitForms.getD 24 0 = aff [0, -1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm25 : splitForms.getD 25 0 = aff [0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm26 : splitForms.getD 26 0 = aff [0, 0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm27 : splitForms.getD 27 0 = aff [0, 0, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm28 : splitForms.getD 28 0 = aff [0, 1, -1, -1, 0, 0, 0, -1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm29 : splitForms.getD 29 0 = aff [0, -1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm30 : splitForms.getD 30 0 = aff [0, 0, 1, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm31 : splitForms.getD 31 0 = aff [0, 0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm32 : splitForms.getD 32 0 = aff [0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 1, 0]

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.splitForm33 : splitForms.getD 33 0 = aff [0, -1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0]

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart0 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[5] - length[10] in the row-14 length cone, with leaves selecting cells 0, 1, 2, 3 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart0_check : treePart0.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart1 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[5] - length[10] in the row-14 length cone, with leaves selecting cells 4, 5, 6, 7 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart1_check : treePart1.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart2 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[8] - length[11] in the row-14 length cone, with leaves selecting cells 0, 8, 9, 10, 11, 12, 13 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart2_check : treePart2.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart3 : GenusFiveClosedCover.CompactCellTree

Contradiction leaf using Farkas receipt 158 to exclude the accumulated affine constraints in this row-14 branch.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.treePart3 = AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.absurd 158

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart3_check : treePart3.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart4 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[2] - length[3] in the row-14 length cone, with leaves selecting cells 14, 15, 16, 17, 18, 19 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart4_check : treePart4.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart5 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[7] in the row-14 length cone, with leaves selecting cells 20, 21, 22, 23, 24, 25, 26, 27 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart5_check : treePart5.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart6 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cells 2, 3, 28, 29 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart6_check : treePart6.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart7 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cells 6, 7, 30, 31 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart7_check : treePart7.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart8 : GenusFiveClosedCover.CompactCellTree

Contradiction leaf using Farkas receipt 204 to exclude the accumulated affine constraints in this row-14 branch.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.treePart8 = AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.absurd 204

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart8_check : treePart8.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart9 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cells 14, 15, 16, 17, 32, 33, 34, 35 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart9_check : treePart9.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart10 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cells 15, 17, 18, 19, 33, 35, 36, 37 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart10_check : treePart10.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart11 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[7] in the row-14 length cone, with leaves selecting cells 22, 23, 26, 27, 38, 39, 40, 41 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart11_check : treePart11.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart12 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[10] in the row-14 length cone, with leaves selecting cells 42, 43, 44 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart12_check : treePart12.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart13 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[10] in the row-14 length cone, with leaves selecting cells 45, 46, 47 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart13_check : treePart13.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart14 : GenusFiveClosedCover.CompactCellTree

Contradiction leaf using Farkas receipt 204 to exclude the accumulated affine constraints in this row-14 branch.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.treePart14 = AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.absurd 204

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart14_check : treePart14.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart15 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[2] - length[3] in the row-14 length cone, with leaves selecting cells 48, 49, 50, 51, 52, 53 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart15_check : treePart15.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, 1, -1, 0, -1, 0, 0, -1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart16 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[1] + length[2] + length[6] in the row-14 length cone, with leaves selecting cells 51, 52, 53, 54, 55, 56 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart16_check : treePart16.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, -1, 0, -1, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart17 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 24, 26, 40, 57, 58, 59 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart17_check : treePart17.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart18 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[8] + length[9] in the row-14 length cone, with leaves selecting cells 60, 61, 62, 63, 64, 65 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart18_check : treePart18.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart19 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cell 66 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart19_check : treePart19.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart20 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cell 67 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart20_check : treePart20.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart21 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cell 68 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart21_check : treePart21.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart22 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[1] - length[3] - length[6] in the row-14 length cone, with leaves selecting cells 69, 70, 71 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart22_check : treePart22.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart23 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 25, 41, 72, 73 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart23_check : treePart23.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart24 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[8] + length[9] in the row-14 length cone, with leaves selecting cells 74, 75, 76, 77, 78, 79 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart24_check : treePart24.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart25 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[10] in the row-14 length cone, with leaves selecting cell 66 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart25_check : treePart25.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart26 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[10] in the row-14 length cone, with leaves selecting cell 67 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart26_check : treePart26.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart27 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[10] in the row-14 length cone, with leaves selecting cell 68 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart27_check : treePart27.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart28 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[1] - length[3] - length[6] in the row-14 length cone, with leaves selecting cells 69, 70, 71 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart28_check : treePart28.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart29 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 27, 41, 73, 80 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart29_check : treePart29.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart30 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[8] + length[9] in the row-14 length cone, with leaves selecting cells 62, 63, 64, 65, 81 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart30_check : treePart30.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart31 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[5] in the row-14 length cone, with leaves selecting cell 82 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart31_check : treePart31.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart32 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[5] in the row-14 length cone, with leaves selecting cell 76 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart32_check : treePart32.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart33 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[1] - length[3] - length[6] in the row-14 length cone, with leaves selecting cells 77, 78, 79 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart33_check : treePart33.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart34 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 25, 27, 83, 84 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart34_check : treePart34.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart35 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[8] + length[9] in the row-14 length cone, with leaves selecting cells 68, 69, 70, 71, 85 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart35_check : treePart35.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart36 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[5] + length[10] in the row-14 length cone, with leaves selecting cell 82 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart36_check : treePart36.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart37 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[5] + length[10] in the row-14 length cone, with leaves selecting cell 76 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart37_check : treePart37.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart38 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[1] - length[3] - length[6] in the row-14 length cone, with leaves selecting cells 77, 78, 79 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart38_check : treePart38.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart39 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 27, 41, 84, 86 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart39_check : treePart39.check splitForms farkasReceipts cells (base ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart40 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[7] in the row-14 length cone, with leaves selecting cells 87, 88, 89, 90, 91, 92, 93 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart40_check : treePart40.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart41 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[7] in the row-14 length cone, with leaves selecting cells 1, 5, 11, 12, 13, 21, 25 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart41_check : treePart41.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart42 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[5] in the row-14 length cone, with leaves selecting cells 29, 94 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart42_check : treePart42.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart43 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[1] + length[7] in the row-14 length cone, with leaves selecting cells 94, 95, 96, 97, 98 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart43_check : treePart43.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart44 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[8] + length[11] in the row-14 length cone, with leaves selecting cells 29, 31, 34, 35, 37 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart44_check : treePart44.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart45 : GenusFiveClosedCover.CompactCellTree

Contradiction leaf using Farkas receipt 292 to exclude the accumulated affine constraints in this row-14 branch.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.treePart45 = AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.absurd 292

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart45_check : treePart45.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart46 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 41, 99, 100, 101 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart46_check : treePart46.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart47 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[7] in the row-14 length cone, with leaves selecting cells 102, 103, 104, 105, 106 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart47_check : treePart47.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart48 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[4] + length[10] in the row-14 length cone, with leaves selecting cells 94, 95, 96, 97, 98 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart48_check : treePart48.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart49 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[5] in the row-14 length cone, with leaves selecting cells 3, 29 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart49_check : treePart49.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 1]] ++ [aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart50 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[5] in the row-14 length cone, with leaves selecting cells 7, 31 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart50_check : treePart50.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart51 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] - length[1] + length[7] in the row-14 length cone, with leaves selecting cells 16, 17, 19, 34, 35, 37 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart51_check : treePart51.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 1]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart52 : GenusFiveClosedCover.CompactCellTree

Contradiction leaf using Farkas receipt 302 to exclude the accumulated affine constraints in this row-14 branch.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.treePart52 = AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.absurd 302

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart52_check : treePart52.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, 0, 1])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart53 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[7] in the row-14 length cone, with leaves selecting cells 100, 107, 108, 109 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart53_check : treePart53.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart54 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 27, 41, 101, 110 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart54_check : treePart54.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart55 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[6] in the row-14 length cone, with leaves selecting cells 93, 111, 112, 113, 114, 115, 116, 117 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart55_check : treePart55.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart56 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[6] in the row-14 length cone, with leaves selecting cells 93, 112, 113, 114, 115, 116, 117 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart56_check : treePart56.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart57 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[6] in the row-14 length cone, with leaves selecting cells 113, 114, 115, 116, 118 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart57_check : treePart57.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart58 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 119, 120, 121, 122, 123 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart58_check : treePart58.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart59 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 109, 124 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart59_check : treePart59.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart60 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[6] in the row-14 length cone, with leaves selecting cells 25, 60, 61, 62, 63, 64, 65, 72 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart60_check : treePart60.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart61 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[0] - length[6] in the row-14 length cone, with leaves selecting cells 25, 62, 63, 64, 65, 81, 83 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart61_check : treePart61.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, -1, -1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart62 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[4] - length[5] in the row-14 length cone, with leaves selecting cells 76, 77, 78, 79, 82 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart62_check : treePart62.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart63 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 27, 84 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart63_check : treePart63.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart64 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 125, 126, 127, 128, 129 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart64_check : treePart64.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart65 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 68, 69, 70, 71, 85 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart65_check : treePart65.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart66 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 119, 120, 121, 122, 123 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart66_check : treePart66.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 1, 0]] ++ [aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0]]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart67 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on - length[0] + length[6] in the row-14 length cone, with leaves selecting cells 76, 77, 78, 79, 82 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart67_check : treePart67.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])] ++ [aff [0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 1, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart68 : GenusFiveClosedCover.CompactCellTree

Contradiction leaf using Farkas receipt 346 to exclude the accumulated affine constraints in this row-14 branch.

Equations

• AtanasovRanganathan.GenusFiveRow14FixedCover.treePart68 = AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.absurd 346

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart68_check : treePart68.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0]] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 1, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.treePart69 : GenusFiveClosedCover.CompactCellTree

Subtree splitting on length[1] - length[6] in the row-14 length cone, with leaves selecting cells 27, 41, 84, 86, 100, 109, 124, 130 and Farkas receipts excluding inconsistent sign branches.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.treePart69_check : treePart69.check splitForms farkasReceipts cells (base ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, -1])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0])] ++ [Utilities.Certificate.AffineCover.AffineForm.violation (aff [0, 1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0])]) = true

def AtanasovRanganathan.GenusFiveRow14FixedCover.tree : GenusFiveClosedCover.CompactCellTree

The complete compact decision tree for row 14 on the length cone, assembling 70 subtrees whose cell and Farkas certificates are replayed by the cover checker.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cells_check : (cells.all fun (cell : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core) => cell.certificate.checkClosed 4) = true

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.cells_valid (cell : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row14Core) : cell ∈ cells → cell.certificate.ValidClosed 4

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.tree_check : tree.check splitForms farkasReceipts cells base = true

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.base_holds (length : Fin 12 → ℕ) : Utilities.Certificate.ExplicitPotential.FormsHold base (GenusFiveClosedCover.lengthPoint length)

theorem AtanasovRanganathan.GenusFiveRow14FixedCover.closedConstruction : Configurations.ClosedSubdivisionDharConstruction GenusFiveCoreAtlas.row14Core closedConstruction._proof_1