name(c82_).
:- dynamic p/2,l/2,i/2.

%domain elements
dom(a1). dom(b1). dom(c1). dom(a2). dom(b2). dom(c2).
dom(ab). dom(ac). dom(bc). dom(o).
dom(oa). dom(ob). dom(oc). 
dom(a1b1). dom(b1c1). dom(a1c1). dom(a2b2). dom(b2c2). dom(a2c2).

_ axiom goal_normal(U)  : (l(U,U),i(bc,U),i(ac,U),i(ab,U) => goal).
_ axiom t1in2 : (i(a1,b2c2),i(b1,a2c2),i(c1,a2b2) => goal).
_ axiom t2in1 : (i(a2,b1c1),i(b2,a1c1),i(c2,a1b1) => goal).

_ axiom gap_a : (true => i(a1,b2c2);i(b2,a1c1)).
_ axiom gap_b : (true => i(b1,a2c2);i(c2,a1b1)).
_ axiom gap_c : (true => i(c1,a2b2);i(a2,b1c1)).

%Desargues assumptions: points, lines and incidences
%triangles a1b1c1 and a2b2c2
_ axiom ia1b1 : (true => i(a1,a1b1)).
_ axiom ib1a1 : (true => i(b1,a1b1)).
_ axiom ia2b2 : (true => i(a2,a2b2)).
_ axiom ib2a2 : (true => i(b2,a2b2)).
_ axiom ia1c1 : (true => i(a1,a1c1)).
_ axiom ic1a1 : (true => i(c1,a1c1)).
_ axiom ia2c2 : (true => i(a2,a2c2)).
_ axiom ic2a2 : (true => i(c2,a2c2)).
_ axiom ic1b1 : (true => i(c1,b1c1)).
_ axiom ib1c1 : (true => i(b1,b1c1)).
_ axiom ic2b2 : (true => i(c2,b2c2)).
_ axiom ib2c2 : (true => i(b2,b2c2)).
% lines through perspectivity point o and corresponding vertices
_ axiom iooa  : (true => i(o,oa)).
_ axiom ioob  : (true => i(o,ob)).
_ axiom iooc  : (true => i(o,oc)).
_ axiom ia1oa : (true => i(a1,oa)).
_ axiom ia2oa : (true => i(a2,oa)).
_ axiom ib1ob : (true => i(b1,ob)).
_ axiom ib2ob : (true => i(b2,ob)).
_ axiom ic1oc : (true => i(c1,oc)).
_ axiom ic2oc : (true => i(c2,oc)).
% cross b1c1,b2c2 in point bc
_ axiom ibc1 : (true => i(bc,b1c1)).
_ axiom ibc2 : (true => i(bc,b2c2)).
% cross a1c1, a2c2 in point ac
_ axiom iac1 : (true => i(ac,a1c1)).
_ axiom iac2 : (true => i(ac,a2c2)).
% cross a1b1,a2b2 in point ab
_ axiom iab1 : (true => i(ab,a1b1)).
_ axiom iab2 : (true => i(ab,a2b2)).
%to prove: points ab,bc,ac on (perspectivity) line 

%triangle1 non-degenerate
_ axiom triangle1(L) : (i(a1,L),i(b1,L),i(c1,L) => false).

%triangle2 non-degenerate
_ axiom triangle2(L) : (i(a2,L),i(b2,L),i(c2,L) => false).

%no corresponding vertices in common
_ axiom notaa : (p(a2,a1)=>false). 
_ axiom notbb : (p(b2,b1)=>false). 
_ axiom notcc : (p(c2,c1)=>false).

%no corresponding edges in common
_ axiom notbc : (l(b1c1,b2c2)=>false). 
_ axiom notac : (l(a1c1,a2c2)=>false). 
_ axiom notab : (l(a1b1,a2b2)=>false).


%pequality for points
_ axiom pref(P,L)   : (i(P,L) => p(P,P)).     %sorted incidence
_ axiom psym(P,Q)   : (p(P,Q) => p(Q,P)).
_ axiom ptra(P,Q,R) : (p(P,Q),p(Q,R) => p(P,R)).

%pequality for lines
_ axiom lref(P,L)   : (i(P,L) => l(L,L)).     %sorted incidence
_ axiom lsym(L,M)   : (l(L,M) => l(M,L)).
_ axiom ltra(L,M,N) : (l(L,M),l(M,N) => l(L,N)).

%congruence
_ axiom pcon(P,Q,L) : (p(P,Q),i(Q,L) => i(P,L)).
_ axiom lcon(P,L,M) : (i(P,L),l(L,M) => i(P,M)).


%projective uniqueness
_ axiom unique(P,Q,L,M) : (i(P,L),i(P,M),i(Q,L),i(Q,M) => p(P,Q);l(L,M)).

 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%proof script%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%not necessary
