%--------------------------------------------------------------------------
% File     : GEO004-0 : TPTP v7.2.0. Released v2.4.0.
% Domain   : Geometry (Oriented curves)
% Axioms   : Simple curve axioms
% Version  : [EHK99] axioms.
% English  :

% Refs     : [KE99]  Kulik & Eschenbach (1999), A Geometry of Oriented Curv
%          : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% Source   : [EHK99]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :   48 (  21 non-Horn;   1 unit;  43 RR)
%            Number of atoms      :  154 (  21 equality)
%            Maximal clause size  :   12 (   3 average)
%            Number of predicates :    8 (   0 propositional; 1-3 arity)
%            Number of functors   :   14 (   0 constant; 1-3 arity)
%            Number of variables  :  126 (  10 singleton)
%            Maximal term depth   :    3 (   1 average)
% SPC      : 

% Comments : Created by tptp2X -f tptp -t clausify:otter GEO004+0.ax
%--------------------------------------------------------------------------
cnf(part_of_defn_1,axiom,
    ( ~ part_of(A,B)
    | ~ incident_c(C,A)
    | incident_c(C,B) )).

cnf(part_of_defn_2,axiom,
    ( incident_c(ax0_sk1(A,B),A)
    | part_of(A,B) )).

cnf(part_of_defn_3,axiom,
    ( ~ incident_c(ax0_sk1(A,B),B)
    | part_of(A,B) )).

cnf(sum_defn_4,axiom,
    ( A != sum(B,C)
    | ~ incident_c(D,A)
    | incident_c(D,B)
    | incident_c(D,C) )).

cnf(sum_defn_5,axiom,
    ( A != sum(B,C)
    | ~ incident_c(D,B)
    | incident_c(D,A) )).

cnf(sum_defn_6,axiom,
    ( A != sum(B,C)
    | ~ incident_c(D,C)
    | incident_c(D,A) )).

cnf(sum_defn_7,axiom,
    ( incident_c(ax0_sk2(A,B,C),C)
    | incident_c(ax0_sk2(A,B,C),B)
    | incident_c(ax0_sk2(A,B,C),A)
    | C = sum(B,A) )).

cnf(sum_defn_8,axiom,
    ( incident_c(ax0_sk2(A,B,C),C)
    | ~ incident_c(ax0_sk2(A,B,C),C)
    | C = sum(B,A) )).

cnf(sum_defn_9,axiom,
    ( ~ incident_c(ax0_sk2(A,B,C),B)
    | incident_c(ax0_sk2(A,B,C),B)
    | incident_c(ax0_sk2(A,B,C),A)
    | C = sum(B,A) )).

cnf(sum_defn_10,axiom,
    ( ~ incident_c(ax0_sk2(A,B,C),A)
    | incident_c(ax0_sk2(A,B,C),B)
    | incident_c(ax0_sk2(A,B,C),A)
    | C = sum(B,A) )).

cnf(sum_defn_11,axiom,
    ( ~ incident_c(ax0_sk2(A,B,C),B)
    | ~ incident_c(ax0_sk2(A,B,C),C)
    | C = sum(B,A) )).

cnf(sum_defn_12,axiom,
    ( ~ incident_c(ax0_sk2(A,B,C),A)
    | ~ incident_c(ax0_sk2(A,B,C),C)
    | C = sum(B,A) )).

cnf(end_point_defn_13,axiom,
    ( ~ end_point(A,B)
    | incident_c(A,B) )).

cnf(end_point_defn_14,axiom,
    ( ~ end_point(A,B)
    | ~ part_of(C,B)
    | ~ part_of(D,B)
    | ~ incident_c(A,C)
    | ~ incident_c(A,D)
    | part_of(C,D)
    | part_of(D,C) )).

cnf(end_point_defn_15,axiom,
    ( ~ incident_c(A,B)
    | part_of(ax0_sk3(B,A),B)
    | end_point(A,B) )).

cnf(end_point_defn_16,axiom,
    ( ~ incident_c(A,B)
    | part_of(ax0_sk4(B,A),B)
    | end_point(A,B) )).

cnf(end_point_defn_17,axiom,
    ( ~ incident_c(A,B)
    | incident_c(A,ax0_sk3(B,A))
    | end_point(A,B) )).

cnf(end_point_defn_18,axiom,
    ( ~ incident_c(A,B)
    | incident_c(A,ax0_sk4(B,A))
    | end_point(A,B) )).

cnf(end_point_defn_19,axiom,
    ( ~ incident_c(A,B)
    | ~ part_of(ax0_sk3(B,A),ax0_sk4(B,A))
    | end_point(A,B) )).

cnf(end_point_defn_20,axiom,
    ( ~ incident_c(A,B)
    | ~ part_of(ax0_sk4(B,A),ax0_sk3(B,A))
    | end_point(A,B) )).

cnf(inner_point_defn_21,axiom,
    ( ~ inner_point(A,B)
    | incident_c(A,B) )).

cnf(inner_point_defn_22,axiom,
    ( ~ inner_point(A,B)
    | ~ end_point(A,B) )).

cnf(inner_point_defn_23,axiom,
    ( ~ incident_c(A,B)
    | end_point(A,B)
    | inner_point(A,B) )).

cnf(meet_defn_24,axiom,
    ( ~ meet(A,B,C)
    | incident_c(A,B) )).

cnf(meet_defn_25,axiom,
    ( ~ meet(A,B,C)
    | incident_c(A,C) )).

cnf(meet_defn_26,axiom,
    ( ~ meet(A,B,C)
    | ~ incident_c(D,B)
    | ~ incident_c(D,C)
    | end_point(D,B) )).

cnf(meet_defn_27,axiom,
    ( ~ meet(A,B,C)
    | ~ incident_c(D,B)
    | ~ incident_c(D,C)
    | end_point(D,C) )).

cnf(meet_defn_28,axiom,
    ( ~ incident_c(A,B)
    | ~ incident_c(A,C)
    | incident_c(ax0_sk5(C,B,A),B)
    | meet(A,B,C) )).

cnf(meet_defn_29,axiom,
    ( ~ incident_c(A,B)
    | ~ incident_c(A,C)
    | incident_c(ax0_sk5(C,B,A),C)
    | meet(A,B,C) )).

cnf(meet_defn_30,axiom,
    ( ~ incident_c(A,B)
    | ~ incident_c(A,C)
    | ~ end_point(ax0_sk5(C,B,A),B)
    | ~ end_point(ax0_sk5(C,B,A),C)
    | meet(A,B,C) )).

cnf(closed_defn_31,axiom,
    ( ~ closed(A)
    | ~ end_point(B,A) )).

cnf(closed_defn_32,axiom,
    ( end_point(ax0_sk6(A),A)
    | closed(A) )).

cnf(open_defn_33,axiom,
    ( ~ open(A)
    | end_point(ax0_sk7(A),A) )).

cnf(open_defn_34,axiom,
    ( ~ end_point(A,B)
    | open(B) )).

cnf(c1_35,axiom,
    ( ~ part_of(A,B)
    | A = B
    | open(A) )).

cnf(c2_36,axiom,
    ( ~ part_of(A,B)
    | ~ part_of(C,B)
    | ~ part_of(D,B)
    | ~ end_point(E,A)
    | ~ end_point(E,C)
    | ~ end_point(E,D)
    | part_of(C,D)
    | part_of(D,C)
    | part_of(A,C)
    | part_of(C,A)
    | part_of(A,D)
    | part_of(D,A) )).

cnf(c3_37,axiom,
    ( inner_point(ax0_sk8(A),A) )).

cnf(c4_38,axiom,
    ( ~ inner_point(A,B)
    | meet(A,ax0_sk9(A,B),ax0_sk10(A,B)) )).

cnf(c4_39,axiom,
    ( ~ inner_point(A,B)
    | B = sum(ax0_sk9(A,B),ax0_sk10(A,B)) )).

cnf(c5_40,axiom,
    ( ~ end_point(A,B)
    | ~ end_point(C,B)
    | ~ end_point(D,B)
    | A = C
    | A = D
    | C = D )).

cnf(c6_41,axiom,
    ( ~ end_point(A,B)
    | end_point(ax0_sk11(A,B),B) )).

cnf(c6_42,axiom,
    ( ~ end_point(A,B)
    | A != ax0_sk11(A,B) )).

cnf(c7_43,axiom,
    ( ~ closed(A)
    | ~ meet(B,C,D)
    | A != sum(C,D)
    | ~ end_point(E,C)
    | meet(E,C,D) )).

cnf(c8_44,axiom,
    ( ~ meet(A,B,C)
    | ax0_sk12(C,B) = sum(B,C) )).

cnf(c9_45,axiom,
    ( incident_c(ax0_sk13(A,B),B)
    | incident_c(ax0_sk13(A,B),A)
    | B = A )).

cnf(c9_46,axiom,
    ( incident_c(ax0_sk13(A,B),B)
    | ~ incident_c(ax0_sk13(A,B),B)
    | B = A )).

cnf(c9_47,axiom,
    ( ~ incident_c(ax0_sk13(A,B),A)
    | incident_c(ax0_sk13(A,B),A)
    | B = A )).

cnf(c9_48,axiom,
    ( ~ incident_c(ax0_sk13(A,B),A)
    | ~ incident_c(ax0_sk13(A,B),B)
    | B = A )).

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