diff options
Diffstat (limited to 'test/golden/geometry/generating tasks.golden')
| -rw-r--r-- | test/golden/geometry/generating tasks.golden | 17323 |
1 files changed, 0 insertions, 17323 deletions
diff --git a/test/golden/geometry/generating tasks.golden b/test/golden/geometry/generating tasks.golden deleted file mode 100644 index f2be772..0000000 --- a/test/golden/geometry/generating tasks.golden +++ /dev/null @@ -1,17323 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "upperdim" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "innerpasch" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "betw_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "five_segment" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a_" ) - ) - , TermVar - ( B - ( NamedVar "b_" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "ofs" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "r" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "r" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "segment_construction" Quantified Universally - ( Scope - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "d" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "e" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cong_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_pseudotransitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_refl_swap" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "collinear" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ] - , taskConjectureLabel = Marker "cong_refl" - , taskLocation = Location - { locFile = "test/examples/geometry.tex" - , locLine = 82 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "cong_refl" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "upperdim" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "innerpasch" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "betw_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "five_segment" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a_" ) - ) - , TermVar - ( B - ( NamedVar "b_" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "ofs" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "r" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "r" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "segment_construction" Quantified Universally - ( Scope - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "d" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "e" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cong_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_pseudotransitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_refl_swap" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "collinear" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_5" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 90 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - , Hypothesis Marker "_local_4" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - , Hypothesis Marker "_local_3" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ] - , taskConjectureLabel = Marker "cong_sym" - , taskLocation = Location - { locFile = "test/examples/geometry.tex" - , locLine = 88 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 91 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "cong_sym" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 90 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 91 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "cong_refl" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "upperdim" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "innerpasch" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "betw_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "five_segment" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a_" ) - ) - , TermVar - ( B - ( NamedVar "b_" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "ofs" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "r" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "r" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "segment_construction" Quantified Universally - ( Scope - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "d" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "e" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cong_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_pseudotransitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_refl_swap" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "collinear" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_6" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "f" ) - ] - , Hypothesis Marker "_local_5" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "e" ) - ] - , Hypothesis Marker "_local_4" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - , Hypothesis Marker "_local_3" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ] - , taskConjectureLabel = Marker "cong_transitive" - , taskLocation = Location - { locFile = "test/examples/geometry.tex" - , locLine = 95 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 98 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "f" ) - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "cong_transitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "e" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 98 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_sym" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 90 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 91 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "cong_refl" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "upperdim" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "innerpasch" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "betw_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "five_segment" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a_" ) - ) - , TermVar - ( B - ( NamedVar "b_" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "ofs" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "r" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "r" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "segment_construction" Quantified Universally - ( Scope - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "d" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "e" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cong_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_pseudotransitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_refl_swap" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "collinear" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_4" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - , Hypothesis Marker "_local_3" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ] - , taskConjectureLabel = Marker "cong_shuffle_left" - , taskLocation = Location - { locFile = "test/examples/geometry.tex" - , locLine = 102 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 104 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 105 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "cong_shuffle_left" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 104 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 105 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_transitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "e" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 98 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_sym" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 90 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 91 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "cong_refl" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "upperdim" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "innerpasch" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "betw_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "five_segment" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a_" ) - ) - , TermVar - ( B - ( NamedVar "b_" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "ofs" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "r" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "r" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "segment_construction" Quantified Universally - ( Scope - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "d" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "e" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cong_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_pseudotransitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_refl_swap" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "collinear" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_4" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "d" ) - ] - , Hypothesis Marker "_local_3" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - ] - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ] - , taskConjectureLabel = Marker "cong_shuffle_right" - , taskLocation = Location - { locFile = "test/examples/geometry.tex" - , locLine = 109 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 111 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "d" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 112 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "d" ) - , TermVar - ( NamedVar "c" ) - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "cong_shuffle_right" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 110 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 111 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 112 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_shuffle_left" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 103 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 104 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 105 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_transitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "e" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 96 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 97 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 98 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_sym" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 89 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 90 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 91 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "cong_refl" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 83 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 84 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "upperdim" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 67 - , locColumn = 24 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 68 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 69 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 70 - , locColumn = 17 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "innerpasch" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 53 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 54 - , locColumn = 66 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 55 - , locColumn = 37 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "betw_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 47 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 48 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "five_segment" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c_" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 40 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 41 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a_" ) - ) - , TermVar - ( B - ( NamedVar "b_" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "neq" ) - ( ParameterArity 0 ) - ( Marker "neq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 42 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "c_" ) - ) - , TermVar - ( B - ( NamedVar "d_" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "ofs" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "r" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "u" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "v" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "w" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 27 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 26 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateSymbol "OFS" ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "r" ) - ) - , TermVar - ( B - ( NamedVar "u" ) - ) - , TermVar - ( B - ( NamedVar "v" ) - ) - , TermVar - ( B - ( NamedVar "w" ) - ) - , TermVar - ( B - ( NamedVar "p" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 29 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 30 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 32 - , locColumn = 6 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 33 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "z" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "w" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 34 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "u" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 35 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "y" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "r" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "v" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "p" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "segment_construction" Quantified Universally - ( Scope - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 22 - , locColumn = 62 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "d" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "e" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cong_id" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 16 - , locColumn = 22 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 17 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_pseudotransitive" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 11 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "c" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 12 - , locColumn = 58 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "e" ) - ) - , TermVar - ( B - ( NamedVar "f" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "cong_refl_swap" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 6 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 7 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "a" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "collinear" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "collinear" ) - ( TokenCons - ( Word "with" ) - ( HoleCons - ( TokenCons - ( Word "and" ) ( HoleCons End ) - ) - ) - ) - ) - ( Marker "collinear" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( B - ( NamedVar "c" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Disjunction - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 64 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 2 - , locColumn = 84 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Betw" ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "c" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "b" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 117 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 117 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "point" ) End - , pl = TokenCons - ( Word "points" ) End - } - ) - ( Marker "point" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - ] - ] - , taskConjectureLabel = Marker "cong_zero" - , taskLocation = Location - { locFile = "test/examples/geometry.tex" - , locLine = 116 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/geometry.tex" - , locLine = 118 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateSymbol "Cong" ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "b" ) - ] - } -]
\ No newline at end of file |