https://web.sfc.keio.ac.jp/~hagino/logic16/11.pdf
refutation
導出を用いた背理法証明
Selective Linear resolution for Definite clause