Example resolution proof tree.

Constructing interpolants for this case.

Continuation of correctness proof for interpolant construction from resolution proof trees: the 'ite' and the 'and' case.

Running DPLL on the example.

Playing with Alloy.