SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, Div(LengthOfLine(AC)=LengthOfLine(AD)), BC is parallel to DE. Find the ratio of the length of line AB to the length of line AE.
问题：如图所示，Div(LengthOfLine(AC)=LengthOfLine(AD))，BC∥DE。求直线AB的长度与直线AE的长度之比。
Construction (CDL):
Shape(BA,AC,CB)
Shape(AD,DE,EA)
Collinear(BAE)
Collinear(DAC)
Conditions (CDL):
Equal(Div(LengthOfLine(AC),LengthOfLine(AD)),1/2)
ParallelBetweenLine(BC,DE)
Goal: Value(Div(LengthOfLine(AB),LengthOfLine(AE)))
Answer: 1/2
Theorem sequence:
parallel_property_alternate_interior_angle(2,BC,DE)
vertical_angle(1,BAC,EAD)
similar_triangle_judgment_aa(1,BAC,EAD)
similar_triangle_property_line_ratio(1,BAC,EAD)
similar_triangle_property_line_ratio(1,CBA,DEA)
Problem: As shown in the diagram, Div(LengthOfLine(EG)=LengthOfLine(AB)), DC=6, DC is parallel to EF, EF∥AB. Find the length of line GF.
问题：如图所示，Div(LengthOfLine(EG)=LengthOfLine(AB))，DC=6，DC平行于EF，EF∥AB。求直线GF的长度。
Construction (CDL):
Shape(DE,EG,GD)
Shape(DG,GF,FC,CD)
Shape(EA,AB,BG,GE)
Shape(GB,BF,FG)
Collinear(EGF)
Collinear(DGB)
Collinear(DEA)
Collinear(CFB)
Conditions (CDL):
Equal(Div(LengthOfLine(EG),LengthOfLine(AB)),1/2)
Equal(LengthOfLine(DC),6)
ParallelBetweenLine(DC,EF)
ParallelBetweenLine(EF,AB)
Goal: Value(LengthOfLine(GF))
Answer: 3
Theorem sequence:
parallel_property_collinear_extend(3,EF,AB,G)
parallel_property_corresponding_angle(1,FE,CD,B)
parallel_property_corresponding_angle(1,EF,AB,D)
parallel_property_corresponding_angle(2,BA,GE,D)
line_addition(1,DG,GB)
similar_triangle_judgment_aa(1,GBF,DBC)
similar_triangle_judgment_aa(1,DAB,DEG)
similar_triangle_property_line_ratio(1,BFG,BCD)
similar_triangle_property_line_ratio(1,FGB,CDB)
similar_triangle_property_line_ratio(1,DAB,DEG)
similar_triangle_property_line_ratio(1,ABD,EGD)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(CD)), ∠ADC=90°, ∠CAB=90°. Find the ratio of the length of line AB to the length of line AC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(CD))，∠ADC=90°，∠CAB=90°。求直线AB的长度与直线AC的长度之比。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DC,CA)
Collinear(BDC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(CD)),3/2)
Equal(MeasureOfAngle(ADC),90)
Equal(MeasureOfAngle(CAB),90)
Goal: Value(Div(LengthOfLine(AB),LengthOfLine(AC)))
Answer: 3/2
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,ADC,BCA)
mirror_similar_triangle_judgment_aa(1,BCA,ADC)
mirror_similar_triangle_property_line_ratio(1,ADC,BCA)
mirror_similar_triangle_property_line_ratio(1,CAD,CAB)
mirror_similar_triangle_property_line_ratio(1,BCA,ADC)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), DE=3, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，DE=3，DE∥BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),2/5)
Equal(LengthOfLine(DE),3)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 15/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_line_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, the area of triangle ADE is 1, D is the midpoint of segment AB, E bisects segment AC. Find the area of triangle ABC.
问题：如图所示，△ADE的面积为1，D平分线段AB，E平分线段AC。求△ABC的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),1)
IsMidpointOfLine(D,AB)
IsMidpointOfLine(E,AC)
Goal: Value(AreaOfTriangle(ABC))
Answer: 4
Theorem sequence:
line_addition(1,AD,DB)
line_addition(1,AE,EC)
similar_triangle_judgment_sas(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, Div(LengthOfLine(AF)=LengthOfLine(BF)), AD=8, ABCD is a ▱. Find the length of line AE.
问题：如图所示，Div(LengthOfLine(AF)=LengthOfLine(BF))，AD=8，四边形ABCD是▱。求直线AE的长度。
Construction (CDL):
Shape(EF,FA,AE)
Shape(FB,BC,CF)
Shape(AF,FC,CD,DA)
Collinear(EAD)
Collinear(BFA)
Collinear(EFC)
Conditions (CDL):
Equal(Div(LengthOfLine(AF),LengthOfLine(BF)),3/4)
Equal(LengthOfLine(AD),8)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(AE))
Answer: 6
Theorem sequence:
parallelogram_property_opposite_line_equal(1,BCDA)
parallel_property_collinear_extend(1,AD,BC,E)
parallel_property_alternate_interior_angle(1,EA,BC)
parallel_property_alternate_interior_angle(2,EA,BC)
similar_triangle_judgment_aa(1,FBC,FAE)
similar_triangle_property_line_ratio(1,FBC,FAE)
similar_triangle_property_line_ratio(1,CFB,EFA)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), DE=6, DE∥BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，DE=6，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),1/3)
Equal(LengthOfLine(DE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 24
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=10, BD=3/2, DE=8, ∠ADE=∠ABC. Find the length of line AB.
问题：如图所示，BC=10，BD=3/2，DE=8，∠ADE=∠ABC。求直线AB的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(BC),10)
Equal(LengthOfLine(BD),3/2)
Equal(LengthOfLine(DE),8)
Equal(MeasureOfAngle(ADE),MeasureOfAngle(ABC))
Goal: Value(LengthOfLine(AB))
Answer: 15/2
Theorem sequence:
line_addition(1,AD,DB)
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, AB=1, CD=4, BA∥FE, FE is parallel to DC. Find the length of line EF.
问题：如图所示，AB=1，CD=4，BA平行于FE，FE∥DC。求直线EF的长度。
Construction (CDL):
Shape(AB,BE,EA)
Shape(EB,BF,FE)
Shape(EF,FD,DE)
Shape(ED,DC,CE)
Collinear(AED)
Collinear(BEC)
Collinear(BFD)
Conditions (CDL):
Equal(LengthOfLine(AB),1)
Equal(LengthOfLine(CD),4)
ParallelBetweenLine(BA,FE)
ParallelBetweenLine(FE,DC)
Goal: Value(LengthOfLine(EF))
Answer: 4/5
Theorem sequence:
parallel_property_corresponding_angle(1,FE,DC,B)
parallel_property_corresponding_angle(2,BA,FE,D)
line_addition(1,BF,FD)
similar_triangle_judgment_aa(1,EBF,CBD)
similar_triangle_judgment_aa(1,EFD,ABD)
similar_triangle_judgment_aa(1,ABD,EFD)
similar_triangle_property_line_ratio(1,EBF,CBD)
similar_triangle_property_line_ratio(1,BFE,BDC)
similar_triangle_property_line_ratio(1,EFD,ABD)
similar_triangle_property_line_ratio(1,ABD,EFD)
similar_triangle_property_line_ratio(1,DAB,DEF)
Problem: As shown in the diagram, AE=3, EC=6, DE is parallel to BC. Find the ratio of the length of line DE to the length of line BC.
问题：如图所示，AE=3，EC=6，DE平行于BC。求直线DE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(EC),6)
ParallelBetweenLine(DE,BC)
Goal: Value(Div(LengthOfLine(DE),LengthOfLine(BC)))
Answer: 1/3
Theorem sequence:
line_addition(1,AE,EC)
parallel_property_corresponding_angle(1,DE,BC,A)
similar_triangle_judgment_aa(1,CAB,EAD)
similar_triangle_property_line_ratio(1,ABC,ADE)
similar_triangle_property_line_ratio(1,BCA,DEA)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), BC=12, DE∥BC. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，BC=12，DE平行于BC。求直线DE的长度。
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(BC),12)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 4
Theorem sequence:
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(AE)=LengthOfLine(BE)), BF=2, AD and BC are opposite sides of the parallelogram ABCD. Find the length of line DF.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(BE))，BF=2，BA和CD是▱ABCD的一组对边。求直线DF的长度。
Construction (CDL):
Shape(BF,FE,EB)
Shape(FB,BC,CF)
Shape(FC,CD,DF)
Shape(EF,FD,DA,AE)
Collinear(AEB)
Collinear(BFD)
Collinear(EFC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(BE)),2)
Equal(LengthOfLine(BF),2)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(DF))
Answer: 6
Theorem sequence:
line_addition(1,AE,EB)
parallelogram_property_opposite_line_equal(1,ABCD)
parallel_property_collinear_extend(3,BA,CD,E)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(2,BE,CD)
similar_triangle_judgment_aa(1,FCD,FEB)
similar_triangle_property_line_ratio(1,FCD,FEB)
similar_triangle_property_line_ratio(1,CDF,EBF)
Problem: As shown in the diagram, AB=6, BC=5, EF=3, BE is the altitude of △ BCA, CF is the altitude of △ CAB. Find the length of line AE.
问题：如图所示，AB=6，BC=5，EF=3，BE是△BCA的高，CF是△CAB的高。求直线AE的长度。
Construction (CDL):
Shape(AF,FE,EA)
Shape(FB,BD,DF)
Shape(DB,BC,CD)
Shape(DC,CE,ED)
Shape(FD,DE,EF)
Collinear(AFB)
Collinear(AEC)
Collinear(BDE)
Collinear(FDC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(BC),5)
Equal(LengthOfLine(EF),3)
IsAltitudeOfTriangle(BE,BCA)
IsAltitudeOfTriangle(CF,CAB)
Goal: Value(LengthOfLine(AE))
Answer: 18/5
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,CAF,BEA)
mirror_similar_triangle_property_line_ratio(1,CAF,BEA)
mirror_similar_triangle_property_line_ratio(1,FCA,EAB)
mirror_similar_triangle_judgment_sas(1,AFE,ABC)
mirror_similar_triangle_property_line_ratio(1,AFE,ABC)
mirror_similar_triangle_property_line_ratio(1,FEA,CAB)
Problem: As shown in the diagram, the area of triangle ADC is 1, AC=2, AD=1, ∠DCA=∠ABC. Find the area of triangle ABC.
问题：如图所示，三角形ADC的面积为1，AC=2，AD=1，∠DCA=∠ABC。求△ABC的面积。
Construction (CDL):
Shape(AD,DC,CA)
Shape(DB,BC,CD)
Collinear(ADB)
Conditions (CDL):
Equal(AreaOfTriangle(ADC),1)
Equal(LengthOfLine(AC),2)
Equal(LengthOfLine(AD),1)
Equal(MeasureOfAngle(DCA),MeasureOfAngle(ABC))
Goal: Value(AreaOfTriangle(ABC))
Answer: 4
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DCA,CAB)
mirror_similar_triangle_property_line_ratio(1,CAD,BCA)
mirror_similar_triangle_property_area_square_ratio(1,DCA,CAB)
Problem: As shown in the diagram, AD=4, DB=2, DE=3, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AD=4，DB=2，DE=3，DE∥BC。求直线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)
Equal(LengthOfLine(DE),3)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 9/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)
line_addition(1,AD,DB)
similar_triangle_property_line_ratio(1,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, the area of △ADC is 3, AC=2, AD=1, ∠DCA=∠ABC. Find the area of △ABC minus the area of △ADC.
问题：如图所示，△ADC的面积为3，AC=2，AD=1，∠DCA=∠ABC。求三角形ABC的面积减去三角形ADC的面积。
Construction (CDL):
Shape(BC,CD,DB)
Shape(AD,DC,CA)
Collinear(BDA)
Conditions (CDL):
Equal(AreaOfTriangle(ADC),3)
Equal(LengthOfLine(AC),2)
Equal(LengthOfLine(AD),1)
Equal(MeasureOfAngle(DCA),MeasureOfAngle(ABC))
Goal: Value(Sub(AreaOfTriangle(ABC),AreaOfTriangle(ADC)))
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(AD)=LengthOfLine(BD)), Div(LengthOfLine(AE)=LengthOfLine(EC)), DE=3. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(BD))，Div(LengthOfLine(AE)=LengthOfLine(EC))，DE=3。求直线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/2)
Equal(Div(LengthOfLine(AE),LengthOfLine(EC)),1/2)
Equal(LengthOfLine(DE),3)
Goal: Value(LengthOfLine(BC))
Answer: 9
Theorem sequence:
line_addition(1,AD,DB)
line_addition(1,AE,EC)
similar_triangle_judgment_sas(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, Div(LengthOfLine(AE)=LengthOfLine(AC)), BC=30, DE is parallel to BC. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AC))，BC=30，DE平行于BC。求直线DE的长度。
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(BC),30)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 10
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,DEA,BCA)
Problem: As shown in the diagram, AB=15, AC=12, AEDF is a rhombus. Find the length of line AE.
问题：如图所示，AB=15，AC=12，AEDF是菱形。求直线AE的长度。
Construction (CDL):
Shape(BD,DE,EB)
Shape(ED,DF,FA,AE)
Shape(FD,DC,CF)
Collinear(BEA)
Collinear(BDC)
Collinear(AFC)
Conditions (CDL):
Equal(LengthOfLine(AB),15)
Equal(LengthOfLine(AC),12)
Rhombus(AEDF)
Goal: Value(LengthOfLine(AE))
Answer: 20/3
Theorem sequence:
parallel_property_collinear_extend(2,AF,ED,C)
parallel_property_corresponding_angle(1,FD,AE,C)
parallel_property_corresponding_angle(1,DE,CA,B)
parallel_property_corresponding_angle(2,AF,ED,B)
line_addition(1,BE,EA)
line_addition(1,AF,FC)
similar_triangle_judgment_aa(1,BDE,DCF)
similar_triangle_property_line_ratio(1,BDE,DCF)
similar_triangle_property_line_ratio(1,DEB,CFD)
Problem: As shown in the diagram, AB=1, ABCD is a rhombus. Find the value of 1/AM+1/AN.
问题：如图所示，AB=1，ABCD是菱形。求1/AM+1/AN的值。
Construction (CDL):
Shape(ND,DC,CN)
Shape(DA,AB,BC,CD)
Shape(CB,BM,MC)
Collinear(ADN)
Collinear(MCN)
Collinear(ABM)
Conditions (CDL):
Equal(LengthOfLine(AB),1)
Rhombus(ABCD)
Goal: Value(Add(Div(1,LengthOfLine(AM)),Div(1,LengthOfLine(AN))))
Answer: 1
Theorem sequence:
parallel_property_corresponding_angle(2,AD,BC,M)
line_addition(1,AB,BM)
similar_triangle_judgment_aa(1,NAM,CBM)
similar_triangle_property_line_ratio(1,NAM,CBM)
similar_triangle_property_line_ratio(1,MNA,MCB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), DE=6, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，DE=6，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(DB)),3/4)
Equal(LengthOfLine(DE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 14
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, AC=4, CD=2, CA⊥BA, ED is perpendicular to CD. Find the length of line CE.
问题：如图所示，AB=3，AC=4，CD=2，CA垂直于BA，ED⊥CD。求直线CE的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(CE,ED,DC)
Collinear(ACE)
Collinear(BCD)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(AC),4)
Equal(LengthOfLine(CD),2)
PerpendicularBetweenLine(CA,BA)
PerpendicularBetweenLine(ED,CD)
Goal: Value(LengthOfLine(CE))
Answer: 5/2
Theorem sequence:
vertical_angle(1,BCA,DCE)
mirror_similar_triangle_judgment_aa(1,BCA,EDC)
mirror_similar_triangle_property_line_ratio(1,BCA,EDC)
mirror_similar_triangle_property_line_ratio(1,CAB,CED)
right_triangle_judgment_angle(1,EDC)
right_triangle_property_pythagorean(1,EDC)
Problem: As shown in the diagram, Div(LengthOfLine(AB)=LengthOfLine(BC)), AB=6, ∠ABC=90°. Find the length of line AC.
问题：如图所示，Div(LengthOfLine(AB)=LengthOfLine(BC))，AB=6，∠ABC=90°。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(Div(LengthOfLine(AB),LengthOfLine(BC)),3/4)
Equal(LengthOfLine(AB),6)
Equal(MeasureOfAngle(ABC),90)
Goal: Value(LengthOfLine(AC))
Answer: 10
Theorem sequence:
right_triangle_judgment_angle(1,ABC)
right_triangle_property_pythagorean(1,ABC)
Problem: As shown in the diagram, BC=8, ∠BCA=90°, ∠CAB=30°. Find the length of line AB.
问题：如图所示，BC=8，∠BCA=90°，∠CAB=30°。求直线AB的长度。
Construction (CDL):
Shape(BC,CA,AB)
Conditions (CDL):
Equal(LengthOfLine(BC),8)
Equal(MeasureOfAngle(BCA),90)
Equal(MeasureOfAngle(CAB),30)
Goal: Value(LengthOfLine(AB))
Answer: 16
Theorem sequence:
sine_theorem(1,BCA)
Problem: As shown in the diagram, AB=4, ∠ABD=60°, ∠ACD=45°. Find the length of line AC.
问题：如图所示，AB=4，∠ABD=60°，∠ACD=45°。求直线AC的长度。
Construction (CDL):
Shape(AC,CB,BA)
Shape(AB,BD,DA)
Collinear(CBD)
Conditions (CDL):
Equal(LengthOfLine(AB),4)
Equal(MeasureOfAngle(ABD),60)
Equal(MeasureOfAngle(ACD),45)
Goal: Value(LengthOfLine(AC))
Answer: 2*sqrt(6)
Theorem sequence:
sine_theorem(1,ABD)
sine_theorem(1,ACD)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(AC)), AC=12, ∠BCA=90°. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(AC))，AC=12，∠BCA=90°。求直线AB的长度。
Construction (CDL):
Shape(DE,EC,CB,BD)
Shape(BC,CA,AB)
Collinear(ECA)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(AC)),1/2)
Equal(LengthOfLine(AC),12)
Equal(MeasureOfAngle(BCA),90)
Goal: Value(LengthOfLine(AB))
Answer: 6*sqrt(5)
Theorem sequence:
right_triangle_judgment_angle(1,BCA)
right_triangle_property_pythagorean(1,BCA)
Problem: As shown in the diagram, AB=600, ∠ACB=90°, ∠BAC=30°. Find the length of line BC.
问题：如图所示，AB=600，∠ACB=90°，∠BAC=30°。求直线BC的长度。
Construction (CDL):
Shape(BA,AC,CB)
Conditions (CDL):
Equal(LengthOfLine(AB),600)
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(BAC),30)
Goal: Value(LengthOfLine(BC))
Answer: 300
Theorem sequence:
sine_theorem(1,BAC)
Problem: As shown in the diagram, AB=6, ∠ABC=90°, Sin(MeasureOfAngle(BCA))=1/3. Find the length of line AC.
问题：如图所示，AB=6，∠ABC=90°，Sin(MeasureOfAngle(BCA))=1/3。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(MeasureOfAngle(ABC),90)
Equal(Sin(MeasureOfAngle(BCA)),1/3)
Goal: Value(LengthOfLine(AC))
Answer: 18
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, AB=6, ∠ABC=90°, Sin(MeasureOfAngle(BCA))=3/5. Find the length of line AC.
问题：如图所示，AB=6，∠ABC=90°，Sin(MeasureOfAngle(BCA))=3/5。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(MeasureOfAngle(ABC),90)
Equal(Sin(MeasureOfAngle(BCA)),3/5)
Goal: Value(LengthOfLine(AC))
Answer: 10
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, CD=5, ∠ADC=90°, ∠CAD=60°. Find the length of line AC.
问题：如图所示，CD=5，∠ADC=90°，∠CAD=60°。求直线AC的长度。
Construction (CDL):
Shape(CA,AD,DC)
Shape(CD,DB,BC)
Collinear(ADB)
Conditions (CDL):
Equal(LengthOfLine(CD),5)
Equal(MeasureOfAngle(ADC),90)
Equal(MeasureOfAngle(CAD),60)
Goal: Value(LengthOfLine(AC))
Answer: 10*sqrt(3)/3
Theorem sequence:
sine_theorem(1,CAD)
Problem: As shown in the diagram, AC=2, ∠ACB=90°, ∠BAC=30°. Find the length of line AB.
问题：如图所示，AC=2，∠ACB=90°，∠BAC=30°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(AC),2)
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(BAC),30)
Goal: Value(LengthOfLine(AB))
Answer: 4*sqrt(3)/3
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,ACB)
Problem: As shown in the diagram, AB=13, BC=12, ∠BCA=90°. Find the ratio of the length of line AC to the length of line BC.
问题：如图所示，AB=13，BC=12，∠BCA=90°。求直线AC的长度与直线BC的长度之比。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),13)
Equal(LengthOfLine(BC),12)
Equal(MeasureOfAngle(BCA),90)
Goal: Value(Div(LengthOfLine(AC),LengthOfLine(BC)))
Answer: 5/12
Theorem sequence:
right_triangle_judgment_angle(1,BCA)
right_triangle_property_pythagorean(1,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(AC)), BC=5, ∠BCA=90°. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(AC))，BC=5，∠BCA=90°。求直线AB的长度。
Construction (CDL):
Shape(BC,CA,AB)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(AC)),1/2)
Equal(LengthOfLine(BC),5)
Equal(MeasureOfAngle(BCA),90)
Goal: Value(LengthOfLine(AB))
Answer: 5*sqrt(5)
Theorem sequence:
right_triangle_judgment_angle(1,BCA)
right_triangle_property_pythagorean(1,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(AC)), AC=6, ∠ACB=90°. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(AC))，AC=6，∠ACB=90°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(AC)),1/2)
Equal(LengthOfLine(AC),6)
Equal(MeasureOfAngle(ACB),90)
Goal: Value(LengthOfLine(AB))
Answer: 3*sqrt(5)
Theorem sequence:
right_triangle_judgment_angle(1,ACB)
right_triangle_property_pythagorean(1,ACB)
Problem: As shown in the diagram, AC=6, ∠ACB=90°, ∠BAC=30°. Find the length of line AB.
问题：如图所示，AC=6，∠ACB=90°，∠BAC=30°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(AC),6)
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(BAC),30)
Goal: Value(LengthOfLine(AB))
Answer: 4*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,ACB)
Problem: As shown in the diagram, Div(LengthOfLine(BC)=LengthOfLine(AC)), BC=1, ∠ACB=90°. Find the length of line AB.
问题：如图所示，Div(LengthOfLine(BC)=LengthOfLine(AC))，BC=1，∠ACB=90°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(Div(LengthOfLine(BC),LengthOfLine(AC)),1/2)
Equal(LengthOfLine(BC),1)
Equal(MeasureOfAngle(ACB),90)
Goal: Value(LengthOfLine(AB))
Answer: sqrt(5)
Theorem sequence:
right_triangle_judgment_angle(1,ACB)
right_triangle_property_pythagorean(1,ACB)
Problem: As shown in the diagram, CE=5, ∠ABC=150°, ∠BEC=90°. Find the length of line BC.
问题：如图所示，CE=5，∠ABC=150°，∠BEC=90°。求直线BC的长度。
Construction (CDL):
Shape(AB,BC)
Shape(DC,CB)
Shape(CB,BE,EC)
Collinear(ABE)
Conditions (CDL):
Equal(LengthOfLine(CE),5)
Equal(MeasureOfAngle(ABC),150)
Equal(MeasureOfAngle(BEC),90)
Goal: Value(LengthOfLine(BC))
Answer: 10
Theorem sequence:
adjacent_complementary_angle(1,ABC,CBE)
sine_theorem(1,CBE)
Problem: As shown in the diagram, BD=6, ∠BDE=90°, ∠EBD=15°. Find the length of line DE.
问题：如图所示，BD=6，∠BDE=90°，∠EBD=15°。求直线DE的长度。
Construction (CDL):
Shape(BD,DE,EB)
Conditions (CDL):
Equal(LengthOfLine(BD),6)
Equal(MeasureOfAngle(BDE),90)
Equal(MeasureOfAngle(EBD),15)
Goal: Value(LengthOfLine(DE))
Answer: 12-6*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BDE)
sine_theorem(1,DEB)
Problem: As shown in the diagram, BC=5, ∠BCA=90°, ∠CAB=30°. Find the length of line AB.
问题：如图所示，BC=5，∠BCA=90°，∠CAB=30°。求直线AB的长度。
Construction (CDL):
Shape(BC,CA,AB)
Conditions (CDL):
Equal(LengthOfLine(BC),5)
Equal(MeasureOfAngle(BCA),90)
Equal(MeasureOfAngle(CAB),30)
Goal: Value(LengthOfLine(AB))
Answer: 10
Theorem sequence:
sine_theorem(1,BCA)
Problem: As shown in the diagram, AC=13, BC=5, ∠ABC=90°. Find the value of tan(CA).
问题：如图所示，AC=13，BC=5，∠ABC=90°。求tan(CA)的值。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AC),13)
Equal(LengthOfLine(BC),5)
Equal(MeasureOfAngle(ABC),90)
Goal: Value(Tan(MeasureOfAngle(CAB)))
Answer: 5/12
Theorem sequence:
sine_theorem(1,CAB)
Problem: As shown in the diagram, the area of △ADE is 4, D is the midpoint of segment AB, E is the midpoint of segment AC. Find the area of △ABC.
问题：如图所示，△ADE的面积为4，D是线段AB的中点，E是线段AC的中点。求三角形ABC的面积。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ADE),4)
IsMidpointOfLine(D,AB)
IsMidpointOfLine(E,AC)
Goal: Value(AreaOfTriangle(ABC))
Answer: 16
Theorem sequence:
line_addition(1,AD,DB)
line_addition(1,AE,EC)
similar_triangle_judgment_sas(1,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_area_square_ratio(1,ADE,ABC)