SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(AC)), AD=9, DE is parallel to BC. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AC))，AD=9，DE平行于BC。求直线AB的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(AC)),3/4)
Equal(LengthOfLine(AD),9)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AB))
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,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AB=3, AC=15, DE=2, ABED is similar to ACFD. Find the length of line EF.
问题：如图所示，AB=3，AC=15，DE=2，四边形ABED与四边形ACFD相似。求直线EF的长度。
Construction (CDL):
Shape(DA,AB,BE,ED)
Shape(BC,CF,FE,EB)
Collinear(ABC)
Collinear(DEF)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(AC),15)
Equal(LengthOfLine(DE),2)
SimilarBetweenQuadrilateral(ABED,ACFD)
Goal: Value(LengthOfLine(EF))
Answer: 8
Theorem sequence:
line_addition(1,DE,EF)
similar_quadrilateral_property_line_ratio(1,ABED,ACFD)
similar_quadrilateral_property_line_ratio(1,EDAB,FDAC)
Problem: As shown in the diagram, Div(LengthOfLine(EC)=LengthOfLine(AC)), AD is the angle bisector of ∠CAB, AB∥ED, BA∥DE. Find the ratio of the length of line CD to the length of line CB.
问题：如图所示，Div(LengthOfLine(EC)=LengthOfLine(AC))，AD是∠CAB的角平分线，AB∥ED，BA平行于DE。求直线CD的长度与直线CB的长度之比。
Construction (CDL):
Shape(AB,BD,DA)
Shape(EA,AD,DE)
Shape(ED,DC,CE)
Collinear(BDC)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(EC),LengthOfLine(AC)),5/8)
IsBisectorOfAngle(AD,CAB)
ParallelBetweenLine(AB,ED)
ParallelBetweenLine(BA,DE)
Goal: Value(Div(LengthOfLine(CD),LengthOfLine(CB)))
Answer: 5/8
Theorem sequence:
parallel_property_corresponding_angle(1,ED,AB,C)
parallel_property_corresponding_angle(2,BA,DE,C)
similar_triangle_judgment_aa(1,CED,CAB)
similar_triangle_property_line_ratio(1,EDC,ABC)
similar_triangle_property_line_ratio(1,DCE,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(EC)), BC=10, DE∥BC, DE is parallel to FC, DF∥AC, DF is parallel to EC, EG is parallel to AB, DE and FC are opposite sides of the parallelogram DFCE. Find the length of line FG.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(EC))，BC=10，DE∥BC，DE∥FC，DF平行于AC，DF平行于EC，EG平行于AB，DFCE是▱。求直线FG的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BF,FD)
Shape(ED,DF,FG,GE)
Shape(EG,GC,CE)
Collinear(ADB)
Collinear(AEC)
Collinear(BFGC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(EC)),3/2)
Equal(LengthOfLine(BC),10)
ParallelBetweenLine(DE,BC)
ParallelBetweenLine(DE,FC)
ParallelBetweenLine(DF,AC)
ParallelBetweenLine(DF,EC)
ParallelBetweenLine(EG,AB)
Parallelogram(DFCE)
Goal: Value(LengthOfLine(FG))
Answer: 2
Theorem sequence:
line_addition(1,AE,EC)
line_addition(1,BF,FG)
line_addition(1,BF,FC)
parallel_property_collinear_extend(3,CB,ED,G)
parallel_property_collinear_extend(3,BA,GE,D)
parallelogram_judgment_parallel_and_parallel(1,DBGE)
parallelogram_property_opposite_line_equal(1,FCED)
parallelogram_property_opposite_line_equal(1,BGED)
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CF,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, AC=4, BD=3, CE=6, DF=x, quadrilateral ACDB is similar to quadrilateral AEFB. Find the length of line DF.
问题：如图所示，AC=4，BD=3，CE=6，DF=x，四边形ACDB与四边形AEFB相似。求直线DF的长度。
Construction (CDL):
Shape(BA,AC,CD,DB)
Shape(DC,CE,EF,FD)
Collinear(ACE)
Collinear(BDF)
Conditions (CDL):
Equal(LengthOfLine(AC),4)
Equal(LengthOfLine(BD),3)
Equal(LengthOfLine(CE),6)
Equal(LengthOfLine(DF),x)
SimilarBetweenQuadrilateral(ACDB,AEFB)
Goal: Value(LengthOfLine(DF))
Answer: 9/2
Theorem sequence:
line_addition(1,AC,CE)
line_addition(1,BD,DF)
similar_quadrilateral_property_line_ratio(1,ACDB,AEFB)
similar_quadrilateral_property_line_ratio(1,DBAC,FBAE)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(AC)), AD=6, DE∥BC. Find the length of line BD.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AC))，AD=6，DE∥BC。求直线BD的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(AC)),3/4)
Equal(LengthOfLine(AD),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BD))
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,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(BE)), DC=BD, AG∥BD, AG∥DC. Find the ratio of the length of line AF to the length of line FC.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(BE))，DC=BD，AG∥BD，AG平行于DC。求直线AF的长度与直线FC的长度之比。
Construction (CDL):
Shape(EA,AG,GE)
Shape(GA,AF,FG)
Shape(FA,AB,BD,DF)
Shape(FD,DC,CF)
Collinear(EAB)
Collinear(EGFD)
Collinear(AFC)
Collinear(BDC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(BE)),1/3)
Equal(LengthOfLine(DC),LengthOfLine(BD))
ParallelBetweenLine(AG,BD)
ParallelBetweenLine(AG,DC)
Goal: Value(Div(LengthOfLine(AF),LengthOfLine(FC)))
Answer: 1/3
Theorem sequence:
parallel_property_corresponding_angle(1,AG,BD,E)
parallel_property_corresponding_angle(2,DB,GA,E)
parallel_property_alternate_interior_angle(1,AG,DC)
parallel_property_alternate_interior_angle(2,AG,DC)
similar_triangle_judgment_aa(1,FDC,FGA)
similar_triangle_judgment_aa(1,EBD,EAG)
similar_triangle_property_line_ratio(1,FDC,FGA)
similar_triangle_property_line_ratio(1,DCF,GAF)
similar_triangle_property_line_ratio(1,EBD,EAG)
similar_triangle_property_line_ratio(1,DEB,GEA)
Problem: As shown in the diagram, AE=5, BF=3/2, EC=3, DE is parallel to BC, FD∥CA. Find the length of line BC.
问题：如图所示，AE=5，BF=3/2，EC=3，DE∥BC，FD平行于CA。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BF,FD)
Shape(ED,DF,FC,CE)
Collinear(ADB)
Collinear(AEC)
Collinear(BFC)
Conditions (CDL):
Equal(LengthOfLine(AE),5)
Equal(LengthOfLine(BF),3/2)
Equal(LengthOfLine(EC),3)
ParallelBetweenLine(DE,BC)
ParallelBetweenLine(FD,CA)
Goal: Value(LengthOfLine(BC))
Answer: 4
Theorem sequence:
line_addition(1,AD,DB)
line_addition(1,AE,EC)
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(1,FD,CA,B)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ADE,DBF)
similar_triangle_judgment_aa(1,ADE,ABC)
similar_triangle_property_line_ratio(1,ADE,DBF)
similar_triangle_property_line_ratio(1,EAD,FDB)
similar_triangle_property_line_ratio(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, Div(LengthOfLine(AD)=LengthOfLine(DF)), Div(LengthOfLine(DF)=LengthOfLine(FB)), AG=15, DE is parallel to BC, DE is parallel to FG, FG∥BC. Find the length of line CE.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DF))，Div(LengthOfLine(DF)=LengthOfLine(FB))，AG=15，DE平行于BC，DE∥FG，FG∥BC。求直线CE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DF,FG,GE,ED)
Shape(FB,BC,CG,GF)
Collinear(ADFB)
Collinear(AEGC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DF)),3/2)
Equal(Div(LengthOfLine(DF),LengthOfLine(FB)),2/1)
Equal(LengthOfLine(AG),15)
ParallelBetweenLine(DE,BC)
ParallelBetweenLine(DE,FG)
ParallelBetweenLine(FG,BC)
Goal: Value(LengthOfLine(CE))
Answer: 9
Theorem sequence:
line_addition(1,AD,DF)
line_addition(1,AF,FB)
line_addition(1,AE,EC)
parallel_property_corresponding_angle(1,DE,FG,A)
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,GF,ED,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ADE,AFG)
similar_triangle_judgment_aa(1,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,FGA)
similar_triangle_property_line_ratio(1,EAD,GAF)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AF=4, BD=6, CD=3, AD is the angle bisector of ∠EAC, EG perpendicular bisects AD, FG is the perpendicular bisector of DA. Find the length of line BE.
问题：如图所示，AF=4，BD=6，CD=3，AD平分∠EAC，EG垂直平分AB，FG是DA的垂直平分线。求直线BE的长度。
Construction (CDL):
Shape(BE,ED,DB)
Shape(EG,GD,DE)
Shape(EA,AG,GE)
Shape(GA,AF,FG)
Shape(GF,FD,DG)
Shape(DF,FC,CD)
Collinear(AEB)
Collinear(AFC)
Collinear(AGD)
Collinear(BDC)
Collinear(EGF)
Conditions (CDL):
Equal(LengthOfLine(AF),4)
Equal(LengthOfLine(BD),6)
Equal(LengthOfLine(CD),3)
IsBisectorOfAngle(AD,EAC)
IsPerpendicularBisectorOfLine(EG,AD)
IsPerpendicularBisectorOfLine(FG,DA)
Goal: Value(LengthOfLine(BE))
Answer: 8
Theorem sequence:
perpendicular_bisector_property_distance_equal(1,EG,AD)
perpendicular_bisector_property_distance_equal(1,FG,DA)
isosceles_triangle_judgment_line_equal(1,EAD)
isosceles_triangle_judgment_line_equal(1,FDA)
isosceles_triangle_property_angle_equal(1,EAD)
isosceles_triangle_property_angle_equal(1,FDA)
parallel_judgment_alternate_interior_angle(1,AE,FD)
parallel_judgment_alternate_interior_angle(2,ED,AF)
parallel_judgment_alternate_interior_angle(2,ED,AC)
parallelogram_judgment_parallel_and_parallel(1,EAFD)
kite_judgment_equal_and_equal(1,EAFD)
rhombus_judgment_parallelogram_and_kite(1,EAFD)
line_addition(1,AE,EB)
line_addition(1,BD,DC)
parallel_property_corresponding_angle(1,ED,AF,B)
parallel_property_corresponding_angle(2,CA,DE,B)
similar_triangle_judgment_aa(1,BED,BAC)
similar_triangle_property_line_ratio(1,EDB,ACB)
similar_triangle_property_line_ratio(1,DBE,CBA)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), AE=6, DE is parallel to BC. Find the length of line EC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，AE=6，DE平行于BC。求直线EC的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),3/5)
Equal(LengthOfLine(AE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(EC))
Answer: 10
Theorem sequence:
line_addition(1,AE,EC)
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,DEA,BCA)
Problem: As shown in the diagram, AD=2, AE=3, BD=4, DE is parallel to BC. Find the length of line AC.
问题：如图所示，AD=2，AE=3，BD=4，DE平行于BC。求直线AC的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(BD),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AC))
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,DEA,BCA)
Problem: As shown in the diagram, AE=2, CG=BD, ED=EC, triangle ABC is an equilateral triangle. Find the length of line BD.
问题：如图所示，AE=2，CG=BD，ED=EC，三角形ABC为等边三角形。求直线BD的长度。
Construction (CDL):
Shape(EA,AF,FE)
Shape(FA,AB,BD,DF)
Shape(FD,DC,CF)
Shape(FC,CE,EF)
Shape(EC,CG,GE)
Collinear(EFD)
Collinear(AFC)
Collinear(BDCG)
Collinear(EAB)
Conditions (CDL):
Equal(LengthOfLine(AE),2)
Equal(LengthOfLine(CG),LengthOfLine(BD))
Equal(LengthOfLine(ED),LengthOfLine(EC))
EquilateralTriangle(ABC)
Goal: Value(LengthOfLine(BD))
Answer: 2
Theorem sequence:
isosceles_triangle_judgment_line_equal(1,EDC)
isosceles_triangle_property_angle_equal(1,ABC)
isosceles_triangle_property_angle_equal(1,EDC)
flat_angle(1,BDC)
flat_angle(1,BCG)
angle_addition(1,BDE,EDC)
angle_addition(1,BCE,ECG)
mirror_congruent_triangle_judgment_sas(1,DEB,CGE)
mirror_congruent_triangle_property_angle_equal(1,BDE,GEC)
similar_triangle_judgment_aa(1,ABC,EBG)
line_addition(1,BC,CG)
line_addition(1,EA,AB)
similar_triangle_property_line_ratio(1,ABC,EBG)
similar_triangle_property_line_ratio(1,CAB,GEB)
Problem: As shown in the diagram, AE=3, DE=6, EC=5, DE∥BC. Find the length of line BC.
问题：如图所示，AE=3，DE=6，EC=5，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(DE),6)
Equal(LengthOfLine(EC),5)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 16
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, BC=2, BD=1/2, DE=3/2, DE is parallel to BC. Find the length of line AB.
问题：如图所示，BC=2，BD=1/2，DE=3/2，DE∥BC。求直线AB的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(BC),2)
Equal(LengthOfLine(BD),1/2)
Equal(LengthOfLine(DE),3/2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AB))
Answer: 2
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=6, AP=3, BD=4, DE∥BC, AQ⊥CQ, BQ is perpendicular to AQ. Find the length of line AQ.
问题：如图所示，AD=6，AP=3，BD=4，DE∥BC，AQ垂直于CQ，BQ垂直于AQ。求直线AQ的长度。
Construction (CDL):
Shape(AD,DP,PA)
Shape(PD,DB,BQ,QP)
Shape(AP,PE,EA)
Shape(EP,PQ,QC,CE)
Collinear(DPE)
Collinear(BQC)
Collinear(APQ)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),6)
Equal(LengthOfLine(AP),3)
Equal(LengthOfLine(BD),4)
ParallelBetweenLine(DE,BC)
PerpendicularBetweenLine(AQ,CQ)
PerpendicularBetweenLine(BQ,AQ)
Goal: Value(LengthOfLine(AQ))
Answer: 5
Theorem sequence:
line_addition(1,AD,DB)
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,PAD,QAB)
similar_triangle_property_line_ratio(1,PAD,QAB)
similar_triangle_property_line_ratio(1,DPA,BQA)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(EC)), CD=10, DC and AB are opposite sides of the parallelogram DABC. Find the length of line BF.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(EC))，CD=10，DC和AB是平行四边形DABC的一组对边。求直线BF的长度。
Construction (CDL):
Shape(DA,AE,ED)
Shape(EA,AF,FE)
Shape(DE,EC,CD)
Shape(CE,EF,FB,BC)
Collinear(AFB)
Collinear(AEC)
Collinear(DEF)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(EC)),2/5)
Equal(LengthOfLine(CD),10)
Parallelogram(DABC)
Goal: Value(LengthOfLine(BF))
Answer: 6
Theorem sequence:
parallel_property_alternate_interior_angle(2,DC,AB)
vertical_angle(1,DEC,FEA)
similar_triangle_judgment_aa(1,FEA,DEC)
similar_triangle_property_line_ratio(1,FEA,DEC)
similar_triangle_property_line_ratio(1,EAF,ECD)
parallelogram_property_opposite_line_equal(1,ABCD)
line_addition(1,AF,FB)
Problem: As shown in the diagram, AE=EB, AF=2, AG=3, DF=4, quadrilateral DABC is a ▱. Find the length of line AC.
问题：如图所示，AE=EB，AF=2，AG=3，DF=4，DABC是平行四边形。求直线AC的长度。
Construction (CDL):
Shape(DF,FG,GC,CD)
Shape(GF,FA,AG)
Shape(GA,AE,EG)
Shape(CG,GE,EB,BC)
Shape(BE,EH,HB)
Collinear(DFA)
Collinear(AGC)
Collinear(AEB)
Collinear(FGEH)
Collinear(CBH)
Conditions (CDL):
Equal(LengthOfLine(AE),LengthOfLine(EB))
Equal(LengthOfLine(AF),2)
Equal(LengthOfLine(AG),3)
Equal(LengthOfLine(DF),4)
Parallelogram(DABC)
Goal: Value(LengthOfLine(AC))
Answer: 15
Theorem sequence:
parallel_property_collinear_extend(2,CB,DA,H)
parallel_property_collinear_extend(3,AD,HC,F)
parallel_property_alternate_interior_angle(1,AD,BC)
parallel_property_alternate_interior_angle(2,AF,HC)
parallel_property_alternate_interior_angle(2,DC,AB)
vertical_angle(1,AEF,BEH)
congruent_triangle_judgment_aas(1,BEH,AEF)
congruent_triangle_judgment_aas(2,DAC,BCA)
congruent_triangle_property_line_equal(1,EHB,EFA)
congruent_triangle_property_line_equal(1,CDA,ABC)
line_addition(1,DF,FA)
line_addition(1,AG,GC)
line_addition(1,CB,BH)
similar_triangle_judgment_aa(1,GFA,GHC)
similar_triangle_property_line_ratio(1,GFA,GHC)
similar_triangle_property_line_ratio(1,FAG,HCG)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(AD)), AF=1, BD=CD, BG=GF, DG is parallel to CF, GD is parallel to FC. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AD))，AF=1，BD=CD，BG=GF，DG平行于CF，GD平行于FC。求直线AB的长度。
Construction (CDL):
Shape(AF,FE,EA)
Shape(EF,FG,GD,DE)
Shape(GB,BD,DG)
Shape(AE,EC,CA)
Shape(ED,DC,CE)
Collinear(AED)
Collinear(BDC)
Collinear(FEC)
Collinear(AFGB)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(AD)),1/3)
Equal(LengthOfLine(AF),1)
Equal(LengthOfLine(BD),LengthOfLine(CD))
Equal(LengthOfLine(BG),LengthOfLine(GF))
ParallelBetweenLine(DG,CF)
ParallelBetweenLine(GD,FC)
Goal: Value(LengthOfLine(AB))
Answer: 5
Theorem sequence:
line_addition(1,AF,FG)
line_addition(1,AG,GB)
parallel_property_collinear_extend(3,FC,GD,E)
parallel_property_corresponding_angle(1,FC,GD,A)
parallel_property_corresponding_angle(2,DG,EF,A)
similar_triangle_judgment_aa(1,AFE,AGD)
similar_triangle_property_line_ratio(1,FEA,GDA)
similar_triangle_property_line_ratio(1,EAF,DAG)
Problem: As shown in the diagram, Div(LengthOfLine(DE)=LengthOfLine(EA)), EF=4, EF∥AB, quadrilateral DABC is a ▱. Find the length of line CD.
问题：如图所示，Div(LengthOfLine(DE)=LengthOfLine(EA))，EF=4，EF平行于AB，DC和AB是▱DABC的一组对边。求直线CD的长度。
Construction (CDL):
Shape(DE,EF,FD)
Shape(EA,AB,BF,FE)
Shape(CD,DF,FB,BC)
Collinear(DEA)
Collinear(DFB)
Conditions (CDL):
Equal(Div(LengthOfLine(DE),LengthOfLine(EA)),2/3)
Equal(LengthOfLine(EF),4)
ParallelBetweenLine(EF,AB)
Parallelogram(DABC)
Goal: Value(LengthOfLine(CD))
Answer: 10
Theorem sequence:
line_addition(1,DE,EA)
parallel_property_corresponding_angle(1,EF,AB,D)
parallel_property_corresponding_angle(2,BA,FE,D)
similar_triangle_judgment_aa(1,DEF,DAB)
similar_triangle_property_line_ratio(1,DEF,DAB)
similar_triangle_property_line_ratio(1,FDE,BDA)
parallelogram_property_opposite_line_equal(1,ABCD)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，DE平行于BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),1/3)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 1/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, Div(LengthOfLine(AD)=LengthOfLine(AB)), AE=6, DE is parallel to BC. Find the length of line AC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，AE=6，DE平行于BC。求直线AC的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),3/4)
Equal(LengthOfLine(AE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AC))
Answer: 8
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,DEA,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(DE)), AF=5, BD=DC, EF is parallel to DG, FE∥GD. Find the length of line AC.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(DE))，AF=5，BD=DC，EF平行于DG，FE∥GD。求直线AC的长度。
Construction (CDL):
Shape(AE,EF,FA)
Shape(EB,BD,DE)
Shape(FE,ED,DG,GF)
Shape(GD,DC,CG)
Collinear(AED)
Collinear(AFGC)
Collinear(BEF)
Collinear(BDC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(DE)),1/2)
Equal(LengthOfLine(AF),5)
Equal(LengthOfLine(BD),LengthOfLine(DC))
ParallelBetweenLine(EF,DG)
ParallelBetweenLine(FE,GD)
Goal: Value(LengthOfLine(AC))
Answer: 25
Theorem sequence:
line_addition(1,AE,ED)
line_addition(1,AF,FC)
line_addition(1,AG,GC)
line_addition(1,BD,DC)
parallel_property_corresponding_angle(1,EF,DG,A)
parallel_property_corresponding_angle(1,GD,FE,C)
parallel_property_corresponding_angle(2,GD,FE,A)
similar_triangle_judgment_aa(1,AEF,ADG)
similar_triangle_judgment_aa(1,DCG,BCF)
similar_triangle_property_line_ratio(1,EFA,DGA)
similar_triangle_property_line_ratio(1,FAE,GAD)
similar_triangle_property_line_ratio(1,DCG,BCF)
similar_triangle_property_line_ratio(1,GDC,FBC)
Problem: As shown in the diagram, AB=10, AC=8, BO is the angle bisector of ∠ABC, CO bisects ∠BCA, MN is parallel to BC. Find the sum of the length of line AM, the length of line MN and the length of line NA.
问题：如图所示，AB=10，AC=8，BO平分∠ABC，CO是∠BCA的角平分线，MN平行于BC。求直线AM的长度、直线MN的长度与直线NA的长度之和。
Construction (CDL):
Shape(AM,MO,ON,NA)
Shape(OM,MB,BO)
Shape(OB,BC,CO)
Shape(NO,OC,CN)
Collinear(MON)
Collinear(AMB)
Collinear(ANC)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(LengthOfLine(AC),8)
IsBisectorOfAngle(BO,ABC)
IsBisectorOfAngle(CO,BCA)
ParallelBetweenLine(MN,BC)
Goal: Value(Add(LengthOfLine(AM),LengthOfLine(MN),LengthOfLine(NA)))
Answer: 18
Theorem sequence:
parallel_property_collinear_extend(3,MN,BC,O)
parallel_property_alternate_interior_angle(1,ON,BC)
parallel_property_alternate_interior_angle(2,MO,BC)
isosceles_triangle_judgment_angle_equal(1,MBO)
isosceles_triangle_judgment_angle_equal(1,NOC)
line_addition(1,MO,ON)
line_addition(1,AM,MB)
line_addition(1,AN,NC)
Problem: As shown in the diagram, AD=4, DB=2, DE∥BC. Find the ratio of the length of line AD to the length of line DB.
问题：如图所示，AD=4，DB=2，DE平行于BC。求直线AD的长度与直线DB的长度之比。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AD),4)
Equal(LengthOfLine(DB),2)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(AD),LengthOfLine(DB)))
Answer: 2
Theorem sequence:
Problem: As shown in the diagram, AB=6, BC=3, DE=1, DE is parallel to BC. Find the length of line AD.
问题：如图所示，AB=6，BC=3，DE=1，DE平行于BC。求直线AD的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(BC),3)
Equal(LengthOfLine(DE),1)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AD))
Answer: 2
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)
Problem: As shown in the diagram, AD=2, DB=4, DE is parallel to BC. Find the ratio of the length of line AE to the length of line EC.
问题：如图所示，AD=2，DB=4，DE∥BC。求直线AE的长度与直线EC的长度之比。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(DB),4)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(AE),LengthOfLine(EC)))
Answer: 1/2
Theorem sequence:
line_addition(1,AE,EC)
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,DEA,BCA)
Problem: As shown in the diagram, AB=15, AC=19, BD=4, DE is parallel to BC. Find the length of line AE.
问题：如图所示，AB=15，AC=19，BD=4，DE平行于BC。求直线AE的长度。
Construction (CDL):
Shape(EA,AD,DE)
Shape(CE,ED,DB,BC)
Collinear(AEC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(AB),15)
Equal(LengthOfLine(AC),19)
Equal(LengthOfLine(BD),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AE))
Answer: 209/15
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,DEA,BCA)