Consider the following FOL problem. { . (require() require(depend())) depend(clang)=llvm depend(llvm)=libc require(clang) } |= require(libc) Translate the problem to TPTP and use Vampire to obtain 3 different proofs which satisfy the following criteria: 1 proof should be done with the equality proxy as set for run_vampire, and 1 proof should not use an equality proxy 1 proof should be done with ordered resolution as set for run_vampire, and 1 proof should use unordered resolution