```    1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2%
3% Copyright 2003,    Renate Schmidt,  University of Manchester
4%  Modified 2009-10, Ullrich Hustadt, University of Liverpool
5%
6% Uses
7%
8%   p, -p
9%   ----- (p must be atomic and X-free)
10%   clash
11%
12%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
13
14:-module(inf_closure,
15    [
16        inf_closure/3,
17	inf_closure/4
18    ]).   19
20:- dynamic
21        inf_closure/3.   22
23
24%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25
26inf_closure(State, not(true), _, Fml) :- !,
27    set_satisfiable_flag(0),
28    store_inconsistent(Fml),
29    pdl_write(State), pdl_write(' ** Unsatisfiable [not(true)] ** '), pdl_write(not(true)), pdl_nl,
30    print_proof_step(State, '** Unsatisfiable **', ['clash',not(true)]),
31    fail.
32
33% Definitions 7 and 23 in (De Giacomo and Massacci, 2000) give different
34% conditions for the simplest form of an inconsistency: Definition 7 only
35% recognises an inconsistency between A and not(A) where A is atomic,
36% while Definition 23 recognises an inconsistency between F and not(F) where
37% F can be an arbitrary formula. However, using Definition 23, gives incorrect
38% results for some formulae. Therefore, we only use Definition 7.
39inf_closure(State, not(A), [A|_], Fml) :-
40    atomic(A),
41    !,
42    set_satisfiable_flag(0),
43    store_inconsistent(Fml),
44    pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl,
45    print_proof_step(State, '** Unsatisfiable **', ['clash',not(A),A]),
46    fail.
47
48inf_closure(State, A, [not(A)|_], Fml) :-
49    atomic(A),
50    !,
51    set_satisfiable_flag(0),
52    store_inconsistent(Fml),
53    pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl,
54    print_proof_step(State, '** Unsatisfiable **', ['clash',A,not(A)]),
55    fail.
56
57inf_closure(_, _, [], _) :- !.
58
59inf_closure(State, Term, [_|Set], Fml) :- !,
60    inf_closure(State, Term, Set, Fml)```