%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ020-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n013.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:42:05 EDT 2024 % Result : Unsatisfiable 0.19s 0.59s % Output : CNFRefutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ020-1 : TPTP v8.2.0. Released v1.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 10:40:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 0.19/0.58 %------------------------------------------- % 0.19/0.58 % File :CSE---1.7 % 0.19/0.58 % Problem :theBenchmark % 0.19/0.58 % Transform :cnf % 0.19/0.58 % Format :tptp:raw % 0.19/0.58 % Command :java -jar mcs_scs.jar %d %s % 0.19/0.58 % 0.19/0.58 % Result :Theorem 0.000000s % 0.19/0.58 % Output :CNFRefutation 0.000000s % 0.19/0.58 %------------------------------------------- % 0.19/0.59 %-------------------------------------------------------------------------- % 0.19/0.59 % File : PUZ020-1 : TPTP v8.2.0. Released v1.0.0. % 0.19/0.59 % Domain : Puzzles % 0.19/0.59 % Problem : A knights & knaves problem, if he's a knight, so is she % 0.19/0.59 % Version : Especial. % 0.19/0.59 % English : % 0.19/0.59 % 0.19/0.59 % Refs : [Rap95] Raptis (1995), Email to G. Sutcliffe % 0.19/0.59 % Source : [ANL] % 0.19/0.59 % Names : knightknave.in [ANL] % 0.19/0.59 % 0.19/0.59 % Status : Unsatisfiable % 0.19/0.59 % Rating : 0.05 v8.1.0, 0.00 v5.3.0, 0.06 v5.2.0, 0.00 v2.0.0 % 0.19/0.59 % Syntax : Number of clauses : 19 ( 5 unt; 3 nHn; 19 RR) % 0.19/0.59 % Number of literals : 41 ( 4 equ; 25 neg) % 0.19/0.59 % Maximal clause size : 3 ( 2 avg) % 0.19/0.59 % Maximal term depth : 2 ( 1 avg) % 0.19/0.59 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 0.19/0.59 % Number of functors : 3 ( 3 usr; 2 con; 0-1 aty) % 0.19/0.59 % Number of variables : 16 ( 2 sgn) % 0.19/0.59 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.19/0.59 % 0.19/0.59 % Comments : Dimitris Raptis [Rap95] has pointed out that the clause % 0.19/0.59 % statements_are_true_or_not is a tautology. Does your ATP system % 0.19/0.59 % ignore it? % 0.19/0.59 %-------------------------------------------------------------------------- % 0.19/0.59 %----This axiom is omitted in the orginal, because of paramodulation % 0.19/0.59 %----Everyone's either a knight or a knave; statements are true or false. % 0.19/0.59 cnf(everyone_a_knight_or_knave,axiom, % 0.19/0.59 ( ~ person(X) % 0.19/0.59 | knight(X) % 0.19/0.59 | knave(X) ) ). % 0.19/0.59 % 0.19/0.59 cnf(not_both_a_knight_and_knave,axiom, % 0.19/0.59 ( ~ person(X) % 0.19/0.59 | ~ knight(X) % 0.19/0.59 | ~ knave(X) ) ). % 0.19/0.59 % 0.19/0.59 cnf(statements_are_true_or_false,axiom, % 0.19/0.59 ( ~ says(X,Y) % 0.19/0.59 | a_truth(Y) % 0.19/0.59 | ~ a_truth(Y) ) ). % 0.19/0.59 % 0.19/0.59 %----Rules about statements % 0.19/0.59 cnf(people_do_not_equal_their_statements1,axiom, % 0.19/0.59 ( ~ says(X,Y) % 0.19/0.59 | X != Y ) ). % 0.19/0.59 % 0.19/0.59 cnf(peoples_statements,axiom, % 0.19/0.59 ( ~ says(X,Y) % 0.19/0.59 | Y = statement_by(X) ) ). % 0.19/0.59 % 0.19/0.59 cnf(people_do_not_equal_their_statement2,axiom, % 0.19/0.59 ( ~ person(X) % 0.19/0.59 | X != statement_by(Y) ) ). % 0.19/0.59 % 0.19/0.59 cnf(knights_make_true_statements,axiom, % 0.19/0.59 ( ~ person(X) % 0.19/0.59 | ~ a_truth(statement_by(X)) % 0.19/0.59 | knight(X) ) ). % 0.19/0.59 % 0.19/0.59 cnf(knaves_make_false_statements,axiom, % 0.19/0.59 ( ~ person(X) % 0.19/0.59 | a_truth(statement_by(X)) % 0.19/0.59 | knave(X) ) ). % 0.19/0.59 % 0.19/0.59 %----What knights say is true, what knaves say is false % 0.19/0.59 cnf(knights_say_the_truth,axiom, % 0.19/0.59 ( ~ knight(X) % 0.19/0.59 | ~ says(X,Y) % 0.19/0.59 | a_truth(Y) ) ). % 0.19/0.59 % 0.19/0.59 cnf(knaves_do_not_say_the_truth,axiom, % 0.19/0.59 ( ~ knave(X) % 0.19/0.59 | ~ says(X,Y) % 0.19/0.59 | ~ a_truth(Y) ) ). % 0.19/0.59 % 0.19/0.59 %----This is for the husband & wife problem; if he's a knight, then she % 0.19/0.59 %----is % 0.19/0.59 cnf(husband,hypothesis, % 0.19/0.59 person(husband) ). % 0.19/0.59 % 0.19/0.59 cnf(wife,hypothesis, % 0.19/0.59 person(wife) ). % 0.19/0.59 % 0.19/0.59 cnf(husband_not_wife,hypothesis, % 0.19/0.59 husband != wife ). % 0.19/0.59 % 0.19/0.59 cnf(husband_makes_statements,hypothesis, % 0.19/0.59 says(husband,statement_by(husband)) ). % 0.19/0.59 % 0.19/0.59 cnf(truthful_knight_husband_means_knight_wife,hypothesis, % 0.19/0.59 ( ~ a_truth(statement_by(husband)) % 0.19/0.59 | ~ knight(husband) % 0.19/0.59 | knight(wife) ) ). % 0.19/0.59 % 0.19/0.59 cnf(knight_husband_makes_true_statements,hypothesis, % 0.19/0.59 ( a_truth(statement_by(husband)) % 0.19/0.59 | ~ knight(husband) ) ). % 0.19/0.59 % 0.19/0.59 cnf(knight_wife_or_truthful_husband,hypothesis, % 0.19/0.59 ( a_truth(statement_by(husband)) % 0.19/0.59 | knight(wife) ) ). % 0.19/0.59 % 0.19/0.59 cnf(knight_wife_means_truthful_husband,hypothesis, % 0.19/0.59 ( ~ knight(wife) % 0.19/0.59 | a_truth(statement_by(husband)) ) ). % 0.19/0.59 % 0.19/0.59 cnf(prove_knight_husband,negated_conjecture, % 0.19/0.59 ~ knight(husband) ). % 0.19/0.59 % 0.19/0.59 %-------------------------------------------------------------------------- % 0.19/0.59 %------------------------------------------- % 0.19/0.59 % Proof found % 0.19/0.59 % SZS status Theorem for theBenchmark % 0.19/0.59 % SZS output start Proof % 0.19/0.59 %ClaNum:28(EqnAxiom:10) % 0.19/0.59 %VarNum:31(SingletonVarNum:14) % 0.19/0.59 %MaxLitNum:3 % 0.19/0.59 %MaxfuncDepth:1 % 0.19/0.59 %SharedTerms:12 % 0.19/0.59 %goalClause: 15 % 0.19/0.59 %singleGoalClaCount:1 % 0.19/0.59 [11]P1(a1) % 0.19/0.59 [12]P1(a2) % 0.19/0.59 [14]~E(a1,a2) % 0.19/0.59 [15]~P2(a1) % 0.19/0.59 [13]P5(a1,f3(a1)) % 0.19/0.59 [16]P2(a2)+P3(f3(a1)) % 0.19/0.59 [18]~P2(a2)+P3(f3(a1)) % 0.19/0.59 [24]~P5(x241,x242)+~E(x241,x242) % 0.19/0.59 [19]~P1(x191)+~E(x191,f3(x192)) % 0.19/0.59 [25]~P5(x252,x251)+E(x251,f3(x252)) % 0.19/0.59 [20]P4(x201)+~P1(x201)+P2(x201) % 0.19/0.59 [22]~P2(x221)+~P4(x221)+~P1(x221) % 0.19/0.59 [23]~P1(x231)+P4(x231)+P3(f3(x231)) % 0.19/0.59 [26]~P1(x261)+P2(x261)+~P3(f3(x261)) % 0.19/0.59 [27]~P5(x272,x271)+P3(x271)+~P2(x272) % 0.19/0.59 [28]~P5(x281,x282)+~P4(x281)+~P3(x282) % 0.19/0.59 %EqnAxiom % 0.19/0.59 [1]E(x11,x11) % 0.19/0.59 [2]E(x22,x21)+~E(x21,x22) % 0.19/0.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.19/0.59 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.19/0.59 [5]~P1(x51)+P1(x52)+~E(x51,x52) % 0.19/0.59 [6]P5(x62,x63)+~E(x61,x62)+~P5(x61,x63) % 0.19/0.59 [7]P5(x73,x72)+~E(x71,x72)+~P5(x73,x71) % 0.19/0.59 [8]~P3(x81)+P3(x82)+~E(x81,x82) % 0.19/0.59 [9]~P2(x91)+P2(x92)+~E(x91,x92) % 0.19/0.59 [10]~P4(x101)+P4(x102)+~E(x101,x102) % 0.19/0.59 % 0.19/0.59 %------------------------------------------- % 0.19/0.59 cnf(30,plain, % 0.19/0.59 (~P5(x301,x301)), % 0.19/0.59 inference(equality_inference,[],[24])). % 0.19/0.59 cnf(36,plain, % 0.19/0.59 (~P5(x361,x361)), % 0.19/0.59 inference(rename_variables,[],[30])). % 0.19/0.59 cnf(40,plain, % 0.19/0.59 ($false), % 0.19/0.59 inference(scs_inference,[],[15,11,30,36,13,20,28,6,7,16,18]), % 0.19/0.59 ['proof']). % 0.19/0.59 % SZS output end Proof % 0.19/0.59 % Total time :0.000000s %------------------------------------------------------------------------------