1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%
    3% Copyright 2003, Renate Schmidt, University of Manchester
    4%
    5%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    6
    7:-module(inf_closure, 
    8    [
    9        inf_closure/3
   10    ]).   11
   12:- dynamic
   13        inf_closure/3.   14
   15%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   16
   17inf_closure(State, not(true), _) :- !,
   18    set_satisfiable_flag(0),
   19    pdl_write(State), pdl_write(' ** Unsatisfiable [not(true)] ** '), pdl_write(not(true)), pdl_nl,
   20    print_proof_step(State, '** Unsatisfiable **', ['clash',not(true)]), 
   21    fail.
   22
   23inf_closure(State, not(A), [A|_]) :- !,
   24    set_satisfiable_flag(0),
   25    pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl,
   26    print_proof_step(State, '** Unsatisfiable **', ['clash',not(A),A]), 
   27    fail.
   28
   29inf_closure(State, A, [not(A)|_]) :- !,
   30    set_satisfiable_flag(0),
   31    pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(A), pdl_write(' - '), pdl_write(not(A)), pdl_nl,
   32    print_proof_step(State, '** Unsatisfiable **', ['clash',A,not(A)]), 
   33    fail.
   34
   35inf_closure(State, x(Y,A), [not(A)|_]) :- !,
   36    set_satisfiable_flag(0),
   37    pdl_write(State), pdl_write(' ** Unsatisfiable [x(Y,A)-not(A)] ** '), pdl_write(x(Y,A)), pdl_write(' - '), pdl_write(not(A)), pdl_nl,
   38    print_proof_step(State, '** Unsatisfiable **', ['clash',x(Y,A),not(A)]), 
   39    fail.
   40
   41inf_closure(_, _, []) :- !.

inf_closure(State, x(_,_), _) :- !. inf_closure(State, not(x(_,_)), _) :- !.

   47inf_closure(State, Term, [_|Set]) :- !,
   48    inf_closure(State, Term, Set).
   49
   50
   51%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%