[ BlockDefn
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 1
        , locColumn = 1
        }
    ) Nothing
    ( Marker "collinear" )
    ( Defn []
        ( DefnAdj Nothing
            ( NamedVar "a" )
            ( Adj
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 2
                    , locColumn = 12
                    }
                )
                ( LexicalItem
                    ( TokenCons
                        ( Word "collinear" )
                        ( TokenCons
                            ( Word "with" )
                            ( HoleCons
                                ( TokenCons
                                    ( Word "and" ) ( HoleCons End )
                                )
                            )
                        )
                    )
                    ( Marker "collinear" )
                )
                [ NamedVar "b"
                , NamedVar "c"
                ]
            )
        )
        ( StmtConnected
            { conn = Disjunction
            , mloc = Nothing
            , stmt1 = StmtConnected
                { conn = Disjunction
                , mloc = Nothing
                , stmt1 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 2
                            , locColumn = 44
                            }
                        )
                        ( PrefixPredicate "Betw" 3 )
                        ( Marker "betw" )
                        ( ExprVar
                            ( NamedVar "a" ) :|
                            [ ExprVar
                                ( NamedVar "b" )
                            , ExprVar
                                ( NamedVar "c" )
                            ]
                        )
                    }
                , stmt2 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 2
                            , locColumn = 64
                            }
                        )
                        ( PrefixPredicate "Betw" 3 )
                        ( Marker "betw" )
                        ( ExprVar
                            ( NamedVar "b" ) :|
                            [ ExprVar
                                ( NamedVar "c" )
                            , ExprVar
                                ( NamedVar "a" )
                            ]
                        )
                    }
                }
            , stmt2 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 2
                        , locColumn = 84
                        }
                    )
                    ( PrefixPredicate "Betw" 3 )
                    ( Marker "betw" )
                    ( ExprVar
                        ( NamedVar "c" ) :|
                        [ ExprVar
                            ( NamedVar "a" )
                        , ExprVar
                            ( NamedVar "b" )
                        ]
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 5
        , locColumn = 1
        }
    )
    ( Just
        [ Word "reflexivity"
        , Word "of"
        , Word "congruence"
        ]
    )
    ( Marker "cong_refl_swap" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b" ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 6
                    , locColumn = 19
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtFormula
            { formula = FormulaPredicate
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 7
                    , locColumn = 11
                    }
                )
                ( PrefixPredicate "Cong" 4 )
                ( Marker "cong" )
                ( ExprVar
                    ( NamedVar "a" ) :|
                    [ ExprVar
                        ( NamedVar "b" )
                    , ExprVar
                        ( NamedVar "b" )
                    , ExprVar
                        ( NamedVar "a" )
                    ]
                )
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 10
        , locColumn = 1
        }
    )
    ( Just
        [ Word "pseudotransitivity"
        , Word "of"
        , Word "congruence"
        ]
    )
    ( Marker "cong_pseudotransitive" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                , NamedVar "d"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 11
                    , locColumn = 25
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 12
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtConnected
                { conn = Conjunction
                , mloc = Nothing
                , stmt1 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 12
                            , locColumn = 9
                            }
                        )
                        ( PrefixPredicate "Cong" 4 )
                        ( Marker "cong" )
                        ( ExprVar
                            ( NamedVar "c" ) :|
                            [ ExprVar
                                ( NamedVar "d" )
                            , ExprVar
                                ( NamedVar "a" )
                            , ExprVar
                                ( NamedVar "b" )
                            ]
                        )
                    }
                , stmt2 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 12
                            , locColumn = 33
                            }
                        )
                        ( PrefixPredicate "Cong" 4 )
                        ( Marker "cong" )
                        ( ExprVar
                            ( NamedVar "c" ) :|
                            [ ExprVar
                                ( NamedVar "d" )
                            , ExprVar
                                ( NamedVar "e" )
                            , ExprVar
                                ( NamedVar "f" )
                            ]
                        )
                    }
                }
            , stmt2 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 12
                        , locColumn = 58
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "e" )
                        , ExprVar
                            ( NamedVar "f" )
                        ]
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 15
        , locColumn = 1
        }
    )
    ( Just
        [ Word "identity"
        , Word "of"
        , Word "congruence"
        ]
    )
    ( Marker "cong_id" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 16
                    , locColumn = 22
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 17
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 17
                        , locColumn = 9
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "c" )
                        , ExprVar
                            ( NamedVar "c" )
                        ]
                    )
                }
            , stmt2 = StmtFormula
                { formula = FormulaChain
                    ( ChainBase
                        ( ExprVar
                            ( NamedVar "a" ) :| []
                        ) Positive
                        ( Relation
                            ( Location
                                { locFile = "test/examples/geometry.tex"
                                , locLine = 17
                                , locColumn = 36
                                }
                            )
                            ( RelationSymbol
                                ( Symbol "=" )
                                ( ParameterArity 0 )
                                ( Marker "eq" )
                            ) []
                        )
                        ( ExprVar
                            ( NamedVar "b" ) :| []
                        )
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 21
        , locColumn = 1
        }
    )
    ( Just
        [ Word "segment"
        , Word "construction"
        ]
    )
    ( Marker "segment_construction" )
    ( Axiom []
        ( StmtExists
            { loc = Location
                { locFile = "test/examples/geometry.tex"
                , locLine = 22
                , locColumn = 5
                }
            , np = NounPhrase ( [] )
                ( Noun
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 22
                        , locColumn = 20
                        }
                    )
                    ( LexicalItemSgPl
                        ( SgPl
                            { sg = TokenCons
                                ( Word "point" ) End
                            , pl = TokenCons
                                ( Word "points" ) End
                            }
                        )
                        ( Marker "point" )
                    ) []
                )
                (
                    [ NamedVar "c" ]
                ) ( [] )
                ( Just
                    ( StmtConnected
                        { conn = Conjunction
                        , mloc = Nothing
                        , stmt1 = StmtFormula
                            { formula = FormulaPredicate
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 22
                                    , locColumn = 41
                                    }
                                )
                                ( PrefixPredicate "Betw" 3 )
                                ( Marker "betw" )
                                ( ExprVar
                                    ( NamedVar "a" ) :|
                                    [ ExprVar
                                        ( NamedVar "b" )
                                    , ExprVar
                                        ( NamedVar "c" )
                                    ]
                                )
                            }
                        , stmt2 = StmtFormula
                            { formula = FormulaPredicate
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 22
                                    , locColumn = 62
                                    }
                                )
                                ( PrefixPredicate "Cong" 4 )
                                ( Marker "cong" )
                                ( ExprVar
                                    ( NamedVar "b" ) :|
                                    [ ExprVar
                                        ( NamedVar "c" )
                                    , ExprVar
                                        ( NamedVar "d" )
                                    , ExprVar
                                        ( NamedVar "e" )
                                    ]
                                )
                            }
                        }
                    )
                )
            }
        )
    )
, BlockDefn
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 26
        , locColumn = 1
        }
    ) Nothing
    ( Marker "ofs" )
    ( Defn
        [ AsmLetNoun
            ( NamedVar "x" :|
                [ NamedVar "y"
                , NamedVar "z"
                , NamedVar "r"
                , NamedVar "u"
                , NamedVar "v"
                , NamedVar "w"
                , NamedVar "p"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 27
                    , locColumn = 30
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( DefnSymbolicPredicate
            ( PrefixPredicate "OFS" 8 )
            ( Marker "ofs" )
            ( NamedVar "x" :|
                [ NamedVar "y"
                , NamedVar "z"
                , NamedVar "r"
                , NamedVar "u"
                , NamedVar "v"
                , NamedVar "w"
                , NamedVar "p"
                ]
            )
        )
        ( StmtConnected
            { conn = Conjunction
            , mloc = Nothing
            , stmt1 = StmtFormula
                { formula = Connected
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 29
                        , locColumn = 6
                        }
                    ) Conjunction
                    ( FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 29
                            , locColumn = 6
                            }
                        )
                        ( PrefixPredicate "Betw" 3 )
                        ( Marker "betw" )
                        ( ExprVar
                            ( NamedVar "x" ) :|
                            [ ExprVar
                                ( NamedVar "y" )
                            , ExprVar
                                ( NamedVar "z" )
                            ]
                        )
                    )
                    ( FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 30
                            , locColumn = 13
                            }
                        )
                        ( PrefixPredicate "Betw" 3 )
                        ( Marker "betw" )
                        ( ExprVar
                            ( NamedVar "u" ) :|
                            [ ExprVar
                                ( NamedVar "v" )
                            , ExprVar
                                ( NamedVar "w" )
                            ]
                        )
                    )
                }
            , stmt2 = StmtFormula
                { formula = Connected
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 32
                        , locColumn = 6
                        }
                    ) Conjunction
                    ( Connected
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 32
                            , locColumn = 6
                            }
                        ) Conjunction
                        ( Connected
                            ( Location
                                { locFile = "test/examples/geometry.tex"
                                , locLine = 32
                                , locColumn = 6
                                }
                            ) Conjunction
                            ( FormulaPredicate
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 32
                                    , locColumn = 6
                                    }
                                )
                                ( PrefixPredicate "Cong" 4 )
                                ( Marker "cong" )
                                ( ExprVar
                                    ( NamedVar "x" ) :|
                                    [ ExprVar
                                        ( NamedVar "y" )
                                    , ExprVar
                                        ( NamedVar "u" )
                                    , ExprVar
                                        ( NamedVar "v" )
                                    ]
                                )
                            )
                            ( FormulaPredicate
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 33
                                    , locColumn = 13
                                    }
                                )
                                ( PrefixPredicate "Cong" 4 )
                                ( Marker "cong" )
                                ( ExprVar
                                    ( NamedVar "y" ) :|
                                    [ ExprVar
                                        ( NamedVar "z" )
                                    , ExprVar
                                        ( NamedVar "v" )
                                    , ExprVar
                                        ( NamedVar "w" )
                                    ]
                                )
                            )
                        )
                        ( FormulaPredicate
                            ( Location
                                { locFile = "test/examples/geometry.tex"
                                , locLine = 34
                                , locColumn = 13
                                }
                            )
                            ( PrefixPredicate "Cong" 4 )
                            ( Marker "cong" )
                            ( ExprVar
                                ( NamedVar "x" ) :|
                                [ ExprVar
                                    ( NamedVar "r" )
                                , ExprVar
                                    ( NamedVar "u" )
                                , ExprVar
                                    ( NamedVar "p" )
                                ]
                            )
                        )
                    )
                    ( FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 35
                            , locColumn = 13
                            }
                        )
                        ( PrefixPredicate "Cong" 4 )
                        ( Marker "cong" )
                        ( ExprVar
                            ( NamedVar "y" ) :|
                            [ ExprVar
                                ( NamedVar "r" )
                            , ExprVar
                                ( NamedVar "v" )
                            , ExprVar
                                ( NamedVar "p" )
                            ]
                        )
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 39
        , locColumn = 1
        }
    )
    ( Just
        [ Word "five"
        , Word "segment"
        , Word "axiom"
        ]
    )
    ( Marker "five_segment" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                , NamedVar "d"
                , NamedVar "a_"
                , NamedVar "b_"
                , NamedVar "c_"
                , NamedVar "d_"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 40
                    , locColumn = 34
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 41
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtConnected
                { conn = Conjunction
                , mloc = Nothing
                , stmt1 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 41
                            , locColumn = 9
                            }
                        )
                        ( PrefixPredicate "OFS" 8 )
                        ( Marker "ofs" )
                        ( ExprVar
                            ( NamedVar "a" ) :|
                            [ ExprVar
                                ( NamedVar "b" )
                            , ExprVar
                                ( NamedVar "c" )
                            , ExprVar
                                ( NamedVar "d" )
                            , ExprVar
                                ( NamedVar "a_" )
                            , ExprVar
                                ( NamedVar "b_" )
                            , ExprVar
                                ( NamedVar "c_" )
                            , ExprVar
                                ( NamedVar "d_" )
                            ]
                        )
                    }
                , stmt2 = StmtFormula
                    { formula = FormulaChain
                        ( ChainBase
                            ( ExprVar
                                ( NamedVar "a" ) :| []
                            ) Positive
                            ( Relation
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 42
                                    , locColumn = 8
                                    }
                                )
                                ( RelationSymbol
                                    ( Command "neq" )
                                    ( ParameterArity 0 )
                                    ( Marker "neq" )
                                ) []
                            )
                            ( ExprVar
                                ( NamedVar "b" ) :| []
                            )
                        )
                    }
                }
            , stmt2 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 42
                        , locColumn = 22
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "c" ) :|
                        [ ExprVar
                            ( NamedVar "d" )
                        , ExprVar
                            ( NamedVar "c_" )
                        , ExprVar
                            ( NamedVar "d_" )
                        ]
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 46
        , locColumn = 1
        }
    )
    ( Just
        [ Word "identity"
        , Word "of"
        , Word "betweenness"
        ]
    )
    ( Marker "betw_id" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b" ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 47
                    , locColumn = 18
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 48
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 48
                        , locColumn = 9
                        }
                    )
                    ( PrefixPredicate "Betw" 3 )
                    ( Marker "betw" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "a" )
                        ]
                    )
                }
            , stmt2 = StmtFormula
                { formula = FormulaChain
                    ( ChainBase
                        ( ExprVar
                            ( NamedVar "a" ) :| []
                        ) Positive
                        ( Relation
                            ( Location
                                { locFile = "test/examples/geometry.tex"
                                , locLine = 48
                                , locColumn = 33
                                }
                            )
                            ( RelationSymbol
                                ( Symbol "=" )
                                ( ParameterArity 0 )
                                ( Marker "eq" )
                            ) []
                        )
                        ( ExprVar
                            ( NamedVar "b" ) :| []
                        )
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 52
        , locColumn = 1
        }
    )
    ( Just
        [ Word "inner"
        , Word "pasch"
        ]
    )
    ( Marker "innerpasch" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "x" :|
                [ NamedVar "y"
                , NamedVar "z"
                , NamedVar "u"
                , NamedVar "v"
                , NamedVar "w"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 53
                    , locColumn = 26
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 54
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtConnected
                { conn = Conjunction
                , mloc = Nothing
                , stmt1 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 54
                            , locColumn = 9
                            }
                        )
                        ( PrefixPredicate "Betw" 3 )
                        ( Marker "betw" )
                        ( ExprVar
                            ( NamedVar "x" ) :|
                            [ ExprVar
                                ( NamedVar "u" )
                            , ExprVar
                                ( NamedVar "z" )
                            ]
                        )
                    }
                , stmt2 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 54
                            , locColumn = 30
                            }
                        )
                        ( PrefixPredicate "Betw" 3 )
                        ( Marker "betw" )
                        ( ExprVar
                            ( NamedVar "y" ) :|
                            [ ExprVar
                                ( NamedVar "v" )
                            , ExprVar
                                ( NamedVar "z" )
                            ]
                        )
                    }
                }
            , stmt2 = StmtExists
                { loc = Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 54
                    , locColumn = 51
                    }
                , np = NounPhrase ( [] )
                    ( Noun
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 54
                            , locColumn = 66
                            }
                        )
                        ( LexicalItemSgPl
                            ( SgPl
                                { sg = TokenCons
                                    ( Word "point" ) End
                                , pl = TokenCons
                                    ( Word "points" ) End
                                }
                            )
                            ( Marker "point" )
                        ) []
                    )
                    (
                        [ NamedVar "w" ]
                    ) ( [] )
                    ( Just
                        ( StmtConnected
                            { conn = Conjunction
                            , mloc = Nothing
                            , stmt1 = StmtFormula
                                { formula = FormulaPredicate
                                    ( Location
                                        { locFile = "test/examples/geometry.tex"
                                        , locLine = 55
                                        , locColumn = 16
                                        }
                                    )
                                    ( PrefixPredicate "Betw" 3 )
                                    ( Marker "betw" )
                                    ( ExprVar
                                        ( NamedVar "u" ) :|
                                        [ ExprVar
                                            ( NamedVar "w" )
                                        , ExprVar
                                            ( NamedVar "y" )
                                        ]
                                    )
                                }
                            , stmt2 = StmtFormula
                                { formula = FormulaPredicate
                                    ( Location
                                        { locFile = "test/examples/geometry.tex"
                                        , locLine = 55
                                        , locColumn = 37
                                        }
                                    )
                                    ( PrefixPredicate "Betw" 3 )
                                    ( Marker "betw" )
                                    ( ExprVar
                                        ( NamedVar "v" ) :|
                                        [ ExprVar
                                            ( NamedVar "w" )
                                        , ExprVar
                                            ( NamedVar "x" )
                                        ]
                                    )
                                }
                            }
                        )
                    )
                }
            }
        )
    )
, BlockAxiom
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 66
        , locColumn = 1
        }
    )
    ( Just
        [ Word "upper"
        , Word "dimension"
        ]
    )
    ( Marker "upperdim" )
    ( Axiom
        [ AsmLetNoun
            ( NamedVar "x" :|
                [ NamedVar "y"
                , NamedVar "z"
                , NamedVar "u"
                , NamedVar "v"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 67
                    , locColumn = 24
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 68
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtConnected
                { conn = Conjunction
                , mloc = Nothing
                , stmt1 = StmtConnected
                    { conn = Conjunction
                    , mloc = Nothing
                    , stmt1 = StmtConnected
                        { conn = Conjunction
                        , mloc = Nothing
                        , stmt1 = StmtFormula
                            { formula = FormulaPredicate
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 68
                                    , locColumn = 9
                                    }
                                )
                                ( PrefixPredicate "Cong" 4 )
                                ( Marker "cong" )
                                ( ExprVar
                                    ( NamedVar "x" ) :|
                                    [ ExprVar
                                        ( NamedVar "u" )
                                    , ExprVar
                                        ( NamedVar "x" )
                                    , ExprVar
                                        ( NamedVar "v" )
                                    ]
                                )
                            }
                        , stmt2 = StmtFormula
                            { formula = FormulaPredicate
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 68
                                    , locColumn = 33
                                    }
                                )
                                ( PrefixPredicate "Cong" 4 )
                                ( Marker "cong" )
                                ( ExprVar
                                    ( NamedVar "y" ) :|
                                    [ ExprVar
                                        ( NamedVar "u" )
                                    , ExprVar
                                        ( NamedVar "y" )
                                    , ExprVar
                                        ( NamedVar "v" )
                                    ]
                                )
                            }
                        }
                    , stmt2 = StmtFormula
                        { formula = FormulaPredicate
                            ( Location
                                { locFile = "test/examples/geometry.tex"
                                , locLine = 69
                                , locColumn = 10
                                }
                            )
                            ( PrefixPredicate "Cong" 4 )
                            ( Marker "cong" )
                            ( ExprVar
                                ( NamedVar "z" ) :|
                                [ ExprVar
                                    ( NamedVar "u" )
                                , ExprVar
                                    ( NamedVar "z" )
                                , ExprVar
                                    ( NamedVar "v" )
                                ]
                            )
                        }
                    }
                , stmt2 = StmtFormula
                    { formula = FormulaChain
                        ( ChainBase
                            ( ExprVar
                                ( NamedVar "u" ) :| []
                            ) Positive
                            ( Relation
                                ( Location
                                    { locFile = "test/examples/geometry.tex"
                                    , locLine = 69
                                    , locColumn = 36
                                    }
                                )
                                ( RelationSymbol
                                    ( Command "neq" )
                                    ( ParameterArity 0 )
                                    ( Marker "neq" )
                                ) []
                            )
                            ( ExprVar
                                ( NamedVar "v" ) :| []
                            )
                        )
                    }
                }
            , stmt2 = StmtVerbPhrase
                { args = TermExpr
                    ( ExprVar
                        ( NamedVar "x" )
                    ) :| []
                , verb = VPAdj
                    ( Adj
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 70
                            , locColumn = 17
                            }
                        )
                        ( LexicalItem
                            ( TokenCons
                                ( Word "collinear" )
                                ( TokenCons
                                    ( Word "with" )
                                    ( HoleCons
                                        ( TokenCons
                                            ( Word "and" ) ( HoleCons End )
                                        )
                                    )
                                )
                            )
                            ( Marker "collinear" )
                        )
                        [ TermExpr
                            ( ExprVar
                                ( NamedVar "y" )
                            )
                        , TermExpr
                            ( ExprVar
                                ( NamedVar "z" )
                            )
                        ] :| []
                    )
                }
            }
        )
    )
, BlockClaim Lemma
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 82
        , locColumn = 1
        }
    )
    ( Just
        [ Word "reflexivity"
        , Word "of"
        , Word "congruence"
        ]
    )
    ( Marker "cong_refl" )
    ( Claim
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b" ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 83
                    , locColumn = 19
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtFormula
            { formula = FormulaPredicate
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 84
                    , locColumn = 11
                    }
                )
                ( PrefixPredicate "Cong" 4 )
                ( Marker "cong" )
                ( ExprVar
                    ( NamedVar "a" ) :|
                    [ ExprVar
                        ( NamedVar "b" )
                    , ExprVar
                        ( NamedVar "a" )
                    , ExprVar
                        ( NamedVar "b" )
                    ]
                )
            }
        )
    )
, BlockClaim Lemma
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 88
        , locColumn = 1
        }
    )
    ( Just
        [ Word "symmetry"
        , Word "of"
        , Word "congruence"
        ]
    )
    ( Marker "cong_sym" )
    ( Claim
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                , NamedVar "d"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 89
                    , locColumn = 25
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        , AsmSuppose
            ( StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 90
                        , locColumn = 14
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "c" )
                        , ExprVar
                            ( NamedVar "d" )
                        ]
                    )
                }
            )
        ]
        ( StmtFormula
            { formula = FormulaPredicate
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 91
                    , locColumn = 11
                    }
                )
                ( PrefixPredicate "Cong" 4 )
                ( Marker "cong" )
                ( ExprVar
                    ( NamedVar "c" ) :|
                    [ ExprVar
                        ( NamedVar "d" )
                    , ExprVar
                        ( NamedVar "a" )
                    , ExprVar
                        ( NamedVar "b" )
                    ]
                )
            }
        )
    )
, BlockClaim Lemma
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 95
        , locColumn = 1
        }
    )
    ( Just
        [ Word "transitivity"
        , Word "of"
        , Word "congruence"
        ]
    )
    ( Marker "cong_transitive" )
    ( Claim
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                , NamedVar "d"
                , NamedVar "e"
                , NamedVar "f"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 96
                    , locColumn = 31
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 97
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtConnected
                { conn = Conjunction
                , mloc = Nothing
                , stmt1 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 97
                            , locColumn = 9
                            }
                        )
                        ( PrefixPredicate "Cong" 4 )
                        ( Marker "cong" )
                        ( ExprVar
                            ( NamedVar "a" ) :|
                            [ ExprVar
                                ( NamedVar "b" )
                            , ExprVar
                                ( NamedVar "c" )
                            , ExprVar
                                ( NamedVar "d" )
                            ]
                        )
                    }
                , stmt2 = StmtFormula
                    { formula = FormulaPredicate
                        ( Location
                            { locFile = "test/examples/geometry.tex"
                            , locLine = 97
                            , locColumn = 33
                            }
                        )
                        ( PrefixPredicate "Cong" 4 )
                        ( Marker "cong" )
                        ( ExprVar
                            ( NamedVar "c" ) :|
                            [ ExprVar
                                ( NamedVar "d" )
                            , ExprVar
                                ( NamedVar "e" )
                            , ExprVar
                                ( NamedVar "f" )
                            ]
                        )
                    }
                }
            , stmt2 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 98
                        , locColumn = 11
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "e" )
                        , ExprVar
                            ( NamedVar "f" )
                        ]
                    )
                }
            }
        )
    )
, BlockClaim Lemma
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 102
        , locColumn = 1
        }
    ) Nothing
    ( Marker "cong_shuffle_left" )
    ( Claim
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                , NamedVar "d"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 103
                    , locColumn = 25
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 104
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 104
                        , locColumn = 9
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "c" )
                        , ExprVar
                            ( NamedVar "d" )
                        ]
                    )
                }
            , stmt2 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 105
                        , locColumn = 11
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "b" ) :|
                        [ ExprVar
                            ( NamedVar "a" )
                        , ExprVar
                            ( NamedVar "c" )
                        , ExprVar
                            ( NamedVar "d" )
                        ]
                    )
                }
            }
        )
    )
, BlockClaim Lemma
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 109
        , locColumn = 1
        }
    ) Nothing
    ( Marker "cong_shuffle_right" )
    ( Claim
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b"
                , NamedVar "c"
                , NamedVar "d"
                ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 110
                    , locColumn = 25
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtConnected
            { conn = Implication
            , mloc = Just
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 111
                    , locColumn = 5
                    }
                )
            , stmt1 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 111
                        , locColumn = 9
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "a" ) :|
                        [ ExprVar
                            ( NamedVar "b" )
                        , ExprVar
                            ( NamedVar "c" )
                        , ExprVar
                            ( NamedVar "d" )
                        ]
                    )
                }
            , stmt2 = StmtFormula
                { formula = FormulaPredicate
                    ( Location
                        { locFile = "test/examples/geometry.tex"
                        , locLine = 112
                        , locColumn = 11
                        }
                    )
                    ( PrefixPredicate "Cong" 4 )
                    ( Marker "cong" )
                    ( ExprVar
                        ( NamedVar "b" ) :|
                        [ ExprVar
                            ( NamedVar "a" )
                        , ExprVar
                            ( NamedVar "d" )
                        , ExprVar
                            ( NamedVar "c" )
                        ]
                    )
                }
            }
        )
    )
, BlockClaim Lemma
    ( Location
        { locFile = "test/examples/geometry.tex"
        , locLine = 116
        , locColumn = 1
        }
    )
    ( Just
        [ Word "zero"
        , Word "segments"
        , Word "are"
        , Word "congruent"
        ]
    )
    ( Marker "cong_zero" )
    ( Claim
        [ AsmLetNoun
            ( NamedVar "a" :|
                [ NamedVar "b" ]
            ) NounPhrase ( [] )
            ( Noun
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 117
                    , locColumn = 18
                    }
                )
                ( LexicalItemSgPl
                    ( SgPl
                        { sg = TokenCons
                            ( Word "point" ) End
                        , pl = TokenCons
                            ( Word "points" ) End
                        }
                    )
                    ( Marker "point" )
                ) []
            ) ( Nothing ) ( [] ) ( Nothing )
        ]
        ( StmtFormula
            { formula = FormulaPredicate
                ( Location
                    { locFile = "test/examples/geometry.tex"
                    , locLine = 118
                    , locColumn = 11
                    }
                )
                ( PrefixPredicate "Cong" 4 )
                ( Marker "cong" )
                ( ExprVar
                    ( NamedVar "a" ) :|
                    [ ExprVar
                        ( NamedVar "a" )
                    , ExprVar
                        ( NamedVar "b" )
                    , ExprVar
                        ( NamedVar "b" )
                    ]
                )
            }
        )
    )
]