SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, BC=CD, BD=4, ED=1, ∠ABC=90°, ∠ACE=90°, ∠CDE=90°. Find the length of line AB.
问题：如图所示，BC=CD，BD=4，ED=1，∠ABC=90°，∠ACE=90°，∠CDE=90°。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(EC,CD,DE)
Collinear(BCD)
Conditions (CDL):
Equal(LengthOfLine(BC),LengthOfLine(CD))
Equal(LengthOfLine(BD),4)
Equal(LengthOfLine(ED),1)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(ACE),90)
Equal(MeasureOfAngle(CDE),90)
Goal: Value(LengthOfLine(AB))
Answer: 4
Theorem sequence:
line_addition(1,BC,CD)
angle_addition(1,BCA,ACE)
adjacent_complementary_angle(1,BCE,ECD)
triangle_property_angle_sum(1,CDE)
similar_triangle_judgment_aa(1,ABC,CDE)
similar_triangle_property_line_ratio(1,ABC,CDE)
similar_triangle_property_line_ratio(1,CAB,ECD)
Problem: As shown in the diagram, AD=4, DB=2, DE∥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, AB=10, AE=8, DE=6, ∠DEA=∠ABC. Find the length of line BC.
问题：如图所示，AB=10，AE=8，DE=6，∠DEA=∠ABC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(LengthOfLine(AE),8)
Equal(LengthOfLine(DE),6)
Equal(MeasureOfAngle(DEA),MeasureOfAngle(ABC))
Goal: Value(LengthOfLine(BC))
Answer: 15/2
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DEA,CAB)
mirror_similar_triangle_property_line_ratio(1,DEA,CAB)
mirror_similar_triangle_property_line_ratio(1,ADE,ABC)
Problem: As shown in the diagram, Div(LengthOfLine(DE)=LengthOfLine(EA)), EF=4, EF∥AB, BA and CD are opposite sides of the parallelogram ABCD. Find the length of line CD.
问题：如图所示，Div(LengthOfLine(DE)=LengthOfLine(EA))，EF=4，EF∥AB，四边形ABCD是平行四边形。求直线CD的长度。
Construction (CDL):
Shape(DE,EF,FD)
Shape(EA,AB,BF,FE)
Shape(DF,FB,BC,CD)
Collinear(DFB)
Collinear(DEA)
Conditions (CDL):
Equal(Div(LengthOfLine(DE),LengthOfLine(EA)),2/3)
Equal(LengthOfLine(EF),4)
ParallelBetweenLine(EF,AB)
Parallelogram(ABCD)
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(CE)=LengthOfLine(BC)), AB=6, AB is the diameter of circle O. Find the length of line EF.
问题：如图所示，Div(LengthOfLine(CE)=LengthOfLine(BC))，AB=6，圆O的直径为AB。求直线EF的长度。
Construction (CDL):
Shape(AE,OEA)
Shape(AM,ME,EA)
Shape(MA,OAF,FM)
Shape(MF,FB,BM)
Shape(BF,OFB)
Shape(EB,OBE)
Shape(EM,MB,BE)
Shape(BC,CE,OBE)
Collinear(AEC)
Collinear(AOMB)
Collinear(EMF)
Collinear(CBF)
Cocircular(O,AFBE)
Conditions (CDL):
Equal(Div(LengthOfLine(CE),LengthOfLine(BC)),2/3)
Equal(LengthOfLine(AB),6)
IsDiameterOfCircle(AB,O)
Goal: Value(LengthOfLine(EF))
Answer: 4
Theorem sequence:
arc_property_circumference_angle_external(1,OBE,A)
arc_property_circumference_angle_external(1,OBE,F)
mirror_similar_triangle_judgment_aa(1,EFC,BCA)
mirror_similar_triangle_property_line_ratio(1,FCE,ABC)
mirror_similar_triangle_property_line_ratio(1,CEF,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(EO)=LengthOfLine(OC)), AE=3, ED is parallel to BC. Find the length of line EB.
问题：如图所示，Div(LengthOfLine(EO)=LengthOfLine(OC))，AE=3，ED∥BC。求直线EB的长度。
Construction (CDL):
Shape(AE,ED,DA)
Shape(EO,OD,DE)
Shape(OE,EB,BO)
Shape(OB,BC,CO)
Shape(DO,OC,CD)
Collinear(AEB)
Collinear(ADC)
Collinear(EOC)
Collinear(DOB)
Conditions (CDL):
Equal(Div(LengthOfLine(EO),LengthOfLine(OC)),1/3)
Equal(LengthOfLine(AE),3)
ParallelBetweenLine(ED,BC)
Goal: Value(LengthOfLine(EB))
Answer: 6
Theorem sequence:
parallel_property_alternate_interior_angle(1,ED,BC)
parallel_property_alternate_interior_angle(2,ED,BC)
similar_triangle_judgment_aa(1,ODE,OBC)
similar_triangle_property_line_ratio(1,ODE,OBC)
similar_triangle_property_line_ratio(1,DEO,BCO)
parallel_property_corresponding_angle(1,ED,BC,A)
parallel_property_corresponding_angle(2,CB,DE,A)
similar_triangle_judgment_aa(1,AED,ABC)
similar_triangle_property_line_ratio(1,AED,ABC)
similar_triangle_property_line_ratio(1,DAE,CAB)
line_addition(1,AE,EB)
Problem: As shown in the diagram, AB=12, AE=4, AE=EC, BC=10, ∠DEA=∠ABC. Find the ratio of the perimeter of △ADE to the perimeter of triangle ABC.
问题：如图所示，AB=12，AE=4，AE=EC，BC=10，∠DEA=∠ABC。求△ADE的周长与三角形ABC的周长之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(LengthOfLine(AE),4)
Equal(LengthOfLine(AE),LengthOfLine(EC))
Equal(LengthOfLine(BC),10)
Equal(MeasureOfAngle(DEA),MeasureOfAngle(ABC))
Goal: Value(Div(PerimeterOfTriangle(ADE),PerimeterOfTriangle(ABC)))
Answer: 1/3
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,CAB,DEA)
mirror_similar_triangle_property_line_ratio(1,CAB,DEA)
mirror_similar_triangle_property_perimeter_ratio(1,CAB,DEA)
Problem: As shown in the diagram, AD=3, CB=CF, DF=4, ∠ADF=90°. Find the sum of the length of line AC and the length of line BC.
问题：如图所示，AD=3，CB=CF，DF=4，∠ADF=90°。求直线AC的长度与直线BC的长度之和。
Construction (CDL):
Shape(AD,DB,BC,CA)
Shape(CB,BF,FC)
Collinear(ACF)
Collinear(DBF)
Conditions (CDL):
Equal(LengthOfLine(AD),3)
Equal(LengthOfLine(CB),LengthOfLine(CF))
Equal(LengthOfLine(DF),4)
Equal(MeasureOfAngle(ADF),90)
Goal: Value(Add(LengthOfLine(AC),LengthOfLine(BC)))
Answer: 5
Theorem sequence:
line_addition(1,AC,CF)
right_triangle_judgment_angle(1,ADF)
right_triangle_property_pythagorean(1,ADF)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE=4, DE∥BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，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(AD),LengthOfLine(AB)),1/3)
Equal(LengthOfLine(DE),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 12
Theorem sequence:
parallel_property_corresponding_angle(1,DE,BC,A)
parallel_property_corresponding_angle(2,CB,ED,A)
similar_triangle_judgment_aa(1,ADE,ABC)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AD=2, DB=3, DE=1, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AD=2，DB=3，DE=1，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(DB),3)
Equal(LengthOfLine(DE),1)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 5/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, CD=2, GC=6, GT is the median of △ GDP, ABCD is a square, GCEF is a square. Find the length of line GT.
问题：如图所示，CD=2，GC=6，GT是三角形GDP的中线，ABCD是正方形，四边形GCEF是正方形。求直线GT的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(DB,BC,CD)
Shape(GD,DT,TG)
Shape(TD,DC,CE,ET)
Shape(GT,TP,PG)
Shape(PT,TE,EF,FP)
Collinear(GPF)
Collinear(GDC)
Collinear(BCE)
Collinear(BDTP)
Collinear(GTE)
Conditions (CDL):
Equal(LengthOfLine(CD),2)
Equal(LengthOfLine(GC),6)
IsMedianOfTriangle(GT,GDP)
Square(ABCD)
Square(GCEF)
Goal: Value(LengthOfLine(GT))
Answer: 2*sqrt(2)
Theorem sequence:
right_triangle_judgment_angle(1,PGD)
line_addition(1,GD,DC)
isosceles_triangle_judgment_line_equal(1,CDB)
isosceles_triangle_property_angle_equal(1,CDB)
triangle_property_angle_sum(1,DBC)
triangle_property_angle_sum(1,GDP)
vertical_angle(1,GDT,CDB)
isosceles_triangle_judgment_angle_equal(1,GDP)
right_triangle_property_pythagorean(1,PGD)
right_triangle_property_length_of_median(1,PGD,T)
Problem: As shown in the diagram, AB=BD, AC=6, EC=1, O is the center of ⊙O, the diameter of circle O is AC, OB∥DC. Find the length of line AD.
问题：如图所示，AB=BD，AC=6，EC=1，⊙O的圆心为O，AC是圆O的直径，OB平行于DC。求直线AD的长度。
Construction (CDL):
Shape(AB,OBA)
Shape(DA,OAD)
Shape(CD,ODC)
Shape(BC,OCB)
Shape(AD,DE,EA)
Shape(ED,DC,CE)
Shape(BA,AO,OB)
Shape(BO,OE,EB)
Shape(BE,EC,CB)
Collinear(AOEC)
Collinear(BED)
Cocircular(O,ADCB)
Conditions (CDL):
Equal(LengthOfLine(AB),LengthOfLine(BD))
Equal(LengthOfLine(AC),6)
Equal(LengthOfLine(EC),1)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AC,O)
ParallelBetweenLine(OB,DC)
Goal: Value(LengthOfLine(AD))
Answer: 3*sqrt(15)/2
Theorem sequence:
diameter_of_circle_property_length_equal(1,AC,O)
circle_property_length_of_radius_and_diameter(1,O)
radius_of_circle_property_length_equal(1,OC,O)
radius_of_circle_property_length_equal(1,OB,O)
line_addition(1,OE,EC)
parallel_property_alternate_interior_angle(1,OB,DC)
parallel_property_alternate_interior_angle(2,OB,DC)
similar_triangle_judgment_aa(1,EDC,EBO)
similar_triangle_property_line_ratio(1,EDC,EBO)
similar_triangle_property_line_ratio(1,DCE,BOE)
diameter_of_circle_property_right_angle(1,ADC,O)
right_triangle_judgment_angle(1,ADC)
right_triangle_property_pythagorean(1,ADC)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE=4, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，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(AD),LengthOfLine(AB)),1/2)
Equal(LengthOfLine(DE),4)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
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,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, the area of △ABC is 36, AD=BD, AE=EC. Find the area of triangle ADE.
问题：如图所示，△ABC的面积为36，AD=BD，AE=EC。求三角形ADE的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ABC),36)
Equal(LengthOfLine(AD),LengthOfLine(BD))
Equal(LengthOfLine(AE),LengthOfLine(EC))
Goal: Value(AreaOfTriangle(ADE))
Answer: 9
Theorem sequence:
midsegment_of_triangle_judgment_midpoint(1,DE,ABC)
midsegment_of_triangle_property_parallel(1,DE,ABC)
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, the area of triangle ABC is 24, AB=Mul(2,LengthOfLine(DE)), AC=Mul(2,LengthOfLine(DF)), ∠CAB=∠FDE. Find the area of △DEF.
问题：如图所示，三角形ABC的面积为24，AB=Mul(2,LengthOfLine(DE))，AC=Mul(2,LengthOfLine(DF))，∠CAB=∠FDE。求△DEF的面积。
Construction (CDL):
Shape(AB,BC,CA)
Shape(DE,EF,FD)
Conditions (CDL):
Equal(AreaOfTriangle(ABC),24)
Equal(LengthOfLine(AB),Mul(2,LengthOfLine(DE)))
Equal(LengthOfLine(AC),Mul(2,LengthOfLine(DF)))
Equal(MeasureOfAngle(CAB),MeasureOfAngle(FDE))
Goal: Value(AreaOfTriangle(DEF))
Answer: 6
Theorem sequence:
similar_triangle_judgment_sas(1,ABC,DEF)
similar_triangle_property_line_ratio(1,CAB,FDE)
similar_triangle_property_area_square_ratio(1,ABC,DEF)
Problem: As shown in the diagram, AB=AC, AE=1, BD=2, CD=3, CE=4, ∠ABC=∠FDE. Find the length of line AF.
问题：如图所示，AB=AC，AE=1，BD=2，CD=3，CE=4，∠ABC=∠FDE。求直线AF的长度。
Construction (CDL):
Shape(AF,FD,DE,EA)
Shape(FB,BD,DF)
Shape(ED,DC,CE)
Collinear(AFB)
Collinear(BDC)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AB),LengthOfLine(AC))
Equal(LengthOfLine(AE),1)
Equal(LengthOfLine(BD),2)
Equal(LengthOfLine(CD),3)
Equal(LengthOfLine(CE),4)
Equal(MeasureOfAngle(ABC),MeasureOfAngle(FDE))
Goal: Value(LengthOfLine(AF))
Answer: 7/2
Theorem sequence:
line_addition(1,AE,EC)
line_addition(1,AF,FB)
isosceles_triangle_judgment_line_equal(1,ABC)
isosceles_triangle_property_angle_equal(1,ABC)
triangle_property_angle_sum(1,BDF)
angle_addition(1,BDF,FDE)
adjacent_complementary_angle(1,BDE,EDC)
similar_triangle_judgment_aa(1,DFB,EDC)
similar_triangle_property_line_ratio(1,DFB,EDC)
similar_triangle_property_line_ratio(1,FBD,DCE)
Problem: As shown in the diagram, the area of triangle ADE is 2, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE is parallel to BC. Find the area of triangle ABC.
问题：如图所示，三角形ADE的面积为2，Div(LengthOfLine(AD)=LengthOfLine(AB))，DE∥BC。求△ABC的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),2)
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),1/3)
ParallelBetweenLine(DE,BC)
Goal: Value(AreaOfTriangle(ABC))
Answer: 18
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_area_square_ratio(1,ADE,ABC)
Problem: As shown in the diagram, AP=6, DC=6, DP=3, ∠BDA=∠BCA. Find the length of line AB.
问题：如图所示，AP=6，DC=6，DP=3，∠BDA=∠BCA。求直线AB的长度。
Construction (CDL):
Shape(DA,AP,PD)
Shape(CD,DP,PC)
Shape(CP,PB,BC)
Shape(PA,AB,BP)
Collinear(DPB)
Collinear(APC)
Conditions (CDL):
Equal(LengthOfLine(AP),6)
Equal(LengthOfLine(DC),6)
Equal(LengthOfLine(DP),3)
Equal(MeasureOfAngle(BDA),MeasureOfAngle(BCA))
Goal: Value(LengthOfLine(AB))
Answer: 12
Theorem sequence:
vertical_angle(1,DPC,BPA)
vertical_angle(1,APD,CPB)
mirror_similar_triangle_judgment_aa(1,BCP,APD)
mirror_similar_triangle_property_line_ratio(1,BCP,APD)
mirror_similar_triangle_property_line_ratio(1,CPB,DAP)
mirror_similar_triangle_judgment_sas(1,PCD,PAB)
mirror_similar_triangle_property_line_ratio(1,PCD,PAB)
mirror_similar_triangle_property_line_ratio(1,CDP,BPA)
Problem: As shown in the diagram, the area of triangle ADE is 4, Div(LengthOfLine(AD)=LengthOfLine(BD)), DE is parallel to BC. Find the area of △ABC.
问题：如图所示，三角形ADE的面积为4，Div(LengthOfLine(AD)=LengthOfLine(BD))，DE平行于BC。求三角形ABC的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),4)
Equal(Div(LengthOfLine(AD),LengthOfLine(BD)),1/2)
ParallelBetweenLine(DE,BC)
Goal: Value(AreaOfTriangle(ABC))
Answer: 36
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,EAD,CAB)
similar_triangle_property_area_square_ratio(1,ADE,ABC)
Problem: As shown in the diagram, the area of triangle ADC is 9, Div(LengthOfLine(AC)=LengthOfLine(BC)), CD is the altitude of △ CAB, ∠BCA is the right angle of the right triangle BCA. Find the area of △CDB.
问题：如图所示，三角形ADC的面积为9，Div(LengthOfLine(AC)=LengthOfLine(BC))，CD是三角形CAB的高，∠BCA是直角三角形BCA的直角。求△CDB的面积。
Construction (CDL):
Shape(AD,DC,CA)
Shape(CD,DB,BC)
Collinear(ADB)
Conditions (CDL):
Equal(AreaOfTriangle(ADC),9)
Equal(Div(LengthOfLine(AC),LengthOfLine(BC)),3/2)
IsAltitudeOfTriangle(CD,CAB)
RightTriangle(BCA)
Goal: Value(AreaOfTriangle(CDB))
Answer: 4
Theorem sequence:
angle_addition(1,BCD,DCA)
triangle_property_angle_sum(1,ADC)
triangle_property_angle_sum(1,CDB)
similar_triangle_judgment_aa(1,DCA,DBC)
similar_triangle_property_line_ratio(1,DCA,DBC)
similar_triangle_property_area_square_ratio(1,DCA,DBC)
Problem: As shown in the diagram, AB=3, BC=5, BE bisects ∠ABC, BA and CD are opposite sides of the ▱ ABCD. Find the ratio of the length of line BF to the length of line EF.
问题：如图所示，AB=3，BC=5，BE平分∠ABC，ABCD是平行四边形。求直线BF的长度与直线EF的长度之比。
Construction (CDL):
Shape(AB,BF,FA)
Shape(AF,FE,EA)
Shape(FB,BC,CF)
Shape(EF,FC,CD,DE)
Collinear(AED)
Collinear(AFC)
Collinear(BFE)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BC),5)
IsBisectorOfAngle(BE,ABC)
Parallelogram(ABCD)
Goal: Value(Div(LengthOfLine(BF),LengthOfLine(EF)))
Answer: 5/3
Theorem sequence:
parallel_property_collinear_extend(3,AD,BC,E)
parallel_property_alternate_interior_angle(1,AE,BC)
parallel_property_alternate_interior_angle(2,AE,BC)
isosceles_triangle_judgment_angle_equal(1,ABE)
similar_triangle_judgment_aa(1,FEA,FBC)
similar_triangle_property_line_ratio(1,FEA,FBC)
similar_triangle_property_line_ratio(1,AFE,CFB)
Problem: As shown in the diagram, Div(LengthOfLine(CE)=LengthOfLine(ED)), AB=14, BC=6, AE is perpendicular to CE, BA and DC are the non-parallel sides of right trapezoid BADC. Find the length of line AD.
问题：如图所示，Div(LengthOfLine(CE)=LengthOfLine(ED))，AB=14，BC=6，AE垂直于CE，∠CBA和∠BAD是直角梯形BADC的直角。求直线AD的长度。
Construction (CDL):
Shape(AE,EC,CB,BA)
Shape(CE,ED,DC)
Collinear(AED)
Conditions (CDL):
Equal(Div(LengthOfLine(CE),LengthOfLine(ED)),1/2)
Equal(LengthOfLine(AB),14)
Equal(LengthOfLine(BC),6)
PerpendicularBetweenLine(AE,CE)
RightTrapezoid(BADC)
Goal: Value(LengthOfLine(AD))
Answer: 34
Theorem sequence:
parallel_judgment_ipsilateral_internal_angle(1,AB,EC)
parallel_property_collinear_extend(3,DA,CB,E)
parallelogram_judgment_parallel_and_parallel(1,BAEC)
parallelogram_property_opposite_line_equal(1,BAEC)
parallelogram_property_opposite_line_equal(1,AECB)
line_addition(1,AE,ED)
Problem: As shown in the diagram, AB=10, ∠ABC=30°, BC is perpendicular to AC. Find the length of line CA.
问题：如图所示，AB=10，∠ABC=30°，BC垂直于AC。求直线CA的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(MeasureOfAngle(ABC),30)
PerpendicularBetweenLine(BC,AC)
Goal: Value(LengthOfLine(CA))
Answer: 5
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, BC=2, Tan(MeasureOfAngle(BAC))=1/3, AC is perpendicular to BC. Find the length of line AB.
问题：如图所示，BC=2，Tan(MeasureOfAngle(BAC))=1/3，AC垂直于BC。求直线AB的长度。
Construction (CDL):
Shape(BA,AC,CB)
Conditions (CDL):
Equal(LengthOfLine(BC),2)
Equal(Tan(MeasureOfAngle(BAC)),1/3)
PerpendicularBetweenLine(AC,BC)
Goal: Value(LengthOfLine(AB))
Answer: 2*sqrt(10)
Theorem sequence:
sine_theorem(1,BAC)
Problem: As shown in the diagram, AC=6, BC=24, Tan(MeasureOfAngle(ADC))=1/6, BC⊥AC. Find the length of line BD.
问题：如图所示，AC=6，BC=24，Tan(MeasureOfAngle(ADC))=1/6，BC⊥AC。求直线BD的长度。
Construction (CDL):
Shape(AD,DB,BA)
Shape(AB,BC,CA)
Collinear(DBC)
Conditions (CDL):
Equal(LengthOfLine(AC),6)
Equal(LengthOfLine(BC),24)
Equal(Tan(MeasureOfAngle(ADC)),1/6)
PerpendicularBetweenLine(BC,AC)
Goal: Value(LengthOfLine(BD))
Answer: 12
Theorem sequence:
triangle_property_angle_sum(1,ADC)
sine_theorem(1,CAD)
line_addition(1,DB,BC)
Problem: As shown in the diagram, AB=6, Sin(MeasureOfAngle(BCA))=3/5, AB⊥CB. Find the length of line AC.
问题：如图所示，AB=6，Sin(MeasureOfAngle(BCA))=3/5，AB⊥CB。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(Sin(MeasureOfAngle(BCA)),3/5)
PerpendicularBetweenLine(AB,CB)
Goal: Value(LengthOfLine(AC))
Answer: 10
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, BC=2, Tan(MeasureOfAngle(CAB))=1/3, BC is perpendicular to AC. Find the length of line AB.
问题：如图所示，BC=2，Tan(MeasureOfAngle(CAB))=1/3，BC垂直于AC。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(BE,EF,FC,CB)
Collinear(FCA)
Conditions (CDL):
Equal(LengthOfLine(BC),2)
Equal(Tan(MeasureOfAngle(CAB)),1/3)
PerpendicularBetweenLine(BC,AC)
Goal: Value(LengthOfLine(AB))
Answer: 2*sqrt(10)
Theorem sequence:
sine_theorem(1,BCA)
Problem: As shown in the diagram, AB=300, AC=500, AB⊥CB. Find the value of tan(BC).
问题：如图所示，AB=300，AC=500，AB⊥CB。求tan(BC)的值。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),300)
Equal(LengthOfLine(AC),500)
PerpendicularBetweenLine(AB,CB)
Goal: Value(Tan(MeasureOfAngle(BCA)))
Answer: 3/4
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, BC=50, ∠ABC=120°, BE is perpendicular to DE, BF⊥CF. Find the length of line CF.
问题：如图所示，BC=50，∠ABC=120°，BE⊥DE，BF⊥CF。求直线CF的长度。
Construction (CDL):
Shape(AB,BC)
Shape(CB,BF,FC)
Shape(DC,CF,FE,ED)
Collinear(ABFE)
Conditions (CDL):
Equal(LengthOfLine(BC),50)
Equal(MeasureOfAngle(ABC),120)
PerpendicularBetweenLine(BE,DE)
PerpendicularBetweenLine(BF,CF)
Goal: Value(LengthOfLine(CF))
Answer: 25*sqrt(3)
Theorem sequence:
adjacent_complementary_angle(1,ABC,CBF)
sine_theorem(1,CBF)
Problem: As shown in the diagram, AC=12, Tan(MeasureOfAngle(BAC))=5/12, AC⊥BC. Find the length of line AB.
问题：如图所示，AC=12，Tan(MeasureOfAngle(BAC))=5/12，AC垂直于BC。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(AC),12)
Equal(Tan(MeasureOfAngle(BAC)),5/12)
PerpendicularBetweenLine(AC,BC)
Goal: Value(LengthOfLine(AB))
Answer: 13
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,ACB)
Problem: As shown in the diagram, BC=100, ∠ABC=120°, BE⊥DE, BF is perpendicular to CF. Find the length of line CF.
问题：如图所示，BC=100，∠ABC=120°，BE⊥DE，BF垂直于CF。求直线CF的长度。
Construction (CDL):
Shape(AB,BC)
Shape(CB,BF,FC)
Shape(DC,CF,FE,ED)
Collinear(ABFE)
Conditions (CDL):
Equal(LengthOfLine(BC),100)
Equal(MeasureOfAngle(ABC),120)
PerpendicularBetweenLine(BE,DE)
PerpendicularBetweenLine(BF,CF)
Goal: Value(LengthOfLine(CF))
Answer: 50*sqrt(3)
Theorem sequence:
adjacent_complementary_angle(1,ABC,CBF)
sine_theorem(1,CBF)
Problem: As shown in the diagram, BC=4, ∠BDC=60°, ∠CBD=30°, AB is perpendicular to DB. Find the length of line AB.
问题：如图所示，BC=4，∠BDC=60°，∠CBD=30°，AB垂直于DB。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(BD,DC,CB)
Collinear(ACD)
Conditions (CDL):
Equal(LengthOfLine(BC),4)
Equal(MeasureOfAngle(BDC),60)
Equal(MeasureOfAngle(CBD),30)
PerpendicularBetweenLine(AB,DB)
Goal: Value(LengthOfLine(AB))
Answer: 8
Theorem sequence:
angle_addition(1,ABC,CBD)
triangle_property_angle_sum(1,ABC)
triangle_property_angle_sum(1,ABD)
sine_theorem(1,BCA)
Problem: As shown in the diagram, BC=4, Tan(MeasureOfAngle(ABC))=1/2, BC is perpendicular to AC. Find the length of line AB.
问题：如图所示，BC=4，Tan(MeasureOfAngle(ABC))=1/2，BC⊥AC。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(BC),4)
Equal(Tan(MeasureOfAngle(ABC)),1/2)
PerpendicularBetweenLine(BC,AC)
Goal: Value(LengthOfLine(AB))
Answer: 2*sqrt(5)
Theorem sequence:
triangle_property_angle_sum(1,ABC)
sine_theorem(1,BCA)
Problem: As shown in the diagram, AB=10, CA=6, BC is perpendicular to AC. Find the value of tan(AB).
问题：如图所示，AB=10，CA=6，BC⊥AC。求tan(AB)的值。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(LengthOfLine(CA),6)
PerpendicularBetweenLine(BC,AC)
Goal: Value(Tan(MeasureOfAngle(ABC)))
Answer: 3/4
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, BC=10, BE=12, Tan(MeasureOfAngle(BAE))=2/3, BADC is a isosceles trapezoid, AE is perpendicular to BE, CF is perpendicular to DF. Find the length of line AD.
问题：如图所示，BC=10，BE=12，Tan(MeasureOfAngle(BAE))=2/3，BA和DC是等腰梯形BADC的腰，AE⊥BE，CF垂直于DF。求直线AD的长度。
Construction (CDL):
Shape(AE,EB,BA)
Shape(BE,EF,FC,CB)
Shape(CF,FD,DC)
Collinear(AEFD)
Conditions (CDL):
Equal(LengthOfLine(BC),10)
Equal(LengthOfLine(BE),12)
Equal(Tan(MeasureOfAngle(BAE)),2/3)
IsoscelesTrapezoid(BADC)
PerpendicularBetweenLine(AE,BE)
PerpendicularBetweenLine(CF,DF)
Goal: Value(LengthOfLine(AD))
Answer: 46
Theorem sequence:
line_addition(1,AE,EF)
line_addition(1,AF,FD)
isosceles_trapezoid_property_angle_equal(1,BADC)
triangle_property_angle_sum(1,AEB)
triangle_property_angle_sum(1,CFD)
sine_theorem(1,EBA)
sine_theorem(1,FDC)
parallel_property_collinear_extend(3,DA,CB,F)
parallel_property_collinear_extend(3,FA,CB,E)
adjacent_complementary_angle(1,AEB,BEF)
adjacent_complementary_angle(1,AFC,CFD)
parallel_judgment_ipsilateral_internal_angle(1,EB,FC)
parallelogram_judgment_parallel_and_parallel(1,BEFC)
parallelogram_property_opposite_line_equal(1,BEFC)
parallelogram_property_opposite_line_equal(1,EFCB)