SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, AD=120, ∠ADB=90°, ∠BAD=30°, ∠CDA=90°, ∠DAC=60°. Find the length of line BC.
问题：如图所示，AD=120，∠ADB=90°，∠BAD=30°，∠CDA=90°，∠DAC=60°。求直线BC的长度。
Construction (CDL):
Shape(BA,AD,DB)
Shape(DA,AC,CD)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AD),120)
Equal(MeasureOfAngle(ADB),90)
Equal(MeasureOfAngle(BAD),30)
Equal(MeasureOfAngle(CDA),90)
Equal(MeasureOfAngle(DAC),60)
Goal: Value(LengthOfLine(BC))
Answer: 160*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BAD)
triangle_property_angle_sum(1,DAC)
triangle_property_angle_sum(1,BAC)
sine_theorem(1,ADB)
sine_theorem(1,BAC)
Problem: As shown in the diagram, BC=50, CD=3/2, CE=2, ∠ECB=90°. Find the ratio of the length of line CE to the length of line BC.
问题：如图所示，BC=50，CD=3/2，CE=2，∠ECB=90°。求直线CE的长度与直线BC的长度之比。
Construction (CDL):
Shape(AB,BC,CD,DA)
Shape(AE,EB,BA)
Collinear(CBE)
Conditions (CDL):
Equal(LengthOfLine(BC),50)
Equal(LengthOfLine(CD),3/2)
Equal(LengthOfLine(CE),2)
Equal(MeasureOfAngle(ECB),90)
Goal: Value(Div(LengthOfLine(CE),LengthOfLine(BC)))
Answer: 1/25
Theorem sequence:
Problem: As shown in the diagram, AD=90, ∠ADB=90°, ∠BAD=30°, ∠CDA=90°, ∠DAC=60°. Find the length of line BC.
问题：如图所示，AD=90，∠ADB=90°，∠BAD=30°，∠CDA=90°，∠DAC=60°。求直线BC的长度。
Construction (CDL):
Shape(BA,AD,DB)
Shape(DA,AC,CD)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AD),90)
Equal(MeasureOfAngle(ADB),90)
Equal(MeasureOfAngle(BAD),30)
Equal(MeasureOfAngle(CDA),90)
Equal(MeasureOfAngle(DAC),60)
Goal: Value(LengthOfLine(BC))
Answer: 120*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BAD)
triangle_property_angle_sum(1,DAC)
triangle_property_angle_sum(1,BAC)
sine_theorem(1,ADB)
sine_theorem(1,BAC)
Problem: As shown in the diagram, Div(LengthOfLine(CE)=LengthOfLine(BE)), AE=1200, BE=450, ∠BEC=90°, ∠CAB=12°, ∠DAE=13°. Find the length of line CD.
问题：如图所示，Div(LengthOfLine(CE)=LengthOfLine(BE))，AE=1200，BE=450，∠BEC=90°，∠CAB=12°，∠DAE=13°。求直线CD的长度。
Construction (CDL):
Shape(CD,DA,AC)
Shape(CA,AB,BC)
Shape(CB,BE,EC)
Collinear(DCE)
Collinear(ABE)
Conditions (CDL):
Equal(Div(LengthOfLine(CE),LengthOfLine(BE)),8/15)
Equal(LengthOfLine(AE),1200)
Equal(LengthOfLine(BE),450)
Equal(MeasureOfAngle(BEC),90)
Equal(MeasureOfAngle(CAB),12)
Equal(MeasureOfAngle(DAE),13)
Goal: Value(LengthOfLine(CD))
Answer: -240+1200*tan(13*pi/180)
Theorem sequence:
line_addition(1,DC,CE)
triangle_property_angle_sum(1,DAE)
sine_theorem(1,EDA)
Problem: As shown in the diagram, AC=100, ∠ABC=30°, ∠BCA=90°. Find the length of line BC.
问题：如图所示，AC=100，∠ABC=30°，∠BCA=90°。求直线BC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AC),100)
Equal(MeasureOfAngle(ABC),30)
Equal(MeasureOfAngle(BCA),90)
Goal: Value(LengthOfLine(BC))
Answer: 100*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ABC)
sine_theorem(1,CAB)
Problem: As shown in the diagram, CD=20, DE=10, ∠BCA=60°, ∠BDF=30°, ∠CAB=90°, ∠DEC=90°, ∠DFB=90°. Find the length of line AB.
问题：如图所示，CD=20，DE=10，∠BCA=60°，∠BDF=30°，∠CAB=90°，∠DEC=90°，∠DFB=90°。求直线AB的长度。
Construction (CDL):
Shape(CD,DE,EC)
Shape(GD,DC,CG)
Shape(FG,GC,CA,AF)
Shape(BD,DG,GB)
Shape(BG,GF,FB)
Collinear(DGF)
Collinear(ECA)
Collinear(BGC)
Collinear(BFA)
Conditions (CDL):
Equal(LengthOfLine(CD),20)
Equal(LengthOfLine(DE),10)
Equal(MeasureOfAngle(BCA),60)
Equal(MeasureOfAngle(BDF),30)
Equal(MeasureOfAngle(CAB),90)
Equal(MeasureOfAngle(DEC),90)
Equal(MeasureOfAngle(DFB),90)
Goal: Value(LengthOfLine(AB))
Answer: 30
Theorem sequence:
right_triangle_judgment_angle(1,CAB)
right_triangle_property_pythagorean(1,CAB)
triangle_property_angle_sum(1,BDG)
triangle_property_angle_sum(1,BGF)
triangle_property_angle_sum(1,DCB)
triangle_property_angle_sum(1,CAB)
sine_theorem(1,DEC)
sine_theorem(1,BDG)
sine_theorem(1,BGF)
sine_theorem(1,DCB)
sine_theorem(1,BDC)
sine_theorem(1,CAB)
sine_theorem(1,BDF)
flat_angle(1,ECA)
angle_addition(1,ECB,BCA)
angle_addition(1,ECD,DCB)
Problem: As shown in the diagram, BC=30, ∠ACB=90°, ∠DAB=30°, ∠DAC=90°. Find the length of line AC.
问题：如图所示，BC=30，∠ACB=90°，∠DAB=30°，∠DAC=90°。求直线AC的长度。
Construction (CDL):
Shape(AC,CB,BA)
Shape(DA,AB)
Conditions (CDL):
Equal(LengthOfLine(BC),30)
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(DAB),30)
Equal(MeasureOfAngle(DAC),90)
Goal: Value(LengthOfLine(AC))
Answer: 10*sqrt(3)
Theorem sequence:
angle_addition(1,DAB,BAC)
sine_theorem(1,BAC)
cosine_theorem(1,ACB)
Problem: As shown in the diagram, AB=10, ∠BDC=90°, ∠CAB=30°, ∠CBD=60°. Find the length of line DC.
问题：如图所示，AB=10，∠BDC=90°，∠CAB=30°，∠CBD=60°。求直线DC的长度。
Construction (CDL):
Shape(CA,AB,BC)
Shape(CB,BD,DC)
Collinear(ABD)
Conditions (CDL):
Equal(LengthOfLine(AB),10)
Equal(MeasureOfAngle(BDC),90)
Equal(MeasureOfAngle(CAB),30)
Equal(MeasureOfAngle(CBD),60)
Goal: Value(LengthOfLine(DC))
Answer: 5*sqrt(3)
Theorem sequence:
adjacent_complementary_angle(1,ABC,CBD)
triangle_property_angle_sum(1,ABC)
isosceles_triangle_judgment_angle_equal(1,BCA)
sine_theorem(1,CBD)
Problem: As shown in the diagram, AD=60, ∠ACB=60°, ∠ADB=90°, ∠CBA=30°. Find the length of line BC.
问题：如图所示，AD=60，∠ACB=60°，∠ADB=90°，∠CBA=30°。求直线BC的长度。
Construction (CDL):
Shape(BA,AD,DB)
Shape(DA,AC,CD)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AD),60)
Equal(MeasureOfAngle(ACB),60)
Equal(MeasureOfAngle(ADB),90)
Equal(MeasureOfAngle(CBA),30)
Goal: Value(LengthOfLine(BC))
Answer: 80*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BAC)
sine_theorem(1,ADB)
sine_theorem(1,BAC)
Problem: As shown in the diagram, CD=1, DF=120, ∠ACE=30°, ∠AEG=60°, ∠EGA=90°, CDFE is a rectangle, quadrilateral EFBG is a rectangle. Find the length of line AB.
问题：如图所示，CD=1，DF=120，∠ACE=30°，∠AEG=60°，∠EGA=90°，四边形CDFE是矩形，EFBG是矩形。求直线AB的长度。
Construction (CDL):
Shape(AC,CE,EA)
Shape(AE,EG,GA)
Shape(CD,DF,FE,EC)
Shape(EF,FB,BG,GE)
Collinear(DFB)
Collinear(CEG)
Collinear(AGB)
Conditions (CDL):
Equal(LengthOfLine(CD),1)
Equal(LengthOfLine(DF),120)
Equal(MeasureOfAngle(ACE),30)
Equal(MeasureOfAngle(AEG),60)
Equal(MeasureOfAngle(EGA),90)
Rectangle(CDFE)
Rectangle(EFBG)
Goal: Value(LengthOfLine(AB))
Answer: 1+60*sqrt(3)
Theorem sequence:
parallelogram_property_opposite_line_equal(1,CDFE)
parallelogram_property_opposite_line_equal(1,DFEC)
parallelogram_property_opposite_line_equal(1,EFBG)
line_addition(1,AG,GB)
adjacent_complementary_angle(1,CEA,AEG)
triangle_property_angle_sum(1,ACE)
sine_theorem(1,CEA)
sine_theorem(1,ACG)
Problem: As shown in the diagram, BC=20, ∠ACB=37°, ∠CBA=90°. Find the length of line AB.
问题：如图所示，BC=20，∠ACB=37°，∠CBA=90°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(BC),20)
Equal(MeasureOfAngle(ACB),37)
Equal(MeasureOfAngle(CBA),90)
Goal: Value(LengthOfLine(AB))
Answer: 20*tan(37*pi/180)
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,BAC)
Problem: As shown in the diagram, ∠ACB=30°, ∠ADB=45°, ∠DBA=90°. Find the measure of ∠DAC.
问题：如图所示，∠ACB=30°，∠ADB=45°，∠DBA=90°。求∠DAC的大小。
Construction (CDL):
Shape(AC,CD,DA)
Shape(AD,DB,BA)
Collinear(CDB)
Conditions (CDL):
Equal(MeasureOfAngle(ACB),30)
Equal(MeasureOfAngle(ADB),45)
Equal(MeasureOfAngle(DBA),90)
Goal: Value(MeasureOfAngle(DAC))
Answer: 15
Theorem sequence:
triangle_property_angle_sum(1,ACD)
adjacent_complementary_angle(1,CDA,ADB)
Problem: As shown in the diagram, AB=12, ∠BDC=90°, ∠CAB=30°, ∠CBD=60°. Find the length of line CD.
问题：如图所示，AB=12，∠BDC=90°，∠CAB=30°，∠CBD=60°。求直线CD的长度。
Construction (CDL):
Shape(CA,AB,BC)
Shape(CB,BD,DC)
Collinear(ABD)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(MeasureOfAngle(BDC),90)
Equal(MeasureOfAngle(CAB),30)
Equal(MeasureOfAngle(CBD),60)
Goal: Value(LengthOfLine(CD))
Answer: 6*sqrt(3)
Theorem sequence:
adjacent_complementary_angle(1,ABC,CBD)
triangle_property_angle_sum(1,CAB)
sine_theorem(1,ABC)
sine_theorem(1,CAD)
Problem: As shown in the diagram, AD=120, ∠ACB=60°, ∠ADB=90°, ∠CBA=30°. Find the length of line BC.
问题：如图所示，AD=120，∠ACB=60°，∠ADB=90°，∠CBA=30°。求直线BC的长度。
Construction (CDL):
Shape(BA,AD,DB)
Shape(DA,AC,CD)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AD),120)
Equal(MeasureOfAngle(ACB),60)
Equal(MeasureOfAngle(ADB),90)
Equal(MeasureOfAngle(CBA),30)
Goal: Value(LengthOfLine(BC))
Answer: 160*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BAC)
sine_theorem(1,ADB)
sine_theorem(1,BAC)
Problem: As shown in the diagram, AC=100, ∠ACB=90°, ∠DAB=30°, ∠DAC=90°. Find the length of line BC.
问题：如图所示，AC=100，∠ACB=90°，∠DAB=30°，∠DAC=90°。求直线BC的长度。
Construction (CDL):
Shape(AC,CB,BA)
Shape(DA,AB)
Conditions (CDL):
Equal(LengthOfLine(AC),100)
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(DAB),30)
Equal(MeasureOfAngle(DAC),90)
Goal: Value(LengthOfLine(BC))
Answer: 100*sqrt(3)
Theorem sequence:
angle_addition(1,DAB,BAC)
triangle_property_angle_sum(1,ACB)
sine_theorem(1,CBA)
Problem: As shown in the diagram, AC=1200, ∠BAD=∠ABC, ∠BAD=α°, ∠BCA=90°, Tan(α)=5/12. Find the length of line AB.
问题：如图所示，AC=1200，∠BAD=∠ABC，∠BAD=α°，∠BCA=90°，Tan(α)=5/12。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(BA,AD)
Conditions (CDL):
Equal(LengthOfLine(AC),1200)
Equal(MeasureOfAngle(BAD),MeasureOfAngle(ABC))
Equal(MeasureOfAngle(BAD),α)
Equal(MeasureOfAngle(BCA),90)
Equal(Tan(α),5/12)
Goal: Value(LengthOfLine(AB))
Answer: 3120
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, AB=12, ∠ABC=90°, ∠CAB=60°. Find the length of line BC.
问题：如图所示，AB=12，∠ABC=90°，∠CAB=60°。求直线BC的长度。
Construction (CDL):
Shape(CA,AB,BC)
Conditions (CDL):
Equal(LengthOfLine(AB),12)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(CAB),60)
Goal: Value(LengthOfLine(BC))
Answer: (-36+24*sqrt(3))/sqrt(7-4*sqrt(3))
Theorem sequence:
sine_theorem(1,CAB)
sine_theorem(1,ABC)
cosine_theorem(1,CAB)
Problem: As shown in the diagram, AE=BE, BD=30, ∠ABD=90°, ∠BDE=90°, ∠EBD=30°. Find the length of line AB.
问题：如图所示，AE=BE，BD=30，∠ABD=90°，∠BDE=90°，∠EBD=30°。求直线AB的长度。
Construction (CDL):
Shape(AE,EC)
Shape(EA,AB,BE)
Shape(BD,DE,EB)
Collinear(CED)
Conditions (CDL):
Equal(LengthOfLine(AE),LengthOfLine(BE))
Equal(LengthOfLine(BD),30)
Equal(MeasureOfAngle(ABD),90)
Equal(MeasureOfAngle(BDE),90)
Equal(MeasureOfAngle(EBD),30)
Goal: Value(LengthOfLine(AB))
Answer: 20*sqrt(3)
Theorem sequence:
angle_addition(1,ABE,EBD)
triangle_property_angle_sum(1,EAB)
triangle_property_angle_sum(1,BDE)
sine_theorem(1,EAB)
sine_theorem(1,ABE)
sine_theorem(1,BDE)
Problem: As shown in the diagram, BC=10, ∠ABC=60°, ∠BCA=90°. Find the length of line AC.
问题：如图所示，BC=10，∠ABC=60°，∠BCA=90°。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(BC),10)
Equal(MeasureOfAngle(ABC),60)
Equal(MeasureOfAngle(BCA),90)
Goal: Value(LengthOfLine(AC))
Answer: (-30+20*sqrt(3))/sqrt(7-4*sqrt(3))
Theorem sequence:
sine_theorem(1,ABC)
sine_theorem(1,BCA)
cosine_theorem(1,ABC)
Problem: As shown in the diagram, CD=8, ∠ABC=30°, ∠CDA=90°, ∠DAC=60°, ∠ECD=90°. Find the length of line AB.
问题：如图所示，CD=8，∠ABC=30°，∠CDA=90°，∠DAC=60°，∠ECD=90°。求直线AB的长度。
Construction (CDL):
Shape(EC,CB)
Shape(BC,CA,AB)
Shape(CD,DA,AC)
Collinear(DAB)
Conditions (CDL):
Equal(LengthOfLine(CD),8)
Equal(MeasureOfAngle(ABC),30)
Equal(MeasureOfAngle(CDA),90)
Equal(MeasureOfAngle(DAC),60)
Equal(MeasureOfAngle(ECD),90)
Goal: Value(LengthOfLine(AB))
Answer: 16*sqrt(3)/3
Theorem sequence:
line_addition(1,DA,AB)
triangle_property_angle_sum(1,CDA)
triangle_property_angle_sum(1,BCD)
sine_theorem(1,DAC)
sine_theorem(1,DBC)
Problem: As shown in the diagram, ∠BDC=90°, ∠CAB=30°, ∠CBD=45°. Find the measure of ∠BCA.
问题：如图所示，∠BDC=90°，∠CAB=30°，∠CBD=45°。求∠BCA的大小。
Construction (CDL):
Shape(CA,AB,BC)
Shape(CB,BD,DC)
Collinear(ABD)
Conditions (CDL):
Equal(MeasureOfAngle(BDC),90)
Equal(MeasureOfAngle(CAB),30)
Equal(MeasureOfAngle(CBD),45)
Goal: Value(MeasureOfAngle(BCA))
Answer: 15
Theorem sequence:
angle_addition(1,DCB,BCA)
triangle_property_angle_sum(1,CBD)
triangle_property_angle_sum(1,CAD)
Problem: As shown in the diagram, BC=8, CD=2, ∠AED=90°, ∠EDA=35°, quadrilateral EBCD is a rectangle. Find the length of line AB.
问题：如图所示，BC=8，CD=2，∠AED=90°，∠EDA=35°，EBCD是矩形。求直线AB的长度。
Construction (CDL):
Shape(AE,ED,DA)
Shape(EB,BC,CD,DE)
Collinear(AEB)
Conditions (CDL):
Equal(LengthOfLine(BC),8)
Equal(LengthOfLine(CD),2)
Equal(MeasureOfAngle(AED),90)
Equal(MeasureOfAngle(EDA),35)
Rectangle(EBCD)
Goal: Value(LengthOfLine(AB))
Answer: 2+8*tan(7*pi/36)
Theorem sequence:
parallelogram_property_opposite_line_equal(1,EBCD)
parallelogram_property_opposite_line_equal(1,BCDE)
line_addition(1,AE,EB)
triangle_property_angle_sum(1,AED)
sine_theorem(1,EDA)
Problem: As shown in the diagram, PC=450, ∠APQ=30°, ∠BCP=90°, ∠PAB=30°, ∠PBC=60°. Find the length of line AB.
问题：如图所示，PC=450，∠APQ=30°，∠BCP=90°，∠PAB=30°，∠PBC=60°。求直线AB的长度。
Construction (CDL):
Shape(AP,PQ)
Shape(PA,AB,BP)
Shape(PB,BC,CP)
Collinear(ABC)
Conditions (CDL):
Equal(LengthOfLine(PC),450)
Equal(MeasureOfAngle(APQ),30)
Equal(MeasureOfAngle(BCP),90)
Equal(MeasureOfAngle(PAB),30)
Equal(MeasureOfAngle(PBC),60)
Goal: Value(LengthOfLine(AB))
Answer: 300*sqrt(3)
Theorem sequence:
line_addition(1,AB,BC)
triangle_property_angle_sum(1,PBC)
triangle_property_angle_sum(1,PAC)
sine_theorem(1,CPB)
sine_theorem(1,CPA)
Problem: As shown in the diagram, AC=100, ∠ABC=45°, ∠BCA=90°. Find the length of line AB.
问题：如图所示，AC=100，∠ABC=45°，∠BCA=90°。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AC),100)
Equal(MeasureOfAngle(ABC),45)
Equal(MeasureOfAngle(BCA),90)
Goal: Value(LengthOfLine(AB))
Answer: 100*sqrt(2)
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, AC=24, ∠ACB=90°, ∠BAC=30°. Find the length of line BC.
问题：如图所示，AC=24，∠ACB=90°，∠BAC=30°。求直线BC的长度。
Construction (CDL):
Shape(BA,AC,CB)
Conditions (CDL):
Equal(LengthOfLine(AC),24)
Equal(MeasureOfAngle(ACB),90)
Equal(MeasureOfAngle(BAC),30)
Goal: Value(LengthOfLine(BC))
Answer: 8*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BAC)
sine_theorem(1,CBA)
Problem: As shown in the diagram, AC=1200, ∠ABC=α°, ∠BAD=α°, ∠BCA=90°, α=30. Find the length of line AB.
问题：如图所示，AC=1200，∠ABC=α°，∠BAD=α°，∠BCA=90°，α=30。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(BA,AD)
Conditions (CDL):
Equal(LengthOfLine(AC),1200)
Equal(MeasureOfAngle(ABC),α)
Equal(MeasureOfAngle(BAD),α)
Equal(MeasureOfAngle(BCA),90)
Equal(α,30)
Goal: Value(LengthOfLine(AB))
Answer: 2400
Theorem sequence:
sine_theorem(1,ABC)
Problem: As shown in the diagram, AB=450, ∠ABC=90°, ∠BCA=60°, ∠BDA=30°. Find the length of line DC.
问题：如图所示，AB=450，∠ABC=90°，∠BCA=60°，∠BDA=30°。求直线DC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(AC,CD,DA)
Collinear(BCD)
Conditions (CDL):
Equal(LengthOfLine(AB),450)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(BCA),60)
Equal(MeasureOfAngle(BDA),30)
Goal: Value(LengthOfLine(DC))
Answer: 300*sqrt(3)
Theorem sequence:
line_addition(1,BC,CD)
triangle_property_angle_sum(1,ABC)
triangle_property_angle_sum(1,ABD)
sine_theorem(1,BCA)
sine_theorem(1,BDA)
Problem: As shown in the diagram, CD=12, ∠ABC=90°, ∠BCA=60°, ∠BDA=30°. Find the length of line AB.
问题：如图所示，CD=12，∠ABC=90°，∠BCA=60°，∠BDA=30°。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(AC,CD,DA)
Collinear(BCD)
Conditions (CDL):
Equal(LengthOfLine(CD),12)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(BCA),60)
Equal(MeasureOfAngle(BDA),30)
Goal: Value(LengthOfLine(AB))
Answer: 6*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ABC)
triangle_property_angle_sum(1,ABD)
angle_addition(1,DAC,CAB)
isosceles_triangle_judgment_angle_equal(1,CDA)
sine_theorem(1,ABC)
Problem: As shown in the diagram, BC=2, BF=8, ∠ABC=90°, ∠AFE=90°, ∠CAB=a°, Tan(a)=3/4. Find the length of line EF.
问题：如图所示，BC=2，BF=8，∠ABC=90°，∠AFE=90°，∠CAB=a°，Tan(a)=3/4。求直线EF的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(CB,BF,FE,EC)
Collinear(ACE)
Collinear(ABF)
Conditions (CDL):
Equal(LengthOfLine(BC),2)
Equal(LengthOfLine(BF),8)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(AFE),90)
Equal(MeasureOfAngle(CAB),a)
Equal(Tan(a),3/4)
Goal: Value(LengthOfLine(EF))
Answer: 8
Theorem sequence:
line_addition(1,AB,BF)
triangle_property_angle_sum(1,ABC)
triangle_property_angle_sum(1,AFE)
sine_theorem(1,BCA)
sine_theorem(1,FEA)
Problem: As shown in the diagram, BC=4, ∠ABC=90°, ∠BCA=60°. Find the length of line AB.
问题：如图所示，BC=4，∠ABC=90°，∠BCA=60°。求直线AB的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(BC),4)
Equal(MeasureOfAngle(ABC),90)
Equal(MeasureOfAngle(BCA),60)
Goal: Value(LengthOfLine(AB))
Answer: 4*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ABC)
sine_theorem(1,BCA)
Problem: As shown in the diagram, AC=10, ∠ADB=90°, ∠BAD=30°, ∠BCD=60°. Find the length of line BD.
问题：如图所示，AC=10，∠ADB=90°，∠BAD=30°，∠BCD=60°。求直线BD的长度。
Construction (CDL):
Shape(BA,AC,CB)
Shape(BC,CD,DB)
Collinear(ACD)
Conditions (CDL):
Equal(LengthOfLine(AC),10)
Equal(MeasureOfAngle(ADB),90)
Equal(MeasureOfAngle(BAD),30)
Equal(MeasureOfAngle(BCD),60)
Goal: Value(LengthOfLine(BD))
Answer: 5*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,BCD)
triangle_property_angle_sum(1,BAD)
angle_addition(1,DBC,CBA)
isosceles_triangle_judgment_angle_equal(1,CBA)
sine_theorem(1,BCD)
Problem: As shown in the diagram, AC=10, ∠ACB=60°, ∠BAC=90°. Find the length of line AB.
问题：如图所示，AC=10，∠ACB=60°，∠BAC=90°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(AC),10)
Equal(MeasureOfAngle(ACB),60)
Equal(MeasureOfAngle(BAC),90)
Goal: Value(LengthOfLine(AB))
Answer: 10*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,ACB)
Problem: As shown in the diagram, BC=10, ∠ACB=50°, ∠CBA=90°. Find the length of line AB.
问题：如图所示，BC=10，∠ACB=50°，∠CBA=90°。求直线AB的长度。
Construction (CDL):
Shape(AC,CB,BA)
Conditions (CDL):
Equal(LengthOfLine(BC),10)
Equal(MeasureOfAngle(ACB),50)
Equal(MeasureOfAngle(CBA),90)
Goal: Value(LengthOfLine(AB))
Answer: 10/tan(2*pi/9)
Theorem sequence:
triangle_property_angle_sum(1,ACB)
sine_theorem(1,BAC)
Problem: As shown in the diagram, AB=2, ∠BCA=30°, ∠CAB=90°. Find the length of line AC.
问题：如图所示，AB=2，∠BCA=30°，∠CAB=90°。求直线AC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Conditions (CDL):
Equal(LengthOfLine(AB),2)
Equal(MeasureOfAngle(BCA),30)
Equal(MeasureOfAngle(CAB),90)
Goal: Value(LengthOfLine(AC))
Answer: 2*sqrt(3)
Theorem sequence:
triangle_property_angle_sum(1,ABC)
sine_theorem(1,ABC)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(AB)), Div(LengthOfLine(AF)=LengthOfLine(AC)), AB=AC, EF=60, Tan(MeasureOfAngle(DCA))=5/2, AD is the altitude of △ ABC, AG is the altitude of △ AEF. Find the length of line AD.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AB))，Div(LengthOfLine(AF)=LengthOfLine(AC))，AB=AC，EF=60，Tan(MeasureOfAngle(DCA))=5/2，AD是三角形ABC的高，AG是△AEF的高。求直线AD的长度。
Construction (CDL):
Shape(AE,EG,GA)
Shape(AG,GF,FA)
Shape(EB,BD,DG,GE)
Shape(GD,DC,CF,FG)
Collinear(AEB)
Collinear(AFC)
Collinear(EGF)
Collinear(BDC)
Collinear(AGD)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(AB)),5/12)
Equal(Div(LengthOfLine(AF),LengthOfLine(AC)),5/12)
Equal(LengthOfLine(AB),LengthOfLine(AC))
Equal(LengthOfLine(EF),60)
Equal(Tan(MeasureOfAngle(DCA)),5/2)
IsAltitudeOfTriangle(AD,ABC)
IsAltitudeOfTriangle(AG,AEF)
Goal: Value(LengthOfLine(AD))
Answer: 180
Theorem sequence:
isosceles_triangle_judgment_line_equal(1,AEF)
isosceles_triangle_judgment_line_equal(1,ABC)
isosceles_triangle_property_angle_equal(1,ABC)
isosceles_triangle_property_line_coincidence(1,AEF,G)
line_addition(1,EG,GF)
triangle_property_angle_sum(1,ABD)
sine_theorem(1,EGA)
sine_theorem(1,ABD)
Problem: As shown in the diagram, AB=7, AD=10, CM=4, AD and BC are opposite sides of the parallelogram ABCD. Find the length of line DN.
问题：如图所示，AB=7，AD=10，CM=4，AD和BC是平行四边形ABCD的一组对边。求直线DN的长度。
Construction (CDL):
Shape(AB,BP,PA)
Shape(AP,PD,DA)
Shape(DP,PN,ND)
Shape(PB,BC,CN,NP)
Shape(NC,CM,MN)
Collinear(BPD)
Collinear(APNM)
Collinear(DNC)
Collinear(BCM)
Conditions (CDL):
Equal(LengthOfLine(AB),7)
Equal(LengthOfLine(AD),10)
Equal(LengthOfLine(CM),4)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(DN))
Answer: 5
Theorem sequence:
parallel_property_collinear_extend(1,CB,DA,M)
parallelogram_property_opposite_line_equal(1,ABCD)
line_addition(1,DN,NC)
parallel_property_alternate_interior_angle(1,MC,DA)
parallel_property_alternate_interior_angle(2,MC,DA)
similar_triangle_judgment_aa(1,NDA,NCM)
similar_triangle_property_line_ratio(1,NDA,NCM)
similar_triangle_property_line_ratio(1,AND,MNC)
Problem: As shown in the diagram, ∠BCA=70°, the center of circle O is O, PA is the tangent to ⊙O, PB is the tangent to circle O. Find the measure of ∠APB.
问题：如图所示，∠BCA=70°，⊙O的圆心为O，圆O的切线为PA，PB是⊙O的切线。求∠APB的大小。
Construction (CDL):
Shape(AP,PB,OAB)
Shape(BO,OA,OAB)
Shape(AO,OB,BC,CA)
Shape(CB,OBC)
Shape(AC,OCA)
Cocircular(O,ABC)
Conditions (CDL):
Equal(MeasureOfAngle(BCA),70)
IsCentreOfCircle(O,O)
IsTangentOfCircle(PA,O)
IsTangentOfCircle(PB,O)
Goal: Value(MeasureOfAngle(APB))
Answer: 40
Theorem sequence:
arc_property_center_angle(1,OAB,O)
arc_property_circumference_angle_external(1,OAB,C)
tangent_of_circle_property_perpendicular(1,PA,O,O)
tangent_of_circle_property_perpendicular(2,PB,O,O)
quadrilateral_property_angle_sum(1,APBO)
Problem: As shown in the diagram, ∠CAB=25°, the center of circle O is O, AB is the diameter of circle O, the tangent to ⊙O is DC. Find the measure of ∠BDC.
问题：如图所示，∠CAB=25°，圆O的圆心为O，AB是圆O的直径，DC是圆O的切线。求∠BDC的大小。
Construction (CDL):
Shape(AO,OB,BC,CA)
Shape(BO,OA,OAB)
Shape(AC,OCA)
Shape(CB,OBC)
Shape(BD,DC,OBC)
Collinear(AOBD)
Cocircular(O,ABC)
Conditions (CDL):
Equal(MeasureOfAngle(CAB),25)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AB,O)
IsTangentOfCircle(DC,O)
Goal: Value(MeasureOfAngle(BDC))
Answer: 40
Theorem sequence:
angle_addition(1,DCB,BCA)
arc_property_circumference_angle_external(1,OBC,A)
diameter_of_circle_property_right_angle(1,BCA,O)
triangle_property_angle_sum(1,CAD)
circle_property_angle_of_osculation(2,OBC,D)
Problem: As shown in the diagram, ∠BPA=50°, the center of circle O is O, AC is the diameter of ⊙O, the tangent to ⊙O is PA, PB is the tangent to ⊙O. Find the measure of ∠BOC.
问题：如图所示，∠BPA=50°，圆O的圆心为O，AC是圆O的直径，PA是圆O的切线，PB是圆O的切线。求∠BOC的大小。
Construction (CDL):
Shape(AO,OB,BA)
Shape(BO,OC,OCB)
Shape(CO,OA,OAC)
Shape(AB,OBA)
Shape(BP,PA,OBA)
Collinear(AOC)
Cocircular(O,ACB)
Conditions (CDL):
Equal(MeasureOfAngle(BPA),50)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AC,O)
IsTangentOfCircle(PA,O)
IsTangentOfCircle(PB,O)
Goal: Value(MeasureOfAngle(BOC))
Answer: 50
Theorem sequence:
tangent_of_circle_property_perpendicular(2,PA,O,O)
tangent_of_circle_property_perpendicular(1,PB,O,O)
quadrilateral_property_angle_sum(1,AOBP)
adjacent_complementary_angle(1,AOB,BOC)
Problem: As shown in the diagram, OA=10, OC=6, the center of circle N is O, OC is the perpendicular bisector of AB, AC is the tangent to ⊙O. Find the length of line AB.
问题：如图所示，OA=10，OC=6，⊙N的圆心为O，OC是AB的垂直平分线，AC是圆O的切线。求直线AB的长度。
Construction (CDL):
Shape(BC,CA,OAB)
Shape(CO,OD,ODC)
Shape(DA,AC,ODC)
Collinear(ODA)
Collinear(ACB)
Cocircular(O,AB)
Cocircular(N,DC)
Conditions (CDL):
Equal(LengthOfLine(OA),10)
Equal(LengthOfLine(OC),6)
IsCentreOfCircle(O,N)
IsPerpendicularBisectorOfLine(OC,AB)
IsTangentOfCircle(AC,O)
Goal: Value(LengthOfLine(AB))
Answer: 16
Theorem sequence:
right_triangle_judgment_angle(1,ACO)
right_triangle_property_pythagorean(1,ACO)
line_addition(1,AC,CB)
Problem: As shown in the diagram, the diameter of circle O is 8, AB=10, OB=OA, O is the center of ⊙O, AC is the tangent to ⊙O, BC is the tangent to ⊙O. Find the length of line OA.
问题：如图所示，⊙O的直径为8，AB=10，OB=OA，O是⊙O的圆心，⊙O的切线为AC，BC是⊙O的切线。求直线OA的长度。
Construction (CDL):
Shape(EO,OC,OCE)
Shape(CO,OD,ODC)
Shape(DA,AC,ODC)
Shape(CB,BE,OCE)
Collinear(ADO)
Collinear(BEO)
Collinear(ACB)
Cocircular(O,DCE)
Conditions (CDL):
Equal(DiameterOfCircle(O),8)
Equal(LengthOfLine(AB),10)
Equal(LengthOfLine(OB),LengthOfLine(OA))
IsCentreOfCircle(O,O)
IsTangentOfCircle(AC,O)
IsTangentOfCircle(BC,O)
Goal: Value(LengthOfLine(OA))
Answer: sqrt(41)
Theorem sequence:
line_addition(1,AC,CB)
circle_property_length_of_radius_and_diameter(1,O)
tangent_of_circle_property_perpendicular(2,AC,O,O)
radius_of_circle_property_length_equal(1,OC,O)
altitude_of_triangle_judgment(1,OC,OAB)
isosceles_triangle_judgment_line_equal(1,OAB)
isosceles_triangle_property_line_coincidence(1,OAB,C)
cosine_theorem(1,COA)