Automated Geometry Theorem Generation

Philip Todd, Saltire Software

(RowDefault[, (Spacer1), , (Spacer1), ])  #WolframTechConf

ABSTRACT

We present a method for automatically generating new geometry theorems, suitable for solution using “angle chasing”.  Specifically,  we consider geometry theorems whose premises and conclusion comprise a set of bisector conditions. Each premise and the conclusion can be represented as the rows of a “bisector matrix”: one whose rows contain 1,1,-2 as their only non-zero entries. The existence of a theorem corresponds to rank deficiency in this matrix. 
We initially consider rank deficient matrices which have an underlying graph, whose vertices correspond to matrix rows and whose edges correspond to matrix columns.  We give each edge of the graph (considered in a specific direction) a head-weight equal to the matrix entry in the row corresponding to the vertex adjacent to its head and column corresponding to the edge.  Similarly we give the edge a tail-weight.  With this definition, a bisector matrix with underlying graph is rank deficient if and only if the graph is bicubic and for any cycle the product of head weights equals the product of tail weights. We present a Mathematica program which uses this characterization to identify all possible such matrices for 14 or less rows.  
We present methods of transforming the rank deficient matrices into forms which incorporate line angles in addition to bisectors, and which have columns of more than two non-zero entries, while retaining the rank deficiency.
We present code which takes such transformed matrices as input and outputs geometry theorems in the form of GeometricScenes.

Angle Bisector Theorems

The reflection of the altitude of a triangle in its angle bisector passes through the circumcenter, as illustrated here

Though the description of the theorem has only one explicit mention of “bisector”, the reflection can be expressed as a bisector.
In addition, the circumcenter forms isosceles triangles with the triangle sides.  The base of an isosceles triangle is perpendicular to its angle bisector.
This theorem can therefore be considered as an angle bisector theorem.

We will present a method for discovering new such theorems.

Angles of a triangle

Let the direction of a vector be its angle from the positive x direction.
Then the angle between two vectors is either the difference in their directions, or that difference plus 2π.

Angle Bisectors

γ=((α+β)/2)           α+β-2γ=0

Isosceles Triangles

γ=((α+β)/2)-(π/2)           α+β-2γ=π

A Bisector Theorem

({{θ((Subscript[v, 1]))+θ((Subscript[v, 2]))-2θ((Subscript[v, 5]))==0}, {θ((Subscript[v, 2]))+θ((Subscript[v, 3]))-2θ((Subscript[v, 6]))==0}, {θ((Subscript[v, 3]))+θ((Subscript[v, 4]))-2θ((Subscript[v, 7]))==0}, {θ((Subscript[v, 1]))+θ((Subscript[v, 4]))-2θ((Subscript[v, 8]))==0}, {θ((Subscript[v, 5]))+θ((Subscript[v, 7]))-2θ((Subscript[v, 9]))==0}, {θ((Subscript[v, 6]))+θ((Subscript[v, 8]))-2θ((Subscript[v, 9]))==0}})

(({{ 1 ,  1 ,  0 ,  0 ,  -2 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  1 ,  1 ,  0 ,  0 ,  -2 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  1 ,  1 ,  0 ,  0 ,  -2 ,  0 ,  0 }, { 1 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  -2 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  1 ,  0 ,  -2 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  1 ,  -2 }}))(({{ (Subscript[θ, 1]) }, { (Subscript[θ, 2]) }, { (Subscript[θ, 3]) }, { (Subscript[θ, 4]) }, { (Subscript[θ, 5]) }, { (Subscript[θ, 6]) }, { (Subscript[θ, 7]) }, { (Subscript[θ, 8]) }, { (Subscript[θ, 9]) }}))==(({{ 0 }, { 0 }, { 0 }, { 0 }, { 0 }, { 0 }}))

MatrixRank[(({{1, 1, 0, 0, -2, 0, 0, 0, 0}, {0, 1, 1, 0, 0, -2, 0, 0, 0}, {0, 0, 1, 1, 0, 0, -2, 0, 0}, {1, 0, 0, 1, 0, 0, 0, -2, 0}, {0, 0, 0, 0, 1, 0, 1, 0, -2}, {0, 0, 0, 0, 0, 1, 0, 1, -2}}))]

Isosceles triangles

({{θ((Subscript[w, 1]))+θ((Subscript[w, 2]))-2θ((Subscript[w, 5]))==π}, {θ((Subscript[w, 2]))+θ((Subscript[w, 3]))-2θ((Subscript[w, 6]))==π}, {θ((Subscript[w, 3]))+θ((Subscript[w, 4]))-2θ((Subscript[w, 7]))==-π}, {θ((Subscript[w, 1]))+θ((Subscript[w, 4]))-2θ((Subscript[w, 8]))==π}, {θ((Subscript[w, 5]))+θ((Subscript[w, 7]))-2θ((Subscript[w, 9]))==0}, {θ((Subscript[w, 6]))+θ((Subscript[w, 8]))-2θ((Subscript[w, 10]))==0}, {θ((Subscript[w, 10]))-θ((Subscript[w, 9]))=π/2}})

MatrixRank[(({{1, 1, 0, 0, -2, 0, 0, 0, 0, 0, π}, {0, 1, 1, 0, 0, -2, 0, 0, 0, 0, π}, {0, 0, 1, 1, 0, 0, -2, 0, 0, 0, -π}, {1, 0, 0, 1, 0, 0, 0, -2, 0, 0, π}, {0, 0, 0, 0, 1, 0, 1, 0, -2, 0, 0}, {0, 0, 0, 0, 0, 1, 0, 1, 0, -2, 0}, {0, 0, 0, 0, 0, 0, 0, 0, 1, -1, (π/2)}}))]

Two Bisector Theorems

(({{ 1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  -2 }, { 1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 }, { 0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  1 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  1 ,  0 ,  -2 }}))

(({{ -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  1 }, { -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  1 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  0 ,  0 }, { 0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  1 ,  1 ,  0 ,  0 ,  0 ,  -2 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  1 ,  0 ,  -2 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  -2 ,  0 ,  1 }}))

Matrices have non zero entries in the same positions but the values are not the same.
    (({{ 1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  -2 }, { 1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 }, { 0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  1 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  1 ,  0 ,  -2 }}))        (({{ -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  1 }, { -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  1 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  0 ,  0 }, { 0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  1 ,  1 ,  0 ,  0 ,  0 ,  -2 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  1 ,  0 ,  -2 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  -2 ,  0 ,  1 }}))

Both have rank 7 (out of a possible 8).
How many such matrices are there?

3^8

How many have rank 7?
33

Shape Graphs

If a matrix has two non-zero elements per columns we can define a shape graph whose edges correspond to the columns.
    (({{ 1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  -2 }, { 1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 }, { 0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  1 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  1 ,  0 ,  -2 }}))

Graph[{1\[UndirectedEdge]2,2\[UndirectedEdge]3,3\[UndirectedEdge]4,4\[UndirectedEdge]5,5\[UndirectedEdge]6,6\[UndirectedEdge]7,7\[UndirectedEdge]8,1\[UndirectedEdge]6,2\[UndirectedEdge]5,3\[UndirectedEdge]8,4\[UndirectedEdge]7,1\[UndirectedEdge]8}]

Decorated Shape Graphs

Add an arrow to indicate the location of the -2
    (({{ 1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  -2 }, { 1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 }, { 0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  1 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  1 ,  0 ,  -2 }}))

The matrix for the second theorem looks like this..
(({{ -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  1 }, { -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  1 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  0 ,  0 }, { 0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  1 ,  1 ,  0 ,  0 ,  0 ,  -2 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  1 ,  0 ,  -2 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  -2 ,  0 ,  1 }}))

These are clearly not rotated versions of each other
How about the other 31?

We can transform each of our 33 solutions using the GraphAutomorphismGroup of the cube to eliminate duplicates, yielding these four non-isomorphic matrices:

({{matrix, , , , }, {rotations, 12, 12, 6, 3}})

Here are theorems to go with the two new ones.

Generalize matrix

Consider matrices with 2 non-zero entries per column and 3 per row, consisting of 2, -1,-1.  
When are they rank-deficient?
Consider the associated graph .. each vertex is degree 3.  Hence a cubic graph
There are 5 connected cubic graphs on 8 vertices.

Rank deficient matrices

({{Graph, , , , , }, {RD Matrices, 0, 0, 33 (4), 0, 0}})

Why?

Rank deficient matrix characterization (proof sketch)

A matrix with underlying connected graph is rank deficient if and only if the matrix corresponding to any graph cycle has zero determinant.

Rows and columns can be arranged so the cycle’s matrix is this:

determinant(({{(Subscript[a, 1]), 0, 0, ⋯, (Subscript[b, n])}, {(Subscript[b, 1]), (Subscript[a, 2]), 0, ⋯, 0}, {0, (Subscript[b, 2]), (Subscript[a, 3]), ⋯, 0}, {⋮, ⋮, ⋮, ⋱, 0}, {0, 0, 0, ⋯, (Subscript[a, n])}}))       

({{n Even, (Subscript[a, 1])(Subscript[a, 2])(Subscript[a, 3])(Subscript[⋯a, n])-(Subscript[b, 1])(Subscript[b, 2])(Subscript[b, 3])(Subscript[⋯b, n])}, {n Odd, (Subscript[a, 1])(Subscript[a, 2])(Subscript[a, 3])(Subscript[⋯a, n])+(Subscript[b, 1])(Subscript[b, 2])(Subscript[b, 3])(Subscript[⋯b, n])}})

If possible values of (Subscript[a, i]) and (Subscript[b, i]) are 1, 1 and -2, there can be no odd cycles.

Further, even cycles must contain the same number of -2’s among the a’s as among the b’s.

Rank Deficient Bisector Matrices

We need these characteristics

The graph only has cycles of even length (bicubic).

If you traverse any cycle, you encounter as many arrows in your direction of travel as against it

Other values of n

6

10

12     

146 matrices

14     

13 bicubic graphs 807 matrices

Merging sides

Matrix->Geometry

(({{ 1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 ,  -2 }, { 1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 }, { 0 ,  0 ,  1 ,  -2 ,  0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  1 ,  -2 ,  0 ,  1 ,  0 ,  0 ,  0 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  -2 ,  1 ,  0 ,  0 ,  0 ,  1 ,  0 }, { 0 ,  0 ,  0 ,  0 ,  0 ,  0 ,  1 ,  0 ,  0 ,  1 ,  0 ,  -2 }}))

Finding New Theorems

Create arrow-decorated graph of rank-deficient matrix.

Identify cycles of arrow-free edges.

Create cyclic polygons.

Add parallel constraints for sides which are shared .

Create a sequence of reflections / bisections along with parallel constraints to complete the description.

{{"cyclicPolygonCenter",{b,c,d,e,f,g,h,p},a},{"parallel",{{e,d}},{{h,g}}},
{"parallel",{{f,e}},{{p,h}}},
{"bisector",{{b,c}},{{g,f}},L1},{"bisector",{{d,c}},{{b,p}},L2},
{"conclusion",{L2},{L1}}}

Textual form of description

"Let bcdefghp be a cyclic octagon with centre a. Let ed be parallel to hg. Let fe be parallel to ph. Let L1 be the angle bisector of bc and gf. Let L2 be the angle bisector of dc and bp."

(Conclusion will be added later)
Graphical form (conclusion indicated in red)

GeometricScene[{{a,b,c,d,e,f,g,h,p,q,r,s,t},{}},{Line[{p,b}],Line[{b,c}],Line[{c,d}],Line[{d,e}],Line[{e,f}],Line[{f,g}],Line[{g,h}],Line[{h,p}],CircleThrough[{b,c,d,e,f,g,h,p},a],GeometricAssertion[{Line[{e,d}],Line[{h,g}]},"Parallel"],GeometricAssertion[{Line[{f,e}],Line[{p,h}]},"Parallel"],L1==AngleBisector[{b,q,f}],q∈InfiniteLine[{b,c}],q∈InfiniteLine[{g,f}],L2==AngleBisector[{c,r,b}],r∈InfiniteLine[{d,c}],r∈InfiniteLine[{b,p}],s∈L2,t∈L1,L2,L1},{}]

Random Theorem Generator

Picks a rank-deficient matrix at random

Randomly merges pairs of columns (=merging lines).

Interprets as a theorem.

Creates statement (without conclusion)

Creates a diagram (abandons the example and starts again if this step takes too long) .

Measures “conclusion angle” from the diagram and completes statement.

({{   }})

({{}})

philt@saltire.com

p6={{{1,7,6},{2,8,1},{2,3,9},{3,4,7},{4,8,5},{5,9,6}},{{1,7,6},{1,2,8},{2,9,3},{4,7,3},{4,5,8},{5,9,6}}};

p8={{{1,9,8},{2,10,1},{2,3,11},{3,4,12},{4,10,5},{5,9,6},{7,12,6},{7,11,8}},{{1,9,8},{2,10,1},{2,3,11},{3,12,4},{5,10,4},{5,6,9},{6,12,7},{7,11,8}},{{1,9,8},{1,2,10},{2,11,3},{4,12,3},{4,5,10},{5,9,6},{7,12,6},{7,11,8}},{{1,9,8},{1,10,2},{3,11,2},{3,12,4},{5,10,4},{5,9,6},{7,12,6},{7,11,8}}};

p10a={{{1,11,10},{2,12,1},{2,3,13},{3,4,14},{4,5,15},{5,6,11},{6,12,7},{7,13,8},{9,14,8},{9,15,10}},{{1,11,10},{2,12,1},{2,3,13},{3,14,4},{4,15,5},{6,11,5},{7,12,6},{7,8,13},{8,14,9},{9,15,10}},{{1,11,10},{2,12,1},{2,13,3},{4,14,3},{4,5,15},{5,6,11},{6,12,7},{8,13,7},{8,14,9},{9,15,10}},{{1,11,10},{2,12,1},{2,13,3},{3,4,14},{4,15,5},{6,11,5},{7,12,6},{7,13,8},{8,9,14},{9,15,10}},{{1,11,10},{2,12,1},{2,13,3},{3,14,4},{4,5,15},{6,11,5},{7,12,6},{7,13,8},{8,14,9},{9,10,15}},{{1,11,10},{1,2,12},{2,3,13},{3,4,14},{4,15,5},{6,11,5},{6,7,12},{7,8,13},{8,9,14},{9,15,10}},{{1,11,10},{1,2,12},{2,3,13},{3,14,4},{4,5,15},{6,11,5},{6,7,12},{7,8,13},{8,14,9},{9,10,15}},{{1,11,10},{1,2,12},{2,13,3},{4,14,3},{4,15,5},{6,11,5},{6,7,12},{7,13,8},{9,14,8},{9,15,10}},{{1,11,10},{1,2,12},{2,13,3},{3,4,14},{4,5,15},{6,11,5},{6,7,12},{7,13,8},{8,9,14},{9,10,15}},{{1,11,10},{1,12,2},{3,13,2},{3,14,4},{5,15,4},{5,11,6},{7,12,6},{7,13,8},{9,14,8},{9,15,10}},{{1,11,10},{1,12,2},{3,13,2},{3,14,4},{4,5,15},{6,11,5},{6,12,7},{8,13,7},{8,14,9},{9,10,15}},{{1,11,10},{1,12,2},{2,3,13},{3,4,14},{4,5,15},{6,11,5},{6,12,7},{7,8,13},{8,9,14},{9,10,15}},{{10,1,11},{1,2,12},{2,3,13},{3,4,14},{4,5,15},{5,6,11},{6,7,12},{7,8,13},{8,9,14},{9,10,15}}};

p10b={{{1,11,10},{2,12,1},{2,3,13},{4,14,3},{4,15,5},{5,6,11},{7,14,6},{7,15,8},{8,12,9},{9,13,10}},{{1,11,10},{2,12,1},{2,3,13},{3,4,14},{4,5,15},{5,6,11},{6,7,14},{7,8,15},{8,12,9},{9,13,10}},{{1,11,10},{2,12,1},{2,3,13},{3,4,14},{4,15,5},{5,11,6},{7,14,6},{8,15,7},{8,12,9},{9,13,10}},{{1,11,10},{1,2,12},{2,13,3},{4,14,3},{5,15,4},{5,6,11},{6,7,14},{7,15,8},{8,9,12},{9,13,10}},{{1,11,10},{1,2,12},{2,13,3},{4,14,3},{4,5,15},{5,11,6},{7,14,6},{7,8,15},{8,9,12},{9,13,10}},{{10,1,11},{2,12,1},{2,13,3},{4,14,3},{4,15,5},{5,6,11},{7,14,6},{7,15,8},{9,12,8},{9,13,10}}};

p12a={{{1,13,12},{2,14,1},{3,15,2},{3,16,4},{4,5,17},{5,18,6},{7,14,6},{7,8,13},{9,16,8},{9,15,10},{10,18,11},{11,17,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,5,17},{5,6,18},{6,14,7},{7,13,8},{9,16,8},{9,15,10},{11,18,10},{11,17,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,5,17},{5,18,6},{7,14,6},{7,8,13},{8,9,16},{9,10,15},{10,18,11},{11,17,12}},{{1,13,12},{2,14,1},{2,3,15},{3,16,4},{4,5,17},{5,6,18},{7,14,6},{7,8,13},{8,16,9},{9,15,10},{10,18,11},{12,17,11}},{{1,13,12},{2,14,1},{2,3,15},{3,16,4},{4,17,5},{6,18,5},{7,14,6},{7,8,13},{8,16,9},{9,15,10},{11,18,10},{11,17,12}},{{1,13,12},{1,2,14},{2,3,15},{3,4,16},{4,5,17},{5,6,18},{6,7,14},{7,13,8},{8,16,9},{10,15,9},{10,18,11},{12,17,11}},{{1,13,12},{1,2,14},{2,3,15},{3,4,16},{4,17,5},{6,18,5},{6,7,14},{7,13,8},{8,16,9},{10,15,9},{11,18,10},{11,17,12}},{{1,13,12},{1,2,14},{2,3,15},{3,16,4},{5,17,4},{5,6,18},{6,7,14},{7,13,8},{9,16,8},{9,10,15},{10,11,18},{11,17,12}},{{1,13,12},{1,14,2},{3,15,2},{3,16,4},{5,17,4},{5,18,6},{7,14,6},{7,13,8},{9,16,8},{9,15,10},{11,18,10},{11,17,12}},{{1,13,12},{1,14,2},{3,15,2},{3,16,4},{4,5,17},{5,6,18},{7,14,6},{7,13,8},{9,16,8},{9,15,10},{10,11,18},{11,12,17}},{{1,13,12},{1,14,2},{2,3,15},{3,4,16},{4,5,17},{5,6,18},{7,14,6},{7,13,8},{8,9,16},{9,10,15},{10,11,18},{11,12,17}},{{12,1,13},{2,14,1},{2,3,15},{3,4,16},{4,5,17},{5,6,18},{6,14,7},{7,8,13},{8,16,9},{10,15,9},{10,18,11},{12,17,11}},{{12,1,13},{1,2,14},{2,3,15},{3,4,16},{4,5,17},{5,6,18},{6,7,14},{7,8,13},{8,9,16},{9,10,15},{10,11,18},{11,12,17}},{{12,1,13},{1,2,14},{2,3,15},{3,4,16},{4,17,5},{6,18,5},{6,7,14},{7,8,13},{8,9,16},{9,10,15},{10,18,11},{12,17,11}}};

p12b={{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,5,17},{5,6,18},{6,14,7},{7,15,8},{9,21,8},{9,17,10},{11,18,10},{11,21,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,5,17},{5,6,18},{6,14,7},{7,15,8},{8,9,21},{10,17,9},{10,18,11},{11,12,21}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,5,17},{5,18,6},{7,14,6},{7,8,15},{8,9,21},{9,10,17},{10,18,11},{11,21,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,17,5},{6,18,5},{6,14,7},{7,15,8},{9,21,8},{10,17,9},{10,18,11},{11,21,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,17,5},{5,6,18},{7,14,6},{7,8,15},{8,9,21},{9,17,10},{10,11,18},{11,21,12}},{{1,13,12},{2,14,1},{2,15,3},{3,13,4},{5,17,4},{5,6,18},{7,14,6},{7,15,8},{8,9,21},{9,17,10},{10,18,11},{12,21,11}},{{1,13,12},{2,14,1},{2,15,3},{3,13,4},{5,17,4},{5,6,18},{7,14,6},{7,15,8},{8,21,9},{10,17,9},{10,11,18},{11,21,12}},{{1,13,12},{1,2,14},{3,15,2},{3,4,13},{4,17,5},{5,6,18},{6,7,14},{8,15,7},{8,9,21},{9,17,10},{10,11,18},{11,21,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{5,6,18},{6,7,14},{7,8,15},{8,9,21},{9,17,10},{10,18,11},{12,21,11}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{5,6,18},{6,7,14},{7,8,15},{8,21,9},{10,17,9},{10,11,18},{11,21,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{5,18,6},{6,14,7},{8,15,7},{9,21,8},{9,17,10},{11,18,10},{11,21,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{5,18,6},{6,14,7},{8,15,7},{8,9,21},{10,17,9},{10,18,11},{11,12,21}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,5,17},{5,6,18},{6,14,7},{8,15,7},{8,9,21},{9,10,17},{10,11,18},{11,12,21}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,5,17},{5,6,18},{6,14,7},{8,15,7},{8,21,9},{9,17,10},{11,18,10},{12,21,11}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,17,5},{6,18,5},{6,14,7},{8,15,7},{8,9,21},{9,17,10},{11,18,10},{11,12,21}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,17},{5,6,18},{6,7,14},{7,15,8},{8,9,21},{9,17,10},{11,18,10},{11,12,21}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,17},{5,6,18},{6,7,14},{7,15,8},{8,21,9},{10,17,9},{10,18,11},{12,21,11}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,17,5},{6,18,5},{6,7,14},{7,15,8},{9,21,8},{9,17,10},{11,18,10},{11,21,12}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,17,5},{6,18,5},{6,7,14},{7,15,8},{8,9,21},{10,17,9},{10,18,11},{11,12,21}},{{1,13,12},{1,14,2},{3,15,2},{3,13,4},{5,17,4},{5,6,18},{6,14,7},{8,15,7},{8,9,21},{9,17,10},{10,18,11},{12,21,11}},{{1,13,12},{1,14,2},{3,15,2},{3,13,4},{5,17,4},{5,18,6},{7,14,6},{7,15,8},{9,21,8},{9,17,10},{11,18,10},{11,21,12}},{{1,13,12},{1,14,2},{3,15,2},{3,13,4},{4,5,17},{5,6,18},{7,14,6},{7,15,8},{8,9,21},{9,10,17},{10,11,18},{11,12,21}},{{1,13,12},{1,14,2},{3,15,2},{3,13,4},{4,5,17},{5,6,18},{7,14,6},{7,15,8},{8,21,9},{9,17,10},{11,18,10},{12,21,11}},{{1,13,12},{1,14,2},{3,15,2},{3,13,4},{4,17,5},{6,18,5},{7,14,6},{7,15,8},{8,9,21},{9,17,10},{11,18,10},{11,12,21}},{{1,13,12},{1,14,2},{2,3,15},{4,13,3},{4,5,17},{5,6,18},{6,14,7},{7,8,15},{8,9,21},{9,17,10},{11,18,10},{11,12,21}},{{1,13,12},{1,14,2},{2,3,15},{4,13,3},{4,5,17},{5,6,18},{6,14,7},{7,8,15},{8,21,9},{10,17,9},{10,18,11},{12,21,11}},{{1,13,12},{1,14,2},{2,3,15},{4,13,3},{4,17,5},{6,18,5},{6,14,7},{7,8,15},{8,9,21},{10,17,9},{10,18,11},{11,12,21}},{{12,1,13},{1,2,14},{2,3,15},{3,4,13},{4,5,17},{5,6,18},{6,7,14},{7,8,15},{8,9,21},{9,10,17},{10,11,18},{11,12,21}},{{12,1,13},{1,2,14},{2,3,15},{3,4,13},{4,5,17},{5,6,18},{6,7,14},{7,8,15},{8,21,9},{9,17,10},{11,18,10},{12,21,11}},{{12,1,13},{1,2,14},{2,3,15},{3,4,13},{4,17,5},{6,18,5},{6,7,14},{7,8,15},{8,9,21},{9,17,10},{11,18,10},{11,12,21}},{{12,1,13},{1,14,2},{3,15,2},{3,4,13},{4,5,17},{5,6,18},{6,14,7},{8,15,7},{8,21,9},{9,17,10},{11,18,10},{12,21,11}},{{12,1,13},{1,14,2},{3,15,2},{3,4,13},{4,17,5},{6,18,5},{6,14,7},{8,15,7},{8,9,21},{9,17,10},{11,18,10},{11,12,21}},{{12,13,1},{1,14,2},{3,15,2},{4,13,3},{4,5,17},{5,6,18},{6,7,14},{7,8,15},{8,21,9},{9,17,10},{11,18,10},{12,21,11}}};

p12c={{{1,13,12},{2,14,1},{2,3,15},{4,16,3},{4,5,14},{5,6,18},{6,16,7},{7,8,20},{8,18,9},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{4,16,3},{4,5,14},{5,6,18},{6,16,7},{7,20,8},{9,18,8},{9,10,13},{10,20,11},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{4,16,3},{4,5,14},{5,18,6},{7,16,6},{7,8,20},{8,18,9},{9,10,13},{10,20,11},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{6,18,5},{6,7,16},{7,8,20},{8,18,9},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{6,18,5},{6,7,16},{7,20,8},{9,18,8},{9,10,13},{10,20,11},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{5,6,18},{6,16,7},{8,20,7},{8,9,18},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{5,18,6},{7,16,6},{8,20,7},{8,9,18},{9,10,13},{10,20,11},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{5,18,6},{7,16,6},{7,8,20},{8,18,9},{10,13,9},{10,11,20},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{5,18,6},{7,16,6},{7,20,8},{9,18,8},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,16,4},{5,14,4},{5,6,18},{6,16,7},{7,8,20},{8,18,9},{10,13,9},{10,11,20},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,16,4},{5,14,4},{5,6,18},{6,16,7},{7,20,8},{9,18,8},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,16,4},{5,14,4},{5,18,6},{7,16,6},{7,8,20},{8,18,9},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{2,14,1},{2,3,15},{3,16,4},{5,14,4},{5,18,6},{7,16,6},{7,20,8},{9,18,8},{9,10,13},{10,20,11},{11,15,12}},{{1,13,12},{1,2,14},{2,3,15},{3,4,16},{4,5,14},{5,6,18},{6,7,16},{7,8,20},{8,9,18},{9,13,10},{10,20,11},{12,15,11}},{{1,13,12},{1,2,14},{2,3,15},{3,4,16},{4,5,14},{5,18,6},{6,16,7},{8,20,7},{9,18,8},{9,13,10},{10,20,11},{12,15,11}},{{1,13,12},{1,2,14},{2,3,15},{3,16,4},{4,14,5},{6,18,5},{7,16,6},{7,8,20},{8,9,18},{9,13,10},{10,20,11},{12,15,11}},{{1,13,12},{1,2,14},{2,15,3},{4,16,3},{4,5,14},{5,6,18},{6,16,7},{8,20,7},{8,9,18},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{1,2,14},{2,15,3},{4,16,3},{4,5,14},{5,18,6},{7,16,6},{7,8,20},{8,18,9},{10,13,9},{10,11,20},{11,15,12}},{{1,13,12},{1,2,14},{2,15,3},{4,16,3},{4,5,14},{5,18,6},{7,16,6},{7,20,8},{9,18,8},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{1,2,14},{2,15,3},{3,4,16},{4,14,5},{6,18,5},{6,7,16},{8,20,7},{8,9,18},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{1,14,2},{3,15,2},{3,16,4},{5,14,4},{5,18,6},{7,16,6},{7,20,8},{9,18,8},{9,13,10},{11,20,10},{11,15,12}},{{1,13,12},{1,14,2},{2,3,15},{3,4,16},{5,14,4},{5,18,6},{6,7,16},{7,8,20},{9,18,8},{9,13,10},{10,11,20},{11,12,15}},{{12,1,13},{2,14,1},{2,3,15},{4,16,3},{4,5,14},{5,6,18},{6,16,7},{7,8,20},{8,18,9},{9,10,13},{10,20,11},{12,15,11}},{{12,1,13},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{6,18,5},{6,7,16},{7,8,20},{8,18,9},{9,10,13},{10,20,11},{12,15,11}},{{12,1,13},{2,14,1},{2,3,15},{3,4,16},{4,14,5},{5,6,18},{6,16,7},{8,20,7},{8,9,18},{9,10,13},{10,20,11},{12,15,11}},{{12,1,13},{1,2,14},{2,3,15},{3,4,16},{4,5,14},{5,6,18},{6,7,16},{7,8,20},{8,9,18},{9,10,13},{10,11,20},{11,12,15}},{{12,1,13},{1,2,14},{2,15,3},{4,16,3},{4,5,14},{5,6,18},{6,16,7},{8,20,7},{8,9,18},{9,10,13},{10,20,11},{12,15,11}}};

p12d={{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,5,17},{6,18,5},{6,19,7},{7,8,15},{9,18,8},{9,19,10},{10,14,11},{11,17,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,5,17},{5,6,18},{6,7,19},{7,8,15},{8,9,18},{9,10,19},{10,14,11},{11,17,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,5,17},{5,6,18},{6,19,7},{7,15,8},{9,18,8},{10,19,9},{10,14,11},{11,17,12}},{{1,13,12},{2,14,1},{2,15,3},{3,13,4},{5,17,4},{6,18,5},{7,19,6},{7,8,15},{8,9,18},{9,19,10},{10,14,11},{11,17,12}},{{1,13,12},{2,14,1},{2,15,3},{3,13,4},{5,17,4},{6,18,5},{6,7,19},{7,15,8},{9,18,8},{9,10,19},{10,14,11},{11,17,12}},{{1,13,12},{2,14,1},{2,15,3},{3,13,4},{5,17,4},{5,6,18},{7,19,6},{7,15,8},{8,9,18},{10,19,9},{10,14,11},{11,17,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{6,18,5},{6,19,7},{7,8,15},{9,18,8},{9,19,10},{10,11,14},{11,17,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{5,6,18},{6,7,19},{7,8,15},{8,9,18},{9,10,19},{10,11,14},{11,17,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{5,17,4},{5,6,18},{6,19,7},{7,15,8},{9,18,8},{10,19,9},{10,11,14},{11,17,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,5,17},{6,18,5},{6,7,19},{7,8,15},{8,18,9},{9,19,10},{11,14,10},{11,12,17}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,5,17},{5,6,18},{6,7,19},{7,15,8},{8,18,9},{10,19,9},{11,14,10},{11,12,17}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,5,17},{5,6,18},{6,19,7},{8,15,7},{8,9,18},{9,19,10},{11,14,10},{11,12,17}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,17},{6,18,5},{6,7,19},{7,8,15},{8,18,9},{9,19,10},{10,14,11},{12,17,11}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,17},{5,6,18},{6,7,19},{7,15,8},{8,18,9},{10,19,9},{10,14,11},{12,17,11}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,17},{5,6,18},{6,19,7},{8,15,7},{8,9,18},{9,19,10},{10,14,11},{12,17,11}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,17,5},{6,18,5},{7,19,6},{7,8,15},{8,9,18},{9,19,10},{10,11,14},{11,17,12}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,17,5},{6,18,5},{6,7,19},{7,15,8},{9,18,8},{9,10,19},{10,11,14},{11,17,12}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,17,5},{5,6,18},{7,19,6},{7,15,8},{8,9,18},{10,19,9},{10,11,14},{11,17,12}},{{1,13,12},{1,14,2},{2,3,15},{4,13,3},{4,17,5},{6,18,5},{6,19,7},{7,8,15},{9,18,8},{9,19,10},{11,14,10},{11,17,12}},{{1,13,12},{1,14,2},{2,3,15},{4,13,3},{4,17,5},{5,6,18},{6,7,19},{7,8,15},{8,9,18},{9,10,19},{11,14,10},{11,17,12}},{{1,13,12},{1,14,2},{2,3,15},{4,13,3},{4,17,5},{5,6,18},{6,19,7},{7,15,8},{9,18,8},{10,19,9},{11,14,10},{11,17,12}}};

p12e={{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,14,5},{5,15,6},{7,19,6},{8,20,7},{8,9,21},{9,10,19},{10,20,11},{11,21,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,14,5},{5,15,6},{7,19,6},{7,8,20},{8,9,21},{9,19,10},{10,20,11},{12,21,11}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,14,5},{5,15,6},{7,19,6},{7,8,20},{8,21,9},{10,19,9},{10,11,20},{11,21,12}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,14,5},{5,15,6},{6,7,19},{7,8,20},{8,9,21},{9,10,19},{10,11,20},{11,12,21}},{{1,13,12},{2,14,1},{2,3,15},{3,4,13},{4,14,5},{5,15,6},{6,7,19},{7,8,20},{8,21,9},{9,19,10},{11,20,10},{12,21,11}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,14,5},{6,15,5},{7,19,6},{7,8,20},{8,9,21},{9,19,10},{10,20,11},{12,21,11}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,14,5},{6,15,5},{7,19,6},{7,8,20},{8,21,9},{10,19,9},{10,11,20},{11,21,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,14,5},{6,15,5},{6,7,19},{8,20,7},{8,21,9},{9,10,19},{11,20,10},{11,21,12}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,14,5},{6,15,5},{6,7,19},{7,8,20},{8,9,21},{9,10,19},{10,11,20},{11,12,21}},{{1,13,12},{1,2,14},{2,3,15},{3,13,4},{4,14,5},{6,15,5},{6,7,19},{7,8,20},{8,21,9},{9,19,10},{11,20,10},{12,21,11}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,14},{5,15,6},{7,19,6},{7,8,20},{8,21,9},{10,19,9},{10,11,20},{11,21,12}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,14},{5,15,6},{6,7,19},{7,8,20},{8,9,21},{9,10,19},{10,11,20},{11,12,21}},{{1,13,12},{1,2,14},{2,15,3},{4,13,3},{4,5,14},{5,15,6},{6,7,19},{7,8,20},{8,21,9},{9,19,10},{11,20,10},{12,21,11}},{{12,1,13},{1,2,14},{2,3,15},{3,4,13},{4,5,14},{5,6,15},{6,7,19},{7,8,20},{8,9,21},{9,10,19},{10,11,20},{11,12,21}},{{12,1,13},{1,2,14},{2,3,15},{3,4,13},{4,5,14},{5,6,15},{6,7,19},{7,8,20},{8,21,9},{9,19,10},{11,20,10},{12,21,11}},{{12,1,13},{1,2,14},{2,15,3},{3,13,4},{5,14,4},{6,15,5},{6,7,19},{7,8,20},{8,21,9},{9,19,10},{11,20,10},{12,21,11}}};
createVanillaGraphEdges[lst_]:=Module[{m,n,ret,pos,u,v,w,vlabels,vsizes,nextv,k,headArrow,tailArrow},n=Max[lst];
ret={};
m=Length[lst];
vlabels={};
vsizes={};
nextv=m+1;
For[i=1,i<=n,i++,pos=Position[lst,i];
If[Length[pos]>0,u=pos[[1]][[1]];
If[Length[pos]==2,v=pos[[2]][[1]];
AppendTo[ret,u<->v]];
];];
Return[{ret,vlabels,vsizes}];]


createVanillaTheoremGraph[lst_]:=Module[{g,ev},ev=createVanillaGraphEdges[lst];
g=Graph[ev[[1]],VertexLabels->ev[[2]],VertexSize->ev[[3]]];
Return[g];]

otherUnarrowElement[triple_,el_]:=Module[{},If[triple[[1]]==el,Return[triple[[2]]],Return[triple[[1]]]];]

orderUnarrowCycle[lst_,cc_]:=Module[{i,j,ret,ret2,u,v,w,pos,p,q,rem,len,tt},ret2={};
len=Length[cc];
u=cc[[len]];
For[i=1,i<=len,i++,v=cc[[i]];
For[j=1,j<=Length[lst],j++,tt=lst[[j]];
If[tt[[1]]==u&&tt[[2]]==v,AppendTo[ret2,j]];
If[tt[[1]]==v&&tt[[2]]==u,AppendTo[ret2,j]];];
u=v;];
Return[{cc,ret2}];]

unarrowGraph[lst_]:=Graph[Drop[#,-1]&/@lst,VertexLabels->"Name",EdgeWeight->Range[Length[lst]]]

unarrowCycles[lst_]:=Module[{cc,unarrow,ret,vv},unarrow=Graph[Drop[#,-1]&/@lst,VertexLabels->"Name",EdgeWeight->Range[Length[lst]]];
cc=ConnectedComponents[unarrow];
ret=Select[(Subgraph[unarrow,#1]&)/@cc,!AcyclicGraphQ[#]&];
ret=Graph[FindCycle[#][[1]]]&/@ret;
vv=VertexList/@ret;
ret=(orderUnarrowCycle[lst,#])&/@vv;
Return[ret];]

longishPath[g_]:=If[AcyclicGraphQ[g]&&(GraphDiameter[g]>1),True,False]

unarrowPaths[lst_]:=Module[{cc,unarrow,ret,vv},unarrow=Graph[Drop[#,-1]&/@lst,VertexLabels->"Name"];
cc=ConnectedComponents[unarrow];
ret=Select[(Subgraph[unarrow,#1]&)/@cc,longishPath[#]&];
Return[ret];]


unarrowEdgeCycles[lst_]:=Module[{ret,u},u=unarrowCycles[lst];
ret=#[[1]]&/@u;
Return[ret];]

findLongPath[g_]:=Module[{d,u,v,w,ret,vv,found,i,j},d=GraphDiameter[g];
vv=VertexList[g];
found=False;
For[i=1,i<=Length[vv]&&!found,i++,u=vv[[i]];
If[VertexEccentricity[g,u]==d,found=True;];];
found=False;
For[i=1,i<=Length[vv]&&!found,i++,v=vv[[i]];
If[GraphDistance[g,u,v]==d,found=True;];];
ret=FindPath[g,u,v,{d}];
Return[ret[[1]]];]

pathToCycle[path_]:=Module[{ret,h,e},h=findLongPath[path];
Return[h];]



unarrowCyclesFromPaths[lst_]:=Module[{cc,unarrow,ret,vv},ret=unarrowPaths[lst];
ret=pathToCycle/@ret;
vv=ret;
ret=(orderUnarrowCycle[lst,#])&/@vv;
Return[ret];]


(* ::Package::*)findAngleDescription[line1_,line2_]:=Module[{uc,vc,u1,u2},uc=line1[[1]];
vc=line2[[1]];
If[Position[vc,uc[[1]]]=={{1}},Return[{uc[[2]],uc[[1]],vc[[2]]}],If[Position[vc,uc[[1]]]=={{2}},Return[{uc[[2]],uc[[1]],vc[[1]]}],If[Position[vc,uc[[2]]]=={{1}},Return[{uc[[1]],uc[[2]],vc[[2]]}],If[Position[vc,uc[[2]]]=={{2}},Return[{uc[[1]],uc[[2]],vc[[1]]}],Return[{uc[[1]],uc[[2]],vc[[1]],vc[[2]]}]];];]]]



segmentContribution[vertices_]:=Module[{points,quantities,geometry},quantities="";
points="";
geometry=ToString[Line[vertices]];
Return[{points,quantities,geometry,0}];]



polygonAsLines[vertices_]:=Module[{i,u,v,ret},ret="";
u=vertices[[-1]];
For[i=1,i<=Length[vertices],i++,v=vertices[[i]];
ret=StringJoin[ret,ToString[Line[{u,v}]]];
u=v;
If[i<Length[vertices],ret=StringJoin[ret,","]];];
Return[ret];]

polygonContribution[vertices_]:=Module[{i,points,quantities,geometry},points="";
For[i=1,i<=Length[vertices],i++,points=addToListAsString[points,ToString[vertices[[i]]]]];
quantities="";
geometry=ToString[Polygon[vertices]];
Return[{points,quantities,geometry,Length[vertices]}];]

cyclicPolygonContribution[vertices_]:=Module[{i,points,quantities,geometry},points="";
For[i=1,i<=Length[vertices],i++,points=addToListAsString[points,ToString[vertices[[i]]]]];
quantities="";
geometry=StringJoin[ToString[Polygon[vertices]],",",ToString[CircleThrough[vertices]]];
Return[{points,quantities,geometry,Length[vertices]}];]


cyclicPolygonCenterContribution[vertices_,center_]:=Module[{i,points,quantities,geometry},points=ToString[center];
For[i=1,i<=Length[vertices],i++,points=addToListAsString[points,ToString[vertices[[i]]]]];
quantities="";
geometry=StringJoin[polygonAsLines[vertices],",",ToString[CircleThrough[vertices,center]]];
Return[{points,quantities,geometry,Length[vertices]}];]


elementAsString[p_,objstr_]:=Module[{str},str=StringJoin["Element[",ToString[p],",",objstr,"]"];
Return[str];]

infiniteLineAsString[line1_,styleStr_]:=Module[{str},dontPrint[Length[line1[[1]]]];
If[Length[line1[[1]]]==0,str=ToString[line1[[1]]],str=StringJoin["InfiniteLine[",ToString[line1[[1]]],"]"];
If[StringLength[styleStr]>0,str=StringJoin["Style[",str,",",styleStr,"]"];];];
Return[str];]

lineAsString[line1_]:=Module[{str},If[Length[line1[[1]]]==0,str=ToString[line1[[1]]],str=StringJoin["Line[",ToString[line1[[1]]],"]"];];
Return[str];]



angleBisectorAsString[p1_,p2_,p3_,styleStr_]:=Module[{str},str=ToString[AngleBisector[{p1,p2,p3}]];
If[StringLength[styleStr]>0,str=StringJoin["Style[",str,",",styleStr,"]"];];
Return[str];]

intersectionContribution[nextv_,line1_,line2_]:=Module[{ad,p,points,quantities,geometry,added},added=0;
quantities="";
ad=findAngleDescription[line1,line2];
If[Length[ad]==4,p=nextv;
points=ToString[p];
geometry=StringJoin[elementAsString[p,infiniteLineAsString[line1,"Dashed"]],",",elementAsString[p,infiniteLineAsString[line2,"Dashed"]]];
added=1,points="";
geometry="";];
Return[{points,quantities,geometry,added}];]

parallelLinesContribution[line1_,line2_]:=Module[{points,quantities,geometry},points="";
quantities="";
geometry=StringJoin["GeometricAssertion[{",lineAsString[line1],",",lineAsString[line2],"},\"Parallel\"]"];
Return[{points,quantities,geometry,0}];]


collinearPointsContribution[pp_]:=Module[{points,quantities,geometry},points="";
quantities="";
dontPrint["in collinearPoiontsContribution ",ToString[pp]];
geometry=StringJoin["GeometricAssertion[",ToString[pp],",\"Collinear\"]"];
Return[{points,quantities,geometry,0}];]

arbitraryLineContribution[p_,bname_,additionalVertices_,nextv_]:=Module[{q,ad,points,quantities,geometry,added,u,angle,contrib,L1,L2,L3},quantities="";
points="";
q=additionalVertices[[nextv]];
points=addToListAsString[points,ToString[q]];
geometry=StringJoin[ToString[bname],"==",infiniteLineAsString[{{p,q}},""]];
Return[{points,quantities,geometry,1}];]

conclusionContribution[line1_,line2_,additionalVertices_,nextv_]:=Module[{points,quantities,geometry,pol1,pol2,added,q1,q2,L1,L2},points="";
quantities="";
added=0;
geometry="";
pol1=getPointsOnLine[line1];
pol2=getPointsOnLine[line2];
L1=line1;
L2=line2;
If[Length[pol1]==1,q1=additionalVertices[[nextv]];
geometry=addToListAsString[geometry,elementAsString[q1,lineAsString[line1]]];
added=added+1;
points=addToListAsString[points,ToString[q1]];
pol1=AppendTo[pol1,q1];
L1={line1[[1]],pol1};];
If[Length[pol2]==1,q2=additionalVertices[[nextv+added]];
geometry=addToListAsString[geometry,elementAsString[q2,lineAsString[line2]]];
added=added+1;
pol2=AppendTo[pol2,q2];
points=addToListAsString[points,ToString[q2]];
L2={line2[[1]],pol2};];
geometry=addToListAsString[geometry,StringJoin["Style[",lineAsString[line1],",Red]"]];
geometry=addToListAsString[geometry,StringJoin["Style[",lineAsString[line2],",Red]"]];
Return[{points,quantities,geometry,added,L1,L2}];]

angleBisectorContribution[line1_,line2_,bname_,additionalVertices_,nextv_]:=Module[{ad,p,points,quantities,geometry,added,u,angle,contrib,L1,L2,L3},added=0;
quantities="";
u=findOrAddAngleDescription[line1,line2,additionalVertices,nextv];
angle=u[[1]];
L1=u[[2]];
L2=u[[3]];
contrib=u[[4]];
points="";
quantities="";
geometry=StringJoin[ToString[bname],"==",ToString[AngleBisector[{angle[[1]],angle[[2]],angle[[3]]}]]];
dontPrint["contrib= ",contrib];
u=addContribution[points,quantities,geometry,contrib];
L3={ToString[bname],{angle[[2]]}};
Return[{u[[1]],u[[2]],u[[3]],contrib[[4]],L1,L2,L3}];]




reflectionContribution[line1_,line2_,rname_,additionalVertices_,nextv_]:=Module[{ad,p,q,points,quantities,geometry,added,u,str,contrib,angle,L1,L2,L3},added=0;
quantities="";
u=findOrAddAngleDescription[line1,line2,additionalVertices,nextv];
angle=u[[1]];
L1=u[[2]];
L2=u[[3]];
contrib=u[[4]];
added=contrib[[4]];
dontPrint["in reflection u = ",u];
quantities="";
q=additionalVertices[[nextv+added]];
points=ToString[q];
str=infiniteLineAsString[line2,"Dashed"];
geometry=StringJoin[ToString[rname],"==",infiniteLineAsString[{{angle[[2]],q}},""],",",elementAsString[angle[[3]],angleBisectorAsString[angle[[1]],angle[[2]],q,""]]];
L3={ToString[rname],{angle[[2]],q}};
geometry=addToListAsString[geometry,StringJoin["GeometricAssertion[{",ToString[angle[[3]]],",",ToString[angle[[2]]],"},\"Distinct\"]"]];
u=addContribution[points,quantities,geometry,contrib];
Return[{u[[1]],u[[2]],u[[3]],contrib[[4]]+1,L1,L2,L3}];]

addToListAsString[str_,item_]:=Module[{ret},If[StringLength[str]>0,If[StringLength[item]>0,ret=StringJoin[str,",",item],ret=str];,ret=item,ret=""];
Return[ret];]


addContribution[points_,quantities_,geometry_,contribution_]:=Module[{ret,p,q,g,c},p=addToListAsString[points,contribution[[1]]];
q=addToListAsString[quantities,contribution[[2]]];
g=addToListAsString[geometry,contribution[[3]]];
ret={p,q,g};
Return[ret];]

createGeometricScene[points_,quantities_,geometry_,conclusions_]:=Module[{str,ret,geomex},str=StringJoin["GeometricScene[{",points,",{",quantities,"}},{",geometry,"}]"];
Return[str];]

storedLine[lines_,L_]:=Module[{ret},ret=lines[ToString[L[[1]]]];
If[MissingQ[ret],dontPrint["missingQ in storedLine ",lines,"  :  ",L];ret=L];
Return[ret];]

mergeLinePoints[L0_,L1_]:=Module[{L3,u},u=Union[L0[[2]],L1[[2]]];
L3={L1[[1]],u};
Return[L3];]

addOrMergeLine[linesIn_,line_]:=Module[{L1,L2,lines},lines=linesIn;
L1=lines[ToString[line[[1]]]];
If[MissingQ[L1],lines[ToString[line[[1]]]]=line;,If[Length[L1]>1,L2=mergeLinePoints[L1,line],L2=line;];
lines[ToString[line[[1]]]]=L2;];
Return[lines];]

algorithmGeometricScene[additionalVertices_,conditions_]:=Module[{points,quantities,geometry,ret,u,pp,v1,v2,i,nextv,con,nextnextv,nextL,lines,L1,L2,L3,qq,conclusionV,pol1,pol2},u={"","",""};
lines=<||>;
nextv=1;
nextL=1;
con={"","","",0};
dontPrint[conditions];
For[i=1,i<=Length[conditions],i++,pp=conditions[[i]];
If[pp[[1]]=="conclusion",L1=storedLine[lines,pp[[2]]];
L2=storedLine[lines,pp[[3]]];
con=conclusionContribution[L1,L2,additionalVertices,nextv];
u=addContribution[u[[1]],u[[2]],u[[3]],con];
L1=con[[5]];
L2=con[[6]];
nextv=nextv+con[[4]];
pol1=getPointsOnLine[L1];
pol2=getPointsOnLine[L2];
v1=If[Length[pol1]>1,Take[pol1,2],pol1];
v2=If[Length[pol2]>1,Take[pol2,2],pol2];
conclusionV={v1,v2,L1,L2};];
If[pp[[1]]=="segment",u=addContribution[u[[1]],u[[2]],u[[3]],segmentContribution[pp[[2]]]]];
If[pp[[1]]=="cyclicPolygon",u=addContribution[u[[1]],u[[2]],u[[3]],cyclicPolygonContribution[pp[[2]]]]];
If[pp[[1]]=="cyclicPolygonCenter",u=addContribution[u[[1]],u[[2]],u[[3]],cyclicPolygonCenterContribution[pp[[2]],pp[[3]]]]];
If[pp[[1]]=="polygon",u=addContribution[u[[1]],u[[2]],u[[3]],polygonContribution[pp[[2]]]]];
If[pp[[1]]=="parallel",u=addContribution[u[[1]],u[[2]],u[[3]],parallelLinesContribution[pp[[2]],pp[[3]]]];];
If[pp[[1]]=="collinear",u=addContribution[u[[1]],u[[2]],u[[3]],collinearPointsContribution[pp[[2]]]]];
If[pp[[1]]=="arbitrary",Print["in arbitrary contribution pp = ",pp];
con=arbitraryLineContribution[pp[[2]],pp[[3]],additionalVertices,nextv];
u=addContribution[u[[1]],u[[2]],u[[3]],con];
nextv=nextv+con[[4]];];
If[pp[[1]]=="bisector",L1=storedLine[lines,pp[[2]]];
L2=storedLine[lines,pp[[3]]];
con=angleBisectorContribution[L1,L2,pp[[4]],additionalVertices,nextv];
nextL=nextL+1;
u=addContribution[u[[1]],u[[2]],u[[3]],con];
L1=con[[5]];
L2=con[[6]];
L3=con[[7]];
lines=addOrMergeLine[lines,L1];
lines=addOrMergeLine[lines,L2];
lines=addOrMergeLine[lines,L3];
dontPrint["lines = ",lines];
nextv=nextv+con[[4]];];
If[pp[[1]]=="reflection",L1=storedLine[lines,pp[[2]]];
L2=storedLine[lines,pp[[3]]];
con=reflectionContribution[L1,L2,pp[[4]],additionalVertices,nextv];
u=addContribution[u[[1]],u[[2]],u[[3]],con];
L1=con[[5]];
L2=con[[6]];
L3=con[[7]];
(*lines[ToString[L1[[1]]]]=L1;
lines[ToString[L2[[1]]]]=L2;
lines[ToString[L3[[1]]]]=L3;*)lines=addOrMergeLine[lines,L1];
lines=addOrMergeLine[lines,L2];
lines=addOrMergeLine[lines,L3];
dontPrint["lines = ",lines];
nextv=nextv+con[[4]];];];
qq=ToExpression[StringJoin["{",u[[1]],"}"]];
qq=ToString[DeleteDuplicates[qq]];
ret=createGeometricScene[qq,u[[2]],u[[3]],{}];
Return[{ret,conclusionV}];]

polygonNamer[vertices_]:=Module[{vertexCount,isCyclicPresent,str},vertexCount=Length[vertices];
isCyclicPresent="cyclic ";
If[vertexCount<3,str="[Invalid Shape]";];
If[vertexCount==3,str="triangle";
isCyclicPresent="";];
If[vertexCount==4,str="quadrilateral";];
If[vertexCount==5,str="pentagon";];
If[vertexCount==6,str="hexagon";];
If[vertexCount==7,str="heptagon";];
If[vertexCount==8,str="octagon";];
If[vertexCount==9,str="nonagon";];
If[vertexCount==10,str="decagon";];
If[vertexCount==11,str="hendecagon";];
If[vertexCount==12,str="dodecagon";];
If[vertexCount>12,str=StringJoin[ToString[vertexCount],"-gon"];];
str=StringJoin[isCyclicPresent,str];
Return[str];]

conclusionDescription[line1_,line2_]:=Module[{str,str1,str2},If[Length[line1]==2,str1=StringJoin[ToString[line1[[1]]],ToString[line1[[2]]]],str1=ToString[line1]];
If[Length[line2]==2,str2=StringJoin[ToString[line2[[1]]],ToString[line2[[2]]]],str2=ToString[line2]];
str=StringJoin["Determine the angle between ",str1," and ",str2,". "];
Return[str];]

specificConclusionDescription[line1_,line2_,theta_]:=Module[{str,str1,str2},If[Length[line1]==2,str1=StringJoin[ToString[line1[[1]]],ToString[line1[[2]]]],str1=ToString[line1]];
If[Length[line2]==2,str2=StringJoin[ToString[line2[[1]]],ToString[line2[[2]]]],str2=ToString[line2]];
str=StringJoin["Determine the angle between ",str1," and ",str2,"."];
If[theta==0,str=StringJoin["Prove ",str1," is parallel to ",str2,". "]];
If[theta==22.5,str=StringJoin["Prove ",str1," is 22.5 degrees to ",str2,". "]];
If[theta==45,str=StringJoin["Prove ",str1," is 45 degrees to ",str2,". "]];
If[theta==67.5,str=StringJoin["Prove ",str1," is 67.5 degrees to ",str2,". "]];
If[theta==90,str=StringJoin["Prove ",str1," is perpendicular to ",str2,". "]];
Return[str];]



cyclicPolygonDescription[vertices_]:=Module[{str},str=StringJoin["Let ",ToString[vertices]," be a ",ToString[polygonNamer[vertices]],". "];
Return[str];]

cyclicPolygonCenterDescription[vertices_,centre_]:=Module[{str,centreNaming},centreNaming="centre";
If[Length[vertices]==3,centreNaming="circumcentre"];
str=StringJoin["Let ",ToString[vertices]," be a ",ToString[polygonNamer[vertices]]," with ",centreNaming," ",ToString[centre],". "];
Return[str];]

polygonDescription[vertices_]:=Module[{str},str=StringJoin["Let ",ToString[vertices]," be a ","polygon",". "];
Return[str];]

parallelLinesDescription[line1_,line2_]:=Module[{str},str=StringJoin["Let ",ToString[line1]," be parallel to ",ToString[line2],". "];
Return[str];]

collinearPointsDescription[points_]:=Module[{str},str=StringJoin["Let ",ToString[points]," be collinear. "];
Return[str];]

arbitraryLineDescription[p_,bname_]:=Module[{str},str=StringJoin["Let ",ToString[bname]," be a line through ",ToString[p],". "];
Return[str];]



angleBisectorDescription[line1_,line2_,bname_]:=Module[{str,angle,str1},angle={};
If[Length[line1[[1]]]==2&&Length[line2[[1]]]==2,angle=findAngleDescription[line1,line2];];
If[Length[angle]==3,str1=StringJoin[ToString[angle[[1]]],ToString[angle[[2]]],ToString[angle[[3]]]];
str=StringJoin["Let ",ToString[bname]," be the angle bisector of ",str1,". "],str=StringJoin["Let ",ToString[bname]," be the angle bisector of ",ToString[line1]," and ",ToString[line2],". "];];
Return[str];]


reflectionDescription[line1_,line2_,rname_]:=Module[{str},str=StringJoin["Let ",ToString[rname]," be the reflection of ",ToString[line1]," in ",ToString[line2],". "];
Return[str];]



algorithmGeometricDescription[conditions_]:=Module[{pp,i,str},str="";
For[i=1,i<=Length[conditions],i++,pp=conditions[[i]];
If[pp[[1]]=="segment",str=StringJoin[str,""];];
If[pp[[1]]=="cyclicPolygon",str=StringJoin[str,cyclicPolygonDescription[pp[[2]]]];];
If[pp[[1]]=="collinear",str=StringJoin[str,collinearPointsDescription[pp[[2]]]];];
If[pp[[1]]=="cyclicPolygonCenter",str=StringJoin[str,cyclicPolygonCenterDescription[pp[[2]],pp[[3]]]];];
If[pp[[1]]=="polygon",str=StringJoin[str,polygonDescription[pp[[2]]]];];
If[pp[[1]]=="parallel",str=StringJoin[str,parallelLinesDescription[pp[[2]],pp[[3]]]];];
If[pp[[1]]=="arbitrary",str=StringJoin[str,arbitraryLineDescription[pp[[2]],pp[[3]]]];];
If[pp[[1]]=="bisector",str=StringJoin[str,angleBisectorDescription[pp[[2]],pp[[3]],pp[[4]]]];];
If[pp[[1]]=="reflection",str=StringJoin[str,reflectionDescription[pp[[2]],pp[[3]],pp[[4]]]];]];
str=StringDelete[str,"{"];
str=StringDelete[str,"}"];
str=StringDelete[str,", "];
Return[str];]


getPointsOnLine[line_]:=Module[{uc,points},uc=line[[1]];
points={};
If[Length[line]>=2,points=line[[2]]];
If[Length[uc]==2,points=Union[line[[1]],points]];
dontPrint["in getPointsOnLine uc = ",uc," points = ",points];
Return[points];]

findOrAddIntersectionPoint[points1_,points2_,additionalVertices_,nextv_]:=Module[{p,u,added,pp1,pp2,nv},added=0;
nv=nextv;
u=Intersection[points1,points2];
pp1=points1;
pp2=points2;
dontPrint["in findOrAddIntersectionPoint nv = ",nv,"  u = ",u," additionalVertices = ",additionalVertices];
If[Length[u]>0,p=u[[1]],p=additionalVertices[[nv]];
AppendTo[pp1,p];
AppendTo[pp2,p];
nv=nv+1;
added=1;];
Return[{p,pp1,pp2,added}];]

notEqualTo[p_,q_]:=!SameQ[p,q];

findOrAddOtherPoint[points_,q_,additionalVertices_,nextv_]:=Module[{p,q0,pp,u,notq},pp=points;
q0=q;
notq=Select[pp,notEqualTo[#,q0]&];
dontPrint["in findOrAddOtherPoint  notq=",notq];
If[Length[notq]>0,Return[{notq[[1]],pp,0}];];
p=additionalVertices[[nextv]];
AppendTo[pp,p];
Return[{p,pp,1}];]



findOrAddIntersection[line1_,line2_,additionalVertices_,nextv_]:=Module[{uu,vv,p,q1,q2,L1,L2,pp1,pp2,points,quantities,geometry,added},points="";
quantities="";
geometry="";
L1=line1;
L2=line2;
pp1=getPointsOnLine[line1];
pp2=getPointsOnLine[line2];
uu=findOrAddIntersectionPoint[pp1,pp2,additionalVertices,nextv];
p=uu[[1]];
pp1=uu[[2]];
pp2=uu[[3]];
L1={L1[[1]],pp1};
L2={L2[[1]],pp2};
added=uu[[4]];
If[added==1,points=ToString[p];
geometry=StringJoin[elementAsString[p,infiniteLineAsString[line1,"Dashed"]],",",elementAsString[p,infiniteLineAsString[line2,"Dashed"]]];];
Return[{p,L1,L2,{points,quantities,geometry,added}}];]

findOrAddOtherPointOnLine[line_,p_,additionalVertices_,nextv_]:=Module[{pp,q,uu,points,quantities,geometry,added,L},points="";
quantities="";
geometry="";
L=line;
pp=getPointsOnLine[line];
uu=findOrAddOtherPoint[pp,p,additionalVertices,nextv];
q=uu[[1]];
pp=uu[[2]];
added=uu[[3]];
If[added==1,geometry=addToListAsString[geometry,elementAsString[q,infiniteLineAsString[line,"Dashed"]]];
points=ToString[q];
L={L[[1]],pp};
];
Return[{q,Evaluate[L],{points,quantities,geometry,added}}];]


findOrAddAngleDescription[line1_,line2_,additionalVertices_,nextv_]:=Module[{ret,u,uu,uc,vc,pu,pv,pp,points,quantities,geometry,added,angle,p,q1,q2,L1,L2},points="";
quantities="";
geometry="";
added=0;
L1=line1;
L2=line2;
uc=line1[[1]];
vc=line2[[1]];
If[Length[uc]===2&&Length[vc]===2,angle=findAngleDescription[line1,line2];
];
If[Length[angle]==3,Return[{angle,L1,L2,{points,quantities,geometry,0}}];];
uu=findOrAddIntersection[L1,L2,additionalVertices,nextv];
p=uu[[1]];
L1=uu[[2]];
L2=uu[[3]];
u=addContribution[points,quantities,geometry,uu[[4]]];
added=added+uu[[4]][[4]];
uu=findOrAddOtherPointOnLine[L1,p,additionalVertices,nextv+added];
q1=uu[[1]];
L1=uu[[2]];
u=addContribution[u[[1]],u[[2]],u[[3]],uu[[3]]];
added=added+uu[[3]][[4]];
uu=findOrAddOtherPointOnLine[L2,p,additionalVertices,nextv+added];
q2=uu[[1]];
L2=uu[[2]];
u=addContribution[u[[1]],u[[2]],u[[3]],uu[[3]]];
added=added+uu[[3]][[4]];
angle={q1,p,q2};
Return[{angle,L1,L2,{u[[1]],u[[2]],u[[3]],added}}];]


createParallel[line1_,line2_]:=Module[{ret},ret={"parallel",{line1},{line2}};
Return[ret];]

createUnarrowCycle[triplets_,knownLines_,cycle_,pointNames_,nextPoint_]:=Module[{ret,u,lines,i,ecycle,vcycle,p,q,center,j,k,tt,L1,L2,L3,ret2,polyv},lines=knownLines;
polyv=<||>;
ecycle=cycle[[1]];
vcycle=cycle[[2]];
u={};
ret2={};
center=pointNames[[nextPoint]];
For[i=1,i<=Length[ecycle],i++,p=pointNames[[nextPoint+i]];
AppendTo[u,p];
k=ecycle[[i]];
polyv[ToString[k]]=p;
L3=lines[ToString[k]];
If[MissingQ[L3],lines[ToString[k]]={center,p};,dontPrint["make parallel  ",L3,"   ,   ",{center,p}];
AppendTo[ret2,createParallel[L3,{center,p}]]];];
ret={{"cyclicPolygonCenter",u,center}};
For[i=1,i<=Length[vcycle],i++,tt=triplets[[vcycle[[i]]]];
q=pointNames[[nextPoint+i]];
p=polyv[ToString[tt[[1]]]];
q=polyv[ToString[tt[[2]]]];
L3={p,q};
If[MissingQ[lines[ToString[tt[[3]]]]],lines[ToString[tt[[3]]]]=L3,AppendTo[ret,createParallel[lines[ToString[tt[[3]]]],L3]]];];
ret=Join[ret,ret2];
Return[{ret,lines}];]

lineEndsFromTriplets[triplets_,lines_,n_]:=Module[{dd,tt,pos,L1,L2,p1,p2,ret,u,v,w},pos=Position[triplets,n];
For[i=1,i<=Length[pos],i++,tt=triplets[[pos[[i]][[1]]]];
dd=Drop[tt,{pos[[i]][[2]]}];
L1=lines[ToString[dd[[1]]]];
L2=lines[ToString[dd[[2]]]];
If[!(MissingQ[L1]||MissingQ[L2]),u=L1[[1]];
v=L2[[1]];
w=Intersection[u,v];
u=Complement[u,w];
v=Complement[v,w];
ret={u[[1]],v[[1]]} dontPrint["ret  ",ret];];];
Return[ret];]


createConclusion[triplets_,knownLines_,con1_,con2_]:=Module[{ret,lines,L1,L2,L3,uu},lines=knownLines;
L1=lines[ToString[con1]];
L2=lines[ToString[con2]];
If[MissingQ[L1],L1=lineEndsFromTriplets[triplets,knownLines,con1];
lines[ToString[con1]]=L1;];
If[MissingQ[L2],L2=lineEndsFromTriplets[triplets,knownLines,con2];
lines[ToString[con2]]=L2;];
ret={{"conclusion",{L1},{L2}}};
Return[{ret,lines}];]


removeArbitraryLine[triplets_,knownLines_,conclusion_]:=Module[{ret,u,lines,remainder,success},success=False;
remainder=triplets;
lines=knownLines;
For[i=1,(i<=Length[remainder])&&(!success),i++,tt=remainder[[i]];
L1=lines[ToString[tt[[1]]]];
L2=lines[ToString[tt[[2]]]];
L3=lines[ToString[tt[[3]]]];
If[!success&&MissingQ[L1]&&!MissingQ[L2]&&MissingQ[L3]&&!MemberQ[conclusion,tt[[3]]],success=True;
u={tt[[1]]->tt[[2]]};
lines[ToString[tt[[1]]]]=L2;];
If[!success&&!MissingQ[L1]&&MissingQ[L2]&&MissingQ[L3]&&!MemberQ[conclusion,tt[[3]]],success=True;
u={tt[[2]]->tt[[1]]};
lines[ToString[tt[[1]]]]=L1;];
If[success,remainder=Drop[remainder,{i}];remainder=remainder/.u;];];
Return[{success,remainder,lines}];];

createBisectorsAndReflections[triplets_,knownLines_,lineNames_,nextLine_,conclusion_]:=Module[{remainder,lines,ret,L1,L2,L3,added,success,tt,nextLineName,u},remainder=triplets;
lines=knownLines;
ret={};
added=0;
success=True;
While[Length[remainder]>0,success=False;
nextLineName=lineNames[[nextLine+added]];
For[i=1,(i<=Length[remainder])&&(!success),i++,tt=remainder[[i]];
L1=lines[ToString[tt[[1]]]];
L2=lines[ToString[tt[[2]]]];
L3=lines[ToString[tt[[3]]]];
If[MissingQ[L1]&&!MissingQ[L2]&&!MissingQ[L3],AppendTo[ret,{"reflection",{L2},{L3},nextLineName}];
success=True;
lines[ToString[tt[[1]]]]=nextLineName;];
If[!success&&!MissingQ[L1]&&MissingQ[L2]&&!MissingQ[L3],AppendTo[ret,{"reflection",{L1},{L3},nextLineName}];
success=True;
lines[ToString[tt[[2]]]]=nextLineName;];
If[!success&&!MissingQ[L1]&&!MissingQ[L2]&&MissingQ[L3],AppendTo[ret,{"bisector",{L1},{L2},nextLineName}];
success=True;
lines[ToString[tt[[3]]]]=nextLineName;];
If[!success&&!MissingQ[L1]&&!MissingQ[L2]&&!MissingQ[L3],AppendTo[ret,{"bisector",{L1},{L2},nextLineName}];
lines[nextLineName]={nextLineName};
AppendTo[ret,{"parallel",{L3},{ToExpression[nextLineName]}}];
success=True;];
If[success,added=added+1;remainder=Drop[remainder,{i}]];];
If[!success,remainder={}];];
If[success,Return[{ret,lines}],Return[False]];]


addArbitraryLine[remainderIn_,knownLines_,lineNames_,nextLine_]:=Module[{i,remainder,lines,ret,L1,L2,L3,added,success,tt,u,nMissing,nextLineName,lineNumber,q},remainder=remainderIn;
Print["into arbitrary line remainder = ",remainder];
lines=knownLines;
ret={};
added=0;
success=False;
nextLineName=lineNames[[nextLine+added]];
For[i=1,(i<=Length[remainder])&&(!success),i++,tt=remainder[[i]];
L1=lines[ToString[tt[[1]]]];
L2=lines[ToString[tt[[2]]]];
L3=lines[ToString[tt[[3]]]];
If[MissingQ[L1]&&MissingQ[L2]&&!MissingQ[L3],q=getPointsOnLine[L3];
AppendTo[ret,{"arbitrary",q,nextLineName}];
success=True;
lines[ToString[tt[[1]]]]=nextLineName;
lineNumber=tt[[1]];];
If[MissingQ[L1]&&!MissingQ[L2]&&MissingQ[L3],q=getPointsOnLine[L2];
AppendTo[ret,{"arbitrary",q,nextLineName}];
success=True;
lines[ToString[tt[[1]]]]=nextLineName;
lineNumber=tt[[1]];];
If[!MissingQ[L1]&&MissingQ[L2]&&MissingQ[L3],q=getPointsOnLine[L1];
AppendTo[ret,{"arbitrary",q,nextLineName}];
success=True;
lines[ToString[tt[[2]]]]=nextLineName;
lineNumber=tt[[2]];];
If[success==True,added=added+1];];
If[success==True,Return[{ret,remainder,lines,added,lineNumber,nextLineName}],Return[False]];]


findMergeSchedule[geometry_]:=Module[{u,v,cyclePos,i,j},u={};
cyclePos=Position[geometry,"cyclicPolygonCenter"];
For[i=1,i<=Length[cyclePos],i++,AppendTo[u,geometry[[cyclePos[[i]][[1]]]]];];
u=Sort[u,(If[countMyParallels[#1,geometry]<countMyParallels[#2,geometry],-1,1])&];
Return[u];]

isSharedParallel[knownV_,cycle2_,parallel_]:=Module[{v1,v2,w1,w2},v1=knownV;
v2=Join[cycle2[[2]],{cycle2[[3]]}];
w1=parallel[[2]][[1]];
w2=parallel[[3]][[1]];
If[(Length[Intersection[w1,v1]]==2)&&(Length[Intersection[w2,v2]]==2),Return[True]];
If[(Length[Intersection[w2,v1]]==2)&&(Length[Intersection[w1,v2]]==2),Return[True]];
Return[False];]

isMyParallel[cycle2_,parallel_]:=Module[{v1,v2,w1,w2},v2=Join[cycle2[[2]],{cycle2[[3]]}];
w1=parallel[[2]][[1]];
w2=parallel[[3]][[1]];
If[Length[Intersection[w1,v2]]==2,Return[True]];
If[Length[Intersection[w2,v2]]==2,Return[True]];
Return[False];]

countMyParallels[cycle_,geometry_]:=Module[{ret,parallelPos,i,u,v},ret=0;
parallelPos=Position[geometry,"parallel"];
For[i=1,i<=Length[parallelPos],i++,u=geometry[[parallelPos[[i]][[1]]]];
If[isMyParallel[cycle,u],ret=ret+1];];
Return[ret];]



findSharedParallels[knownV_,cycle2_,geometry_]:=Module[{ret,parallelPos,i,u,v},ret={};
parallelPos=Position[geometry,"parallel"];
For[i=1,i<=Length[parallelPos],i++,u=geometry[[parallelPos[[i]][[1]]]];
If[isSharedParallel[knownV,cycle2,u],AppendTo[ret,u]];];
Return[ret];]

countSharedParallels[cycle1_,cycle2_,geometry_]:=Module[{ret,parallelPos,i,u,v},u=Join[cycle1[[2]],{cycle1[[3]]}];
v=findSharedParallels[u,cycle2,geometry];
Return[Length[u]];]

findParallelMergeSchedule[geometry_,cycles_]:=Module[{u,v,cycle,i,knownV,ret},cycle=cycles[[1]];
knownV=Join[cycle[[2]],{cycle[[3]]}];
ret={};
For[i=2,i<=Length[cycles],i++,cycle=cycles[[i]];
u=findSharedParallels[knownV,cycle,geometry];
AppendTo[ret,u];
knownV=Join[knownV,cycle[[2]],{cycle[[3]]}];];
Return[ret];]

isReplaceableParallel[parallel_]:=Module[{w1,w2},w1=parallel[[2]][[1]];
w2=parallel[[3]][[1]];
If[Length[Intersection[w1,w2]]==1,Return[True],Return[False]];]

isDuplicateParallel[parallel_]:=Module[{w1,w2},w1=parallel[[2]][[1]];
w2=parallel[[3]][[1]];
If[Length[Intersection[w1,w2]]==2,Return[True],Return[False]];]

replaceParallel[parallel_]:=Module[{w1,w2,w,a,b,c},w1=parallel[[2]][[1]];
w2=parallel[[3]][[1]];
w=Intersection[w1,w2];
a=w[[1]];
w1=Complement[w1,w];
w2=Complement[w2,w];
b=w1[[1]];
c=w2[[1]];
Return[{"collinear",{a,b,c}}];]


getMerge[parallel_,dir_]:=Module[{aa,bb,cc,dd,ret},aa=parallel[[2]][[1]][[1]];
bb=parallel[[2]][[1]][[2]];
cc=parallel[[3]][[1]][[1]];
dd=parallel[[3]][[1]][[2]];
ret={aa->cc,dd->bb};
Return[ret];]

doMerge[geometryIn_,pmsIn_,selections_]:=Module[{ret,u,v,i,parallel,dir,pms,geometry,replacements},geometry=geometryIn;
pms=pmsIn;
replacements={};
For[i=1,i<=Length[pms],i++,parallel=pms[[i]][[selections[[i]][[1]]]];
dir=pms[[i]][[selections[[i]][[2]]]];
u=getMerge[parallel,dir];
geometry=geometry/. u;
pms=pms/. u;
replacements=Join[replacements,u];];
Return[{geometry,replacements}];]

replaceParallels[geometry_]:=Module[{i,ret,u,isDuplicate},ret={};
For[i=1,i<=Length[geometry],i++,isDuplicate=False;
u=geometry[[i]];
If[u[[1]]=="parallel",If[isDuplicateParallel[u],isDuplicate=True];
If[isReplaceableParallel[u],u=replaceParallel[u]];];
If[!isDuplicate,AppendTo[ret,u]];];
Return[ret];]

totalSchedules[pms_]:=Module[{ret,i},ret=1;
For[i=1,i<=Length[pms],i++,ret=ret*Length[pms[[i]]]*2;];
Return[ret];]

getSchedule[pms_,ii_]:=Module[{ret,u,v,i,j,k,n,dir},ret={};
u=ii-1;
For[i=1,i<=Length[pms],i++,n=Length[pms[[i]]];
dir=Mod[u,2];
u=u-dir;
u=u/2;
v=Mod[u,n];
u=(u-v)/n;
AppendTo[ret,{v+1,dir*2-1}];];
Return[ret];]

mergeCycles[geometry_]:=Module[{ret,ms,pms,bestMerge,bestMergeScore,nn,ii,sched,v,w,pp,score,bestReplacements},ms=findMergeSchedule[geometry];
bestMerge=geometry;
bestReplacements={};
If[Length[ms]>1,pms=findParallelMergeSchedule[geometry,ms];
bestMergeScore=-1;
nn=totalSchedules[pms];
For[ii=1,ii<=nn,ii++,sched=getSchedule[pms,ii];
v=doMerge[geometry,pms,sched];
w=replaceParallels[v[[1]]];
pp=Position[w,"collinear"];
score=Length[pp];
If[score>bestMergeScore,bestMergeScore=score;
bestMerge=w;
bestReplacements=v[[2]];];];];
Return[{bestMerge,bestReplacements}];]

unitVectorAlong[pp_]:=Module[{v},v=pp[[2]]-pp[[1]];
v=v/Sqrt[(v.v)];
Return[v];]

angleBetween[pp1_,pp2_]:=Module[{u,v,dp,ret},u=unitVectorAlong[pp1];
v=unitVectorAlong[pp2];
dp=u.v;
ret=ArcCos[dp]*180/Pi;
If[ret<25||ret>175,ret=0];
If[ret>40&&ret<50,ret=45];
If[ret>85&&ret<95,ret=90];
If[ret>130&&ret<140,ret=45];
If[ret>20&&ret<25,ret=22.5];
If[ret>155&&ret<160,ret=22.5];
If[ret>65&&ret<70,ret=67.5];
If[ret>110&&ret<115,ret=67.5];
Return[ret];]


createTheoremA1B1[triplets_,conclusion_,pointNames_,lineNames_]:=Module[{nextPoint,nextLine,u,i,cycle,uc,ucp,lines,uu,vv,ret,c2,remainder,used,tt,success,len,j,str,v},nextPoint=1;
nextLine=1;
lines=<||>;
u={};
uc=unarrowCycles[triplets];
ucp=unarrowCyclesFromPaths[triplets];
uc=Join[uc,ucp];
remainder=triplets;
len=Length[uc];
For[i=1,i<=len,i++,cycle=uc[[i]];
uu=createUnarrowCycle[triplets,lines,cycle,pointNames,nextPoint];
u=Join[u,uu[[1]]];
lines=Merge[{lines,uu[[2]]},First];
nextPoint=nextPoint+1+Length[cycle[[1]]];
c2=Sort[cycle[[2]],Greater];
used={};
For[j=1,j<=Length[c2],j++,used=Join[used,Take[triplets,{c2[[j]]}]];];
remainder=Complement[remainder,used];
];
v=mergeCycles[u];
u=v[[1]];
lines=lines/.v[[2]];

uu=createBisectorsAndReflections[remainder,lines,lineNames,nextLine,conclusion];
If[uu===False,Return[False]];
u=Join[u,uu[[1]]];
lines=Merge[{lines,uu[[2]]},First];
uu=createConclusion[triplets,lines,conclusion[[1]],conclusion[[2]]];
u=Join[u,uu[[1]]];
lines=Merge[{lines,uu[[2]]},First];
str=algorithmGeometricDescription[u];
vv=algorithmGeometricScene[Drop[pointNames,nextPoint-1],u];
Return[{vv[[1]],str,lines,vv[[2]]}];]




findGoodTarget[triplets_]:=Module[{best,i,pos,pp,n,score,bestscore,myT},n=Max[triplets];
pp=Position[triplets,#]&/@Range[n];
bestscore=0;
best={0,0};
For[i=1,i<=n,i++,score=0;
pos=pp[[i]];
If[Length[pos]>=2,If[pos[[1]][[2]]==3,score=score+1;myT=pos[[1]][[1]]];
If[pos[[2]][[2]]==3,score=score+1;myT=pos[[2]][[1]]];];
If[Length[pos]==2,score=score*10];
If[score>bestscore||(score==bestscore)&&(myT<best[[2]]),bestscore=score;
best={i,myT};];];
Return[best];]

createTheoremA1[tripletsIn_,pointNames_,lineNames_]:=Module[{ret,triplets,conclusion,nn,u},triplets=tripletsIn;
nn=Max[triplets];
u=findGoodTarget[triplets];
triplets[[u[[2]]]][[3]]=nn+1;
conclusion={u[[1]],nn+1};
ret=createTheoremA1B1[triplets,conclusion,pointNames,lineNames];
Return[ret];]



removeTriplet[tripletsIn_,n_]:=Module[{triplets,tt,ret},triplets=tripletsIn;
tt=triplets[[n]];
triplets=Replace[triplets,{tt[[2]]->tt[[1]]},Infinity];
triplets=Replace[triplets,{tt[[3]]->tt[[1]]},Infinity];
triplets=Drop[triplets,{n}];
Return[triplets];]


createTheoremRemovingRows[tripletsIn_,remove_,pointNames_,lineNames_]:=Module[{ret,triplets,tt,conclusion,mm,nn,i},mm=ReverseSort[remove];
triplets=tripletsIn;
For[i=1,i<=Length[mm],i++,triplets=removeTriplet[triplets,mm[[i]]];];
Return[createTheoremA1[triplets,pointNames,lineNames]];]

instanceAndDescription[theorem_]:=Module[{ret,inst,angle,pp,vv,theta,description,cdesc,line1,line2},inst=RandomInstance[ToExpression[theorem[[1]]]];
If[!Head[inst]==="RandomInstance",pp=inst["Points"];
vv=theorem[[4]]/.pp;
line1=theorem[[4]][[3]];
line2=theorem[[4]][[4]];
If[Length[vv[[1]]]==2&&Length[vv[[2]]]==2,theta=angleBetween[vv[[1]],vv[[2]]];
cdesc=specificConclusionDescription[line1[[1]],line2[[1]],theta],cdesc=conclusionDescription[line1[[1]],line2[[1]]];];,cdesc=conclusionDescription[line1[[1]],line2[[1]]];];
description=theorem[[2]];
description=StringJoin[description,cdesc];
If[Head[inst]==="RandomInstance",ret=False,ret=Grid[{{inst},{description}}];];
Return[ret];]

forbiddenVertices[g_,v_]:=Module[{ret,ng,c,u},ng=NeighborhoodGraph[g,v,2];
c=Flatten[FindCycle[ng,{4},All]];
ret=VertexList[c];
ng=NeighborhoodGraph[g,v,1];
u=VertexList[ng];
ret=Union[ret,u];
Return[ret];]

randomRemovableVertices[graph_]:=Module[{u,forbidden,w,ret,n},n=VertexCount[graph];
u=RandomInteger[{1,n}];
ret={u};
forbidden=forbiddenVertices[graph,u];
While[Length[forbidden]<n,While[MemberQ[forbidden,u],u=RandomInteger[{1,n}]];
AppendTo[ret,u];
forbidden=Union[forbidden,forbiddenVertices[graph,u]];];
Return[ret];]


randomTheorem[pointNames_,lineNames_,time_]:=Module[{triplets,u,removable,g,ret,count,pp,best},pp=Join[p6,p8,p10a,p10b,p12a,p12b,p12c,p12d,p12e];
u=RandomInteger[{1,Length[pp]}];
triplets=pp[[u]];
g=createVanillaTheoremGraph[triplets];
count=0;removable={};best=0;
While[count<4,u=randomRemovableVertices[g];count=count+1;
If[Length[u]>best,best=Length[u];removable=u];];
ret=createTheoremRemovingRows[triplets,removable,pointNames,lineNames];
If[!ret===False,ret=TimeConstrained[instanceAndDescription[ret],time,False]];
Return[ret];]







randomTheorem14[pointNames_,lineNames_,time_]:=Module[{triplets,u,removable,g,ret,count,p14},p14=Join[p14a,p14b,p14c,p14d,p14e,p14f,p14g,p14h,p14i,p14j,p14k,p14l,p14m];
u=RandomInteger[{1,Length[p14]}];
triplets=p14[[u]];
g=createVanillaTheoremGraph[triplets];
count=0;removable={};
While[Length[removable]<4&&count<4,removable=randomRemovableVertices[g];count=count+1];
ret=createTheoremRemovingRows[triplets,removable,pointNames,lineNames];
If[!ret===False,ret=TimeConstrained[instanceAndDescription[ret],time,False]];
Return[ret];]



createRandomTheorems[nn_:2,time_:15]:=Module[{i,ret,u,pname,lnames},ret={};
pnames={a,b,c,d,e,f,g,h,m,n,p,q,r,s,t,u,v,w,x,y,z};
lnames={L1,L2,L3,L4,L5,L6,L7,L8,L9};
While[Length[ret]<nn,u=randomTheorem[pnames,lnames,time];
If[!((u===False)||(Head[u]===RandomInstance)),AppendTo[ret,u(*ExpressionCell[u]*)]];];
Return[ret];]

createRandomTheorems14[nn_,time_]:=Module[{i,ret,u,pnames,lnames},ret={};
pnames={a,b,c,d,e,f,g,h,m,n,p,q,r,s,t,u,v,w,x,y,z};
lnames={L1,L2,L3,L4,L5,L6,L7,L8,L9};
While[Length[ret]<nn,u=randomTheorem14[pnames,lnames,time];
If[!((u===False)||(Head[u]===RandomInstance)),AppendTo[ret,u(*ExpressionCell[u]*)]];];
Return[ret];]

createRandomTheorems[]