%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ001-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 13:41:59 EDT 2024 % Result : Unsatisfiable 0.59s 0.65s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PUZ001-1 : TPTP v8.2.0. Released v1.0.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.32 % Computer : n003.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Tue Jun 18 10:14:08 EDT 2024 % 0.13/0.33 % CPUTime : % 0.49/0.59 start to proof:theBenchmark % 0.59/0.64 %------------------------------------------- % 0.59/0.64 % File :CSE---1.7 % 0.59/0.64 % Problem :theBenchmark % 0.59/0.64 % Transform :cnf % 0.59/0.64 % Format :tptp:raw % 0.59/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.64 % 0.59/0.64 % Result :Theorem 0.010000s % 0.59/0.64 % Output :CNFRefutation 0.010000s % 0.59/0.64 %------------------------------------------- % 0.59/0.64 %------------------------------------------------------------------------------ % 0.59/0.64 % File : PUZ001-1 : TPTP v8.2.0. Released v1.0.0. % 0.59/0.64 % Domain : Puzzles % 0.59/0.64 % Problem : Dreadbury Mansion % 0.59/0.64 % Version : Especial. % 0.59/0.64 % Theorem formulation : Made unsatisfiable. % 0.59/0.64 % English : Someone who lives in Dreadbury Mansion killed Aunt Agatha. % 0.59/0.64 % Agatha, the butler, and Charles live in Dreadbury Mansion, % 0.59/0.64 % and are the only people who live therein. A killer always % 0.59/0.64 % hates his victim, and is never richer than his victim. % 0.59/0.64 % Charles hates no one that Aunt Agatha hates. Agatha hates % 0.59/0.64 % everyone except the butler. The butler hates everyone not % 0.59/0.64 % richer than Aunt Agatha. The butler hates everyone Aunt % 0.59/0.64 % Agatha hates. No one hates everyone. Agatha is not the % 0.59/0.64 % butler. Therefore : Agatha killed herself. % 0.59/0.64 % 0.59/0.64 % Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 0.59/0.64 % : [MB88] Manthey & Bry (1988), SATCHMO: A Theorem Prover Implem % 0.59/0.64 % Source : [TPTP] % 0.59/0.64 % Names : % 0.59/0.64 % 0.59/0.64 % Status : Unsatisfiable % 0.59/0.64 % Rating : 0.00 v2.0.0 % 0.59/0.64 % Syntax : Number of clauses : 12 ( 5 unt; 2 nHn; 12 RR) % 0.59/0.64 % Number of literals : 21 ( 0 equ; 10 neg) % 0.59/0.64 % Maximal clause size : 3 ( 1 avg) % 0.59/0.64 % Maximal term depth : 1 ( 1 avg) % 0.59/0.64 % Number of predicates : 4 ( 4 usr; 0 prp; 1-2 aty) % 0.59/0.64 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 0.59/0.64 % Number of variables : 8 ( 0 sgn) % 0.59/0.64 % SPC : CNF_UNS_EPR_NEQ_NHN % 0.59/0.64 % 0.59/0.64 % Comments : Modified from the [MB88] version to be unsatisfiable, by Geoff % 0.59/0.64 % Sutcliffe. % 0.59/0.64 % : Also known as "Who killed Aunt Agatha" % 0.59/0.64 %------------------------------------------------------------------------------ % 0.59/0.64 cnf(agatha,hypothesis, % 0.59/0.64 lives(agatha) ). % 0.59/0.64 % 0.59/0.64 cnf(butler,hypothesis, % 0.59/0.64 lives(butler) ). % 0.59/0.64 % 0.59/0.64 cnf(charles,hypothesis, % 0.59/0.64 lives(charles) ). % 0.59/0.64 % 0.59/0.64 cnf(poorer_killer,hypothesis, % 0.59/0.64 ( ~ killed(X,Y) % 0.59/0.64 | ~ richer(X,Y) ) ). % 0.59/0.64 % 0.59/0.64 cnf(different_hates,hypothesis, % 0.59/0.65 ( ~ hates(agatha,X) % 0.59/0.65 | ~ hates(charles,X) ) ). % 0.59/0.65 % 0.59/0.65 cnf(no_one_hates_everyone,hypothesis, % 0.59/0.65 ( ~ hates(X,agatha) % 0.59/0.65 | ~ hates(X,butler) % 0.59/0.65 | ~ hates(X,charles) ) ). % 0.59/0.65 % 0.59/0.65 cnf(agatha_hates_agatha,hypothesis, % 0.59/0.65 hates(agatha,agatha) ). % 0.59/0.65 % 0.59/0.65 cnf(agatha_hates_charles,hypothesis, % 0.59/0.65 hates(agatha,charles) ). % 0.59/0.65 % 0.59/0.65 cnf(killer_hates_victim,hypothesis, % 0.59/0.65 ( ~ killed(X,Y) % 0.59/0.65 | hates(X,Y) ) ). % 0.59/0.65 % 0.59/0.65 cnf(same_hates,hypothesis, % 0.59/0.65 ( ~ hates(agatha,X) % 0.59/0.65 | hates(butler,X) ) ). % 0.59/0.65 % 0.59/0.65 cnf(butler_hates_poor,hypothesis, % 0.59/0.65 ( ~ lives(X) % 0.59/0.65 | richer(X,agatha) % 0.59/0.65 | hates(butler,X) ) ). % 0.59/0.65 % 0.59/0.65 %----Literal dropped from here to make it unsatisfiable % 0.59/0.65 cnf(prove_neither_charles_nor_butler_did_it,negated_conjecture, % 0.59/0.65 ( killed(butler,agatha) % 0.59/0.65 | killed(charles,agatha) ) ). % 0.59/0.65 % 0.59/0.65 %------------------------------------------------------------------------------ % 0.59/0.65 %------------------------------------------- % 0.59/0.65 % Proof found % 0.59/0.65 % SZS status Theorem for theBenchmark % 0.59/0.65 % SZS output start Proof % 0.59/0.65 %ClaNum:12(EqnAxiom:0) % 0.59/0.65 %VarNum:18(SingletonVarNum:8) % 0.59/0.65 %MaxLitNum:3 % 0.59/0.65 %MaxfuncDepth:0 % 0.59/0.65 %SharedTerms:10 % 0.59/0.65 %goalClause: 6 % 0.59/0.65 [1]P1(a1) % 0.59/0.65 [2]P1(a2) % 0.59/0.65 [3]P1(a3) % 0.59/0.65 [4]P2(a1,a1) % 0.59/0.65 [5]P2(a1,a3) % 0.59/0.65 [6]P3(a2,a1)+P3(a3,a1) % 0.59/0.65 [8]~P2(a1,x81)+P2(a2,x81) % 0.59/0.65 [10]~P2(a3,x101)+~P2(a1,x101) % 0.59/0.65 [9]~P3(x91,x92)+P2(x91,x92) % 0.59/0.65 [11]~P4(x111,x112)+~P3(x111,x112) % 0.59/0.65 [7]~P1(x71)+P2(a2,x71)+P4(x71,a1) % 0.59/0.65 [12]~P2(x121,a2)+~P2(x121,a3)+~P2(x121,a1) % 0.59/0.65 %EqnAxiom % 0.59/0.65 % 0.59/0.65 %------------------------------------------- % 0.59/0.65 cnf(17,plain, % 0.59/0.65 (~P3(a3,a1)), % 0.59/0.65 inference(scs_inference,[],[4,5,10,12,9])). % 0.59/0.65 cnf(19,plain, % 0.59/0.65 (P3(a2,a1)), % 0.59/0.65 inference(scs_inference,[],[17,6])). % 0.59/0.65 cnf(24,plain, % 0.59/0.65 (~P4(a2,a1)), % 0.59/0.65 inference(scs_inference,[],[19,11])). % 0.59/0.65 cnf(52,plain, % 0.59/0.65 (~P2(a2,a1)+~P2(a2,a2)), % 0.59/0.65 inference(scs_inference,[],[5,8,12])). % 0.59/0.65 cnf(83,plain, % 0.59/0.65 (~P2(a2,a2)), % 0.59/0.65 inference(scs_inference,[],[19,52,9])). % 0.59/0.65 cnf(86,plain, % 0.59/0.65 ($false), % 0.59/0.65 inference(scs_inference,[],[24,83,2,9,7]), % 0.59/0.65 ['proof']). % 0.59/0.65 % SZS output end Proof % 0.59/0.65 % Total time :0.010000s %------------------------------------------------------------------------------