[ 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" ) ] } ]