fof(diet1,conjecture, (~b => f) & ((b & f) => ~i) & ((i | ~b) => ~f) => b ).