SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, BM=10, ∠MBN=30°, BN is perpendicular to MN. Find the length of line MN.
问题：如图所示，BM=10，∠MBN=30°，BN⊥MN。求直线MN的长度。
Construction (CDL):
Shape(MB,BN,NM)
Conditions (CDL):
Equal(LengthOfLine(BM),10)
Equal(MeasureOfAngle(MBN),30)
PerpendicularBetweenLine(BN,MN)
Goal: Value(LengthOfLine(MN))
Answer: 5
Theorem sequence:
sine_theorem(1,MBN)
Problem: As shown in the diagram, AC=2, Tan(MeasureOfAngle(ABC))=1/2, BC is perpendicular to AC. Find the sum of the length of line AC and the length of line BC.
问题：如图所示，AC=2，Tan(MeasureOfAngle(ABC))=1/2，BC垂直于AC。求直线AC的长度与直线BC的长度之和。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AC),2)
Equal(Tan(MeasureOfAngle(ABC)),1/2)
PerpendicularBetweenLine(BC,AC)
Goal: Value(Add(LengthOfLine(AC),LengthOfLine(BC)))
Answer: 6
Theorem sequence:
triangle_property_angle_sum(1,ABC)
sine_theorem(1,CAB)
Problem: As shown in the diagram, AB=4, ∠ACB=30°, ∠BAC=45°, AD is perpendicular to BD. Find the length of line BC.
问题：如图所示，AB=4，∠ACB=30°，∠BAC=45°，AD垂直于BD。求直线BC的长度。
Construction (CDL):
Shape(BA,AD,DB)
Shape(BD,DC,CB)
Collinear(ADC)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(MeasureOfAngle(ACB),30)
Equal(MeasureOfAngle(BAC),45)
PerpendicularBetweenLine(AD,BD)
Goal: Value(LengthOfLine(BC))
Answer: 4*sqrt(2)
Theorem sequence:
sine_theorem(1,BAC)
Problem: As shown in the diagram, Cos(MeasureOfAngle(BCA))=4/5, AB=6, AB is perpendicular to CB. Find the length of line AC.
问题：如图所示，Cos(MeasureOfAngle(BCA))=4/5，AB=6，AB垂直于CB。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(Cos(MeasureOfAngle(BCA)),4/5)
Equal(LengthOfLine(AB),6)
PerpendicularBetweenLine(AB,CB)
Goal: Value(LengthOfLine(AC))
Answer: 10
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, AB=6, Tan(MeasureOfAngle(BCA))=3/4, AB is perpendicular to CB. Find the length of line AC.
问题：如图所示，AB=6，Tan(MeasureOfAngle(BCA))=3/4，AB垂直于CB。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(Tan(MeasureOfAngle(BCA)),3/4)
PerpendicularBetweenLine(AB,CB)
Goal: Value(LengthOfLine(AC))
Answer: 10
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, AC=3, ∠BAC=30°, AC is perpendicular to BC. Find the length of line AB.
问题：如图所示，AC=3，∠BAC=30°，AC⊥BC。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(AC),3)
Equal(MeasureOfAngle(BAC),30)
PerpendicularBetweenLine(AC,BC)
Goal: Value(LengthOfLine(AB))
Answer: 2*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,ACB)
Problem: As shown in the diagram, BC=2, Tan(MeasureOfAngle(BAC))=1/2, AC⊥BC. Find the length of line AB.
问题：如图所示，BC=2，Tan(MeasureOfAngle(BAC))=1/2，AC⊥BC。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(BC),2)
Equal(Tan(MeasureOfAngle(BAC)),1/2)
PerpendicularBetweenLine(AC,BC)
Goal: Value(LengthOfLine(AB))
Answer: 2*sqrt(5)
Theorem sequence:
sine_theorem(1,BAC)
Problem: As shown in the diagram, AB=100, BC=60, AC⊥BC. Find the value of sin(CB).
问题：如图所示，AB=100，BC=60，AC垂直于BC。求sin(CB)的值。
Construction (CDL):
Shape(BA,AC,CB)
Conditions (CDL):
Equal(LengthOfLine(AB),100)
Equal(LengthOfLine(BC),60)
PerpendicularBetweenLine(AC,BC)
Goal: Value(Sin(MeasureOfAngle(CBA)))
Answer: 4/5
Theorem sequence:
right_triangle_judgment_angle(1,ACB)
right_triangle_property_pythagorean(1,ACB)
cosine_theorem(1,BAC)
Problem: As shown in the diagram, AD=3, AE=4, Tan(MeasureOfAngle(ABE))=2/3, AB and CD are the non-parallel sides of isosceles trapezoid ABCD, BE⊥AE, DF⊥CF. Find the length of line BC.
问题：如图所示，AD=3，AE=4，Tan(MeasureOfAngle(ABE))=2/3，ABCD是等腰梯形，BE垂直于AE，DF⊥CF。求直线BC的长度。
Construction (CDL):
Shape(AB,BE,EA)
Shape(AE,EF,FD,DA)
Shape(DF,FC,CD)
Collinear(BEFC)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(AE),4)
Equal(Tan(MeasureOfAngle(ABE)),2/3)
IsoscelesTrapezoid(ABCD)
PerpendicularBetweenLine(BE,AE)
PerpendicularBetweenLine(DF,CF)
Goal: Value(LengthOfLine(BC))
Answer: 15
Theorem sequence:
isosceles_trapezoid_property_angle_equal(1,ABCD)
adjacent_complementary_angle(1,BEA,AEF)
adjacent_complementary_angle(1,BFD,DFC)
parallel_judgment_ipsilateral_internal_angle(1,EA,FD)
parallel_property_collinear_extend(3,CB,DA,F)
parallel_property_collinear_extend(3,FB,DA,E)
parallelogram_judgment_parallel_and_parallel(1,AEFD)
parallelogram_property_opposite_line_equal(1,AEFD)
parallelogram_property_opposite_line_equal(1,EFDA)
triangle_property_angle_sum(1,ABE)
triangle_property_angle_sum(1,DFC)
sine_theorem(1,EAB)
sine_theorem(1,FCD)
line_addition(1,BE,EF)
line_addition(1,BF,FC)
Problem: As shown in the diagram, AC=12, Tan(MeasureOfAngle(BAC))=1/2, AC⊥BC. Find the length of line AB.
问题：如图所示，AC=12，Tan(MeasureOfAngle(BAC))=1/2，AC⊥BC。求直线AB的长度。
Construction (CDL):
Shape(BA,AC,CB)
Shape(BC,CE,ED,DB)
Collinear(ACE)
Conditions (CDL):
Equal(LengthOfLine(AC),12)
Equal(Tan(MeasureOfAngle(BAC)),1/2)
PerpendicularBetweenLine(AC,BC)
Goal: Value(LengthOfLine(AB))
Answer: 6*sqrt(5)
Theorem sequence:
triangle_property_angle_sum(1,BAC)
sine_theorem(1,ACB)
Problem: As shown in the diagram, AF=4, AG=5, DF=8, E is the midpoint of segment AB, quadrilateral ABCD is a rectangle. Find the length of line AC.
问题：如图所示，AF=4，AG=5，DF=8，E平分线段AB，ABCD是矩形。求直线AC的长度。
Construction (CDL):
Shape(DF,FG,GC,CD)
Shape(FA,AG,GF)
Shape(GA,AE,EG)
Shape(CG,GE,EB,BC)
Shape(BE,EH,HB)
Collinear(AFD)
Collinear(AGC)
Collinear(AEB)
Collinear(FGEH)
Collinear(CBH)
Conditions (CDL):
Equal(LengthOfLine(AF),4)
Equal(LengthOfLine(AG),5)
Equal(LengthOfLine(DF),8)
IsMidpointOfLine(E,AB)
Rectangle(ABCD)
Goal: Value(LengthOfLine(AC))
Answer: 25
Theorem sequence:
adjacent_complementary_angle(1,HBA,ABC)
vertical_angle(1,AEF,BEH)
congruent_triangle_judgment_aas(2,FAE,HBE)
congruent_triangle_property_line_equal(1,EFA,EHB)
line_addition(1,AG,GC)
line_addition(1,AF,FD)
line_addition(1,HB,BC)
parallelogram_property_opposite_line_equal(1,BCDA)
parallel_property_alternate_interior_angle(1,AD,BC)
vertical_angle(1,AGF,CGH)
similar_triangle_judgment_aa(1,FAG,HCG)
similar_triangle_property_line_ratio(1,FAG,HCG)
similar_triangle_property_line_ratio(1,GFA,GHC)
Problem: As shown in the diagram, AB=9, BD=3, △ABC is an equilateral △, triangle ADE is an equilateral triangle. Find the length of line CF.
问题：如图所示，AB=9，BD=3，△ABC为等边△，△ADE为等边△。求直线CF的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DF,FA)
Shape(FD,DC,CF)
Shape(AF,FE,EA)
Collinear(BDC)
Collinear(DFE)
Collinear(AFC)
Conditions (CDL):
Equal(LengthOfLine(AB),9)
Equal(LengthOfLine(BD),3)
EquilateralTriangle(ABC)
EquilateralTriangle(ADE)
Goal: Value(LengthOfLine(CF))
Answer: 2
Theorem sequence:
equilateral_triangle_property_angle(1,ABC)
equilateral_triangle_property_angle(1,BCA)
equilateral_triangle_property_angle(1,ADE)
equilateral_triangle_property_angle(1,EAD)
cosine_theorem(1,BDA)
angle_addition(1,CAD,DAB)
angle_addition(1,EAF,FAD)
mirror_similar_triangle_judgment_aa(1,DAB,FEA)
mirror_similar_triangle_property_line_ratio(1,DAB,FEA)
mirror_similar_triangle_property_line_ratio(1,BDA,EAF)
line_addition(1,AF,FC)
Problem: As shown in the diagram, AB=18, AC=18, AD=AG, BC=12, DG=6, FH⊥CH, DEFG is a square. Find the length of line FH.
问题：如图所示，AB=18，AC=18，AD=AG，BC=12，DG=6，FH⊥CH，DEFG是正方形。求直线FH的长度。
Construction (CDL):
Shape(AD,DG,GA)
Shape(DB,BH,HF,FE,ED)
Shape(DE,EF,FG,GD)
Shape(GF,FH,HC,CG)
Collinear(ADB)
Collinear(AGC)
Collinear(BHC)
Collinear(GFH)
Conditions (CDL):
Equal(LengthOfLine(AB),18)
Equal(LengthOfLine(AC),18)
Equal(LengthOfLine(AD),LengthOfLine(AG))
Equal(LengthOfLine(BC),12)
Equal(LengthOfLine(DG),6)
PerpendicularBetweenLine(FH,CH)
Square(DEFG)
Goal: Value(LengthOfLine(FH))
Answer: -9*cos(acos(7/9)/2)-6+12*sqrt(2)
Theorem sequence:
cosine_theorem(1,ABC)
cosine_theorem(1,CAB)
isosceles_triangle_judgment_line_equal(1,ADG)
isosceles_triangle_property_angle_equal(1,ADG)
triangle_property_angle_sum(1,ADG)
sine_theorem(1,GAD)
line_addition(1,AG,GC)
sine_theorem(1,GHC)
line_addition(1,GF,FH)
Problem: As shown in the diagram, Div(LengthOfLine(AB)=LengthOfLine(AC)), AD=3, AD=CE, BC=10, DE∥BC. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(AB)=LengthOfLine(AC))，AD=3，AD=CE，BC=10，DE∥BC。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AB),LengthOfLine(AC)),3/2)
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(AD),LengthOfLine(CE))
Equal(LengthOfLine(BC),10)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 4
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)
similar_triangle_property_line_ratio(1,DEA,BCA)
line_addition(1,AE,EC)
Problem: As shown in the diagram, AB=9, BD=3, ∠ADE=60°, △ABC is an equilateral △. Find the length of line AE.
问题：如图所示，AB=9，BD=3，∠ADE=60°，三角形ABC为等边三角形。求直线AE的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DE,EA)
Shape(DC,CE,ED)
Collinear(BDC)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AB),9)
Equal(LengthOfLine(BD),3)
Equal(MeasureOfAngle(ADE),60)
EquilateralTriangle(ABC)
Goal: Value(LengthOfLine(AE))
Answer: 7
Theorem sequence:
equilateral_triangle_property_angle(1,BCA)
equilateral_triangle_property_angle(1,CAB)
triangle_property_angle_sum(1,ABD)
angle_addition(1,BDA,ADE)
adjacent_complementary_angle(1,BDE,EDC)
similar_triangle_judgment_aa(1,DAB,EDC)
line_addition(1,BD,DC)
line_addition(1,AE,EC)
similar_triangle_property_line_ratio(1,DAB,EDC)
similar_triangle_property_line_ratio(1,ABD,DCE)
Problem: As shown in the diagram, the area of triangle ADE is 8, EA=2, EC=5, ED∥BC. Find the area of △ABC.
问题：如图所示，三角形ADE的面积为8，EA=2，EC=5，ED∥BC。求△ABC的面积。
Construction (CDL):
Shape(EA,AD,DE)
Shape(AB,BC,CA)
Collinear(EAC)
Collinear(DAB)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),8)
Equal(LengthOfLine(EA),2)
Equal(LengthOfLine(EC),5)
ParallelBetweenLine(ED,BC)
Goal: Value(AreaOfTriangle(ABC))
Answer: 18
Theorem sequence:
parallel_property_alternate_interior_angle(1,ED,BC)
parallel_property_alternate_interior_angle(2,ED,BC)
similar_triangle_judgment_aa(1,ADE,ABC)
line_addition(1,EA,AC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_area_square_ratio(1,ADE,ABC)
Problem: As shown in the diagram, AB=15, AC=12, AD=10, AD is the altitude of triangle ABC, the center of ⊙O is O. Find the length of line AE.
问题：如图所示，AB=15，AC=12，AD=10，AD是三角形ABC的高，O是圆O的圆心。求直线AE的长度。
Construction (CDL):
Shape(AB,BO,OA)
Shape(OB,BM,MO)
Shape(AO,OM,MD,DA)
Shape(AD,DC,CA)
Shape(MB,OBE,EM)
Shape(ME,OEC,CD,DM)
Shape(OAB,BA)
Shape(AC,OCA)
Collinear(AOME)
Collinear(BMDC)
Cocircular(O,ABEC)
Conditions (CDL):
Equal(LengthOfLine(AB),15)
Equal(LengthOfLine(AC),12)
Equal(LengthOfLine(AD),10)
IsAltitudeOfTriangle(AD,ABC)
IsCentreOfCircle(O,O)
Goal: Value(LengthOfLine(AE))
Answer: 18
Theorem sequence:
sine_theorem(1,ADC)
arc_property_circumference_angle_external(1,OAB,C)
arc_property_center_angle(1,OAB,O)
radius_of_circle_property_length_equal(1,OA,O)
radius_of_circle_property_length_equal(1,OB,O)
cosine_theorem(1,OAB)
circle_property_length_of_radius_and_diameter(1,O)
diameter_of_circle_judgment_pass_centre(1,AOE,O)
diameter_of_circle_property_length_equal(1,AE,O)
Problem: As shown in the diagram, AB=12, BF=3, ABCD is a square, quadrilateral EFGH is a square. Find the length of line BE.
问题：如图所示，AB=12，BF=3，四边形ABCD是正方形，EFGH是正方形。求直线BE的长度。
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(BFC)
Collinear(FGD)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(LengthOfLine(BF),3)
Square(ABCD)
Square(EFGH)
Goal: Value(LengthOfLine(BE))
Answer: 9/4
Theorem sequence:
angle_addition(1,BFE,EFG)
triangle_property_angle_sum(1,DFC)
adjacent_complementary_angle(1,BFD,DFC)
similar_triangle_judgment_aa(1,EBF,FCD)
similar_triangle_property_line_ratio(1,EBF,FCD)
similar_triangle_property_line_ratio(1,FEB,DFC)
line_addition(1,BF,FC)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(BD)), BC=8, △DAE is mirror congruent to △DEM, DE is parallel to BC. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(BD))，BC=8，三角形DAE与三角形DEM是镜像全等三角形，DE平行于BC。求直线DE的长度。
Construction (CDL):
Shape(MD,DE,EM)
Shape(DA,AE,ED)
Shape(AD,DB,BC,CE,EA)
Collinear(MDB)
Collinear(MEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(BD)),1/3)
Equal(LengthOfLine(BC),8)
MirrorCongruentBetweenTriangle(DAE,DEM)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 2
Theorem sequence:
mirror_congruent_triangle_property_line_equal(1,EDA,EMD)
line_addition(1,MD,DB)
parallel_property_corresponding_angle(1,DE,BC,M)
parallel_property_corresponding_angle(2,CB,ED,M)
similar_triangle_judgment_aa(1,MDE,MBC)
similar_triangle_property_line_ratio(1,MDE,MBC)
similar_triangle_property_line_ratio(1,EMD,CMB)
Problem: As shown in the diagram, AB=12, BF=3, ABCD is a square, quadrilateral EFGH is a square. Find the length of line EF.
问题：如图所示，AB=12，BF=3，ABCD是正方形，EFGH是正方形。求直线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(BFC)
Collinear(FGD)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(LengthOfLine(BF),3)
Square(ABCD)
Square(EFGH)
Goal: Value(LengthOfLine(EF))
Answer: 15/4
Theorem sequence:
angle_addition(1,BFE,EFG)
triangle_property_angle_sum(1,DFC)
adjacent_complementary_angle(1,BFD,DFC)
similar_triangle_judgment_aa(1,EBF,FCD)
similar_triangle_property_line_ratio(1,EBF,FCD)
similar_triangle_property_line_ratio(1,FEB,DFC)
line_addition(1,BF,FC)
right_triangle_judgment_angle(1,EBF)
right_triangle_property_pythagorean(1,EBF)
Problem: As shown in the diagram, AD=5, BA=15, DE=4, DE∥BC. Find the length of line BC.
问题：如图所示，AD=5，BA=15，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),5)
Equal(LengthOfLine(BA),15)
Equal(LengthOfLine(DE),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 12
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=9, AF=3, EF is perpendicular to CF, quadrilateral ABCD is a square. Find the length of line AE.
问题：如图所示，AB=9，AF=3，EF垂直于CF，ABCD是正方形。求直线AE的长度。
Construction (CDL):
Shape(DE,EF,FC,CD)
Shape(EA,AF,FE)
Shape(CF,FB,BC)
Collinear(AED)
Collinear(AFB)
Conditions (CDL):
Equal(LengthOfLine(AB),9)
Equal(LengthOfLine(AF),3)
PerpendicularBetweenLine(EF,CF)
Square(ABCD)
Goal: Value(LengthOfLine(AE))
Answer: 2
Theorem sequence:
angle_addition(1,AFE,EFC)
adjacent_complementary_angle(1,AFC,CFB)
triangle_property_angle_sum(1,EAF)
line_addition(1,AF,FB)
similar_triangle_judgment_aa(1,FEA,CFB)
similar_triangle_property_line_ratio(1,FEA,CFB)
similar_triangle_property_line_ratio(1,EAF,FBC)
Problem: As shown in the diagram, AB=4, BC=3, ∠ABC=90°, ∠CAB=∠CBD, ∠DCB=90°. Find the length of line CD.
问题：如图所示，AB=4，BC=3，∠ABC=90°，∠CAB=∠CBD，∠DCB=90°。求直线CD的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(CB,BD,DC)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(BC),3)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(CAB),MeasureOfAngle(CBD))
Equal(MeasureOfAngle(DCB),90)
Goal: Value(LengthOfLine(CD))
Answer: 9/4
Theorem sequence:
triangle_property_angle_sum(1,ABC)
triangle_property_angle_sum(1,CBD)
sine_theorem(1,BCA)
sine_theorem(1,CBD)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AC)), Div(LengthOfLine(AE)=LengthOfLine(AB)), BC=6. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AC))，Div(LengthOfLine(AE)=LengthOfLine(AB))，BC=6。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AC)),1/2)
Equal(Div(LengthOfLine(AE),LengthOfLine(AB)),1/2)
Equal(LengthOfLine(BC),6)
Goal: Value(LengthOfLine(DE))
Answer: 3
Theorem sequence:
mirror_similar_triangle_judgment_sas(1,ADE,ABC)
mirror_similar_triangle_property_line_ratio(1,ADE,ABC)
mirror_similar_triangle_property_line_ratio(1,DEA,CAB)
Problem: As shown in the diagram, AB=12, BF=3, ABCD is a square, quadrilateral EFGH is a square. Find the length of line BE.
问题：如图所示，AB=12，BF=3，ABCD是正方形，四边形EFGH是正方形。求直线BE的长度。
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(BFC)
Collinear(FGD)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(LengthOfLine(BF),3)
Square(ABCD)
Square(EFGH)
Goal: Value(LengthOfLine(BE))
Answer: 9/4
Theorem sequence:
angle_addition(1,BFE,EFG)
triangle_property_angle_sum(1,DFC)
adjacent_complementary_angle(1,BFD,DFC)
similar_triangle_judgment_aa(1,EBF,FCD)
similar_triangle_property_line_ratio(1,EBF,FCD)
similar_triangle_property_line_ratio(1,FEB,DFC)
line_addition(1,BF,FC)
Problem: As shown in the diagram, AB=2, AC=3, ∠BAC=90°, D is the midpoint of segment BC, AD∥FH, EG∥AD, FE∥CB. Find the sum of the length of line EG, the length of line FH and the length of line EF.
问题：如图所示，AB=2，AC=3，∠BAC=90°，D平分线段BC，AD平行于FH，EG∥AD，FE平行于CB。求直线EG的长度、直线FH的长度与直线EF的长度之和。
Construction (CDL):
Shape(BE,EG,GB)
Shape(EA,AM,ME)
Shape(EM,MD,DG,GE)
Shape(MA,AF,FM)
Shape(MF,FH,HD,DM)
Shape(FC,CH,HF)
Collinear(BGDHC)
Collinear(EMF)
Collinear(AFC)
Collinear(AEB)
Collinear(AMD)
Conditions (CDL):
Equal(LengthOfLine(AB),2)
Equal(LengthOfLine(AC),3)
Equal(MeasureOfAngle(BAC),90)
IsMidpointOfLine(D,BC)
ParallelBetweenLine(AD,FH)
ParallelBetweenLine(EG,AD)
ParallelBetweenLine(FE,CB)
Goal: Value(Add(LengthOfLine(EG),LengthOfLine(FH),LengthOfLine(EF)))
Answer: sqrt(13)
Theorem sequence:
right_triangle_judgment_angle(1,BAC)
right_triangle_property_pythagorean(1,BAC)
line_addition(1,BG,GH)
line_addition(1,BH,HC)
line_addition(1,BD,DC)
median_of_triangle_judgment(1,AD,ACB)
right_triangle_property_length_of_median(1,BAC,D)
parallel_judgment_par_par(1,EG,AD,FH)
parallel_property_collinear_extend(3,BC,EF,G)
parallel_property_collinear_extend(3,GC,EF,H)
parallelogram_judgment_parallel_and_parallel(1,EFHG)
parallelogram_property_opposite_line_equal(1,EFHG)
parallel_property_corresponding_angle(1,EG,AD,B)
parallel_property_corresponding_angle(2,AD,FH,C)
sine_theorem(1,DBA)
sine_theorem(1,DAC)
isosceles_triangle_judgment_angle_equal(1,GBE)
isosceles_triangle_judgment_angle_equal(1,HFC)
Problem: As shown in the diagram, AD=5, DB=3, DE=4, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AD=5，DB=3，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),5)
Equal(LengthOfLine(DB),3)
Equal(LengthOfLine(DE),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 32/5
Theorem sequence:
line_addition(1,AD,DB)
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=AC, AE=3/2, BD=2, CD=3, CE=4, ∠ABC=∠FDE. Find the length of line AF.
问题：如图所示，AB=AC，AE=3/2，BD=2，CD=3，CE=4，∠ABC=∠FDE。求直线AF的长度。
Construction (CDL):
Shape(AF,FD,DE,EA)
Shape(FB,BD,DF)
Shape(ED,DC,CE)
Collinear(AFB)
Collinear(AEC)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AB),LengthOfLine(AC))
Equal(LengthOfLine(AE),3/2)
Equal(LengthOfLine(BD),2)
Equal(LengthOfLine(CD),3)
Equal(LengthOfLine(CE),4)
Equal(MeasureOfAngle(ABC),MeasureOfAngle(FDE))
Goal: Value(LengthOfLine(AF))
Answer: 4
Theorem sequence:
line_addition(1,AE,EC)
line_addition(1,AF,FB)
isosceles_triangle_judgment_line_equal(1,ABC)
isosceles_triangle_property_angle_equal(1,ABC)
triangle_property_angle_sum(1,BDF)
angle_addition(1,BDF,FDE)
adjacent_complementary_angle(1,BDE,EDC)
similar_triangle_judgment_aa(1,DFB,EDC)
similar_triangle_property_line_ratio(1,DFB,EDC)
similar_triangle_property_line_ratio(1,FBD,DCE)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，DE平行于BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),2/3)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 2/3
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, AD=3, DC=4, DE=5/2, ∠FDE=90°, FH⊥EH, quadrilateral ABCD is a rectangle. Find the length of line DF.
问题：如图所示，AD=3，DC=4，DE=5/2，∠FDE=90°，FH垂直于EH，四边形ABCD是长方形。求直线DF的长度。
Construction (CDL):
Shape(FH,HM,MF)
Shape(MD,DE,EM)
Shape(HA,AN,NH)
Shape(MH,HN,ND,DM)
Shape(NA,AB,BC,CN)
Shape(NC,CD,DN)
Collinear(FMD)
Collinear(FHNC)
Collinear(EMHA)
Collinear(AND)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(DC),4)
Equal(LengthOfLine(DE),5/2)
Equal(MeasureOfAngle(FDE),90)
PerpendicularBetweenLine(FH,EH)
Rectangle(ABCD)
Goal: Value(LengthOfLine(DF))
Answer: 10/3
Theorem sequence:
vertical_angle(1,HMF,EMD)
triangle_property_angle_sum(1,MFH)
triangle_property_angle_sum(1,EMD)
angle_addition(1,CDA,ADF)
angle_addition(1,ADF,FDE)
similar_triangle_judgment_aa(1,CDF,ADE)
similar_triangle_property_line_ratio(1,CDF,ADE)
similar_triangle_property_line_ratio(1,FCD,EAD)
Problem: As shown in the diagram, AB=9, BP=3, ∠APD=60°, triangle ABC is an equilateral triangle. Find the length of line CD.
问题：如图所示，AB=9，BP=3，∠APD=60°，△ABC为等边△。求直线CD的长度。
Construction (CDL):
Shape(AB,BP,PA)
Shape(AP,PD,DA)
Shape(DP,PC,CD)
Collinear(BPC)
Collinear(ADC)
Conditions (CDL):
Equal(LengthOfLine(AB),9)
Equal(LengthOfLine(BP),3)
Equal(MeasureOfAngle(APD),60)
EquilateralTriangle(ABC)
Goal: Value(LengthOfLine(CD))
Answer: 2
Theorem sequence:
equilateral_triangle_property_angle(1,BCA)
equilateral_triangle_property_angle(1,CAB)
triangle_property_angle_sum(1,ABP)
angle_addition(1,BPA,APD)
adjacent_complementary_angle(1,BPD,DPC)
line_addition(1,BP,PC)
similar_triangle_judgment_aa(1,PAB,DPC)
similar_triangle_property_line_ratio(1,PAB,DPC)
similar_triangle_property_line_ratio(1,ABP,PCD)
Problem: As shown in the diagram, the area of △DFE is 2, E bisects segment DC, BA and CD are opposite sides of the ▱ ABCD. Find the area of triangle ABF.
问题：如图所示，三角形DFE的面积为2，E平分线段DC，AD和BC是平行四边形ABCD的一组对边。求△ABF的面积。
Construction (CDL):
Shape(DF,FE,ED)
Shape(FA,AB,BF)
Shape(DA,AF,FD)
Shape(EF,FB,BC,CE)
Collinear(DEC)
Collinear(DFB)
Collinear(AFE)
Conditions (CDL):
Equal(AreaOfTriangle(DFE),2)
IsMidpointOfLine(E,DC)
Parallelogram(ABCD)
Goal: Value(AreaOfTriangle(ABF))
Answer: 8
Theorem sequence:
parallelogram_property_opposite_line_equal(1,ABCD)
line_addition(1,DE,EC)
parallel_property_collinear_extend(3,DC,AB,E)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(2,DE,AB)
similar_triangle_judgment_aa(1,FED,FAB)
similar_triangle_property_line_ratio(1,FED,FAB)
similar_triangle_property_area_square_ratio(1,FED,FAB)
Problem: As shown in the diagram, Div(LengthOfLine(AO)=LengthOfLine(OD)), AB∥CD. Find the ratio of the perimeter of triangle AOB to the perimeter of triangle DOC.
问题：如图所示，Div(LengthOfLine(AO)=LengthOfLine(OD))，AB平行于CD。求三角形AOB的周长与三角形DOC的周长之比。
Construction (CDL):
Shape(BA,AO,OB)
Shape(OC,CD,DO)
Collinear(AOD)
Collinear(BOC)
Conditions (CDL):
Equal(Div(LengthOfLine(AO),LengthOfLine(OD)),2/3)
ParallelBetweenLine(AB,CD)
Goal: Value(Div(PerimeterOfTriangle(AOB),PerimeterOfTriangle(DOC)))
Answer: 2/3
Theorem sequence:
parallel_property_alternate_interior_angle(1,AB,CD)
parallel_property_alternate_interior_angle(2,AB,CD)
similar_triangle_judgment_aa(1,OBA,OCD)
similar_triangle_property_line_ratio(1,BAO,CDO)
similar_triangle_property_perimeter_ratio(1,OBA,OCD)