Pasted

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).