SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, ∠APO=30°, the center of ⊙O is O, the tangent to ⊙O is PA. Find the measure of ∠BOA.
问题：如图所示，∠APO=30°，⊙O的圆心为O，⊙O的切线为PA。求∠BOA的大小。
Construction (CDL):
Shape(OA,OAB,BO)
Shape(AP,PB,OAB)
Collinear(PBO)
Cocircular(O,AB)
Conditions (CDL):
Equal(MeasureOfAngle(APO),30)
IsCentreOfCircle(O,O)
IsTangentOfCircle(PA,O)
Goal: Value(MeasureOfAngle(BOA))
Answer: 60
Theorem sequence:
tangent_of_circle_property_perpendicular(1,PA,O,O)
triangle_property_angle_sum(1,OAP)
Problem: As shown in the diagram, AB=5, AC=4, BC=3, ∠ACB=90°, the center of circle O is O, the diameter of ⊙O is CD, the tangent to ⊙O is AC, the tangent to ⊙O is AE, BE is the tangent to circle O. Find the length of line BD.
问题：如图所示，AB=5，AC=4，BC=3，∠ACB=90°，⊙O的圆心为O，⊙O的直径为CD，圆O的切线为AC，⊙O的切线为AE，BE是⊙O的切线。求直线BD的长度。
Construction (CDL):
Shape(EA,AC,OEC)
Shape(OD,ODE,OEC,CO)
Shape(DB,BE,ODE)
Collinear(BDOC)
Collinear(AEB)
Cocircular(O,DEC)
Conditions (CDL):
Equal(LengthOfLine(AB),5)
Equal(LengthOfLine(AC),4)
Equal(LengthOfLine(BC),3)
Equal(MeasureOfAngle(ACB),90)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(CD,O)
IsTangentOfCircle(AC,O)
IsTangentOfCircle(AE,O)
IsTangentOfCircle(BE,O)
Goal: Value(LengthOfLine(BD))
Answer: 1/3
Theorem sequence:
tangent_of_circle_property_length_equal(1,AE,AC,O)
line_addition(1,AE,EB)
circle_property_circular_power_tangent_and_segment_line(1,BE,BDC,O)
Problem: As shown in the diagram, BP=6, ∠BPA=30°, O is the center of ⊙O, AE is the diameter of circle O, PB is the tangent to circle O, AC⊥OC, OC is perpendicular to BC. Find the length of line CD.
问题：如图所示，BP=6，∠BPA=30°，⊙O的圆心为O，AE是⊙O的直径，⊙O的切线为PB，AC⊥OC，OC⊥BC。求直线CD的长度。
Construction (CDL):
Shape(OA,AC,CO)
Shape(BO,OC,CB)
Shape(CA,OAD,DC)
Shape(BC,CD,ODB)
Shape(OB,BE,EO)
Shape(OBE,EB)
Shape(BP,PE,OBE)
Collinear(ACB)
Collinear(AOEP)
Collinear(OCD)
Cocircular(O,ADBE)
Conditions (CDL):
Equal(LengthOfLine(BP),6)
Equal(MeasureOfAngle(BPA),30)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AE,O)
IsTangentOfCircle(PB,O)
PerpendicularBetweenLine(AC,OC)
PerpendicularBetweenLine(OC,BC)
Goal: Value(LengthOfLine(CD))
Answer: sqrt(3)
Theorem sequence:
tangent_of_circle_property_perpendicular(1,PB,O,O)
triangle_property_angle_sum(1,OAB)
triangle_property_angle_sum(1,OBP)
flat_angle(1,EOA)
angle_addition(1,EOB,BOA)
radius_of_circle_property_length_equal(1,OA,O)
radius_of_circle_property_length_equal(1,OD,O)
radius_of_circle_property_length_equal(1,OB,O)
sine_theorem(1,OAC)
sine_theorem(1,OCB)
sine_theorem(1,BPO)
line_addition(1,OC,CD)
Problem: As shown in the diagram, OA=13, OB=5, O is the center of ⊙O, the tangent to circle O is AB. Find the length of line AB.
问题：如图所示，OA=13，OB=5，⊙O的圆心为O，AB是圆O的切线。求直线AB的长度。
Construction (CDL):
Shape(OC,OCB,BO)
Shape(CA,AB,OCB)
Collinear(ACO)
Cocircular(O,CB)
Conditions (CDL):
Equal(LengthOfLine(OA),13)
Equal(LengthOfLine(OB),5)
IsCentreOfCircle(O,O)
IsTangentOfCircle(AB,O)
Goal: Value(LengthOfLine(AB))
Answer: 12
Theorem sequence:
tangent_of_circle_property_perpendicular(2,AB,O,O)
right_triangle_judgment_angle(1,ABO)
right_triangle_property_pythagorean(1,ABO)
Problem: As shown in the diagram, AB=6, AD=3, O is the center of circle O, AB is the diameter of ⊙O. Find the measure of ∠ABD.
问题：如图所示，AB=6，AD=3，O是⊙O的圆心，圆O的直径为AB。求∠ABD的大小。
Construction (CDL):
Shape(OD,DA,AO)
Shape(DO,OB,BD)
Shape(ODA,AD)
Shape(OBD,DB)
Collinear(AOB)
Cocircular(O,BDA)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(AD),3)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AB,O)
Goal: Value(MeasureOfAngle(ABD))
Answer: 30
Theorem sequence:
diameter_of_circle_property_right_angle(1,BDA,O)
sine_theorem(1,ABD)
Problem: As shown in the diagram, ∠DCA=36°, O is the center of ⊙O, the tangent to ⊙O is CB. Find the measure of ∠DBA.
问题：如图所示，∠DCA=36°，⊙O的圆心为O，⊙O的切线为CB。求∠DBA的大小。
Construction (CDL):
Shape(OA,AB,BO)
Shape(CO,OB,BC)
Shape(DB,BA)
Shape(OAB,BA)
Collinear(CBD)
Collinear(AOC)
Cocircular(O,AB)
Conditions (CDL):
Equal(MeasureOfAngle(DCA),36)
IsCentreOfCircle(O,O)
IsTangentOfCircle(CB,O)
Goal: Value(MeasureOfAngle(DBA))
Answer: 63
Theorem sequence:
tangent_of_circle_property_perpendicular(1,CB,O,O)
triangle_property_angle_sum(1,OAB)
adjacent_complementary_angle(1,COB,BOA)
radius_of_circle_property_length_equal(1,OA,O)
radius_of_circle_property_length_equal(1,OB,O)
isosceles_triangle_judgment_line_equal(1,OAB)
isosceles_triangle_property_angle_equal(1,OAB)
triangle_property_angle_sum(1,COB)
angle_addition(1,ABO,OBC)
adjacent_complementary_angle(1,DBA,ABC)
Problem: As shown in the diagram, AB=2*sqrt(3), BC=2*sqrt(3), CF=DF, ED=EA, O is the center of circle O. Find the perimeter of △BEF.
问题：如图所示，AB=2*sqrt(3)，BC=2*sqrt(3)，CF=DF，ED=EA，O是⊙O的圆心。求三角形BEF的周长。
Construction (CDL):
Shape(BE,ED,DF,FB)
Shape(DE,EA,ODA)
Shape(CF,FD,OCD)
Shape(ODA,OAC,OCD)
Collinear(EDF)
Collinear(AEB)
Collinear(BFC)
Cocircular(O,DAC)
Conditions (CDL):
Equal(LengthOfLine(AB),2*sqrt(3))
Equal(LengthOfLine(BC),2*sqrt(3))
Equal(LengthOfLine(CF),LengthOfLine(DF))
Equal(LengthOfLine(ED),LengthOfLine(EA))
IsCentreOfCircle(O,O)
Goal: Value(PerimeterOfTriangle(BEF))
Answer: 4*sqrt(3)
Theorem sequence:
line_addition(1,ED,DF)
line_addition(1,AE,EB)
line_addition(1,BF,FC)
triangle_perimeter_formula(1,BEF)
Problem: As shown in the diagram, AD=4, DC=9, the center of circle O is O, the diameter of ⊙O is AB, the tangent to circle O is CB, CE is the tangent to circle O, the tangent to circle O is DA, DE is the tangent to circle O. Find the length of line BC.
问题：如图所示，AD=4，DC=9，⊙O的圆心为O，AB是圆O的直径，CB是圆O的切线，CE是圆O的切线，圆O的切线为DA，DE是圆O的切线。求直线BC的长度。
Construction (CDL):
Shape(ED,DA,OEA)
Shape(OEA,AE)
Shape(OE,EA,AO)
Shape(OB,OBE,EO)
Shape(BC,CE,OBE)
Collinear(AOB)
Collinear(DEC)
Cocircular(O,EAB)
Conditions (CDL):
Equal(LengthOfLine(AD),4)
Equal(LengthOfLine(DC),9)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AB,O)
IsTangentOfCircle(CB,O)
IsTangentOfCircle(CE,O)
IsTangentOfCircle(DA,O)
IsTangentOfCircle(DE,O)
Goal: Value(LengthOfLine(BC))
Answer: 5
Theorem sequence:
tangent_of_circle_property_length_equal(1,CE,CB,O)
tangent_of_circle_property_length_equal(1,DA,DE,O)
line_addition(1,DE,EC)
Problem: As shown in the diagram, ∠BCD=130°, the center of circle O is O, the diameter of circle O is AB. Find the measure of ∠ABD.
问题：如图所示，∠BCD=130°，⊙O的圆心为O，AB是圆O的直径。求∠ABD的大小。
Construction (CDL):
Shape(ODA,AD)
Shape(DA,AO,OB,BD)
Shape(CD,DB,BC)
Shape(OCD,DC)
Shape(OBC,CB)
Shape(OA,OAB,BO)
Collinear(AOB)
Cocircular(O,ABCD)
Conditions (CDL):
Equal(MeasureOfAngle(BCD),130)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AB,O)
Goal: Value(MeasureOfAngle(ABD))
Answer: 40
Theorem sequence:
round_arc(1,OAB,OBA)
arc_addition_measure(1,OAB,OBD)
arc_property_circumference_angle_internal(1,OAD,B)
arc_property_circumference_angle_internal(1,OBA,D)
arc_property_circumference_angle_internal(1,OBD,C)
diameter_of_circle_property_right_angle(1,BDA,O)
Problem: As shown in the diagram, ∠ABO=70°, O is the center of ⊙O, CA is the tangent to ⊙O. Find the measure of ∠BAC.
问题：如图所示，∠ABO=70°，圆O的圆心为O，CA是⊙O的切线。求∠BAC的大小。
Construction (CDL):
Shape(BO,OA,AB)
Shape(OAB,BA)
Shape(BA,AC)
Cocircular(O,AB)
Conditions (CDL):
Equal(MeasureOfAngle(ABO),70)
IsCentreOfCircle(O,O)
IsTangentOfCircle(CA,O)
Goal: Value(MeasureOfAngle(BAC))
Answer: 20
Theorem sequence:
tangent_of_circle_property_perpendicular(1,CA,O,O)
angle_addition(1,OAB,BAC)
radius_of_circle_property_length_equal(1,OA,O)
radius_of_circle_property_length_equal(1,OB,O)
isosceles_triangle_judgment_line_equal(1,OAB)
isosceles_triangle_property_angle_equal(1,OAB)
Problem: As shown in the diagram, ∠CAB=55°, O is the center of circle O, the tangent to circle O is CA. Find the measure of ∠AOB.
问题：如图所示，∠CAB=55°，⊙O的圆心为O，CA是圆O的切线。求∠AOB的大小。
Construction (CDL):
Shape(AO,OB,BA)
Shape(OBA,AB)
Shape(CA,AB)
Cocircular(O,BA)
Conditions (CDL):
Equal(MeasureOfAngle(CAB),55)
IsCentreOfCircle(O,O)
IsTangentOfCircle(CA,O)
Goal: Value(MeasureOfAngle(AOB))
Answer: 110
Theorem sequence:
tangent_of_circle_property_perpendicular(2,CA,O,O)
angle_addition(1,CAB,BAO)
radius_of_circle_property_length_equal(1,OB,O)
radius_of_circle_property_length_equal(1,OA,O)
isosceles_triangle_judgment_line_equal(1,OBA)
isosceles_triangle_property_angle_equal(1,OBA)
triangle_property_angle_sum(1,AOB)
Problem: As shown in the diagram, ∠BEA=75°, ∠EMD=90°, ∠EQP=90°, ∠PAE=90°, ∠QPA=150°. Find the measure of ∠MDE.
问题：如图所示，∠BEA=75°，∠EMD=90°，∠EQP=90°，∠PAE=90°，∠QPA=150°。求∠MDE的大小。
Construction (CDL):
Shape(QP,PA,AE,EQ)
Shape(DQ,QE,EM,MD)
Shape(BE,EM)
Collinear(DQE)
Collinear(BEM)
Conditions (CDL):
Equal(MeasureOfAngle(BEA),75)
Equal(MeasureOfAngle(EMD),90)
Equal(MeasureOfAngle(EQP),90)
Equal(MeasureOfAngle(PAE),90)
Equal(MeasureOfAngle(QPA),150)
Goal: Value(MeasureOfAngle(MDE))
Answer: 15
Theorem sequence:
quadrilateral_property_angle_sum(1,QPAE)
flat_angle(1,BEM)
angle_addition(1,BEA,AEQ)
angle_addition(1,BED,DEM)
triangle_property_angle_sum(1,DEM)
Problem: As shown in the diagram, AB=3, ABCD is a square. Find the area of quadrilateral ABCD.
问题：如图所示，AB=3，ABCD是正方形。求ABCD的面积。
Construction (CDL):
Shape(AB,BC,CD,DA)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Square(ABCD)
Goal: Value(AreaOfQuadrilateral(ABCD))
Answer: 9
Theorem sequence:
parallelogram_area_formula_sine(1,DABC)
Problem: As shown in the diagram, BC=NG, CE=MN, ∠GNA=90°, ∠MCE=42°, ∠MGN=90°, ABCD is a square. Find the measure of ∠MNA.
问题：如图所示，BC=NG，CE=MN，∠GNA=90°，∠MCE=42°，∠MGN=90°，ABCD是正方形。求∠MNA的大小。
Construction (CDL):
Shape(AE,EF,FN,NA)
Shape(FE,EB,BM,MF)
Shape(FM,MG,GH,HF)
Shape(HG,GC,CH)
Shape(NH,HC,CD,DN)
Shape(NF,FH,HN)
Collinear(AND)
Collinear(AEB)
Collinear(EFHC)
Collinear(BMGC)
Collinear(NFM)
Collinear(NHG)
Conditions (CDL):
Equal(LengthOfLine(BC),LengthOfLine(NG))
Equal(LengthOfLine(CE),LengthOfLine(MN))
Equal(MeasureOfAngle(GNA),90)
Equal(MeasureOfAngle(MCE),42)
Equal(MeasureOfAngle(MGN),90)
Square(ABCD)
Goal: Value(MeasureOfAngle(MNA))
Answer: 48
Theorem sequence:
congruent_triangle_judgment_hl(2,MGN,EBC)
congruent_triangle_property_angle_equal(1,NMG,CEB)
angle_addition(1,GNM,MNA)
Problem: As shown in the diagram, AB=1, ∠CAB=45°, AE is the angle bisector of ∠OAB, ABCD is a square. Find the length of line DE.
问题：如图所示，AB=1，∠CAB=45°，AE是∠OAB的角平分线，四边形ABCD是正方形。求直线DE的长度。
Construction (CDL):
Shape(AB,BE,EA)
Shape(AE,EO,OA)
Shape(AO,OD,DA)
Shape(OE,EB,BC,CO)
Shape(OC,CD,DO)
Collinear(AOC)
Collinear(BEOD)
Conditions (CDL):
Equal(LengthOfLine(AB),1)
Equal(MeasureOfAngle(CAB),45)
IsBisectorOfAngle(AE,OAB)
Square(ABCD)
Goal: Value(LengthOfLine(DE))
Answer: 1
Theorem sequence:
kite_property_diagonal_perpendicular_bisection(1,ABCD,O)
isosceles_triangle_judgment_line_equal(1,ABD)
isosceles_triangle_property_angle_equal(1,ABD)
triangle_property_angle_sum(1,ABE)
triangle_property_angle_sum(1,AEO)
triangle_property_angle_sum(1,ABO)
triangle_property_angle_sum(1,AED)
sine_theorem(1,ABE)
sine_theorem(1,EDA)
Problem: As shown in the diagram, AE=1, CF=2, ∠AEB=90°, ∠BFC=90°, ∠EBA=∠FCB, quadrilateral ABCD is a square. Find the length of line AB.
问题：如图所示，AE=1，CF=2，∠AEB=90°，∠BFC=90°，∠EBA=∠FCB，四边形ABCD是正方形。求直线AB的长度。
Construction (CDL):
Shape(AE,EB,BA)
Shape(CB,BF,FC)
Shape(AB,BC,CD,DA)
Collinear(EBF)
Conditions (CDL):
Equal(LengthOfLine(AE),1)
Equal(LengthOfLine(CF),2)
Equal(MeasureOfAngle(AEB),90)
Equal(MeasureOfAngle(BFC),90)
Equal(MeasureOfAngle(EBA),MeasureOfAngle(FCB))
Square(ABCD)
Goal: Value(LengthOfLine(AB))
Answer: sqrt(5)
Theorem sequence:
triangle_property_angle_sum(1,AEB)
triangle_property_angle_sum(1,CBF)
congruent_triangle_judgment_aas(1,BAE,CBF)
congruent_triangle_property_line_equal(1,AEB,BFC)
right_triangle_judgment_angle(1,AEB)
right_triangle_property_pythagorean(1,AEB)
Problem: As shown in the diagram, CA=80, ∠BCA and ∠BCA are the base angles of the isosceles right △ BCA. Find the length of line AB.
问题：如图所示，CA=80，△BCA为等腰直角△。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(CA),80)
IsoscelesRightTriangle(BCA)
Goal: Value(LengthOfLine(AB))
Answer: 40*sqrt(2)
Theorem sequence:
right_triangle_property_pythagorean(1,ABC)
Problem: As shown in the diagram, AB=8, AE=1, AE=GF, AG=EF, FC=1, AE is parallel to GF, EF is parallel to AG, ABCD is a square. Find the length of line EF.
问题：如图所示，AB=8，AE=1，AE=GF，AG=EF，FC=1，AE平行于GF，EF平行于AG，ABCD是正方形。求直线EF的长度。
Construction (CDL):
Shape(AE,EF,FG,GA)
Shape(EB,BC,CF,FE)
Shape(AG,GD,DA)
Collinear(AEB)
Collinear(DGFC)
Conditions (CDL):
Equal(LengthOfLine(AB),8)
Equal(LengthOfLine(AE),1)
Equal(LengthOfLine(AE),LengthOfLine(GF))
Equal(LengthOfLine(AG),LengthOfLine(EF))
Equal(LengthOfLine(FC),1)
ParallelBetweenLine(AE,GF)
ParallelBetweenLine(EF,AG)
Square(ABCD)
Goal: Value(LengthOfLine(EF))
Answer: 10
Theorem sequence:
line_addition(1,DG,GC)
line_addition(1,GF,FC)
right_triangle_judgment_angle(1,GDA)
right_triangle_property_pythagorean(1,GDA)
Problem: As shown in the diagram, BC=8, FB=6, ∠AFE=90°, ∠CAB=45°, ∠CMF=90°, FM is the median of △ FFG, MN is the median of △ MFC, quadrilateral FBCE is a rectangle, CM and MF are the legs of the right triangle CMF, ABCD is a square. Find the length of line MN.
问题：如图所示，BC=8，FB=6，∠AFE=90°，∠CAB=45°，∠CMF=90°，FM是三角形FFG的中线，MN是△MFC的中线，FBCE是矩形，∠CMF是直角三角形CMF的直角，四边形ABCD是正方形。求直线MN的长度。
Construction (CDL):
Shape(AF,FM,MA)
Shape(MF,FN,NM)
Shape(MN,NC,CG,GM)
Shape(FB,BC,CN,NF)
Shape(EG,GC,CE)
Shape(AM,MG,GE,ED,DA)
Collinear(AMGC)
Collinear(AFB)
Collinear(FGE)
Collinear(FNC)
Collinear(DEC)
Collinear(ENB)
Conditions (CDL):
Equal(LengthOfLine(BC),8)
Equal(LengthOfLine(FB),6)
Equal(MeasureOfAngle(AFE),90)
Equal(MeasureOfAngle(CAB),45)
Equal(MeasureOfAngle(CMF),90)
IsMedianOfTriangle(FM,AFG)
IsMedianOfTriangle(MN,MFC)
Rectangle(FBCE)
RightTriangle(CMF)
Square(ABCD)
Goal: Value(LengthOfLine(MN))
Answer: 5
Theorem sequence:
right_triangle_judgment_angle(1,FBC)
right_triangle_property_pythagorean(1,FBC)
right_triangle_property_length_of_median(1,CMF,N)
Problem: As shown in the diagram, triangle BEA is congruent to triangle AGD, AB=13, AE=5, BE=12, CF=5, DF=12, ∠FGE=90°, ABCD is a square. Find the length of line EF.
问题：如图所示，三角形BEA与三角形AGD是全等三角形，AB=13，AE=5，BE=12，CF=5，DF=12，∠FGE=90°，ABCD是正方形。求直线EF的长度。
Construction (CDL):
Shape(EA,AB,BE)
Shape(FE,EB,BC,CF)
Shape(GE,EF,FG)
Shape(DG,GF,FC,CD)
Shape(AE,EG,GD,DA)
Collinear(AEG)
Collinear(DGF)
Conditions (CDL):
CongruentBetweenTriangle(BEA,AGD)
Equal(LengthOfLine(AB),13)
Equal(LengthOfLine(AE),5)
Equal(LengthOfLine(BE),12)
Equal(LengthOfLine(CF),5)
Equal(LengthOfLine(DF),12)
Equal(MeasureOfAngle(FGE),90)
Square(ABCD)
Goal: Value(LengthOfLine(EF))
Answer: 7*sqrt(2)
Theorem sequence:
congruent_triangle_property_line_equal(1,BEA,AGD)
congruent_triangle_property_line_equal(1,ABE,DAG)
line_addition(1,AE,EG)
line_addition(1,DG,GF)
right_triangle_judgment_angle(1,FGE)
right_triangle_property_pythagorean(1,FGE)
Problem: As shown in the diagram, AB=4, BQ=QP, CP=3, MQ=Mul(1/2,LengthOfLine(BP)), ∠BQM=90°, ∠MQP=90°, quadrilateral ABCD is a square. Find the length of line MQ.
问题：如图所示，AB=4，BQ=QP，CP=3，MQ=Mul(1/2,LengthOfLine(BP))，∠BQM=90°，∠MQP=90°，四边形ABCD是正方形。求直线MQ的长度。
Construction (CDL):
Shape(MA,AB,BM)
Shape(MB,BQ,QM)
Shape(MQ,QP,PM)
Shape(QB,BC,CP,PQ)
Shape(AM,MP,PD,DA)
Collinear(DPC)
Collinear(BQP)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(BQ),LengthOfLine(QP))
Equal(LengthOfLine(CP),3)
Equal(LengthOfLine(MQ),Mul(1/2,LengthOfLine(BP)))
Equal(MeasureOfAngle(BQM),90)
Equal(MeasureOfAngle(MQP),90)
Square(ABCD)
Goal: Value(LengthOfLine(MQ))
Answer: 5/2
Theorem sequence:
right_triangle_judgment_angle(1,BCP)
right_triangle_property_pythagorean(1,BCP)
Problem: As shown in the diagram, CD=3, CP=2, EF=5, EF=FN, EQ=DP, EQ=FG, MB=2, MC=CD, ∠CPD=90°, ∠EQF=90°, ∠FGN=90°, ∠MBC=90°. Find the length of line GN.
问题：如图所示，CD=3，CP=2，EF=5，EF=FN，EQ=DP，EQ=FG，MB=2，MC=CD，∠CPD=90°，∠EQF=90°，∠FGN=90°，∠MBC=90°。求直线GN的长度。
Construction (CDL):
Shape(MB,BC,CM)
Shape(DC,CP,PD)
Shape(EQ,QF,FE)
Shape(NF,FG,GN)
Collinear(BCPQFG)
Conditions (CDL):
Equal(LengthOfLine(CD),3)
Equal(LengthOfLine(CP),2)
Equal(LengthOfLine(EF),5)
Equal(LengthOfLine(EF),LengthOfLine(FN))
Equal(LengthOfLine(EQ),LengthOfLine(DP))
Equal(LengthOfLine(EQ),LengthOfLine(FG))
Equal(LengthOfLine(MB),2)
Equal(LengthOfLine(MC),LengthOfLine(CD))
Equal(MeasureOfAngle(CPD),90)
Equal(MeasureOfAngle(EQF),90)
Equal(MeasureOfAngle(FGN),90)
Equal(MeasureOfAngle(MBC),90)
Goal: Value(LengthOfLine(GN))
Answer: 2*sqrt(5)
Theorem sequence:
right_triangle_judgment_angle(1,CPD)
right_triangle_judgment_angle(1,FGN)
right_triangle_property_pythagorean(1,CPD)
right_triangle_property_pythagorean(1,FGN)
Problem: As shown in the diagram, AE=3, BO=CO, EO=OF, FC=1, ∠BOE=∠COF, ∠COB=90°, ∠FOE=90°, quadrilateral ABCD is a square. Find the length of line EF.
问题：如图所示，AE=3，BO=CO，EO=OF，FC=1，∠BOE=∠COF，∠COB=90°，∠FOE=90°，四边形ABCD是正方形。求直线EF的长度。
Construction (CDL):
Shape(OA,AE,EO)
Shape(OE,EG,GO)
Shape(GE,EB,BG)
Shape(GB,BF,FG)
Shape(OG,GF,FO)
Shape(OF,FC,CO)
Shape(AO,OD,DA)
Shape(DO,OC,CD)
Collinear(AOC)
Collinear(BGOD)
Collinear(AEB)
Collinear(BFC)
Collinear(EGF)
Conditions (CDL):
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(BO),LengthOfLine(CO))
Equal(LengthOfLine(EO),LengthOfLine(OF))
Equal(LengthOfLine(FC),1)
Equal(MeasureOfAngle(BOE),MeasureOfAngle(COF))
Equal(MeasureOfAngle(COB),90)
Equal(MeasureOfAngle(FOE),90)
Square(ABCD)
Goal: Value(LengthOfLine(EF))
Answer: sqrt(10)
Theorem sequence:
congruent_triangle_judgment_sas(1,OEB,OFC)
congruent_triangle_property_line_equal(1,OEB,OFC)
line_addition(1,AE,EB)
line_addition(1,BF,FC)
right_triangle_judgment_angle(1,EBF)
right_triangle_property_pythagorean(1,EBF)
Problem: As shown in the diagram, DE=1, DF=2, ∠CFD=90°, ∠DEA=90°, ∠FDC=∠EAD, ABCD is a square. Find the area of quadrilateral ABCD.
问题：如图所示，DE=1，DF=2，∠CFD=90°，∠DEA=90°，∠FDC=∠EAD，ABCD是正方形。求四边形ABCD的面积。
Construction (CDL):
Shape(EA,AD,DE)
Shape(AB,BC,CD,DA)
Shape(DC,CF,FD)
Collinear(EDF)
Conditions (CDL):
Equal(LengthOfLine(DE),1)
Equal(LengthOfLine(DF),2)
Equal(MeasureOfAngle(CFD),90)
Equal(MeasureOfAngle(DEA),90)
Equal(MeasureOfAngle(FDC),MeasureOfAngle(EAD))
Square(ABCD)
Goal: Value(AreaOfQuadrilateral(ABCD))
Answer: 5
Theorem sequence:
congruent_triangle_judgment_aas(3,DEA,CFD)
congruent_triangle_property_line_equal(1,DEA,CFD)
right_triangle_judgment_angle(1,DEA)
right_triangle_property_pythagorean(1,DEA)
parallelogram_area_formula_sine(1,DABC)
Problem: As shown in the diagram, AB=12, BF=3, ∠FEB=∠DFC, ABCD is a square, EFGH is a square. Find the length of line EF.
问题：如图所示，AB=12，BF=3，∠FEB=∠DFC，四边形ABCD是正方形，EFGH是正方形。求直线EF的长度。
Construction (CDL):
Shape(AE,EH,HG,GD,DA)
Shape(EF,FG,GH,HE)
Shape(FE,EB,BF)
Shape(DG,GF,FC,CD)
Collinear(BFC)
Collinear(AEB)
Collinear(DGF)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(LengthOfLine(BF),3)
Equal(MeasureOfAngle(FEB),MeasureOfAngle(DFC))
Square(ABCD)
Square(EFGH)
Goal: Value(LengthOfLine(EF))
Answer: 15/4
Theorem sequence:
line_addition(1,BF,FC)
similar_triangle_judgment_aa(1,FEB,DFC)
similar_triangle_property_line_ratio(1,FEB,DFC)
similar_triangle_property_line_ratio(1,EBF,FCD)
right_triangle_judgment_angle(1,EBF)
right_triangle_property_pythagorean(1,EBF)
Problem: As shown in the diagram, AC=2, AD=2, ND=4, ∠DAC=90°. Find the sum of the length of line ND and the length of line DC.
问题：如图所示，AC=2，AD=2，ND=4，∠DAC=90°。求直线ND的长度与直线DC的长度之和。
Construction (CDL):
Shape(NA,AD,DN)
Shape(DA,AC,CD)
Conditions (CDL):
Equal(LengthOfLine(AC),2)
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(ND),4)
Equal(MeasureOfAngle(DAC),90)
Goal: Value(Add(LengthOfLine(ND),LengthOfLine(DC)))
Answer: 2*sqrt(2)+4
Theorem sequence:
right_triangle_judgment_angle(1,DAC)
right_triangle_property_pythagorean(1,DAC)
Problem: As shown in the diagram, AB=10, quadrilateral ABCD is a square. Find the area of quadrilateral ABCD.
问题：如图所示，AB=10，四边形ABCD是正方形。求四边形ABCD的面积。
Construction (CDL):
Shape(AB,BC,CD,DA)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Square(ABCD)
Goal: Value(AreaOfQuadrilateral(ABCD))
Answer: 100
Theorem sequence:
parallelogram_area_formula_sine(1,DABC)
Problem: As shown in the diagram, AB=8, BE=CE, CQ=QD, EF=4, ∠ABC=90°, ∠AEP=90°, ∠DAQ=x°, ∠EAB=x°, ∠EFA=90°, ∠FAE=x°, ∠PAB=2*x°, ∠PFE=90°, △AEP is similar to △ECP., ABCD is a square. Find the length of line CP.
问题：如图所示，AB=8，BE=CE，CQ=QD，EF=4，∠ABC=90°，∠AEP=90°，∠DAQ=x°，∠EAB=x°，∠EFA=90°，∠FAE=x°，∠PAB=2*x°，∠PFE=90°，△AEP与△ECP是相似三角形，ABCD是正方形。求直线CP的长度。
Construction (CDL):
Shape(AB,BE,EA)
Shape(FA,AE,EF)
Shape(PF,FE,EP)
Shape(PE,EC,CP)
Shape(AP,PQ,QA)
Shape(AQ,QD,DA)
Collinear(DQPC)
Collinear(BEC)
Collinear(AFP)
Conditions (CDL):
Equal(LengthOfLine(AB),8)
Equal(LengthOfLine(BE),LengthOfLine(CE))
Equal(LengthOfLine(CQ),LengthOfLine(QD))
Equal(LengthOfLine(EF),4)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(AEP),90)
Equal(MeasureOfAngle(DAQ),x)
Equal(MeasureOfAngle(EAB),x)
Equal(MeasureOfAngle(EFA),90)
Equal(MeasureOfAngle(FAE),x)
Equal(MeasureOfAngle(PAB),2*x)
Equal(MeasureOfAngle(PFE),90)
SimilarBetweenTriangle(AEP,ECP)
Square(ABCD)
Goal: Value(LengthOfLine(CP))
Answer: 2
Theorem sequence:
line_addition(1,AF,FP)
mirror_congruent_triangle_judgment_aas(1,EAB,EFA)
mirror_congruent_triangle_property_line_equal(1,EAB,EFA)
right_triangle_judgment_angle(1,EFA)
right_triangle_judgment_angle(1,PFE)
right_triangle_judgment_angle(1,AEP)
right_triangle_property_pythagorean(1,EFA)
right_triangle_property_pythagorean(1,PFE)
right_triangle_property_pythagorean(1,AEP)
similar_triangle_property_line_ratio(1,AEP,ECP)
similar_triangle_property_line_ratio(1,EPA,CPE)
Problem: As shown in the diagram, ∠CEF=60°, ∠FEA=∠AED. Find the measure of ∠AED.
问题：如图所示，∠CEF=60°，∠FEA=∠AED。求∠AED的大小。
Construction (CDL):
Shape(CE,EF)
Shape(FE,EA)
Shape(AE,ED)
Collinear(CED)
Conditions (CDL):
Equal(MeasureOfAngle(CEF),60)
Equal(MeasureOfAngle(FEA),MeasureOfAngle(AED))
Goal: Value(MeasureOfAngle(AED))
Answer: 60
Theorem sequence:
flat_angle(1,CED)
angle_addition(1,CEF,FED)
angle_addition(1,FEA,AED)
Problem: As shown in the diagram, Add(LengthOfLine(AD)=LengthOfLine(DC)), DE=2, EF=EC, ∠CEF=90°, ∠FEA=∠ECD, ABCD is a rectangle. Find the length of line AE.
问题：如图所示，Add(LengthOfLine(AD)=LengthOfLine(DC))，DE=2，EF=EC，∠CEF=90°，∠FEA=∠ECD，ABCD是长方形。求直线AE的长度。
Construction (CDL):
Shape(EA,AF,FE)
Shape(CD,DE,EC)
Shape(EF,FB,BC,CE)
Collinear(AED)
Collinear(AFB)
Conditions (CDL):
Equal(Add(LengthOfLine(AD),LengthOfLine(DC)),8)
Equal(LengthOfLine(DE),2)
Equal(LengthOfLine(EF),LengthOfLine(EC))
Equal(MeasureOfAngle(CEF),90)
Equal(MeasureOfAngle(FEA),MeasureOfAngle(ECD))
Rectangle(ABCD)
Goal: Value(LengthOfLine(AE))
Answer: 3
Theorem sequence:
congruent_triangle_judgment_aas(1,FEA,ECD)
congruent_triangle_property_line_equal(1,FEA,ECD)
line_addition(1,AE,ED)
Problem: As shown in the diagram, AC=6, ∠BOA=60°, ABCD is a rectangle. Find the length of line AB.
问题：如图所示，AC=6，∠BOA=60°，四边形ABCD是矩形。求直线AB的长度。
Construction (CDL):
Shape(AB,BO,OA)
Shape(OB,BC,CO)
Shape(OC,CD,DO)
Shape(AO,OD,DA)
Collinear(AOC)
Collinear(BOD)
Conditions (CDL):
Equal(LengthOfLine(AC),6)
Equal(MeasureOfAngle(BOA),60)
Rectangle(ABCD)
Goal: Value(LengthOfLine(AB))
Answer: 3
Theorem sequence:
rectangle_property_diagonal_equal(1,ABCD)
triangle_property_angle_sum(1,ABO)
triangle_property_angle_sum(1,ABC)
triangle_property_angle_sum(1,ABD)
sine_theorem(1,ABC)
sine_theorem(1,BDA)
Problem: As shown in the diagram, AB=4, AD=2, OA=2, OB=2, ∠BPA=90°, PO is the median of triangle PAB, quadrilateral ADCB is a rectangle. Find the length of line DP.
问题：如图所示，AB=4，AD=2，OA=2，OB=2，∠BPA=90°，PO是△PAB的中线，ADCB是矩形。求直线DP的长度。
Construction (CDL):
Shape(OA,AD,DO)
Shape(AO,OP,PA)
Shape(PO,OB,BP)
Shape(OD,DC,CB,BO)
Collinear(AOB)
Collinear(POD)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(OA),2)
Equal(LengthOfLine(OB),2)
Equal(MeasureOfAngle(BPA),90)
IsMedianOfTriangle(PO,PAB)
Rectangle(ADCB)
Goal: Value(LengthOfLine(DP))
Answer: 2+2*sqrt(2)
Theorem sequence:
right_triangle_judgment_angle(1,OAD)
right_triangle_judgment_angle(1,BPA)
right_triangle_property_pythagorean(1,OAD)
right_triangle_property_length_of_median(1,BPA,O)
line_addition(1,PO,OD)
Problem: As shown in the diagram, AM=MD, AO=OC, OM=3, ABCD is a rectangle. Find the length of line AB.
问题：如图所示，AM=MD，AO=OC，OM=3，四边形ABCD是长方形。求直线AB的长度。
Construction (CDL):
Shape(MA,AO,OM)
Shape(DM,MO,OC,CD)
Shape(OA,AB,BO)
Shape(OB,BC,CO)
Collinear(AMD)
Collinear(AOC)
Conditions (CDL):
Equal(LengthOfLine(AM),LengthOfLine(MD))
Equal(LengthOfLine(AO),LengthOfLine(OC))
Equal(LengthOfLine(OM),3)
Rectangle(ABCD)
Goal: Value(LengthOfLine(AB))
Answer: 6
Theorem sequence:
midsegment_of_triangle_judgment_midpoint(1,OM,ACD)
midsegment_of_triangle_property_length(1,OM,ACD)
parallelogram_property_opposite_line_equal(1,ABCD)