angle congruences, but not similarity

[unhandyandy]

Not the following three theorems have exactly the same hypotheses.

test1
b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? eqangle g d g c h b h c
test2
b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? eqangle b c b d c g c d
test3
b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? simtri c g d b h c

AG is able to prove the first two, which establish that two of corresponding angles in cgb and bhc are congruent; but it is unable to prove the third, that the two triangles are similar.

Thinking that combining test1 and test2 to deduce test3 might require a little more computing space, I tried increasing the parameters

BATCH_SIZE=2
BEAM_SIZE=2
DEPTH=2

But that didn't work

Anyone have an idea what's going on here?

[1509cxt]

Please check the point elements in the conclusion(goal) of your test2. We can see that the point H wasn't mentioned in it. But you know, mentioning point H is necessary for the similarity you want to prove :)

[unhandyandy]

Tests 1 and 2 were successful. Only test3 failed.

[1509cxt]

I mean, the similarity you want to prove in the test3 is wrong.

Please manually check whether there is a deductive relation between the conclusions of your test1&2 and the similarity you want to prove in the test3.

[unhandyandy]

Ah, I see what you mean . Actually angle cbd is congruent to cbh; and when I change test2 to b c d = triangle b c d; a = circumcenter a b c d; e = on_line e b d, on_tline e c c a; f = on_line f e c, on_tline f b b d; g = on_line g e c, on_tline g d d b; h = on_line h b d, on_line h a c ? eqangle b c b h c g c d it still works.