show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound

fix remote Vampire diagnosis

make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases; some of these aliases pop up only after Sledgehammer has converted the formula to CNF, so it can be very confusing to the user who said "add: foo del: bar" that "bar" is used in the end.