% This file was mechanically generated
% from the master list in TarskiTheorems.php.
% Tarski-Szmielew's axiom system is used.
% T is Tarski's B,  non-strict betweenness.
% E is equidistance.
% Names for the axioms follow the book SST
% by Schwabhäuser, Szmielew, and Tarski.
% This file attempts to prove Satz3.17.

set(hyper_res).
set(para_into).
set(para_from).
set(binary_res).
set(ur_res).
set(order_history).
assign(max_seconds,120).
assign(max_mem,2000000).
clear(print_kept).
set(input_sos_first).
set(back_sub).
assign(bsub_hint_wt,-1).
set(keep_hint_subsumers).
assign(max_weight,20).
assign(max_distinct_vars,3).
assign(pick_given_ratio,4).
assign(max_proofs,1).

list(usable).
% Following is axiom A1
E(x,y,y,x).
% Following is axiom A2
-E(x,y,z,v) | -E(x,y,z2,v2) | E(z,v,z2,v2).
% Following is axiom A3
-E(x,y,z,z) | x=y.
% Following is axiom A4
T(x,y,ext(x,y,w,v)).
E(y,ext(x,y,w,v),w,v).
% Following is axiom A5
-E(x,y,x1,y1) | -E(y,z,y1,z1) | -E(x,v,x1,v1) | -E(y,v,y1,v1) | -T(x,y,z) 
|  -T(x1,y1,z1) | x=y | E(z,v,z1,v1).
% Following is axiom A6
 -T(x,y,x) | x=y.
% Following is axiom A7
-T(xa,xp,xc) | -T(xb,xq,xc) | T(xp,ip(xa,xp,xc,xb,xq),xb).
-T(xa,xp,xc) | -T(xb,xq,xc) | T(xq,ip(xa,xp,xc,xb,xq),xa).
% Following is axiom A8
-T(alpha,beta,gamma).
-T(beta,gamma,alpha).
-T(gamma,alpha,beta).

% Following is Satz2.1
E(xa,xb,xa,xb).
% Following is Satz2.2
-E(xa,xb,xc,xd) | E(xc,xd,xa,xb).
% Following is Satz2.3
-E(xa,xb,xc,xd) | -E(xc,xd,xe,xf) | E(xa,xb,xe,xf).
% Following is Satz2.4
-E(xa,xb,xc,xd) | E(xb,xa,xc,xd).
% Following is Satz2.5
-E(xa,xb,xc,xd) | E(xa,xb,xd,xc).
% Following is Satz2.8
E(xa,xa,xb,xb).
% Following is Satz2.11
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1) 
|  E(xa,xc,xa1,xc1).
% Following is Satz2.12
xq = xa | -T(xq,xa,xd) | -E(xa,xd,xb,xc) | xd = ext(xq,xa,xb,xc).
% Following is Satz2.13
-E(xb,xc,xa,xa) | xb=xc.
% Following is Satz2.14
-E(xa,xb,xc,xd) | E(xb,xa,xd,xc).
% Following is Satz2.15
-T(xa,xb,xc) | -T(xA,xB,xC) | -E(xa,xb,xB,xC)| -E(xb,xc,xA,xB) 
|  E(xa,xc,xA,xC).
% Following is Satz3.1
T(xa,xb,xb).
% Following is Satz3.2
-T(xa,xb,xc) | T(xc,xb,xa).
% Following is Satz3.3
T(xa1,xa1,xb1).
% Following is Satz3.4
-T(xa,xb,xc) | -T(xb,xa,xc) | xa = xb.
% Following is Satz3.5a
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xb,xc).
% Following is Satz3.6a
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xb,xc,xd).
% Following is Satz3.7a
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xc,xd).
% Following is Satz3.5b
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xc,xd).
% Following is Satz3.6b
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd).
% Following is Satz3.7b
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xb,xd).
% Following is Satz3.13a
alpha != beta.
% Following is Satz3.13b
beta != gamma.
% Following is Satz3.13a
alpha != gamma.
% Following is Satz3.14a
T(xa,xb,ext(xa,xb,alpha,gamma)).
% Following is Satz3.14b
xb != ext(xa,xb,alpha,gamma).
end_of_list.

list(sos).
% Following is the negated form of Satz3.17
T(a,b,c).
T(a1,b1,c).
T(a,p,a1).
-T(p,x,c) | -T(b,x,b1).
% Following is the diagram:
e = ip(c,b1,a1,a,p).
d = ip(c,b,a,b1,e).
end_of_list.

list(demodulators).
ip(c,b1,a1,a,p) = e.
ip(c,b,a,b1,e) = d.
end_of_list.