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