Hugging Face's logo

Spaces:
HugoVoxx
/
GeoGenSolve
Running

App Files
GeoGenSolve
File size: 88,610 Bytes 
be3b34d
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
 
++ 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