%------------------------------------------------------------------------------ % File : PUZ001-1 : TPTP v3.3.0. Released v1.0.0. % Domain : Puzzles % Problem : Dreadbury Mansion % Version : Especial. % Theorem formulation : Made unsatisfiable. % English : Someone who lives in Dreadbury Mansion killed Aunt Agatha. % Agatha, the butler, and Charles live in Dreadbury Mansion, % and are the only people who live therein. A killer always % hates his victim, and is never richer than his victim. % Charles hates no one that Aunt Agatha hates. Agatha hates % everyone except the butler. The butler hates everyone not % richer than Aunt Agatha. The butler hates everyone Aunt % Agatha hates. No one hates everyone. Agatha is not the % butler. Therefore : Agatha killed herself. % Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % : [MB88] Manthey & Bry (1988), SATCHMO: A Theorem Prover Implem % Source : [TPTP] % Names : % Status : Unsatisfiable % Rating : 0.00 v2.0.0 % Syntax : Number of clauses : 12 ( 2 non-Horn; 5 unit; 12 RR) % Number of atoms : 21 ( 0 equality) % Maximal clause size : 3 ( 2 average) % Number of predicates : 4 ( 0 propositional; 1-2 arity) % Number of functors : 3 ( 3 constant; 0-0 arity) % Number of variables : 8 ( 0 singleton) % Maximal term depth : 1 ( 1 average) % Comments : Modified from the [MB88] version to be unsatisfiable, by Geoff % Sutcliffe. % : Also known as "Who killed Aunt Agatha" % : tptp2X -f tptp:short PUZ001-1.p %------------------------------------------------------------------------------ cnf(agatha,hypothesis,( lives(agatha) )). cnf(butler,hypothesis,( lives(butler) )). cnf(charles,hypothesis,( lives(charles) )). cnf(poorer_killer,hypothesis, ( ~ killed(X,Y) | ~ richer(X,Y) )). cnf(different_hates,hypothesis, ( ~ hates(agatha,X) | ~ hates(charles,X) )). cnf(no_one_hates_everyone,hypothesis, ( ~ hates(X,agatha) | ~ hates(X,butler) | ~ hates(X,charles) )). cnf(agatha_hates_agatha,hypothesis,( hates(agatha,agatha) )). cnf(agatha_hates_charles,hypothesis,( hates(agatha,charles) )). cnf(killer_hates_victim,hypothesis, ( ~ killed(X,Y) | hates(X,Y) )). cnf(same_hates,hypothesis, ( ~ hates(agatha,X) | hates(butler,X) )). cnf(butler_hates_poor,hypothesis, ( ~ lives(X) | richer(X,agatha) | hates(butler,X) )). cnf(prove_neither_charles_nor_butler_did_it,negated_conjecture, ( killed(butler,agatha) | killed(charles,agatha) )). %------------------------------------------------------------------------------