%
% TPTP format version 3
%
% With E, for example, test with
%
%   eprover --tptp3in -xAuto -tAuto e.tptp

% betweenness axioms

fof(bet1,axiom,
  (![A,B,C] : ((point(A) & point(B) & point(C)) =>
    (bet(A,B,C) =>
      (bet(C,B,A) & (A != B) & (A != C) & ~bet(B,A,C)))))).

fof(bet2,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) =>
    ((bet(A,B,C) & on(A,L) & on(C,L)) =>
      on(B,L))))).

fof(bet3,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) =>
    ((bet(A,B,C) & on(A,L) & on(B,L)) =>
      on(C,L))))).

fof(bet4,axiom,
  (![A,B,C,D] : ((point(A) & point(B) & point(C) & point(D)) =>
    ((bet(A,B,C) & bet(A,D,B)) =>
      bet(A,D,C))))).
%      (bet(A,D,C) & bet(D,B,C)))))). This variant is redundant.

fof(bet5,axiom,
  (![A,B,C,D] : ((point(A) & point(B) & point(C) & point(D)) =>
    ((bet(A,B,C) & bet(B,C,D)) =>
      bet(A,B,D))))).
%      (bet(A,C,D) & bet(A,B,D)))))). This variant is redundant.

fof(bet6,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) =>
    ((on(A,L) & on(B,L) & on(C,L) & A != B & A != C & B != C) =>
      (bet(A,B,C) | bet(B,A,C) | bet(A,C,B)))))).

% same-side axioms

fof(sameside1,axiom,
  (![A,L] : ((point(A) & line(L)) =>
    (~on(A,L) => sameside(A,A,L))))).

fof(sameside2,axiom,
  (![A,B,L] : ((point(A) & point(B) & line(L)) =>
    (sameside(A,B,L) =>
      (~on(A,L) & sameside(B,A,L)))))).

fof(sameside3,axiom,
 (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) =>
    ((sameside(A,B,L) & sameside(A,C,L)) =>
      sameside(B,C,L))))).

fof(sameside4,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) => 
    ((~on(A,L) & ~on(B,L) & ~on(C,L)) =>
      (sameside(A,B,L) | sameside(A,C,L) | sameside(B,C,L)))))).

% Pasch axioms

fof(pasch1,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) => 
    ((bet(A,B,C) & sameside(A,C,L)) =>
      sameside(A,B,L))))).

fof(pasch2,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) => 
    ((bet(A,B,C) & on(A,L) & ~on(B,L)) =>
      sameside(B,C,L))))).

fof(pasch3,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L)) => 
    ((bet(A,B,C) & on(B,L)) =>
      ~sameside(A,C,L))))).

fof(pasch4,axiom,
  (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & line(M)) =>
    ((A != B & B != C & L != M & on(A,M) & on(B,M) & on(C,M) &
      ~sameside(A,C,L) & on(B,L)) =>
        bet(A,B,C))))).

% test them out

fof(type1,hypothesis, point(p)).
fof(type2,hypothesis, point(q)).
fof(type3,hypothesis, point(r)).
fof(type4,hypothesis, point(s)).
fof(type5,hypothesis, point(t)).
fof(type6,hypothesis, point(u)).
fof(type7,hypothesis, point(v)).
fof(type8,hypothesis, line(k)).
fof(type9,hypothesis, line(l)).
fof(type10,hypothesis, line(m)).
fof(type11,hypothesis, line(n)).
fof(type12,hypothesis, line(o)).

fof(test1,hypothesis, on(p,l)).
fof(test2,hypothesis, on(q,l)).
fof(test3,hypothesis, on(p,n)).
fof(test4,hypothesis, on(s,n)).
fof(test5,hypothesis, on(t,n)).
fof(test6,hypothesis, on(p,m)).
fof(test7,hypothesis, on(r,m)).
fof(test8,hypothesis, on(q,o)).
fof(test9,hypothesis, on(s,o)).
fof(test10,hypothesis, on(r,o)).
fof(test11,hypothesis, ~on(r,l)).
fof(test12,hypothesis, bet(p,s,t)).
fof(test13,hypothesis, bet(q,s,r)).
fof(test14,hypothesis, bet(s,u,t)).
fof(test15,hypothesis, p!=q).
fof(test16,hypothesis, bet(p,q,v)).
fof(test17,hypothesis, on(q,k)).
fof(test18,hypothesis, on(t,k)).

% check consistency
%fof(con0,conjecture,$false).

%fof(con1,conjecture,~sameside(p,t,o)).
%fof(con2,conjecture,~sameside(s,t,o)).
%fof(con3,conjecture,sameside(s,t,m)).
%fof(con4,conjecture,sameside(u,t,m)).
%fof(con5,conjecture,~bet(s,p,t)).
fof(con6,conjecture,~bet(q,s,u)).
%fof(con7,conjecture,~on(q,n)).
%fof(con8,conjecture,sameside(r,s,l)).
%fof(con8b,conjecture,sameside(r,u,l)).
%fof(con9,conjecture,~sameside(s,v,k)).