1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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)).
|
