Delete ag4masses/outputs

ag4masses/outputs/solved/5circles-ddar-ok.log

@@ -1,81 +0,0 @@
-++ BATCH_SIZE=32
-++ BEAM_SIZE=128
-++ DEPTH=8
-++ NWORKERS=8
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt
-++ PROB=5circles
-++ MODEL=alphageometry
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt --problem_name=5circles --mode=alphageometry --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=128 --search_depth=8 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=32 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out --n_workers=8
-I0310 12:49:36.705405 133820260323328 graph.py:498] 5circles
-I0310 12:49:36.705694 133820260323328 graph.py:499] a b c d e = pentagon a b c d e; f = on_line f b e, on_line f a c; g = on_line g a c, on_line g b d; h = on_line h b d, on_line h c e; i = on_line i c e, on_line i d a; j = on_line j d a, on_line j b e; k = circumcenter k a f j; l = circumcenter l b f g; m = circumcenter m c g h; n = circumcenter n d h i; o = circumcenter o e i j; p = on_circle p k f, on_circle p l f; q = on_circle q l g, on_circle q m g; r = on_circle r m h, on_circle r n h; s = on_circle s n i, on_circle s o i; t = on_circle t o j, on_circle t k j ? cyclic p q r t
-I0310 12:55:28.171156 133820260323328 alphageometry.py:200] 
-==========================
- * From theorem premises:
-A B C D E F G H I J K L M N O P Q R T : Points
-F,A,C are collinear [00]
-F,E,B are collinear [01]
-D,B,G are collinear [02]
-A,G,C are collinear [03]
-D,B,H are collinear [04]
-A,I,D are collinear [05]
-E,C,I are collinear [06]
-E,J,B are collinear [07]
-KA = KF [08]
-KF = KJ [09]
-LF = LG [10]
-LB = LF [11]
-MG = MH [12]
-MC = MG [13]
-ND = NH [14]
-NH = NI [15]
-OE = OI [16]
-OI = OJ [17]
-KP = KF [18]
-LP = LF [19]
-MQ = MG [20]
-LQ = LG [21]
-NR = NH [22]
-MR = MH [23]
-KT = KJ [24]
-OT = OJ [25]
-
- * Auxiliary Constructions:
-S : Points
-OS = OI [26]
-
- * Proof steps:
-001. KA = KF [08] & KF = KJ [09] & KT = KJ [24] ⇒  F,A,J,T are concyclic [27]
-002. F,A,J,T are concyclic [27] & KA = KF [08] & KP = KF [18] & KF = KJ [09] ⇒  A,F,P,T are concyclic [28]
-003. A,F,P,T are concyclic [28] ⇒  ∠AFP = ∠ATP [29]
-004. ND = NH [14] & NR = NH [22] & NH = NI [15] ⇒  D,I,R,H are concyclic [30]
-005. D,I,R,H are concyclic [30] ⇒  ∠DHR = ∠DIR [31]
-006. MG = MH [12] & MR = MH [23] & MC = MG [13] ⇒  H,C,R,G are concyclic [32]
-007. H,C,R,G are concyclic [32] ⇒  ∠HGC = ∠HRC [33]
-008. I,A,D are collinear [05] & ∠DHR = ∠DIR [31] & D,B,H are collinear [04] & ∠HGC = ∠HRC [33] & D,B,G are collinear [02] & A,G,C are collinear [03] ⇒  ∠ACR = ∠AIR [34]
-009. ∠ACR = ∠AIR [34] ⇒  A,I,R,C are concyclic [35]
-010. OE = OI [16] & OI = OJ [17] & OT = OJ [25] & OS = OI [26] ⇒  E,I,J,T are concyclic [36]
-011. E,I,J,T are concyclic [36] ⇒  ∠JTI = ∠JEI [37]
-012. F,A,J,T are concyclic [27] ⇒  ∠AFJ = ∠ATJ [38]
-013. E,I,C are collinear [06] & ∠JTI = ∠JEI [37] & E,J,B are collinear [07] & ∠AFJ = ∠ATJ [38] & F,A,C are collinear [00] & F,E,B are collinear [01] ⇒  ∠CAT = ∠CIT [39]
-014. ∠CAT = ∠CIT [39] ⇒  A,I,T,C are concyclic [40]
-015. A,I,R,C are concyclic [35] & A,I,T,C are concyclic [40] ⇒  A,C,T,R are concyclic [41]
-016. A,C,T,R are concyclic [41] ⇒  ∠CAT = ∠CRT [42]
-017. ∠AFP = ∠ATP [29] & F,A,C are collinear [00] & ∠CAT = ∠CRT [42] ⇒  ∠CRT = ∠FPT [43]
-018. H,C,R,G are concyclic [32] & MG = MH [12] & MQ = MG [20] & MC = MG [13] ⇒  C,R,G,Q are concyclic [44]
-019. Q,G,C,R are concyclic [44] ⇒  ∠QGC = ∠QRC [45]
-020. LP = LF [19] & LF = LG [10] & LQ = LG [21] & LB = LF [11] ⇒  F,Q,P,G are concyclic [46]
-021. F,Q,P,G are concyclic [46] ⇒  ∠FPQ = ∠FGQ [47]
-022. ∠QGC = ∠QRC [45] & A,G,C are collinear [03] & ∠FPQ = ∠FGQ [47] & F,A,C are collinear [00] ⇒  ∠FPQ = ∠CRQ [48]
-023. ∠CRT = ∠FPT [43] & ∠FPQ = ∠CRQ [48] ⇒  ∠TPQ = ∠TRQ [49]
-024. ∠TPQ = ∠TRQ [49] ⇒  Q,P,R,T are concyclic
-==========================
-
-I0310 12:55:28.171662 133820260323328 alphageometry.py:204] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.

ag4masses/outputs/solved/angle-side-bisec-cyclic-ag-ok.log

@@ -1,59 +0,0 @@
-I0210 22:07:57.112957 140473292709888 graph.py:498] angbisec_bline_cyclic
-I0210 22:07:57.113278 140473292709888 graph.py:499] a b c = triangle a b c; d = on_bline d b c, angle_bisector d b a c ? cyclic a b c d
-I0210 22:07:57.142698 140473292709888 alphageometry.py:221] DD+AR failed to solve the problem.
-I0210 22:07:57.142895 140473292709888 alphageometry.py:555] Depth 0. There are 1 nodes to expand:
-I0210 22:07:57.143001 140473292709888 alphageometry.py:559] {S} a : ; b : ; c : ; d : D b d c d 00 ^ a b a d a d a c 01 ^ c b c d b d b c 02 ? O a b c d {F1} x00
-I0210 22:07:57.143262 140473292709888 alphageometry.py:564] Decoding from {S} a : ; b : ; c : ; d : D b d c d 00 ^ a b a d a d a c 01 ^ c b c d b d b c 02 ? O a b c d {F1} x00
-I0210 22:10:02.080104 140473292709888 alphageometry.py:582] Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/pyvenv/alphageometry/alphageometry.py", line 454, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/pyvenv/alphageometry/graph.py", line 2637, in add_clause
-    raise PointTooFarError()
-graph.PointTooFarError
-"
-
-I0210 22:10:02.080281 140473292709888 alphageometry.py:582] Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/pyvenv/alphageometry/alphageometry.py", line 454, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/pyvenv/alphageometry/graph.py", line 2622, in add_clause
-    nums = draw_fn()
-  File "/home/tong_peng/pyvenv/alphageometry/graph.py", line 2608, in draw_fn
-    return nm.reduce(to_be_intersected, existing_points)
-  File "/home/tong_peng/pyvenv/alphageometry/numericals.py", line 1310, in reduce
-    result = a.intersect(b)
-  File "/home/tong_peng/pyvenv/alphageometry/numericals.py", line 213, in intersect
-    return line_line_intersection(self, obj)
-  File "/home/tong_peng/pyvenv/alphageometry/numericals.py", line 584, in line_line_intersection
-    raise InvalidLineIntersectError
-numericals.InvalidLineIntersectError
-"
-
-I0210 22:10:02.080370 140473292709888 alphageometry.py:582] Translation: "e = on_bline e b a, on_bline e c a"
-
-I0210 22:10:02.080573 140473292709888 graph.py:498] 
-I0210 22:10:02.080641 140473292709888 graph.py:499] a b c = triangle a b c; d = on_bline d b c, angle_bisector d b a c; e = on_bline e b a, on_bline e c a ? cyclic a b c d
-I0210 22:10:02.356900 140473292709888 alphageometry.py:191] 
-==========================
- * From theorem premises:
-A B C D : Points
-∠BAD = ∠DAC [00]
-DB = DC [01]
-
- * Auxiliary Constructions:
-E : Points
-EC = EA [02]
-EB = EA [03]
-∠EBA = ∠BAE [04]
-∠ECA = ∠CAE [05]
-
- * Proof steps:
-001. EB = EA [03] & EC = EA [02] ⇒  EC = EB [06]
-002. EC = EB [06] ⇒  ∠ECB = ∠CBE [07]
-003. DB = DC [01] & EC = EB [06] ⇒  BC ⟂ DE [08]
-004. ∠BAD = ∠DAC [00] & ∠EBA = ∠BAE [04] & ∠ECA = ∠CAE [05] & ∠ECB = ∠CBE [07] & BC ⟂ DE [08] (Angle chase)⇒  ∠DAE = ∠EDA [09]
-005. ∠DAE = ∠EDA [09] ⇒  EA = ED [10]
-006. EC = EA [02] & EB = EA [03] & EA = ED [10] ⇒  C,B,A,D are concyclic
-==========================
-
-I0210 22:10:02.357384 140473292709888 alphageometry.py:195] Solution written to /home/tong_peng/pyvenv/agtest/ag.out2.
-I0210 22:11:16.577270 140473292709888 alphageometry.py:597] Solved.

ag4masses/outputs/solved/castillon-lemma-ag-ok.log

@@ -1,89 +0,0 @@
-I0211 17:53:45.675628 140166174494720 graph.py:498] castillon_lemma
-I0211 17:53:45.676038 140166174494720 graph.py:499] a b = segment a b; c = on_circle c a b; d = on_line d a b, lc_tangent d c a; e = foot e c a b; f = on_circle f a b; g = on_tline g d a b, lc_tangent g f a; h = on_line h d g, on_line h e f; i = on_circle i a b; j = on_circle j a b, on_line j i g; k = on_circle k a b, on_line k i h ? coll e j k
-I0211 17:56:14.703040 140166174494720 alphageometry.py:191] 
-==========================
- * From theorem premises:
-A B C D E F G H I J K : Points
-AC = AB [00]
-D,A,B are collinear [01]
-CD ⟂ AC [02]
-CE ⟂ AB [03]
-A,E,B are collinear [04]
-AF = AB [05]
-∠BAF = ∠BAF [06]
-AB ⟂ GD [07]
-FG ⟂ AF [08]
-F,H,E are collinear [09]
-D,G,H are collinear [10]
-AI = AB [11]
-AJ = AB [12]
-G,J,I are collinear [13]
-AK = AB [14]
-H,K,I are collinear [15]
-
- * Auxiliary Constructions:
-: Points
-
-
- * Proof steps:
-001. AB ⟂ GD [07] & CE ⟂ AB [03] ⇒  GD ∥ CE [16]
-002. AI = AB [11] & AK = AB [14] & AC = AB [00] & AF = AB [05] & AJ = AB [12] ⇒  J,C,B,K are concyclic [17]
-003. J,C,B,K are concyclic [17] ⇒  ∠JBC = ∠JKC [18]
-004. J,C,B,K are concyclic [17] ⇒  ∠JCB = ∠JKB [19]
-005. AC = AB [00] ⇒  ∠ACB = ∠CBA [20]
-006. AK = AB [14] & AC = AB [00] ⇒  AC = AK [21]
-007. AC = AK [21] ⇒  ∠ACK = ∠CKA [22]
-008. AK = AB [14] ⇒  ∠ABK = ∠BKA [23]
-009. CE ⟂ AB [03] & DG ∥ CE [16] & ∠JBC = ∠JKC [18] & ∠JCB = ∠JKB [19] & ∠ACB = ∠CBA [20] & ∠ACK = ∠CKA [22] & ∠ABK = ∠BKA [23] (Angle chase)⇒  ∠(DG-BJ) = ∠BCJ [24]
-010. ∠(DG-BJ) = ∠BCJ [24] & DG ∥ CE [16] & ∠BCJ = ∠BKJ [19] ⇒  ∠BKJ = ∠(DG-JB) [25]
-011. AI = AB [11] & AF = AB [05] & AJ = AB [12] ⇒  A is the circumcenter of \Delta FIJ [26]
-012. A is the circumcenter of \Delta FIJ [26] & FG ⟂ AF [08] ⇒  ∠GFI = ∠FJI [27]
-013. G,J,I are collinear [13] & ∠GFI = ∠FJI [27] ⇒  ∠FJG = ∠GFI [28]
-014. G,J,I are collinear [13] ⇒  ∠FGJ = ∠FGI [29]
-015. ∠FJG = ∠GFI [28] & ∠FGJ = ∠FGI [29] (Similar Triangles)⇒  FJ:FG = FI:GI [30]
-016. ∠FJG = ∠GFI [28] & ∠FGJ = ∠FGI [29] (Similar Triangles)⇒  FJ:GJ = FI:FG [31]
-017. D,A,B are collinear [01] & FG ⟂ AF [08] & CE ⟂ AB [03] & CE ∥ DG [16] ⇒  ∠GDA = ∠GFA [32]
-018. ∠GDA = ∠GFA [32] ⇒  D,F,A,G are concyclic [33]
-019. D,F,A,G are concyclic [33] ⇒  ∠FDG = ∠FAG [34]
-020. D,F,A,G are concyclic [33] ⇒  ∠DFG = ∠DAG [35]
-021. A,E,B are collinear [04] & CE ⟂ AB [03] & CD ⟂ AC [02] ⇒  ∠ACD = ∠CEA [36]
-022. D,A,B are collinear [01] & AB ⟂ DG [07] ⇒  DA ⟂ DG [37]
-023. DA ⟂ DG [37] & CD ⟂ AC [02] ⇒  ∠ADC = ∠(DG-CA) [38]
-024. DA ⟂ DG [37] & CD ⟂ AC [02] ⇒  ∠DAC = ∠GDC [39]
-025. D,A,B are collinear [01] & ∠ADC = ∠(DG-CA) [38] & DG ∥ CE [16] ⇒  ∠ADC = ∠ECA [40]
-026. ∠ACD = ∠CEA [36] & ∠ADC = ∠ECA [40] (Similar Triangles)⇒  AC:AD = AE:AC [41]
-027. AC:AD = AE:AC [41] & AC = AB [00] & FA = AB [05] ⇒  AE:AF = AF:AD [42]
-028. A,E,B are collinear [04] & D,A,B are collinear [01] & ∠BAF = ∠BAF [06] ⇒  ∠EAF = ∠DAF [43]
-029. AE:AF = AF:AD [42] & ∠EAF = ∠DAF [43] (Similar Triangles)⇒  ∠AEF = ∠DFA [44]
-030. F,H,E are collinear [09] & ∠DFG = ∠DAG [35] & D,A,B are collinear [01] & ∠AEF = ∠DFA [44] & A,E,B are collinear [04] ⇒  ∠AFH = ∠FGA [45]
-031. FG ⟂ AF [08] & ∠AFH = ∠FGA [45] ⇒  ∠GFH = ∠FAG [46]
-032. F,H,E are collinear [09] & ∠FDG = ∠FAG [34] & DG ∥ CE [16] & ∠GFH = ∠FAG [46] ⇒  ∠HFG = ∠GDF [47]
-033. D,G,H are collinear [10] & CE ∥ DG [16] ⇒  ∠FGD = ∠FGH [48]
-034. ∠HFG = ∠GDF [47] & ∠FGD = ∠FGH [48] (Similar Triangles)⇒  DF:FG = FH:GH [49]
-035. ∠HFG = ∠GDF [47] & ∠FGD = ∠FGH [48] (Similar Triangles)⇒  DF:DG = FH:FG [50]
-036. FJ:FG = FI:GI [30] & FJ:GJ = FI:FG [31] & DF:FG = FH:GH [49] & DF:DG = FH:FG [50] (Ratio chase)⇒  GI:GH = DG:GJ [51]
-037. G,J,I are collinear [13] & D,G,H are collinear [10] ⇒  ∠DGJ = ∠HGI [52]
-038. GI:GH = DG:GJ [51] & ∠DGJ = ∠HGI [52] (Similar Triangles)⇒  ∠GDJ = ∠HIG [53]
-039. AI = AB [11] & AK = AB [14] & AC = AB [00] & AF = AB [05] & AJ = AB [12] ⇒  J,B,K,I are concyclic [54]
-040. J,B,K,I are concyclic [54] ⇒  ∠JBK = ∠JIK [55]
-041. ∠GDJ = ∠HIG [53] & DG ∥ CE [16] & ∠JBK = ∠JIK [55] & G,J,I are collinear [13] & H,K,I are collinear [15] ⇒  ∠KBJ = ∠GDJ [56]
-042. ∠BKJ = ∠(DG-JB) [25] & ∠KBJ = ∠GDJ [56] ⇒  ∠KJB = ∠BJD [57]
-043. A,E,B are collinear [04] & D,A,B are collinear [01] ⇒  B,D,E are collinear [58]
-044. A,E,B are collinear [04] & D,A,B are collinear [01] & CE ⟂ AB [03] ⇒  ∠DEC = ∠CEA [59]
-045. A,E,B are collinear [04] & ∠DAC = ∠GDC [39] & D,A,B are collinear [01] & DG ∥ CE [16] ⇒  ∠DCE = ∠CAE [60]
-046. ∠DEC = ∠CEA [59] & ∠DCE = ∠CAE [60] (Similar Triangles)⇒  CD:AC = CE:AE [61]
-047. AC:AD = AE:AC [41] & AC = AB [00] & JA = AB [12] ⇒  AE:AJ = AJ:AD [62]
-048. A,E,B are collinear [04] & D,A,B are collinear [01] ⇒  ∠EAJ = ∠DAJ [63]
-049. AE:AJ = AJ:AD [62] & ∠EAJ = ∠DAJ [63] (Similar Triangles)⇒  EA:EJ = JA:JD [64]
-050. EA:EJ = JA:JD [64] & AJ = AB [12] & CA = AB [00] ⇒  CA:DJ = AE:JE [65]
-051. CA:DC = AE:CE [61] & CA:DJ = AE:JE [65] ⇒  DC:CE = DJ:JE [66]
-052. CD ⟂ AC [02] & CE ⟂ AB [03] & ∠ACB = ∠CBA [20] (Angle chase)⇒  ∠DCB = ∠BCE [67]
-053. ∠DCB = ∠BCE [67] & B,D,E are collinear [58] ⇒  DB:EB = DC:CE [68]
-054. DC:CE = DJ:JE [66] & DB:EB = DC:CE [68] ⇒  BD:BE = JD:JE [69]
-055. BD:BE = JD:JE [69] & B,D,E are collinear [58] ⇒  ∠BJD = ∠EJB [70]
-056. ∠KJB = ∠BJD [57] & ∠BJD = ∠EJB [70] ⇒  ∠EJB = ∠KJB [71]
-057. ∠EJB = ∠KJB [71] ⇒  JE ∥ JK [72]
-058. EJ ∥ JK [72] ⇒  J,K,E are collinear
-==========================
-
-I0211 17:56:14.704421 140166174494720 alphageometry.py:195] Solution written to /home/tong_peng/pyvenv/agtest/ag.out.

ag4masses/outputs/solved/castillon4p-ag-ok.log

@@ -1,148 +0,0 @@
-++ BATCH_SIZE=4
-++ BEAM_SIZE=256
-++ DEPTH=16
-++ OUTFILE=ag.out
-+++ pwd
-++ PROB_FILE=/home/tong_peng/pyvenv/alphageometry/myexamples.txt
-++ PROB=castillon_4p
-++ MODEL=alphageometry
-++ DATA=ag_ckpt_vocab
-++ MELIAD_PATH=meliad_lib/meliad
-++ export PYTHONPATH=:meliad_lib/meliad
-++ PYTHONPATH=:meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$(pwd)/defs.txt --rules_file=$(pwd)/rules.txt)
-+++ pwd
-+++ pwd
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ echo :meliad_lib/meliad
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/pyvenv/alphageometry/myexamples.txt --problem_name=castillon_4p --mode=alphageometry --defs_file=/home/tong_peng/pyvenv/alphageometry/defs.txt --rules_file=/home/tong_peng/pyvenv/alphageometry/rules.txt --beam_size=256 --search_depth=16 --ckpt_path=ag_ckpt_vocab --vocab_path=ag_ckpt_vocab/geometry.757.model --gin_search_paths=meliad_lib/meliad/transformer/configs --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=4 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=ag.out
-I0204 15:41:01.128032 139642560315392 graph.py:498] castillon_4p
-I0204 15:41:01.128285 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c ? cong e f e o
-I0204 15:42:34.936169 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 15:42:34.936503 139642560315392 alphageometry.py:539] Depth 0. There are 1 nodes to expand:
-I0204 15:42:34.936591 139642560315392 alphageometry.py:543] {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00
-I0204 15:42:34.936649 139642560315392 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00
-I0204 15:46:26.592027 139642560315392 alphageometry.py:566] Translation: "p = on_line p m l, on_bline p l m"
-
-I0204 15:46:26.592694 139642560315392 graph.py:498] 
-I0204 15:46:26.592885 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p m l, on_bline p l m ? cong e f e o
-I0204 15:48:34.950014 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 15:48:34.950472 139642560315392 alphageometry.py:566] Translation: "p = on_line p k l, on_bline p l k"
-
-I0204 15:48:34.950905 139642560315392 graph.py:498] 
-I0204 15:48:34.951006 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p k l, on_bline p l k ? cong e f e o
-I0204 15:50:36.427841 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 15:50:36.428340 139642560315392 alphageometry.py:566] Translation: "p = on_line p f g, on_bline p g f"
-
-I0204 15:50:36.428967 139642560315392 graph.py:498] 
-I0204 15:50:36.429156 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p f g, on_bline p g f ? cong e f e o
-I0204 15:52:45.975893 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 15:52:45.976284 139642560315392 alphageometry.py:566] Translation: "p = on_line p k l, on_circle p k l"
-
-I0204 15:52:45.976680 139642560315392 graph.py:498] 
-I0204 15:52:45.976783 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p k l, on_circle p k l ? cong e f e o
-I0204 15:54:36.985071 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 15:54:36.985389 139642560315392 alphageometry.py:539] Depth 1. There are 4 nodes to expand:
-I0204 15:54:36.985542 139642560315392 alphageometry.py:543] {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00 p : C m l p 18 D m p l p 19 ; x00
-I0204 15:54:36.985688 139642560315392 alphageometry.py:543] {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00 p : C k l p 18 D k p l p 19 ; x00
-I0204 15:54:36.985815 139642560315392 alphageometry.py:543] {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00 p : C f g p 18 D f p g p 19 ; x00
-I0204 15:54:36.985927 139642560315392 alphageometry.py:543] {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00 p : C k l p 18 D k l k p 19 ; x00
-I0204 15:54:36.986042 139642560315392 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : ; e : ; f : ; g : C a f g 00 D e f e g 01 ; h : C a b h 02 O b f g h 03 ; i : C d f i 04 D e f e i 05 ; j : C c d j 06 O c f i j 07 ; k : C a b k 08 C c d k 09 ; l : D e f e l 10 O h j k l 11 ; m : C a l m 12 D e f e m 13 ; n : C d l n 14 D e f e n 15 ; o : C b m o 16 C c n o 17 ? D e f e o {F1} x00 p : C m l p 18 D m p l p 19 ; x00
-I0204 15:57:42.645735 139642560315392 alphageometry.py:566] Translation: "q = on_line q k l, on_bline q l k"
-
-I0204 15:57:42.646229 139642560315392 graph.py:498] 
-I0204 15:57:42.646357 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p m l, on_bline p l m; q = on_line q k l, on_bline q l k ? cong e f e o
-I0204 16:00:04.265960 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 16:00:04.266489 139642560315392 alphageometry.py:566] Translation: "q = on_line q b l, on_bline q l b"
-
-I0204 16:00:04.267304 139642560315392 graph.py:498] 
-I0204 16:00:04.267570 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p m l, on_bline p l m; q = on_line q b l, on_bline q l b ? cong e f e o
-I0204 16:02:36.520836 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 16:02:36.521435 139642560315392 alphageometry.py:566] Translation: "q = on_line q l n, on_bline q n l"
-
-I0204 16:02:36.522110 139642560315392 graph.py:498] 
-I0204 16:02:36.522347 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p m l, on_bline p l m; q = on_line q l n, on_bline q n l ? cong e f e o
-I0204 16:05:21.532783 139642560315392 alphageometry.py:221] DD+AR failed to solve the problem.
-I0204 16:05:21.533322 139642560315392 alphageometry.py:566] Translation: "q = on_line q l o, on_bline q o l"
-
-I0204 16:05:21.533951 139642560315392 graph.py:498] 
-I0204 16:05:21.534170 139642560315392 graph.py:499] a b c d = quadrangle a b c d; e f = segment e f; g = on_line g a f, on_circle g e f; h = on_circum h f b g, on_line h a b; i = on_line i d f, on_circle i e f; j = on_circum j f c i, on_line j c d; k = on_line k a b, on_line k c d; l = on_circum l k h j, on_circle l e f; m = on_line m l a, on_circle m e f; n = on_line n l d, on_circle n e f; o = on_line o m b, on_line o n c; p = on_line p m l, on_bline p l m; q = on_line q l o, on_bline q o l ? cong e f e o
-I0204 16:08:19.006508 139642560315392 alphageometry.py:191] 
-==========================
- * From theorem premises:
-A B C D E F G H I J K L M N O : Points
-F,G,A are collinear [00]
-EG = EF [01]
-B,H,A are collinear [02]
-B,F,H,G are concyclic [03]
-EI = EF [04]
-D,F,I are collinear [05]
-J,D,C are collinear [06]
-J,F,I,C are concyclic [07]
-B,A,K are collinear [08]
-D,C,K are collinear [09]
-EL = EF [10]
-H,L,J,K are concyclic [11]
-L,M,A are collinear [12]
-EM = EF [13]
-D,L,N are collinear [14]
-EN = EF [15]
-N,O,C are collinear [16]
-B,M,O are collinear [17]
-
- * Auxiliary Constructions:
-P Q : Points
-L,M,P are collinear [18]
-PL = PM [19]
-O,L,Q are collinear [20]
-QO = QL [21]
-
- * Proof steps:
-001. O,L,Q are collinear [20] & QO = QL [21] ⇒  Q is midpoint of LO [22]
-002. B,F,H,G are concyclic [03] ⇒  ∠BHF = ∠BGF [23]
-003. ∠BHF = ∠BGF [23] & B,H,A are collinear [02] & F,G,A are collinear [00] ⇒  ∠ABG = ∠HFA [24]
-004. B,H,A are collinear [02] & F,G,A are collinear [00] & ∠BHF = ∠BGF [23] ⇒  ∠AHF = ∠BGA [25]
-005. ∠AHF = ∠BGA [25] & ∠ABG = ∠HFA [24] (Similar Triangles)⇒  HA:FA = GA:BA [26]
-006. EG = EF [01] & EM = EF [13] & EI = EF [04] & EL = EF [10] ⇒  G,L,M,F are concyclic [27]
-007. G,L,M,F are concyclic [27] ⇒  ∠GLM = ∠GFM [28]
-008. ∠GLM = ∠GFM [28] & L,M,A are collinear [12] & F,G,A are collinear [00] ⇒  ∠GLA = ∠AFM [29]
-009. L,M,A are collinear [12] & F,G,A are collinear [00] & ∠GLM = ∠GFM [28] ⇒  ∠AMF = ∠LGA [30]
-010. ∠AMF = ∠LGA [30] & ∠GLA = ∠AFM [29] (Similar Triangles)⇒  MA:FA = GA:LA [31]
-011. HA:FA = GA:BA [26] & MA:FA = GA:LA [31] (Ratio chase)⇒  BA:MA = LA:HA [32]
-012. L,M,A are collinear [12] & B,H,A are collinear [02] ⇒  ∠BAM = ∠HAL [33]
-013. BA:MA = LA:HA [32] & ∠BAM = ∠HAL [33] (Similar Triangles)⇒  ∠(HL-AB) = ∠(AL-BM) [34]
-014. H,L,J,K are concyclic [11] ⇒  ∠HLJ = ∠HKJ [35]
-015. J,F,I,C are concyclic [07] ⇒  ∠JIF = ∠JCF [36]
-016. D,F,I are collinear [05] & ∠JIF = ∠JCF [36] & J,D,C are collinear [06] ⇒  ∠DCF = ∠JID [37]
-017. D,C,J are collinear [06] & ∠JIF = ∠JCF [36] & D,F,I are collinear [05] ⇒  ∠DFC = ∠IJD [38]
-018. ∠DCF = ∠JID [37] & ∠DFC = ∠IJD [38] (Similar Triangles)⇒  DC:DF = DI:DJ [39]
-019. EG = EF [01] & EN = EF [15] & EM = EF [13] & EI = EF [04] & F,M,G,L are concyclic [27] ⇒  I,L,N,F are concyclic [40]
-020. I,L,N,F are concyclic [40] ⇒  ∠ILN = ∠IFN [41]
-021. D,F,I are collinear [05] & D,L,N are collinear [14] & ∠ILN = ∠IFN [41] ⇒  ∠LID = ∠DNF [42]
-022. D,F,I are collinear [05] & D,L,N are collinear [14] ⇒  ∠LDI = ∠NDF [43]
-023. ∠LID = ∠DNF [42] & ∠LDI = ∠NDF [43] (Similar Triangles)⇒  LI:DL = FN:DF [44]
-024. ∠LID = ∠DNF [42] & ∠LDI = ∠NDF [43] (Similar Triangles)⇒  LI:DI = FN:DN [45]
-025. DC:DF = DI:DJ [39] & LI:DL = FN:DF [44] & LI:DI = FN:DN [45] (Ratio chase)⇒  DJ:DL = DN:DC [46]
-026. D,C,J are collinear [06] & D,L,N are collinear [14] ⇒  ∠JDL = ∠CDN [47]
-027. DJ:DL = DN:DC [46] & ∠JDL = ∠CDN [47] (Similar Triangles)⇒  ∠DJL = ∠CND [48]
-028. D,L,N are collinear [14] & O,C,N are collinear [16] & L,M,A are collinear [12] & O,M,B are collinear [17] & ∠(HL-AB) = ∠(AL-BM) [34] & ∠HLJ = ∠HKJ [35] & B,A,K are collinear [08] & B,H,A are collinear [02] & D,C,K are collinear [09] & J,D,C are collinear [06] & ∠DJL = ∠CND [48] ⇒  ∠LNO = ∠LMO [49]
-029. ∠LNO = ∠LMO [49] ⇒  O,L,M,N are concyclic [50]
-030. O,L,M,N are concyclic [50] & EG = EF [01] & EN = EF [15] & EM = EF [13] & EI = EF [04] & EL = EF [10] & F,M,G,L are concyclic [27] ⇒  O,L,M,F are concyclic [51]
-031. O,L,M,F are concyclic [51] ⇒  ∠OLF = ∠OMF [52]
-032. EM = EF [13] & EL = EF [10] ⇒  E is the circumcenter of \Delta FML [53]
-033. EM = EF [13] & EL = EF [10] ⇒  EM = EL [54]
-034. P,L,M are collinear [18] & PL = PM [19] ⇒  P is midpoint of LM [55]
-035. E is the circumcenter of \Delta FML [53] & P is midpoint of LM [55] ⇒  ∠LFM = ∠LEP [56]
-036. P is midpoint of LM [55] & Q is midpoint of LO [22] ⇒  PQ ∥ MO [57]
-037. Q,L,O are collinear [20] & ∠OLF = ∠OMF [52] & B,M,O are collinear [17] & ∠LFM = ∠LEP [56] & PQ ∥ MO [57] ⇒  ∠LEP = ∠LQP [58]
-038. ∠LEP = ∠LQP [58] ⇒  Q,L,P,E are concyclic [59]
-039. Q,L,P,E are concyclic [59] ⇒  ∠QLP = ∠QEP [60]
-040. EM = EL [54] & PL = PM [19] ⇒  ML ⟂ EP [61]
-041. ∠QLP = ∠QEP [60] & O,L,Q are collinear [20] & L,M,P are collinear [18] & L,M,A are collinear [12] & ML ⟂ EP [61] ⇒  OL ⟂ QE [62]
-042. Q is midpoint of LO [22] & OL ⟂ QE [62] ⇒  EO = EL [63]
-043. EO = EL [63] & EL = EF [10] ⇒  EF = EO
-==========================
-
-I0204 16:08:19.007035 139642560315392 alphageometry.py:195] Solution written to ag.out.
-I0204 20:43:09.655949 139642560315392 alphageometry.py:581] Solved.

ag4masses/outputs/solved/ceva_menelaus_hint-ag-ok.log

@@ -1,43 +0,0 @@
-I0218 15:36:12.138049 140279694163968 graph.py:498] ceva_menelaus_hint
-I0218 15:36:12.139024 140279694163968 graph.py:499] a b c = triangle; d = free; e = on_line b c, on_line a d; f = on_line c a, on_line b d; g = on_line a b, on_line c d; h = on_line c a, on_pline h b e f; i = on_line c d, on_pline i e a b; j = on_line b f, on_pline j e a c ? eqratio f h f a g b g a
-I0218 15:36:15.467568 140279694163968 alphageometry.py:191] 
-==========================
- * From theorem premises:
-A B C D E F G H : Points
-B,E,C are collinear [00]
-A,D,E are collinear [01]
-A,F,C are collinear [02]
-B,D,F are collinear [03]
-A,B,G are collinear [04]
-G,D,C are collinear [05]
-HB ∥ EF [06]
-A,H,C are collinear [07]
-
- * Auxiliary Constructions:
-I J : Points
-IE ∥ AB [08]
-D,I,C are collinear [09]
-JE ∥ AC [10]
-B,J,F are collinear [11]
-
- * Proof steps:
-001. A,B,G are collinear [04] & EI ∥ AB [08] ⇒  BG ∥ EI [12]
-002. D,I,C are collinear [09] & G,D,C are collinear [05] ⇒  C,G,I are collinear [13]
-003. D,I,C are collinear [09] & G,D,C are collinear [05] ⇒  D,G,I are collinear [14]
-004. BG ∥ EI [12] & B,E,C are collinear [00] & C,G,I are collinear [13] ⇒  BC:EC = BG:IE [15]
-005. A,H,C are collinear [07] & A,F,C are collinear [02] ⇒  C,H,F are collinear [16]
-006. BH ∥ EF [06] & B,E,C are collinear [00] & C,H,F are collinear [16] ⇒  BC:EC = BH:EF [17]
-007. A,H,C are collinear [07] & A,F,C are collinear [02] & BH ∥ EF [06] & AC ∥ EJ [10] ⇒  ∠BHF = ∠FEJ [18]
-008. B,D,F are collinear [03] & A,H,C are collinear [07] & A,F,C are collinear [02] & B,J,F are collinear [11] & AC ∥ EJ [10] ⇒  ∠BFH = ∠FJE [19]
-009. ∠BHF = ∠FEJ [18] & ∠BFH = ∠FJE [19] (Similar Triangles)⇒  BH:EF = HF:JE [20]
-010. BC:EC = BG:IE [15] & BC:EC = BH:EF [17] & BH:EF = HF:JE [20] ⇒  HF:JE = BG:IE [21]
-011. A,G,B are collinear [04] & EI ∥ AB [08] ⇒  AG ∥ EI [22]
-012. AG ∥ EI [22] & A,D,E are collinear [01] & D,G,I are collinear [14] ⇒  DE:AD = IE:AG [23]
-013. A,C,F are collinear [02] & EJ ∥ AC [10] ⇒  JE ∥ FA [24]
-014. B,J,F are collinear [11] & B,D,F are collinear [03] ⇒  D,J,F are collinear [25]
-015. JE ∥ FA [24] & A,D,E are collinear [01] & D,J,F are collinear [25] ⇒  DE:AD = JE:AF [26]
-016. DE:AD = IE:AG [23] & DE:AD = JE:AF [26] ⇒  JE:AF = IE:AG [27]
-017. HF:JE = BG:IE [21] & JE:AF = IE:AG [27] ⇒  HF:AF = BG:AG
-==========================
-
-I0218 15:36:15.468291 140279694163968 alphageometry.py:195] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out4.

ag4masses/outputs/solved/gaolian100-12-ag-ok.log

@@ -1,717 +0,0 @@
-++ BATCH_SIZE=24
-++ BEAM_SIZE=64
-++ DEPTH=8
-++ NWORKERS=8
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt
-++ PROB=gaolian100-12
-++ MODEL=alphageometry
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt --problem_name=gaolian100-12 --mode=alphageometry --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=64 --search_depth=8 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=24 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out --n_workers=8
-I0406 21:02:04.637060 135279079972864 graph.py:498] gaolian100-12
-I0406 21:02:04.637331 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f ? cong c g c h
-I0406 21:02:08.278219 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:02:08.293032 135279079972864 alphageometry.py:522] Worker initializing. PID=2866
-I0406 21:02:08.304146 135279079972864 alphageometry.py:522] Worker initializing. PID=2867
-I0406 21:02:08.313952 135279079972864 alphageometry.py:522] Worker initializing. PID=2868
-I0406 21:02:08.325267 135279079972864 alphageometry.py:522] Worker initializing. PID=2869
-I0406 21:02:08.336427 135279079972864 alphageometry.py:522] Worker initializing. PID=2900
-I0406 21:02:08.347604 135279079972864 alphageometry.py:522] Worker initializing. PID=2980
-I0406 21:02:08.358955 135279079972864 alphageometry.py:522] Worker initializing. PID=3061
-I0406 21:02:08.373842 135279079972864 alphageometry.py:651] Depth 0. There are 1 nodes to expand:
-I0406 21:02:08.375748 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00
-I0406 21:02:08.373595 135279079972864 alphageometry.py:522] Worker initializing. PID=3092
-I0406 21:02:49.498787 135279079972864 alphageometry.py:527] Worker PID=2867 called for beam search node 0
-I0406 21:02:49.499006 135279079972864 alphageometry.py:530] Worker PID=2867: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00
-I0406 21:13:56.945881 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_circle i a g, on_tline i a a g"
-I0406 21:13:56.946334 135279079972864 graph.py:498] 
-I0406 21:13:56.946453 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g, on_tline i a a g ? cong c g c h
-I0406 21:14:03.930609 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:03.930845 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i g a g"
-I0406 21:14:03.931167 135279079972864 graph.py:498] 
-I0406 21:14:03.931272 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g a g ? cong c g c h
-I0406 21:14:08.306693 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:08.306905 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = eqdistance i f b d, eqdistance i b d f"
-I0406 21:14:08.307243 135279079972864 graph.py:498] 
-I0406 21:14:08.307356 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i f b d, eqdistance i b d f ? cong c g c h
-I0406 21:14:16.438935 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:16.439152 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i g c g"
-I0406 21:14:16.439466 135279079972864 graph.py:498] 
-I0406 21:14:16.439598 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g ? cong c g c h
-I0406 21:14:20.761389 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:20.761627 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_circle i d b, on_tline i d b d"
-I0406 21:14:20.761930 135279079972864 graph.py:498] 
-I0406 21:14:20.762036 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d ? cong c g c h
-I0406 21:14:30.414432 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:30.414695 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_circle i a g"
-I0406 21:14:30.415171 135279079972864 graph.py:498] 
-I0406 21:14:30.415279 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g ? cong c g c h
-I0406 21:14:34.602563 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:34.602819 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i a a d"
-I0406 21:14:34.603156 135279079972864 graph.py:498] 
-I0406 21:14:34.603270 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d ? cong c g c h
-I0406 21:14:38.816597 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:38.816833 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = eqdistance i e b d, on_pline i e b d"
-I0406 21:14:38.817201 135279079972864 graph.py:498] 
-I0406 21:14:38.817309 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d ? cong c g c h
-I0406 21:14:44.272838 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:44.273066 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i f a d"
-I0406 21:14:44.273362 135279079972864 graph.py:498] 
-I0406 21:14:44.273469 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i f a d ? cong c g c h
-I0406 21:14:48.564496 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:48.564748 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_circle i e b, on_tline i e b e"
-I0406 21:14:48.565085 135279079972864 graph.py:498] 
-I0406 21:14:48.565196 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i e b, on_tline i e b e ? cong c g c h
-I0406 21:14:57.972463 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:14:57.972725 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i c a d"
-I0406 21:14:57.973040 135279079972864 graph.py:498] 
-I0406 21:14:57.973146 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i c a d ? cong c g c h
-I0406 21:15:04.119190 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:04.119508 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = eqdistance i e b d, eqdistance i b d e"
-I0406 21:15:04.119842 135279079972864 graph.py:498] 
-I0406 21:15:04.119958 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, eqdistance i b d e ? cong c g c h
-I0406 21:15:09.003309 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:09.003546 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_circle i d b, on_tline i b a d"
-I0406 21:15:09.003843 135279079972864 graph.py:498] 
-I0406 21:15:09.003956 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i b a d ? cong c g c h
-I0406 21:15:16.884920 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:16.885142 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i f a d, on_tline i a c f"
-I0406 21:15:16.885437 135279079972864 graph.py:498] 
-I0406 21:15:16.885537 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i f a d, on_tline i a c f ? cong c g c h
-I0406 21:15:22.199810 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:22.200044 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i d a d"
-I0406 21:15:22.200363 135279079972864 graph.py:498] 
-I0406 21:15:22.200474 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i d a d ? cong c g c h
-I0406 21:15:27.122571 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:27.122815 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i f c g"
-I0406 21:15:27.123185 135279079972864 graph.py:498] 
-I0406 21:15:27.123303 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i f c g ? cong c g c h
-I0406 21:15:31.335536 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:31.335802 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = eqdistance i f b d, eqdistance i d b f"
-I0406 21:15:31.336160 135279079972864 graph.py:498] 
-I0406 21:15:31.336274 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i f b d, eqdistance i d b f ? cong c g c h
-I0406 21:15:36.526077 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:36.526310 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_circle i a g, on_circle i d g"
-I0406 21:15:36.526664 135279079972864 graph.py:498] 
-I0406 21:15:36.526772 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g, on_circle i d g ? cong c g c h
-I0406 21:15:48.296082 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:48.296318 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i d c d"
-I0406 21:15:48.296624 135279079972864 graph.py:498] 
-I0406 21:15:48.296736 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i d c d ? cong c g c h
-I0406 21:15:52.434981 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:52.435211 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i f b d, on_tline i b d f"
-I0406 21:15:52.435536 135279079972864 graph.py:498] 
-I0406 21:15:52.435616 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i f b d, on_tline i b d f ? cong c g c h
-I0406 21:15:57.832671 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:15:57.832907 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_bline i e a, on_pline i a c e"
-I0406 21:15:57.833286 135279079972864 graph.py:498] 
-I0406 21:15:57.833390 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_bline i e a, on_pline i a c e ? cong c g c h
-I0406 21:16:09.423190 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:16:09.423428 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i a a g"
-I0406 21:16:09.423742 135279079972864 graph.py:498] 
-I0406 21:16:09.423850 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a g ? cong c g c h
-I0406 21:16:13.777367 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:16:13.777575 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i e a e"
-I0406 21:16:13.777849 135279079972864 graph.py:498] 
-I0406 21:16:13.777960 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i e a e ? cong c g c h
-I0406 21:16:18.341279 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:16:18.341541 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "i = on_tline i e c g"
-I0406 21:16:18.341862 135279079972864 graph.py:498] 
-I0406 21:16:18.341978 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i e c g ? cong c g c h
-I0406 21:16:22.745383 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:16:22.745531 135279079972864 alphageometry.py:587] Worker PID=2867 beam search node 0: returning
-I0406 21:16:24.331641 135279079972864 alphageometry.py:651] Depth 1. There are 24 nodes to expand:
-I0406 21:16:24.331839 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D a g a i 10 T a g a i 11 ; x00
-I0406 21:16:24.331892 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a g g i 10 ; x00
-I0406 21:16:24.331933 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d f i 10 D b i d f 11 ; x00
-I0406 21:16:24.331971 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T c g g i 10 ; x00
-I0406 21:16:24.332006 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d d i 10 T b d d i 11 ; x00
-I0406 21:16:24.332041 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D a g a i 10 ; x00
-I0406 21:16:24.332075 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d a i 10 ; x00
-I0406 21:16:24.332113 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d e i 10 P b d e i 11 ; x00
-I0406 21:16:24.332154 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d f i 10 ; x00
-I0406 21:16:24.332188 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b e e i 10 T b e e i 11 ; x00
-I0406 21:16:24.332222 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d c i 10 ; x00
-I0406 21:16:24.332256 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d e i 10 D b i d e 11 ; x00
-I0406 21:16:24.332289 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d d i 10 T a d b i 11 ; x00
-I0406 21:16:24.332323 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d f i 10 T a i c f 11 ; x00
-I0406 21:16:24.332356 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d d i 10 ; x00
-I0406 21:16:24.332393 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T c g f i 10 ; x00
-I0406 21:16:24.332427 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d f i 10 D b f d i 11 ; x00
-I0406 21:16:24.332461 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D a g a i 10 D d g d i 11 ; x00
-I0406 21:16:24.332494 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T c d d i 10 ; x00
-I0406 21:16:24.332528 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T b d f i 10 T b i d f 11 ; x00
-I0406 21:16:24.332560 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D a i e i 10 P a i c e 11 ; x00
-I0406 21:16:24.332593 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a g a i 10 ; x00
-I0406 21:16:24.332636 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a e e i 10 ; x00
-I0406 21:16:24.332669 135279079972864 alphageometry.py:655] {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T c g e i 10 ; x00
-I0406 21:16:24.343865 135279079972864 alphageometry.py:527] Worker PID=2869 called for beam search node 0
-I0406 21:16:24.344102 135279079972864 alphageometry.py:530] Worker PID=2869: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D a g a i 10 T a g a i 11 ; x00
-I0406 21:16:24.349621 135279079972864 alphageometry.py:527] Worker PID=2980 called for beam search node 1
-I0406 21:16:24.349802 135279079972864 alphageometry.py:530] Worker PID=2980: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a g g i 10 ; x00
-I0406 21:16:24.361777 135279079972864 alphageometry.py:527] Worker PID=3092 called for beam search node 2
-I0406 21:16:24.362129 135279079972864 alphageometry.py:530] Worker PID=3092: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d f i 10 D b i d f 11 ; x00
-I0406 21:16:24.367914 135279079972864 alphageometry.py:527] Worker PID=2900 called for beam search node 3
-I0406 21:16:24.368237 135279079972864 alphageometry.py:530] Worker PID=2900: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T c g g i 10 ; x00
-I0406 21:16:24.377397 135279079972864 alphageometry.py:527] Worker PID=3061 called for beam search node 4
-I0406 21:16:24.377711 135279079972864 alphageometry.py:530] Worker PID=3061: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d d i 10 T b d d i 11 ; x00
-I0406 21:16:24.384681 135279079972864 alphageometry.py:527] Worker PID=2868 called for beam search node 5
-I0406 21:16:24.385004 135279079972864 alphageometry.py:530] Worker PID=2868: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D a g a i 10 ; x00
-I0406 21:16:24.389691 135279079972864 alphageometry.py:527] Worker PID=2866 called for beam search node 6
-I0406 21:16:24.390028 135279079972864 alphageometry.py:530] Worker PID=2866: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d a i 10 ; x00
-I0406 21:16:24.399608 135279079972864 alphageometry.py:527] Worker PID=2867 called for beam search node 7
-I0406 21:16:24.399883 135279079972864 alphageometry.py:530] Worker PID=2867: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b d e i 10 P b d e i 11 ; x00
-I0406 21:34:44.569499 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j g c g"
-I0406 21:34:44.570352 135279079972864 graph.py:498] 
-I0406 21:34:44.570582 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j g c g ? cong c g c h
-I0406 21:34:58.049735 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:34:58.050385 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f c g"
-I0406 21:34:58.051663 135279079972864 graph.py:498] 
-I0406 21:34:58.052101 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f c g ? cong c g c h
-I0406 21:35:04.055794 135279079972864 alphageometry.py:549] Worker PID=2980: Translation: "j = on_line j d f, on_bline j f d"
-I0406 21:35:04.056796 135279079972864 graph.py:498] 
-I0406 21:35:04.057057 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g a g; j = on_line j d f, on_bline j f d ? cong c g c h
-I0406 21:35:10.207267 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:10.207506 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j g a g"
-I0406 21:35:10.207924 135279079972864 graph.py:498] 
-I0406 21:35:10.208041 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j g a g ? cong c g c h
-I0406 21:35:18.224543 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:18.224733 135279079972864 alphageometry.py:549] Worker PID=2980: Translation: "j = on_line j c d, on_circle j c d"
-I0406 21:35:18.225127 135279079972864 graph.py:498] 
-I0406 21:35:18.225236 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g a g; j = on_line j c d, on_circle j c d ? cong c g c h
-I0406 21:35:21.336542 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:21.336846 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j e b e"
-I0406 21:35:21.339354 135279079972864 graph.py:498] 
-I0406 21:35:21.339623 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j e b e ? cong c g c h
-I0406 21:35:35.422725 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:35.423094 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f f g"
-I0406 21:35:35.423927 135279079972864 graph.py:498] 
-I0406 21:35:35.424194 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f f g ? cong c g c h
-I0406 21:35:47.282572 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:47.283175 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j e a e"
-I0406 21:35:47.284379 135279079972864 graph.py:498] 
-I0406 21:35:47.284843 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j e a e ? cong c g c h
-I0406 21:35:47.961218 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:47.961620 135279079972864 alphageometry.py:549] Worker PID=2980: Translation: "j = on_line j c d, on_bline j d c"
-I0406 21:35:47.962604 135279079972864 graph.py:498] 
-I0406 21:35:47.962907 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g a g; j = on_line j c d, on_bline j d c ? cong c g c h
-I0406 21:35:54.152234 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_circle j i g, on_pline j i c g"
-I0406 21:35:54.152926 135279079972864 graph.py:498] 
-I0406 21:35:54.153108 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_circle j i g, on_pline j i c g ? cong c g c h
-I0406 21:35:58.792886 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:58.793093 135279079972864 alphageometry.py:549] Worker PID=2980: Translation: "j = on_line j d e, on_bline j e d"
-I0406 21:35:58.793512 135279079972864 graph.py:498] 
-I0406 21:35:58.793627 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g a g; j = on_line j d e, on_bline j e d ? cong c g c h
-I0406 21:35:59.969265 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:35:59.969680 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f c h"
-I0406 21:35:59.970638 135279079972864 graph.py:498] 
-I0406 21:35:59.970931 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f c h ? cong c g c h
-I0406 21:36:07.810665 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:07.811211 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_circle j a g"
-I0406 21:36:07.812321 135279079972864 graph.py:498] 
-I0406 21:36:07.812585 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_circle j a g ? cong c g c h
-I0406 21:36:09.361270 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_line j d f, on_bline j f d"
-I0406 21:36:09.361698 135279079972864 graph.py:498] 
-I0406 21:36:09.361810 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_line j d f, on_bline j f d ? cong c g c h
-I0406 21:36:09.970334 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:09.970793 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f b d, on_tline j d b f"
-I0406 21:36:09.971568 135279079972864 graph.py:498] 
-I0406 21:36:09.971765 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f b d, on_tline j d b f ? cong c g c h
-I0406 21:36:16.590908 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:16.591608 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = eqdistance j e b d, on_pline j e b d"
-I0406 21:36:16.592999 135279079972864 graph.py:498] 
-I0406 21:36:16.593404 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = eqdistance j e b d, on_pline j e b d ? cong c g c h
-I0406 21:36:20.248831 135279079972864 alphageometry.py:201] 
-==========================
- * From theorem premises:
-A B C D E F G H : Points
-CA = CB [00]
-A,C,B are collinear [01]
-CD = CA [02]
-CE = CA [03]
-D,F,E are collinear [04]
-BF ⟂ AB [05]
-A,G,E are collinear [06]
-C,G,F are collinear [07]
-D,A,H are collinear [08]
-H,C,F are collinear [09]
-
- * Auxiliary Constructions:
-J : Points
-D,J,E are collinear [10]
-JE = JD [11]
-
- * Proof steps:
-001. CE = CA [03] & CA = CB [00] ⇒  AB:CB = AB:CB [12]
-002. CD = CA [02] & CE = CA [03] & CA = CB [00] ⇒  D,A,B,E are concyclic [13]
-003. D,A,B,E are concyclic [13] ⇒  ∠BAD = ∠BED [14]
-004. D,A,B,E are concyclic [13] ⇒  ∠BDE = ∠BAE [15]
-005. D,J,E are collinear [10] & A,C,B are collinear [01] & D,A,H are collinear [08] & ∠BED = ∠BAD [14] ⇒  ∠BEJ = ∠CAH [16]
-006. CE = CA [03] & CD = CA [02] ⇒  CD = CE [17]
-007. CD = CE [17] & JE = JD [11] ⇒  DE ⟂ CJ [18]
-008. D,J,E are collinear [10] & D,F,E are collinear [04] & A,C,B are collinear [01] & BF ⟂ AB [05] & DE ⟂ CJ [18] ⇒  ∠FJC = ∠FBC [19]
-009. ∠FJC = ∠FBC [19] ⇒  C,B,F,J are concyclic [20]
-010. C,B,F,J are concyclic [20] ⇒  ∠CBJ = ∠CFJ [21]
-011. D,J,E are collinear [10] & A,C,B are collinear [01] & H,C,F are collinear [09] & ∠CBJ = ∠CFJ [21] & D,F,E are collinear [04] ⇒  ∠BJE = ∠ACH [22]
-012. ∠BEJ = ∠CAH [16] & ∠BJE = ∠ACH [22] (Similar Triangles)⇒  JB:JE = CH:CA [23]
-013. D,J,E are collinear [10] & A,C,B are collinear [01] & A,G,E are collinear [06] & ∠BDE = ∠BAE [15] ⇒  ∠BDJ = ∠CAG [24]
-014. D,J,E are collinear [10] & A,C,B are collinear [01] & C,G,F are collinear [07] & ∠CBJ = ∠CFJ [21] & D,F,E are collinear [04] ⇒  ∠BJD = ∠ACG [25]
-015. ∠BDJ = ∠CAG [24] & ∠BJD = ∠ACG [25] (Similar Triangles)⇒  JB:JD = CG:CA [26]
-016. JB:JE = CH:CA [23] & JE = JD [11] & CE = CA [03] & JB:JD = CG:CA [26] & CA = CB [00] ⇒  CB:CG = CB:HC [27]
-017. AB:CB = AB:CB [12] & CB:CG = CB:HC [27] ⇒  CG = HC
-==========================
-
-I0406 21:36:20.249316 135279079972864 alphageometry.py:205] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.
-I0406 21:36:20.645020 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:20.645223 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j e d e"
-I0406 21:36:20.645624 135279079972864 graph.py:498] 
-I0406 21:36:20.645737 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j e d e ? cong c g c h
-I0406 21:36:23.653055 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:23.653348 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_tline j g c g"
-I0406 21:36:23.653846 135279079972864 graph.py:498] 
-I0406 21:36:23.653970 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_tline j g c g ? cong c g c h
-I0406 21:36:27.031312 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:27.031643 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_circle j d b, on_tline j d b d"
-I0406 21:36:27.032306 135279079972864 graph.py:498] 
-I0406 21:36:27.032487 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_circle j d b, on_tline j d b d ? cong c g c h
-I0406 21:36:29.715667 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:29.715946 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/alphageometry.py", line 470, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/graph.py", line 2637, in add_clause
-    raise PointTooFarError()
-graph.PointTooFarError
-"
-I0406 21:36:29.716192 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_line j d f, on_bline j f d"
-I0406 21:36:29.716957 135279079972864 graph.py:498] 
-I0406 21:36:29.717258 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_line j d f, on_bline j f d ? cong c g c h
-I0406 21:36:32.949274 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:32.949479 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_line j e f, on_bline j f e"
-I0406 21:36:32.949885 135279079972864 graph.py:498] 
-I0406 21:36:32.950003 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_line j e f, on_bline j f e ? cong c g c h
-I0406 21:36:41.680137 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:41.680413 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j b b e"
-I0406 21:36:41.680746 135279079972864 graph.py:498] 
-I0406 21:36:41.680859 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j b b e ? cong c g c h
-I0406 21:36:46.137916 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:46.138115 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_tline j e a g"
-I0406 21:36:46.138513 135279079972864 graph.py:498] 
-I0406 21:36:46.138630 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_tline j e a g ? cong c g c h
-I0406 21:36:46.981028 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:46.981215 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = eqdistance j i c g, eqdistance j c g i"
-I0406 21:36:46.981653 135279079972864 graph.py:498] 
-I0406 21:36:46.981772 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = eqdistance j i c g, eqdistance j c g i ? cong c g c h
-I0406 21:36:51.426852 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:51.427627 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j d d f"
-I0406 21:36:51.428849 135279079972864 graph.py:498] 
-I0406 21:36:51.429218 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j d d f ? cong c g c h
-I0406 21:36:57.077456 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:36:57.077900 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_tline j f a d, on_tline j a d f"
-I0406 21:36:57.078405 135279079972864 graph.py:498] 
-I0406 21:36:57.078583 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_tline j f a d, on_tline j a d f ? cong c g c h
-I0406 21:37:00.467643 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:00.467977 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j i a g"
-I0406 21:37:00.468417 135279079972864 graph.py:498] 
-I0406 21:37:00.468530 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j i a g ? cong c g c h
-I0406 21:37:02.528216 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:02.528428 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_circle j e b, on_tline j e b e"
-I0406 21:37:02.528862 135279079972864 graph.py:498] 
-I0406 21:37:02.528984 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_circle j e b, on_tline j e b e ? cong c g c h
-I0406 21:37:09.236507 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:09.236723 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f a g"
-I0406 21:37:09.237131 135279079972864 graph.py:498] 
-I0406 21:37:09.237249 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f a g ? cong c g c h
-I0406 21:37:09.724565 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:09.725005 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_bline j e a, on_pline j e a c"
-I0406 21:37:09.725809 135279079972864 graph.py:498] 
-I0406 21:37:09.726027 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_bline j e a, on_pline j e a c ? cong c g c h
-I0406 21:37:17.533022 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:17.533642 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f a d"
-I0406 21:37:17.534647 135279079972864 graph.py:498] 
-I0406 21:37:17.534846 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f a d ? cong c g c h
-I0406 21:37:17.811438 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j a g"
-I0406 21:37:17.812013 135279079972864 graph.py:498] 
-I0406 21:37:17.812188 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j a g ? cong c g c h
-I0406 21:37:20.141452 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:20.141658 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_circle j g c, on_circle j i c"
-I0406 21:37:20.142048 135279079972864 graph.py:498] 
-I0406 21:37:20.142148 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_circle j g c, on_circle j i c ? cong c g c h
-I0406 21:37:25.062191 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:25.062385 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j d f g"
-I0406 21:37:25.062779 135279079972864 graph.py:498] 
-I0406 21:37:25.062888 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j d f g ? cong c g c h
-I0406 21:37:27.287778 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:27.287961 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j i a, on_pline j i a g"
-I0406 21:37:27.288327 135279079972864 graph.py:498] 
-I0406 21:37:27.288454 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j i a, on_pline j i a g ? cong c g c h
-I0406 21:37:31.861815 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:31.862011 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = eqdistance j f b d, eqdistance j d b f"
-I0406 21:37:31.862457 135279079972864 graph.py:498] 
-I0406 21:37:31.862594 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = eqdistance j f b d, eqdistance j d b f ? cong c g c h
-I0406 21:37:32.255301 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:32.255503 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f b d, on_tline j b d f"
-I0406 21:37:32.255910 135279079972864 graph.py:498] 
-I0406 21:37:32.256016 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f b d, on_tline j b d f ? cong c g c h
-I0406 21:37:38.904896 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:38.905115 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j g a"
-I0406 21:37:38.905497 135279079972864 graph.py:498] 
-I0406 21:37:38.905614 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j g a ? cong c g c h
-I0406 21:37:45.942854 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:45.943288 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j f g, on_bline j g f"
-I0406 21:37:45.944226 135279079972864 graph.py:498] 
-I0406 21:37:45.944470 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j f g, on_bline j g f ? cong c g c h
-I0406 21:37:46.129451 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:46.129663 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = eqdistance j f b d, eqdistance j b d f"
-I0406 21:37:46.130024 135279079972864 graph.py:498] 
-I0406 21:37:46.130141 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = eqdistance j f b d, eqdistance j b d f ? cong c g c h
-I0406 21:37:46.333416 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:46.333612 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f b e, on_tline j e b f"
-I0406 21:37:46.333992 135279079972864 graph.py:498] 
-I0406 21:37:46.334098 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f b e, on_tline j e b f ? cong c g c h
-I0406 21:37:50.596647 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:50.596966 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_bline j e a, on_circle j e c"
-I0406 21:37:50.597499 135279079972864 graph.py:498] 
-I0406 21:37:50.597680 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_bline j e a, on_circle j e c ? cong c g c h
-I0406 21:37:55.204475 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:55.204856 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/alphageometry.py", line 470, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/graph.py", line 2637, in add_clause
-    raise PointTooFarError()
-graph.PointTooFarError
-"
-I0406 21:37:55.205193 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "ERROR: point m does not exist."
-I0406 21:37:55.205496 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f c f"
-I0406 21:37:55.206369 135279079972864 graph.py:498] 
-I0406 21:37:55.206668 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f c f ? cong c g c h
-I0406 21:37:56.761510 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:37:56.761708 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j i a, on_bline j i g"
-I0406 21:37:56.762120 135279079972864 graph.py:498] 
-I0406 21:37:56.762236 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j i a, on_bline j i g ? cong c g c h
-I0406 21:38:00.203181 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:00.203947 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_circle j g b, on_circle j i b"
-I0406 21:38:00.205290 135279079972864 graph.py:498] 
-I0406 21:38:00.205653 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_circle j g b, on_circle j i b ? cong c g c h
-I0406 21:38:03.093170 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:03.093492 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_tline j f b e"
-I0406 21:38:03.093988 135279079972864 graph.py:498] 
-I0406 21:38:03.094102 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_tline j f b e ? cong c g c h
-I0406 21:38:06.277068 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:06.277499 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j d f, on_bline j f d"
-I0406 21:38:06.278472 135279079972864 graph.py:498] 
-I0406 21:38:06.278775 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j d f, on_bline j f d ? cong c g c h
-I0406 21:38:09.501839 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:09.502068 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_line j c d, on_bline j d c"
-I0406 21:38:09.502479 135279079972864 graph.py:498] 
-I0406 21:38:09.502599 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_line j c d, on_bline j d c ? cong c g c h
-I0406 21:38:10.931700 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:10.931901 135279079972864 alphageometry.py:549] Worker PID=2866: Translation: "j = on_circle j e b"
-I0406 21:38:10.932282 135279079972864 graph.py:498] 
-I0406 21:38:10.932393 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i a a d; j = on_circle j e b ? cong c g c h
-I0406 21:38:11.518033 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:11.518240 135279079972864 alphageometry.py:549] Worker PID=2867: Translation: "j = on_line j d e, on_bline j e d"
-I0406 21:38:11.518603 135279079972864 graph.py:498] 
-I0406 21:38:11.518743 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i e b d, on_pline i e b d; j = on_line j d e, on_bline j e d ? cong c g c h
-I0406 21:38:15.640065 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:15.640356 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j f h, on_bline j h f"
-I0406 21:38:15.640886 135279079972864 graph.py:498] 
-I0406 21:38:15.641034 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j f h, on_bline j h f ? cong c g c h
-I0406 21:38:17.513923 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:17.514285 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_line j c d, on_circle j c d"
-I0406 21:38:17.515101 135279079972864 graph.py:498] 
-I0406 21:38:17.515330 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_line j c d, on_circle j c d ? cong c g c h
-I0406 21:38:18.017590 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:18.017823 135279079972864 alphageometry.py:587] Worker PID=2866 beam search node 6: returning
-I0406 21:38:18.204073 135279079972864 alphageometry.py:527] Worker PID=2866 called for beam search node 8
-I0406 21:38:18.204339 135279079972864 alphageometry.py:530] Worker PID=2866: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d f i 10 ; x00
-I0406 21:38:26.579273 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:26.579579 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/alphageometry.py", line 470, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/graph.py", line 2635, in add_clause
-    raise PointTooCloseError()
-graph.PointTooCloseError
-"
-I0406 21:38:26.580100 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j c d, on_bline j d c"
-I0406 21:38:26.580790 135279079972864 graph.py:498] 
-I0406 21:38:26.581004 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j c d, on_bline j d c ? cong c g c h
-I0406 21:38:30.064866 135279079972864 alphageometry.py:201] 
-==========================
- * From theorem premises:
-A B C D E F G H : Points
-B,C,A are collinear [00]
-CA = CB [01]
-CD = CA [02]
-CE = CA [03]
-F,D,E are collinear [04]
-BF ⟂ AB [05]
-G,A,E are collinear [06]
-F,C,G are collinear [07]
-H,A,D are collinear [08]
-F,C,H are collinear [09]
-
- * Auxiliary Constructions:
-J : Points
-J,D,E are collinear [10]
-JE = JD [11]
-
- * Proof steps:
-001. CA = CE [03] ⇒  BA:CA = BA:CA [12]
-002. CA = CB [01] & CE = CA [03] & CD = CA [02] ⇒  B,A,D,E are concyclic [13]
-003. B,A,D,E are concyclic [13] ⇒  ∠BAD = ∠BED [14]
-004. B,A,D,E are concyclic [13] ⇒  ∠BAE = ∠BDE [15]
-005. D,J,E are collinear [10] & B,C,A are collinear [00] & D,A,H are collinear [08] & ∠BED = ∠BAD [14] ⇒  ∠BEJ = ∠CAH [16]
-006. CE = CA [03] & CD = CA [02] ⇒  CD = CE [17]
-007. CD = CE [17] & JE = JD [11] ⇒  DE ⟂ CJ [18]
-008. B,C,A are collinear [00] & D,J,E are collinear [10] & F,D,E are collinear [04] & DE ⟂ CJ [18] & BF ⟂ AB [05] ⇒  ∠CBF = ∠CJF [19]
-009. ∠CBF = ∠CJF [19] ⇒  B,C,F,J are concyclic [20]
-010. B,C,F,J are concyclic [20] ⇒  ∠BCF = ∠BJF [21]
-011. D,J,E are collinear [10] & B,C,A are collinear [00] & F,C,H are collinear [09] & ∠BCF = ∠BJF [21] & F,D,E are collinear [04] ⇒  ∠BJE = ∠ACH [22]
-012. ∠BEJ = ∠CAH [16] & ∠BJE = ∠ACH [22] (Similar Triangles)⇒  JB:JE = CH:CA [23]
-013. J,D,E are collinear [10] & B,C,A are collinear [00] & G,A,E are collinear [06] & ∠BDE = ∠BAE [15] ⇒  ∠BDJ = ∠CAG [24]
-014. D,J,E are collinear [10] & B,C,A are collinear [00] & F,C,G are collinear [07] & ∠BCF = ∠BJF [21] & F,D,E are collinear [04] ⇒  ∠BJD = ∠ACG [25]
-015. ∠BDJ = ∠CAG [24] & ∠BJD = ∠ACG [25] (Similar Triangles)⇒  JB:JD = CG:CA [26]
-016. JB:JE = CH:CA [23] & JE = JD [11] & CE = CA [03] & JB:JD = CG:CA [26] ⇒  CA:CG = CA:CH [27]
-017. BA:CA = BA:CA [12] & CA:CG = CA:CH [27] ⇒  CG = CH
-==========================
-
-I0406 21:38:30.065437 135279079972864 alphageometry.py:205] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.
-I0406 21:38:34.469381 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:34.469591 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = eqdistance j f a g, on_pline j f a g"
-I0406 21:38:34.470004 135279079972864 graph.py:498] 
-I0406 21:38:34.470118 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = eqdistance j f a g, on_pline j f a g ? cong c g c h
-I0406 21:38:39.136036 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:39.136258 135279079972864 alphageometry.py:549] Worker PID=2900: Translation: "j = on_line j d e, on_bline j e d"
-I0406 21:38:39.136672 135279079972864 graph.py:498] 
-I0406 21:38:39.136780 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_tline i g c g; j = on_line j d e, on_bline j e d ? cong c g c h
-I0406 21:38:43.400059 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:43.400297 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j i a"
-I0406 21:38:43.400664 135279079972864 graph.py:498] 
-I0406 21:38:43.400782 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j i a ? cong c g c h
-I0406 21:38:43.999250 135279079972864 alphageometry.py:549] Worker PID=3092: Translation: "j = on_circle j b g, on_circle j d g"
-I0406 21:38:44.000010 135279079972864 graph.py:498] 
-I0406 21:38:44.000227 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i f b d, eqdistance i b d f; j = on_circle j b g, on_circle j d g ? cong c g c h
-I0406 21:38:49.713116 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:49.713308 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/alphageometry.py", line 470, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/graph.py", line 2635, in add_clause
-    raise PointTooCloseError()
-graph.PointTooCloseError
-"
-I0406 21:38:49.713453 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_tline j f a d"
-I0406 21:38:49.713856 135279079972864 graph.py:498] 
-I0406 21:38:49.713969 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_tline j f a d ? cong c g c h
-I0406 21:38:53.238985 135279079972864 alphageometry.py:201] 
-==========================
- * From theorem premises:
-A B C D E F G H : Points
-C,A,B are collinear [00]
-CA = CB [01]
-CD = CA [02]
-CE = CA [03]
-E,D,F are collinear [04]
-BF ⟂ AB [05]
-C,G,F are collinear [06]
-A,E,G are collinear [07]
-C,H,F are collinear [08]
-A,H,D are collinear [09]
-
- * Auxiliary Constructions:
-J : Points
-E,D,J are collinear [10]
-JE = JD [11]
-
- * Proof steps:
-001. CA = CE [03] ⇒  AB:CA = AB:CA [12]
-002. CD = CA [02] & CE = CA [03] ⇒  CE = CD [13]
-003. CE = CD [13] & JE = JD [11] ⇒  DE ⟂ CJ [14]
-004. C,A,B are collinear [00] & E,D,J are collinear [10] & E,D,F are collinear [04] & DE ⟂ CJ [14] & BF ⟂ AB [05] ⇒  ∠FBC = ∠FJC [15]
-005. ∠FBC = ∠FJC [15] ⇒  C,B,J,F are concyclic [16]
-006. C,B,J,F are concyclic [16] ⇒  ∠CBJ = ∠CFJ [17]
-007. C,H,F are collinear [08] & C,A,B are collinear [00] & E,D,J are collinear [10] & ∠CBJ = ∠CFJ [17] & E,D,F are collinear [04] ⇒  ∠HCA = ∠EJB [18]
-008. CD = CA [02] & CE = CA [03] & CA = CB [01] ⇒  A,E,B,D are concyclic [19]
-009. A,E,B,D are concyclic [19] ⇒  ∠BAD = ∠BED [20]
-010. A,E,B,D are concyclic [19] ⇒  ∠EAB = ∠EDB [21]
-011. E,D,J are collinear [10] & C,A,B are collinear [00] & A,H,D are collinear [09] & ∠BED = ∠BAD [20] ⇒  ∠BEJ = ∠CAH [22]
-012. ∠HCA = ∠EJB [18] & ∠BEJ = ∠CAH [22] (Similar Triangles)⇒  CH:CA = JB:JE [23]
-013. C,F,G are collinear [06] & C,A,B are collinear [00] & E,D,J are collinear [10] & ∠CBJ = ∠CFJ [17] & E,D,F are collinear [04] ⇒  ∠GCA = ∠DJB [24]
-014. A,E,G are collinear [07] & C,A,B are collinear [00] & E,D,J are collinear [10] & ∠EAB = ∠EDB [21] ⇒  ∠GAC = ∠JDB [25]
-015. ∠GCA = ∠DJB [24] & ∠GAC = ∠JDB [25] (Similar Triangles)⇒  CG:CA = JB:JD [26]
-016. CH:CA = JB:JE [23] & CE = CA [03] & JE = JD [11] & CG:CA = JB:JD [26] ⇒  CA:CG = CA:CH [27]
-017. AB:CA = AB:CA [12] & CA:CG = CA:CH [27] ⇒  CG = CH
-==========================
-
-I0406 21:38:53.239541 135279079972864 alphageometry.py:205] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.
-I0406 21:38:54.720835 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_bline j i b, on_circle j i d"
-I0406 21:38:54.721310 135279079972864 graph.py:498] 
-I0406 21:38:54.721446 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_bline j i b, on_circle j i d ? cong c g c h
-I0406 21:38:56.126976 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:38:56.127166 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j d b, on_tline j d b d"
-I0406 21:38:56.127589 135279079972864 graph.py:498] 
-I0406 21:38:56.127710 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j d b, on_tline j d b d ? cong c g c h
-I0406 21:39:00.638771 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:00.639181 135279079972864 alphageometry.py:549] Worker PID=3092: Translation: "j = on_line j d f, on_bline j f d"
-I0406 21:39:00.640205 135279079972864 graph.py:498] 
-I0406 21:39:00.640492 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i f b d, eqdistance i b d f; j = on_line j d f, on_bline j f d ? cong c g c h
-I0406 21:39:07.888156 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:07.888344 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j a g, on_tline j a a g"
-I0406 21:39:07.888679 135279079972864 graph.py:498] 
-I0406 21:39:07.888788 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j a g, on_tline j a a g ? cong c g c h
-I0406 21:39:15.073183 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:15.073381 135279079972864 alphageometry.py:549] Worker PID=3092: Translation: "j = on_line j d i, on_bline j i d"
-I0406 21:39:15.073718 135279079972864 graph.py:498] 
-I0406 21:39:15.073836 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i f b d, eqdistance i b d f; j = on_line j d i, on_bline j i d ? cong c g c h
-I0406 21:39:15.650620 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:15.650794 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_circle j b i, on_tline j b b i"
-I0406 21:39:15.651189 135279079972864 graph.py:498] 
-I0406 21:39:15.651305 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_circle j b i, on_tline j b b i ? cong c g c h
-I0406 21:39:17.097661 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:17.098130 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j a d"
-I0406 21:39:17.098557 135279079972864 graph.py:498] 
-I0406 21:39:17.098665 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j a d ? cong c g c h
-I0406 21:39:23.051526 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:23.051856 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_tline j g c g"
-I0406 21:39:23.052671 135279079972864 graph.py:498] 
-I0406 21:39:23.052952 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_tline j g c g ? cong c g c h
-I0406 21:39:28.515337 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:28.515597 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_tline j f f h"
-I0406 21:39:28.516244 135279079972864 graph.py:498] 
-I0406 21:39:28.516447 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_tline j f f h ? cong c g c h
-I0406 21:39:29.003840 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:29.004138 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_circle j i b, on_tline j i b i"
-I0406 21:39:29.004765 135279079972864 graph.py:498] 
-I0406 21:39:29.004932 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_circle j i b, on_tline j i b i ? cong c g c h
-I0406 21:39:30.670721 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:30.670897 135279079972864 alphageometry.py:549] Worker PID=3092: Translation: "j = on_circle j g b, on_circle j h b"
-I0406 21:39:30.671322 135279079972864 graph.py:498] 
-I0406 21:39:30.671436 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = eqdistance i f b d, eqdistance i b d f; j = on_circle j g b, on_circle j h b ? cong c g c h
-I0406 21:39:34.026746 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:34.026888 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j e f, on_bline j f e"
-I0406 21:39:34.027255 135279079972864 graph.py:498] 
-I0406 21:39:34.027362 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j e f, on_bline j f e ? cong c g c h
-I0406 21:39:41.835646 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:41.835915 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "ERROR: Traceback (most recent call last):
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/alphageometry.py", line 470, in try_translate_constrained_to_construct
-    g.copy().add_clause(clause, 0, DEFINITIONS)
-  File "/home/tong_peng/onedrive_googie32u/alphageometry/graph.py", line 2635, in add_clause
-    raise PointTooCloseError()
-graph.PointTooCloseError
-"
-I0406 21:39:41.836076 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j c d, on_circle j c d"
-I0406 21:39:41.836421 135279079972864 graph.py:498] 
-I0406 21:39:41.836537 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j c d, on_circle j c d ? cong c g c h
-I0406 21:39:44.631866 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:44.632070 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_circle j c b, on_tline j c b c"
-I0406 21:39:44.632437 135279079972864 graph.py:498] 
-I0406 21:39:44.632554 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_circle j c b, on_tline j c b c ? cong c g c h
-I0406 21:39:54.147388 135279079972864 alphageometry.py:201] 
-==========================
- * From theorem premises:
-A B C D E F G H : Points
-B,A,C are collinear [00]
-CA = CB [01]
-CD = CA [02]
-CE = CA [03]
-D,F,E are collinear [04]
-BF ⟂ AB [05]
-G,E,A are collinear [06]
-F,G,C are collinear [07]
-H,F,C are collinear [08]
-H,D,A are collinear [09]
-
- * Auxiliary Constructions:
-I J : Points
-IB = DF [10]
-GJ = GB [11]
-HJ = HB [12]
-
- * Proof steps:
-001. GJ = GB [11] & HJ = HB [12] (SSS)⇒  ∠BGH = ∠HGJ [13]
-002. GJ = GB [11] & HJ = HB [12] ⇒  BJ ⟂ GH [14]
-003. F,G,C are collinear [07] & ∠BGH = ∠HGJ [13] & H,F,C are collinear [08] ⇒  ∠BGC = ∠CGJ [15]
-004. GJ = GB [11] & ∠BGC = ∠CGJ [15] (SAS)⇒  CB = CJ [16]
-005. CA = CB [01] & CE = CA [03] & CB = CJ [16] ⇒  B,E,J,A are concyclic [17]
-006. A,E,B,J are concyclic [17] ⇒  ∠BAE = ∠BJE [18]
-007. A,E,B,J are concyclic [17] ⇒  ∠BAJ = ∠BEJ [19]
-008. B,A,C are collinear [00] & E,G,A are collinear [06] & ∠BJE = ∠BAE [18] ⇒  ∠BJE = ∠CAG [20]
-009. CA = CB [01] & CB = CJ [16] ⇒  C is the circumcenter of \Delta BAJ [21]
-010. C is the circumcenter of \Delta BAJ [21] & B,A,C are collinear [00] ⇒  JB ⟂ AJ [22]
-011. B,A,C are collinear [00] & F,G,C are collinear [07] & ∠BEJ = ∠BAJ [19] & JB ⟂ AJ [22] & BJ ⟂ GH [14] & H,F,C are collinear [08] ⇒  ∠BEJ = ∠ACG [23]
-012. ∠BJE = ∠CAG [20] & ∠BEJ = ∠ACG [23] (Similar Triangles)⇒  EB:EJ = CG:CA [24]
-013. CD = CA [02] & CA = CB [01] & CE = CA [03] ⇒  C is the circumcenter of \Delta BDE [25]
-014. B,A,C are collinear [00] & AB ⟂ BF [05] ⇒  CB ⟂ BF [26]
-015. C is the circumcenter of \Delta BDE [25] & CB ⟂ BF [26] ⇒  ∠DBF = ∠DEB [27]
-016. D,F,E are collinear [04] & ∠DBF = ∠DEB [27] ⇒  ∠DBF = ∠FEB [28]
-017. D,F,E are collinear [04] ⇒  ∠DFB = ∠EFB [29]
-018. D,F,E are collinear [04] ⇒  ∠JFE = ∠JFD [30]
-019. ∠DBF = ∠FEB [28] & ∠DFB = ∠EFB [29] (Similar Triangles)⇒  DB:DF = BE:BF [31]
-020. ∠DBF = ∠FEB [28] & ∠DFB = ∠EFB [29] (Similar Triangles)⇒  DF:BF = BF:FE [32]
-021. F,G,C are collinear [07] & ∠BGH = ∠HGJ [13] & H,F,C are collinear [08] ⇒  ∠BGF = ∠FGJ [33]
-022. GJ = GB [11] & ∠BGF = ∠FGJ [33] (SAS)⇒  FB = FJ [34]
-023. DB:DF = BE:BF [31] & BI = DF [10] & FJ = BF [34] ⇒  DB:BI = BE:FJ [35]
-024. BF:FE = DF:BF [32] & FJ = BF [34] ⇒  FJ:FE = FD:FJ [36]
-025. FJ:FE = FD:FJ [36] & ∠JFE = ∠JFD [30] (Similar Triangles)⇒  JF:JE = DF:DJ [37]
-026. JF:JE = DF:DJ [37] & FB = FJ [34] & BI = DF [10] ⇒  BI:DJ = FJ:JE [38]
-027. DB:BI = BE:FJ [35] & BI:DJ = FJ:JE [38] ⇒  DB:DJ = BE:JE [39]
-028. B,E,J,A are concyclic [17] & CD = CA [02] & CA = CB [01] & CE = CA [03] ⇒  D,B,J,A are concyclic [40]
-029. D,B,J,A are concyclic [40] ⇒  ∠DAB = ∠DJB [41]
-030. H,D,A are collinear [09] & B,A,C are collinear [00] & ∠DJB = ∠DAB [41] ⇒  ∠DJB = ∠HAC [42]
-031. H,F,C are collinear [08] & BJ ⟂ GH [14] & F,G,C are collinear [07] ⇒  HF ⟂ BJ [43]
-032. CD = CA [02] & CA = CB [01] ⇒  C is the circumcenter of \Delta BDA [44]
-033. C is the circumcenter of \Delta BDA [44] & B,A,C are collinear [00] ⇒  AD ⟂ BD [45]
-034. H,D,A are collinear [09] & BD ⟂ AD [45] ⇒  DB ⟂ HD [46]
-035. HF ⟂ BJ [43] & DB ⟂ HD [46] ⇒  ∠FHD = ∠JBD [47]
-036. H,D,A are collinear [09] & H,F,C are collinear [08] & ∠FHD = ∠JBD [47] ⇒  ∠DBJ = ∠AHC [48]
-037. ∠DJB = ∠HAC [42] & ∠DBJ = ∠AHC [48] (Similar Triangles)⇒  DJ:DB = CA:CH [49]
-038. EB:EJ = CG:CA [24] & CE = CA [03] & DB:DJ = BE:JE [39] & DJ:DB = CA:CH [49] ⇒  HC:AC = GC:AC [50]
-039. AC = EC [03] ⇒  AC:FC = AC:FC [51]
-040. HC:AC = GC:AC [50] & AC:FC = AC:FC [51] ⇒  HC = GC
-==========================
-
-I0406 21:39:54.148121 135279079972864 alphageometry.py:205] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.
-I0406 21:39:55.925544 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:39:55.926052 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j a b"
-I0406 21:39:55.926870 135279079972864 graph.py:498] 
-I0406 21:39:55.927082 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j a b ? cong c g c h
-I0406 21:40:01.176547 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:40:01.176765 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_circle j a d, on_tline j a a d"
-I0406 21:40:01.177192 135279079972864 graph.py:498] 
-I0406 21:40:01.177350 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_circle j a d, on_tline j a a d ? cong c g c h
-I0406 21:40:10.123482 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:40:10.123683 135279079972864 alphageometry.py:549] Worker PID=2868: Translation: "j = on_line j f g, on_pline j e b d"
-I0406 21:40:10.123999 135279079972864 graph.py:498] 
-I0406 21:40:10.124114 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i a g; j = on_line j f g, on_pline j e b d ? cong c g c h
-I0406 21:40:10.564659 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:40:10.564879 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_bline j i b, on_pline j b d i"
-I0406 21:40:10.565302 135279079972864 graph.py:498] 
-I0406 21:40:10.565432 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_bline j i b, on_pline j b d i ? cong c g c h
-I0406 21:40:19.413986 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:40:19.414096 135279079972864 alphageometry.py:587] Worker PID=2868 beam search node 5: returning
-I0406 21:40:19.525763 135279079972864 alphageometry.py:527] Worker PID=2868 called for beam search node 9
-I0406 21:40:19.526045 135279079972864 alphageometry.py:530] Worker PID=2868: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : D b e e i 10 T b e e i 11 ; x00
-I0406 21:40:31.543770 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:40:31.543967 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_line j b i, on_bline j i b"
-I0406 21:40:31.544381 135279079972864 graph.py:498] 
-I0406 21:40:31.544498 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_line j b i, on_bline j i b ? cong c g c h
-I0406 21:40:45.252281 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:40:45.252490 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = eqdistance j d b i, on_circle j i d"
-I0406 21:40:45.252821 135279079972864 graph.py:498] 
-I0406 21:40:45.252936 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = eqdistance j d b i, on_circle j i d ? cong c g c h
-I0406 21:41:14.303236 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:41:14.303418 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_bline j f b, on_bline j g f"
-I0406 21:41:14.303857 135279079972864 graph.py:498] 
-I0406 21:41:14.304004 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_bline j f b, on_bline j g f ? cong c g c h
-I0406 21:41:31.294658 135279079972864 alphageometry.py:231] DD+AR failed to solve the problem.
-I0406 21:41:31.294843 135279079972864 alphageometry.py:549] Worker PID=3061: Translation: "j = on_bline j i b, on_pline j i b d"
-I0406 21:41:31.295471 135279079972864 graph.py:498] 
-I0406 21:41:31.295630 135279079972864 graph.py:499] a = free a; b = free b; c = midpoint c a b; d = on_circle d c a; e = on_circle e c a; f = on_tline f b b a, on_line f d e; g = on_line g a e, on_line g c f; h = on_line h a d, on_line h c f; i = on_circle i d b, on_tline i d b d; j = on_bline j i b, on_pline j i b d ? cong c g c h
-I0406 21:41:32.860955 135279079972864 alphageometry.py:568] Worker PID={pid}: Solved.
-I0406 21:41:32.874999 135279079972864 alphageometry.py:527] Worker PID=3092 called for beam search node 10
-I0406 21:41:32.875325 135279079972864 alphageometry.py:530] Worker PID=3092: Decoding from {S} a : ; b : ; c : C a b c 00 D a c b c 01 ; d : D a c c d 02 ; e : D a c c e 03 ; f : C d e f 04 T a b b f 05 ; g : C a e g 06 C c f g 07 ; h : C a d h 08 C c f h 09 ? D c g c h {F1} x00 i : T a d c i 10 ; x00

ag4masses/outputs/solved/gaolian100-6-ag-ok.log

@@ -1,188 +0,0 @@
-++ BATCH_SIZE=32
-++ BEAM_SIZE=128
-++ DEPTH=8
-++ NWORKERS=8
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt
-++ PROB=gaolian100-6
-++ MODEL=alphageometry
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt --problem_name=gaolian100-6 --mode=alphageometry --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=128 --search_depth=8 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=32 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out --n_workers=8
-I0321 22:36:52.123446 125862060560384 graph.py:498] gaolian100-6
-I0321 22:36:52.123676 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b ? cong d g g h
-I0321 22:36:56.809170 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:36:56.824296 125862060560384 alphageometry.py:522] Worker initializing. PID=2480
-I0321 22:36:56.834049 125862060560384 alphageometry.py:522] Worker initializing. PID=2481
-I0321 22:36:56.844219 125862060560384 alphageometry.py:522] Worker initializing. PID=2482
-I0321 22:36:56.854738 125862060560384 alphageometry.py:522] Worker initializing. PID=2483
-I0321 22:36:56.865157 125862060560384 alphageometry.py:522] Worker initializing. PID=2484
-I0321 22:36:56.877200 125862060560384 alphageometry.py:522] Worker initializing. PID=2545
-I0321 22:36:56.888153 125862060560384 alphageometry.py:522] Worker initializing. PID=2674
-I0321 22:36:56.901305 125862060560384 alphageometry.py:646] Depth 0. There are 1 nodes to expand:
-I0321 22:36:56.902293 125862060560384 alphageometry.py:650] {S} a : ; b : ; c : D a b a c 00 ; d : D a b a d 01 ; e : T a c c e 02 T a d d e 03 ; f : C a b f 04 T a b d f 05 ; g : C b e g 06 C d f g 07 ; h : C b c h 08 C d f h 09 ? D d g g h {F1} x00
-I0321 22:36:56.900544 125862060560384 alphageometry.py:522] Worker initializing. PID=2690
-I0321 22:37:46.476157 125862060560384 alphageometry.py:527] Worker 0: called, beam_queue size=1
-I0321 22:37:46.476386 125862060560384 alphageometry.py:530] Worker 0: Decoding from {S} a : ; b : ; c : D a b a c 00 ; d : D a b a d 01 ; e : T a c c e 02 T a d d e 03 ; f : C a b f 04 T a b d f 05 ; g : C b e g 06 C d f g 07 ; h : C b c h 08 C d f h 09 ? D d g g h {F1} x00
-I0321 22:52:43.807486 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_bline i d c"
-
-I0321 22:52:43.807765 125862060560384 graph.py:498] 
-I0321 22:52:43.807870 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_bline i d c ? cong d g g h
-I0321 22:52:50.786823 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:52:50.787211 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i b d, on_circle i c d"
-
-I0321 22:52:50.787455 125862060560384 graph.py:498] 
-I0321 22:52:50.787554 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i b d, on_circle i c d ? cong d g g h
-I0321 22:52:58.321355 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:52:58.321696 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i b c, on_circle i c b"
-
-I0321 22:52:58.321956 125862060560384 graph.py:498] 
-I0321 22:52:58.322064 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i b c, on_circle i c b ? cong d g g h
-I0321 22:53:07.199563 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:07.199822 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i c e, on_circle i d e"
-
-I0321 22:53:07.200112 125862060560384 graph.py:498] 
-I0321 22:53:07.200218 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i c e, on_circle i d e ? cong d g g h
-I0321 22:53:16.751102 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:16.751382 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_line i b c, on_bline i c b"
-
-I0321 22:53:16.751604 125862060560384 graph.py:498] 
-I0321 22:53:16.751696 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_line i b c, on_bline i c b ? cong d g g h
-I0321 22:53:25.407969 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:25.408181 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i c f, on_circle i h f"
-
-I0321 22:53:25.408459 125862060560384 graph.py:498] 
-I0321 22:53:25.408561 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i c f, on_circle i h f ? cong d g g h
-I0321 22:53:33.825636 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:33.825941 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i c b, on_circle i d b"
-
-I0321 22:53:33.826215 125862060560384 graph.py:498] 
-I0321 22:53:33.826322 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i c b, on_circle i d b ? cong d g g h
-I0321 22:53:39.953584 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:39.953873 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = eqdistance i h c e, eqdistance i c e h"
-
-I0321 22:53:39.954109 125862060560384 graph.py:498] 
-I0321 22:53:39.954210 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = eqdistance i h c e, eqdistance i c e h ? cong d g g h
-I0321 22:53:46.256042 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:46.256261 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_bline i e c, on_bline i e d"
-
-I0321 22:53:46.256529 125862060560384 graph.py:498] 
-I0321 22:53:46.256639 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_bline i e c, on_bline i e d ? cong d g g h
-I0321 22:53:57.463943 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:53:57.464216 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_line i b d, on_bline i d b"
-
-I0321 22:53:57.464519 125862060560384 graph.py:498] 
-I0321 22:53:57.464628 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_line i b d, on_bline i d b ? cong d g g h
-I0321 22:54:05.113608 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:54:05.113964 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i c e, on_circle i h e"
-
-I0321 22:54:05.114330 125862060560384 graph.py:498] 
-I0321 22:54:05.114442 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i c e, on_circle i h e ? cong d g g h
-I0321 22:54:16.178056 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:54:16.178323 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_bline i d c, on_bline i h c"
-
-I0321 22:54:16.178557 125862060560384 graph.py:498] 
-I0321 22:54:16.178667 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_bline i d c, on_bline i h c ? cong d g g h
-I0321 22:54:29.138074 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:54:29.138308 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_bline i d c, on_bline i e c"
-
-I0321 22:54:29.138582 125862060560384 graph.py:498] 
-I0321 22:54:29.138697 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_bline i d c, on_bline i e c ? cong d g g h
-I0321 22:54:40.013552 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:54:40.013882 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i c d, on_circle i d c"
-
-I0321 22:54:40.014126 125862060560384 graph.py:498] 
-I0321 22:54:40.014218 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i c d, on_circle i d c ? cong d g g h
-I0321 22:54:48.873232 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:54:48.873641 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_line i a e, on_bline i e a"
-
-I0321 22:54:48.874085 125862060560384 graph.py:498] 
-I0321 22:54:48.874257 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_line i a e, on_bline i e a ? cong d g g h
-I0321 22:54:58.874700 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:54:58.875120 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_circle i c f, on_circle i e f"
-
-I0321 22:54:58.875473 125862060560384 graph.py:498] 
-I0321 22:54:58.875631 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_circle i c f, on_circle i e f ? cong d g g h
-I0321 22:55:05.812197 125862060560384 alphageometry.py:230] DD+AR failed to solve the problem.
-I0321 22:55:05.812473 125862060560384 alphageometry.py:548] Worker 0: Translation: "i = on_line i c d, on_bline i d c"
-
-I0321 22:55:05.812747 125862060560384 graph.py:498] 
-I0321 22:55:05.812847 125862060560384 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = foot f d a b; g = on_line g d f, on_line g e b; h = on_line h d f, on_line h c b; i = on_line i c d, on_bline i d c ? cong d g g h
-I0321 22:55:30.485164 125862060560384 alphageometry.py:200] 
-==========================
- * From theorem premises:
-A B C D E F G H : Points
-AC = AB [00]
-AD = AB [01]
-DE ⟂ AD [02]
-CE ⟂ AC [03]
-DF ⟂ AB [04]
-D,G,F are collinear [05]
-B,G,E are collinear [06]
-B,H,C are collinear [07]
-H,D,F are collinear [08]
-
- * Auxiliary Constructions:
-I : Points
-ID = IC [09]
-D,C,I are collinear [10]
-
- * Proof steps:
-001. CA = BA [00] & DI = CI [09] ⇒  CA:DI = CA:DI [11]
-002. AD = AB [01] & AC = AB [00] ⇒  AC = AD [12]
-003. AD = AB [01] & AC = AB [00] ⇒  A is the circumcenter of \Delta CBD [13]
-004. AC = AD [12] & ID = IC [09] ⇒  CD ⟂ AI [14]
-005. AC = AD [12] & ID = IC [09] ⇒  ID:IC = AD:AC [15]
-006. D,C,I are collinear [10] & CD ⟂ AI [14] & DE ⟂ AD [02] ⇒  ∠EDA = ∠CIA [16]
-007. D,C,I are collinear [10] & ID = IC [09] ⇒  I is midpoint of CD [17]
-008. A is the circumcenter of \Delta CBD [13] & I is midpoint of CD [17] ⇒  ∠DBC = ∠IAC [18]
-009. A is the circumcenter of \Delta CBD [13] & CE ⟂ AC [03] ⇒  ∠DCE = ∠DBC [19]
-010. CE ⟂ AC [03] & DE ⟂ AD [02] ⇒  ∠EDA = ∠ECA [20]
-011. ∠EDA = ∠ECA [20] ⇒  D,C,E,A are concyclic [21]
-012. D,C,E,A are concyclic [21] ⇒  ∠DCE = ∠DAE [22]
-013. D,C,E,A are concyclic [21] ⇒  ∠EDC = ∠EAC [23]
-014. ∠DBC = ∠IAC [18] & ∠DCE = ∠DBC [19] & ∠DCE = ∠DAE [22] ⇒  ∠DAE = ∠IAC [24]
-015. ∠EDA = ∠CIA [16] & ∠DAE = ∠IAC [24] (Similar Triangles)⇒  ED:EA = CI:CA [25]
-016. ∠EDA = ∠CIA [16] & ∠DAE = ∠IAC [24] (Similar Triangles)⇒  AE:AD = AC:AI [26]
-017. A is the circumcenter of \Delta CBD [13] & DE ⟂ AD [02] ⇒  ∠CDE = ∠CBD [27]
-018. ∠ECD = ∠CBD [19] & ∠CDE = ∠CBD [27] ⇒  ∠CDE = ∠ECD [28]
-019. ∠CDE = ∠ECD [28] ⇒  EC = ED [29]
-020. ED:EA = CI:CA [25] & AC = AB [00] & DI = CI [09] & CE = DE [29] ⇒  DI:CA = CE:EA [30]
-021. AE:AD = AC:AI [26] & AD = AB [01] & AC = AB [00] ⇒  EA:BA = BA:IA [31]
-022. AC = AD [12] & EC = ED [29] ⇒  CD ⟂ AE [32]
-023. CD ⟂ AI [14] & CE ⟂ AC [03] ⇒  ∠ECA = ∠(DC-IA) [33]
-024. ∠ECA = ∠(DC-IA) [33] & ∠CDE = ∠ECD [28] ⇒  ∠IAC = ∠EDC [34]
-025. ∠EDC = ∠EAC [23] & ∠IAC = ∠EDC [34] ⇒  ∠IAC = ∠EAC [35]
-026. ∠IAC = ∠EAC [35] ⇒  IA ∥ EA [36]
-027. CD ⟂ AE [32] & CD ⟂ AI [14] & AI ∥ AE [36] ⇒  ∠BAI = ∠BAE [37]
-028. EA:BA = BA:IA [31] & ∠BAI = ∠BAE [37] (Similar Triangles)⇒  BA:BI = EA:BE [38]
-029. EA:BA = BA:IA [31] & ∠BAI = ∠BAE [37] (Similar Triangles)⇒  ∠ABI = ∠BEA [39]
-030. BA:BI = EA:BE [38] & CA = BA [00] ⇒  CA:BI = EA:BE [40]
-031. DI:CA = CE:EA [30] & CA:BI = EA:BE [40] ⇒  DI:CE = BI:BE [41]
-032. AD = AB [01] ⇒  ∠ABD = ∠BDA [42]
-033. DE ⟂ AD [02] & DF ⟂ AB [04] & ∠ABD = ∠BDA [42] (Angle chase)⇒  ∠BDE = ∠FDB [43]
-034. D,G,F are collinear [05] & ∠FDB = ∠BDE [43] ⇒  ∠GDB = ∠BDE [44]
-035. ∠GDB = ∠BDE [44] & B,G,E are collinear [06] ⇒  BE:BG = DE:DG [45]
-036. BE:BG = DE:DG [45] & CE = DE [29] ⇒  BE:BG = CE:DG [46]
-037. BI:BE = DI:CE [41] & BE:BG = CE:DG [46] ⇒  BI:BG = DI:DG [47]
-038. AC = AB [00] ⇒  ∠ACB = ∠CBA [48]
-039. AC = AD [12] ⇒  ∠ACD = ∠CDA [49]
-040. DF ⟂ AB [04] & ∠ACB = ∠CBA [48] & ∠ACD = ∠CDA [49] & ∠ABD = ∠BDA [42] (Angle chase)⇒  ∠(BC-DF) = ∠CDB [50]
-041. D,C,I are collinear [10] & B,H,C are collinear [07] & H,D,F are collinear [08] & D,G,F are collinear [05] & ∠CDB = ∠(BC-DF) [50] ⇒  ∠IDB = ∠BHG [51]
-042. ID:IC = AD:AC [15] & D,C,I are collinear [10] ⇒  ∠DAI = ∠IAC [52]
-043. ∠ABI = ∠BEA [39] & AI ∥ AE [36] ⇒  ∠ABI = ∠(BE-AI) [53]
-044. ∠DAI = ∠IAC [52] & ∠ACB = ∠CBA [48] & ∠ABD = ∠BDA [42] & ∠ABI = ∠(BE-AI) [53] (Angle chase)⇒  ∠CBE = ∠IBD [54]
-045. B,H,C are collinear [07] & B,G,E are collinear [06] & ∠IBD = ∠CBE [54] ⇒  ∠IBD = ∠HBG [55]
-046. ∠IDB = ∠BHG [51] & ∠IBD = ∠HBG [55] (Similar Triangles)⇒  ID:GH = IB:GB [56]
-047. BI:BG = DI:DG [47] & ID = IC [09] & ID:GH = IB:GB [56] ⇒  DI:HG = DI:DG [57]
-048. CA:DI = CA:DI [11] & DI:HG = DI:DG [57] ⇒  HG = DG
-==========================
-
-I0321 22:55:30.485701 125862060560384 alphageometry.py:204] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.
-I0321 23:01:11.216471 125862060560384 alphageometry.py:565] Worker 0: Solved.
-I0321 23:01:11.217892 125862060560384 alphageometry.py:670] Worker 0 returned. Solved=True

ag4masses/outputs/solved/gaolian100-6-lemma-ddar-ok.log

@@ -1,78 +0,0 @@
-++ BATCH_SIZE=32
-++ BEAM_SIZE=128
-++ DEPTH=8
-++ NWORKERS=8
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt
-++ PROB=gaolian100-6-lemma
-++ MODEL=alphageometry
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt --problem_name=gaolian100-6-lemma --mode=alphageometry --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=128 --search_depth=8 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=32 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out --n_workers=8
-I0321 22:27:00.674356 136990061826048 graph.py:498] gaolian100-6-lemma
-I0321 22:27:00.674595 136990061826048 graph.py:499] a = free a; b = free b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = midpoint f c d; g = on_line g e b, on_circle g a b ? eqangle f d f g f b f d
-I0321 22:27:06.853825 136990061826048 alphageometry.py:200] 
-==========================
- * From theorem premises:
-A B C D E F G : Points
-AC = AB [00]
-AD = AB [01]
-CE ⟂ AC [02]
-DE ⟂ AD [03]
-D,F,C are collinear [04]
-FC = FD [05]
-G,B,E are collinear [06]
-AG = AB [07]
-
- * Auxiliary Constructions:
-: Points
-
-
- * Proof steps:
-001. AG = AB [07] & AC = AB [00] ⇒  A is the circumcenter of \Delta CGB [08]
-002. A is the circumcenter of \Delta CGB [08] & CE ⟂ AC [02] ⇒  ∠ECG = ∠CBG [09]
-003. B,G,E are collinear [06] & ∠ECG = ∠CBG [09] ⇒  ∠BCE = ∠EGC [10]
-004. B,G,E are collinear [06] ⇒  ∠BEC = ∠GEC [11]
-005. ∠BCE = ∠EGC [10] & ∠BEC = ∠GEC [11] (Similar Triangles)⇒  BC:BE = CG:CE [12]
-006. ∠BCE = ∠EGC [10] & ∠BEC = ∠GEC [11] (Similar Triangles)⇒  CB:CE = GC:GE [13]
-007. AG = AB [07] & AD = AB [01] & AC = AB [00] ⇒  A is the circumcenter of \Delta DGC [14]
-008. A is the circumcenter of \Delta DGC [14] & DE ⟂ AD [03] ⇒  ∠CDE = ∠CGD [15]
-009. A is the circumcenter of \Delta DGC [14] & CE ⟂ AC [02] ⇒  ∠ECD = ∠CGD [16]
-010. ∠CDE = ∠CGD [15] & ∠ECD = ∠CGD [16] ⇒  ∠ECD = ∠CDE [17]
-011. ∠ECD = ∠CDE [17] ⇒  EC = ED [18]
-012. BC:BE = CG:CE [12] & EC = ED [18] ⇒  BC:BE = GC:ED [19]
-013. AC = AB [00] & AD = AB [01] ⇒  AD = AC [20]
-014. AD = AC [20] & FC = FD [05] ⇒  CD ⟂ AF [21]
-015. C,F,D are collinear [04] & CD ⟂ AF [21] & CE ⟂ AC [02] ⇒  ∠ACE = ∠AFD [22]
-016. D,F,C are collinear [04] & FC = FD [05] ⇒  F is midpoint of DC [23]
-017. A is the circumcenter of \Delta DGC [14] & F is midpoint of DC [23] ⇒  ∠CGD = ∠FAD [24]
-018. DE ⟂ AD [03] & CE ⟂ AC [02] ⇒  ∠ECA = ∠EDA [25]
-019. ∠ECA = ∠EDA [25] ⇒  A,D,E,C are concyclic [26]
-020. A,D,E,C are concyclic [26] ⇒  ∠CAE = ∠CDE [27]
-021. ∠CGD = ∠FAD [24] & ∠CDE = ∠CGD [15] & ∠CAE = ∠CDE [27] ⇒  ∠CAE = ∠FAD [28]
-022. ∠ACE = ∠AFD [22] & ∠CAE = ∠FAD [28] (Similar Triangles)⇒  EC:DF = EA:DA [29]
-023. ∠ACE = ∠AFD [22] & ∠CAE = ∠FAD [28] (Similar Triangles)⇒  AE:AC = AD:AF [30]
-024. AE:AC = AD:AF [30] & AC = AB [00] & AD = AB [01] ⇒  AE:AB = AB:AF [31]
-025. AD = AC [20] & EC = ED [18] ⇒  DC ⟂ AE [32]
-026. DC ⟂ AE [32] & CD ⟂ AF [21] ⇒  ∠EAB = ∠FAB [33]
-027. DC ⟂ AE [32] & CD ⟂ AF [21] ⇒  ∠GAF = ∠GAE [34]
-028. AE:AB = AB:AF [31] & ∠EAB = ∠FAB [33] (Similar Triangles)⇒  AE:AB = BE:FB [35]
-029. EC:DF = EA:DA [29] & EC = ED [18] & AD = AB [01] & AE:AB = BE:FB [35] & FC = FD [05] ⇒  BE:FB = ED:FC [36]
-030. BC:BE = GC:ED [19] & BE:FB = ED:FC [36] ⇒  BC:FB = GC:FC [37]
-031. BC:BE = GC:ED [19] & BE:FB = ED:FC [36] ⇒  BC:GC = FB:FC [38]
-032. CB:CE = GC:GE [13] & EC = ED [18] ⇒  BC:ED = GC:GE [39]
-033. AB:AF = AE:AB [31] & AG = AB [07] ⇒  AG:AF = AE:AG [40]
-034. AG:AF = AE:AG [40] & ∠GAF = ∠GAE [34] (Similar Triangles)⇒  GA:EA = GF:EG [41]
-035. EC:DF = EA:DA [29] & EC = ED [18] & AD = AB [01] & GA:EA = GF:EG [41] & AG = AB [07] & FC = FD [05] ⇒  GE:FG = ED:FC [42]
-036. BC:ED = GC:GE [39] & GE:FG = ED:FC [42] ⇒  GC:BC = FG:FC [43]
-037. GC:BC = FG:FC [43] & FC = FD [05] & BC:GC = FB:FC [38] ⇒  FC:FB = FG:FC [44]
-038. BC:FB = GC:FC [37] & FC:FB = FG:FC [44] (Similar Triangles)⇒  ∠GFC = ∠CFB [45]
-039. C,F,D are collinear [04] & ∠GFC = ∠CFB [45] ⇒  ∠DFG = ∠BFD
-==========================
-
-I0321 22:27:06.854308 136990061826048 alphageometry.py:204] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.

ag4masses/outputs/solved/imo-2004p1-ag-ok.log

@@ -1,195 +0,0 @@
-++ BATCH_SIZE=32
-++ BEAM_SIZE=128
-++ DEPTH=8
-++ NWORKERS=8
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/alphageometry/imo_ag_30.txt
-++ PROB=translated_imo_2004_p1
-++ MODEL=alphageometry
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/alphageometry/imo_ag_30.txt --problem_name=translated_imo_2004_p1 --mode=alphageometry --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=128 --search_depth=8 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=32 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out --n_workers=8
-I0314 21:19:02.575181 130621346496512 graph.py:498] translated_imo_2004_p1
-I0314 21:19:02.575465 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g ? coll j b c
-I0314 21:19:23.433823 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:19:23.455061 130621346496512 alphageometry.py:522] Worker initializing. PID=9482
-I0314 21:19:23.467305 130621346496512 alphageometry.py:522] Worker initializing. PID=9483
-I0314 21:19:23.477555 130621346496512 alphageometry.py:522] Worker initializing. PID=9484
-I0314 21:19:23.489834 130621346496512 alphageometry.py:522] Worker initializing. PID=9485
-I0314 21:19:23.501612 130621346496512 alphageometry.py:522] Worker initializing. PID=9486
-I0314 21:19:23.514227 130621346496512 alphageometry.py:522] Worker initializing. PID=9487
-I0314 21:19:23.527762 130621346496512 alphageometry.py:522] Worker initializing. PID=9644
-I0314 21:19:23.548665 130621346496512 alphageometry.py:646] Depth 0. There are 1 nodes to expand:
-I0314 21:19:23.549773 130621346496512 alphageometry.py:650] {S} a : ; b : ; c : ; d : C b c d 00 D b d c d 01 ; e : C a b e 02 D b d d e 03 ; f : C a c f 04 D b d d f 05 ; g : ^ a b a g a g a c 06 ^ d e d g d g d f 07 ; h : D b h e h 08 D e h g h 09 ; i : D c i f i 10 D f i g i 11 ; j : D g h h j 12 D g i i j 13 ? C j b c {F1} x00
-I0314 21:19:23.547642 130621346496512 alphageometry.py:522] Worker initializing. PID=9779
-I0314 21:20:09.040031 130621346496512 alphageometry.py:527] Worker 0: called, beam_queue size=1
-I0314 21:20:09.040336 130621346496512 alphageometry.py:530] Worker 0: Decoding from {S} a : ; b : ; c : ; d : C b c d 00 D b d c d 01 ; e : C a b e 02 D b d d e 03 ; f : C a c f 04 D b d d f 05 ; g : ^ a b a g a g a c 06 ^ d e d g d g d f 07 ; h : D b h e h 08 D e h g h 09 ; i : D c i f i 10 D f i g i 11 ; j : D g h h j 12 D g i i j 13 ? C j b c {F1} x00
-I0314 21:37:52.805149 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a c, on_bline k c a"
-
-I0314 21:37:52.805521 130621346496512 graph.py:498] 
-I0314 21:37:52.805641 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a c, on_bline k c a ? coll j b c
-I0314 21:38:37.121450 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:38:37.121777 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_pline k c a b"
-
-I0314 21:38:37.122064 130621346496512 graph.py:498] 
-I0314 21:38:37.122184 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_pline k c a b ? coll j b c
-I0314 21:39:00.096443 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:39:00.096744 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a d, on_circle k d a"
-
-I0314 21:39:00.097027 130621346496512 graph.py:498] 
-I0314 21:39:00.097140 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a d, on_circle k d a ? coll j b c
-I0314 21:39:28.725176 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:39:28.725494 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a d, on_bline k d a"
-
-I0314 21:39:28.725776 130621346496512 graph.py:498] 
-I0314 21:39:28.725885 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a d, on_bline k d a ? coll j b c
-I0314 21:39:53.279735 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:39:53.280042 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_pline k c a b, on_tline k a a b"
-
-I0314 21:39:53.280367 130621346496512 graph.py:498] 
-I0314 21:39:53.280476 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_pline k c a b, on_tline k a a b ? coll j b c
-I0314 21:40:37.706057 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:40:37.706328 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a c, on_tline k g a c"
-
-I0314 21:40:37.706609 130621346496512 graph.py:498] 
-I0314 21:40:37.706727 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a c, on_tline k g a c ? coll j b c
-I0314 21:41:05.213561 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:41:05.213871 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a j, on_bline k j a"
-
-I0314 21:41:05.214159 130621346496512 graph.py:498] 
-I0314 21:41:05.214273 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a j, on_bline k j a ? coll j b c
-I0314 21:41:28.912238 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:41:28.912539 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k c f, on_bline k f c"
-
-I0314 21:41:28.912819 130621346496512 graph.py:498] 
-I0314 21:41:28.912931 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k c f, on_bline k f c ? coll j b c
-I0314 21:41:59.285758 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:41:59.286082 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a c, on_tline k g a c"
-
-I0314 21:41:59.286429 130621346496512 graph.py:498] 
-I0314 21:41:59.286543 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a c, on_tline k g a c ? coll j b c
-I0314 21:42:27.211067 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:42:27.211405 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k c e, on_bline k e c"
-
-I0314 21:42:27.211685 130621346496512 graph.py:498] 
-I0314 21:42:27.211795 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k c e, on_bline k e c ? coll j b c
-I0314 21:42:53.823427 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:42:53.823667 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_tline k a a c"
-
-I0314 21:42:53.823988 130621346496512 graph.py:498] 
-I0314 21:42:53.824099 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_tline k a a c ? coll j b c
-I0314 21:43:17.842679 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:43:17.843007 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_tline k g a c"
-
-I0314 21:43:17.843296 130621346496512 graph.py:498] 
-I0314 21:43:17.843414 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_tline k g a c ? coll j b c
-I0314 21:43:41.769865 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:43:41.770210 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k c j, on_bline k j c"
-
-I0314 21:43:41.770498 130621346496512 graph.py:498] 
-I0314 21:43:41.770612 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k c j, on_bline k j c ? coll j b c
-I0314 21:44:10.411840 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:44:10.412175 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k d f, on_circle k d f"
-
-I0314 21:44:10.412528 130621346496512 graph.py:498] 
-I0314 21:44:10.412643 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k d f, on_circle k d f ? coll j b c
-I0314 21:44:58.993842 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:44:58.994517 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k a e, on_bline k e a"
-
-I0314 21:44:58.995533 130621346496512 graph.py:498] 
-I0314 21:44:58.995776 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k a e, on_bline k e a ? coll j b c
-I0314 21:45:25.866546 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:45:25.866863 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k e g, on_bline k g e"
-
-I0314 21:45:25.867155 130621346496512 graph.py:498] 
-I0314 21:45:25.867275 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k e g, on_bline k g e ? coll j b c
-I0314 21:45:54.018602 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:45:54.018959 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_pline k d c e"
-
-I0314 21:45:54.019243 130621346496512 graph.py:498] 
-I0314 21:45:54.019360 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_pline k d c e ? coll j b c
-I0314 21:46:20.696980 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:46:20.697405 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k c g, on_bline k g c"
-
-I0314 21:46:20.697771 130621346496512 graph.py:498] 
-I0314 21:46:20.697904 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k c g, on_bline k g c ? coll j b c
-I0314 21:46:48.547189 130621346496512 alphageometry.py:230] DD+AR failed to solve the problem.
-I0314 21:46:48.547529 130621346496512 alphageometry.py:548] Worker 0: Translation: "k = on_line k e f, on_bline k f e"
-
-I0314 21:46:48.547818 130621346496512 graph.py:498] 
-I0314 21:46:48.547931 130621346496512 graph.py:499] a b c = triangle a b c; d = midpoint d b c; e = on_circle e d b, on_line e a b; f = on_circle f d b, on_line f a c; g = angle_bisector g b a c, angle_bisector g e d f; h = circle h b e g; i = circle i c f g; j = on_circle j h g, on_circle j i g; k = on_line k e f, on_bline k f e ? coll j b c
-I0314 21:47:56.216076 130621346496512 alphageometry.py:200] 
-==========================
- * From theorem premises:
-A B C D E F G H I J : Points
-DB = DC [00]
-B,C,D are collinear [01]
-B,E,A are collinear [02]
-DE = DB [03]
-F,C,A are collinear [04]
-DF = DB [05]
-∠BAG = ∠GAC [06]
-∠EDG = ∠GDF [07]
-HB = HE [08]
-HE = HG [09]
-IC = IF [10]
-IF = IG [11]
-IJ = IG [12]
-HJ = HG [13]
-
- * Auxiliary Constructions:
-K : Points
-F,E,K are collinear [14]
-KF = KE [15]
-
- * Proof steps:
-001. IC = IF [10] & IF = IG [11] & IJ = IG [12] ⇒  J,F,C,G are concyclic [16]
-002. J,F,C,G are concyclic [16] ⇒  ∠JCF = ∠JGF [17]
-003. DB = DC [00] & DF = DB [05] ⇒  DF = DC [18]
-004. DF = DC [18] ⇒  ∠DFC = ∠FCD [19]
-005. DB = DC [00] & DF = DB [05] & DE = DB [03] ⇒  B,E,C,F are concyclic [20]
-006. DB = DC [00] & DF = DB [05] & DE = DB [03] ⇒  D is the circumcenter of \Delta CFE [21]
-007. B,E,C,F are concyclic [20] ⇒  ∠BEF = ∠BCF [22]
-008. B,E,C,F are concyclic [20] ⇒  ∠BCE = ∠BFE [23]
-009. B,E,C,F are concyclic [20] ⇒  ∠BEC = ∠BFC [24]
-010. B,E,A are collinear [02] & F,C,A are collinear [04] & ∠DFC = ∠FCD [19] & B,C,D are collinear [01] & ∠BEF = ∠BCF [22] ⇒  ∠BEF = ∠CFD [25]
-011. DE = DB [03] & DB = DC [00] ⇒  D is the circumcenter of \Delta CEB [26]
-012. D is the circumcenter of \Delta CEB [26] & B,C,D are collinear [01] ⇒  CE ⟂ EB [27]
-013. DE = DB [03] & DF = DB [05] ⇒  DF = DE [28]
-014. DF = DE [28] & KF = KE [15] ⇒  EF ⟂ DK [29]
-015. E,F,K are collinear [14] & B,E,A are collinear [02] & CE ⟂ EB [27] & EF ⟂ DK [29] ⇒  ∠FKD = ∠AEC [30]
-016. F,E,K are collinear [14] & KF = KE [15] ⇒  K is midpoint of FE [31]
-017. D is the circumcenter of \Delta CFE [21] & K is midpoint of FE [31] ⇒  ∠FCE = ∠FDK [32]
-018. ∠FCE = ∠FDK [32] & F,C,A are collinear [04] ⇒  ∠ACE = ∠FDK [33]
-019. ∠FKD = ∠AEC [30] & ∠ACE = ∠FDK [33] (Similar Triangles)⇒  FK:AE = FD:AC [34]
-020. FK:AE = FD:AC [34] & KF = KE [15] & DC = DF [18] ⇒  EK:EA = CD:CA [35]
-021. F,E,K are collinear [14] & B,E,A are collinear [02] & D,B,C are collinear [01] & ∠BEF = ∠BCF [22] & F,C,A are collinear [04] ⇒  ∠KEA = ∠ACD [36]
-022. EK:EA = CD:CA [35] & ∠KEA = ∠ACD [36] (Similar Triangles)⇒  KE:DC = KA:DA [37]
-023. EK:EA = CD:CA [35] & ∠KEA = ∠ACD [36] (Similar Triangles)⇒  ∠EKA = ∠ADC [38]
-024. ∠BEC = ∠BFC [24] & B,E,A are collinear [02] & F,C,A are collinear [04] ⇒  ∠(AB-CE) = ∠(BF-AC) [39]
-025. ∠EKA = ∠ADC [38] & F,E,K are collinear [14] & B,C,D are collinear [01] ⇒  ∠(EF-AK) = ∠(AD-BC) [40]
-026. ∠BAG = ∠GAC [06] & ∠BCE = ∠BFE [23] & ∠(AB-CE) = ∠(BF-AC) [39] & ∠(EF-AK) = ∠(AD-BC) [40] (Angle chase)⇒  ∠GAD = ∠KAG [41]
-027. DF = DE [28] & ∠EDG = ∠GDF [07] (SAS)⇒  GF = GE [42]
-028. DF = DE [28] & ∠EDG = ∠GDF [07] (SAS)⇒  ∠DFG = ∠GED [43]
-029. DF = DE [28] & GF = GE [42] ⇒  FE ⟂ DG [44]
-030. FE ⟂ DG [44] & EF ⟂ DK [29] ⇒  D,G,K are collinear [45]
-031. ∠GAD = ∠KAG [41] & D,G,K are collinear [45] ⇒  DG:GK = DA:AK [46]
-032. KE:DC = KA:DA [37] & CD = FD [18] & DG:GK = DA:AK [46] & DE = DF [28] ⇒  GD:GK = ED:EK [47]
-033. GD:GK = ED:EK [47] & D,G,K are collinear [45] ⇒  ∠DEG = ∠GEK [48]
-034. ∠DEG = ∠GEK [48] & F,E,K are collinear [14] & ∠DFG = ∠GED [43] ⇒  ∠DFG = ∠FEG [49]
-035. ∠BEF = ∠CFD [25] & ∠DFG = ∠FEG [49] ⇒  ∠CFG = ∠BEG [50]
-036. HB = HE [08] & HE = HG [09] & HJ = HG [13] ⇒  J,B,E,G are concyclic [51]
-037. J,B,E,G are concyclic [51] ⇒  ∠JBE = ∠JGE [52]
-038. ∠JCF = ∠JGF [17] & F,C,A are collinear [04] & ∠CFG = ∠BEG [50] & B,E,A are collinear [02] & ∠JBE = ∠JGE [52] ⇒  ∠BJG = ∠CJG [53]
-039. ∠BJG = ∠CJG [53] ⇒  JB ∥ JC [54]
-040. BJ ∥ CJ [54] ⇒  J,B,C are collinear
-==========================
-
-I0314 21:47:56.216599 130621346496512 alphageometry.py:204] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out.
-I0314 22:06:50.294282 130621346496512 alphageometry.py:565] Worker 0: Solved.
-I0314 22:06:50.299571 130621346496512 alphageometry.py:670] Worker 0 returned. Solved=True

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

@@ -1,90 +0,0 @@
-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.

ag4masses/outputs/solved/square_angle15-ag-ok.log

@@ -1,88 +0,0 @@
-++ BATCH_SIZE=32
-++ BEAM_SIZE=128
-++ DEPTH=8
-++ NWORKERS=8
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt
-++ PROB=square_angle15
-++ MODEL=alphageometry
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt --problem_name=square_angle15 --mode=alphageometry --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=128 --search_depth=8 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=32 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out2 --n_workers=8
-I0310 09:41:49.753222 130464824438784 graph.py:498] square_angle15
-I0310 09:41:49.753450 130464824438784 graph.py:499] a b c d = isquare a b c d; e = s_angle c d e 15, s_angle d c e -15 ? cong e a a b
-I0310 09:41:51.728961 130464824438784 alphageometry.py:230] DD+AR failed to solve the problem.
-I0310 09:41:51.744117 130464824438784 alphageometry.py:522] Worker initializing. PID=1888
-I0310 09:41:51.753463 130464824438784 alphageometry.py:522] Worker initializing. PID=1889
-I0310 09:41:51.761840 130464824438784 alphageometry.py:522] Worker initializing. PID=1890
-I0310 09:41:51.770576 130464824438784 alphageometry.py:522] Worker initializing. PID=1891
-I0310 09:41:51.780648 130464824438784 alphageometry.py:522] Worker initializing. PID=1892
-I0310 09:41:51.790728 130464824438784 alphageometry.py:522] Worker initializing. PID=1897
-I0310 09:41:51.806141 130464824438784 alphageometry.py:522] Worker initializing. PID=2012
-I0310 09:41:51.818140 130464824438784 alphageometry.py:646] Depth 0. There are 1 nodes to expand:
-I0310 09:41:51.819088 130464824438784 alphageometry.py:650] {S} a : ; b : ; c : D a b b c 00 T a b b c 01 ; d : P a b c d 02 P a d b c 03 ; e : ^ c d c e 1. pi / 12. 04 ^ d e d c 1. pi / 12. 05 ? D e a a b {F1} x00
-I0310 09:41:51.817840 130464824438784 alphageometry.py:522] Worker initializing. PID=2147
-I0310 09:42:40.682207 130464824438784 alphageometry.py:527] Worker 0: called, beam_queue size=1
-I0310 09:42:40.682444 130464824438784 alphageometry.py:530] Worker 0: Decoding from {S} a : ; b : ; c : D a b b c 00 T a b b c 01 ; d : P a b c d 02 P a d b c 03 ; e : ^ c d c e 1. pi / 12. 04 ^ d e d c 1. pi / 12. 05 ? D e a a b {F1} x00
-I0310 09:54:59.187637 130464824438784 alphageometry.py:548] Worker 0: Translation: "ERROR: Invalid predicate ^ c b c f b f b c"
-
-I0310 09:54:59.187752 130464824438784 alphageometry.py:548] Worker 0: Translation: "ERROR: Invalid predicate ^ c d c f f c f d"
-
-I0310 09:54:59.187860 130464824438784 alphageometry.py:548] Worker 0: Translation: "f = on_circle f c d, on_circle f e d"
-
-I0310 09:54:59.188132 130464824438784 graph.py:498] 
-I0310 09:54:59.188237 130464824438784 graph.py:499] a b c d = isquare a b c d; e = s_angle c d e 15, s_angle d c e -15; f = on_circle f c d, on_circle f e d ? cong e a a b
-I0310 09:55:07.133492 130464824438784 alphageometry.py:200] 
-==========================
- * From theorem premises:
-A B C D E : Points
-AB = BC [00]
-AB ⟂ BC [01]
-AB ∥ CD [02]
-AD ∥ BC [03]
-∠ECD = 1_1PI/12 [04]
-∠EDC = 1_PI/12 [05]
-
- * Auxiliary Constructions:
-F : Points
-CF = CD [06]
-EF = ED [07]
-
- * Proof steps:
-001. AB ∥ CD [02] & BC ∥ AD [03] ⇒  ∠CDA = ∠ABC [08]
-002. AD ∥ BC [03] ⇒  ∠CAD = ∠ACB [09]
-003. ∠CDA = ∠ABC [08] & ∠CAD = ∠ACB [09] (Similar Triangles)⇒  CD = AB [10]
-004. ∠CDA = ∠ABC [08] & ∠CAD = ∠ACB [09] (Similar Triangles)⇒  BA:BC = DC:DA [11]
-005. CF = CD [06] & BA:BC = DC:DA [11] & AB = BC [00] ⇒  AD = FC [12]
-006. CF = CD [06] & EF = ED [07] ⇒  DF ⟂ CE [13]
-007. CF = CD [06] & EF = ED [07] (SSS)⇒  ∠FCE = ∠ECD [14]
-008. CF = CD [06] & EF = ED [07] (SSS)⇒  ∠CFE = ∠EDC [15]
-009. DF ⟂ CE [13] & AB ⟂ BC [01] & BC ∥ AD [03] ⇒  ∠DAB = ∠(DF-CE) [16]
-010. ∠FCE = ∠ECD [14] & AB ∥ CD [02] ⇒  ∠FCE = ∠(CE-AB) [17]
-011. ∠ECD = 1_1PI/12 [04] & AB ∥ CD [02] ⇒  ∠(CE-AB) = 1_1PI/12 [18]
-012. ∠EDC = 1_PI/12 [05] & AB ∥ CD [02] ⇒  ∠(DE-AB) = 1_PI/12 [19]
-013. ∠ECF = ∠(AB-CE) [17] & ∠ECD = 1_1PI/12 [04] & AB ∥ CD [02] & ∠(DE-AB) = 1_PI/12 [19] & ∠CFE = ∠EDC [15] ⇒  ∠CFE = ∠ECF [20]
-014. ∠FCE = ∠(CE-AB) [17] & ∠CFE = ∠ECF [20] ⇒  ∠CEF = ∠(AB-CF) [21]
-015. ∠DAB = ∠(DF-CE) [16] & ∠CEF = ∠(AB-CF) [21] ⇒  ∠(AD-CF) = ∠DFE [22]
-016. CF = CD [06] ⇒  ∠CFD = ∠FDC [23]
-017. ∠CFD = ∠FDC [23] & AB ∥ CD [02] ⇒  ∠CFD = ∠(DF-AB) [24]
-018. AB ⟂ BC [01] & ∠(CE-AB) = 1_1PI/12 [18] & ∠CFD = ∠(DF-AB) [24] & DF ⟂ CE [13] (Angle chase)⇒  ∠FCB = 1_PI/3 [25]
-019. EF = ED [07] ⇒  ∠EDF = ∠DFE [26]
-020. ∠(DE-AB) = 1_PI/12 [19] & ∠(CE-AB) = 1_1PI/12 [18] & ∠EDF = ∠DFE [26] & DF ⟂ CE [13] (Angle chase)⇒  ∠DEF = 1_PI/3 [27]
-021. ∠(AD-CF) = ∠DFE [22] & AD ∥ BC [03] & ∠FCB = 1_PI/3 [25] & ∠DEF = 1_PI/3 [27] ⇒  ∠DEF = ∠EFD [28]
-022. ∠DEF = ∠EFD [28] ⇒  DE = DF [29]
-023. ∠(CE-AB) = 1_1PI/12 [18] & ∠EDC = 1_PI/12 [05] & AB ∥ CD [02] ⇒  ∠(AB-DE) = ∠(CE-AB) [30]
-024. ∠DAB = ∠(DF-CE) [16] & ∠(AB-DE) = ∠(CE-AB) [30] ⇒  ∠ADE = ∠(DF-AB) [31]
-025. ∠ADE = ∠(DF-AB) [31] & AD ∥ BC [03] & ∠CFD = ∠(DF-AB) [24] ⇒  ∠CFD = ∠ADE [32]
-026. AD = FC [12] & DE = DF [29] & ∠CFD = ∠ADE [32] (SAS)⇒  EA = DC [33]
-027. CD = AB [10] & EA = DC [33] ⇒  EA = AB
-==========================
-
-I0310 09:55:07.134036 130464824438784 alphageometry.py:204] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out2.
-I0310 10:09:03.396387 130464824438784 alphageometry.py:565] Worker 0: Solved.
-I0310 10:09:03.400158 130464824438784 alphageometry.py:670] Worker 0 returned. Solved=True

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

@@ -1,89 +0,0 @@
-++ BATCH_SIZE=8
-++ BEAM_SIZE=60
-++ DEPTH=16
-++ NWORKERS=12
-++ PROB_FILE=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt
-++ PROB=square_angle15_hint
-++ MODEL=ddar
-++ DATA=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab
-++ MELIAD_PATH=/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ export PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ PYTHONPATH=:/home/tong_peng/onedrive_googie32u/alphageometry:/home/tong_peng/pyvenv/ag:/home/tong_peng/pyvenv/ag/meliad_lib/meliad
-++ DDAR_ARGS=(--defs_file=$AGDIR/defs.txt --rules_file=$AGDIR/rules.txt)
-++ SEARCH_ARGS=(--beam_size=$BEAM_SIZE --search_depth=$DEPTH)
-++ LM_ARGS=(--ckpt_path=$DATA --vocab_path=$DATA/geometry.757.model --gin_search_paths=$MELIAD_PATH/transformer/configs,$AGDIR --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False)
-++ true ==========================================
-++ python -m alphageometry --alsologtostderr --problems_file=/home/tong_peng/onedrive_googie32u/agtest/myexamples.txt --problem_name=square_angle15_hint --mode=ddar --defs_file=/home/tong_peng/onedrive_googie32u/alphageometry/defs.txt --rules_file=/home/tong_peng/onedrive_googie32u/alphageometry/rules.txt --beam_size=60 --search_depth=16 --ckpt_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab --vocab_path=/home/tong_peng/pyvenv/ag/ag_ckpt_vocab/geometry.757.model --gin_search_paths=/home/tong_peng/pyvenv/ag/meliad_lib/meliad/transformer/configs,/home/tong_peng/onedrive_googie32u/alphageometry --gin_file=base_htrans.gin --gin_file=size/medium_150M.gin --gin_file=options/positions_t5.gin --gin_file=options/lr_cosine_decay.gin --gin_file=options/seq_1024_nocache.gin --gin_file=geometry_150M_generate.gin --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True --gin_param=TransformerTaskConfig.batch_size=8 --gin_param=TransformerTaskConfig.sequence_length=128 --gin_param=Trainer.restore_state_variables=False --out_file=/home/tong_peng/onedrive_googie32u/agtest/ag.out2 --n_workers=12
-I0309 23:40:56.050346 139793490157568 graph.py:498] square_angle15_hint
-I0309 23:40:56.050746 139793490157568 graph.py:499] a b c d = isquare a b c d; e = s_angle c d e 15, s_angle d c e -15; f = reflect f e a c ? cong e a a b
-I0309 23:41:21.521977 139793490157568 alphageometry.py:200] 
-==========================
- * From theorem premises:
-A B C D E : Points
-AB ⟂ BC [00]
-AB = BC [01]
-AB ∥ CD [02]
-AD ∥ BC [03]
-∠EDC = 1_PI/12 [04]
-∠ECD = 1_1PI/12 [05]
-
- * Auxiliary Constructions:
-F : Points
-CE = CF [06]
-AE = AF [07]
-
- * Proof steps:
-001. AB ∥ CD [02] & BC ∥ AD [03] ⇒  ∠ABC = ∠CDA [08]
-002. BC ∥ AD [03] ⇒  ∠ACB = ∠CAD [09]
-003. ∠ABC = ∠CDA [08] & ∠ACB = ∠CAD [09] (Similar Triangles)⇒  AB = CD [10]
-004. ∠ABC = ∠CDA [08] & ∠ACB = ∠CAD [09] (Similar Triangles)⇒  CB = AD [11]
-005. ∠ABC = ∠CDA [08] & ∠ACB = ∠CAD [09] (Similar Triangles)⇒  BA:BC = DC:DA [12]
-006. CE = CF [06] ⇒  ∠CFE = ∠FEC [13]
-007. ∠EDC = 1_PI/12 [04] & AB ∥ CD [02] ⇒  ∠(DE-AB) = 1_PI/12 [14]
-008. ∠ECD = 1_1PI/12 [05] & AB ∥ CD [02] ⇒  ∠(CE-AB) = 1_1PI/12 [15]
-009. ∠EDC = 1_PI/12 [04] & AB ∥ CD [02] & ∠(CE-AB) = 1_1PI/12 [15] ⇒  ∠(CE-AB) = ∠(AB-DE) [16]
-010. ∠(CE-AB) = ∠(AB-DE) [16] & AB ∥ CD [02] ⇒  ∠ECD = ∠CDE [17]
-011. ∠ECD = ∠CDE [17] ⇒  EC = ED [18]
-012. AB ⟂ BC [00] & ∠(DE-AB) = 1_PI/12 [14] (Angle chase)⇒  ∠(BC-DE) = 5_PI/12 [19]
-013. AB ⟂ BC [00] & ∠(CE-AB) = 1_1PI/12 [15] (Angle chase)⇒  ∠ECB = 5_PI/12 [20]
-014. ∠(BC-DE) = 5_PI/12 [19] & ∠ECB = 5_PI/12 [20] & BC ∥ AD [03] ⇒  ∠ECB = ∠ADE [21]
-015. EC = ED [18] & CB = AD [11] & ∠ECB = ∠ADE [21] (SAS)⇒  BE = AE [22]
-016. AB ⟂ BC [00] & BC ∥ AD [03] & AB ∥ CD [02] ⇒  ∠ABC = ∠ADC [23]
-017. ∠ABC = ∠ADC [23] ⇒  B,C,A,D are concyclic [24]
-018. AB ∥ CD [02] ⇒  ∠BCD = ∠CBA [25]
-019. B,C,A,D are concyclic [24] & ∠BCD = ∠CBA [25] ⇒  BD = CA [26]
-020. BE = AE [22] & EC = ED [18] & BD = CA [26] (SSS)⇒  ∠(BD-CE) = ∠(DE-AC) [27]
-021. BA:BC = DC:DA [12] & AB = BC [01] ⇒  DC = DA [28]
-022. DC = DA [28] & AB = BC [01] ⇒  AC ⟂ DB [29]
-023. AE = AF [07] & CE = CF [06] ⇒  EF ⟂ AC [30]
-024. ∠(BD-CE) = ∠(DE-AC) [27] & AC ⟂ DB [29] & EF ⟂ AC [30] ⇒  ∠FEC = ∠(DE-AC) [31]
-025. AB = BC [01] ⇒  ∠BAC = ∠ACB [32]
-026. AB ⟂ BC [00] & ∠(DE-AB) = 1_PI/12 [14] & ∠BAC = ∠ACB [32] (Angle chase)⇒  ∠(DE-AC) = 1_PI/3 [33]
-027. AB ⟂ BC [00] & ∠(CE-AB) = 1_1PI/12 [15] & ∠BAC = ∠ACB [32] & ∠CFE = ∠FEC [13] & EF ⟂ AC [30] (Angle chase)⇒  ∠ECF = 1_PI/3 [34]
-028. ∠CFE = ∠FEC [13] & ∠FEC = ∠(DE-AC) [31] & ∠(DE-AC) = 1_PI/3 [33] & ∠ECF = 1_PI/3 [34] ⇒  ∠ECF = ∠CFE [35]
-029. ∠ECF = ∠CFE [35] ⇒  EC = EF [36]
-030. AB = BC [01] & AB = CD [10] ⇒  CD = CB [37]
-031. AE = AF [07] & BE = AE [22] ⇒  BE = AF [38]
-032. CE = CF [06] & EC = ED [18] ⇒  ED = FC [39]
-033. BE = AF [38] & ED = FC [39] & BD = CA [26] (SSS)⇒  ∠(BD-AC) = ∠(DE-CF) [40]
-034. AB ⟂ BC [00] & BC ∥ AD [03] ⇒  AD ⟂ BA [41]
-035. AD ⟂ BA [41] & EF ⟂ AC [30] ⇒  ∠DAB = ∠(AC-EF) [42]
-036. AD ⟂ BA [41] & EF ⟂ AC [30] ⇒  ∠DAB = ∠(EF-AC) [43]
-037. ∠(BD-AC) = ∠(DE-CF) [40] & AC ⟂ DB [29] & EF ⟂ AC [30] & ∠DAB = ∠(AC-EF) [42] & AD ∥ BC [03] ⇒  ∠DAB = ∠(FC-ED) [44]
-038. ∠DAB = ∠(FC-ED) [44] & ∠(CE-AB) = ∠(AB-DE) [16] ⇒  ∠(AD-CF) = ∠(CE-AB) [45]
-039. ∠(AD-CF) = ∠(CE-AB) [45] & AD ∥ BC [03] & AB ∥ CD [02] ⇒  ∠FCB = ∠DCE [46]
-040. CE = CF [06] & CD = CB [37] & ∠FCB = ∠DCE [46] (SAS)⇒  BF = DE [47]
-041. ∠(DE-AB) = 1_PI/12 [14] & ∠(CE-AB) = 1_1PI/12 [15] (Angle chase)⇒  ∠DEC = 1_PI/6 [48]
-042. AB ⟂ BC [00] & ∠(DE-AB) = 1_PI/12 [14] & ∠BAC = ∠ACB [32] & EF ⟂ AC [30] (Angle chase)⇒  ∠FED = 1_PI/6 [49]
-043. ∠(BD-AC) = ∠(DE-CF) [40] & AC ⟂ DB [29] & EF ⟂ AC [30] ⇒  FC ⟂ ED [50]
-044. AD ⟂ BA [41] & FC ⟂ ED [50] ⇒  ∠(AD-CF) = ∠(AB-DE) [51]
-045. ∠(AD-CF) = ∠(AB-DE) [51] & AD ∥ BC [03] & AB ∥ CD [02] ⇒  ∠FCB = ∠EDC [52]
-046. ED = FC [39] & CD = CB [37] & ∠FCB = ∠EDC [52] (SAS)⇒  ∠(BF-CE) = ∠BCD [53]
-047. ∠DAB = ∠(EF-AC) [43] & AD ∥ BC [03] & ∠(BF-CE) = ∠BCD [53] & AB ∥ CD [02] ⇒  ∠(BF-EC) = ∠(FE-CA) [54]
-048. ∠(BF-EC) = ∠(FE-CA) [54] & ∠FEC = ∠(DE-AC) [31] ⇒  ∠BFE = ∠FED [55]
-049. ∠DEC = 1_PI/6 [48] & ∠FED = 1_PI/6 [49] & AC ⟂ DB [29] & EF ⟂ AC [30] & ∠BFE = ∠FED [55] ⇒  ∠BFE = ∠DEC [56]
-050. EC = EF [36] & BF = DE [47] & ∠BFE = ∠DEC [56] (SAS)⇒  DC = BE [57]
-051. AB = CD [10] & DC = BE [57] & BE = AE [22] ⇒  EA = AB
-==========================
-
-I0309 23:41:21.524046 139793490157568 alphageometry.py:204] Solution written to /home/tong_peng/onedrive_googie32u/agtest/ag.out2.