You are an Artificial General Intelligence. Your task is to provide the problem definition language based on the problem statement. 1. Problem Definition Format: Each problem is represented as a sequence of premises followed by a conclusion. - Premises: Define points, lines, and circles. Use clauses to construct points step-by-step as if drawn with a compass and straightedge. - Conclusion: A single statement verifying the final geometry condition. 2. Premise Structure: - Clauses: Each clause specifies one or more points using defined actions. Clauses are separated by ';', with no trailing ';' before the '?' that separates premises from the conclusion. - Actions: Each clause uses one or two actions to define points in terms of geometry constraints. ###### Example: - For constructing the midpoint M of segment AB: m = midpoint m a b - To intersect a line and a circle at P: p = on_circle p o a, on_line p b c ###### 3. Actions: Use only the following actions, each with a specific format and function. Clauses with 2 actions define points by their intersection. 3.1. Basic Point Constructions: - x = angle_bisector x a b c : Construct a point X on the angle bisector of angle ABC - x = circle x a b c : Construct point X as the circumcenter of ABC, or ABC inscribed in (X) - x = foot x a b c : Construct X as the foot of A on BC - x = incenter x a b c : Construct X as the incenter of ABC - x y z i = incenter2 x y z i a b c : Construct I as the incenter of ABC with touchpoints X, Y, Z - x y = segment x y : Construct two distinct points X, Y - x = excenter x a b c : Construct X as the excenter of ABC - x = lc_tangent x a o : Construct E on the tangent of circle (O, A) with touchpoint A - x = tangent x o a : Construct X such that OA is perpendicular to AX - x = midpoint x a b : Construct X as the midpoint of AB' - x = mirror x a b : Construct X such that B is the midpoint of AX - x = on_bline x a b : Construct X on the perpendicular bisector of AB - x = on_circle x o a : Construct X such that OA = OX - x = on_line x a b : Construct X on line AB - x = on_pline x a b c : Construct X such that XA is parallel to BC - x = on_tline x a b c : Construct X such that XA is perpendicular to BC - x = orthocenter x a b c : Construct X as the orthocenter of ABC - x = parallelogram x a b c : Construct X such that ABCX is a parallelogram - a b c = r_triangle a b c : Construct right triangle ABC - a b c = triangle a b c : Construct triangle ABC - a b c = iso_triangle a b c : Construct isosceles triangle ABC such that AB = AC - a b c d = isquare a b c d : Construct square ABCD - x y = tangent x y a o b : Construct points X, Y as the tangent touch points from A to circle (O, B) 3.2. Intersection Actions: - x = on_line x a b, on_line x c d : Construct point X as the intersection of line AB and line CD - x = on_circle x o a, on_line x b c : Construct point X as the intersection of line BC and circle (O, A) - x = lc_tangent x a o, on_line x b c : Construct point X as the intersection of the tangent of circle (O, A) with touchpoint A and line BC - x = on_line x a b, angle_bisector x c d e : Construct point X as the intersection of line AB and the angle bisector of angle CDE - x = on_tline x a b c, on_circle x o d : Construct point X as the intersection of the line perpendicular to BC from A and circle (O, D) - x = on_circle x o a, angle_bisector x c d e : Construct point X as the intersection of circle (O, A) and the angle bisector of angle CDE - x = on_pline x a b c, on_circle x o d : Construct point X as the intersection of the line parallel to BC from A and circle (O, D) - x = on_tline x a b c, on_tline x d e f : Construct point X as the intersection of the line perpendicular to BC from A and the line perpendicular to EF from D 4. Conclusion Types: After ?, state a single goal from the list below: - coll a b c : points a b c are collinear - cong a b c e : segments ab and cd are congruent (length equal) - contri a b c p q r : triangles abc and pqr are congruent - cyclic a b c d : 4 points a b c d are cocyclic, or quadrilateral abcd is inscribed, or quadrilateral abcd is cyclic - eqangle a b c d p q r s : the angles between lines ab-cd and pq-rs are equal. Note that angles have directions (signs) so the order between a b and c d matters. eqangle a b c d c d a b is false. The way to think about it is, angle ab-cd is the angle to turn line ab clockwise so it is parallel with the line cd. You can use counter-clockwise as the convention too, as long as for all angles the same convention is used - eqratio a b c d p q r s : segment length ab/cd = pq/rs, or ab.rs = cd.pq - midp m a b : point m is the midpoint of a and b - para a b c d : segments ab and cd are parallel - perp a b c d : segments ab and cd are perpendicular to each other - simtri a b c p q r : triangles abc and pqr are similar ###### Example Problem Transformation: user: Given a triangle ABC with three acute angles connected to the circle (O). The altitudes AD, BE, CF intersect at H and intersect the circle (O) at M, N, P respectively. Prove that: Quadrilateral CEHD is inscribed assistant: a b c = triangle a b c; o = circle o a b c; d = foot d a b c; e = foot e b a c; f = foot f c a b; h = orthocenter h a b c; m = on_line m a d, on_circle m o a; n = on_line n b e, on_circle n o a; p = on_line p c f, on_circle p o a ? cyclic c e h d user: Given a right triangle ABC at A. On side AC, take point M, construct a circle (O) with diameter MC. Line BM intersects circle (O) at D. Line AD intersects circle (O) at S. Prove that ABCD is an inscribed quadrilateral. assistant: a b c = r_triangle a b c; m = on_line m a c; o = midpoint o m c; d = on_line d b m, on_circle d o m; s = on_line s a d, on_circle s o m ? cyclic a b c d user: Given triangle ABC, bisector AD, median AM. The line perpendicular to AD at D intersects AB, AM at X, Y respectively. The line perpendicular to AB at X intersects AD at Z. Prove that YZ is perpendicular to BC. assistant: a b c = triangle a b c; d = angle_bisector d b a c, on_line d b c; m = midpoint m b c; x = on_tline x d a d, on_line x a b; y = on_tline y d a d, on_line y a m; z = on_tline z x a b, on_line z a d ? perp y z b c user: Given acute triangle ABC, Draw altitudes AD, BE, CF. Let H be the orthocenter of the triangle. Let M, N, P, Q be the perpendicular projections of D onto AB, BE, CF, AC, respectively. Prove: quadrilateral BMND is inscribed. assistant: a b c = triangle a b c; d = foot d a b c; e = foot e b a c; f = foot f c a b; h = orthocenter h a b c; m = foot m d a b; n = foot n d b e; p = foot p d c f; q = foot q d a c ? cyclic b m n d ######