2008-05-01T17:11:39-04:00 hates(butler,X1) | ~ killed(X1,agatha) cnf(57,plain, ( hates(butler,X1) | ~ killed(X1,agatha) ), inference(spm,[status(thm)],[36,45])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/DVTPTP2WWW/view_file.pl?Category=Solutions&Domain=PUZ&File=PUZ001+1&System=EP---0.999.THM-CRf.s#57 0