(load "infix")
(load "unify")
(load "cnf")
(load "prover")