public static List<EdgeAggregator> InstantiateToPerpendicular(GroundedClause clause)
        {
            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is Intersection)
            {
                // Since we receive intersections right away in the instantiation process, just store the intersections
                candidateIntersections.Add(clause as Intersection);
            }
            else if (clause is RightAngle)
            {
                RightAngle ra = clause as RightAngle;

                foreach (Intersection inter in candidateIntersections)
                {
                    newGrounded.AddRange(InstantiateToPerpendicular(inter, ra, clause));
                }
            }
            else if (clause is Strengthened)
            {
                Strengthened streng = clause as Strengthened;

                // Only intrerested in right angles
                if (!(streng.strengthened is RightAngle)) return newGrounded;

                foreach (Intersection inter in candidateIntersections)
                {
                    newGrounded.AddRange(InstantiateToPerpendicular(inter, streng.strengthened as RightAngle, clause));
                }
            }

            return newGrounded;
        }

        public override bool CanBeStrengthenedTo(GroundedClause gc)
        {
            Midpoint midpoint = gc as Midpoint;
            if (midpoint == null) return false;

            return this.point.StructurallyEquals(midpoint.point) && this.segment.StructurallyEquals(midpoint.segment);
        }

        private static List<EdgeAggregator> InstantiateToTheorem(Rhombus rhombus, GroundedClause original)
        {
            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            // For hypergraph
            List<GroundedClause> antecedent = Utilities.MakeList<GroundedClause>(original);

            // Instantiate this rhombus diagonals ONLY if the original figure has the diagonals drawn.
            if (rhombus.TopLeftDiagonalIsValid())
            {
                AngleBisector ab1 = new AngleBisector(rhombus.topLeftAngle, rhombus.topLeftBottomRightDiagonal);
                AngleBisector ab2 = new AngleBisector(rhombus.bottomRightAngle, rhombus.topLeftBottomRightDiagonal);
                newGrounded.Add(new EdgeAggregator(antecedent, ab1, annotation));
                newGrounded.Add(new EdgeAggregator(antecedent, ab2, annotation));
            }

            if (rhombus.BottomRightDiagonalIsValid())
            {
                AngleBisector ab1 = new AngleBisector(rhombus.topRightAngle, rhombus.bottomLeftTopRightDiagonal);
                AngleBisector ab2 = new AngleBisector(rhombus.bottomLeftAngle, rhombus.bottomLeftTopRightDiagonal);
                newGrounded.Add(new EdgeAggregator(antecedent, ab1, annotation));
                newGrounded.Add(new EdgeAggregator(antecedent, ab2, annotation));
            }

            return newGrounded;
        }

        //
        // EquilateralTriangle(A, B, C) -> Equation(m \angle ABC = 60),
        //                                 Equation(m \angle BCA = 60),
        //                                 Equation(m \angle CAB = 60)
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause c)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.EQUILATERAL_TRIANGLE_HAS_SIXTY_DEGREE_ANGLES;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (!(c is EquilateralTriangle) && !(c is Strengthened)) return newGrounded;

            EquilateralTriangle eqTri = c as EquilateralTriangle;

            if (c is Strengthened)
            {
                eqTri = (c as Strengthened).strengthened as EquilateralTriangle;
            }

            if (eqTri == null) return newGrounded;

            // EquilateralTriangle(A, B, C) ->
            List<GroundedClause> antecedent = Utilities.MakeList<GroundedClause>(c);

            //                              -> Equation(m \angle ABC = 60),
            //                                 Equation(m \angle BCA = 60),
            //                                 Equation(m \angle CAB = 60)
            GeometricAngleEquation eq1 = new GeometricAngleEquation(eqTri.AngleA, new NumericValue(60));
            GeometricAngleEquation eq2 = new GeometricAngleEquation(eqTri.AngleB, new NumericValue(60));
            GeometricAngleEquation eq3 = new GeometricAngleEquation(eqTri.AngleC, new NumericValue(60));

            newGrounded.Add(new EdgeAggregator(antecedent, eq1, annotation));
            newGrounded.Add(new EdgeAggregator(antecedent, eq2, annotation));
            newGrounded.Add(new EdgeAggregator(antecedent, eq3, annotation));

            return newGrounded;
        }

        public static void Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.RIGHT_TRIANGLE_DEFINITION;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            //
            // Instantiating FROM a right triangle
            //
            Strengthened streng = clause as Strengthened;
            if (streng == null) return;

            if (streng.strengthened is RightTriangle)
            {
                candidateRight.Add(streng);

                foreach (Strengthened iso in candidateIsosceles)
                {
                    InstantiateRightTriangle(streng, iso);
                }
            }
            else if (streng.strengthened is IsoscelesTriangle)
            {
                candidateIsosceles.Add(streng);

                foreach (Strengthened right in candidateRight)
                {
                    InstantiateRightTriangle(right, streng);
                }
            }
        }

        //
        // In order for two triangles to be congruent, we require the following:
        //    RightTriangle(A, B, C) -> Complementary(Angle(B, A, C), Angle(A, C, B))
        //     A
        //    | \
        //    |  \
        //    |   \
        //    |    \
        //    |_____\
        //    B      C
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause c)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.ACUTE_ANGLES_IN_RIGHT_TRIANGLE_ARE_COMPLEMENTARY;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (!(c is Triangle) && !(c is Strengthened)) return newGrounded;

            if (c is Triangle)
            {
                Triangle tri = c as Triangle;

                if (!(tri is RightTriangle))
                {
                    if (!tri.provenRight) return newGrounded;
                }
                newGrounded.AddRange(InstantiateRightTriangle(tri, c));
            }

            if (c is Strengthened)
            {
                Strengthened streng = c as Strengthened;

                if (!(streng.strengthened is RightTriangle)) return newGrounded;

                newGrounded.AddRange(InstantiateRightTriangle(streng.strengthened as RightTriangle, c));
            }

            return newGrounded;
        }

        public override bool ContainsClause(GroundedClause clause)
        {
            NumericValue clauseValue = clause as NumericValue;
            if (clauseValue == null) return false;

            return Utilities.CompareValues(value, clauseValue.value);
        }

        //
        // Implements transitivity with Relations (Parallel, Similar)
        // Relation(A, B), Relation(B, C) -> Relation(A, C)
        //
        // Generation of new relations is restricted to the following rules; let G be Geometric and A algebriac
        //     G + G -> A
        //     G + A -> A
        //     A + A -X> A  <- Not allowed
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            // Do we have appropriate clauses?
            if (!(clause is Parallel) && !(clause is SimilarTriangles)) return newGrounded;

            // Has this clause been generated before?
            // Since generated clauses will eventually be instantiated as well, this will reach a fixed point and stop.
            // Uniqueness of clauses needs to be handled by the class calling this
            if (ClauseHasBeenDeduced(clause)) return newGrounded;

            // A reflexive expression provides no information of interest or consequence.
            if (clause.IsReflexive()) return newGrounded;

            //
            // Process the clause
            //
            if (clause is Parallel)
            {
                newGrounded.AddRange(HandleNewParallelRelation(clause as Parallel));
            }
            else if (clause is SimilarTriangles)
            {
                newGrounded.AddRange(HandleNewSimilarTrianglesRelation(clause as SimilarTriangles));
            }

            // Add the new clause to the right list for later combining
            AddToAppropriateList(clause);

            return newGrounded;
        }

        //     /        A
        //    /         |)
        //   /          | )
        //  /           |  )
        // Q------- O---X---) D
        //   \          |  )
        //    \         | )
        //     \        |)
        //      \        C
        //
        // Inscribed Angle(AQC) -> Angle(AQC) = 2 * Arc(AC)
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.MEASURE_INSCRIBED_ANGLE_EQUAL_HALF_INTERCEPTED_ARC;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is Angle)
            {
                Angle angle = clause as Angle;

                foreach (Circle circle in candidateCircles)
                {
                    newGrounded.AddRange(InstantiateTheorem(circle, angle));
                }

                candidateAngles.Add(angle);
            }
            else if (clause is Circle)
            {
                Circle circle = clause as Circle;

                foreach (Angle angle in candidateAngles)
                {
                    newGrounded.AddRange(InstantiateTheorem(circle, angle));
                }

                candidateCircles.Add(circle);
            }

            return newGrounded;
        }

        private static List<EdgeAggregator> InstantiateFromAltitude(GroundedClause clause)
        {
            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is Intersection)
            {
                Intersection inter = clause as Intersection;

                // We are only interested in straight-angle type intersections
                if (inter.StandsOnEndpoint()) return newGrounded;
                if (!inter.IsPerpendicular()) return newGrounded;

                foreach (Altitude altitude in candidateAltitude)
                {
                    newGrounded.AddRange(InstantiateFromAltitude(inter, altitude));
                }

                candidateIntersection.Add(inter);
            }
            else if (clause is Altitude)
            {
                Altitude altitude  = clause as Altitude;

                foreach (Intersection inter in candidateIntersection)
                {
                    newGrounded.AddRange(InstantiateFromAltitude(inter, altitude));
                }

                candidateAltitude.Add(altitude);
            }

            return newGrounded;
        }

        //
        // AngleBisector(SegmentA, D), Angle(C, A, B)) -> 2 m\angle CAD = m \angle CAB,
        //                                                2 m\angle BAD = m \angle CAB
        //
        //   A ________________________B
        //    |\
        //    | \
        //    |  \
        //    |   \
        //    |    \
        //    C     D
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause c)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.ANGLE_BISECTOR_THEOREM;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (!(c is AngleBisector)) return newGrounded;

            AngleBisector angleBisector = c as AngleBisector;
            KeyValuePair<Angle, Angle> adjacentAngles = angleBisector.GetBisectedAngles();

            // Construct 2 m\angle CAD
            Multiplication product1 = new Multiplication(new NumericValue(2), adjacentAngles.Key);
            // Construct 2 m\angle BAD
            Multiplication product2 = new Multiplication(new NumericValue(2), adjacentAngles.Value);

            // 2X = AB
            GeometricAngleEquation newEq1 = new GeometricAngleEquation(product1, angleBisector.angle);
            GeometricAngleEquation newEq2 = new GeometricAngleEquation(product2, angleBisector.angle);

            // For hypergraph
            List<GroundedClause> antecedent = Utilities.MakeList<GroundedClause>(angleBisector);

            newGrounded.Add(new EdgeAggregator(antecedent, newEq1, annotation));
            newGrounded.Add(new EdgeAggregator(antecedent, newEq2, annotation));

            return newGrounded;
        }

        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.CORRESPONDING_ANGLES_OF_PARALLEL_LINES;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is Parallel)
            {
                Parallel parallel = clause as Parallel;
                for (int i = 0; i < candidateIntersection.Count; i++)
                {
                    for (int j = i + 1; j < candidateIntersection.Count; j++)
                    {
                        newGrounded.AddRange(InstantiateIntersection(parallel, candidateIntersection[i], candidateIntersection[j]));
                    }
                }
                candidateParallel.Add(parallel);
            }
            else if (clause is Intersection)
            {
                Intersection newInter = clause as Intersection;
                foreach (Intersection oldInter in candidateIntersection)
                {
                    foreach (Parallel parallel in candidateParallel)
                    {
                        newGrounded.AddRange(InstantiateIntersection(parallel, newInter, oldInter));
                    }
                }
                candidateIntersection.Add(newInter);
            }

            return newGrounded;
        }

        //
        // Supplementary(Angle(A, B, D), Angle(B, A, C))
        // Congruent(Angle(A, B, D), Angle(B, A, C)) -> RightAngle(Angle(A, B, D))
        //                                           -> RightAngle(Angle(B, A, C))
        //                            
        //                            C            D
        //                            |            |
        //                            |____________|
        //                            A            B
        //                            
        public static List<EdgeAggregator> Instantiate(GroundedClause c)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.CONGRUENT_SUPPLEMENTARY_ANGLES_IMPLY_RIGHT_ANGLES;

            // The list of new grounded clauses if they are deduced
            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (c is CongruentAngles)
            {
                CongruentAngles conAngles = c as CongruentAngles;

                // We are interested in adjacent angles, not reflexive
                if (conAngles.IsReflexive()) return newGrounded;

                foreach (Supplementary suppAngles in candSupplementary)
                {
                    newGrounded.AddRange(CheckAndGenerateSupplementaryCongruentImplyRightAngles(suppAngles, conAngles));
                }

                candCongruent.Add(conAngles);
            }
            else if (c is Supplementary)
            {
                Supplementary supplementary = c as Supplementary;

                foreach (CongruentAngles cc in candCongruent)
                {
                    newGrounded.AddRange(CheckAndGenerateSupplementaryCongruentImplyRightAngles(supplementary, cc));
                }

                candSupplementary.Add(supplementary);
            }

            return newGrounded;
        }

        //
        // This implements forward and Backward instantiation
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.PERPENDICULAR_DEFINITION;

            // FROM Perpendicular
            if (clause is Perpendicular) return InstantiateFromPerpendicular(clause, clause as Perpendicular);

            // TO Perpendicular
            if (clause is RightAngle || clause is Intersection) return InstantiateToPerpendicular(clause);

            // Handle Strengthening; may be a Perpendicular (FROM) or Right Angle (TO)

            Strengthened streng = clause as Strengthened;
            if (streng != null)
            {
                if (streng.strengthened is Perpendicular && !(streng.strengthened is PerpendicularBisector))
                {
                    return InstantiateFromPerpendicular(clause, streng.strengthened as Perpendicular);
                }
                else if (streng.strengthened is RightAngle)
                {
                    return InstantiateToPerpendicular(clause);
                }
            }

            return new List<EdgeAggregator>();
        }

        //
        //    A \      / B
        //       \    /
        //        \  /
        //  O      \/ X
        //         /\
        //        /  \
        //     C /    \ D
        //
        // Intersection(Segment(AD), Segment(BC)) -> 2 * Angle(CXA) = Arc(A, C) + Arc(B, D),
        //                                           2 * Angle(BXD) = Arc(A, C) + Arc(B, D),
        //                                           2 * Angle(AXB) = Arc(A, B) + Arc(C, D),
        //                                           2 * Angle(CXD) = Arc(A, B) + Arc(C, D)
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.TWO_INTERSECTING_CHORDS_ANGLE_MEASURE_HALF_SUM_INTERCEPTED_ARCS;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is Intersection)
            {
                Intersection newInter = clause as Intersection;

                foreach (Circle circle in candidateCircle)
                {
                    newGrounded.AddRange(InstantiateTheorem(newInter, circle));
                }

                candidateIntersection.Add(newInter);
            }
            else if (clause is Circle)
            {
                Circle circle = clause as Circle;

                foreach (Intersection oldInter in candidateIntersection)
                {
                    newGrounded.AddRange(InstantiateTheorem(oldInter, circle));
                }

                candidateCircle.Add(circle);
            }

            return newGrounded;
        }

 public override bool CanBeStrengthenedTo(GroundedClause gc)
 {
     Perpendicular perp = gc as Perpendicular;
     if (perp == null) return false;
     return intersect.Equals(perp.intersect) && ((lhs.StructurallyEquals(perp.lhs) && rhs.StructurallyEquals(perp.rhs)) ||
                                                 (lhs.StructurallyEquals(perp.rhs) && rhs.StructurallyEquals(perp.lhs)));
 }

        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.TWO_INTERCEPTED_ARCS_HAVE_CONGRUENT_ANGLES;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is Angle)
            {
                Angle angle = clause as Angle;

                foreach (Angle candCongruentAngle in candidateAngles)
                {
                    newGrounded.AddRange(InstantiateTheorem(angle, candCongruentAngle));
                }

                candidateAngles.Add(angle);
            }

            else if (clause is Circle)
            {
                Circle circle = clause as Circle;

                for (int i = 0; i < candidateAngles.Count; ++i)
                {
                    for (int j = i + 1; j < candidateAngles.Count; ++j)
                    {
                        newGrounded.AddRange(InstantiateTheorem(candidateAngles[i], candidateAngles[j]));
                    }
                }

            }

            return newGrounded;
        }

        //     B ---------V---------A
        //                 \
        //                  \
        //                   \
        //                    C
        //
        // Median(Segment(V, C), Triangle(C, A, B)) -> Midpoint(V, Segment(B, A))
        //
        private static List<EdgeAggregator> InstantiateFromMedian(GroundedClause clause)
        {
            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            if (clause is InMiddle && !(clause is Midpoint))
            {
                InMiddle im = clause as InMiddle;

                foreach (Median median in candidateMedian)
                {
                    newGrounded.AddRange(InstantiateFromMedian(im, median));
                }

                candidateInMiddle.Add(im);
            }
            else if (clause is Median)
            {
                Median median = clause as Median;

                foreach (InMiddle im in candidateInMiddle)
                {
                    newGrounded.AddRange(InstantiateFromMedian(im, median));
                }

                candidateMedian.Add(median);
            }

            return newGrounded;
        }

        //         B ____________________ C
        //          /                   /
        //         /                   /
        //        / Circle (center)   /
        //       /        O          /
        //      /                   /
        //   A /___________________/ D
        //
        // Circle(O), Quad(A, B, C, D) -> Supplementary(Angle(ABC), Angle(ADC)), Supplementary(Angle(BAD), Angle(BCD))
        //
        public static List<EdgeAggregator> Instantiate(GroundedClause clause)
        {
            annotation.active = EngineUIBridge.JustificationSwitch.INSCRIBED_QUADRILATERAL_OPPOSITE_ANGLES_SUPPLEMENTARY;

            List<EdgeAggregator> newGrounded = new List<EdgeAggregator>();

            Circle circle = clause as Circle;

            if (circle == null) return newGrounded;

            //
            // For each inscribed quadrilateral, generate accordingly.
            //
            foreach (Quadrilateral quad in circle.inscribedPolys[Polygon.QUADRILATERAL_INDEX])
            {
                Supplementary supp1 = new Supplementary(quad.topLeftAngle, quad.bottomRightAngle);
                Supplementary supp2 = new Supplementary(quad.bottomLeftAngle, quad.topRightAngle);

                // For hypergraph
                List<GroundedClause> antecedent = new List<GroundedClause>();
                antecedent.Add(circle);
                antecedent.Add(quad);

                newGrounded.Add(new EdgeAggregator(antecedent, supp1, annotation));
                newGrounded.Add(new EdgeAggregator(antecedent, supp2, annotation));
            }

            return newGrounded;
        }

        public static List<EdgeAggregator> InstantiateTheorem(GroundedClause original, IsoscelesTriangle isoTri)
        {
            GeometricCongruentAngles newCongSegs = new GeometricCongruentAngles(isoTri.baseAngleOppositeLeg1, isoTri.baseAngleOppositeLeg2);

            List<GroundedClause> antecedent = Utilities.MakeList<GroundedClause>(original);

            return Utilities.MakeList<EdgeAggregator>(new EdgeAggregator(antecedent, newCongSegs, annotation));
        }