Miquel's Theorem:
If four circles are arranged in sequence, each two successive circle intersecting, and a circle pass through one point of each pair of intersection, then the remaining intersections lie on another circle.

Machine input:

Point order : ABCDEGFH

Hypothesis: cyclic(ABCD) cyclic(ABEF) cyclic(BCFG) cyclic(CDGH) cyclic(DAEH)

Conclusion: cyclic(EFGH)

Machine output:

[FG,FE] + [HG,HE]
=   - [FG,FC] + [FE,FC] + [HG,HE]
        ( because -1.0[FG,FE] = -1.0[FG,FC] + [FE,FC])
=   - [GB,CB] + [FE,FC] + [HG,HE]
        ( because cyclic(F,G,C,B) => -1.0[FG,FC] = -1.0[GB,CB] )
=   - [GB,CB] + [FE,FB] - [FC,FB] + [HG,HE]
        ( because [FE,FC] = [FE,FB] + -1.0[FC,FB])
=   - [GB,CB] + [EA,BA] - [FC,FB] + [HG,HE]
        ( because cyclic(F,E,B,A) => [FE,FB] = [EA,BA] )
=   - [GB,CB] + [EA,BA] - [GC,GB] + [HG,HE]
        ( because cyclic(F,C,B,G) => -1.0[FC,FB] = -1.0[GC,GB] )
=   - [GC,CB] + [EA,BA] + [HG,HE]
        ( because -1.0[GB,CB] = [GC,GB]+-1.0[GC,CB], simplifying )
=   - [GC,CB] + [EA,BA] + [HG,HD] - [HE,HD]
        ( because [HG,HE] = [HG,HD] + -1.0[HE,HD])
=   - [GC,CB] + [EA,BA] + [GC,DC] - [HE,HD]
        ( because cyclic(H,G,D,C) => [HG,HD] = [GC,DC] )
=   - [GC,CB] + [EA,BA] + [GC,DC] - [EA,DA]
        ( because cyclic(H,E,D,A) => -1.0[HE,HD] = -1.0[EA,DA] )
=   - [DC,CB] + [EA,BA] - [EA,DA]
        ( because -1.0[GC,CB] = -1.0[GC,DC]+-1.0[DC,CB], simplifying )
=   - [DA,BA] + [EA,BA] - [EA,DA]
        ( because cyclic(D,C,B,A) => -1.0[DC,CB] = -1.0[DA,BA] )
=   0.0