fof( resolution, conjecture, ((a | b) & (~a | c)) => (b | c) ).