diff options
Diffstat (limited to 'test/golden/geometry')
| -rw-r--r-- | test/golden/geometry/encoding tasks.golden | 109 | ||||
| -rw-r--r-- | test/golden/geometry/generating tasks.golden | 14419 | ||||
| -rw-r--r-- | test/golden/geometry/glossing.golden | 2187 | ||||
| -rw-r--r-- | test/golden/geometry/parsing.golden | 1198 | ||||
| -rw-r--r-- | test/golden/geometry/scanning.golden | 15 | ||||
| -rw-r--r-- | test/golden/geometry/tokenizing.golden | 975 | ||||
| -rw-r--r-- | test/golden/geometry/verification.golden | 1 |
7 files changed, 18904 insertions, 0 deletions
diff --git a/test/golden/geometry/encoding tasks.golden b/test/golden/geometry/encoding tasks.golden new file mode 100644 index 0000000..f4bbc14 --- /dev/null +++ b/test/golden/geometry/encoding tasks.golden @@ -0,0 +1,109 @@ +fof(cong_refl,conjecture,'Cong'(fa,fb,fa,fb)). +fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). +fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). +fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). +fof(five_segment,axiom,![Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xaprime)&point(Xbprime)&point(Xcprime)&point(Xdprime))=>(('OFS'(Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime)&Xa!=Xb)=>'Cong'(Xc,Xd,Xcprime,Xdprime)))). +fof(ofs,axiom,![Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp]:((point(Xx)&point(Xy)&point(Xz)&point(Xr)&point(Xu)&point(Xv)&point(Xw)&point(Xp))=>('OFS'(Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp)<=>('Betw'(Xx,Xy,Xz)&'Betw'(Xu,Xv,Xw)&'Cong'(Xx,Xy,Xu,Xv)&'Cong'(Xy,Xz,Xv,Xw)&'Cong'(Xx,Xr,Xu,Xp)&'Cong'(Xy,Xr,Xv,Xp))))). +fof(segment_construction,axiom,![Xa,Xb,Xd,Xe]:?[Xc]:(point(Xc)&'Betw'(Xa,Xb,Xc)&'Cong'(Xb,Xc,Xd,Xe))). +fof(cong_id,axiom,![Xa,Xb,Xc]:((point(Xa)&point(Xb)&point(Xc))=>('Cong'(Xa,Xb,Xc,Xc)=>Xa=Xb))). +fof(cong_pseudotransitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>(('Cong'(Xc,Xd,Xa,Xb)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_refl_swap,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xb,Xa))). +fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'(Xb,Xc,Xa)|'Betw'(Xc,Xa,Xb)))). +fof(cong_refl1,axiom,point(fb)). +fof(cong_refl2,axiom,point(fa)). +------------------ +fof(cong_sym,conjecture,'Cong'(fc,fd,fa,fb)). +fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). +fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). +fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). +fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). +fof(five_segment,axiom,![Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xaprime)&point(Xbprime)&point(Xcprime)&point(Xdprime))=>(('OFS'(Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime)&Xa!=Xb)=>'Cong'(Xc,Xd,Xcprime,Xdprime)))). +fof(ofs,axiom,![Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp]:((point(Xx)&point(Xy)&point(Xz)&point(Xr)&point(Xu)&point(Xv)&point(Xw)&point(Xp))=>('OFS'(Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp)<=>('Betw'(Xx,Xy,Xz)&'Betw'(Xu,Xv,Xw)&'Cong'(Xx,Xy,Xu,Xv)&'Cong'(Xy,Xz,Xv,Xw)&'Cong'(Xx,Xr,Xu,Xp)&'Cong'(Xy,Xr,Xv,Xp))))). +fof(segment_construction,axiom,![Xa,Xb,Xd,Xe]:?[Xc]:(point(Xc)&'Betw'(Xa,Xb,Xc)&'Cong'(Xb,Xc,Xd,Xe))). +fof(cong_id,axiom,![Xa,Xb,Xc]:((point(Xa)&point(Xb)&point(Xc))=>('Cong'(Xa,Xb,Xc,Xc)=>Xa=Xb))). +fof(cong_pseudotransitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>(('Cong'(Xc,Xd,Xa,Xb)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_refl_swap,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xb,Xa))). +fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'(Xb,Xc,Xa)|'Betw'(Xc,Xa,Xb)))). +fof(cong_sym1,axiom,'Cong'(fa,fb,fc,fd)). +fof(cong_sym2,axiom,point(fd)). +fof(cong_sym3,axiom,point(fc)). +fof(cong_sym4,axiom,point(fb)). +fof(cong_sym5,axiom,point(fa)). +------------------ +fof(cong_transitive,conjecture,('Cong'(fa,fb,fc,fd)&'Cong'(fc,fd,fe,ff))=>'Cong'(fa,fb,fe,ff)). +fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). +fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). +fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). +fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). +fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). +fof(five_segment,axiom,![Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xaprime)&point(Xbprime)&point(Xcprime)&point(Xdprime))=>(('OFS'(Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime)&Xa!=Xb)=>'Cong'(Xc,Xd,Xcprime,Xdprime)))). +fof(ofs,axiom,![Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp]:((point(Xx)&point(Xy)&point(Xz)&point(Xr)&point(Xu)&point(Xv)&point(Xw)&point(Xp))=>('OFS'(Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp)<=>('Betw'(Xx,Xy,Xz)&'Betw'(Xu,Xv,Xw)&'Cong'(Xx,Xy,Xu,Xv)&'Cong'(Xy,Xz,Xv,Xw)&'Cong'(Xx,Xr,Xu,Xp)&'Cong'(Xy,Xr,Xv,Xp))))). +fof(segment_construction,axiom,![Xa,Xb,Xd,Xe]:?[Xc]:(point(Xc)&'Betw'(Xa,Xb,Xc)&'Cong'(Xb,Xc,Xd,Xe))). +fof(cong_id,axiom,![Xa,Xb,Xc]:((point(Xa)&point(Xb)&point(Xc))=>('Cong'(Xa,Xb,Xc,Xc)=>Xa=Xb))). +fof(cong_pseudotransitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>(('Cong'(Xc,Xd,Xa,Xb)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_refl_swap,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xb,Xa))). +fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'(Xb,Xc,Xa)|'Betw'(Xc,Xa,Xb)))). +fof(cong_transitive1,axiom,point(ff)). +fof(cong_transitive2,axiom,point(fe)). +fof(cong_transitive3,axiom,point(fd)). +fof(cong_transitive4,axiom,point(fc)). +fof(cong_transitive5,axiom,point(fb)). +fof(cong_transitive6,axiom,point(fa)). +------------------ +fof(cong_shuffle_left,conjecture,'Cong'(fa,fb,fc,fd)=>'Cong'(fb,fa,fc,fd)). +fof(cong_transitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xe)&point(Xf))=>(('Cong'(Xa,Xb,Xc,Xd)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). +fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). +fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). +fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). +fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). +fof(five_segment,axiom,![Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xaprime)&point(Xbprime)&point(Xcprime)&point(Xdprime))=>(('OFS'(Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime)&Xa!=Xb)=>'Cong'(Xc,Xd,Xcprime,Xdprime)))). +fof(ofs,axiom,![Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp]:((point(Xx)&point(Xy)&point(Xz)&point(Xr)&point(Xu)&point(Xv)&point(Xw)&point(Xp))=>('OFS'(Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp)<=>('Betw'(Xx,Xy,Xz)&'Betw'(Xu,Xv,Xw)&'Cong'(Xx,Xy,Xu,Xv)&'Cong'(Xy,Xz,Xv,Xw)&'Cong'(Xx,Xr,Xu,Xp)&'Cong'(Xy,Xr,Xv,Xp))))). +fof(segment_construction,axiom,![Xa,Xb,Xd,Xe]:?[Xc]:(point(Xc)&'Betw'(Xa,Xb,Xc)&'Cong'(Xb,Xc,Xd,Xe))). +fof(cong_id,axiom,![Xa,Xb,Xc]:((point(Xa)&point(Xb)&point(Xc))=>('Cong'(Xa,Xb,Xc,Xc)=>Xa=Xb))). +fof(cong_pseudotransitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>(('Cong'(Xc,Xd,Xa,Xb)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_refl_swap,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xb,Xa))). +fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'(Xb,Xc,Xa)|'Betw'(Xc,Xa,Xb)))). +fof(cong_shuffle_left1,axiom,point(fd)). +fof(cong_shuffle_left2,axiom,point(fc)). +fof(cong_shuffle_left3,axiom,point(fb)). +fof(cong_shuffle_left4,axiom,point(fa)). +------------------ +fof(cong_shuffle_right,conjecture,'Cong'(fa,fb,fc,fd)=>'Cong'(fb,fa,fd,fc)). +fof(cong_shuffle_left,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>('Cong'(Xa,Xb,Xc,Xd)=>'Cong'(Xb,Xa,Xc,Xd)))). +fof(cong_transitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xe)&point(Xf))=>(('Cong'(Xa,Xb,Xc,Xd)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). +fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). +fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). +fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). +fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). +fof(five_segment,axiom,![Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xaprime)&point(Xbprime)&point(Xcprime)&point(Xdprime))=>(('OFS'(Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime)&Xa!=Xb)=>'Cong'(Xc,Xd,Xcprime,Xdprime)))). +fof(ofs,axiom,![Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp]:((point(Xx)&point(Xy)&point(Xz)&point(Xr)&point(Xu)&point(Xv)&point(Xw)&point(Xp))=>('OFS'(Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp)<=>('Betw'(Xx,Xy,Xz)&'Betw'(Xu,Xv,Xw)&'Cong'(Xx,Xy,Xu,Xv)&'Cong'(Xy,Xz,Xv,Xw)&'Cong'(Xx,Xr,Xu,Xp)&'Cong'(Xy,Xr,Xv,Xp))))). +fof(segment_construction,axiom,![Xa,Xb,Xd,Xe]:?[Xc]:(point(Xc)&'Betw'(Xa,Xb,Xc)&'Cong'(Xb,Xc,Xd,Xe))). +fof(cong_id,axiom,![Xa,Xb,Xc]:((point(Xa)&point(Xb)&point(Xc))=>('Cong'(Xa,Xb,Xc,Xc)=>Xa=Xb))). +fof(cong_pseudotransitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>(('Cong'(Xc,Xd,Xa,Xb)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_refl_swap,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xb,Xa))). +fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'(Xb,Xc,Xa)|'Betw'(Xc,Xa,Xb)))). +fof(cong_shuffle_right1,axiom,point(fd)). +fof(cong_shuffle_right2,axiom,point(fc)). +fof(cong_shuffle_right3,axiom,point(fb)). +fof(cong_shuffle_right4,axiom,point(fa)). +------------------ +fof(cong_zero,conjecture,'Cong'(fa,fa,fb,fb)). +fof(cong_shuffle_right,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>('Cong'(Xa,Xb,Xc,Xd)=>'Cong'(Xb,Xa,Xd,Xc)))). +fof(cong_shuffle_left,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>('Cong'(Xa,Xb,Xc,Xd)=>'Cong'(Xb,Xa,Xc,Xd)))). +fof(cong_transitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xe)&point(Xf))=>(('Cong'(Xa,Xb,Xc,Xd)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). +fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). +fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). +fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). +fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). +fof(five_segment,axiom,![Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xaprime)&point(Xbprime)&point(Xcprime)&point(Xdprime))=>(('OFS'(Xa,Xb,Xc,Xd,Xaprime,Xbprime,Xcprime,Xdprime)&Xa!=Xb)=>'Cong'(Xc,Xd,Xcprime,Xdprime)))). +fof(ofs,axiom,![Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp]:((point(Xx)&point(Xy)&point(Xz)&point(Xr)&point(Xu)&point(Xv)&point(Xw)&point(Xp))=>('OFS'(Xx,Xy,Xz,Xr,Xu,Xv,Xw,Xp)<=>('Betw'(Xx,Xy,Xz)&'Betw'(Xu,Xv,Xw)&'Cong'(Xx,Xy,Xu,Xv)&'Cong'(Xy,Xz,Xv,Xw)&'Cong'(Xx,Xr,Xu,Xp)&'Cong'(Xy,Xr,Xv,Xp))))). +fof(segment_construction,axiom,![Xa,Xb,Xd,Xe]:?[Xc]:(point(Xc)&'Betw'(Xa,Xb,Xc)&'Cong'(Xb,Xc,Xd,Xe))). +fof(cong_id,axiom,![Xa,Xb,Xc]:((point(Xa)&point(Xb)&point(Xc))=>('Cong'(Xa,Xb,Xc,Xc)=>Xa=Xb))). +fof(cong_pseudotransitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>(('Cong'(Xc,Xd,Xa,Xb)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). +fof(cong_refl_swap,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xb,Xa))). +fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'(Xb,Xc,Xa)|'Betw'(Xc,Xa,Xb)))). +fof(cong_zero1,axiom,point(fb)). +fof(cong_zero2,axiom,point(fa)).
\ No newline at end of file diff --git a/test/golden/geometry/generating tasks.golden b/test/golden/geometry/generating tasks.golden new file mode 100644 index 0000000..a2869ea --- /dev/null +++ b/test/golden/geometry/generating tasks.golden @@ -0,0 +1,14419 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "r" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "d" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "e" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_refl1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_refl2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_refl" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "r" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "d" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "e" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_sym1" + , TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_sym2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_sym3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_sym4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_sym5" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_sym" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "r" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "d" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "e" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_transitive1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "f" ) + ] + ) + , + ( Marker "cong_transitive2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "e" ) + ] + ) + , + ( Marker "cong_transitive3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_transitive4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_transitive5" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_transitive6" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_transitive" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "e" ) + , TermVar + ( NamedVar "f" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "e" ) + , TermVar + ( NamedVar "f" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_transitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "e" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "r" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "d" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "e" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_shuffle_left1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_shuffle_left2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_shuffle_left3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_shuffle_left4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_shuffle_left" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_shuffle_left" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_transitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "e" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "r" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "d" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "e" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_shuffle_right1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , + ( Marker "cong_shuffle_right2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , + ( Marker "cong_shuffle_right3" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_shuffle_right4" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_shuffle_right" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "c" ) + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "cong_shuffle_right" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_shuffle_left" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_transitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "e" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_sym" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "cong_refl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "upperdim" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "innerpasch" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "betw_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "five_segment" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "aprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "bprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "cprime" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "aprime" ) + ) + , TermVar + ( B + ( NamedVar "bprime" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "cprime" ) + ) + , TermVar + ( B + ( NamedVar "dprime" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ofs" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "r" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "u" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "v" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ) + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( B + ( NamedVar "r" ) + ) + , TermVar + ( B + ( NamedVar "u" ) + ) + , TermVar + ( B + ( NamedVar "v" ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "p" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "z" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "w" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "x" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "u" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "y" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "r" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "v" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "p" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "segment_construction" + , Quantified Universally + ( Scope + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "d" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "e" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_id" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_pseudotransitive" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "d" ) + ) + ] + ) + ) + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( B + ( NamedVar "d" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "e" ) + ) + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "cong_refl_swap" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "collinear" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "c" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "b" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cong_zero1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , + ( Marker "cong_zero2" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + ] + , taskConjectureLabel = Marker "cong_zero" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "b" ) + ] + } +]
\ No newline at end of file diff --git a/test/golden/geometry/glossing.golden b/test/golden/geometry/glossing.golden new file mode 100644 index 0000000..f1e1bd2 --- /dev/null +++ b/test/golden/geometry/glossing.golden @@ -0,0 +1,2187 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "collinear" ) + ( DefnPredicate [] + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "a" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 5 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_refl_swap" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + ] + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + ] + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 10 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_pseudotransitive" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + ] + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ( 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" ) + ] + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_id" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + ] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "c" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 21 + , sourceColumn = Pos 1 + } + ) + ( Marker "segment_construction" ) + ( Axiom [] + ( 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 + ( NamedVar "a" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "b" ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "b" ) + ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "d" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "e" ) + ) + ) + ] + ) + ) + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 26 + , sourceColumn = Pos 1 + } + ) + ( Marker "ofs" ) + ( DefnPredicate + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "z" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "r" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "u" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "v" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "w" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "p" ) + ] + ) + ] + ( PredicateSymbol "OFS" ) + ( NamedVar "x" :| + [ NamedVar "y" + , NamedVar "z" + , NamedVar "r" + , NamedVar "u" + , NamedVar "v" + , NamedVar "w" + , NamedVar "p" + ] + ) + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "z" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "v" ) + , TermVar + ( NamedVar "w" ) + ] + ) + ) + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "v" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "z" ) + , TermVar + ( NamedVar "v" ) + , TermVar + ( NamedVar "w" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "r" ) + , TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "p" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "r" ) + , TermVar + ( NamedVar "v" ) + , TermVar + ( NamedVar "p" ) + ] + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 39 + , sourceColumn = Pos 1 + } + ) + ( Marker "five_segment" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "aprime" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "bprime" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "cprime" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "dprime" ) + ] + ) + ] + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "OFS" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "aprime" ) + , TermVar + ( NamedVar "bprime" ) + , TermVar + ( NamedVar "cprime" ) + , TermVar + ( NamedVar "dprime" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "c" ) + , TermVar + ( NamedVar "d" ) + , TermVar + ( NamedVar "cprime" ) + , TermVar + ( NamedVar "dprime" ) + ] + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 46 + , sourceColumn = Pos 1 + } + ) + ( Marker "betw_id" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + ] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 52 + , sourceColumn = Pos 1 + } + ) + ( Marker "innerpasch" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "z" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "u" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "v" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "w" ) + ] + ) + ] + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "z" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "v" ) + , TermVar + ( 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 + ( NamedVar "u" ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "y" ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Betw" ) + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "v" ) + ) + ) + , TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "x" ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 66 + , sourceColumn = Pos 1 + } + ) + ( Marker "upperdim" ) + ( Axiom + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "x" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "y" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "z" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "u" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "v" ) + ] + ) + ] + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "v" ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "v" ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "z" ) + , TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "z" ) + , TermVar + ( NamedVar "v" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "neq" ) + ) + ) + [ TermVar + ( NamedVar "u" ) + , TermVar + ( NamedVar "v" ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "z" ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 82 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_refl" ) + ( Lemma + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + ] + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 88 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_sym" ) + ( Lemma + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , Asm + ( 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 "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 95 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_transitive" ) + ( Lemma + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "e" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "f" ) + ] + ) + ] + ( 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" ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 102 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_shuffle_left" ) + ( Lemma + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + ] + ( 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" ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 109 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_shuffle_right" ) + ( Lemma + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "c" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "d" ) + ] + ) + ] + ( 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" ) + ] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 116 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_zero" ) + ( Lemma + [ Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "a" ) + ] + ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "b" ) + ] + ) + ] + ( TermSymbol + ( SymbolPredicate + ( PredicateSymbol "Cong" ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) +]
\ No newline at end of file diff --git a/test/golden/geometry/parsing.golden b/test/golden/geometry/parsing.golden new file mode 100644 index 0000000..b57f76c --- /dev/null +++ b/test/golden/geometry/parsing.golden @@ -0,0 +1,1198 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "collinear" ) + ( Defn [] + ( DefnAdj Nothing + ( NamedVar "a" ) + ( Adj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + [ NamedVar "b" + , NamedVar "c" + ] + ) + ) + ( StmtConnected Disjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + ] + ) + ) + ) + ( StmtConnected Disjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "b" ) :| + [ ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "a" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "c" ) :| + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 5 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_refl_swap" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "a" ) + ] + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 10 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_pseudotransitive" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + , NamedVar "d" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "c" ) :| + [ ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "c" ) :| + [ ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "e" ) + , ExprVar + ( NamedVar "f" ) + ] + ) + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "e" ) + , ExprVar + ( NamedVar "f" ) + ] + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_id" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "c" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "b" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 21 + , sourceColumn = Pos 1 + } + ) + ( Marker "segment_construction" ) + ( Axiom [] + ( StmtExists NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) + ( + [ NamedVar "c" ] + ) ( [] ) + ( Just + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "b" ) :| + [ ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "e" ) + ] + ) + ) + ) + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 26 + , sourceColumn = Pos 1 + } + ) + ( Marker "ofs" ) + ( Defn + [ AsmLetNoun + ( NamedVar "x" :| + [ NamedVar "y" + , NamedVar "z" + , NamedVar "r" + , NamedVar "u" + , NamedVar "v" + , NamedVar "w" + , NamedVar "p" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( DefnSymbolicPredicate + ( PrefixPredicate "OFS" 8 ) + ( NamedVar "x" :| + [ NamedVar "y" + , NamedVar "z" + , NamedVar "r" + , NamedVar "u" + , NamedVar "v" + , NamedVar "w" + , NamedVar "p" + ] + ) + ) + ( StmtConnected Conjunction + ( StmtFormula + ( Connected Conjunction + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "x" ) :| + [ ExprVar + ( NamedVar "y" ) + , ExprVar + ( NamedVar "z" ) + ] + ) + ) + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "u" ) :| + [ ExprVar + ( NamedVar "v" ) + , ExprVar + ( NamedVar "w" ) + ] + ) + ) + ) + ) + ( StmtFormula + ( Connected Conjunction + ( Connected Conjunction + ( Connected Conjunction + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "x" ) :| + [ ExprVar + ( NamedVar "y" ) + , ExprVar + ( NamedVar "u" ) + , ExprVar + ( NamedVar "v" ) + ] + ) + ) + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "y" ) :| + [ ExprVar + ( NamedVar "z" ) + , ExprVar + ( NamedVar "v" ) + , ExprVar + ( NamedVar "w" ) + ] + ) + ) + ) + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "x" ) :| + [ ExprVar + ( NamedVar "r" ) + , ExprVar + ( NamedVar "u" ) + , ExprVar + ( NamedVar "p" ) + ] + ) + ) + ) + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "y" ) :| + [ ExprVar + ( NamedVar "r" ) + , ExprVar + ( NamedVar "v" ) + , ExprVar + ( NamedVar "p" ) + ] + ) + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 39 + , sourceColumn = Pos 1 + } + ) + ( Marker "five_segment" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + , NamedVar "d" + , NamedVar "aprime" + , NamedVar "bprime" + , NamedVar "cprime" + , NamedVar "dprime" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "OFS" 8 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "aprime" ) + , ExprVar + ( NamedVar "bprime" ) + , ExprVar + ( NamedVar "cprime" ) + , ExprVar + ( NamedVar "dprime" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "neq" ) + ) + ( ExprVar + ( NamedVar "b" ) :| [] + ) + ) + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "c" ) :| + [ ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "cprime" ) + , ExprVar + ( NamedVar "dprime" ) + ] + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 46 + , sourceColumn = Pos 1 + } + ) + ( Marker "betw_id" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "a" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "b" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 52 + , sourceColumn = Pos 1 + } + ) + ( Marker "innerpasch" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "x" :| + [ NamedVar "y" + , NamedVar "z" + , NamedVar "u" + , NamedVar "v" + , NamedVar "w" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "x" ) :| + [ ExprVar + ( NamedVar "u" ) + , ExprVar + ( NamedVar "z" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "y" ) :| + [ ExprVar + ( NamedVar "v" ) + , ExprVar + ( NamedVar "z" ) + ] + ) + ) + ) + ) + ( StmtExists NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) + ( + [ NamedVar "w" ] + ) ( [] ) + ( Just + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "u" ) :| + [ ExprVar + ( NamedVar "w" ) + , ExprVar + ( NamedVar "y" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Betw" 3 ) + ( ExprVar + ( NamedVar "v" ) :| + [ ExprVar + ( NamedVar "w" ) + , ExprVar + ( NamedVar "x" ) + ] + ) + ) + ) + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 66 + , sourceColumn = Pos 1 + } + ) + ( Marker "upperdim" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "x" :| + [ NamedVar "y" + , NamedVar "z" + , NamedVar "u" + , NamedVar "v" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "x" ) :| + [ ExprVar + ( NamedVar "u" ) + , ExprVar + ( NamedVar "x" ) + , ExprVar + ( NamedVar "v" ) + ] + ) + ) + ) + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "y" ) :| + [ ExprVar + ( NamedVar "u" ) + , ExprVar + ( NamedVar "y" ) + , ExprVar + ( NamedVar "v" ) + ] + ) + ) + ) + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "z" ) :| + [ ExprVar + ( NamedVar "u" ) + , ExprVar + ( NamedVar "z" ) + , ExprVar + ( NamedVar "v" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "u" ) :| [] + ) Positive + ( RelationSymbol + ( Command "neq" ) + ) + ( ExprVar + ( NamedVar "v" ) :| [] + ) + ) + ) + ) + ) + ) + ) + ( StmtVerbPhrase + ( TermExpr + ( ExprVar + ( NamedVar "x" ) + ) :| [] + ) + ( VPAdj + ( Adj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + [ TermExpr + ( ExprVar + ( NamedVar "y" ) + ) + , TermExpr + ( ExprVar + ( NamedVar "z" ) + ) + ] :| [] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 82 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_refl" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 88 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_sym" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + , NamedVar "d" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + , AsmSuppose + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + ] + ) + ) + ) + ] + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "c" ) :| + [ ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 95 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_transitive" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + , NamedVar "d" + , NamedVar "e" + , NamedVar "f" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "c" ) :| + [ ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "e" ) + , ExprVar + ( NamedVar "f" ) + ] + ) + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "e" ) + , ExprVar + ( NamedVar "f" ) + ] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 102 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_shuffle_left" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + , NamedVar "d" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "b" ) :| + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + ] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 109 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_shuffle_right" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" + , NamedVar "c" + , NamedVar "d" + ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Implication + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + , ExprVar + ( NamedVar "d" ) + ] + ) + ) + ) + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "b" ) :| + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "d" ) + , ExprVar + ( NamedVar "c" ) + ] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/geometry.tex" + , sourceLine = Pos 116 + , sourceColumn = Pos 1 + } + ) + ( Marker "cong_zero" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "a" :| + [ NamedVar "b" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "point" ) + ] + , pl = + [ Just + ( Word "points" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtFormula + ( FormulaPredicate + ( PrefixPredicate "Cong" 4 ) + ( ExprVar + ( NamedVar "a" ) :| + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/geometry/scanning.golden b/test/golden/geometry/scanning.golden new file mode 100644 index 0000000..c041c1a --- /dev/null +++ b/test/golden/geometry/scanning.golden @@ -0,0 +1,15 @@ +[ ScanAdj + [ Just + ( Word "collinear" ) + , Just + ( Word "with" ) + , Nothing + , Just + ( Word "and" ) + , Nothing + ] + ( Marker "collinear" ) +, ScanPrefixPredicate + ( PrefixPredicate "OFS" 8 ) + ( Marker "ofs" ) +]
\ No newline at end of file diff --git a/test/golden/geometry/tokenizing.golden b/test/golden/geometry/tokenizing.golden new file mode 100644 index 0000000..ab899fe --- /dev/null +++ b/test/golden/geometry/tokenizing.golden @@ -0,0 +1,975 @@ +[ BeginEnv "definition" +, Label "collinear" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "is" +, Word "collinear" +, Word "with" +, BeginEnv "math" +, Variable "b" +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "c" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, EndEnv "math" +, Word "or" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, EndEnv "math" +, Word "or" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "axiom" +, BracketL +, Word "reflexivity" +, Word "of" +, Word "congruence" +, BracketR +, Label "cong_refl_swap" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, BracketL +, Word "pseudotransitivity" +, Word "of" +, Word "congruence" +, BracketR +, Label "cong_pseudotransitive" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, Symbol "," +, Variable "d" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "e" +, InvisibleBraceR +, InvisibleBraceL +, Variable "f" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "e" +, InvisibleBraceR +, InvisibleBraceL +, Variable "f" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, BracketL +, Word "identity" +, Word "of" +, Word "congruence" +, BracketR +, Label "cong_id" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Variable "a" +, Symbol "=" +, Variable "b" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, BracketL +, Word "segment" +, Word "construction" +, BracketR +, Label "segment_construction" +, Word "there" +, Word "exists" +, Word "a" +, Word "point" +, BeginEnv "math" +, Variable "c" +, EndEnv "math" +, Word "such" +, Word "that" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "e" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "definition" +, Label "ofs" +, Word "let" +, BeginEnv "math" +, Variable "x" +, Symbol "," +, Variable "y" +, Symbol "," +, Variable "z" +, Symbol "," +, Variable "r" +, Symbol "," +, Variable "u" +, Symbol "," +, Variable "v" +, Symbol "," +, Variable "w" +, Symbol "," +, Variable "p" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, BeginEnv "math" +, Command "OFS" +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, InvisibleBraceL +, Variable "r" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, InvisibleBraceL +, Variable "w" +, InvisibleBraceR +, InvisibleBraceL +, Variable "p" +, InvisibleBraceR +, EndEnv "math" +, Word "if" +, Word "and" +, Word "only" +, Word "if" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, Command "land" +, Command "Betw" +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, InvisibleBraceL +, Variable "w" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, Command "land" +, Command "Cong" +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, InvisibleBraceL +, Variable "w" +, InvisibleBraceR +, Command "land" +, Command "Cong" +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "r" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "p" +, InvisibleBraceR +, Command "land" +, Command "Cong" +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "r" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, InvisibleBraceL +, Variable "p" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "axiom" +, BracketL +, Word "five" +, Word "segment" +, Word "axiom" +, BracketR +, Label "five_segment" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, Symbol "," +, Variable "d" +, Symbol "," +, Variable "aprime" +, Symbol "," +, Variable "bprime" +, Symbol "," +, Variable "cprime" +, Symbol "," +, Variable "dprime" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "OFS" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "aprime" +, InvisibleBraceR +, InvisibleBraceL +, Variable "bprime" +, InvisibleBraceR +, InvisibleBraceL +, Variable "cprime" +, InvisibleBraceR +, InvisibleBraceL +, Variable "dprime" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "a" +, Command "neq" +, Variable "b" +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "cprime" +, InvisibleBraceR +, InvisibleBraceL +, Variable "dprime" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, BracketL +, Word "identity" +, Word "of" +, Word "betweenness" +, BracketR +, Label "betw_id" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Variable "a" +, Symbol "=" +, Variable "b" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, BracketL +, Word "inner" +, Word "pasch" +, BracketR +, Label "innerpasch" +, Word "let" +, BeginEnv "math" +, Variable "x" +, Symbol "," +, Variable "y" +, Symbol "," +, Variable "z" +, Symbol "," +, Variable "u" +, Symbol "," +, Variable "v" +, Symbol "," +, Variable "w" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, Word "there" +, Word "exists" +, Word "a" +, Word "point" +, BeginEnv "math" +, Variable "w" +, EndEnv "math" +, Word "such" +, Word "that" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "w" +, InvisibleBraceR +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Betw" +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, InvisibleBraceL +, Variable "w" +, InvisibleBraceR +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, BracketL +, Word "upper" +, Word "dimension" +, BracketR +, Label "upperdim" +, Word "let" +, BeginEnv "math" +, Variable "x" +, Symbol "," +, Variable "y" +, Symbol "," +, Variable "z" +, Symbol "," +, Variable "u" +, Symbol "," +, Variable "v" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, InvisibleBraceL +, Variable "u" +, InvisibleBraceR +, InvisibleBraceL +, Variable "z" +, InvisibleBraceR +, InvisibleBraceL +, Variable "v" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "u" +, Command "neq" +, Variable "v" +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "is" +, Word "collinear" +, Word "with" +, BeginEnv "math" +, Variable "y" +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "z" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "lemma" +, BracketL +, Word "reflexivity" +, Word "of" +, Word "congruence" +, BracketR +, Label "cong_refl" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +, BeginEnv "lemma" +, BracketL +, Word "symmetry" +, Word "of" +, Word "congruence" +, BracketR +, Label "cong_sym" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, Symbol "," +, Variable "d" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "suppose" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +, BeginEnv "lemma" +, BracketL +, Word "transitivity" +, Word "of" +, Word "congruence" +, BracketR +, Label "cong_transitive" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, Symbol "," +, Variable "d" +, Symbol "," +, Variable "e" +, Symbol "," +, Variable "f" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "e" +, InvisibleBraceR +, InvisibleBraceL +, Variable "f" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "e" +, InvisibleBraceR +, InvisibleBraceL +, Variable "f" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +, BeginEnv "lemma" +, Label "cong_shuffle_left" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, Symbol "," +, Variable "d" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +, BeginEnv "lemma" +, Label "cong_shuffle_right" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, Symbol "," +, Variable "c" +, Symbol "," +, Variable "d" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "if" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, EndEnv "math" +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "d" +, InvisibleBraceR +, InvisibleBraceL +, Variable "c" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +, BeginEnv "lemma" +, BracketL +, Word "zero" +, Word "segments" +, Word "are" +, Word "congruent" +, BracketR +, Label "cong_zero" +, Word "let" +, BeginEnv "math" +, Variable "a" +, Symbol "," +, Variable "b" +, EndEnv "math" +, Word "be" +, Word "points" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Command "Cong" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, InvisibleBraceL +, Variable "b" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +]
\ No newline at end of file diff --git a/test/golden/geometry/verification.golden b/test/golden/geometry/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/geometry/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |
