++ 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