%------------------------------------------------------------------------------ % File : GEO009+0 : TPTP v7.2.0. Released v4.0.0. % Domain : Geometry (Constructive) % Axioms : Ordered affine geometry with definitions % Version : [vPl95] axioms. % English : % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry % Source : [ILTP] % Names : % Status : Satisfiable % Syntax : Number of formulae : 36 ( 6 unit) % Number of atoms : 109 ( 0 equality) % Maximal formula depth : 13 ( 5 average) % Number of connectives : 85 ( 12 ~; 22 |; 24 &) % ( 10 <=>; 17 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 18 ( 0 propositional; 1-4 arity) % Number of functors : 4 ( 0 constant; 1-2 arity) % Number of variables : 81 ( 0 sgn; 81 !; 0 ?) % Maximal term depth : 3 ( 1 average) % SPC : % Comments : %------------------------------------------------------------------------------ fof(a1_defns,axiom,( ! [X,Y] : ( unequally_directed_opposite_lines(X,Y) <=> unequally_directed_lines(X,reverse_line(Y)) ) )). fof(a2_defns,axiom,( ! [X,Y] : ( right_apart_point(X,Y) <=> left_apart_point(X,reverse_line(Y)) ) )). fof(a3_defns,axiom,( ! [X,Y] : ( right_convergent_lines(X,Y) <=> left_convergent_lines(X,reverse_line(Y)) ) )). fof(a4_defns,axiom,( ! [X,Y] : ( equally_directed_lines(X,Y) <=> ~ unequally_directed_lines(X,Y) ) )). fof(a5_defns,axiom,( ! [X,Y] : ( equally_directed_opposite_lines(X,Y) <=> ~ unequally_directed_opposite_lines(X,Y) ) )). fof(a6_defns,axiom,( ! [A,L] : ( apart_point_and_line(A,L) <=> ( left_apart_point(A,L) | right_apart_point(A,L) ) ) )). fof(a7_defns,axiom,( ! [L,M] : ( convergent_lines(L,M) <=> ( unequally_directed_lines(L,M) & unequally_directed_opposite_lines(L,M) ) ) )). fof(a8_defns,axiom,( ! [A,B,L] : ( divides_points(L,A,B) <=> ( ( left_apart_point(A,L) & right_apart_point(B,L) ) | ( right_apart_point(A,L) & left_apart_point(B,L) ) ) ) )). fof(ax4_defns,axiom,( ! [L,A,B] : ( before_on_line(L,A,B) <=> ( distinct_points(A,B) & incident_point_and_line(A,L) & incident_point_and_line(B,L) & equally_directed_lines(L,line_connecting(A,B)) ) ) )). fof(a9_defns,axiom,( ! [L,A,B,C] : ( between_on_line(L,A,B,C) <=> ( ( before_on_line(L,A,B) & before_on_line(L,B,C) ) | ( before_on_line(L,C,B) & before_on_line(L,B,A) ) ) ) )). fof(ax1_basics,axiom,( ! [A] : ~ distinct_points(A,A) )). fof(ax2_basics,axiom,( ! [A,B,C] : ( distinct_points(A,B) => ( distinct_points(A,C) | distinct_points(B,C) ) ) )). fof(ax3_basics,axiom,( ! [L] : ~ distinct_lines(L,L) )). fof(ax4_basics,axiom,( ! [L,M,N] : ( distinct_lines(L,M) => ( distinct_lines(L,N) | distinct_lines(M,N) ) ) )). fof(ax5_basics,axiom,( ! [L] : equally_directed_lines(L,L) )). fof(ax6_basics,axiom,( ! [L,M,N] : ( unequally_directed_lines(L,M) => ( unequally_directed_lines(L,N) | unequally_directed_lines(M,N) ) ) )). fof(ax7_basics,axiom,( ! [L,M,N] : ( ( unequally_directed_lines(L,M) & unequally_directed_lines(L,reverse_line(M)) ) => ( ( unequally_directed_lines(L,N) & unequally_directed_lines(L,reverse_line(N)) ) | ( unequally_directed_lines(M,N) & unequally_directed_lines(M,reverse_line(N)) ) ) ) )). fof(ax8_basics,axiom,( ! [L,M] : ( unequally_directed_lines(L,M) | unequally_directed_lines(L,reverse_line(M)) ) )). fof(ax9_basics,axiom,( ! [L,M] : ( ( unequally_directed_lines(L,M) & unequally_directed_lines(L,reverse_line(M)) ) => ( left_convergent_lines(L,M) | left_convergent_lines(L,reverse_line(M)) ) ) )). fof(ax10_basics,axiom,( ! [A,L] : ~ ( left_apart_point(A,L) | left_apart_point(A,reverse_line(L)) ) )). fof(ax11_basics,axiom,( ! [L,M] : ~ ( left_convergent_lines(L,M) | left_convergent_lines(L,reverse_line(M)) ) )). fof(ax1_cons_objs,axiom,( ! [A,B] : ( ( point(A) & point(B) & distinct_points(A,B) ) => line(line_connecting(A,B)) ) )). fof(ax2_cons_objs,axiom,( ! [L,M] : ( ( line(L) & line(M) & unequally_directed_lines(L,M) & unequally_directed_lines(L,reverse_line(M)) ) => point(intersection_point(L,M)) ) )). fof(ax3_cons_objs,axiom,( ! [L,A] : ( ( point(A) & line(L) ) => line(parallel_through_point(L,A)) ) )). fof(ax4_cons_objs,axiom,( ! [L] : ( line(L) => line(reverse_line(L)) ) )). fof(ax5_cons_objs,axiom,( ! [A,B] : ( distinct_points(A,B) => ( ~ apart_point_and_line(A,line_connecting(A,B)) & ~ apart_point_and_line(B,line_connecting(A,B)) ) ) )). fof(ax6_cons_objs,axiom,( ! [L,M] : ( ( unequally_directed_lines(L,M) & unequally_directed_lines(L,reverse_line(M)) ) => ( ~ apart_point_and_line(intersection_point(L,M),L) & ~ apart_point_and_line(intersection_point(L,M),M) ) ) )). fof(ax7_cons_objs,axiom,( ! [A,L] : ~ apart_point_and_line(A,parallel_through_point(L,A)) )). fof(ax8_cons_objs,axiom,( ! [L] : ~ distinct_lines(L,reverse_line(L)) )). fof(ax9_cons_objs,axiom,( ! [A,B] : ( distinct_points(A,B) => equally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A)))) )). fof(ax10_cons_objs,axiom,( ! [A,L] : equally_directed_lines(parallel_through_point(L,A),L) )). fof(ax1_uniq_cons,axiom,( ! [A,B,L,M] : ( ( distinct_points(A,B) & distinct_lines(L,M) ) => ( left_apart_point(A,L) | left_apart_point(B,L) | left_apart_point(A,M) | left_apart_point(B,M) | left_apart_point(A,reverse_line(L)) | left_apart_point(B,reverse_line(L)) | left_apart_point(A,reverse_line(M)) | left_apart_point(B,reverse_line(M)) ) ) )). fof(ax2_uniq_cons,axiom,( ! [A,B,L] : ( ( distinct_points(A,B) & left_apart_point(A,L) ) => ( left_apart_point(B,L) | left_convergent_lines(line_connecting(A,B),L) ) ) )). fof(ax1_subs,axiom,( ! [A,B,L] : ( left_apart_point(A,L) => ( distinct_points(A,B) | left_apart_point(B,L) ) ) )). fof(ax2_subs,axiom,( ! [A,L,M] : ( ( left_apart_point(A,L) & unequally_directed_lines(L,M) ) => ( distinct_lines(L,M) | left_apart_point(A,reverse_line(M)) ) ) )). fof(ax3_subs,axiom,( ! [L,M,N] : ( left_convergent_lines(L,M) => ( unequally_directed_lines(M,N) | left_convergent_lines(L,N) ) ) )). %------------------------------------------------------------------------------