SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(AC)), DE=2, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AC))，DE=2，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(AC)),1/3)
Equal(LengthOfLine(DE),2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 6
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,ADE,ABC)
Problem: As shown in the diagram, the area of △ABC is 8, DE is the midsegment of △ ABC. Find the area of △ADE.
问题：如图所示，三角形ABC的面积为8，DE是△ABC的中位线。求△ADE的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ABC),8)
IsMidsegmentOfTriangle(DE,ABC)
Goal: Value(AreaOfTriangle(ADE))
Answer: 2
Theorem sequence:
midsegment_of_triangle_property_parallel(1,DE,ABC)
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ADE,ABC)
midsegment_of_triangle_property_length(1,DE,ABC)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_area_square_ratio(1,ADE,ABC)
Problem: As shown in the diagram, ∠CAB=35°, ∠BCA is the right angle of the right △ BCA, △EFD is a right △, triangle ABC is similar to triangle DEF.. Find the measure of ∠DEF.
问题：如图所示，∠CAB=35°，BC和CA是直角三角形BCA的两个直角边，∠EFD是直角三角形EFD的直角，△ABC相似于△DEF。求∠DEF的大小。
Construction (CDL):
Shape(AB,BC,CA)
Shape(DE,EF,FD)
Conditions (CDL):
Equal(MeasureOfAngle(CAB),35)
RightTriangle(BCA)
RightTriangle(EFD)
SimilarBetweenTriangle(ABC,DEF)
Goal: Value(MeasureOfAngle(DEF))
Answer: 55
Theorem sequence:
similar_triangle_property_angle_equal(1,ABC,DEF)
triangle_property_angle_sum(1,DEF)
Problem: As shown in the diagram, the area of triangle ABC is 12, D bisects segment AB, E bisects segment AC. Find the area of △ABC minus the area of triangle ADE.
问题：如图所示，三角形ABC的面积为12，D平分线段AB，E平分线段AC。求三角形ABC的面积减去三角形ADE的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ABC),12)
IsMidpointOfLine(D,AB)
IsMidpointOfLine(E,AC)
Goal: Value(Sub(AreaOfTriangle(ABC),AreaOfTriangle(ADE)))
Answer: 9
Theorem sequence:
midsegment_of_triangle_judgment_midpoint(1,DE,ABC)
midsegment_of_triangle_property_parallel(1,DE,ABC)
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ADE,ABC)
midsegment_of_triangle_property_length(1,DE,ABC)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_area_square_ratio(1,ADE,ABC)
Problem: As shown in the diagram, AB=6, AC=4, AD=3, ∠CAD=∠ABD. Find the length of line BD.
问题：如图所示，AB=6，AC=4，AD=3，∠CAD=∠ABD。求直线BD的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DC,CA)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(AC),4)
Equal(LengthOfLine(AD),3)
Equal(MeasureOfAngle(CAD),MeasureOfAngle(ABD))
Goal: Value(LengthOfLine(BD))
Answer: 6
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DCA,ABC)
mirror_similar_triangle_property_line_ratio(1,CAD,CAB)
mirror_similar_triangle_property_line_ratio(1,DCA,ABC)
mirror_similar_triangle_property_line_ratio(1,ADC,BCA)
line_addition(1,BD,DC)
Problem: As shown in the diagram, AB=4, AD=2, ∠ABD=∠BCD. Find the length of line CD.
问题：如图所示，AB=4，AD=2，∠ABD=∠BCD。求直线CD的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(DB,BC,CD)
Collinear(ADC)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(LengthOfLine(AD),2)
Equal(MeasureOfAngle(ABD),MeasureOfAngle(BCD))
Goal: Value(LengthOfLine(CD))
Answer: 6
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DAB,BCA)
mirror_similar_triangle_property_line_ratio(1,BDA,CAB)
mirror_similar_triangle_property_line_ratio(1,DAB,BCA)
line_addition(1,AD,DC)
Problem: As shown in the diagram, AB=10, AD=6, E is the midpoint of segment AD, Triangle FBC is mirror similar to triangle ECD., BA and CD are opposite sides of the parallelogram ABCD. Find the length of line BF.
问题：如图所示，AB=10，AD=6，E平分线段AD，△FBC与△ECD是镜像相似三角形，四边形ABCD是平行四边形。求直线BF的长度。
Construction (CDL):
Shape(AF,FC,CE,EA)
Shape(FB,BC,CF)
Shape(EC,CD,DE)
Collinear(AED)
Collinear(AFB)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(LengthOfLine(AD),6)
IsMidpointOfLine(E,AD)
MirrorSimilarBetweenTriangle(FBC,ECD)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(BF))
Answer: 9/5
Theorem sequence:
parallelogram_property_opposite_line_equal(1,ABCD)
parallelogram_property_opposite_line_equal(1,DABC)
line_addition(1,AE,ED)
mirror_similar_triangle_property_line_ratio(1,FBC,ECD)
mirror_similar_triangle_property_line_ratio(1,CFB,CDE)
Problem: As shown in the diagram, AC=3, BC=sqrt(6), △ABC is mirror similar to △BCD.. Find the length of line CD.
问题：如图所示，AC=3，BC=sqrt(6)，三角形ABC镜像相似于三角形BCD。求直线CD的长度。
Construction (CDL):
Shape(CD,DB,BC)
Shape(DA,AB,BD)
Collinear(CDA)
Conditions (CDL):
Equal(LengthOfLine(AC),3)
Equal(LengthOfLine(BC),sqrt(6))
MirrorSimilarBetweenTriangle(ABC,BCD)
Goal: Value(LengthOfLine(CD))
Answer: 2
Theorem sequence:
mirror_similar_triangle_property_line_ratio(1,BCA,DBC)
mirror_similar_triangle_property_line_ratio(1,ABC,BCD)
Problem: As shown in the diagram, ∠CAD=60°, ∠DCA=40°, △ABC is mirror similar to △ADC.. Find the measure of ∠BCD.
问题：如图所示，∠CAD=60°，∠DCA=40°，△ABC镜像相似于△ADC。求∠BCD的大小。
Construction (CDL):
Shape(AD,DC,CA)
Shape(DB,BC,CD)
Collinear(ADB)
Conditions (CDL):
Equal(MeasureOfAngle(CAD),60)
Equal(MeasureOfAngle(DCA),40)
MirrorSimilarBetweenTriangle(ABC,ADC)
Goal: Value(MeasureOfAngle(BCD))
Answer: 40
Theorem sequence:
triangle_property_angle_sum(1,ADC)
mirror_similar_triangle_property_angle_equal(1,CAB,DCA)
angle_addition(1,BCD,DCA)
Problem: As shown in the diagram, AD=5, AE=3, BD=10, DE∥BC. Find the length of line AC.
问题：如图所示，AD=5，AE=3，BD=10，DE∥BC。求直线AC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),5)
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(BD),10)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AC))
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)
line_addition(1,AD,DB)
similar_triangle_property_line_ratio(1,EAD,CAB)
similar_triangle_property_line_ratio(1,DEA,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), Div(LengthOfLine(AD)=LengthOfLine(DB)). Find the ratio of the length of line AB to the length of line DB.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，Div(LengthOfLine(AD)=LengthOfLine(DB))。求直线AB的长度与直线DB的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),2)
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),Div(LengthOfLine(AE),LengthOfLine(EC)))
Goal: Value(Div(LengthOfLine(AB),LengthOfLine(DB)))
Answer: 3
Theorem sequence:
line_addition(1,AD,DB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE is parallel to BC. Find the ratio of the length of line AE to the length of line AC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，DE∥BC。求直线AE的长度与直线AC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),1/3)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(AE),LengthOfLine(AC)))
Answer: 1/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,EAD,CAB)
similar_triangle_property_line_ratio(1,DEA,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(OE)=LengthOfLine(EG)), OF=12, EF is parallel to GH. Find the length of line OH.
问题：如图所示，Div(LengthOfLine(OE)=LengthOfLine(EG))，OF=12，EF平行于GH。求直线OH的长度。
Construction (CDL):
Shape(OE,EF,FO)
Shape(EG,GH,HF,FE)
Collinear(OEG)
Collinear(OFH)
Conditions (CDL):
Equal(Div(LengthOfLine(OE),LengthOfLine(EG)),4/9)
Equal(LengthOfLine(OF),12)
ParallelBetweenLine(EF,GH)
Goal: Value(LengthOfLine(OH))
Answer: 39
Theorem sequence:
parallel_property_corresponding_angle(1,EF,GH,O)
similar_triangle_judgment_aa(1,FOE,HOG)
line_addition(1,OE,EG)
similar_triangle_property_line_ratio(1,FOE,HOG)
similar_triangle_property_line_ratio(1,EFO,GHO)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(BE)), AC is parallel to DB. Find the ratio of the length of line CE to the length of line CD.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(BE))，AC∥DB。求直线CE的长度与直线CD的长度之比。
Construction (CDL):
Shape(AE,EC,CA)
Shape(ED,DB,BE)
Collinear(AEB)
Collinear(CED)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(BE)),1/2)
ParallelBetweenLine(AC,DB)
Goal: Value(Div(LengthOfLine(CE),LengthOfLine(CD)))
Answer: 1/3
Theorem sequence:
parallel_property_alternate_interior_angle(1,AC,DB)
parallel_property_alternate_interior_angle(2,AC,DB)
similar_triangle_judgment_aa(1,ECA,EDB)
similar_triangle_property_line_ratio(1,CAE,DBE)
similar_triangle_property_line_ratio(1,AEC,BED)
line_addition(1,CE,ED)
Problem: As shown in the diagram, AD=4, AE=3, CE=6, DE is parallel to BC. Find the length of line BD.
问题：如图所示，AD=4，AE=3，CE=6，DE∥BC。求直线BD的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),4)
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(CE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BD))
Answer: 8
Theorem sequence:
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,EAD,CAB)
line_addition(1,AE,EC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
line_addition(1,BD,DA)
Problem: As shown in the diagram, AE=3, EC=5, AD is the angle bisector of ∠EAB, BA∥DE. Find the ratio of the length of line AC to the length of line AB.
问题：如图所示，AE=3，EC=5，AD平分∠EAB，BA∥DE。求直线AC的长度与直线AB的长度之比。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DE,EA)
Shape(ED,DC,CE)
Collinear(AEC)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(EC),5)
IsBisectorOfAngle(AD,EAB)
ParallelBetweenLine(BA,DE)
Goal: Value(Div(LengthOfLine(AC),LengthOfLine(AB)))
Answer: 5/3
Theorem sequence:
parallel_property_corresponding_angle(2,BA,DE,C)
similar_triangle_judgment_aa(1,EDC,ABC)
line_addition(1,AE,EC)
similar_triangle_property_line_ratio(1,DCE,BCA)
similar_triangle_property_line_ratio(1,EDC,ABC)
line_addition(1,BD,DC)
bisector_of_angle_judgment_angle_equal(1,AD,CAB)
bisector_of_angle_property_line_ratio(1,AD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), AE=6, DE is parallel to BC. Find the length of line AC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，AE=6，DE平行于BC。求直线AC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),3)
Equal(LengthOfLine(AE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AC))
Answer: 8
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)
line_addition(1,AD,DB)
Problem: As shown in the diagram, AB=3, BC=6, DF=6, AD is parallel to BE, AD is parallel to CF, BE is parallel to CF, ABED is similar to BCFE. Find the length of line DE.
问题：如图所示，AB=3，BC=6，DF=6，AD平行于BE，AD平行于CF，BE平行于CF，四边形ABED与四边形BCFE相似。求直线DE的长度。
Construction (CDL):
Shape(AB,BE,ED,DA)
Shape(BC,CF,FE,EB)
Collinear(ABC)
Collinear(DEF)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BC),6)
Equal(LengthOfLine(DF),6)
ParallelBetweenLine(AD,BE)
ParallelBetweenLine(AD,CF)
ParallelBetweenLine(BE,CF)
SimilarBetweenQuadrilateral(ABED,BCFE)
Goal: Value(LengthOfLine(DE))
Answer: 2
Theorem sequence:
line_addition(1,DE,EF)
similar_quadrilateral_property_line_ratio(1,ABED,BCFE)
similar_quadrilateral_property_line_ratio(1,EDAB,FEBC)
Problem: As shown in the diagram, AO=3, BO=6, CO=2, DC∥AB. Find the length of line BD.
问题：如图所示，AO=3，BO=6，CO=2，DC平行于AB。求直线BD的长度。
Construction (CDL):
Shape(DO,OC,CD)
Shape(OA,AB,BO)
Collinear(DOB)
Collinear(AOC)
Conditions (CDL):
Equal(LengthOfLine(AO),3)
Equal(LengthOfLine(BO),6)
Equal(LengthOfLine(CO),2)
ParallelBetweenLine(DC,AB)
Goal: Value(LengthOfLine(BD))
Answer: 10
Theorem sequence:
line_addition(1,DO,OB)
parallel_property_alternate_interior_angle(1,DC,AB)
parallel_property_alternate_interior_angle(2,DC,AB)
similar_triangle_judgment_aa(1,OCD,OAB)
similar_triangle_property_line_ratio(1,CDO,ABO)
similar_triangle_property_line_ratio(1,DOC,BOA)
Problem: As shown in the diagram, AB=2, BC=4, DE=3, AD∥BE, AD is parallel to CF, BE is parallel to CF, ABED is similar to BCFE. Find the length of line EF.
问题：如图所示，AB=2，BC=4，DE=3，AD∥BE，AD平行于CF，BE平行于CF，ABED与BCFE相似。求直线EF的长度。
Construction (CDL):
Shape(AB,BE,ED,DA)
Shape(BC,CF,FE,EB)
Collinear(ABC)
Collinear(DEF)
Conditions (CDL):
Equal(LengthOfLine(AB),2)
Equal(LengthOfLine(BC),4)
Equal(LengthOfLine(DE),3)
ParallelBetweenLine(AD,BE)
ParallelBetweenLine(AD,CF)
ParallelBetweenLine(BE,CF)
SimilarBetweenQuadrilateral(ABED,BCFE)
Goal: Value(LengthOfLine(EF))
Answer: 6
Theorem sequence:
similar_quadrilateral_property_line_ratio(1,ABED,BCFE)
similar_quadrilateral_property_line_ratio(1,EDAB,FEBC)
Problem: As shown in the diagram, AD=5, AE=3, BD=10, DE∥BC. Find the length of line CE.
问题：如图所示，AD=5，AE=3，BD=10，DE平行于BC。求直线CE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),5)
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(BD),10)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(CE))
Answer: 6
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)
line_addition(1,AD,DB)
line_addition(1,AE,EC)
Problem: As shown in the diagram, BC=1, DE=3/2, EF=1, AD is parallel to BE, AD is parallel to CF, BE is parallel to CF, quadrilateral ABED is similar to quadrilateral BCFE. Find the length of line AB.
问题：如图所示，BC=1，DE=3/2，EF=1，AD∥BE，AD∥CF，BE∥CF，ABED与BCFE相似。求直线AB的长度。
Construction (CDL):
Shape(AB,BE,ED,DA)
Shape(BC,CF,FE,EB)
Collinear(ABC)
Collinear(DEF)
Conditions (CDL):
Equal(LengthOfLine(BC),1)
Equal(LengthOfLine(DE),3/2)
Equal(LengthOfLine(EF),1)
ParallelBetweenLine(AD,BE)
ParallelBetweenLine(AD,CF)
ParallelBetweenLine(BE,CF)
SimilarBetweenQuadrilateral(ABED,BCFE)
Goal: Value(LengthOfLine(AB))
Answer: 3/2
Theorem sequence:
similar_quadrilateral_property_line_ratio(1,ABED,BCFE)
similar_quadrilateral_property_line_ratio(1,EDAB,FEBC)
Problem: As shown in the diagram, Div(LengthOfLine(DB)=LengthOfLine(AD)), CF=6, DE∥BC, EF is parallel to AB. Find the length of line BF.
问题：如图所示，Div(LengthOfLine(DB)=LengthOfLine(AD))，CF=6，DE∥BC，EF∥AB。求直线BF的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BF,FE,ED)
Shape(EF,FC,CE)
Collinear(AEC)
Collinear(BFC)
Collinear(ADB)
Conditions (CDL):
Equal(Div(LengthOfLine(DB),LengthOfLine(AD)),2)
Equal(LengthOfLine(CF),6)
ParallelBetweenLine(DE,BC)
ParallelBetweenLine(EF,AB)
Goal: Value(LengthOfLine(BF))
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)
parallel_property_collinear_extend(3,CB,ED,F)
parallel_property_collinear_extend(3,BA,FE,D)
parallelogram_judgment_parallel_and_parallel(1,DBFE)
parallelogram_property_opposite_line_equal(1,BFED)
line_addition(1,BF,FC)
line_addition(1,AD,DB)
Problem: As shown in the diagram, Div(LengthOfLine(BE)=LengthOfLine(AE)), CD=16, CB is parallel to AD. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(BE)=LengthOfLine(AE))，CD=16，CB平行于AD。求直线DE的长度。
Construction (CDL):
Shape(CE,EB,BC)
Shape(EA,AD,DE)
Collinear(CED)
Collinear(AEB)
Conditions (CDL):
Equal(Div(LengthOfLine(BE),LengthOfLine(AE)),3/5)
Equal(LengthOfLine(CD),16)
ParallelBetweenLine(CB,AD)
Goal: Value(LengthOfLine(DE))
Answer: 10
Theorem sequence:
parallel_property_alternate_interior_angle(1,CB,AD)
parallel_property_alternate_interior_angle(2,CB,AD)
similar_triangle_judgment_aa(1,EAD,EBC)
line_addition(1,CE,ED)
similar_triangle_property_line_ratio(1,ADE,BCE)
similar_triangle_property_line_ratio(1,DEA,CEB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AE)), AD is the median of △ ABC, HD∥FB. Find the ratio of the length of line AF to the length of line AC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AE))，AD是三角形ABC的中线，HD平行于FB。求直线AF的长度与直线AC的长度之比。
Construction (CDL):
Shape(AB,BE,EA)
Shape(AE,EF,FA)
Shape(EB,BD,DE)
Shape(FE,ED,DH,HF)
Shape(HD,DC,CH)
Collinear(AED)
Collinear(BEF)
Collinear(AFHC)
Collinear(BDC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AE)),4)
IsMedianOfTriangle(AD,ABC)
ParallelBetweenLine(HD,FB)
Goal: Value(Div(LengthOfLine(AF),LengthOfLine(AC)))
Answer: 1/7
Theorem sequence:
midsegment_of_triangle_judgment_parallel(2,HD,CFB)
parallel_property_collinear_extend(3,BF,DH,E)
parallel_property_corresponding_angle(1,EF,DH,A)
parallel_property_corresponding_angle(2,HD,FB,A)
similar_triangle_judgment_aa(1,ADH,AEF)
similar_triangle_property_line_ratio(1,DHA,EFA)
similar_triangle_property_line_ratio(1,HAD,FAE)
line_addition(1,AF,FH)
line_addition(1,AH,HC)
Problem: As shown in the diagram, AB=8, BC=2, M bisects segment AC. Find the length of line AM.
问题：如图所示，AB=8，BC=2，M平分线段AC。求直线AM的长度。
Construction (CDL):
Shape(AM,MC,CB)
Collinear(AMCB)
Conditions (CDL):
Equal(LengthOfLine(AB),8)
Equal(LengthOfLine(BC),2)
IsMidpointOfLine(M,AC)
Goal: Value(LengthOfLine(AM))
Answer: 3
Theorem sequence:
line_addition(1,AM,MC)
line_addition(1,AC,CB)
Problem: As shown in the diagram, ∠AOB=15°, ∠AOC=90°. Find the measure of ∠COD.
问题：如图所示，∠AOB=15°，∠AOC=90°。求∠COD的大小。
Construction (CDL):
Shape(AO,OB)
Shape(BO,OC)
Shape(CO,OD)
Shape(DO,OA)
Collinear(BOD)
Conditions (CDL):
Equal(MeasureOfAngle(AOB),15)
Equal(MeasureOfAngle(AOC),90)
Goal: Value(MeasureOfAngle(COD))
Answer: 105
Theorem sequence:
adjacent_complementary_angle(1,BOC,COD)
angle_addition(1,AOB,BOC)
Problem: As shown in the diagram, ∠ABC=100°, ∠CAB=50°, AC is parallel to BE, BC∥DE. Find the measure of ∠CBE.
问题：如图所示，∠ABC=100°，∠CAB=50°，AC平行于BE，BC∥DE。求∠CBE的大小。
Construction (CDL):
Shape(AB,BC,CA)
Shape(CB,BE)
Shape(EB,BD,DE)
Collinear(ABD)
Conditions (CDL):
Equal(MeasureOfAngle(ABC),100)
Equal(MeasureOfAngle(CAB),50)
ParallelBetweenLine(AC,BE)
ParallelBetweenLine(BC,DE)
Goal: Value(MeasureOfAngle(CBE))
Answer: 30
Theorem sequence:
parallel_property_ipsilateral_internal_angle(1,AC,BE)
angle_addition(1,ABC,CBE)
Problem: As shown in the diagram, AB=20, AD=14, D is the midpoint of segment CB. Find the length of line AC.
问题：如图所示，AB=20，AD=14，D平分线段CB。求直线AC的长度。
Construction (CDL):
Shape(AC,CD,DB)
Collinear(ACDB)
Conditions (CDL):
Equal(LengthOfLine(AB),20)
Equal(LengthOfLine(AD),14)
IsMidpointOfLine(D,CB)
Goal: Value(LengthOfLine(AC))
Answer: 8
Theorem sequence:
line_addition(1,AC,CD)
line_addition(1,AD,DB)
Problem: As shown in the diagram, Div(LengthOfLine(CB)=LengthOfLine(AC)), AC=12, D is the midpoint of segment AC, E is the midpoint of segment AB. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(CB)=LengthOfLine(AC))，AC=12，D平分线段AC，E是线段AB的中点。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EC,CB)
Collinear(ADECB)
Conditions (CDL):
Equal(Div(LengthOfLine(CB),LengthOfLine(AC)),2/3)
Equal(LengthOfLine(AC),12)
IsMidpointOfLine(D,AC)
IsMidpointOfLine(E,AB)
Goal: Value(LengthOfLine(DE))
Answer: 4
Theorem sequence:
line_addition(1,AD,DE)
line_addition(1,AD,DC)
line_addition(1,AE,EB)
line_addition(1,AC,CB)
Problem: As shown in the diagram, CB=4, DB=7, D is the midpoint of segment AC. Find the length of line AC.
问题：如图所示，CB=4，DB=7，D是线段AC的中点。求直线AC的长度。
Construction (CDL):
Shape(AD,DC,CB)
Collinear(ADCB)
Conditions (CDL):
Equal(LengthOfLine(CB),4)
Equal(LengthOfLine(DB),7)
IsMidpointOfLine(D,AC)
Goal: Value(LengthOfLine(AC))
Answer: 6
Theorem sequence:
line_addition(1,AD,DC)
line_addition(1,DC,CB)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(AB)), CD=3, D bisects segment AC. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(AB))，CD=3，D平分线段AC。求直线AB的长度。
Construction (CDL):
Shape(AD,DB,BC)
Collinear(ADBC)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(AB)),1/2)
Equal(LengthOfLine(CD),3)
IsMidpointOfLine(D,AC)
Goal: Value(LengthOfLine(AB))
Answer: 4
Theorem sequence:
line_addition(1,AD,DC)
line_addition(1,AB,BC)
Problem: As shown in the diagram, ∠DAM=110°, ∠MBN=85°, △BNM is mirror congruent to △FMN, AD∥MF, DC∥FN. Find the measure of ∠NCD.
问题：如图所示，∠DAM=110°，∠MBN=85°，三角形BNM与三角形FMN是镜像全等三角形，AD平行于MF，DC平行于FN。求∠NCD的大小。
Construction (CDL):
Shape(DA,AM,MF,FN,NC,CD)
Shape(NF,FM,MN)
Shape(NM,MB,BN)
Collinear(CNB)
Collinear(AMB)
Conditions (CDL):
Equal(MeasureOfAngle(DAM),110)
Equal(MeasureOfAngle(MBN),85)
MirrorCongruentBetweenTriangle(BNM,FMN)
ParallelBetweenLine(AD,MF)
ParallelBetweenLine(DC,FN)
Goal: Value(MeasureOfAngle(NCD))
Answer: 80
Theorem sequence:
parallel_property_corresponding_angle(1,NF,CD,B)
parallel_property_corresponding_angle(2,AD,MF,B)
angle_addition(1,FMN,NMB)
angle_addition(1,BNM,MNF)
mirror_congruent_triangle_property_angle_equal(1,BNM,FMN)
triangle_property_angle_sum(1,NFM)
triangle_property_angle_sum(1,NMB)
Problem: As shown in the diagram, AB=10, CD=3, M is the midpoint of segment AC, N is the midpoint of segment DB. Find the length of line MN.
问题：如图所示，AB=10，CD=3，M是线段AC的中点，N是线段DB的中点。求直线MN的长度。
Construction (CDL):
Collinear(AMCDNB)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(LengthOfLine(CD),3)
IsMidpointOfLine(M,AC)
IsMidpointOfLine(N,DB)
Goal: Value(LengthOfLine(MN))
Answer: 13/2
Theorem sequence:
line_addition(1,AM,MC)
line_addition(1,AM,MN)
line_addition(1,AC,CD)
line_addition(1,AD,DN)
line_addition(1,AN,NB)
Problem: As shown in the diagram, ∠BAE=50°, ∠ECD=30°, AB∥CD. Find the measure of ∠CEA.
问题：如图所示，∠BAE=50°，∠ECD=30°，AB平行于CD。求∠CEA的大小。
Construction (CDL):
Shape(AE,EB,BA)
Shape(CE,EA)
Shape(EC,CD)
Collinear(CEB)
Conditions (CDL):
Equal(MeasureOfAngle(BAE),50)
Equal(MeasureOfAngle(ECD),30)
ParallelBetweenLine(AB,CD)
Goal: Value(MeasureOfAngle(CEA))
Answer: 80
Theorem sequence:
parallel_property_alternate_interior_angle(2,AB,CD)
triangle_property_angle_sum(1,AEB)
adjacent_complementary_angle(1,CEA,AEB)
Problem: As shown in the diagram, Sub(PerimeterOfTriangle(ABD)=PerimeterOfTriangle(ADC)), AD is the median of triangle ABC. Find the length of line AB minus the length of line AC.
问题：如图所示，Sub(PerimeterOfTriangle(ABD)=PerimeterOfTriangle(ADC))，AD是△ABC的中线。求直线AB的长度减去直线AC的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DC,CA)
Collinear(BDC)
Conditions (CDL):
Equal(Sub(PerimeterOfTriangle(ABD),PerimeterOfTriangle(ADC)),3)
IsMedianOfTriangle(AD,ABC)
Goal: Value(Sub(LengthOfLine(AB),LengthOfLine(AC)))
Answer: 3
Theorem sequence:
triangle_perimeter_formula(1,ABD)
triangle_perimeter_formula(1,ADC)
Problem: As shown in the diagram, AB=6, BC=4, M bisects segment AB, N bisects segment BC. Find the length of line MN.
问题：如图所示，AB=6，BC=4，M平分线段AB，N平分线段BC。求直线MN的长度。
Construction (CDL):
Shape(AM,MB,BN,NC)
Collinear(AMBNC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(BC),4)
IsMidpointOfLine(M,AB)
IsMidpointOfLine(N,BC)
Goal: Value(LengthOfLine(MN))
Answer: 5
Theorem sequence:
line_addition(1,AM,MB)
line_addition(1,AM,MN)
line_addition(1,AB,BN)
line_addition(1,AB,BC)
line_addition(1,AN,NC)