% 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 Satz7.25. 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,4). 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 is Satz5.1 xa = xb | -T(xa,xb,xc) | -T(xa,xb,xd) | T(xa,xc,xd) | T(xa,xd,xc). % Following is Satz5.2 xa = xb | -T(xa,xb,xc) | -T(xa,xb,xd)| T(xb,xc,xd) | T(xb,xd,xc). % Following is Satz5.3 -T(xa,xb,xd) | -T(xa,xc,xd) | T(xa,xb,xc) | T(xa,xc,xb). % Following is Satz5.5a -le(xa,xb,xc,xd) | T(xa,xb,ins(xc,xd,xa,xb)). -le(xa,xb,xc,xd) | E(xa,ins(xc,xd,xa,xb),xc,xd). -le(xa,xb,xc,xd) | ins(xc,xd,xa,xb) = ext(xa,xb,insert(xa,xb,xc,xd),xd). % Following is Satz5.5b le(xa,xb,xc,xd) | -T(xa,xb,xe) | -E(xa,xe,xc,xd). % Following is Satz5.6 -le(xa,xb,xc,xd) | -E(xa,xb,xa1,xb1) | - E(xc,xd,xc1,xd1) | le(xa1,xb1,xc1,xd1). % Following is Satz5.7 le(xa,xb,xa,xb). % Following is Satz5.8 -le(xa,xb,xc,xd) | - le(xc,xd,xe,xf) | le(xa,xb,xe,xf). % Following is Satz5.9 -le(xa,xb,xc,xd) | -le(xc,xd,xa,xb) | E(xa,xb,xc,xd). % Following is Satz5.10 le(xa,xb,xc,xd) | le(xc,xd,xa,xb). % Following is Satz5.11 le(xa,xa,xc,xd). % Following is Satz5.12a1 -Col(xa,xb,xc) | -T(xa,xb,xc) | le(xa,xb,xa,xc). % Following is Satz5.12a2 -Col(xa,xb,xc) | -T(xa,xb,xc) | le(xb,xc,xa,xc). % Following is NarbouxLemma1 -T(xa,xb,xc) | -E(xa,xc,xa,xb) | xc = xb. % Following is Satz5.12b -Col(xa,xb,xc) | T(xa,xb,xc) | -le(xa,xb,xa,xc) | -le(xb,xc,xa,xc). % Following is Satz6.2a xa = xp | xb = xp | xc = xp | -T(xa,xp,xc) | -T(xb,xp,xc) | sameside(xa,xp,xb). % Following is Satz6.2b xa = xp | xb = xp | xc = xp | -T(xa,xp,xc) | T(xb,xp,xc) | -sameside(xa,xp,xb). % Following is Satz6.3a -sameside(xa,xp,xb) | xa != xp. -sameside(xa,xp,xb) | xb != xp. -sameside(xa,xp,xb) | c63(xa,xp,xb) != xp. -sameside(xa,xp,xb) | T(xa,xp,c63(xa,xp,xb)). -sameside(xa,xp,xb) | T(xb,xp,c63(xa,xp,xb)). % Following is Satz6.3b sameside(xa,xp,xb) | xa=xp | xb = xp | xc = xp | -T(xa,xp,xc) | -T(xb,xp,xc). % Following is Satz6.4a -sameside(xa,xp,xb) | Col(xa,xp,xb). -sameside(xa,xp,xb) | -T(xa,xp,xb). % Following is Satz6.4b sameside(xa,xp,xb) | -Col(xa,xp,xb) | T(xa,xp,xb). % Following is Satz6.5 xa = xp | sameside(xa,xp,xa). % Following is Satz6.6 -sameside(xa,xp,xb) | sameside(xb,xp,xa). % Following is Satz6.7 -sameside(xa,xp,xb) | -sameside(xb,xp,xc) | sameside(xa,xp,xc). % Following is Satz6.11a xr = xa | xb = xc | sameside(insert(xb,xc,xa,xr),xa,xr). xr = xa | xb = xc | E(xa,insert(xb,xc,xa,xr),xb,xc). % Following is Satz6.11b xr = xa | xb = xc | -sameside(xp,xa,xr) | -E(xa,xp,xb,xc) | -sameside(xq,xa,xr) | -E(xa,xq,xb,xc) | xp=xq. % Following is Satz6.13a -sameside(xa,xp,xb) | -le(xp,xa,xp,xb) | T(xp,xa,xb). % Following is Satz6.13b -sameside(xa,xp,xb) | le(xp,xa,xp,xb) | -T(xp,xa,xb). % Following is Satz6.15a xp = xq | xp = xr | -T(xq,xp,xr) | -Col(xa,xp,xq) | xa = xp | sameside(xa,xp,xq) | sameside(xa,xp,xr). % Following is Satz6.15b xp = xq | xp = xr | -T(xq,xp,xr) | -sameside(xa,xp,xq) | Col(xa,xp,xq). % Following is Satz6.15c xp = xq | xp = xr | -T(xq,xp,xr) | -sameside(xa,xp,xr) | Col(xa,xp,xq). % Following is Satz6.15d xp = xq | xp = xr | -T(xq,xp,xr) | xa != xp | Col(xa,xp,xq). % Following is Satz6.16a xa=xb | -T(xc,xa,xb) | -T(xd,xa,xb) | T(xd,xc,xb) | T(xc,xd,xb). % Following is Satz6.16b xp = xq | xcs = xp | -Col(xp,xq,xcs) | -Col(xp,xq,xr) | Col(xp,xcs,xr). % Following is Satz6.17a xp = xq | Col(xp,xq,xp). % Following is Satz6.17b xp = xq | -Col(xp,xq,xr) | Col(xq,xp,xr). % Following is Satz6.18 xa = xb | xp = xq | -Col(xp,xq,xa) | -Col(xp,xq,xb) | -Col(xp,xq,xr) | Col(xa,xb,xr). % Following is Satz6.21 xa = xb | xp = xq | -Col(xa,xb,xc) | -Col(xp,xq,xc) | -Col(xa,xb,xd) | -Col(xp,xq,xd) | xc=xd | -Col(xa,xb,xe) | Col(xp,xq,xe). % Following is Satz6.25 xa = xb | -Col(xa,xb,pointOffLine(xa,xb)). % Following is Satz6.28 -sameside(xa,xb,xc)| -sameside(xa1,xb1,xc1) | -E(xb,xa,xb1,xa1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1). % Following is Satz7.2 -M(xa,xm,xb) | M(xb,xm,xa). % Following is Satz7.3a -M(xa,xm,xa) | xm = xa. % Following is Satz7.3b M(xa,xm,xa) | xm != xa. % Following is Satz7.4a M(xp,xa,s(xa,xp)). % Following is Satz7.4b -M(xp,xa,xr) | -M(xp,xa,xq) | xr=xq. % Following is Satz7.6 -M(xp,xa,xq) | xq = s(xa,xp). % Following is Satz7.7 s(xa,s(xa,xp)) = xp. % Following is Satz7.8 s(xa,xp) != xr | s(xa,xq) != xr | xp = xq. % Following is Satz7.9 s(xa,xp) != s(xa,xq) | xp = xq. % Following is Satz7.10a s(xa,xp) != xp | xp = xa. % Following is Satz7.10b s(xa,xp)=xp | xp != xa. % Following is Satz7.13 E(xp,xq,s(xa,xp),s(xa,xq)). % Following is Satz7.15a -T(xp,xq,xr) | T(s(xa,xp),s(xa,xq),s(xa,xr)). % Following is Satz7.15b T(xp,xq,xr) | -T(s(xa,xp),s(xa,xq),s(xa,xr)). % Following is Satz7.16a -E(xp,xq,xr,xcs) | E(s(xa,xp),s(xa,xq),s(xa,xr),s(xa,xcs)). % Following is Satz7.16b E(xp,xq,xr,xcs) | -E(s(xa,xp),s(xa,xq),s(xa,xr),s(xa,xcs)). % Following is Satz7.17 -M(xp,xa,xq) | -M(xp,xb,xq) | xa = xb. % Following is Satz7.18 s(xa,xp) != s(xb,xp) | xa = xb. % Following is Satz7.19 s(xa,s(xb,xp)) != s(xb,s(xa,xp)) | xa = xb. % Following is Satz7.20 -Col(xa,xm,xb) | -E(xm,xa,xm,xb) | xa = xb | M(xa,xm,xb). % Following is Satz7.21 Col(xa,xb,xc) | xb = xd | -E(xa,xb,xc,xd) | -E(xb,xc,xd,xa) | -Col(xa,xp,xc) | -Col(xb,xp,xd) | M(xa,xp,xc). % Following is Satz7.22a -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xm1,xc,xm2) | -le(xc,xa1,xc,xa2) . % Following is Satz7.22b -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xm1,xc,xm2). % Following is Satz7.22 -T(xa1,xc,xa2) | -T(xb1,xc,xb2) | -E(xc,xa1,xc,xb1) | -E(xc,xa2,xc,xb2) | -M(xa1,xm1,xb1) | -M(xa2,xm2,xb2) | T(xm1,xc,xm2). % 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). % Following is Defn6.1 -sameside(xa,xp,xb) | xa != xp. -sameside(xa,xp,xb) | xb != xp. -sameside(xa,xp,xb) | T(xp,xa,xb) | T(xp,xb,xa). -T(xp,xa,xb) | xa=xp |xb=xp | sameside(xa,xp,xb). -T(xp,xb,xa) | xa=xp | xb=xp | sameside(xa,xp,xb). % Following is Defn7.1 -M(xa,xm,xb) | T(xa,xm,xb). -M(xa,xm,xb) | E(xm,xa,xm,xb). -T(xa,xm,xb) | -E(xm,xa,xm,xb) | M(xa,xm,xb). % Following is Defn7.23 -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xa1,xc,xa2). -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xb1,xc,xb2). -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | E(xc,xa1,xc,xb1). -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | E(xc,xa2,xc,xb2). -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | M(xa1,xm1,xb1). -KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | M(xa2,xm2,xb2). -T(xa1,xc,xa2) | -T(xb1,xc,xb2) | -E(xc,xa1,xc,xb1) | -E(xc,xa2,xc,xb2) | -M(xa1,xm1,xb1) | -M(xa2,xm2,xb2) | KF(xa1,xm1,xb1,xc,xb2,xm2,xa2). end_of_list. list(demodulators). % Following is Satz 7.7, the only theorem in SST that is an equality. s(xa,s(xa,xp)) = xp. end_of_list. list(sos). % Following is the negated form of Satz7.25 E(c,a,c,b). -M(a,x,b). % Following is the diagram: p = ext(c,a,a,c). q = ext(c,b,a,p). r = ip(p,a,c,q,b). cx = ip(b,r,p,c,a). r1 = insert(b,r,a,q). % Following are tautologies: Col(a,b,c) | -Col(a,b,c). end_of_list. list(demodulators). ext(c,a,a,c) = p. ext(c,b,a,p) = q. ip(p,a,c,q,b) = r. ip(b,r,p,c,a) = cx. insert(b,r,a,q) = r1. end_of_list. list(hints2). -Col(a,c,b)|a=b. -T(a,c,b). -T(x,a,c)| -E(x,a,x,b)|a=b. E(c,a,b,c). E(c,b,c,a). -M(b,x,a). -E(a,a,a,b). E(a,p,a,c). T(c,a,p). E(b,q,a,p). T(c,b,q). -T(p,a,c)| -T(q,b,c)|T(b,r,p). -T(p,a,c)| -T(q,b,c)|T(a,r,q). cx=ip(b,r,ext(c,a,a,c),c,a). r1=ext(ext(q,a,alpha,gamma),a,b,r). -T(b,r,x)| -E(b,x,a,q)|T(a,r1,q). -T(b,c,a). E(a,c,b,c). E(b,c,a,c). -T(b,x,a)| -E(x,b,x,a). -E(x,x,a,b). T(p,a,c). T(a,p,ext(c,p,x,y)). E(a,p,b,q). T(q,b,c). -T(a,c,q). T(b,r,p). Col(p,b,r). T(p,r,b). Col(a,r,q). -T(b,r,ext(c,a,a,c))|T(a,cx,b). -T(b,r,ext(c,a,a,c))|T(r,cx,c). E(a,r1,b,r). -T(b,c,p). -T(a,b,c). -T(x,a,c)| -E(x,a,x,b). -Col(a,c,b). M(p,a,c). -T(p,c,b). AFS(c,a,p,b,c,b,q,a). T(b,r,ext(c,a,a,c)). T(ext(c,a,a,c),r,b). Col(a,q,r). Col(a,cx,b). T(b,cx,a). T(r,cx,c). E(b,r,r1,a). -T(q,c,p). -T(a,q,c). -E(p,a,p,b). -Col(c,a,b). -Col(b,c,a). -Col(b,a,c). -T(b,a,c). c=s(a,p). Col(b,cx,a). -E(cx,b,cx,a). E(r,b,r1,a). -sameside(q,a,c). -T(p,b,c). -T(b,p,c). c=p|p!=a. -IFS(x,cx,y,b,z,cx,u,a). -T(c,b,p). -T(p,q,c). -Col(c,b,p). p!=a. -E(r,b,r,a). -T(a,b,p). -Col(p,b,c). -T(p,a,b). -T(b,p,a). -Col(b,p,a). -Col(a,b,p). -Col(a,p,b). b!=p. a!=b. c!=b. c!=a. a!=c. b!=c. E(p,b,q,a). E(p,a,q,b). b!=a. p!=b. E(p,b,a,q). Col(a,b,b). -E(q,b,q,a). a!=p. E(b,p,a,q). E(a,q,b,p). -T(q,a,c). T(a,r1,q). -Col(q,a,c). -T(c,a,q). Col(r1,q,a). T(q,r1,a). -Col(q,c,a). -Col(a,q,c). q!=a. -T(c,p,q). Col(a,q,r1). E(p,r,q,r1). q!=c. Col(q,a,q). -Col(p,q,c). E(p,r,r1,q). a!=q. Col(a,q,q). p!=q. E(r,p,r1,q). -Col(p,b,q). IFS(b,r,p,q,a,r1,q,p). IFS(b,r,p,a,a,r1,q,b). E(r,q,r1,p). E(r,a,r1,b). E(r,a,b,r1). E(a,r,b,r1). E3(a,r,q,b,r1,p). Col(b,r1,p). Col(p,b,r1). r=r1. -E(r,b,r1,a). end_of_list.