%--------------------------------------------------------------------------
% File     : GEO010-2 : TPTP v2.0.0. Released v1.0.0.
% Domain   : Geometry
% Problem  : Collinearity is invariant
% Version  : [Quaife, 1989] axioms.
% English  : For all points x, y, and z, if x, y, and z are collinear 
%            in one order, they are collinear in any order.

% Refs     : McCharen J.D., Overbeek R.A., Wos L.A. (1976), Problems and 
%            Experiments for and with Automated Theorem Proving Programs, 
%            IEEE Transactions on Computers C-25(8), 773-782.
%          : Schwabbauser W., Szmielew W., and Tarski A. (1983), 
%            Metamathematische Methoden in der Geometrie, Springer-Verlag, 
%            Berlin, Germany.
%          : Quaife A. (1989), Automated Development of Tarski's Geometry, 
%            Journal of Automated Reasoning 5(1), 97-118.
% Source   : [TPTP]
% Names    : 

% Status   : unsatisfiable
% Rating   : 0.89 v2.0.0
% Syntax   : Number of clauses    :   25 (   6 non-Horn;   8 unit;  21 RR)
%            Number of literals   :   73 (   8 equality)
%            Maximal clause size  :    8 (   2 average)
%            Number of predicates :    4 (   0 propositional; 2-4 arity)
%            Number of functors   :   11 (   6 constant; 0-6 arity)
%            Number of variables  :   84 (   3 singleton)
%            Maximal term depth   :    2 (   1 average)

% Comments : 
%          : tptp2X: -fotter:hypothesis:[set(auto),set(tptp_eq)] -trm_equality:stfp GEO010-2.p 
%--------------------------------------------------------------------------
set(prolog_style_variables).
set(auto2).
set(tptp_eq).

set(split_when_given).
set(split_pos).
assign(split_depth, 10).

list(usable).

% reflexivity, axiom.
 equal(A,A).

% reflexivity_for_equidistance, axiom.
 equidistant(A,B,B,A).

% transitivity_for_equidistance, axiom.
-equidistant(A,B,C,D) |
-equidistant(A,B,E,F) |
 equidistant(C,D,E,F).

% identity_for_equidistance, axiom.
-equidistant(A,B,C,C) |
 equal(A,B).

% segment_construction1, axiom.
 between(A,B,extension(A,B,C,D)).

% segment_construction2, axiom.
 equidistant(A,extension(B,A,C,D),C,D).

% outer_five_segment, axiom.
-equidistant(A,B,C,D) |
-equidistant(B,E,D,F) |
-equidistant(A,G,C,H) |
-equidistant(B,G,D,H) |
-between(A,B,E) |
-between(C,D,F) |
 equal(A,B) |
 equidistant(E,G,F,H).

% identity_for_betweeness, axiom.
-between(A,B,A) |
 equal(A,B).

% inner_pasch1, axiom.
-between(A,B,C) |
-between(D,E,C) |
 between(B,inner_pasch(A,B,C,E,D),D).

% inner_pasch2, axiom.
-between(A,B,C) |
-between(D,E,C) |
 between(E,inner_pasch(A,B,C,E,D),A).

% lower_dimension1, axiom.
-between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3).

% lower_dimension2, axiom.
-between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1).

% lower_dimension3, axiom.
-between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2).

% upper_dimension, axiom.
-equidistant(A,B,A,C) |
-equidistant(D,B,D,C) |
-equidistant(E,B,E,C) |
 between(A,D,E) |
 between(D,E,A) |
 between(E,A,D) |
 equal(B,C).

% euclid1, axiom.
-between(A,B,C) |
-between(D,B,E) |
 equal(A,B) |
 between(A,D,euclid1(A,D,B,E,C)).

% euclid2, axiom.
-between(A,B,C) |
-between(D,B,E) |
 equal(A,B) |
 between(A,E,euclid2(A,D,B,E,C)).

% euclid3, axiom.
-between(A,B,C) |
-between(D,B,E) |
 equal(A,B) |
 between(euclid1(A,D,B,E,C),C,euclid2(A,D,B,E,C)).

% continuity1, axiom.
-equidistant(A,B,A,C) |
-equidistant(A,D,A,E) |
-between(A,B,D) |
-between(B,F,D) |
 between(C,continuous(A,B,C,F,D,E),E).

% continuity2, axiom.
-equidistant(A,B,A,C) |
-equidistant(A,D,A,E) |
-between(A,B,D) |
-between(B,F,D) |
 equidistant(A,F,A,continuous(A,B,C,F,D,E)).

% colinearity1, axiom.
-between(A,B,C) |
 colinear(A,B,C).

% colinearity2, axiom.
-between(A,B,C) |
 colinear(C,A,B).

% colinearity3, axiom.
-between(A,B,C) |
 colinear(B,C,A).

% colinearity4, axiom.
-colinear(A,B,C) |
 between(A,B,C) |
 between(B,C,A) |
 between(C,A,B).

end_of_list.

list(sos).

% abc_colinear, hypothesis.
 colinear(a,b,c).

% prove_colinear_in_all_orders, conjecture.
-colinear(a,c,b) |
-colinear(b,a,c) |
-colinear(b,c,a) |
-colinear(c,a,b) |
-colinear(c,b,a).

end_of_list.

%--------------------------------------------------------------------------