SunnyLin/FormalGeo7k_v1 huggingface dataset:
Problem: As shown in the diagram, ∠CAB=45°, the radius of ⊙A is 2, the center of circle A is A. Find the area of the sector ABC.
问题：如图所示，∠CAB=45°，⊙A的半径为2，圆A的圆心为A。求扇形ABC的面积。
Construction (CDL):
Shape(CA,AB,ABC)
Shape(BA,AC,ACB)
Cocircular(A,BC)
Conditions (CDL):
Equal(MeasureOfAngle(CAB),45)
Equal(RadiusOfCircle(A),2)
IsCentreOfCircle(A,A)
Goal: Value(AreaOfSector(ABC))
Answer: pi/2
Theorem sequence:
arc_property_center_angle(1,ABC,A)
sector_area_formula(1,ABC)
Problem: As shown in the diagram, the radius of ⊙O is 1, the center of circle O is O. Find the area of the circle O.
问题：如图所示，⊙O的半径为1，⊙O的圆心为O。求⊙O的面积。
Construction (CDL):
Shape(O)
Cocircular(O)
Conditions (CDL):
Equal(RadiusOfCircle(O),1)
IsCentreOfCircle(O,O)
Goal: Value(AreaOfCircle(O))
Answer: pi
Theorem sequence:
circle_area_formula(1,O)
Problem: As shown in the diagram, the radius of ⊙O is 2, the center of ⊙O is O. Find the area of the circle O.
问题：如图所示，圆O的半径为2，O是⊙O的圆心。求圆O的面积。
Construction (CDL):
Shape(O)
Cocircular(O)
Conditions (CDL):
Equal(RadiusOfCircle(O),2)
IsCentreOfCircle(O,O)
Goal: Value(AreaOfCircle(O))
Answer: 4*pi
Theorem sequence:
circle_area_formula(1,O)
Problem: As shown in the diagram, the measure of arc ABD is 90, the measure of ⌒OBA is 180, the radius of ⊙A is 4, the radius of circle O is 2, A is the center of circle A, the center of ⊙O is O. Find the area of the sector ABD minus the area of the sector OBA.
问题：如图所示，弧ABD的角度为90，弧OBA的角度为180，圆A的半径为4，⊙O的半径为2，A是圆A的圆心，⊙O的圆心为O。求扇形ABD的面积减去扇形OBA的面积。
Construction (CDL):
Shape(AD,ADB,OAB)
Shape(BO,OA,OAB)
Shape(AO,OB,OBA)
Shape(OBA,AD,ABD)
Collinear(AOB)
Cocircular(A,BD)
Cocircular(O,AB)
Conditions (CDL):
Equal(MeasureOfArc(ABD),90)
Equal(MeasureOfArc(OBA),180)
Equal(RadiusOfCircle(A),4)
Equal(RadiusOfCircle(O),2)
IsCentreOfCircle(A,A)
IsCentreOfCircle(O,O)
Goal: Value(Sub(AreaOfSector(ABD),AreaOfSector(OBA)))
Answer: 2*pi
Theorem sequence:
sector_area_formula(1,ABD)
sector_area_formula(1,OBA)
Problem: As shown in the diagram, AD=5, BD=10, DE=6, DE∥BC. Find the length of line BC.
问题：如图所示，AD=5，BD=10，DE=6，DE平行于BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AD),5)
Equal(LengthOfLine(BD),10)
Equal(LengthOfLine(DE),6)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 18
Theorem sequence:
line_addition(1,AD,DB)
parallel_property_corresponding_angle(1,DE,BC,A)
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, BC=3, CA=1, EC=2, ∠ABD=∠ACE. Find the length of line BD.
问题：如图所示，BC=3，CA=1，EC=2，∠ABD=∠ACE。求直线BD的长度。
Construction (CDL):
Shape(EA,AC,CE)
Shape(DE,EC,CB,BD)
Collinear(DEA)
Collinear(BCA)
Conditions (CDL):
Equal(LengthOfLine(BC),3)
Equal(LengthOfLine(CA),1)
Equal(LengthOfLine(EC),2)
Equal(MeasureOfAngle(ABD),MeasureOfAngle(ACE))
Goal: Value(LengthOfLine(BD))
Answer: 8
Theorem sequence:
line_addition(1,AC,CB)
similar_triangle_judgment_aa(1,EAC,DAB)
similar_triangle_property_line_ratio(1,EAC,DAB)
similar_triangle_property_line_ratio(1,ACE,ABD)
Problem: As shown in the diagram, AC=y, AD=6, AE=x, DB=3, DE∥BC. Find the value of x/y.
问题：如图所示，AC=y，AD=6，AE=x，DB=3，DE平行于BC。求x/y的值。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AC),y)
Equal(LengthOfLine(AD),6)
Equal(LengthOfLine(AE),x)
Equal(LengthOfLine(DB),3)
ParallelBetweenLine(DE,BC)
Goal: Value(x/y)
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,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AC=9, AD=4, AE=3, DE is parallel to BC. Find the length of line AB.
问题：如图所示，AC=9，AD=4，AE=3，DE平行于BC。求直线AB的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AC),9)
Equal(LengthOfLine(AD),4)
Equal(LengthOfLine(AE),3)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AB))
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,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(BD)), AD=4, AE=2, DE is parallel to BC. Find the length of line EC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(BD))，AD=4，AE=2，DE平行于BC。求直线EC的长度。
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(LengthOfLine(AD),4)
Equal(LengthOfLine(AE),2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(EC))
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,ADE,ABC)
line_addition(1,AD,DB)
line_addition(1,AE,EC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, AO=2, BO=3, DO=4, AB∥CD. Find the length of line BC.
问题：如图所示，AO=2，BO=3，DO=4，AB平行于CD。求直线BC的长度。
Construction (CDL):
Shape(AO,OB,BA)
Shape(OC,CD,DO)
Collinear(AOD)
Collinear(BOC)
Conditions (CDL):
Equal(LengthOfLine(AO),2)
Equal(LengthOfLine(BO),3)
Equal(LengthOfLine(DO),4)
ParallelBetweenLine(AB,CD)
Goal: Value(LengthOfLine(BC))
Answer: 9
Theorem sequence:
parallel_property_alternate_interior_angle(1,AB,CD)
parallel_property_alternate_interior_angle(2,AB,CD)
similar_triangle_judgment_aa(1,OBA,OCD)
similar_triangle_property_line_ratio(1,BAO,CDO)
similar_triangle_property_line_ratio(1,AOB,DOC)
line_addition(1,BO,OC)
Problem: As shown in the diagram, BA=9, BD=6, BE=4, ED is parallel to CA. Find the length of line EC.
问题：如图所示，BA=9，BD=6，BE=4，ED∥CA。求直线EC的长度。
Construction (CDL):
Shape(BE,ED,DB)
Shape(AD,DE,EC,CA)
Collinear(BDA)
Collinear(BEC)
Conditions (CDL):
Equal(LengthOfLine(BA),9)
Equal(LengthOfLine(BD),6)
Equal(LengthOfLine(BE),4)
ParallelBetweenLine(ED,CA)
Goal: Value(LengthOfLine(EC))
Answer: 2
Theorem sequence:
parallel_property_corresponding_angle(1,ED,CA,B)
parallel_property_corresponding_angle(2,AC,DE,B)
similar_triangle_judgment_aa(1,BED,BCA)
similar_triangle_property_line_ratio(1,EDB,CAB)
similar_triangle_property_line_ratio(1,DBE,ABC)
line_addition(1,BE,EC)
Problem: As shown in the diagram, AB=2, AE=4, BC=1, CD=3, BE∥CF, BE is parallel to DG, CF∥DG. Find the length of line EG.
问题：如图所示，AB=2，AE=4，BC=1，CD=3，BE平行于CF，BE平行于DG，CF∥DG。求直线EG的长度。
Construction (CDL):
Shape(AB,BE,EA)
Shape(BC,CF,FE,EB)
Shape(CD,DG,GF,FC)
Collinear(ABCD)
Collinear(AEFG)
Conditions (CDL):
Equal(LengthOfLine(AB),2)
Equal(LengthOfLine(AE),4)
Equal(LengthOfLine(BC),1)
Equal(LengthOfLine(CD),3)
ParallelBetweenLine(BE,CF)
ParallelBetweenLine(BE,DG)
ParallelBetweenLine(CF,DG)
Goal: Value(LengthOfLine(EG))
Answer: 8
Theorem sequence:
parallel_property_corresponding_angle(1,BE,DG,A)
similar_triangle_judgment_aa(1,EAB,GAD)
line_addition(1,AB,BC)
line_addition(1,AC,CD)
similar_triangle_property_line_ratio(1,EAB,GAD)
similar_triangle_property_line_ratio(1,BEA,DGA)
line_addition(1,AE,EG)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), AE=3, EC=6, DE∥BC. Find the value of x.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，AE=3，EC=6，DE∥BC。求x的值。
Construction (CDL):
Shape(AD,DE,EA)
Shape(ED,DB,BC,CE)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AD),LengthOfLine(AB)),x)
Equal(LengthOfLine(AE),3)
Equal(LengthOfLine(EC),6)
ParallelBetweenLine(DE,BC)
Goal: Value(x)
Answer: 1/3
Theorem sequence:
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_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(AB)), AE=2, DE∥BC. Find the length of line AC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(AB))，AE=2，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(AB)),1/2)
Equal(LengthOfLine(AE),2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(AC))
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,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AE)=LengthOfLine(AB)), M is the midpoint of segment AC, BE is parallel to CP, EA is parallel to CP. Find the ratio of the length of line BC to the length of line CD.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(AB))，M是线段AC的中点，BE∥CP，EA∥CP。求直线BC的长度与直线CD的长度之比。
Construction (CDL):
Shape(AE,EM,MA)
Shape(EB,BC,CM,ME)
Shape(MC,CP,PM)
Shape(PC,CD,DP)
Collinear(AEB)
Collinear(AMC)
Collinear(EMPD)
Collinear(BCD)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(AB)),1/4)
IsMidpointOfLine(M,AC)
ParallelBetweenLine(BE,CP)
ParallelBetweenLine(EA,CP)
Goal: Value(Div(LengthOfLine(BC),LengthOfLine(CD)))
Answer: 2
Theorem sequence:
line_addition(1,BC,CD)
line_addition(1,AE,EB)
parallel_property_alternate_interior_angle(1,EA,CP)
parallel_property_alternate_interior_angle(2,EA,CP)
similar_triangle_judgment_aa(1,MAE,MCP)
similar_triangle_property_line_ratio(1,MAE,MCP)
similar_triangle_property_line_ratio(1,EMA,PMC)
parallel_property_corresponding_angle(2,BE,CP,D)
similar_triangle_judgment_aa(1,PCD,EBD)
similar_triangle_property_line_ratio(1,PCD,EBD)
similar_triangle_property_line_ratio(1,DPC,DEB)
Problem: As shown in the diagram, AB=3, BC=4, BM=1, MN is perpendicular to DN, quadrilateral ADCB is a rectangle. Find the length of line DN.
问题：如图所示，AB=3，BC=4，BM=1，MN⊥DN，四边形ADCB是长方形。求直线DN的长度。
Construction (CDL):
Shape(AN,NM,MB,BA)
Shape(AD,DN,NA)
Shape(ND,DM,MN)
Shape(MD,DC,CM)
Collinear(ANM)
Collinear(BMC)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BC),4)
Equal(LengthOfLine(BM),1)
PerpendicularBetweenLine(MN,DN)
Rectangle(ADCB)
Goal: Value(LengthOfLine(DN))
Answer: 6*sqrt(10)/5
Theorem sequence:
line_addition(1,BM,MC)
line_addition(1,AN,NM)
parallelogram_property_opposite_line_equal(1,ADCB)
parallelogram_property_opposite_line_equal(1,DCBA)
adjacent_complementary_angle(1,MND,DNA)
right_triangle_judgment_angle(1,MBA)
right_triangle_judgment_angle(1,MND)
right_triangle_judgment_angle(1,DCM)
right_triangle_judgment_angle(1,DNA)
right_triangle_property_pythagorean(1,DCM)
right_triangle_property_pythagorean(1,MBA)
right_triangle_property_pythagorean(1,MND)
right_triangle_property_pythagorean(1,DNA)
Problem: As shown in the diagram, AC=8, BC=16, ∠ABD=∠CAD. Find the length of line CD.
问题：如图所示，AC=8，BC=16，∠ABD=∠CAD。求直线CD的长度。
Construction (CDL):
Shape(AB,BD,DA)
Shape(AD,DC,CA)
Collinear(BDC)
Conditions (CDL):
Equal(LengthOfLine(AC),8)
Equal(LengthOfLine(BC),16)
Equal(MeasureOfAngle(ABD),MeasureOfAngle(CAD))
Goal: Value(LengthOfLine(CD))
Answer: 4
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,DCA,ABC)
mirror_similar_triangle_property_line_ratio(1,DCA,ABC)
mirror_similar_triangle_property_line_ratio(1,ADC,BCA)
Problem: As shown in the diagram, Div(LengthOfLine(EC)=LengthOfLine(EA)), the perimeter of △ADE is 3, ED∥BC. Find the perimeter of △ABC.
问题：如图所示，Div(LengthOfLine(EC)=LengthOfLine(EA))，三角形ADE的周长为3，ED平行于BC。求△ABC的周长。
Construction (CDL):
Shape(EA,AD,DE)
Shape(AB,BC,CA)
Collinear(EAC)
Collinear(DAB)
Conditions (CDL):
Equal(Div(LengthOfLine(EC),LengthOfLine(EA)),3)
Equal(PerimeterOfTriangle(ADE),3)
ParallelBetweenLine(ED,BC)
Goal: Value(PerimeterOfTriangle(ABC))
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,ADE,ABC)
line_addition(1,EA,AC)
similar_triangle_property_line_ratio(1,DEA,BCA)
similar_triangle_property_perimeter_ratio(1,ADE,ABC)
Problem: As shown in the diagram, the area of △BED is 4, BE=2, CE=1, ED is parallel to CA. Find the area of triangle ABC.
问题：如图所示，△BED的面积为4，BE=2，CE=1，ED平行于CA。求三角形ABC的面积。
Construction (CDL):
Shape(BE,ED,DB)
Shape(DE,EC,CA,AD)
Collinear(BDA)
Collinear(BEC)
Conditions (CDL):
Equal(AreaOfTriangle(BED),4)
Equal(LengthOfLine(BE),2)
Equal(LengthOfLine(CE),1)
ParallelBetweenLine(ED,CA)
Goal: Value(AreaOfTriangle(ABC))
Answer: 9
Theorem sequence:
parallel_property_corresponding_angle(1,ED,CA,B)
parallel_property_corresponding_angle(2,AC,DE,B)
similar_triangle_judgment_aa(1,BED,BCA)
line_addition(1,BE,EC)
similar_triangle_property_line_ratio(1,DBE,ABC)
similar_triangle_property_area_square_ratio(1,BED,BCA)
Problem: As shown in the diagram, the area of △BED is 3, Div(AreaOfTriangle(DEO)=AreaOfTriangle(AOC)), ED is parallel to CA. Find the area of △ABC.
问题：如图所示，三角形BED的面积为3，Div(AreaOfTriangle(DEO)=AreaOfTriangle(AOC))，ED平行于CA。求三角形ABC的面积。
Construction (CDL):
Shape(AD,DO,OA)
Shape(AO,OC,CA)
Shape(DB,BE,ED)
Shape(DE,EO,OD)
Shape(OE,EC,CO)
Collinear(ADB)
Collinear(AOE)
Collinear(DOC)
Collinear(BEC)
Conditions (CDL):
Equal(AreaOfTriangle(BED),3)
Equal(Div(AreaOfTriangle(DEO),AreaOfTriangle(AOC)),1/9)
ParallelBetweenLine(ED,CA)
Goal: Value(AreaOfTriangle(ABC))
Answer: 27
Theorem sequence:
parallel_property_alternate_interior_angle(1,ED,CA)
parallel_property_alternate_interior_angle(2,ED,CA)
similar_triangle_judgment_aa(1,ODE,OCA)
similar_triangle_property_area_square_ratio(1,ODE,OCA)
similar_triangle_property_line_ratio(1,ODE,OCA)
parallel_property_corresponding_angle(1,ED,CA,B)
similar_triangle_judgment_aa(1,DBE,ABC)
similar_triangle_property_line_ratio(1,BED,BCA)
similar_triangle_property_area_square_ratio(1,DBE,ABC)
Problem: As shown in the diagram, ∠DAB=20°, triangle ABC is similar to triangle ADE.. Find the measure of ∠EAC.
问题：如图所示，∠DAB=20°，三角形ABC相似于三角形ADE。求∠EAC的大小。
Construction (CDL):
Shape(BF,FA,AB)
Shape(AF,FC,CA)
Shape(AC,CE,EA)
Shape(FB,BD,DF)
Shape(FD,DE,EC,CF)
Collinear(BFC)
Collinear(AFD)
Conditions (CDL):
Equal(MeasureOfAngle(DAB),20)
SimilarBetweenTriangle(ABC,ADE)
Goal: Value(MeasureOfAngle(EAC))
Answer: 20
Theorem sequence:
similar_triangle_property_angle_equal(1,ABC,ADE)
angle_addition(1,EAC,CAD)
angle_addition(1,CAD,DAB)
Problem: As shown in the diagram, CD=4, DE=2, AD is the angle bisector of ∠CAB, O is the center of circle O, the diameter of circle O is AB. Find the length of line AE.
问题：如图所示，CD=4，DE=2，AD平分∠CAB，O是圆O的圆心，⊙O的直径为AB。求直线AE的长度。
Construction (CDL):
Shape(AC,OCA)
Shape(CA,AE,EC)
Shape(CE,ED,DC)
Shape(CD,ODC)
Shape(DE,EB,OBD)
Shape(EA,AB,BE)
Shape(BA,OAB)
Collinear(AED)
Collinear(CEB)
Cocircular(O,CABD)
Conditions (CDL):
Equal(LengthOfLine(CD),4)
Equal(LengthOfLine(DE),2)
IsBisectorOfAngle(AD,CAB)
IsCentreOfCircle(O,O)
IsDiameterOfCircle(AB,O)
Goal: Value(LengthOfLine(AE))
Answer: 6
Theorem sequence:
arc_property_circumference_angle_external(1,OBD,C)
arc_property_circumference_angle_external(1,OBD,A)
mirror_similar_triangle_judgment_aa(1,EDC,CAD)
line_addition(1,AE,ED)
mirror_similar_triangle_property_line_ratio(1,EDC,CAD)
mirror_similar_triangle_property_line_ratio(1,CED,ADC)
Problem: As shown in the diagram, AB=7, AC=5, AD=3, ED is parallel to CA. Find the length of line DE.
问题：如图所示，AB=7，AC=5，AD=3，ED∥CA。求直线DE的长度。
Construction (CDL):
Shape(DB,BE,ED)
Shape(AD,DE,EC,CA)
Collinear(ADB)
Collinear(BEC)
Conditions (CDL):
Equal(LengthOfLine(AB),7)
Equal(LengthOfLine(AC),5)
Equal(LengthOfLine(AD),3)
ParallelBetweenLine(ED,CA)
Goal: Value(LengthOfLine(DE))
Answer: 20/7
Theorem sequence:
line_addition(1,AD,DB)
parallel_property_corresponding_angle(1,ED,CA,B)
similar_triangle_judgment_aa(1,DBE,ABC)
similar_triangle_property_line_ratio(1,BED,BCA)
similar_triangle_property_line_ratio(1,EDB,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(FC)=LengthOfLine(EF)), ABCD is a ▱. Find the ratio of the length of line AE to the length of line ED.
问题：如图所示，Div(LengthOfLine(FC)=LengthOfLine(EF))，ABCD是平行四边形。求直线AE的长度与直线ED的长度之比。
Construction (CDL):
Shape(AB,BF,FE,EA)
Shape(EF,FD,DE)
Shape(DF,FC,CD)
Shape(FB,BC,CF)
Collinear(AED)
Collinear(BFD)
Collinear(EFC)
Conditions (CDL):
Equal(Div(LengthOfLine(FC),LengthOfLine(EF)),3)
Parallelogram(ABCD)
Goal: Value(Div(LengthOfLine(AE),LengthOfLine(ED)))
Answer: 2
Theorem sequence:
line_addition(1,AE,ED)
parallel_property_collinear_extend(3,AD,BC,E)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(1,ED,BC)
parallel_property_alternate_interior_angle(2,ED,BC)
similar_triangle_judgment_aa(1,FBC,FDE)
similar_triangle_judgment_aa(1,ABD,CDB)
similar_triangle_property_line_ratio(1,FBC,FDE)
similar_triangle_property_line_ratio(1,BCF,DEF)
similar_triangle_property_line_ratio(1,ABD,CDB)
similar_triangle_property_line_ratio(1,BDA,DBC)
Problem: As shown in the diagram, the area of △ABE is 4, Div(LengthOfLine(AE)=LengthOfLine(CE)), BA∥CD. Find the area of △DEC.
问题：如图所示，△ABE的面积为4，Div(LengthOfLine(AE)=LengthOfLine(CE))，BA平行于CD。求三角形DEC的面积。
Construction (CDL):
Shape(AB,BE,EA)
Shape(EB,BC,CE)
Shape(DE,EC,CD)
Collinear(BED)
Collinear(AEC)
Conditions (CDL):
Equal(AreaOfTriangle(ABE),4)
Equal(Div(LengthOfLine(AE),LengthOfLine(CE)),1/2)
ParallelBetweenLine(BA,CD)
Goal: Value(AreaOfTriangle(DEC))
Answer: 16
Theorem sequence:
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(2,BA,CD)
similar_triangle_judgment_aa(1,EAB,ECD)
similar_triangle_property_line_ratio(1,BEA,DEC)
similar_triangle_property_area_square_ratio(1,EAB,ECD)
Problem: As shown in the diagram, AB=3, BD=6, DE=6, BC∥DE. Find the length of line BC.
问题：如图所示，AB=3，BD=6，DE=6，BC平行于DE。求直线BC的长度。
Construction (CDL):
Shape(AB,BC,CA)
Shape(BD,DE,EC,CB)
Collinear(ABD)
Collinear(ACE)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(BD),6)
Equal(LengthOfLine(DE),6)
ParallelBetweenLine(BC,DE)
Goal: Value(LengthOfLine(BC))
Answer: 2
Theorem sequence:
line_addition(1,AB,BD)
parallel_property_corresponding_angle(1,BC,DE,A)
parallel_property_corresponding_angle(2,ED,CB,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(EC)), BC=12, DE∥BC. Find the length of line DE.
问题：如图所示，Div(LengthOfLine(AE)=LengthOfLine(EC))，BC=12，DE∥BC。求直线DE的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BF,FD)
Shape(ED,DF,FC,CE)
Collinear(ADB)
Collinear(AEC)
Collinear(BFC)
Conditions (CDL):
Equal(Div(LengthOfLine(AE),LengthOfLine(EC)),1/2)
Equal(LengthOfLine(BC),12)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(DE))
Answer: 4
Theorem sequence:
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,ADE,ABC)
similar_triangle_property_line_ratio(1,DEA,BCA)
Problem: As shown in the diagram, AB=3, AD=2, DE=4, DE is parallel to BC. Find the length of line BC.
问题：如图所示，AB=3，AD=2，DE=4，DE∥BC。求直线BC的长度。
Construction (CDL):
Shape(AD,DE,EA)
Shape(DB,BC,CE,ED)
Collinear(ADB)
Collinear(AEC)
Conditions (CDL):
Equal(LengthOfLine(AB),3)
Equal(LengthOfLine(AD),2)
Equal(LengthOfLine(DE),4)
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,ADE,ABC)
similar_triangle_property_line_ratio(1,EAD,CAB)
Problem: As shown in the diagram, Div(LengthOfLine(AO)=LengthOfLine(OB)), CO=6, AC is parallel to DB. Find the length of line DO.
问题：如图所示，Div(LengthOfLine(AO)=LengthOfLine(OB))，CO=6，AC平行于DB。求直线DO的长度。
Construction (CDL):
Shape(AO,OC,CA)
Shape(OD,DB,BO)
Collinear(AOB)
Collinear(COD)
Conditions (CDL):
Equal(Div(LengthOfLine(AO),LengthOfLine(OB)),2/5)
Equal(LengthOfLine(CO),6)
ParallelBetweenLine(AC,DB)
Goal: Value(LengthOfLine(DO))
Answer: 15
Theorem sequence:
parallel_property_alternate_interior_angle(1,AC,DB)
parallel_property_alternate_interior_angle(2,AC,DB)
similar_triangle_judgment_aa(1,ODB,OCA)
similar_triangle_property_line_ratio(1,DBO,CAO)
similar_triangle_property_line_ratio(1,BOD,AOC)
Problem: As shown in the diagram, AB=6, AC=5, ∠ADE=∠GCE, AG is the angle bisector of ∠CAB, D bisects segment AB. Find the ratio of the length of line AF to the length of line AG.
问题：如图所示，AB=6，AC=5，∠ADE=∠GCE，AG是∠CAB的角平分线，D是线段AB的中点。求直线AF的长度与直线AG的长度之比。
Construction (CDL):
Shape(AD,DF,FA)
Shape(AF,FE,EA)
Shape(DB,BG,GF,FD)
Shape(FG,GC,CE,EF)
Collinear(ADB)
Collinear(DFE)
Collinear(AFG)
Collinear(AEC)
Collinear(BGC)
Conditions (CDL):
Equal(LengthOfLine(AB),6)
Equal(LengthOfLine(AC),5)
Equal(MeasureOfAngle(ADE),MeasureOfAngle(GCE))
IsBisectorOfAngle(AG,CAB)
IsMidpointOfLine(D,AB)
Goal: Value(Div(LengthOfLine(AF),LengthOfLine(AG)))
Answer: 3/5
Theorem sequence:
mirror_similar_triangle_judgment_aa(1,FAD,GCA)
mirror_similar_triangle_judgment_aa(1,GCA,FAD)
mirror_similar_triangle_property_line_ratio(1,FAD,GCA)
mirror_similar_triangle_property_line_ratio(1,DFA,CAG)
mirror_similar_triangle_property_line_ratio(1,CAG,DFA)
line_addition(1,AD,DB)
Problem: As shown in the diagram, Div(LengthOfLine(AF)=LengthOfLine(EF)), AB=5, AE=5, BE=5, ∠BCD=120°, AD and BC are opposite sides of the ▱ ABCD. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AF)=LengthOfLine(EF))，AB=5，AE=5，BE=5，∠BCD=120°，BA和CD是▱ABCD的一组对边。求直线BC的长度。
Construction (CDL):
Shape(AB,BF,FA)
Shape(AF,FD,DA)
Shape(FB,BE,EF)
Shape(DF,FE,EC,CD)
Collinear(AFE)
Collinear(BFD)
Collinear(BEC)
Conditions (CDL):
Equal(Div(LengthOfLine(AF),LengthOfLine(EF)),2)
Equal(LengthOfLine(AB),5)
Equal(LengthOfLine(AE),5)
Equal(LengthOfLine(BE),5)
Equal(MeasureOfAngle(BCD),120)
Parallelogram(ABCD)
Goal: Value(LengthOfLine(BC))
Answer: 10
Theorem sequence:
parallelogram_property_opposite_line_equal(1,ABCD)
parallel_property_collinear_extend(3,CB,DA,E)
parallel_property_alternate_interior_angle(1,BA,CD)
parallel_property_alternate_interior_angle(1,EB,DA)
parallel_property_alternate_interior_angle(2,EB,DA)
similar_triangle_judgment_aa(1,FDA,FBE)
similar_triangle_judgment_aa(1,ABD,CDB)
similar_triangle_property_line_ratio(1,FDA,FBE)
similar_triangle_property_line_ratio(1,DAF,BEF)
similar_triangle_property_line_ratio(1,BDA,DBC)
similar_triangle_property_line_ratio(1,DAB,BCD)
Problem: As shown in the diagram, AF=3, E is the midpoint of segment AB, DC and AB are opposite sides of the ▱ DABC. Find the length of line FC.
问题：如图所示，AF=3，E平分线段AB，DABC是▱。求直线FC的长度。
Construction (CDL):
Shape(DA,AF,FD)
Shape(CD,DF,FC)
Shape(FA,AE,EF)
Shape(CF,FE,EB,BC)
Collinear(DFE)
Collinear(AEB)
Collinear(AFC)
Conditions (CDL):
Equal(LengthOfLine(AF),3)
IsMidpointOfLine(E,AB)
Parallelogram(DABC)
Goal: Value(LengthOfLine(FC))
Answer: 6
Theorem sequence:
parallel_property_collinear_extend(3,BA,CD,E)
line_addition(1,AE,EB)
parallelogram_property_opposite_line_equal(1,ABCD)
parallel_property_alternate_interior_angle(1,EA,CD)
parallel_property_alternate_interior_angle(2,EA,CD)
similar_triangle_judgment_aa(1,FCD,FAE)
similar_triangle_property_line_ratio(1,FCD,FAE)
similar_triangle_property_line_ratio(1,DFC,EFA)
Problem: As shown in the diagram, Div(LengthOfLine(AD)=LengthOfLine(DB)), DE=2, DE is parallel to BC. Find the length of line BC.
问题：如图所示，Div(LengthOfLine(AD)=LengthOfLine(DB))，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(AD),LengthOfLine(DB)),1/3)
Equal(LengthOfLine(DE),2)
ParallelBetweenLine(DE,BC)
Goal: Value(LengthOfLine(BC))
Answer: 8
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)