SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, AC=3, BD=AB, ∠ACB=90°, ∠CED=90°, Tan(MeasureOfAngle(BCD))=1/3. Find the value of tan(BA).
问题：如图所示，AC=3，BD=AB，∠ACB=90°，∠CED=90°，Tan(MeasureOfAngle(BCD))=1/3。求tan(BA)的值。
Construction (CDL):
Shape(AC,CB,BA)
Shape(CD,DB,BC)
Shape(CE,ED,DC)
Collinear(ABD)
Collinear(ACE)
Conditions (CDL):
Equal(LengthOfLine(AC),3)
Equal(LengthOfLine(BD),LengthOfLine(AB))
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(CED),90)
Equal(Tan(MeasureOfAngle(BCD)),1/3)
Goal: Value(Tan(MeasureOfAngle(BAC)))
Answer: 3/2
Theorem sequence:
adjacent_complementary_angle(1,ACB,BCE)
parallel_judgment_ipsilateral_internal_angle(1,CB,ED)
parallel_property_corresponding_angle(2,DE,BC,A)
parallel_property_alternate_interior_angle(1,CB,ED)
line_addition(1,AB,BD)
line_addition(1,AC,CE)
similar_triangle_judgment_aa(1,ACB,AED)
similar_triangle_property_line_ratio(1,CBA,EDA)
similar_triangle_property_line_ratio(1,BAC,DAE)
triangle_property_angle_sum(1,CED)
sine_theorem(1,EDC)
right_triangle_judgment_angle(1,AED)
right_triangle_property_pythagorean(1,AED)
sine_theorem(1,DAE)
Problem: As shown in the diagram, AD=2, FG=sqrt(5), G is the midpoint of segment CD, ABCD is a square. Find the length of line AE.
问题：如图所示，AD=2，FG=sqrt(5)，G平分线段CD，ABCD是正方形。求直线AE的长度。
Construction (CDL):
Shape(AF,FD,DA)
Shape(AB,BF,FA)
Shape(DF,FG,GD)
Shape(FB,BC,CG,GF)
Shape(GC,CE,EG)
Collinear(AFGE)
Collinear(BCE)
Collinear(DGC)
Collinear(BFD)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(FG),sqrt(5))
IsMidpointOfLine(G,CD)
Square(ABCD)
Goal: Value(LengthOfLine(AE))
Answer: 6*sqrt(5)
Theorem sequence:
line_addition(1,DG,GC)
parallel_judgment_ipsilateral_internal_angle(1,DG,AB)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(2,DG,AB)
similar_triangle_judgment_aa(1,FAB,FGD)
similar_triangle_property_line_ratio(1,FAB,FGD)
similar_triangle_property_line_ratio(1,BFA,DFG)
line_addition(1,AF,FG)
parallel_property_collinear_extend(2,DG,AB,C)
parallel_property_corresponding_angle(1,GC,AB,E)
parallel_property_corresponding_angle(2,BA,CD,E)
similar_triangle_judgment_aa(1,EGC,EAB)
similar_triangle_property_line_ratio(1,EGC,EAB)
similar_triangle_property_line_ratio(1,CEG,BEA)
line_addition(1,AG,GE)
Problem: As shown in the diagram, AD=3, DB=6, DE=5/2, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AD=3，DB=6，DE=5/2，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),5/2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 15/2
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, the area of △ABC is 16, Div(LengthOfLine(EC)=LengthOfLine(AE)), DE∥BC. Find the area of △ADE.
问题：如图所示，△ABC的面积为16，Div(LengthOfLine(EC)=LengthOfLine(AE))，DE∥BC。求△ADE的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ABC),16)
Equal(Div(LengthOfLine(EC),LengthOfLine(AE)),3)
ParallelBetweenLine(DE,BC)
Goal: Value(AreaOfTriangle(ADE))
Answer: 1
Theorem sequence:
line_addition(1,AE,EC)
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,DEA,BCA)
similar_triangle_property_area_square_ratio(1,ADE,ABC)
Problem: As shown in the diagram, DF=2, E bisects segment AD, ABCD is a rectangle. Find the length of line BF.
问题：如图所示，DF=2，E是线段AD的中点，ABCD是长方形。求直线BF的长度。
Construction (CDL):
Shape(AB,BF,FE,EA)
Shape(EF,FD,DE)
Shape(DF,FC,CD)
Shape(FB,BC,CF)
Collinear(EFC)
Collinear(BFD)
Collinear(AED)
Conditions (CDL):
Equal(LengthOfLine(DF),2)
IsMidpointOfLine(E,AD)
Rectangle(ABCD)
Goal: Value(LengthOfLine(BF))
Answer: 4
Theorem sequence:
line_addition(1,AE,ED)
parallel_property_collinear_extend(3,AD,BC,E)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(1,ED,BC)
parallel_property_alternate_interior_angle(2,ED,BC)
similar_triangle_judgment_aa(1,FDE,FBC)
similar_triangle_judgment_aa(1,ABD,CDB)
similar_triangle_property_line_ratio(1,FDE,FBC)
similar_triangle_property_line_ratio(1,EFD,CFB)
similar_triangle_property_line_ratio(1,ABD,CDB)
similar_triangle_property_line_ratio(1,BDA,DBC)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(DE)), AD=2, DE is parallel to BC. Find the length of line BD.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(DE))，AD=2，DE∥BC。求直线BD的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(DE)),3)
Equal(LengthOfLine(AD),2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BD))
Answer: 4
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,ABC,ADE)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,CAB,EAD)
Problem: As shown in the diagram, AC=4, BC=3, ∠BCA=90°, AD is perpendicular to CD. Find the value of sin(DC).
问题：如图所示，AC=4，BC=3，∠BCA=90°，AD垂直于CD。求sin(DC)的值。
Construction (CDL):
Shape(AD,DC,CA)
Shape(CD,DB,BC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AC),4)
Equal(LengthOfLine(BC),3)
Equal(MeasureOfAngle(BCA),90)
PerpendicularBetweenLine(AD,CD)
Goal: Value(Sin(MeasureOfAngle(DCA)))
Answer: 4/5
Theorem sequence:
line_addition(1,AD,DB)
adjacent_complementary_angle(1,ADC,CDB)
right_triangle_judgment_angle(1,ADC)
right_triangle_judgment_angle(1,CDB)
right_triangle_judgment_angle(1,BCA)
right_triangle_property_pythagorean(1,ADC)
right_triangle_property_pythagorean(1,CDB)
right_triangle_property_pythagorean(1,BCA)
sine_theorem(1,ADC)
Problem: As shown in the diagram, AB=6, AD=2, DE=1, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AB=6，AD=2，DE=1，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(DE),1)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 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, Div(LengthOfLine(BC)=LengthOfLine(BF)), AB and DC are opposite sides of the ▱ BADC. Find the ratio of the length of line BE to the length of line DE.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(BF))，四边形BADC是▱。求直线BE的长度与直线DE的长度之比。
Construction (CDL):
Shape(BE,EF,FB)
Shape(FE,ED,DC,CF)
Shape(AE,EB,BA)
Shape(EA,AD,DE)
Collinear(BFC)
Collinear(BED)
Collinear(AEF)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(BF)),3)
Parallelogram(BADC)
Goal: Value(Div(LengthOfLine(BE),LengthOfLine(DE)))
Answer: 1/3
Theorem sequence:
parallelogram_property_opposite_line_equal(1,ADCB)
parallel_property_collinear_extend(3,BC,AD,F)
parallel_property_alternate_interior_angle(1,BC,AD)
parallel_property_alternate_interior_angle(2,BF,AD)
similar_triangle_judgment_aa(1,EFB,EAD)
similar_triangle_property_line_ratio(1,EFB,EAD)
similar_triangle_property_line_ratio(1,FBE,ADE)
Problem: As shown in the diagram, BF=2, E is the midpoint of segment BC, quadrilateral ABCD is a ▱. Find the length of line FD.
问题：如图所示，BF=2，E是线段BC的中点，四边形ABCD是▱。求直线FD的长度。
Construction (CDL):
Shape(AF,FD,DA)
Shape(AB,BF,FA)
Shape(FB,BE,EF)
Shape(DF,FE,EC,CD)
Collinear(AFE)
Collinear(BEC)
Collinear(BFD)
Conditions (CDL):
Equal(LengthOfLine(BF),2)
IsMidpointOfLine(E,BC)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(FD))
Answer: 4
Theorem sequence:
line_addition(1,BE,EC)
parallelogram_property_opposite_line_equal(1,BCDA)
parallel_property_collinear_extend(3,CB,DA,E)
parallel_property_alternate_interior_angle(1,EB,DA)
parallel_property_alternate_interior_angle(2,EB,DA)
similar_triangle_judgment_aa(1,FDA,FBE)
similar_triangle_property_line_ratio(1,FDA,FBE)
similar_triangle_property_line_ratio(1,AFD,EFB)
Problem: As shown in the diagram, AB=2, ∠BCA=90°, Sin(MeasureOfAngle(ABC))=2/5. Find the length of line AC.
问题：如图所示，AB=2，∠BCA=90°，Sin(MeasureOfAngle(ABC))=2/5。求直线AC的长度。
Construction (CDL):
Shape(BC,CA,AB)
Conditions (CDL):
Equal(LengthOfLine(AB),2)
Equal(MeasureOfAngle(BCA),90)
Equal(Sin(MeasureOfAngle(ABC)),2/5)
Goal: Value(LengthOfLine(AC))
Answer: 4/5
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, the area of △FEA is 2, E is the midpoint of segment AD, quadrilateral ABCD is a rectangle. Find the area of triangle FBC.
问题：如图所示，三角形FEA的面积为2，E是线段AD的中点，ABCD是长方形。求△FBC的面积。
Construction (CDL):
Shape(AF,FE,EA)
Shape(EF,FC,CD,DE)
Shape(AB,BF,FA)
Shape(FB,BC,CF)
Collinear(AED)
Collinear(AFC)
Collinear(BFE)
Conditions (CDL):
Equal(AreaOfTriangle(FEA),2)
IsMidpointOfLine(E,AD)
Rectangle(ABCD)
Goal: Value(AreaOfTriangle(FBC))
Answer: 8
Theorem sequence:
line_addition(1,AE,ED)
parallel_property_collinear_extend(3,AD,BC,E)
parallel_property_alternate_interior_angle(1,AD,BC)
parallel_property_alternate_interior_angle(2,AE,BC)
parallel_property_alternate_interior_angle(2,BA,CD)
similar_triangle_judgment_aa(1,FBC,FEA)
similar_triangle_judgment_aa(1,ACD,CAB)
similar_triangle_property_line_ratio(1,FBC,FEA)
similar_triangle_property_line_ratio(1,CDA,ABC)
similar_triangle_property_line_ratio(1,DAC,BCA)
similar_triangle_property_area_square_ratio(1,FBC,FEA)
Problem: As shown in the diagram, AD=2, BC=3, DE=3/2, CB∥DE. Find the length of line AB.
问题：如图所示，AD=2，BC=3，DE=3/2，CB平行于DE。求直线AB的长度。
Construction (CDL):
Shape(BC,CA,AB)
Shape(AD,DE,EA)
Collinear(BAD)
Collinear(CAE)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(BC),3)
Equal(LengthOfLine(DE),3/2)
ParallelBetweenLine(CB,DE)
Goal: Value(LengthOfLine(AB))
Answer: 4
Theorem sequence:
parallel_property_alternate_interior_angle(1,CB,DE)
parallel_property_alternate_interior_angle(2,CB,DE)
similar_triangle_judgment_aa(1,ABC,ADE)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,CAB,EAD)
Problem: As shown in the diagram, AD=2, BC=10, BD=3, DE is parallel to BC. Find the length of line DE.
问题：如图所示，AD=2，BC=10，BD=3，DE平行于BC。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(BC),10)
Equal(LengthOfLine(BD),3)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 4
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, Div(LengthOfLine(AE)=LengthOfLine(EC)), DE=10, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(EC))，DE=10，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(EC)),5/2)
Equal(LengthOfLine(DE),10)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 14
Theorem sequence:
line_addition(1,AE,EC)
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,DEA,BCA)
Problem: As shown in the diagram, BE=4, EC=6, BD bisects ∠ABC, DE is parallel to AB. Find the length of line AB.
问题：如图所示，BE=4，EC=6，BD是∠ABC的角平分线，DE∥AB。求直线AB的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(DB,BE,ED)
Shape(DE,EC,CD)
Collinear(ADC)
Collinear(BEC)
Conditions (CDL):
Equal(LengthOfLine(BE),4)
Equal(LengthOfLine(EC),6)
IsBisectorOfAngle(BD,ABC)
ParallelBetweenLine(DE,AB)
Goal: Value(LengthOfLine(AB))
Answer: 20/3
Theorem sequence:
line_addition(1,BE,EC)
parallel_property_alternate_interior_angle(1,DE,AB)
isosceles_triangle_judgment_angle_equal(1,EDB)
parallel_property_corresponding_angle(2,BA,ED,C)
similar_triangle_judgment_aa(1,DEC,ABC)
similar_triangle_property_line_ratio(1,DEC,ABC)
similar_triangle_property_line_ratio(1,CDE,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(BE)=LengthOfLine(AE)), EF=3, EF∥BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(BE)=LengthOfLine(AE))，EF=3，EF平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AE,EF,FA)
Shape(EB,BC,CF,FE)
Collinear(AEB)
Collinear(AFC)
Conditions (CDL):
Equal(Div(LengthOfLine(BE),LengthOfLine(AE)),2)
Equal(LengthOfLine(EF),3)
ParallelBetweenLine(EF,BC)
Goal: Value(LengthOfLine(BC))
Answer: 9
Theorem sequence:
line_addition(1,AE,EB)
parallel_property_corresponding_angle(1,EF,BC,A)
parallel_property_corresponding_angle(2,CB,FE,A)
similar_triangle_judgment_aa(1,AEF,ABC)
similar_triangle_property_line_ratio(1,AEF,ABC)
similar_triangle_property_line_ratio(1,FAE,CAB)
Problem: As shown in the diagram, AD=2, BC=6, DB=3, DE is parallel to BC. Find the length of line DE.
问题：如图所示，AD=2，BC=6，DB=3，DE平行于BC。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(BC),6)
Equal(LengthOfLine(DB),3)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 12/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, the area of △ADC is 4/5, AC=2, AD=1, ∠DCA=∠DBC. Find the area of △ABC.
问题：如图所示，三角形ADC的面积为4/5，AC=2，AD=1，∠DCA=∠DBC。求三角形ABC的面积。
Construction (CDL):
Shape(AD,DC,CA)
Shape(DB,BC,CD)
Collinear(ADB)
Conditions (CDL):
Equal(AreaOfTriangle(ADC),4/5)
Equal(LengthOfLine(AC),2)
Equal(LengthOfLine(AD),1)
Equal(MeasureOfAngle(DCA),MeasureOfAngle(DBC))
Goal: Value(AreaOfTriangle(ABC))
Answer: 16/5
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DCA,CAB)
mirror_similar_triangle_property_line_ratio(1,CAD,BCA)
mirror_similar_triangle_property_area_square_ratio(1,DCA,CAB)
Problem: As shown in the diagram, AD=3, BC=5, DB=5, DE∥BC. Find the length of line DE.
问题：如图所示，AD=3，BC=5，DB=5，DE平行于BC。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(BC),5)
Equal(LengthOfLine(DB),5)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 15/8
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, AD=2, OC=3, OD=1, DE is parallel to BC. Find the length of line AB.
问题：如图所示，AD=2，OC=3，OD=1，DE平行于BC。求直线AB的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BO,OD)
Shape(DO,OE,ED)
Shape(EO,OC,CE)
Shape(OB,BC,CO)
Collinear(ADB)
Collinear(AEC)
Collinear(DOC)
Collinear(BOE)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(OC),3)
Equal(LengthOfLine(OD),1)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AB))
Answer: 6
Theorem sequence:
parallel_property_alternate_interior_angle(1,DE,BC)
parallel_property_alternate_interior_angle(2,DE,BC)
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,OBC,OED)
similar_triangle_judgment_aa(1,ABC,ADE)
similar_triangle_property_line_ratio(1,OBC,OED)
similar_triangle_property_line_ratio(1,BCO,EDO)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,CAB,EAD)
Problem: As shown in the diagram, AB=8, AC=12, AD=6, ED is parallel to BC. Find the length of line AE.
问题：如图所示，AB=8，AC=12，AD=6，ED∥BC。求直线AE的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(AB,BC,CA)
Collinear(EAC)
Collinear(DAB)
Conditions (CDL):
Equal(LengthOfLine(AB),8)
Equal(LengthOfLine(AC),12)
Equal(LengthOfLine(AD),6)
ParallelBetweenLine(ED,BC)
Goal: Value(LengthOfLine(AE))
Answer: 9
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)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AB=6, AD=5, AD is the angle bisector of ∠CAB, O is the center of circle O, AB is the diameter of ⊙O, CD∥AB. Find the length of line DE.
问题：如图所示，AB=6，AD=5，AD平分∠CAB，⊙O的圆心为O，⊙O的直径为AB，CD∥AB。求直线DE的长度。
Construction (CDL):
Shape(AC,OCA)
Shape(CA,AE,EC)
Shape(CE,ED,DC)
Shape(CD,ODC)
Shape(AO,OB,BE,EA)
Shape(DE,EB,BD)
Shape(DB,OBD)
Shape(BO,OA,OAB)
Collinear(AED)
Collinear(CEB)
Collinear(AOB)
Cocircular(O,ABDC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(AD),5)
IsBisectorOfAngle(AD,CAB)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AB,O)
ParallelBetweenLine(CD,AB)
Goal: Value(LengthOfLine(DE))
Answer: 7/5
Theorem sequence:
arc_property_circumference_angle_external(1,OBD,A)
arc_property_circumference_angle_external(1,OBD,C)
line_addition(1,AE,ED)
diameter_of_circle_property_right_angle(1,BDA,O)
right_triangle_judgment_angle(1,BDE)
right_triangle_judgment_angle(1,BDA)
right_triangle_property_pythagorean(1,BDE)
right_triangle_property_pythagorean(1,BDA)
parallel_property_alternate_interior_angle(1,CD,AB)
isosceles_triangle_judgment_angle_equal(1,EAB)
Problem: As shown in the diagram, Div(LengthOfLine(CE)=LengthOfLine(BE)), ED is parallel to CA. Find the ratio of the length of line ED to the length of line CA.
问题：如图所示，Div(LengthOfLine(CE)=LengthOfLine(BE))，ED平行于CA。求直线ED的长度与直线CA的长度之比。
Construction (CDL):
Shape(BE,ED,DB)
Shape(DE,EO,OD)
Shape(DO,OA,AD)
Shape(AO,OC,CA)
Shape(OE,EC,CO)
Collinear(BDA)
Collinear(BEC)
Collinear(EOA)
Collinear(DOC)
Conditions (CDL):
Equal(Div(LengthOfLine(CE),LengthOfLine(BE)),3)
ParallelBetweenLine(ED,CA)
Goal: Value(Div(LengthOfLine(ED),LengthOfLine(CA)))
Answer: 1/4
Theorem sequence:
line_addition(1,BE,EC)
parallel_property_corresponding_angle(1,ED,CA,B)
parallel_property_corresponding_angle(2,AC,DE,B)
similar_triangle_judgment_aa(1,BED,BCA)
similar_triangle_property_line_ratio(1,BED,BCA)
similar_triangle_property_line_ratio(1,DBE,ABC)
Problem: As shown in the diagram, Div(LengthOfLine(DB)=LengthOfLine(AD)), DE=4, DE∥BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(DB)=LengthOfLine(AD))，DE=4，DE∥BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(DB),LengthOfLine(AD)),2)
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)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ABC,ADE)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,CAB,EAD)
Problem: As shown in the diagram, Div(LengthOfLine(DB)=LengthOfLine(AD)), BC=8, DE is parallel to BC. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(DB)=LengthOfLine(AD))，BC=8，DE平行于BC。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(DB),LengthOfLine(AD)),3)
Equal(LengthOfLine(BC),8)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 2
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,ABC,ADE)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,CAB,EAD)
Problem: As shown in the diagram, ∠ADE=80°, ∠EAD=60°, Mul(LengthOfLine(AD)=LengthOfLine(AB)). Find the measure of ∠DBC.
问题：如图所示，∠ADE=80°，∠EAD=60°，Mul(LengthOfLine(AD)=LengthOfLine(AB))。求∠DBC的大小。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(MeasureOfAngle(ADE),80)
Equal(MeasureOfAngle(EAD),60)
Equal(Mul(LengthOfLine(AD),LengthOfLine(AB)),Mul(LengthOfLine(AE),LengthOfLine(AC)))
Goal: Value(MeasureOfAngle(DBC))
Answer: 40
Theorem sequence:
mirror_similar_triangle_judgment_sas(1,ADE,ABC)
mirror_similar_triangle_property_angle_equal(1,DEA,CAB)
triangle_property_angle_sum(1,ABC)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(EC)), DE=1, DE∥BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(EC))，DE=1，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(EC)),4/5)
Equal(LengthOfLine(DE),1)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 9/4
Theorem sequence:
line_addition(1,AE,EC)
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,DEA,BCA)
Problem: As shown in the diagram, the area of △ADC is 2, AC=4, AD=2, ∠DCA=∠DBC. Find the area of △ABC minus the area of triangle ADC.
问题：如图所示，三角形ADC的面积为2，AC=4，AD=2，∠DCA=∠DBC。求三角形ABC的面积减去三角形ADC的面积。
Construction (CDL):
Shape(BC,CD,DB)
Shape(AD,DC,CA)
Collinear(ADB)
Conditions (CDL):
Equal(AreaOfTriangle(ADC),2)
Equal(LengthOfLine(AC),4)
Equal(LengthOfLine(AD),2)
Equal(MeasureOfAngle(DCA),MeasureOfAngle(DBC))
Goal: Value(Sub(AreaOfTriangle(ABC),AreaOfTriangle(ADC)))
Answer: 6
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,CAB,DCA)
mirror_similar_triangle_property_line_ratio(1,BCA,CAD)
mirror_similar_triangle_property_area_square_ratio(1,BCA,CAD)
Problem: As shown in the diagram, Div(LengthOfLine(BO)=LengthOfLine(CO)), AD=10, AB∥CD. Find the length of line OA.
问题：如图所示，Div(LengthOfLine(BO)=LengthOfLine(CO))，AD=10，AB平行于CD。求直线OA的长度。
Construction (CDL):
Shape(AO,OB,BA)
Shape(CD,DO,OC)
Collinear(AOD)
Collinear(COB)
Conditions (CDL):
Equal(Div(LengthOfLine(BO),LengthOfLine(CO)),2/3)
Equal(LengthOfLine(AD),10)
ParallelBetweenLine(AB,CD)
Goal: Value(LengthOfLine(OA))
Answer: 4
Theorem sequence:
parallel_property_alternate_interior_angle(1,AB,CD)
vertical_angle(1,AOB,DOC)
line_addition(1,AO,OD)
similar_triangle_judgment_aa(1,CDO,BAO)
similar_triangle_property_line_ratio(1,CDO,BAO)
similar_triangle_property_line_ratio(1,DOC,AOB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE=6, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，DE=6，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)),2/3)
Equal(LengthOfLine(DE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 9
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, CD=6, FD=2, quadrilateral ABCD is a square. Find the length of line ED.
问题：如图所示，CD=6，FD=2，ABCD是正方形。求直线ED的长度。
Construction (CDL):
Shape(EF,FD,DE)
Shape(FA,AB,BF)
Shape(FB,BC,CD,DF)
Collinear(AFD)
Collinear(EDC)
Collinear(EFB)
Conditions (CDL):
Equal(LengthOfLine(CD),6)
Equal(LengthOfLine(FD),2)
Square(ABCD)
Goal: Value(LengthOfLine(ED))
Answer: 3
Theorem sequence:
parallel_property_collinear_extend(3,AD,BC,F)
parallel_property_corresponding_angle(1,FD,BC,E)
parallel_property_corresponding_angle(2,CB,DA,E)
line_addition(1,ED,DC)
similar_triangle_judgment_aa(1,EFD,EBC)
similar_triangle_property_line_ratio(1,EFD,EBC)
similar_triangle_property_line_ratio(1,FDE,BCE)