The following is all the Prolog code from"First-Order Logic and Automated Theorem Proving"Second Editionby Melvin FittingSpringer 1996Each portion is identified by a marker at the beginning,of the form:**-----------------Page numbers-----------------------**-----------------36 to 39---------------------------/*  Dual Clause Form Program  Propositional operators are: neg, and, or, imp, revimp,    uparrow, downarrow, notimp and notrevimp.*/?-op(140, fy, neg).?-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow,    notimp, notrevimp])./*  member(Item, List) :- Item occurs in List.*/member(X, [X | _]).member(X, [_ | Tail]) :- member(X, Tail)./*  remove(Item, List, Newlist) :-      Newlist is the result of removing all occurrences of      Item from List.*/remove(X, [ ], [ ]).remove(X, [X | Tail], Newtail) :-  remove(X, Tail, Newtail).remove(X, [Head | Tail], [Head | Newtail]) :-   remove(X, Tail, Newtail)./*  conjunctive(X) :- X is an alpha formula.*/conjunctive(_ and _).conjunctive(neg(_ or _)).conjunctive(neg(_ imp _)).conjunctive(neg(_ revimp _)).conjunctive(neg(_ uparrow _)).conjunctive(_ downarrow _).conjunctive(_ notimp _).conjunctive(_ notrevimp _)./*  disjunctive(X) :- X is a beta formula.*/disjunctive(neg(_ and _)).disjunctive(_ or _).disjunctive(_ imp _).disjunctive(_ revimp _).disjunctive(_ uparrow _).disjunctive(neg(_ downarrow _)).disjunctive(neg(_ notimp _)).disjunctive(neg(_ notrevimp _))./*  unary(X) :- X is a double negation,      or a negated constant.*/unary(neg neg _).unary(neg true).unary(neg false).    /*  components(X, Y, Z) :- Y and Z are the components      of the formula X, as defined in the alpha and      beta table.*/components(X and Y, X, Y).components(neg(X and Y), neg X, neg Y).components(X or Y, X, Y).components(neg(X or Y), neg X, neg Y).components(X imp Y, neg X, Y).components(neg(X imp Y), X, neg Y).components(X revimp Y, X, neg Y).components(neg(X revimp Y), neg X, Y).components(X uparrow Y, neg X, neg Y).components(neg(X uparrow Y), X, Y).components(X downarrow Y, neg X, neg Y).components(neg(X downarrow Y), X, Y).components(X notimp Y, X, neg Y).components(neg(X notimp Y), neg X, Y).components(X notrevimp Y, neg X, Y).components(neg(X notrevimp Y), X, neg Y)./*  component(X, Y) :- Y is the component of the      unary formula X.*/component(neg neg X, X).component(neg true, false).component(neg false, true)./*  singlestep(Old, New) :-  New is the result of applying      a single step of the expansion process to Old, which      is a generalized disjunction of generalized      conjunctions.*/singlestep([Conjunction | Rest], New) :-  member(Formula, Conjunction),  unary(Formula),  component(Formula, Newformula),  remove(Formula, Conjunction, Temporary),  Newconjunction = [Newformula | Temporary],  New = [Newconjunction | Rest].singlestep([Conjunction | Rest], New) :-  member(Alpha, Conjunction),  conjunctive(Alpha),  components(Alpha, Alphaone, Alphatwo),  remove(Alpha, Conjunction, Temporary),  Newcon = [Alphaone, Alphatwo | Temporary],  New = [Newcon | Rest].singlestep([Conjunction | Rest], New) :-  member(Beta, Conjunction),  disjunctive(Beta),  components(Beta, Betaone, Betatwo),  remove(Beta, Conjunction, Temporary),  Newconone = [Betaone | Temporary],  Newcontwo = [Betatwo | Temporary],  New = [Newconone, Newcontwo | Rest].singlestep([Conjunction|Rest], [Conjunction|Newrest]) :-  singlestep(Rest, Newrest)./*  expand(Old, New) :- New is the result of applying      singlestep as many times as possible, starting      with Old.*/expand(Dis, Newdis) :-  singlestep(Dis, Temp),  expand(Temp, Newdis).expand(Dis, Dis)./*  dualclauseform(X, Y) :- Y is the dual clause form of X.*/dualclauseform(X, Y) :- expand([[X]], Y).**-----------------47 to 47---------------------------/*  closed(Tableau) :- every branch of Tableau contains a        contradiction.*/closed([Branch | Rest]) :-  member(false, Branch),  closed(Rest).closed([Branch | Rest]) :-  member(X, Branch),  member(neg X, Branch),  closed(Rest).closed([ ]).**-----------------48 to 48---------------------------/*  test(X) :- create a complete tableau expansion        for neg X, and see if it is closed.*/test(X) :-  expand([[neg X]], Y),  closed(Y).**-----------------48 to 48---------------------------test(X) :-  expand([[neg X]], Y),  !,  closed(Y).**-----------------48 to 48--------------------------- /*  if_then_else(P, Q, R) :-        either P and Q, or not P and R.*/if_then_else(P, Q, R) :- P, !, Q.if_then_else(P, Q, R) :- R.**-----------------48 to 49---------------------------/*  test(X) :- create a complete tableau expansion        for neg X, if it is closed, say we have a        proof, otherwise, say we don't.*/test(X) :-  expand([[neg X]], Y),  if_then_else(closed(Y), yes, no).yes :- write('Propositional tableau theorem'), nl.no :- write('Not a propositional tableau theorem'), nl.**-----------------49 to 49---------------------------/*  expand_and_close(Tableau) :-      some expansion of Tableau closes.*/expand_and_close(Tableau) :-  closed(Tableau).expand_and_close(Tableau) :-  singlestep(Tableau, Newtableau), !,  expand_and_close(Newtableau).**-----------------50 to 50---------------------------/*  test(X) :- create a tableau expansion for neg X,        if it is closed, say we have a proof,        otherwise, say we don't.*/test(X) :-  if_then_else(expand_and_close([[neg X]]), yes, no).**-----------------161 to 161-------------------------/*  variable(X) :- X is a free variable.*/variable(var(_)).**-----------------162 to 162-------------------------/*  partialvalue(X, Env, Y) :-      Y is the partially evaluated value of term X      in environment Env.*/partialvalue(X, Env, Y) :-   member([X,Z], Env),   partialvalue(Z, Env, Y).partialvalue(X, Env, X)./*  member(X, Y) :- X is a member of the list Y.*/member(X, [X | _]).member(X, [_ | Y]) :- member(X, Y).**-----------------162 to 162-------------------------/*  in(X, T, Env) :-      X occurs in term T, evaluated in environment Env.*/in(X, T, Env) :-   partialvalue(T, Env, U),   ( X == U;     not variable(U), not atomic(U), infunctor(X, U, Env)   ).infunctor(X, U, Env) :-   U =.. [_|L],   inlist(X, L, Env).inlist(X, [T|_], Env) :-   in(X, T, Env).inlist(X, [_|L], Env) :-   inlist(X, L, Env).**-----------------163 to 164-------------------------/*  unify(Term1, Term2, Env, Newenv) :-      Unifying Term1 and Term2 in environment Env      produces the new environment Newenv.*/unify(Term1, Term2, Env, Newenv) :-   partialvalue(Term1, Env, Val1),   partialvalue(Term2, Env, Val2),   (     (Val1==Val2, Newenv = Env);     (variable(Val1), not in(Val1, Val2, Env),        Newenv=[ [Val1, Val2] | Env] );     (variable(Val2), not in(Val2, Val1, Env),        Newenv=[ [Val2, Val1] | Env] );     (not variable(Val1), not variable(Val2),        not atomic(Val1), not atomic(Val2),        unifyfunctor(Val1, Val2, Env, Newenv) )   )./*  unifyfunctor(Fun1, Fun2, Env, Newenv) :-      Unifying the functors Fun1 and Fun2 in      environment Env produces environment Newenv.*/unifyfunctor(Fun1, Fun2, Env, Newenv) :-   Fun1 =.. [FunSymb | Args1],   Fun2 =.. [FunSymb | Args2],   unifylist(Args1, Args2, Env, Newenv)./*  unifylist(List1, List2, Env, Newenv) :-      Starting in environment Env and      unifying each term in List1 with the      corresponding term in List2 produces      the environment Newenv.*/unifylist([ ], [ ], Env, Env).unifylist([Head1 | Tail1], [Head2 | Tail2], Env, Newenv) :-   unify(Head1, Head2, Env, Temp),   unifylist(Tail1, Tail2, Temp, Newenv).**-----------------164 to 165-------------------------/*  unify(Term1, Term2) :-       Term1 and Term2 are unified with the occurs check.       See Sterling and Shapiro, The Art of Prolog.*/unify(X,Y) :-     var(X), var(Y), X=Y.unify(X,Y) :-     var(X), nonvar(Y), not_occurs_in(X,Y), X=Y.unify(X,Y) :-     var(Y), nonvar(X), not_occurs_in(Y,X), Y=X.unify(X,Y) :-     nonvar(X), nonvar(Y), atomic(X), atomic(Y), X=Y.unify(X,Y) :-     nonvar(X), nonvar(Y),     compound(X), compound(Y),     term_unify(X,Y).not_occurs_in(X,Y) :-     var(Y), X \== Y.not_occurs_in(X,Y) :-     nonvar(Y), atomic(Y).not_occurs_in(X,Y) :-     nonvar(Y), compound(Y), functor(Y,F,N),     not_occurs_in(N,X,Y).not_occurs_in(N,X,Y) :-     N>0, arg(N,Y,Arg), not_occurs_in(X,Arg), N1 is N-1,     not_occurs_in(N1,X,Y).not_occurs_in(0,X,Y) .term_unify(X,Y) :-     functor(X,F,N), functor(Y,F,N), unify_args(N,X,Y).unify_args(N,X,Y) :-     N>0, unify_arg(N,X,Y), N1 is N-1, unify_args(N1,X,Y).unify_args(0,X,Y).unify_arg(N,X,Y) :-     arg(N,X,ArgX), arg(N,Y,ArgY), unify(ArgX,ArgY).compound(X) :- functor(X,_,N), N>0.**-----------------169 to 170-------------------------/*   member(Item, List) :- Item occurs in List.*/member(X, [X | _]).member(X, [_ | Tail]) :- member(X, Tail)./*   remove(Item, List, Newlist) :-         Newlist is the result of removing all         occurrences of Item from List.*/remove(X, [ ], [ ]).remove(X, [Y | Tail], Newtail) :-   X == Y,   remove(X, Tail, Newtail).remove(X, [Y | Tail], [Y | Newtail]) :-   X \== Y,   remove(X, Tail, Newtail)./*   append(ListA, ListB, Newlist) :-         Newlist is the result of appending ListA         and ListB.*/append([ ], List, List).append([Head | Tail], List, [Head | Newlist]) :-   append(Tail, List, Newlist).**-----------------170 to 172-------------------------/*   Propositional operators are: neg, and, or, imp,       revimp, uparrow, downarrow, notimp       and notrevimp.*/?-op(140, fy, neg).?-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow,   notimp, notrevimp])./*   conjunctive(X) :- X is an alpha formula.*/conjunctive(_ and _).conjunctive(neg(_ or _)).conjunctive(neg(_ imp _)).conjunctive(neg(_ revimp _)).conjunctive(neg(_ uparrow _)).conjunctive(_ downarrow _).conjunctive(_ notimp _).conjunctive(_ notrevimp _)./*   disjunctive(X) :- X is a beta formula.*/disjunctive(neg(_ and _)).disjunctive(_ or _).disjunctive(_ imp _).disjunctive(_ revimp _).disjunctive(_ uparrow _).disjunctive(neg(_ downarrow _)).disjunctive(neg(_ notimp _)).disjunctive(neg(_ notrevimp _))./*   unary(X) :- X is a double negation,         or a negated propositional constant.*/unary(neg neg _).unary(neg true).unary(neg false)./*   binary_operator(X) :- X is a binary operator.*/binary_operator(X) :-   member(X, [and, or, imp, revimp, uparrow, downarrow,   notimp, notrevimp])./*   components(X, Y, Z) :- Y and Z are the components of         the formula X, as defined in the alpha and         beta table.*/components(X and Y, X, Y).components(neg(X and Y), neg X, neg Y).components(X or Y, X, Y).components(neg(X or Y), neg X, neg Y).components(X imp Y, neg X, Y).components(neg(X imp Y), X, neg Y).components(X revimp Y, X, neg Y).components(neg(X revimp Y), neg X, Y).components(X uparrow Y, neg X, neg Y).components(neg(X uparrow Y), X, Y).components(X downarrow Y, neg X, neg Y).components(neg(X downarrow Y), X, Y).components(X notimp Y, X, neg Y).components(neg(X notimp Y), neg X, Y).components(X notrevimp Y, neg X, Y).components(neg(X notrevimp Y), X, neg Y)./*   component(X, Y) :- Y is the component of the         unary formula X.*/component(neg neg X, X).component(neg true, false).component(neg false, true).**-----------------172 to 173-------------------------/*   universal(X) :- X is a gamma formula.*/universal(all(_,_)).universal(neg some(_,_))./*   existential(X) :- X is a delta formula.*/existential(some(_,_)).existential(neg all(_,_))./*   literal(X) :- X is a literal.*/literal(X) :-   not conjunctive(X),   not disjunctive(X),   not unary(X),   not universal(X),   not existential(X)./*   atomicfmla(X) :- X is an atomic formula.*/atomicfmla(X) :-   literal(X),   X \= neg _.**-----------------173 to 174-------------------------/*   sub(Term, Variable, Formula, NewFormula) :-         NewFormula is the result of substituting         occurrences of Term for each free         occurrence of Variable in Formula.*/sub(Term, Variable, Formula, NewFormula) :-   sub_(Term, Variable, Formula, NewFormula) , !.sub_(Term, Var, A, Term) :- Var == A.sub_(Term, Var, A, A) :- atomic(A).sub_(Term, Var, A, A) :- var(A).sub_(Term, Var, neg X, neg Y) :-   sub_(Term, Var, X, Y).sub_(Term, Var, Binary_One, Binary_Two) :-   binary_operator(F),   Binary_One =.. [F, X, Y],   Binary_Two =.. [F, U, V],   sub_(Term, Var, X, U),   sub_(Term, Var, Y, V).sub_(Term, Var, all(Var, Y), all(Var, Y)).sub_(Term, Var, all(X, Y), all(X, Z)) :-   sub_(Term, Var, Y, Z).sub_(Term, Var, some(Var, Y), some(Var, Y)).sub_(Term, Var, some(X, Y), some(X, Z)) :-   sub_(Term, Var, Y, Z).sub_(Term, Var, Functor, Newfunctor) :-    Functor =.. [F | Arglist],   sub_list(Term, Var, Arglist, Newarglist),   Newfunctor =.. [F | Newarglist].sub_list(Term, Var, [Head | Tail], [Newhead | Newtail]) :-   sub_(Term, Var, Head, Newhead),   sub_list(Term, Var, Tail, Newtail).sub_list(Term, Var, [ ], [ ]).**-----------------174 to 174-------------------------/*  instance(F, Term, Ins) :-         F is a quantified formula, and Ins is the result         of removing the quantifier and replacing all         free occurrences of the quantified variable by         occurrences of Term.*/instance(all(X,Y), Term, Z) :- sub(Term, X, Y, Z).instance(neg some(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).instance(some(X,Y), Term, Z) :- sub(Term, X, Y, Z).instance(neg all(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).**-----------------175 to 175-------------------------/*   funcount(N) :- N is the current Skolem function index.*/funcount(1)./*   newfuncount(N) :-         N is the current Skolem function index, and as a         side effect, the remembered value is incremented.*/newfuncount(N) :-   funcount(N),   retract(funcount(N)),   M is N+1,   assert(funcount(M))./*   reset :- the Skolem function index is reset to 1.*/reset :-   retract(funcount(_)),   assert(funcount(1)),   !.**-----------------175 to 176-------------------------/*   sko_fun(X, Y) :-         X is a list of free variables, and Y is a         previously unused Skolem function symbol         applied to those free variables.*/sko_fun(Varlist, Skoterm) :-   newfuncount(N),   Skoterm =.. [fun | [N | Varlist]].**-----------------176 to 176-------------------------/*   notation(Notated, Free) :-         Notated is a notated formula, and Free is its         associated free variable list.*/notation(n(X, Y), X)./*   fmla(Notated, Formula) :-         Notated is a notated formula, and Formula is its         formula part.*/fmla(n(X, Y), Y).**-----------------178 to 180-------------------------/*   singlestep(OldTableau, OldQdepth,            NewTableau, NewQdepth) :-         the application of one tableau rule to OldTableau,         with a Q-depth of OldQdepth, will produce the         tableau NewTableau, and will change the available         Q-depth to NewQdepth.*/singlestep([OldBranch | Rest], Qdepth,      [NewBranch | Rest], Qdepth) :-   member(NotatedFormula, OldBranch),   notation(NotatedFormula, Free),   fmla(NotatedFormula, Formula),   unary(Formula),   component(Formula, NewFormula),   notation(NewNotatedFormula, Free),   fmla(NewNotatedFormula, NewFormula),   remove(NotatedFormula, OldBranch, TempBranch),   NewBranch = [NewNotatedFormula | TempBranch].singlestep([OldBranch | Rest], Qdepth,      [NewBranch | Rest], Qdepth) :-   member(NotatedAlpha, OldBranch),   notation(NotatedAlpha, Free),   fmla(NotatedAlpha, Alpha),   conjunctive(Alpha),   components(Alpha, AlphaOne, AlphaTwo),   notation(NotatedAlphaOne, Free),   fmla(NotatedAlphaOne, AlphaOne),   notation(NotatedAlphaTwo, Free),   fmla(NotatedAlphaTwo, AlphaTwo),   remove(NotatedAlpha, OldBranch, TempBranch),   NewBranch =     [NotatedAlphaOne, NotatedAlphaTwo | TempBranch].singlestep([OldBranch | Rest], Qdepth,      [NewBranchOne, NewBranchTwo | Rest], Qdepth) :-   member(NotatedBeta, OldBranch),   notation(NotatedBeta, Free),   fmla(NotatedBeta, Beta),   disjunctive(Beta),   components(Beta, BetaOne, BetaTwo),   notation(NotatedBetaOne, Free),   fmla(NotatedBetaOne, BetaOne),   notation(NotatedBetaTwo, Free),   fmla(NotatedBetaTwo, BetaTwo),   remove(NotatedBeta, OldBranch, TempBranch),   NewBranchOne = [NotatedBetaOne | TempBranch],   NewBranchTwo = [NotatedBetaTwo | TempBranch].singlestep([OldBranch | Rest], Qdepth,      [NewBranch | Rest], Qdepth) :-   member(NotatedDelta, OldBranch),   notation(NotatedDelta, Free),   fmla(NotatedDelta, Delta),   existential(Delta),   sko_fun(Free, Term),   instance(Delta, Term, DeltaInstance),   notation(NotatedDeltaInstance, Free),   fmla(NotatedDeltaInstance, DeltaInstance),   remove(NotatedDelta, OldBranch, TempBranch),   NewBranch = [NotatedDeltaInstance | TempBranch].singlestep([OldBranch | Rest], OldQdepth,      NewTree, NewQdepth) :-   member(NotatedGamma, OldBranch),   notation(NotatedGamma, Free),   fmla(NotatedGamma, Gamma),   universal(Gamma),   OldQdepth > 0,   remove(NotatedGamma, OldBranch, TempBranch),   NewFree = [V | Free],   instance(Gamma, V, GammaInstance),   notation(NotatedGammaInstance, NewFree),   fmla(NotatedGammaInstance, GammaInstance),   append([NotatedGammaInstance | TempBranch],      [NotatedGamma], NewBranch),   append(Rest, [NewBranch], NewTree),   NewQdepth is OldQdepth-1.singlestep([Branch | OldRest], OldQdepth,      [Branch | NewRest], NewQdepth) :-   singlestep(OldRest, OldQdepth, NewRest, NewQdepth).**-----------------180 to 180-------------------------/*   expand(Tree, Qdepth, Newtree) :-         the complete expansion of the tableau Tree,         allowing Qdepth applications of the gamma         rule, is Newtree.*/expand(Tree, Qdepth, Newtree) :-   singlestep(Tree, Qdepth, TempTree, TempQdepth),   expand(TempTree, TempQdepth, Newtree).expand(Tree, Qdepth, Tree).**-----------------180 to 181-------------------------/*   unify(Term1, Term2) :-         Term1 and Term2 are unified with the occurs check.         See Sterling and Shapiro,         The Art of Prolog.*/unify(X,Y) :-   var(X), var(Y), X=Y.unify(X,Y) :-   var(X), nonvar(Y), not_occurs_in(X,Y), X=Y.unify(X,Y) :-   var(Y), nonvar(X), not_occurs_in(Y,X), Y=X.unify(X,Y) :-   nonvar(X), nonvar(Y), atomic(X), atomic(Y), X=Y.unify(X,Y) :-   nonvar(X), nonvar(Y),   compound(X), compound(Y),   term_unify(X,Y).not_occurs_in(X,Y) :-   var(Y), X \== Y.not_occurs_in(X,Y) :-   nonvar(Y), atomic(Y).not_occurs_in(X,Y) :-   nonvar(Y), compound(Y), functor(Y,F,N),   not_occurs_in(N,X,Y).not_occurs_in(N,X,Y) :-   N>0, arg(N,Y,Arg), not_occurs_in(X,Arg), N1 is N-1,   not_occurs_in(N1,X,Y).not_occurs_in(0,X,Y) .term_unify(X,Y) :-   functor(X,F,N), functor(Y,F,N), unify_args(N,X,Y).unify_args(N,X,Y) :-   N>0, unify_arg(N,X,Y), N1 is N-1, unify_args(N1,X,Y).unify_args(0,X,Y).unify_arg(N,X,Y) :-   arg(N,X,ArgX), arg(N,Y,ArgY), unify(ArgX,ArgY).compound(X) :- functor(X,_,N), N>0.**-----------------181 to 182-------------------------/*   closed(Tableau) :- every branch of Tableau can be        made to contain a contradiction, after a suitable        free variable substitution.*/closed([Branch | Rest]) :-   member(Falsehood, Branch),   fmla(Falsehood, false),   closed(Rest).closed([Branch | Rest]) :-   member(NotatedOne, Branch),   fmla(NotatedOne, X),   atomicfmla(X),   member(NotatedTwo, Branch),   fmla(NotatedTwo, neg Y),   unify(X, Y),   closed(Rest).closed([ ]).**-----------------182 to 183-------------------------/*   if_then_else(P, Q, R) :-         either P and Q, or not P and R.*/if_then_else(P, Q, R) :- P, !, Q.if_then_else(P, Q, R) :- R./*   test(X, Qdepth) :- create a complete tableau expansion        for neg X, allowing Qdepth applications of the        gamma rule.  Test for closure.*/test(X, Qdepth) :-    reset,   notation(NotatedFormula, [ ]),   fmla(NotatedFormula, neg X),   expand([[NotatedFormula]], Qdepth, Tree),   if_then_else(closed(Tree), yes(Qdepth), no(Qdepth)).yes(Qdepth) :-   write('First-order tableau theorem at Q-depth '),   write(Qdepth),   write(.),   nl.no(Qdepth) :-   write('Not a first-order tableau theorem at Q-depth '),   write(Qdepth),   write('.'),   nl.**-----------------305 to 305-------------------------?-op(120, xfy, eq).**-----------------305 to 305-------------------------/*   not_member(Item, List) :-         Item does not occur in List, where an         occurrence must be via identity, not         via unification.*/not_member(_, [ ]).not_member(Item, [Head | Tail]) :-   Item \== Head, not_member(Item, Tail).**-----------------306 to 307-------------------------/*   replace_term(T, Term, U, NewTerm) :-         NewTerm is the result of replacing one         occurrence of T in Term (after a unification)         with an occurrence of U.*/replace_term(T, Term, U, NewTerm) :-   unify(T, Term),   unify(U, NewTerm).replace_term(T, Term, U, NewTerm) :-   compound(Term),   Term =.. [F | Args],   replace_term_list(T, Args, U, NewArgs),   NewTerm =.. [F | NewArgs]./*   replace_term_list(T, OldList, U, NewList) :-         OldList is a list of terms, and NewList         is the result of applying replace_term         to one of them, replacing T by U.*/replace_term_list(T, [First | Rest],    U, [NewFirst | Rest]) :-      replace_term(T, First, U, NewFirst).replace_term_list(T, [First | Rest],    U, [First | NewRest]) :-      replace_term_list(T, Rest, U, NewRest).**-----------------307 to 307-------------------------/*   replace_atomic(T, Atomic, U, NewAtomic) :-         NewAtomic is the result of replacing one          occurrence of the term T in the atomic formula         Atomic with an occurrence of U.*/replace_atomic(T, Atomic, U, NewAtomic):-   atomicfmla(Atomic),   Atomic =.. [F | Args],   replace_term_list(T, Args, U, NewArgs),   NewAtomic =.. [F | NewArgs]./*   replace_literal(T, Literal, U, NewLiteral) :-         NewLiteral is the result of replacing one         occurrence of the term T in the literal         Literal with an occurrence of U.*/replace_literal(T, Atomic, U, NewAtomic) :-   replace_atomic(T, Atomic, U, NewAtomic).replace_literal(T, neg Atomic, U, neg NewAtomic) :-   replace_atomic(T, Atomic, U, NewAtomic).**-----------------308 to 309-------------------------/*   reorganize(OldTableau, RDepth, NewTableau) :-         NewTableau is OldTableau with each branch         purged of all non-literals, and for each         notated literal, the notation is changed         to RDepth.*/reorganize([ ], _, [ ]).reorganize([OldBranch | Rest], RDepth,     [NewBranch | NewRest]) :-   modifybranch(OldBranch, RDepth, NewBranch),   reorganize(Rest, RDepth, NewRest)./*   modifybranch(OldBranch, RDepth, NewBranch) :-         NewBranch is OldBranch with each non-literal         removed, and for each notated literal, the         notation is changed to RDepth.*/modifybranch([ ], _, [ ]).modifybranch([NotatedLiteral | Rest], RDepth,     [NewNotatedLiteral | NewRest]) :-   fmla(NotatedLiteral, Literal),   literal(Literal),   fmla(NewNotatedLiteral, Literal),   notation(NewNotatedLiteral, RDepth),   modifybranch(Rest, RDepth, NewRest).modifybranch([NonNotatedLiteral | Rest], RDepth,     NewRest) :-   modifybranch(Rest, RDepth, NewRest).**-----------------309 to 310-------------------------closed([Branch | Rest]) :-   member(Notated, Branch),   fmla(Notated, neg X eq Y),   unify(X, Y),   closed(Rest).**-----------------310 to 310-------------------------closed([OldBranch | Rest]) :-   member(NotatedEquality, OldBranch),   fmla(NotatedEquality, X eq Y),   member(NotatedLiteral, OldBranch),   notation(NotatedLiteral, RDepth),   RDepth > 0,   fmla(NotatedLiteral, Literal),   replace_literal(X, Literal, Y, NewLiteral),   NewRDepth is RDepth - 1,   fmla(NewNotatedLiteral, NewLiteral),   notation(NewNotatedLiteral, NewRDepth),   fmla(RevisedNotatedLiteral, Literal),   notation(RevisedNotatedLiteral, NewRDepth),   remove(NotatedLiteral, OldBranch, TempBranch),   NewBranch = [NewNotatedLiteral, RevisedNotatedLiteral |     TempBranch],   closed([NewBranch | Rest]).**-----------------310 to 311-------------------------/*   test(X, Qdepth, RDepth) :- create a complete tableau         expansion for neg X, allowing Qdepth applications         of the gamma rule, but no equality rules.  Then         reorganize the tableau and test for closure,         allowing the equality replacement rule to be         used RDepth times on each formula.      Note that this replaces the earlier test predicate.*/test(X, Qdepth, RDepth) :-   reset,   notation(NotatedFormula, [ ]),   fmla(NotatedFormula, neg X),   expand([[NotatedFormula]], Qdepth, Tree), !,   reorganize(Tree, RDepth, NewTree), !,   if_then_else(closed(NewTree),       yes(Qdepth, RDepth), no(Qdepth, RDepth)),   !, fail.yes(Qdepth, RDepth) :-   write('Theorem at Q-depth '),   write(Qdepth),   write(' and R-depth '),   write(RDepth),   write('.'),   nl.no(Qdepth, RDepth) :-   write('Not a theorem at Q-depth '),   write(Qdepth),   write(' and R-depth '),   write(RDepth),   write('.'),   nl.