TPTP にはまってしまった。