SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE=8, DE∥BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，DE=8，DE∥BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),4/5)
Equal(LengthOfLine(DE),8)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 10
Theorem sequence:
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ADE,ABC)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AB=3, BC=5, ∠BAC=90°, CD is perpendicular to AD. Find the length of line DC.
问题：如图所示，AB=3，BC=5，∠BAC=90°，CD垂直于AD。求直线DC的长度。
Construction (CDL):
Shape(AC,CD,DA)
Shape(AD,DB,BA)
Collinear(CDB)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BC),5)
Equal(MeasureOfAngle(BAC),90)
PerpendicularBetweenLine(CD,AD)
Goal: Value(LengthOfLine(DC))
Answer: 16/5
Theorem sequence:
adjacent_complementary_angle(1,CDA,ADB)
mirror_similar_triangle_judgment_aa(1,CBA,ADB)
mirror_similar_triangle_property_line_ratio(1,CBA,ADB)
mirror_similar_triangle_property_line_ratio(1,ACB,DBA)
line_addition(1,CD,DB)
Problem: As shown in the diagram, AD=3, AE=2, CE=3, AD∥BC. Find the length of line BC.
问题：如图所示，AD=3，AE=2，CE=3，AD平行于BC。求直线BC的长度。
Construction (CDL):
Shape(BC,CE,EB)
Shape(ED,DA,AE)
Collinear(BED)
Collinear(CEA)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(AE),2)
Equal(LengthOfLine(CE),3)
ParallelBetweenLine(AD,BC)
Goal: Value(LengthOfLine(BC))
Answer: 9/2
Theorem sequence:
parallel_property_alternate_interior_angle(1,AD,BC)
parallel_property_alternate_interior_angle(2,AD,BC)
similar_triangle_judgment_aa(1,EBC,EDA)
similar_triangle_property_line_ratio(1,EBC,EDA)
similar_triangle_property_line_ratio(1,BCE,DAE)
Problem: As shown in the diagram, DA=5, DE=2, EF=4, EF is parallel to AB, quadrilateral DABC is a parallelogram. Find the length of line CD.
问题：如图所示，DA=5，DE=2，EF=4，EF∥AB，AD和BC是▱DABC的一组对边。求直线CD的长度。
Construction (CDL):
Shape(DE,EF,FD)
Shape(EA,AB,BF,FE)
Shape(DF,FB,BC,CD)
Collinear(DEA)
Collinear(DFB)
Conditions (CDL):
Equal(LengthOfLine(DA),5)
Equal(LengthOfLine(DE),2)
Equal(LengthOfLine(EF),4)
ParallelBetweenLine(EF,AB)
Parallelogram(DABC)
Goal: Value(LengthOfLine(CD))
Answer: 10
Theorem sequence:
parallel_property_corresponding_angle(1,EF,AB,D)
similar_triangle_judgment_aa(1,FDE,BDA)
similar_triangle_property_line_ratio(1,FDE,BDA)
similar_triangle_property_line_ratio(1,DEF,DAB)
parallelogram_property_opposite_line_equal(1,ABCD)
Problem: As shown in the diagram, AD=1, BD=2, DE=2, DE∥BC. Find the length of line BC.
问题：如图所示，AD=1，BD=2，DE=2，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),1)
Equal(LengthOfLine(BD),2)
Equal(LengthOfLine(DE),2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 6
Theorem sequence:
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
similar_triangle_property_line_ratio(1,EAD,CAB)
similar_triangle_property_line_ratio(1,ADE,ABC)
line_addition(1,AD,DB)
Problem: As shown in the diagram, the area of △ADE is 8, BC=3, DE=2, DE∥BC. Find the area of △ABC minus the area of △ADE.
问题：如图所示，三角形ADE的面积为8，BC=3，DE=2，DE平行于BC。求△ABC的面积减去△ADE的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),8)
Equal(LengthOfLine(BC),3)
Equal(LengthOfLine(DE),2)
ParallelBetweenLine(DE,BC)
Goal: Value(Sub(AreaOfTriangle(ABC),AreaOfTriangle(ADE)))
Answer: 10
Theorem sequence:
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_area_square_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AC=6, AE=1, BE=3, AD is parallel to EF, DABC is a parallelogram. Find the length of line AG.
问题：如图所示，AC=6，AE=1，BE=3，AD∥EF，AD和BC是平行四边形DABC的一组对边。求直线AG的长度。
Construction (CDL):
Shape(DA,AG,GF,FD)
Shape(GA,AE,EG)
Shape(CF,FG,GC)
Shape(GE,EB,BC,CG)
Collinear(FGE)
Collinear(AGC)
Collinear(DFC)
Collinear(AEB)
Conditions (CDL):
Equal(LengthOfLine(AC),6)
Equal(LengthOfLine(AE),1)
Equal(LengthOfLine(BE),3)
ParallelBetweenLine(AD,EF)
Parallelogram(DABC)
Goal: Value(LengthOfLine(AG))
Answer: 3/2
Theorem sequence:
parallel_property_collinear_extend(3,DC,AB,F)
parallel_property_collinear_extend(3,BA,FD,E)
parallel_property_collinear_extend(3,BA,CF,E)
parallelogram_judgment_parallel_and_parallel(1,AEFD)
parallelogram_property_opposite_line_equal(1,ABCD)
parallelogram_property_opposite_line_equal(1,AEFD)
line_addition(1,AE,EB)
line_addition(1,DF,FC)
parallel_property_alternate_interior_angle(1,FC,AE)
parallel_property_alternate_interior_angle(2,FC,AE)
similar_triangle_judgment_aa(1,GAE,GCF)
similar_triangle_property_line_ratio(1,GAE,GCF)
similar_triangle_property_line_ratio(1,EGA,FGC)
line_addition(1,AG,GC)
Problem: As shown in the diagram, the area of △ABC is 18, CA=3, CD=2, DE is parallel to AB. Find the area of △DEC.
问题：如图所示，△ABC的面积为18，CA=3，CD=2，DE平行于AB。求三角形DEC的面积。
Construction (CDL):
Shape(CD,DE,EC)
Shape(AB,BE,ED,DA)
Collinear(BEC)
Collinear(ADC)
Conditions (CDL):
Equal(AreaOfTriangle(ABC),18)
Equal(LengthOfLine(CA),3)
Equal(LengthOfLine(CD),2)
ParallelBetweenLine(DE,AB)
Goal: Value(AreaOfTriangle(DEC))
Answer: 8
Theorem sequence:
parallel_property_corresponding_angle(1,DE,AB,C)
similar_triangle_judgment_aa(1,ECD,BCA)
similar_triangle_property_line_ratio(1,ECD,BCA)
similar_triangle_property_area_square_ratio(1,ECD,BCA)
Problem: As shown in the diagram, AD=DF, BE=5, FB=8, E is the midpoint of segment AB. Find the ratio of the length of line CB to the length of line AD.
问题：如图所示，AD=DF，BE=5，FB=8，E平分线段AB。求直线CB的长度与直线AD的长度之比。
Construction (CDL):
Shape(OAC,CE,EA)
Shape(AE,ED,DA)
Shape(CB,BE,EC)
Shape(OCB,BC)
Shape(OBG,GB)
Shape(ODA,AD)
Shape(DE,EB,BG,OGD)
Shape(FD,OGD,GF)
Collinear(AEB)
Collinear(CED)
Collinear(ADF)
Collinear(BGF)
Cocircular(O,CBGDA)
Conditions (CDL):
Equal(LengthOfLine(AD),LengthOfLine(DF))
Equal(LengthOfLine(BE),5)
Equal(LengthOfLine(FB),8)
IsMidpointOfLine(E,AB)
Goal: Value(Div(LengthOfLine(CB),LengthOfLine(AD)))
Answer: 5/4
Theorem sequence:
midsegment_of_triangle_judgment_midpoint(1,ED,ABF)
midsegment_of_triangle_property_parallel(1,ED,ABF)
parallel_property_corresponding_angle(1,ED,BF,A)
similar_triangle_judgment_aa(1,DAE,FAB)
similar_triangle_property_line_ratio(1,DAE,FAB)
similar_triangle_property_line_ratio(1,AED,ABF)
line_addition(1,AE,EB)
vertical_angle(1,AED,BEC)
arc_property_circumference_angle_external(1,OAC,D)
arc_property_circumference_angle_external(1,OAC,B)
mirror_similar_triangle_judgment_aa(1,CBE,AED)
mirror_similar_triangle_property_line_ratio(1,CBE,AED)
mirror_similar_triangle_property_line_ratio(1,ECB,EDA)
Problem: As shown in the diagram, MN is the diameter of ⊙O, D bisects segment BC. Prove that ∠NMD=∠BCA.
问题：如图所示，圆O的直径为MN，D是线段BC的中点。求证∠NMD=∠BCA。
Construction (CDL):
Shape(OAM,MA)
Shape(AM,ME,EA)
Shape(AE,EN,NA)
Shape(ONA,AN)
Shape(MB,BF,OMF)
Shape(OMF,FD,DM)
Shape(MD,DE,EM)
Shape(ED,DN,NE)
Shape(ODN,ND)
Shape(OFD,DF)
Shape(DC,CN,ODN)
Collinear(AMB)
Collinear(ANC)
Collinear(BFDC)
Collinear(AED)
Collinear(MEN)
Cocircular(O,AMFDN)
Conditions (CDL):
IsDiameterOfCircle(MN,O)
IsMidpointOfLine(D,BC)
Goal: Equal(MeasureOfAngle(NMD),MeasureOfAngle(BCA))
Answer: 0
Theorem sequence:
diameter_of_circle_property_right_angle(1,NAM,O)
right_triangle_judgment_angle(1,CAB)
median_of_triangle_judgment(1,AD,ABC)
right_triangle_property_length_of_median(1,CAB,D)
line_addition(1,BD,DC)
isosceles_triangle_judgment_line_equal(1,DCA)
isosceles_triangle_property_angle_equal(1,DCA)
arc_property_circumference_angle_external(1,ODN,M)
arc_property_circumference_angle_external(1,ODN,A)
Problem: As shown in the diagram, AB=12, AF=3, FC=9, quadrilateral ABCD is a rhombus. Find the length of line AE.
问题：如图所示，AB=12，AF=3，FC=9，ABCD是菱形。求直线AE的长度。
Construction (CDL):
Shape(AF,FE,EA)
Shape(AB,BF,FA)
Shape(FB,BC,CF)
Shape(EF,FC,CD,DE)
Collinear(AED)
Collinear(BFE)
Collinear(AFC)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(LengthOfLine(AF),3)
Equal(LengthOfLine(FC),9)
Rhombus(ABCD)
Goal: Value(LengthOfLine(AE))
Answer: 4
Theorem sequence:
parallel_property_collinear_extend(3,AD,BC,E)
parallel_property_alternate_interior_angle(1,AE,BC)
parallel_property_alternate_interior_angle(2,AE,BC)
similar_triangle_judgment_aa(1,FBC,FEA)
similar_triangle_property_line_ratio(1,FBC,FEA)
similar_triangle_property_line_ratio(1,BCF,EAF)
Problem: As shown in the diagram, AB=4, BC=6, CE=2, OM is parallel to BC, BA and CD are opposite sides of the ▱ ABCD. Find the length of line CF.
问题：如图所示，AB=4，BC=6，CE=2，OM∥BC，ABCD是▱。求直线CF的长度。
Construction (CDL):
Shape(AB,BO,OA)
Shape(AO,OD,DA)
Shape(OB,BF,FO)
Shape(DO,OM,MD)
Shape(OC,CM,MO)
Shape(OF,FC,CO)
Shape(FE,EC,CF)
Collinear(AOC)
Collinear(BOD)
Collinear(BFC)
Collinear(OFE)
Collinear(ECMD)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(BC),6)
Equal(LengthOfLine(CE),2)
ParallelBetweenLine(OM,BC)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(CF))
Answer: 3/2
Theorem sequence:
parallelogram_property_diagonal_bisection(1,BCDA,O)
parallelogram_property_opposite_line_equal(1,ABCD)
midsegment_of_triangle_judgment_parallel(1,OM,DBC)
midsegment_of_triangle_property_length(1,OM,DBC)
line_addition(1,DM,MC)
line_addition(1,EC,CM)
parallel_property_corresponding_angle(1,CB,MO,E)
similar_triangle_judgment_aa(1,FEC,OEM)
similar_triangle_property_line_ratio(1,FEC,OEM)
similar_triangle_property_line_ratio(1,ECF,EMO)
Problem: As shown in the diagram, the area of △AEF is 3, AE=3, EB=6, DC and AB are opposite sides of the parallelogram DABC. Find the area of △FCD.
问题：如图所示，三角形AEF的面积为3，AE=3，EB=6，DABC是平行四边形。求△FCD的面积。
Construction (CDL):
Shape(DA,AF,FD)
Shape(FA,AE,EF)
Shape(DF,FC,CD)
Shape(FE,EB,BC,CF)
Collinear(AFC)
Collinear(DFE)
Collinear(AEB)
Conditions (CDL):
Equal(AreaOfTriangle(AEF),3)
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(EB),6)
Parallelogram(DABC)
Goal: Value(AreaOfTriangle(FCD))
Answer: 27
Theorem sequence:
line_addition(1,AE,EB)
parallelogram_property_opposite_line_equal(1,ABCD)
parallel_property_collinear_extend(3,BA,CD,E)
parallel_property_alternate_interior_angle(1,DC,AE)
parallel_property_alternate_interior_angle(2,DC,AE)
similar_triangle_judgment_aa(1,FAE,FCD)
similar_triangle_property_line_ratio(1,FAE,FCD)
similar_triangle_property_area_square_ratio(1,FAE,FCD)
Problem: As shown in the diagram, AC=3, EC=1, DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，AC=3，EC=1，DE平行于BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AC),3)
Equal(LengthOfLine(EC),1)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 2/3
Theorem sequence:
line_addition(1,AE,EC)
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,BCA)
Problem: As shown in the diagram, AD=3, DB=6, DE=3, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AD=3，DB=6，DE=3，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(DB),6)
Equal(LengthOfLine(DE),3)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 9
Theorem sequence:
line_addition(1,AD,DB)
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
similar_triangle_property_line_ratio(1,EAD,CAB)
similar_triangle_property_line_ratio(1,ADE,ABC)
Problem: As shown in the diagram, AD=3, DB=6, DE=4, DE∥BC. Find the length of line BC.
问题：如图所示，AD=3，DB=6，DE=4，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(DB),6)
Equal(LengthOfLine(DE),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 12
Theorem sequence:
line_addition(1,AD,DB)
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
similar_triangle_property_line_ratio(1,EAD,CAB)
similar_triangle_property_line_ratio(1,ADE,ABC)
Problem: As shown in the diagram, AD=2, DB=4, DE∥BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，AD=2，DB=4，DE平行于BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(DB),4)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 1/3
Theorem sequence:
line_addition(1,AD,DB)
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
similar_triangle_property_line_ratio(1,EAD,CAB)
similar_triangle_property_line_ratio(1,ADE,ABC)
Problem: As shown in the diagram, AB=20, AC=15, ∠CAB=90°, AD is the altitude of triangle ABC, CF is the angle bisector of ∠BCA. Find the ratio of the length of line DE to the length of line AF.
问题：如图所示，AB=20，AC=15，∠CAB=90°，AD是三角形ABC的高，CF平分∠BCA。求直线DE的长度与直线AF的长度之比。
Construction (CDL):
Shape(AF,FE,EA)
Shape(FB,BD,DE,EF)
Shape(ED,DC,CE)
Shape(AE,EC,CA)
Collinear(AFB)
Collinear(FEC)
Collinear(AED)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AB),20)
Equal(LengthOfLine(AC),15)
Equal(MeasureOfAngle(CAB),90)
IsAltitudeOfTriangle(AD,ABC)
IsBisectorOfAngle(CF,BCA)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(AF)))
Answer: 3/5
Theorem sequence:
right_triangle_judgment_angle(1,CAB)
right_triangle_property_pythagorean(1,CAB)
triangle_area_formula_common(1,ABC)
triangle_area_formula_sine(1,ABC)
right_triangle_judgment_angle(1,ADC)
right_triangle_property_pythagorean(1,ADC)
mirror_similar_triangle_judgment_aa(1,EDC,FCA)
mirror_similar_triangle_property_line_ratio(1,EDC,FCA)
mirror_similar_triangle_property_line_ratio(1,CED,CAF)
Problem: As shown in the diagram, AB=6, AE=4, EF=4, EF is parallel to BC. Find the length of line BC.
问题：如图所示，AB=6，AE=4，EF=4，EF平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AE,EF,FA)
Shape(EB,BC,CF,FE)
Collinear(AEB)
Collinear(AFC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(AE),4)
Equal(LengthOfLine(EF),4)
ParallelBetweenLine(EF,BC)
Goal: Value(LengthOfLine(BC))
Answer: 6
Theorem sequence:
parallel_property_corresponding_angle(1,EF,BC,A)
similar_triangle_judgment_aa(1,FAE,CAB)
similar_triangle_property_line_ratio(1,FAE,CAB)
similar_triangle_property_line_ratio(1,AEF,ABC)
Problem: As shown in the diagram, the area of triangle ECF is 1, E is the midpoint of segment BC, AE⊥FE, quadrilateral ABCD is a square. Find the area of △ABE.
问题：如图所示，三角形ECF的面积为1，E是线段BC的中点，AE垂直于FE，四边形ABCD是正方形。求△ABE的面积。
Construction (CDL):
Shape(AB,BE,EA)
Shape(AE,EF,FD,DA)
Shape(FE,EC,CF)
Collinear(BEC)
Collinear(DFC)
Conditions (CDL):
Equal(AreaOfTriangle(ECF),1)
IsMidpointOfLine(E,BC)
PerpendicularBetweenLine(AE,FE)
Square(ABCD)
Goal: Value(AreaOfTriangle(ABE))
Answer: 4
Theorem sequence:
line_addition(1,BE,EC)
triangle_property_angle_sum(1,ABE)
angle_addition(1,BEA,AEF)
adjacent_complementary_angle(1,BEF,FEC)
similar_triangle_judgment_aa(1,EAB,FEC)
similar_triangle_property_line_ratio(1,EAB,FEC)
similar_triangle_property_area_square_ratio(1,EAB,FEC)
Problem: As shown in the diagram, AE=EB, AF=2, quadrilateral DABC is a ▱. Find the length of line FC.
问题：如图所示，AE=EB，AF=2，DABC是▱。求直线FC的长度。
Construction (CDL):
Shape(DA,AF,FD)
Shape(DF,FC,CD)
Shape(FA,AE,EF)
Shape(CF,FE,EB,BC)
Collinear(DFE)
Collinear(AFC)
Collinear(AEB)
Conditions (CDL):
Equal(LengthOfLine(AE),LengthOfLine(EB))
Equal(LengthOfLine(AF),2)
Parallelogram(DABC)
Goal: Value(LengthOfLine(FC))
Answer: 4
Theorem sequence:
line_addition(1,AE,EB)
parallelogram_property_opposite_line_equal(1,ABCD)
parallel_property_collinear_extend(3,BA,CD,E)
parallel_property_alternate_interior_angle(1,DC,AE)
parallel_property_alternate_interior_angle(2,DC,AE)
similar_triangle_judgment_aa(1,FAE,FCD)
similar_triangle_property_line_ratio(1,FAE,FCD)
similar_triangle_property_line_ratio(1,EFA,DFC)
Problem: As shown in the diagram, BM=6, ∠NDC=∠ADM, quadrilateral DABC is a ▱. Find the perimeter of quadrilateral DABC.
问题：如图所示，BM=6，∠NDC=∠ADM，DABC是▱。求四边形DABC的周长。
Construction (CDL):
Shape(ND,DC,CN)
Shape(DM,MA,AD)
Shape(DA,AB,BC,CD)
Collinear(NDM)
Collinear(MAB)
Collinear(BCN)
Conditions (CDL):
Equal(LengthOfLine(BM),6)
Equal(MeasureOfAngle(NDC),MeasureOfAngle(ADM))
Parallelogram(DABC)
Goal: Value(PerimeterOfQuadrilateral(DABC))
Answer: 12
Theorem sequence:
parallel_property_collinear_extend(1,CB,DA,N)
parallel_property_collinear_extend(2,BA,CD,M)
parallel_property_corresponding_angle(1,DC,MB,N)
parallel_property_corresponding_angle(2,NB,DA,M)
isosceles_triangle_judgment_angle_equal(1,CND)
isosceles_triangle_judgment_angle_equal(1,ADM)
isosceles_triangle_judgment_angle_equal(1,BNM)
line_addition(1,MA,AB)
line_addition(1,BC,CN)
quadrilateral_perimeter_formula(1,DABC)
Problem: As shown in the diagram, AD=3, DE=2, AD is perpendicular to CD, AE⊥DE, △CAB is a right △. Find the length of line CD.
问题：如图所示，AD=3，DE=2，AD⊥CD，AE⊥DE，三角形CAB为直角三角形。求直线CD的长度。
Construction (CDL):
Shape(AE,ED,DA)
Shape(EB,BD,DE)
Shape(AD,DC,CA)
Collinear(AEB)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(DE),2)
PerpendicularBetweenLine(AD,CD)
PerpendicularBetweenLine(AE,DE)
RightTriangle(CAB)
Goal: Value(LengthOfLine(CD))
Answer: 3*sqrt(5)/2
Theorem sequence:
right_triangle_judgment_angle(1,AED)
right_triangle_property_pythagorean(1,AED)
angle_addition(1,CAD,DAB)
triangle_property_angle_sum(1,AED)
mirror_similar_triangle_judgment_aa(1,AED,CAD)
mirror_similar_triangle_property_line_ratio(1,AED,CAD)
mirror_similar_triangle_property_line_ratio(1,DAE,ADC)
Problem: As shown in the diagram, AE=4, BC=12, EC=8, ∠BCD=90°. Find the length of line DE.
问题：如图所示，AE=4，BC=12，EC=8，∠BCD=90°。求直线DE的长度。
Construction (CDL):
Shape(OCA,AE,EC)
Shape(OAD,DA)
Shape(AD,DE,EA)
Shape(CE,EB,BC)
Shape(OBC,CB)
Shape(BE,ED,ODB)
Collinear(AEB)
Collinear(DEC)
Cocircular(O,ADBC)
Conditions (CDL):
Equal(LengthOfLine(AE),4)
Equal(LengthOfLine(BC),12)
Equal(LengthOfLine(EC),8)
Equal(MeasureOfAngle(BCD),90)
Goal: Value(LengthOfLine(DE))
Answer: 2*sqrt(13)
Theorem sequence:
vertical_angle(1,DEA,CEB)
arc_property_circumference_angle_external(1,ODB,C)
arc_property_circumference_angle_external(1,ODB,A)
mirror_similar_triangle_judgment_aa(1,DEA,BCE)
mirror_similar_triangle_property_line_ratio(1,DEA,BCE)
mirror_similar_triangle_property_line_ratio(1,EAD,EBC)
right_triangle_judgment_angle(1,EAD)
right_triangle_property_pythagorean(1,EAD)
Problem: As shown in the diagram, AB=4, BF=1, ABCD is a square, quadrilateral HEFG is a square. Find the length of line EF.
问题：如图所示，AB=4，BF=1，四边形ABCD是正方形，HEFG是正方形。求直线EF的长度。
Construction (CDL):
Shape(AE,EH,HG,GD,DA)
Shape(HE,EF,FG,GH)
Shape(EB,BF,FE)
Shape(DG,GF,FC,CD)
Collinear(AEB)
Collinear(FGD)
Collinear(BFC)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(BF),1)
Square(ABCD)
Square(HEFG)
Goal: Value(LengthOfLine(EF))
Answer: 5/4
Theorem sequence:
triangle_property_angle_sum(1,EBF)
angle_addition(1,BFE,EFG)
adjacent_complementary_angle(1,BFG,GFC)
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, AB=3, BC=4, ∠ABC=90°, DO perpendicular bisects AC, AD∥BC. Find the length of line AD.
问题：如图所示，AB=3，BC=4，∠ABC=90°，DO是AC的垂直平分线，AD平行于BC。求直线AD的长度。
Construction (CDL):
Shape(AB,BE,EO,OA)
Shape(AO,OD,DA)
Shape(OE,EC,CO)
Shape(DO,OC,CD)
Collinear(AOC)
Collinear(EOD)
Collinear(BEC)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BC),4)
Equal(MeasureOfAngle(ABC),90)
IsPerpendicularBisectorOfLine(DO,AC)
ParallelBetweenLine(AD,BC)
Goal: Value(LengthOfLine(AD))
Answer: 25/8
Theorem sequence:
right_triangle_judgment_angle(1,ABC)
right_triangle_property_pythagorean(1,ABC)
line_addition(1,AO,OC)
parallel_property_alternate_interior_angle(1,AD,BC)
mirror_similar_triangle_judgment_aa(1,ABC,DAO)
mirror_similar_triangle_property_line_ratio(1,ABC,DAO)
mirror_similar_triangle_property_line_ratio(1,BCA,ODA)
Problem: As shown in the diagram, CG=Mul(1/3,LengthOfLine(CE)), CH=Mul(1/3,LengthOfLine(CD)), the radius of ⊙O is 6, O is the center of circle O, AO⊥BO, CD is perpendicular to OD, OE is perpendicular to CE. Find the length of line GH.
问题：如图所示，CG=Mul(1/3,LengthOfLine(CE))，CH=Mul(1/3,LengthOfLine(CD))，圆O的半径为6，O是圆O的圆心，AO⊥BO，CD垂直于OD，OE垂直于CE。求直线GH的长度。
Construction (CDL):
Shape(OBC,CG,GE,EB)
Shape(GC,CF,FG)
Shape(EG,GF,FN,NE)
Shape(EN,NO,OE)
Shape(FC,CH,HF)
Shape(NF,FH,HD,DN)
Shape(ND,DO,ON)
Shape(OAC,AD,DH,HC)
Shape(OD,DA,OAB,BE,EO)
Collinear(BEO)
Collinear(ADO)
Collinear(CGE)
Collinear(CHD)
Collinear(CFNO)
Collinear(GFH)
Collinear(END)
Cocircular(O,BCA)
Conditions (CDL):
Equal(LengthOfLine(CG),Mul(1/3,LengthOfLine(CE)))
Equal(LengthOfLine(CH),Mul(1/3,LengthOfLine(CD)))
Equal(RadiusOfCircle(O),6)
IsCentreOfCircle(O,O)
PerpendicularBetweenLine(AO,BO)
PerpendicularBetweenLine(CD,OD)
PerpendicularBetweenLine(OE,CE)
Goal: Value(LengthOfLine(GH))
Answer: 2
Theorem sequence:
radius_of_circle_property_length_equal(1,OC,O)
parallel_judgment_ipsilateral_internal_angle(1,DC,OE)
parallel_judgment_ipsilateral_internal_angle(1,OD,EC)
parallelogram_judgment_parallel_and_parallel(1,CDOE)
rectangle_judgment_right_angle(1,CDOE)
rectangle_property_diagonal_equal(1,CDOE)
similar_triangle_judgment_sas(1,CHG,CDE)
similar_triangle_property_line_ratio(1,GCH,ECD)
similar_triangle_property_line_ratio(1,CHG,CDE)
Problem: As shown in the diagram, the area of △ADE is 1, AE=1, EB=2, DA∥BC. Find the area of △EBC.
问题：如图所示，三角形ADE的面积为1，AE=1，EB=2，DA∥BC。求△EBC的面积。
Construction (CDL):
Shape(DE,EA,AD)
Shape(EB,BC,CE)
Collinear(DEC)
Collinear(AEB)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),1)
Equal(LengthOfLine(AE),1)
Equal(LengthOfLine(EB),2)
ParallelBetweenLine(DA,BC)
Goal: Value(AreaOfTriangle(EBC))
Answer: 4
Theorem sequence:
parallel_property_alternate_interior_angle(1,DA,BC)
parallel_property_alternate_interior_angle(2,DA,BC)
similar_triangle_judgment_aa(1,EAD,EBC)
similar_triangle_property_line_ratio(1,DEA,CEB)
similar_triangle_property_area_square_ratio(1,EAD,EBC)
Problem: As shown in the diagram, AB=4, DF=3, DG=1, FC=1, DG is the altitude of △ DAF, AE is the angle bisector of ∠DAB, AD and BC are opposite sides of the ▱ DABC. Find the length of line AE.
问题：如图所示，AB=4，DF=3，DG=1，FC=1，DG是三角形DAF的高，AE是∠DAB的角平分线，AD和BC是▱DABC的一组对边。求直线AE的长度。
Construction (CDL):
Shape(DA,AG,GD)
Shape(DG,GF,FD)
Shape(EF,FC,CE)
Shape(FG,GA,AB,BC,CF)
Collinear(DFC)
Collinear(EFGA)
Collinear(ECB)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(DF),3)
Equal(LengthOfLine(DG),1)
Equal(LengthOfLine(FC),1)
IsAltitudeOfTriangle(DG,DAF)
IsBisectorOfAngle(AE,DAB)
Parallelogram(DABC)
Goal: Value(LengthOfLine(AE))
Answer: 16*sqrt(2)/3
Theorem sequence:
right_triangle_judgment_angle(1,DGF)
right_triangle_property_pythagorean(1,DGF)
parallel_property_collinear_extend(3,DC,AB,F)
parallel_property_alternate_interior_angle(2,DF,AB)
isosceles_triangle_judgment_angle_equal(1,DAF)
isosceles_triangle_property_line_coincidence(1,DAF,G)
line_addition(1,AG,GF)
parallel_property_collinear_extend(1,CB,DA,E)
parallel_property_alternate_interior_angle(1,EC,DA)
similar_triangle_judgment_aa(1,DAF,BEA)
similar_triangle_property_line_ratio(1,DAF,BEA)
similar_triangle_property_line_ratio(1,AFD,EAB)