validateGoalWithLastRow([ProofHead|[]], Goal) :-
	[_,Fact,_] = ProofHead,
	Goal = Fact,!.
validateGoalWithLastRow([_|ProofTail], Goal) :-
	validateGoalWithLastRow(ProofTail, Goal),!.

main :-
	open('invalid28.txt',read,Stream),
	read(Stream,Premises),
	read(Stream,Goal),
	read(Stream,Proof),
	close(Stream),
	validateGoalWithLastRow(Proof,Goal),
	validateProof(Premises,Goal,Proof,[],false),!.

validateProof(_,_,[],_,_).
validateProof(Premises,Goal,[[RowNr,Fact,assumption]|ProofTail],VerifiedRows,true) :-
	validateProof(Premises,Goal,ProofTail,[[RowNr,Fact]|VerifiedRows],false).
validateProof(Premises,Goal,[[RowNr,Fact,Rule]|ProofTail],VerifiedRows,false) :-
	examineRow([RowNr,Fact,Rule],Premises,Goal,VerifiedRows),
	validateProof(Premises,Goal,ProofTail,[[RowNr,Fact]|VerifiedRows],false).
validateProof(Premises,Goal,[ProofHead|ProofTail],VerifiedRows,false) :-
	validateProof(Premises,Goal,ProofHead,VerifiedRows,true),
	[[RowNr,Fact,assumption]|NewTail] = ProofHead,
	last(ProofHead,[RowNr2,Fact2,_]),
	NewVerifiedRows = [[RowNr, RowNr2, Fact, Fact2] | VerifiedRows],
	validateProof(Premises,Goal,ProofTail,NewVerifiedRows,false).

% [RowNr,Fact,premise] check if the fact is amongst our Premises.
examineRow([_,Fact,premise],Premises,_,_) :-
	member(Fact,Premises),!.

% [RowNr,Fact,impel(X,Y)] check if the elimination of implication is performed correctly
% accordingly to " p, p->q", remember that p needs to be stated first as X and p->q second as Y.
% Implication Elimination
examineRow([_,Fact,impel(X,Y)],_,_,VerifiedRows) :-
	member([X,Q], VerifiedRows),!,
	member([Y,imp(Q,Fact)],VerifiedRows),!.

%Copy(X).
examineRow([_,Fact,copy(X)],_,_,VerifiedRows) :-
	member([X,Fact], VerifiedRows).

%Implication Introduction
examineRow([_, imp(P,Q), impint(X,Y)],_,_,VerifiedRows) :-
	member([X,Y,P,Q],VerifiedRows).

%Contradiction check, check if Q is at row X and then check if neg(Q) is at row Y.
%Negation Elimination
examineRow([_, cont, negel(X,Y)],_,_,VerifiedRows) :-
	member([X,Q], VerifiedRows),
	member([Y,neg(Q)], VerifiedRows).

%OREL Or Elimination
examineRow([_, Whatever, orel(A,B,C,D,E)],_,_,VerifiedRows) :-
	member([A, or(Q,R)], VerifiedRows),
	member([B,C,Q,Whatever], VerifiedRows),
	member([D,E,R,Whatever], VerifiedRows).

%PBC 
examineRow([_, Q, pbc(X,Y)],_,_,VerifiedRows) :-
	member([X,Y,neg(Q),cont], VerifiedRows).


/*fffffffffffffffffffffffffffffffffffffffffffff*/

%And Introduction
examineRow([_, and(P,Q), andint(X,Y)],_,_,VerifiedRows) :-
	member([X, P], VerifiedRows),
	member([Y, Q], VerifiedRows).

%And elimination 1
examineRow([_, P, andel1(X)],_,_,VerifiedRows) :-
	member([X, and(P,_)], VerifiedRows).

%And Elimination 2
examineRow([_, Q, andel2(X)],_,_,VerifiedRows) :-
	member([X, and(_,Q)], VerifiedRows).

%Or Introduction 1
examineRow([_, or(P,_), orint1(X)],_,_,VerifiedRows) :-
	member([X, P], VerifiedRows).

%Or introduction 2
examineRow([_, or(_,Q), orint2(X)],_,_,VerifiedRows) :-
	member([X, Q], VerifiedRows).

%LEM
examineRow([_, or(Q,neg(Q)), lem],_,_,_).

%MT
examineRow([_, neg(Q), mt(X,Y)],_,_,VerifiedRows) :-
	member([X, imp(Q,P)], VerifiedRows),
	member([Y, neg(P)], VerifiedRows).

%negation introduction
examineRow([_, neg(P), negint(X,Y)],_,_,VerifiedRows) :-
	member([X,Y,P,cont], VerifiedRows).

examineRow([_, _, contel(X)],_,_,VerifiedRows) :-
	member([X, cont], VerifiedRows).

examineRow([_, neg(neg(P)), negnegint(X)],_,_,VerifiedRows) :-
	member([X, P], VerifiedRows).

examineRow([_, P, negnegel(X)],_,_,VerifiedRows) :-
	member([X, neg(neg(P))], VerifiedRows).