SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, AB=1, BD=2/5, ∠DAB=∠BCA. Find the length of line BC.
问题：如图所示，AB=1，BD=2/5，∠DAB=∠BCA。求直线BC的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DC,CA)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AB),1)
Equal(LengthOfLine(BD),2/5)
Equal(MeasureOfAngle(DAB),MeasureOfAngle(BCA))
Goal: Value(LengthOfLine(BC))
Answer: 5/2
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DAB,ABC)
mirror_similar_triangle_property_line_ratio(1,DAB,ABC)
mirror_similar_triangle_property_line_ratio(1,ABD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(BD)), DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(BD))，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(BD)),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,ADE,ABC)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, FG=2, G is the midpoint of segment DC, ABCD is a square. Find the length of line AE.
问题：如图所示，FG=2，G是线段DC的中点，ABCD是正方形。求直线AE的长度。
Construction (CDL):
Shape(AF,FD,DA)
Shape(AB,BF,FA)
Shape(FB,BC,CG,GF)
Shape(DF,FG,GD)
Shape(GC,CE,EG)
Collinear(AFGE)
Collinear(BFD)
Collinear(BCE)
Collinear(DGC)
Conditions (CDL):
Equal(LengthOfLine(FG),2)
IsMidpointOfLine(G,DC)
Square(ABCD)
Goal: Value(LengthOfLine(AE))
Answer: 12
Theorem sequence:
line_addition(1,DG,GC)
parallel_property_collinear_extend(3,DC,AB,G)
parallel_property_alternate_interior_angle(1,BA,GD)
vertical_angle(1,BFA,DFG)
similar_triangle_judgment_aa(1,ABF,GDF)
similar_triangle_property_line_ratio(1,FAB,FGD)
similar_triangle_property_line_ratio(1,BFA,DFG)
line_addition(1,AF,FG)
parallel_property_corresponding_angle(1,GC,AB,E)
similar_triangle_judgment_aa(1,CEG,BEA)
similar_triangle_property_line_ratio(1,CEG,BEA)
similar_triangle_property_line_ratio(1,EGC,EAB)
line_addition(1,AG,GE)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), DE∥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(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
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:
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
line_addition(1,AD,DB)
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(DE)=LengthOfLine(EB)), AD=18, EF∥BC, BA and CD are opposite sides of the ▱ ABCD. Find the length of line EF.
问题：如图所示，Div(LengthOfLine(DE)=LengthOfLine(EB))，AD=18，EF∥BC，BA和CD是▱ABCD的一组对边。求直线EF的长度。
Construction (CDL):
Shape(AB,BE,ED,DA)
Shape(DE,EF,FD)
Shape(EB,BC,CF,FE)
Collinear(BED)
Collinear(DFC)
Conditions (CDL):
Equal(Div(LengthOfLine(DE),LengthOfLine(EB)),1/2)
Equal(LengthOfLine(AD),18)
ParallelBetweenLine(EF,BC)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(EF))
Answer: 6
Theorem sequence:
parallelogram_property_opposite_line_equal(1,BCDA)
parallel_property_corresponding_angle(1,EF,BC,D)
parallel_property_corresponding_angle(2,CB,FE,D)
line_addition(1,BE,ED)
similar_triangle_judgment_aa(1,DEF,DBC)
similar_triangle_property_line_ratio(1,DEF,DBC)
similar_triangle_property_line_ratio(1,FDE,CDB)
Problem: As shown in the diagram, AB=4, AD=2, DE=3/2, CB∥DE. Find the length of line BC.
问题：如图所示，AB=4，AD=2，DE=3/2，CB平行于DE。求直线BC的长度。
Construction (CDL):
Shape(BC,CA,AB)
Shape(AD,DE,EA)
Collinear(BAD)
Collinear(CAE)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(DE),3/2)
ParallelBetweenLine(CB,DE)
Goal: Value(LengthOfLine(BC))
Answer: 3
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, the area of △AEF is 3, Div(LengthOfLine(AE)=LengthOfLine(EB)), ABCD is a ▱. Find the area of triangle FCD.
问题：如图所示，△AEF的面积为3，Div(LengthOfLine(AE)=LengthOfLine(EB))，ABCD是平行四边形。求△FCD的面积。
Construction (CDL):
Shape(AF,FD,DA)
Shape(AE,EF,FA)
Shape(DF,FC,CD)
Shape(FE,EB,BC,CF)
Collinear(AFC)
Collinear(DFE)
Collinear(AEB)
Conditions (CDL):
Equal(AreaOfTriangle(AEF),3)
Equal(Div(LengthOfLine(AE),LengthOfLine(EB)),1/2)
Parallelogram(ABCD)
Goal: Value(AreaOfTriangle(FCD))
Answer: 27
Theorem sequence:
parallel_property_collinear_extend(3,BA,CD,E)
parallel_property_alternate_interior_angle(1,AD,BC)
parallel_property_alternate_interior_angle(1,EA,CD)
parallel_property_alternate_interior_angle(2,EA,CD)
similar_triangle_judgment_aa(1,FCD,FAE)
similar_triangle_judgment_aa(1,BCA,DAC)
line_addition(1,AE,EB)
similar_triangle_property_line_ratio(1,FCD,FAE)
similar_triangle_property_line_ratio(1,BCA,DAC)
similar_triangle_property_line_ratio(1,CAB,ACD)
similar_triangle_property_area_square_ratio(1,FCD,FAE)
Problem: As shown in the diagram, Div(LengthOfLine(DP)=LengthOfLine(BQ)), DE∥BC. Find the ratio of the length of line PE to the length of line QC.
问题：如图所示，Div(LengthOfLine(DP)=LengthOfLine(BQ))，DE∥BC。求直线PE的长度与直线QC的长度之比。
Construction (CDL):
Shape(AD,DP,PA)
Shape(AP,PE,EA)
Shape(PD,DB,BQ,QP)
Shape(EP,PQ,QC,CE)
Collinear(DPE)
Collinear(BQC)
Collinear(ADB)
Collinear(AEC)
Collinear(APQ)
Conditions (CDL):
Equal(Div(LengthOfLine(DP),LengthOfLine(BQ)),3/5)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(PE),LengthOfLine(QC)))
Answer: 3/5
Theorem sequence:
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,PAD,QAB)
similar_triangle_judgment_aa(1,PEA,QCA)
similar_triangle_property_line_ratio(1,ADP,ABQ)
similar_triangle_property_line_ratio(1,DPA,BQA)
similar_triangle_property_line_ratio(1,APE,AQC)
similar_triangle_property_line_ratio(1,EAP,CAQ)
Problem: As shown in the diagram, AD=4, BC=6, AD is the altitude of △ ABC, HEFG is a square. Find the length of line HG.
问题：如图所示，AD=4，BC=6，AD是三角形ABC的高，四边形HEFG是正方形。求直线HG的长度。
Construction (CDL):
Shape(AH,HI,IA)
Shape(AI,IG,GA)
Shape(HB,BE,EH)
Shape(HE,ED,DI,IH)
Shape(GI,ID,DF,FG)
Shape(GF,FC,CG)
Collinear(AHB)
Collinear(AGC)
Collinear(AID)
Collinear(HIG)
Collinear(BEDFC)
Conditions (CDL):
Equal(LengthOfLine(AD),4)
Equal(LengthOfLine(BC),6)
IsAltitudeOfTriangle(AD,ABC)
Square(HEFG)
Goal: Value(LengthOfLine(HG))
Answer: 12/5
Theorem sequence:
parallel_judgment_corresponding_angle(2,EH,DI,F)
parallel_property_collinear_extend(1,FE,GH,C)
parallel_property_collinear_extend(2,FE,GH,B)
parallel_property_collinear_extend(3,HG,BE,I)
parallel_property_collinear_extend(1,EB,IH,D)
parallelogram_judgment_parallel_and_parallel(1,HEDI)
parallelogram_property_opposite_line_equal(1,HEDI)
parallel_property_corresponding_angle(1,HG,BF,A)
parallel_property_corresponding_angle(2,CF,GH,A)
parallel_property_corresponding_angle(2,DE,IH,A)
similar_triangle_judgment_aa(1,AHG,ABC)
altitude_of_triangle_judgment(1,AI,AHG)
triangle_area_formula_common(1,AHG)
triangle_area_formula_common(1,ABC)
similar_triangle_property_area_square_ratio(1,AHG,ABC)
similar_triangle_property_line_ratio(1,AHG,ABC)
line_addition(1,AI,ID)
Problem: As shown in the diagram, AM=1, BC=3, MB=2, MN∥BC. Find the length of line MN.
问题：如图所示，AM=1，BC=3，MB=2，MN∥BC。求直线MN的长度。
Construction (CDL):
Shape(AM,MN,NA)
Shape(MB,BC,CN,NM)
Collinear(AMB)
Collinear(ANC)
Conditions (CDL):
Equal(LengthOfLine(AM),1)
Equal(LengthOfLine(BC),3)
Equal(LengthOfLine(MB),2)
ParallelBetweenLine(MN,BC)
Goal: Value(LengthOfLine(MN))
Answer: 1
Theorem sequence:
parallel_property_corresponding_angle(1,MN,BC,A)
parallel_property_corresponding_angle(2,CB,NM,A)
similar_triangle_judgment_aa(1,AMN,ABC)
line_addition(1,AM,MB)
similar_triangle_property_line_ratio(1,AMN,ABC)
similar_triangle_property_line_ratio(1,NAM,CAB)
Problem: As shown in the diagram, ∠ADC=90°, ∠CAD=30°, BC⊥AC. Find the ratio of the perimeter of triangle CDB to the perimeter of △ABC.
问题：如图所示，∠ADC=90°，∠CAD=30°，BC垂直于AC。求三角形CDB的周长与△ABC的周长之比。
Construction (CDL):
Shape(AD,DC,CA)
Shape(CD,DB,BC)
Collinear(ADB)
Conditions (CDL):
Equal(MeasureOfAngle(ADC),90)
Equal(MeasureOfAngle(CAD),30)
PerpendicularBetweenLine(BC,AC)
Goal: Value(Div(PerimeterOfTriangle(CDB),PerimeterOfTriangle(ABC)))
Answer: 1/2
Theorem sequence:
sine_theorem(1,BCA)
adjacent_complementary_angle(1,ADC,CDB)
mirror_similar_triangle_judgment_aa(1,CDB,ABC)
mirror_similar_triangle_property_line_ratio(1,DBC,CAB)
mirror_similar_triangle_property_perimeter_ratio(1,CDB,ABC)
Problem: As shown in the diagram, the area of △CNM is 1, M is the midpoint of segment CA, N is the midpoint of segment CB. Find the area of triangle CBA.
问题：如图所示，三角形CNM的面积为1，M平分线段CA，N是线段CB的中点。求三角形CBA的面积。
Construction (CDL):
Shape(CN,NM,MC)
Shape(NB,BA,AM,MN)
Collinear(CMA)
Collinear(CNB)
Conditions (CDL):
Equal(AreaOfTriangle(CNM),1)
IsMidpointOfLine(M,CA)
IsMidpointOfLine(N,CB)
Goal: Value(AreaOfTriangle(CBA))
Answer: 4
Theorem sequence:
line_addition(1,CM,MA)
line_addition(1,CN,NB)
similar_triangle_judgment_sas(1,CNM,CBA)
similar_triangle_property_line_ratio(1,NMC,BAC)
similar_triangle_property_area_square_ratio(1,CNM,CBA)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(AC)), ∠ABC=90°, BD⊥AD. Find the ratio of the length of line BD to the length of line AD.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(AC))，∠ABC=90°，BD⊥AD。求直线BD的长度与直线AD的长度之比。
Construction (CDL):
Shape(AB,BD,DA)
Shape(CD,DB,BC)
Collinear(ADC)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(AC)),5/13)
Equal(MeasureOfAngle(ABC),90)
PerpendicularBetweenLine(BD,AD)
Goal: Value(Div(LengthOfLine(BD),LengthOfLine(AD)))
Answer: 5/12
Theorem sequence:
adjacent_complementary_angle(1,CDB,BDA)
mirror_similar_triangle_judgment_aa(1,BDA,CAB)
mirror_similar_triangle_judgment_aa(1,BCD,ABC)
mirror_similar_triangle_property_line_ratio(1,BDA,CAB)
mirror_similar_triangle_property_line_ratio(1,DAB,BCA)
mirror_similar_triangle_property_line_ratio(1,ABD,ABC)
mirror_similar_triangle_property_line_ratio(1,BCD,ABC)
mirror_similar_triangle_property_line_ratio(1,CDB,CAB)
line_addition(1,AD,DC)
Problem: As shown in the diagram, the area of triangle ADC is 1, AC=3, AD=1, ∠DCA=∠DBC. Find the area of △ABC.
问题：如图所示，三角形ADC的面积为1，AC=3，AD=1，∠DCA=∠DBC。求△ABC的面积。
Construction (CDL):
Shape(AD,DC,CA)
Shape(DB,BC,CD)
Collinear(BDA)
Conditions (CDL):
Equal(AreaOfTriangle(ADC),1)
Equal(LengthOfLine(AC),3)
Equal(LengthOfLine(AD),1)
Equal(MeasureOfAngle(DCA),MeasureOfAngle(DBC))
Goal: Value(AreaOfTriangle(ABC))
Answer: 9
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, Div(LengthOfLine(CF)=LengthOfLine(AB)), quadrilateral ADCB is a ▱. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，Div(LengthOfLine(CF)=LengthOfLine(AB))，ADCB是▱。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DF,FB,BA)
Shape(BF,FC,CB)
Shape(FD,DE,EF)
Collinear(CFD)
Collinear(BFE)
Collinear(ADE)
Conditions (CDL):
Equal(Div(LengthOfLine(CF),LengthOfLine(AB)),2/3)
Parallelogram(ADCB)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 1/2
Theorem sequence:
parallelogram_property_opposite_line_equal(1,DCBA)
line_addition(1,CF,FD)
parallel_property_collinear_extend(1,DA,CB,E)
parallel_property_alternate_interior_angle(1,ED,CB)
parallel_property_alternate_interior_angle(2,ED,CB)
similar_triangle_judgment_aa(1,FCB,FDE)
similar_triangle_property_line_ratio(1,FCB,FDE)
similar_triangle_property_line_ratio(1,BFC,EFD)
Problem: As shown in the diagram, AB=BC, BG=BE, ∠EFG=120°, ∠QCD=120°, P is the midpoint of segment DF, DC is parallel to GF, AD and BC are opposite sides of the parallelogram ABCD, EB and FG are opposite sides of the parallelogram BEFG. Find the ratio of the length of line PG to the length of line PC.
问题：如图所示，AB=BC，BG=BE，∠EFG=120°，∠QCD=120°，P是线段DF的中点，DC平行于GF，ABCD是平行四边形，BEFG是▱。求直线PG的长度与直线PC的长度之比。
Construction (CDL):
Shape(DP,PH,HD)
Shape(HP,PC,CH)
Shape(CP,PQ,QC)
Shape(QP,PG,GQ)
Shape(FQ,QG,GF)
Shape(DA,AB,BG,GP,PD)
Shape(GB,BE,EF,FG)
Collinear(DHC)
Collinear(CQGB)
Collinear(ABE)
Collinear(HPG)
Collinear(DPQF)
Conditions (CDL):
Equal(LengthOfLine(AB),LengthOfLine(BC))
Equal(LengthOfLine(BG),LengthOfLine(BE))
Equal(MeasureOfAngle(EFG),120)
Equal(MeasureOfAngle(QCD),120)
IsMidpointOfLine(P,DF)
ParallelBetweenLine(DC,GF)
Parallelogram(ABCD)
Parallelogram(BEFG)
Goal: Value(Div(LengthOfLine(PG),LengthOfLine(PC)))
Answer: sqrt(3)
Theorem sequence:
parallel_property_collinear_extend(3,DC,GF,H)
parallel_property_alternate_interior_angle(2,DH,GF)
vertical_angle(1,DPH,FPG)
triangle_property_angle_sum(1,CPG)
congruent_triangle_judgment_aas(1,DPH,FPG)
congruent_triangle_property_line_equal(1,DPH,FPG)
congruent_triangle_property_line_equal(1,PHD,PGF)
parallelogram_property_opposite_line_equal(1,ABCD)
parallelogram_property_opposite_line_equal(1,BEFG)
line_addition(1,DH,HC)
line_addition(1,CG,GB)
mirror_congruent_triangle_judgment_sss(1,HPC,GCP)
mirror_congruent_triangle_property_angle_equal(1,PCH,PGC)
mirror_congruent_triangle_property_angle_equal(1,CHP,CPG)
adjacent_complementary_angle(1,HPC,CPG)
angle_addition(1,QCP,PCH)
sine_theorem(1,PGC)
Problem: As shown in the diagram, AD=1, BD=2, DE∥BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，AD=1，BD=2，DE∥BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BF,FE,ED)
Shape(EF,FC,CE)
Collinear(ADB)
Collinear(AEC)
Collinear(BFC)
Conditions (CDL):
Equal(LengthOfLine(AD),1)
Equal(LengthOfLine(BD),2)
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)
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, BC=5, CD=4, ∠ACB=90°, BD is perpendicular to CD. Find the length of line AC.
问题：如图所示，BC=5，CD=4，∠ACB=90°，BD⊥CD。求直线AC的长度。
Construction (CDL):
Shape(CB,BD,DC)
Shape(CD,DA,AC)
Collinear(BDA)
Conditions (CDL):
Equal(LengthOfLine(BC),5)
Equal(LengthOfLine(CD),4)
Equal(MeasureOfAngle(ACB),90)
PerpendicularBetweenLine(BD,CD)
Goal: Value(LengthOfLine(AC))
Answer: 20/3
Theorem sequence:
right_triangle_judgment_angle(1,BDC)
right_triangle_property_pythagorean(1,BDC)
adjacent_complementary_angle(1,BDC,CDA)
triangle_property_angle_sum(1,CDA)
triangle_property_angle_sum(1,CBA)
similar_triangle_judgment_aa(1,CBD,ACD)
similar_triangle_property_line_ratio(1,CBD,ACD)
similar_triangle_property_line_ratio(1,DCB,DAC)
Problem: As shown in the diagram, AD=1, BD=2, DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，AD=1，BD=2，DE∥BC。求直线DE的长度与直线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)
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)
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, BP=1, ∠APD=60°, triangle ABC is an equilateral triangle. Find the length of line CD.
问题：如图所示，AB=3，BP=1，∠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),3)
Equal(LengthOfLine(BP),1)
Equal(MeasureOfAngle(APD),60)
EquilateralTriangle(ABC)
Goal: Value(LengthOfLine(CD))
Answer: 2/3
Theorem sequence:
equilateral_triangle_property_angle(1,BCA)
equilateral_triangle_property_angle(1,CAB)
triangle_property_angle_sum(1,ABP)
adjacent_complementary_angle(1,BPA,APC)
angle_addition(1,APD,DPC)
similar_triangle_judgment_aa(1,PAB,DPC)
line_addition(1,BP,PC)
similar_triangle_property_line_ratio(1,PAB,DPC)
similar_triangle_property_line_ratio(1,ABP,PCD)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AC)), Div(LengthOfLine(AE)=LengthOfLine(AB)), AN bisects ∠EAD. Find the ratio of the length of line EN to the length of line BM.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AC))，Div(LengthOfLine(AE)=LengthOfLine(AB))，AN是∠EAD的角平分线。求直线EN的长度与直线BM的长度之比。
Construction (CDL):
Shape(AD,DN,NA)
Shape(AN,NE,EA)
Shape(DB,BM,MN,ND)
Shape(NM,MC,CE,EN)
Collinear(ADB)
Collinear(ANM)
Collinear(AEC)
Collinear(DNE)
Collinear(BMC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AC)),1/2)
Equal(Div(LengthOfLine(AE),LengthOfLine(AB)),1/2)
IsBisectorOfAngle(AN,EAD)
Goal: Value(Div(LengthOfLine(EN),LengthOfLine(BM)))
Answer: 1/2
Theorem sequence:
mirror_similar_triangle_judgment_sas(1,ADE,ABC)
mirror_similar_triangle_property_angle_equal(1,EAD,BCA)
mirror_similar_triangle_judgment_aa(1,NEA,MAB)
mirror_similar_triangle_property_line_ratio(1,NEA,MAB)
mirror_similar_triangle_property_line_ratio(1,ANE,ABM)
Problem: As shown in the diagram, AB=3, BC=5, BF is the angle bisector of ∠ABC, quadrilateral ABCD is a parallelogram. Find the ratio of the length of line AF to the length of line FC.
问题：如图所示，AB=3，BC=5，BF平分∠ABC，BA和CD是平行四边形ABCD的一组对边。求直线AF的长度与直线FC的长度之比。
Construction (CDL):
Shape(AB,BF,FA)
Shape(FB,BC,CF)
Shape(AF,FE,EA)
Shape(DE,EF,FC,CD)
Collinear(AED)
Collinear(AFC)
Collinear(BFE)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BC),5)
IsBisectorOfAngle(BF,ABC)
Parallelogram(ABCD)
Goal: Value(Div(LengthOfLine(AF),LengthOfLine(FC)))
Answer: 3/5
Theorem sequence:
parallel_property_collinear_extend(3,AD,BC,E)
parallel_property_alternate_interior_angle(1,AD,BC)
parallel_property_alternate_interior_angle(2,AE,BC)
isosceles_triangle_judgment_angle_equal(1,ABE)
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, Div(LengthOfLine(BF)=LengthOfLine(FD)), quadrilateral ABCD is a ▱. Find the ratio of the length of line BE to the length of line EC.
问题：如图所示，Div(LengthOfLine(BF)=LengthOfLine(FD))，AD和BC是▱ABCD的一组对边。求直线BE的长度与直线EC的长度之比。
Construction (CDL):
Shape(AB,BF,FA)
Shape(FB,BE,EF)
Shape(AF,FD,DA)
Shape(FE,EC,CD,DF)
Collinear(AFE)
Collinear(BFD)
Collinear(BEC)
Conditions (CDL):
Equal(Div(LengthOfLine(BF),LengthOfLine(FD)),1/3)
Parallelogram(ABCD)
Goal: Value(Div(LengthOfLine(BE),LengthOfLine(EC)))
Answer: 1/2
Theorem sequence:
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)
parallelogram_property_opposite_line_equal(1,BCDA)
line_addition(1,BE,EC)
Problem: As shown in the diagram, AD=4, DB=2, DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，AD=4，DB=2，DE∥BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),4)
Equal(LengthOfLine(DB),2)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 2/3
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(AG)=LengthOfLine(AH)), BC=15, DE=12, GH=4. Find the length of line AH.
问题：如图所示，Div(LengthOfLine(AG)=LengthOfLine(AH))，BC=15，DE=12，GH=4。求直线AH的长度。
Construction (CDL):
Shape(AD,DG,GA)
Shape(AG,GE,EA)
Shape(DB,BH,HG,GD)
Shape(GH,HC,CE,EG)
Collinear(ADB)
Collinear(AGH)
Collinear(AEC)
Collinear(DGE)
Collinear(BHC)
Conditions (CDL):
Equal(Div(LengthOfLine(AG),LengthOfLine(AH)),Div(LengthOfLine(DE),LengthOfLine(BC)))
Equal(LengthOfLine(BC),15)
Equal(LengthOfLine(DE),12)
Equal(LengthOfLine(GH),4)
Goal: Value(LengthOfLine(AH))
Answer: 20
Theorem sequence:
line_addition(1,AG,GH)
Problem: As shown in the diagram, Div(PerimeterOfTriangle(ADE)=PerimeterOfTriangle(ABC)), AD=4, DE∥BC. Find the length of line DB.
问题：如图所示，Div(PerimeterOfTriangle(ADE)=PerimeterOfTriangle(ABC))，AD=4，DE∥BC。求直线DB的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(PerimeterOfTriangle(ADE),PerimeterOfTriangle(ABC)),2/3)
Equal(LengthOfLine(AD),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DB))
Answer: 2
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_perimeter_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
line_addition(1,AD,DB)
Problem: As shown in the diagram, AB=6, BC=8, BE=6, quadrilateral ABCD is a rectangle. Find the length of line CF.
问题：如图所示，AB=6，BC=8，BE=6，ABCD是矩形。求直线CF的长度。
Construction (CDL):
Shape(AB,BE,EA)
Shape(AE,ED,DA)
Shape(DE,EF,FD)
Shape(EB,BC,CF,FE)
Collinear(AEF)
Collinear(BED)
Collinear(DFC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(BC),8)
Equal(LengthOfLine(BE),6)
Rectangle(ABCD)
Goal: Value(LengthOfLine(CF))
Answer: 2
Theorem sequence:
parallelogram_property_opposite_line_equal(1,ABCD)
right_triangle_judgment_angle(1,BCD)
right_triangle_property_pythagorean(1,BCD)
line_addition(1,BE,ED)
parallel_property_collinear_extend(3,DC,AB,F)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(2,DF,AB)
similar_triangle_judgment_aa(1,EAB,EFD)
similar_triangle_property_line_ratio(1,EAB,EFD)
similar_triangle_property_line_ratio(1,ABE,FDE)
line_addition(1,DF,FC)
Problem: As shown in the diagram, Div(LengthOfLine(DE)=LengthOfLine(EA)), EF=6, EF is parallel to AB, ABCD is a ▱. Find the length of line CD.
问题：如图所示，Div(LengthOfLine(DE)=LengthOfLine(EA))，EF=6，EF∥AB，四边形ABCD是▱。求直线CD的长度。
Construction (CDL):
Shape(DE,EF,FD)
Shape(EA,AB,BF,FE)
Shape(DF,FB,BC,CD)
Collinear(DEA)
Collinear(DFB)
Conditions (CDL):
Equal(Div(LengthOfLine(DE),LengthOfLine(EA)),2/3)
Equal(LengthOfLine(EF),6)
ParallelBetweenLine(EF,AB)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(CD))
Answer: 15
Theorem sequence:
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)
line_addition(1,DE,EA)
parallelogram_property_opposite_line_equal(1,ABCD)
Problem: As shown in the diagram, DE=5, ∠ABD=30°, ∠FCE=30°, ∠BDA is the right angle of the right triangle BDA, ∠CEA is the right angle of the right triangle CEA. Find the length of line BC.
问题：如图所示，DE=5，∠ABD=30°，∠FCE=30°，∠BDA是直角△BDA的直角，CE和EA是直角△CEA的两个直角边。求直线BC的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DF,FA)
Shape(AF,FE,EA)
Shape(BC,CF,FD,DB)
Shape(EF,FC,CE)
Collinear(AFC)
Collinear(DFE)
Conditions (CDL):
Equal(LengthOfLine(DE),5)
Equal(MeasureOfAngle(ABD),30)
Equal(MeasureOfAngle(FCE),30)
RightTriangle(BDA)
RightTriangle(CEA)
Goal: Value(LengthOfLine(BC))
Answer: 10
Theorem sequence:
similar_triangle_judgment_aa(1,ABD,ACE)
similar_triangle_property_angle_equal(1,ABD,ACE)
angle_addition(1,FAD,DAB)
angle_addition(1,EAF,FAD)
sine_theorem(1,ABD)
sine_theorem(1,ACE)
similar_triangle_judgment_sas(1,ABC,ADE)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,CAB,EAD)