diff options
Diffstat (limited to 'test/golden/geometry/generating tasks.golden')
| -rw-r--r-- | test/golden/geometry/generating tasks.golden | 14419 |
1 files changed, 14419 insertions, 0 deletions
diff --git a/test/golden/geometry/generating tasks.golden b/test/golden/geometry/generating tasks.golden new file mode 100644 index 0000000..a2869ea --- /dev/null +++ b/test/golden/geometry/generating tasks.golden @@ -0,0 +1,14419 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( 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 + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( 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 + ( 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 + ( 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 + ( 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 + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_refl1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_refl2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_refl" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( 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 + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( 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 + ( 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 + ( 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 + ( 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 + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_sym1" + , TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_sym2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_sym3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_sym4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_sym5" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_sym" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( 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 + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( 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 + ( 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 + ( 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 + ( 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 + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_transitive1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "f" ) + ] + ) + , + ( Marker "cong_transitive2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "e" ) + ] + ) + , + ( Marker "cong_transitive3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_transitive4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_transitive5" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_transitive6" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_transitive" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "e" ) + , TermVar + ( NamedVar "f" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "e" ) + , TermVar + ( NamedVar "f" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_transitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "e" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( 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 + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( 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 + ( 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 + ( 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 + ( 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 + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_shuffle_left1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_shuffle_left2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_shuffle_left3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_shuffle_left4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_shuffle_left" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_shuffle_left" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_transitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "e" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( 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 + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( 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 + ( 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 + ( 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 + ( 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 + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_shuffle_right1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_shuffle_right2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_shuffle_right3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_shuffle_right4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_shuffle_right" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "c" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_shuffle_right" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_shuffle_left" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_transitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "e" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( 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 + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( 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 + ( 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 + ( 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 + ( 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 + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( 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" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_zero1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_zero2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_zero" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "b" ) + ] + } +]
\ No newline at end of file |