% 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 Satz5.1.

set(hyper_res).
set(para_into).
set(para_from).
set(binary_res).
set(ur_res).
set(order_history).
assign(max_seconds,20).
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,8).
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).
% Following is Satz3.17
-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1) 
|  T(xp,crossbar(xa,xb,xc,xa1,xb1,xp),xc).
-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1) 
|  T(xb,crossbar(xa,xb,xc,xa1,xb1,xp),xb1).
% Following is Satz4.2
-IFS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1).
% Following is Satz4.3
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xc,xa1,xc1) | -E(xb,xc,xb1,xc1) 
|  E(xa,xb,xa1,xb1).
% Following is Satz4.5
-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) | T(xa1,insert(xa,xb,xa1,xc1),xc1).
-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) | E3(xa,xb,xc,xa1,insert(xa,xb,xa1,xc1),xc1).
% Following is Satz4.6
-T(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | T(xa1,xb1,xc1).
% Following is Satz4.11a
-Col(xa,xb,xc) | Col(xb,xc,xa).
% Following is Satz4.11b
-Col(xa,xb,xc) | Col(xc,xa,xb).
% Following is Satz4.11c
-Col(xa,xb,xc) | Col(xc,xb,xa).
% Following is Satz4.11d
-Col(xa,xb,xc) | Col(xb,xa,xc).
% Following is Satz4.11e
-Col(xa,xb,xc) | Col(xa,xc,xb).
% Following is Satz4.12
Col(xa,xa,xb).
% Following is Satz4.12b
Col(xa,xb,xa).
% Following is Satz4.13
-Col(xa,xb,xc) | - E3(xa,xb,xc,xa1,xb1,xc1) | Col(xa1,xb1,xc1).
% Following is Satz4.14
-Col(xa,xb,xc) | -E(xa,xb,xa1,xb1) 
|  E3(xa,xb,xc,xa1,xb1,insert5(xa,xb,xc,xa1,xb1)).
% Following is Satz4.16
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | xa = xb | E(xc,xd,xc1,xd1).
% Following is Satz4.17
xa = xb | -Col(xa,xb,xc) | -E(xa,xp,xa,xq) | -E(xb,xp,xb,xq) |E(xc,xp,xc,xq).
% Following is Satz4.18
xa = xb | -Col(xa,xb,xc) | -E(xa,xc,xa,xc1) | -E(xb,xc,xb,xc1) | xc = xc1.
% Following is Satz4.19
-T(xa,xc,xb) | -E(xa,xc,xa,xc1) | -E(xb,xc,xb,xc1) | xc = xc1.
% Following defines the function insert
insert(xa,xb,xa1,xc1) = ext(ext(xc1,xa1,alpha,gamma),xa1,xa,xb).
% Following is Defn2.10
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xb,za,zb).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xd,zb,zd).
-T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xb,za,zb) | -E(xb,xc,zb,zc) 
|  -E(xa,xd,za,zd) | -E(xb,xd,zb,zd)| AFS(xa,xb,xc,xd,za,zb,zc,zd).
% Following is Defn4.1
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xc,za,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xc,xd,zc,zd).
 -T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xc,za,zc) | -E(xb,xc,zb,zc) 
|  -E(xa,xd,za,zd) | -E(xc,xd,zc,zd)| IFS(xa,xb,xc,xd,za,zb,zc,zd).
% Following is Defn4.4
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa2,xb1,xb2).
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa3,xb1,xb3).
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa2,xa3,xb2,xb3).
-E(xa1,xa2,xb1,xb2) | -E(xa1,xa3,xb1,xb3) | -E(xa2,xa3,xb2,xb3) 
|  E3(xa1,xa2,xa3,xb1,xb2,xb3).
% Following is Defn4.10
-Col(xa,xb,xc) | T(xa,xb,xc) | T(xb,xc,xa) | T(xc,xa,xb).
Col(xa,xb,xc) | -T(xa,xb,xc).
Col(xa,xb,xc) | -T(xb,xc,xa).
Col(xa,xb,xc) | -T(xc,xa,xb).
% Following is Defn4.15
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | Col(xa,xb,xc).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E3(xa,xb,xc,xa1,xb1,xc1).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xa,xd,xa1,xd1).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1).
-Col(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | -E(xa,xd,xa1,xd1) 
|  -E(xb,xd,xb1,xd1) | FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1).
% Following is Defn5.4
-le(xa,xb,xc,xd) | T(xc,insert(xa,xb,xc,xd),xd).
-le(xa,xb,xc,xd) | E(xa,xb,xc,insert(xa,xb,xc,xd)).
-T(xc,y,xd) | -E(xa,xb,xc,y) | le(xa,xb,xc,xd).
end_of_list.

list(sos).
% Following is the negated form of Satz5.1
a != b.
T(a,b,c).
T(a,b,d).
-T(a,c,d).
-T(a,d,c).
% Following is the diagram:
c1=ext(a,d,c,d).
d1=ext(a,c,c,d).
p=ext(c1,c,c,d).
r=ext(d1,c,c,e).
q=ext(p,r,r,p).
b1 = ext(a,c1,c,b).
b2 = ext(a,d1,d,b).
e = ip(c1,d,b,d1,c).
% Following are tautologies:
d1=e | d1!=e.
c = c1 | c != c1.
end_of_list.

list(demodulators).
ext(a,d,c,d) = c1.
ext(a,c,c,d) = d1.
ext(c1,c,c,d) = p.
ext(d1,c,c,e) = r.
ext(p,r,r,p) = q.
ext(a,c1,c,b) = b1.
ext(a,d1,d,b) = b2.
ip(c1,d,b,d1,c) = e.
end_of_list.

list(hints2).
T(b,c,ext(a,c,x,y)).
T(d,b,a).
T(b,d,ext(a,d,x,y)).
E(d,c1,c,d).
T(a,d,c1).
E(c,d1,c,d).
T(a,c,d1).
E(c,p,c,d).
T(c1,c,p).
E(c,r,c,e).
T(d1,c,r).
E(r,q,r,p).
T(p,r,q).
E(c1,b1,c,b).
T(a,c1,b1).
E(d1,b2,d,b).
T(a,d1,b2).
-T(c1,d,b)| -T(d1,c,b)|T(c,e,c1).
T(b,c,d1).
T(ext(a,d,x,y),d,b).
T(b,d,c1).
-E(d,x,c,y)| -E(x,c1,y,d)|E3(d,x,c1,c,y,d).
E(d,c1,d,c).
E(c,d,c1,d).
T(c1,d,a).
T(a,b,c1).
c!=c1.
E(d1,c,c,d).
E(c,d,c,d1).
E(c,d,d1,c).
Col(c,d1,a).
T(a,b,d1).
-T(c,d,d1).
-E(c,d,x,y)|E(c,p,x,y).
E(c,d,p,c).
Col(c1,c,p).
E(r,c,e,c).
E(c,e,c,r).
Col(c,r,d1).
T(r,c,d1).
E(r,p,r,q).
E(b1,c1,b,c).
T(b1,c1,a).
E(b2,d1,b,d).
T(a,c,b2).
T(c,d1,b2).
-T(d1,c,b)|T(c,e,c1).
Col(c,d1,b).
T(d1,c,b).
T(c1,d,b).
E(d,c,d,c1).
E(c,d1,c1,d).
T(c1,b,a).
Col(a,b,c1).
T(a,b,b1).
E3(c,d1,d,c,d,d1).
E(c,p,c,d1).
E(d,c1,c,d1).
E(c1,d,c,d1).
T(a,b,b2).
E(d1,c,p,c).
Col(c,c1,p).
E(e,c,r,c).
E(b,c,b1,c1).
T(b1,c1,d).
E(b,d,b2,d1).
T(b,c,b2).
T(c,e,c1).
T(c1,e,c).
T(d,e,d1).
E(c,b2,c1,b).
T(b1,c1,b).
-T(c,d1,d).
E(b1,d,b,d1).
Col(c,c1,e).
T(e,c,p).
T(d1,e,d).
E(b,b2,b1,b).
-E3(x,y,y,c,d1,d).
T(p,c,e).
E(b,b2,b,b1).
-E(c1,c1,d1,d).
d1=c|E(r,p,e,d1).
E(b2,x,b1,x).
-E(x,x,d1,d).
E(r,p,e,d1).
E(x,b2,x,b1).
E(b2,d,b,d1).
E(p,r,d1,e).
E(r,q,e,d1).
E(e,d1,r,q).
b1=b2.
E(d1,e,p,r).
T(b2,c1,b).
IFS(b,c,b2,d,b2,c1,b,d1).
E(c,d,c1,d1).
E(c1,d1,d1,c).
E(c1,d1,c1,d).
E(d1,c,d1,c1).
E(e,d1,e,d).
-Col(c,c1,d1).
IFS(d,e,d1,c,d,e,d1,c1).
-E(r,c,r,c1).
E(r,q,e,d).
E(e,d,r,q).
-Col(c,d1,c1).
d1!=e.
E(e,c,e,c1).
-E(c,r,c1,r).
E(p,q,d1,d).
E(d,c,q,c).
-T(c,d1,c1).
E(r,c,e,c1).
-E(c1,r,c,r).
-E(x,x,p,q).
E(c,d,c,q).
-E(c1,r,c,e).
E(c,p,c,q).
-T(c1,r,c).
c=r|E(d1,p,d1,q).
-E(c1,p,c1,q).
E(d1,p,d1,q).
c=d1|E(b,p,b,q).
c=d1|E(a,p,a,q).
E(b,p,b,q).
E(a,p,a,q).
-E(a,p,a,q).
end_of_list.