% problem-set/geometry/tarski/t9.ver1.clauses
% created : 07/16/86
% revised : 08/08/89

% description : 

% Theorem T9: For all points x, y, z, and w, if y and w are between x and
% z, then either y is between x and w or w is between x and y.

% representation :
%
% declare_predicates(4,[L]).
% declare_predicates(3,[B,C]).
% declare_predicates(2,[EQ]).
% declare_functions(6,[cont]).
% declare_functions(5,[op,euc1,euc2]).
% declare_functions(4,[ext]).
% declare_constants([C1,C2,C3,a,b,c,d,e]).
% declare_variables([u,v,w,x,y,z,v1,v2,v3,v4,v5,x1,y1,z1]). 
%
% Note that skolem functions have been renamed to agree with the second
% axiom set's names, for purposed of consistency and readability. Also,
% the weakened form of the continuity axiom, axiom A13', is used.
%
% B(x,y,z) : y is between x and z.
% L(x1,y1,x2,y2) : the distance from x1 to y1 equals that from x2 to y2. 
% C1, C2, C3 : Skolem constants arising from the Lower Dimension Axiom (A11)
% op   : Skolem function arising from Outer Pasch Axiom (A7)
% euc1 : Skolem function arising from Euclid's Axiom (A8)
% euc2 : Skolem function arising from Euclid's Axiom (A8)
% ext  : Skolem function arising from the Segment Construction Axiom (A10)
% cont : Skolem function arising from the Weakened form of the Elementary
% 	Continuity Axiom (A13')

% A8 : Euclid's Axiom
% B(u,v,euc1(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) |  EQ(u,w).
% B(u,x,euc2(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) |  EQ(u,w).
% B(euc1(u,v,w,x,y),y,euc2(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) |  EQ(u,w).

% A13 : Continuity Axiom (Weak Form)
% -L(v,x,v,x1) | -L(v,z,v,z1) | -B(v,x,z) | -B(x,y,z) | L(v,y,v,cont(x,y,z,x1,z1,v)).
% -L(v,x,v,x1) | -L(v,z,v,z1) | -B(v,x,z) | -B(x,y,z) | B(x1,cont(x,y,z,x1,z1,v),z1).

%  Equality axioms
EQ(x,x).
-EQ(x,y) | EQ(y,x).
-EQ(x,y) | -EQ(y,z) |  EQ(x,z).
 
%  Equality Substitution Axioms
-B(x,w,z) |  B(y,w,z) | -EQ(x,y).
-B(w,x,z) |  B(w,y,z) | -EQ(x,y).
-B(w,z,x) |  B(w,z,y) | -EQ(x,y).
% -C(x,w,z) |  C(y,w,z) | -EQ(x,y).
% -C(w,x,z) |  C(w,y,z) | -EQ(x,y).
% -C(w,z,x) |  C(w,z,y) | -EQ(x,y).
-L(x,v,w,z) |  L(y,v,w,z) | -EQ(x,y).
-L(v,x,w,z) |  L(v,y,w,z) | -EQ(x,y).
-L(v,w,x,z) |  L(v,w,y,z) | -EQ(x,y).
-L(v,w,z,x) |  L(v,w,y,z) | -EQ(x,y).
EQ(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)) | -EQ(x,y).
EQ(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)) | -EQ(x,y).
EQ(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)) | -EQ(x,y).
EQ(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)) | -EQ(x,y).
EQ(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)) | -EQ(x,y).
% EQ(euc1(x,v1,v2,v3,v4),euc1(y,v1,v2,v3,v4)) | -EQ(x,y).
% EQ(euc1(v1,x,v2,v3,v4),euc1(v1,y,v2,v3,v4)) | -EQ(x,y).
% EQ(euc1(v1,v2,x,v3,v4),euc1(v1,v2,y,v3,v4)) | -EQ(x,y).
% EQ(euc1(v1,v2,v3,x,v4),euc1(v1,v2,v3,y,v4)) | -EQ(x,y).
% EQ(euc1(v1,v2,v3,v4,x),euc1(v1,v2,v3,v4,y)) | -EQ(x,y).
% EQ(euc2(x,v1,v2,v3,v4),euc2(y,v1,v2,v3,v4)) | -EQ(x,y).
% EQ(euc2(v1,x,v2,v3,v4),euc2(v1,y,v2,v3,v4)) | -EQ(x,y).
% EQ(euc2(v1,v2,x,v3,v4),euc2(v1,v2,y,v3,v4)) | -EQ(x,y).
% EQ(euc2(v1,v2,v3,x,v4),euc2(v1,v2,v3,y,v4)) | -EQ(x,y).
% EQ(euc2(v1,v2,v3,v4,x),euc2(v1,v2,v3,v4,y)) | -EQ(x,y).
EQ(ext(x,v1,v2,v3),ext(y,v1,v2,v3)) | -EQ(x,y).
EQ(ext(v1,x,v2,v3),ext(v1,y,v2,v3)) | -EQ(x,y).
EQ(ext(v1,v2,x,v3),ext(v1,v2,y,v3)) | -EQ(x,y).
EQ(ext(v1,v2,v3,x),ext(v1,v2,v3,y)) | -EQ(x,y).
% EQ(cont(x,v1,v2,v3,v4,v5),cont(y,v1,v2,v3,v4,v5)) | -EQ(x,y).
% EQ(cont(v1,x,v2,v3,v4,v5),cont(v1,y,v2,v3,v4,v5)) | -EQ(x,y).
% EQ(cont(v1,v2,x,v3,v4,v5),cont(v1,v2,y,v3,v4,v5)) | -EQ(x,y).
% EQ(cont(v1,v2,v3,x,v4,v5),cont(v1,v2,v3,y,v4,v5)) | -EQ(x,y).
% EQ(cont(v1,v2,v3,v4,x,v5),cont(v1,v2,v3,v4,y,v5)) | -EQ(x,y).
% EQ(cont(v1,v2,v3,v4,v5,x),cont(v1,v2,v3,v4,v5,y)) | -EQ(x,y).


% A1 : Identity axiom for betweenness 
-B(x,y,x) |  EQ(x,y).

% A2 : Transitivity axiom for betweenness
-B(x,y,v) | -B(y,z,v) |  B(x,y,z).

% A3 : Connectivity axiom for betweenness
-B(x,y,z) | -B(x,y,v) | B(x,z,v) |  B(x,v,z) | EQ(x,y).

% A4 : Reflexivity axiom for equidistance
L(x,y,y,x).

% A5 : Identity axiom for equidistance
-L(x,y,z,z) |  EQ(x,y).

% A6 : Transitivity axiom for equidistance
-L(x,y,z,v) | -L(x,y,v2,w) |  L(z,v,v2,w).

% A7 : Outer Pasch Axiom
B(x,op(w,x,y,z,v),y) | -B(x,w,v) | -B(y,v,z).
B(z,w,op(w,x,y,z,v)) | -B(x,w,v) | -B(y,v,z).

% A9 : Five Segment Axiom
-L(x,y,x1,y1) | -L(y,z,y1,z1) | -L(x,v,x1,v1) | -L(y,v,y1,v1) |
	L(z,v,z1,v1) | -B(x,y,z) | -B(x1,y1,z1) |  EQ(x,y).

% A10 : Segment Construction Axiom
B(x,y,ext(x,y,w,v)).
L(y,ext(x,y,w,v),w,v).

% A11 : Lower Dimension Axiom
-B(C1,C2,C3).
-B(C2,C3,C1).
-B(C3,C1,C2).

% A12 : Upper Dimension Axiom
-L(x,w,x,v) | -L(y,w,y,v) | -L(z,w,z,v) | B(x,y,z) | B(y,z,x) |  
	B(z,x,y) | EQ(w,v).

% Definition of Collinearity
% -C(x,y,z) | B(x,y,z) | B(y,x,z) | B(x,z,y).
% -B(x,y,z) | C(x,y,z).
% -B(y,x,z) | C(x,y,z).
% -B(x,z,y) | C(x,y,z).

% T1 : 
-B(x,y,z) | B(z,y,x).

% T2 : 
B(x,x,y).

% T3 : 
B(x,y,y).

% T6 : 
-B(x,y,z) | -B(x,z,y) | EQ(x,y) | EQ(y,z) | EQ(x,z).
-B(x,y,z) | -B(y,x,z) | EQ(x,y) | EQ(y,z) | EQ(x,z).

% T7 : 
-B(w,y,z) | -B(x,y,z) | B(x,w,y) | B(w,x,y) | EQ(y,z).

% T8 : 
-B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z).

% T10 : 
% -C(x,y,z) | C(x,z,y).
% -C(x,y,z) | C(y,x,z).
% -C(x,y,z) | C(y,z,x).
% -C(x,y,z) | C(z,x,y).
% -C(x,y,z) | C(z,y,x).

% T11 : 
% -C(C1,C2,C3).

% denial of the theorem:
B(a,c,e).
B(a,d,e).
-B(a,c,d).
-B(a,d,c).

EQ(ext(x,y,z,z),y). 

% literal demodulators: 
(B(x,y,x) =  EQ(x,y)).
(L(x,y,z,z) =  EQ(x,y)).
(L(x,y,y,x) = $T).
% (B(x,y,ext(x,y,w,v)) = $T).
% (L(y,ext(x,y,w,v),w,v) = $T).
(B(C1,C2,C3) = $F).
(B(C2,C3,C1) = $F).
(B(C3,C1,C2) = $F).
(B(x,x,y) = $T).
(B(x,y,y) = $T).
% (C(C1,C2,C3) = $F).
% 	lex-dependant
(EQ(x,y) = EQ(y,x)).
(B(x,y,z) = B(z,y,x)).
% (C(x,y,z) = C(x,z,y)).
% (C(x,y,z) = C(y,x,z)).
% (C(x,y,z) = C(y,z,x)).
% (C(x,y,z) = C(z,x,y)).
% (C(x,y,z) = C(z,y,x)).
(L(x,y,z,w) = L(z,w,x,y)).
(L(x,y,z,w) = L(x,y,w,z)).
(L(x,y,z,w) = L(y,x,z,w)).