ag4masses/outputs/solved/napoleon-ddar-ok.log

I0210 12:02:02.231461 140467004882944 graph.py:498] napoleon
I0210 12:02:02.231686 140467004882944 graph.py:499] a1 a2 a3 = triangle; b3 = on_circle a1 a2, s_angle a1 a2 b3 60; b1 = on_circle a2 a3, s_angle a2 a3 b1 60; b2 = on_circle a3 a1, s_angle a3 a1 b2 60; c1 = circumcenter b1 a2 a3; c2 = circumcenter b2 a3 a1; c3 = circumcenter b3 a1 a2 ? cong c1 c2 c1 c3
I0210 12:02:42.035380 140467004882944 alphageometry.py:191] 
==========================
 * From theorem premises:
A1 A2 A3 B3 B1 B2 C1 C2 C3 : Points
A_1B_3 = A_1A_2 [00]
∠B_3A_2A_1 = 1_PI/3 [01]
∠A_1A_2B_3 = 2_PI/3 [02]
A_2B_1 = A_2A_3 [03]
∠B_1A_3A_2 = 1_PI/3 [04]
∠A_2A_3B_1 = 2_PI/3 [05]
A_3B_2 = A_3A_1 [06]
∠B_2A_1A_3 = 1_PI/3 [07]
∠A_3A_1B_2 = 2_PI/3 [08]
C_1A_2 = C_1A_3 [09]
C_1B_1 = C_1A_2 [10]
C_2B_2 = C_2A_3 [11]
C_2A_3 = C_2A_1 [12]
C_3A_1 = C_3A_2 [13]
C_3B_3 = C_3A_1 [14]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. C_1A_3 = A_2C_1 [09] ⇒  C_1A_3:C_2A_3 = C_1A_3:C_2A_3 [15]
002. C_2B_2 = C_2A_3 [11] & C_2A_3 = C_2A_1 [12] ⇒  C_2A_1 = C_2B_2 [16]
003. A_3B_2 = A_3A_1 [06] & C_2A_1 = C_2B_2 [16] ⇒  A_1B_2 ⟂ A_3C_2 [17]
004. C_1B_1 = C_1A_2 [10] & C_1A_2 = C_1A_3 [09] ⇒  C_1A_3 = C_1B_1 [18]
005. A_2B_1 = A_2A_3 [03] & C_1A_3 = C_1B_1 [18] ⇒  A_3B_1 ⟂ A_2C_1 [19]
006. A_1B_2 ⟂ A_3C_2 [17] & A_3B_1 ⟂ A_2C_1 [19] ⇒  ∠(A_2C_1-A_3B_1) = ∠(C_2A_3-B_2A_1) [20]
007. ∠B_2A_1A_3 = 1_PI/3 [07] & ∠B_1A_3A_2 = 1_PI/3 [04] ⇒  ∠B_1A_3A_2 = ∠B_2A_1A_3 [21]
008. ∠(A_2C_1-A_3B_1) = ∠(C_2A_3-B_2A_1) [20] & ∠B_1A_3A_2 = ∠B_2A_1A_3 [21] ⇒  ∠C_1A_2A_3 = ∠C_2A_3A_1 [22]
009. A_2B_1 = A_2A_3 [03] & C_1A_2 = C_1A_3 [09] & C_1B_1 = C_1A_2 [10] (SSS)⇒  ∠B_1A_2A_3 = ∠A_2C_1A_3 [23]
010. A_2B_1 = A_2A_3 [03] & C_1A_2 = C_1A_3 [09] & C_1B_1 = C_1A_2 [10] (SSS)⇒  ∠A_3A_2B_1 = ∠A_2C_1B_1 [24]
011. A_2B_1 = A_2A_3 [03] & C_1A_2 = C_1A_3 [09] & C_1B_1 = C_1A_2 [10] (SSS)⇒  ∠A_3A_2C_1 = ∠A_2B_1C_1 [25]
012. A_3B_2 = A_3A_1 [06] ⇒  ∠A_1B_2A_3 = ∠A_3A_1B_2 [26]
013. A_2B_1 = A_2A_3 [03] ⇒  ∠A_2A_3B_1 = ∠A_3B_1A_2 [27]
014. ∠A_1B_2A_3 = ∠A_3A_1B_2 [26] & ∠A_3A_1B_2 = 2_PI/3 [08] & ∠A_2A_3B_1 = 2_PI/3 [05] & ∠A_2A_3B_1 = ∠A_3B_1A_2 [27] ⇒  ∠A_3B_1A_2 = ∠A_1B_2A_3 [28]
015. ∠A_3B_1A_2 = ∠A_1B_2A_3 [28] & ∠B_1A_3A_2 = ∠B_2A_1A_3 [21] ⇒  ∠B_2A_3A_1 = ∠B_1A_2A_3 [29]
016. ∠A_3B_1A_2 = ∠A_1B_2A_3 [28] & ∠B_1A_3A_2 = ∠B_2A_1A_3 [21] ⇒  ∠(A_3B_2-A_2B_1) = ∠A_1A_3A_2 [30]
017. A_3B_2 = A_3A_1 [06] & C_2A_3 = C_2A_1 [12] & C_2B_2 = C_2A_3 [11] (SSS)⇒  ∠B_2A_3A_1 = ∠A_3C_2A_1 [31]
018. ∠B_1A_2A_3 = ∠A_2C_1A_3 [23] & ∠B_2A_3A_1 = ∠B_1A_2A_3 [29] & ∠B_2A_3A_1 = ∠A_3C_2A_1 [31] ⇒  ∠A_3C_2A_1 = ∠A_2C_1A_3 [32]
019. ∠C_1A_2A_3 = ∠C_2A_3A_1 [22] & ∠A_3C_2A_1 = ∠A_2C_1A_3 [32] (Similar Triangles)⇒  A_3A_2:A_1A_3 = A_3C_1:A_1C_2 [33]
020. A_3A_2:A_1A_3 = A_3C_1:A_1C_2 [33] & C_1A_2 = C_1A_3 [09] & C_2A_3 = C_2A_1 [12] & B_2A_3 = A_3A_1 [06] ⇒  A_2A_3:B_2A_3 = C_1A_3:C_2A_3 [34]
021. ∠(A_2C_1-A_3B_1) = ∠(C_2A_3-B_2A_1) [20] & ∠A_3B_1A_2 = ∠A_1B_2A_3 [28] ⇒  ∠(A_2C_1-A_3C_2) = ∠(A_2B_1-A_3B_2) [35]
022. ∠A_3A_2B_1 = ∠A_3C_1A_2 [23] & ∠(A_2C_1-A_3C_2) = ∠(A_2B_1-A_3B_2) [35] ⇒  ∠A_2A_3B_2 = ∠C_1A_3C_2 [36]
023. A_2A_3:B_2A_3 = C_1A_3:C_2A_3 [34] & ∠A_2A_3B_2 = ∠C_1A_3C_2 [36] (Similar Triangles)⇒  ∠A_3A_2B_2 = ∠A_3C_1C_2 [37]
024. A_2A_3:B_2A_3 = C_1A_3:C_2A_3 [34] & ∠A_2A_3B_2 = ∠C_1A_3C_2 [36] (Similar Triangles)⇒  ∠A_2B_2A_3 = ∠C_1C_2A_3 [38]
025. ∠A_3A_2B_2 = ∠A_3C_1C_2 [37] & ∠A_2B_2A_3 = ∠C_1C_2A_3 [38] (Similar Triangles)⇒  A_2A_3:A_2B_2 = C_1A_3:C_1C_2 [39]
026. C_3A_1 = C_3A_2 [13] & C_3B_3 = C_3A_1 [14] ⇒  C_3B_3 = C_3A_2 [40]
027. A_1B_3 = A_1A_2 [00] & C_3B_3 = C_3A_2 [40] ⇒  A_2B_3 ⟂ A_1C_3 [41]
028. A_3B_1 ⟂ A_2C_1 [19] & A_2B_3 ⟂ A_1C_3 [41] ⇒  ∠(A_2C_1-A_1C_3) = ∠(A_3B_1-A_2B_3) [42]
029. A_3B_1 ⟂ A_2C_1 [19] & A_2B_3 ⟂ A_1C_3 [41] ⇒  ∠(A_2C_1-A_3B_1) = ∠(C_3A_1-A_2B_3) [43]
030. ∠B_3A_2A_1 = 1_PI/3 [01] & ∠B_1A_3A_2 = 1_PI/3 [04] ⇒  ∠B_1A_3A_2 = ∠B_3A_2A_1 [44]
031. ∠(A_2C_1-A_3B_1) = ∠(C_3A_1-A_2B_3) [43] & ∠B_1A_3A_2 = ∠B_3A_2A_1 [44] ⇒  ∠(A_2C_1-A_1C_3) = ∠A_3A_2A_1 [45]
032. ∠(A_2C_1-A_3B_1) = ∠(C_3A_1-A_2B_3) [43] & ∠B_1A_3A_2 = ∠B_3A_2A_1 [44] ⇒  ∠C_1A_2A_3 = ∠C_3A_1A_2 [46]
033. ∠(A_2C_1-A_1C_3) = ∠(A_3B_1-A_2B_3) [42] & ∠(A_2C_1-A_1C_3) = ∠A_3A_2A_1 [45] ⇒  ∠A_3A_2A_1 = ∠(A_3B_1-A_2B_3) [47]
034. ∠A_2A_3B_1 = ∠A_3B_1A_2 [27] & ∠A_3A_2A_1 = ∠(A_3B_1-A_2B_3) [47] ⇒  ∠A_2B_1A_3 = ∠B_3A_2A_1 [48]
035. A_1B_3 = A_1A_2 [00] ⇒  ∠A_1A_2B_3 = ∠A_2B_3A_1 [49]
036. ∠B_3A_2A_1 = 1_PI/3 [01] & ∠A_1A_2B_3 = ∠A_2B_3A_1 [49] (Angle chase)⇒  ∠A_2A_1B_3 = 1_PI/3 [50]
037. ∠A_1A_2B_3 = ∠A_2B_3A_1 [49] & ∠A_1A_2B_3 = 2_PI/3 [02] & ∠A_2A_3B_1 = 2_PI/3 [05] & ∠A_2A_3B_1 = ∠A_3B_1A_2 [27] ⇒  ∠A_3B_1A_2 = ∠A_2B_3A_1 [51]
038. ∠A_3B_1A_2 = ∠A_2B_3A_1 [51] & ∠B_1A_3A_2 = ∠B_3A_2A_1 [44] ⇒  ∠A_3A_2B_1 = ∠A_2A_1B_3 [52]
039. ∠A_2B_1A_3 = ∠B_3A_2A_1 [48] & ∠B_3A_2A_1 = 1_PI/3 [01] & ∠A_2A_1B_3 = 1_PI/3 [50] & ∠A_3A_2B_1 = ∠A_2A_1B_3 [52] ⇒  ∠A_3A_2B_1 = ∠A_2B_1A_3 [53]
040. ∠A_3A_2B_1 = ∠A_2B_1A_3 [53] ⇒  A_3A_2 = A_3B_1 [54]
041. A_1B_3 = A_1A_2 [00] & C_3B_3 = C_3A_1 [14] & C_3A_1 = C_3A_2 [13] (SSS)⇒  ∠A_2A_1B_3 = ∠A_1C_3B_3 [55]
042. A_1B_3 = A_1A_2 [00] & C_3B_3 = C_3A_1 [14] & C_3A_1 = C_3A_2 [13] (SSS)⇒  ∠B_3A_1A_2 = ∠A_1C_3A_2 [56]
043. ∠A_3A_2B_1 = ∠A_2C_1B_1 [24] & ∠A_3A_2B_1 = ∠A_2A_1B_3 [52] & ∠A_2A_1B_3 = ∠A_1C_3B_3 [55] ⇒  ∠A_1C_3B_3 = ∠A_2C_1B_1 [57]
044. ∠C_1A_2A_3 = ∠C_3A_1A_2 [46] & ∠A_1C_3B_3 = ∠A_2C_1B_1 [57] ⇒  ∠(B_3C_3-A_1A_2) = ∠(B_1C_1-A_2A_3) [58]
045. C_3B_3 = C_3A_1 [14] ⇒  ∠C_3B_3A_1 = ∠B_3A_1C_3 [59]
046. C_3B_3 = C_3A_2 [40] ⇒  ∠C_3B_3A_2 = ∠B_3A_2C_3 [60]
047. C_3A_1 = C_3A_2 [13] ⇒  ∠C_3A_1A_2 = ∠A_1A_2C_3 [61]
048. ∠B_3A_2A_1 = 1_PI/3 [01] & ∠A_1A_2B_3 = ∠A_2B_3A_1 [49] & ∠C_3B_3A_1 = ∠B_3A_1C_3 [59] & ∠C_3B_3A_2 = ∠B_3A_2C_3 [60] & ∠C_3A_1A_2 = ∠A_1A_2C_3 [61] (Angle chase)⇒  A_1A_2 ⟂ B_3C_3 [62]
049. ∠(B_3C_3-A_1A_2) = ∠(B_1C_1-A_2A_3) [58] & A_1A_2 ⟂ B_3C_3 [62] & A_3B_1 ⟂ A_2C_1 [19] ⇒  ∠(A_2C_1-A_3B_1) = ∠(C_1B_1-A_2A_3) [63]
050. ∠A_3A_2C_1 = ∠A_2B_1C_1 [25] & ∠(A_3B_2-A_2B_1) = ∠A_1A_3A_2 [30] ⇒  ∠(B_1C_1-A_3B_2) = ∠(A_2C_1-A_1A_3) [64]
051. ∠(A_2C_1-A_3B_1) = ∠(C_1B_1-A_2A_3) [63] & ∠(B_1C_1-A_3B_2) = ∠(A_2C_1-A_1A_3) [64] ⇒  ∠A_2A_3B_2 = ∠B_1A_3A_1 [65]
052. A_3A_2 = A_3B_1 [54] & A_3B_2 = A_3A_1 [06] & ∠A_2A_3B_2 = ∠B_1A_3A_1 [65] (SAS)⇒  B_2A_2 = A_1B_1 [66]
053. ∠B_1A_2A_3 = ∠A_2C_1A_3 [23] & ∠B_1A_2A_3 = ∠B_3A_1A_2 [52] & ∠B_3A_1A_2 = ∠A_1C_3A_2 [56] ⇒  ∠A_1C_3A_2 = ∠A_2C_1A_3 [67]
054. ∠C_1A_2A_3 = ∠C_3A_1A_2 [46] & ∠A_1C_3A_2 = ∠A_2C_1A_3 [67] (Similar Triangles)⇒  A_3A_2:A_2A_1 = A_3C_1:A_2C_3 [68]
055. A_3A_2:A_2A_1 = A_3C_1:A_2C_3 [68] & C_1A_2 = C_1A_3 [09] & C_3A_1 = C_3A_2 [13] & A_2B_1 = A_2A_3 [03] ⇒  A_2A_1:A_2B_1 = A_2C_3:A_2C_1 [69]
056. ∠(A_2C_1-A_3B_1) = ∠(C_3A_1-A_2B_3) [43] & ∠A_3B_1A_2 = ∠A_2B_3A_1 [51] ⇒  ∠(A_2C_1-A_1C_3) = ∠(A_2B_1-A_1B_3) [70]
057. ∠A_2A_1B_3 = ∠A_2C_3A_1 [56] & ∠(A_2C_1-A_1C_3) = ∠(A_2B_1-A_1B_3) [70] ⇒  ∠C_3A_2C_1 = ∠A_1A_2B_1 [71]
058. A_2A_1:A_2B_1 = A_2C_3:A_2C_1 [69] & ∠C_3A_2C_1 = ∠A_1A_2B_1 [71] (Similar Triangles)⇒  B_1A_1:B_1A_2 = C_1C_3:C_1A_2 [72]
059. A_2A_3:A_2B_2 = C_1A_3:C_1C_2 [39] & B_2A_2 = A_1B_1 [66] & C_1A_2 = C_1A_3 [09] & B_1A_1:B_1A_2 = C_1C_3:C_1A_2 [72] & A_2B_1 = A_2A_3 [03] ⇒  C_1A_3:C_1C_3 = C_1A_3:C_1C_2 [73]
060. C_1A_3:C_2A_3 = C_1A_3:C_2A_3 [15] & C_1A_3:C_1C_3 = C_1A_3:C_1C_2 [73] ⇒  C_1C_3 = C_1C_2
==========================

I0210 12:02:42.036046 140467004882944 alphageometry.py:195] Solution written to /home/tong_peng/pyvenv/agtest/ag.out.