DDB (Simplified Version)
When a contradiction is asserted (i.e., two nodes currently IN, say A and B, are discovered to be contradictory) a CONTRADICTION node marked IN is inserted:
Ni CONTRAD. (SL (A, B) ( )).
Starting from the IN-list of the SL justification of the contradiction node, the assumption which led to the contradiction is identified. Let's suppose that this assumption is A. This is recorded by means of a new node:
Nj NOGOOD A (CP Ni (A, B) ( ))
The assumption is then disbelieved. If the situation before the contradiction was:
A ........ (SL ( ) (X)) IN
then node X is made IN and justified with
X ........ (SL (Nj) ( )) IN,
which makes OUT the node A and all its consequences.