%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ012-1 : TPTP v8.2.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:03 EDT 2024 % Result : Unsatisfiable 58.52s 59.18s % Output : CNFRefutation 59.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : PUZ012-1 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.06/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.34 % Computer : n022.cluster.edu % 0.11/0.34 % Model : x86_64 x86_64 % 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.34 % Memory : 8042.1875MB % 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.34 % CPULimit : 300 % 0.11/0.34 % WCLimit : 300 % 0.11/0.34 % DateTime : Tue Jun 18 10:56:38 EDT 2024 % 0.11/0.34 % CPUTime : % 0.52/0.59 start to proof:theBenchmark % 58.52/59.15 %------------------------------------------- % 58.52/59.15 % File :CSE---1.7 % 58.52/59.15 % Problem :theBenchmark % 58.52/59.15 % Transform :cnf % 58.52/59.15 % Format :tptp:raw % 58.52/59.15 % Command :java -jar mcs_scs.jar %d %s % 58.52/59.15 % 58.52/59.15 % Result :Theorem 58.000000s % 58.52/59.15 % Output :CNFRefutation 58.000000s % 58.52/59.15 %------------------------------------------- % 58.52/59.18 %-------------------------------------------------------------------------- % 58.52/59.18 % File : PUZ012-1 : TPTP v8.2.0. Bugfixed v1.2.1. % 58.52/59.18 % Domain : Puzzles % 58.52/59.18 % Problem : The Mislabeled Boxes % 58.52/59.18 % Version : Especial. % 58.52/59.18 % English : There are three boxes a, b, and c on a table. Each box contains % 58.52/59.18 % apples or bananas or oranges. No two boxes contain the same % 58.52/59.18 % thing. Each box has a label that says it contains apples or says % 58.52/59.18 % it contains bananas or says it contains oranges. No box contains % 58.52/59.18 % what it says on its label. The label on box a says "apples". % 58.52/59.18 % The label on box b says "oranges". The label on box c says % 58.52/59.18 % "bananas". You pick up box b and it contains apples. What do % 58.52/59.18 % the other two boxes contain? % 58.52/59.18 % 58.52/59.18 % Refs : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a % 58.52/59.18 % : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr % 58.52/59.18 % Source : [ANL] % 58.52/59.18 % Names : Boxes-of-fruit [WO+92] % 58.52/59.18 % : Boxes-of-fruit [Wos88] % 58.52/59.18 % : boxes.ver1.in [ANL] % 58.52/59.18 % 58.52/59.18 % Status : Unsatisfiable % 58.52/59.18 % Rating : 0.00 v2.0.0 % 58.52/59.18 % Syntax : Number of clauses : 18 ( 12 unt; 2 nHn; 14 RR) % 58.52/59.18 % Number of literals : 28 ( 0 equ; 14 neg) % 58.52/59.18 % Maximal clause size : 3 ( 1 avg) % 58.52/59.18 % Maximal term depth : 1 ( 1 avg) % 58.52/59.18 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty) % 58.52/59.18 % Number of functors : 6 ( 6 usr; 6 con; 0-0 aty) % 58.52/59.18 % Number of variables : 12 ( 0 sgn) % 58.52/59.18 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.52/59.18 % 58.52/59.18 % Comments : % 58.52/59.18 % Bugfixes : v1.2.1 - Theorem clause uncommented (commented out during some % 58.52/59.18 % local testing, and forgot to uncomment it again). % 58.52/59.18 %-------------------------------------------------------------------------- % 58.52/59.18 cnf(reflexivity_for_fruits,axiom, % 58.52/59.18 equal_fruits(X,X) ). % 58.52/59.18 % 58.52/59.18 cnf(reflexivity_for_boxes,axiom, % 58.52/59.18 equal_boxes(X,X) ). % 58.52/59.18 % 58.52/59.18 cnf(label_is_wrong,axiom, % 58.52/59.18 ( ~ label(X,Y) % 58.52/59.18 | ~ contains(X,Y) ) ). % 58.52/59.18 % 58.52/59.18 cnf(each_thing_is_in_a_box,axiom, % 58.52/59.18 ( contains(boxa,X) % 58.52/59.18 | contains(boxb,X) % 58.52/59.18 | contains(boxc,X) ) ). % 58.52/59.18 % 58.52/59.18 cnf(each_box_contains_something,axiom, % 58.52/59.18 ( contains(X,apples) % 58.52/59.18 | contains(X,bananas) % 58.52/59.18 | contains(X,oranges) ) ). % 58.52/59.18 % 58.52/59.18 cnf(contains_is_well_defined1,axiom, % 58.52/59.18 ( ~ contains(X,Y) % 58.52/59.18 | ~ contains(X,Z) % 58.52/59.18 | equal_fruits(Y,Z) ) ). % 58.52/59.18 % 58.52/59.18 cnf(contains_is_well_defined2,axiom, % 58.52/59.18 ( ~ contains(X,Y) % 58.52/59.18 | ~ contains(Z,Y) % 58.52/59.18 | equal_boxes(X,Z) ) ). % 58.52/59.18 % 58.52/59.18 cnf(boxa_not_boxb,axiom, % 58.52/59.18 ~ equal_boxes(boxa,boxb) ). % 58.52/59.18 % 58.52/59.18 cnf(boxb_not_boxc,axiom, % 58.52/59.18 ~ equal_boxes(boxb,boxc) ). % 58.52/59.18 % 58.52/59.18 cnf(boxa_not_boxc,axiom, % 58.52/59.18 ~ equal_boxes(boxa,boxc) ). % 58.52/59.18 % 58.52/59.18 cnf(apples_not_bananas,axiom, % 58.52/59.18 ~ equal_fruits(apples,bananas) ). % 58.52/59.18 % 58.52/59.18 cnf(bananas_not_oranges,axiom, % 58.52/59.18 ~ equal_fruits(bananas,oranges) ). % 58.52/59.18 % 58.52/59.18 cnf(apples_not_oranges,axiom, % 58.52/59.18 ~ equal_fruits(apples,oranges) ). % 58.52/59.18 % 58.52/59.18 cnf(boxa_labelled_apples,hypothesis, % 58.52/59.18 label(boxa,apples) ). % 58.52/59.18 % 58.52/59.18 cnf(boxb_labelled_oranges,hypothesis, % 58.52/59.18 label(boxb,oranges) ). % 58.52/59.18 % 58.52/59.18 cnf(boxc_labelled_bananas,hypothesis, % 58.52/59.18 label(boxc,bananas) ). % 58.52/59.18 % 58.52/59.18 cnf(boxb_contains_apples,hypothesis, % 58.52/59.18 contains(boxb,apples) ). % 58.52/59.18 % 58.52/59.18 cnf(prove_boxa_contains_bananas_and_boxc_oranges,negated_conjecture, % 58.52/59.18 ( ~ contains(boxa,bananas) % 58.52/59.18 | ~ contains(boxc,oranges) ) ). % 58.52/59.18 % 58.52/59.18 %-------------------------------------------------------------------------- % 58.52/59.18 %------------------------------------------- % 58.52/59.18 % Proof found % 58.52/59.18 % SZS status Theorem for theBenchmark % 58.52/59.18 % SZS output start Proof % 58.52/59.21 %ClaNum:18(EqnAxiom:0) % 58.52/59.21 %VarNum:26(SingletonVarNum:12) % 58.52/59.21 %MaxLitNum:3 % 58.52/59.21 %MaxfuncDepth:0 % 58.52/59.21 %SharedTerms:18 % 58.52/59.21 %goalClause: 13 % 58.52/59.21 [1]P1(a1,a2) % 58.52/59.21 [2]P1(a4,a5) % 58.52/59.21 [3]P1(a6,a3) % 58.52/59.21 [4]P2(a4,a2) % 58.52/59.21 [7]~P3(a2,a3) % 58.52/59.21 [8]~P3(a2,a5) % 58.52/59.21 [9]~P3(a3,a5) % 58.52/59.21 [10]~P4(a1,a4) % 58.52/59.21 [11]~P4(a1,a6) % 58.52/59.21 [12]~P4(a4,a6) % 58.52/59.21 [5]P3(x51,x51) % 58.52/59.21 [6]P4(x61,x61) % 58.52/59.21 [13]~P2(a1,a3)+~P2(a6,a5) % 58.52/59.21 [16]~P2(x161,x162)+~P1(x161,x162) % 58.52/59.21 [14]P2(x141,a3)+P2(x141,a5)+P2(x141,a2) % 58.52/59.21 [15]P2(a4,x151)+P2(a6,x151)+P2(a1,x151) % 58.52/59.21 [17]~P2(x173,x171)+P3(x171,x172)+~P2(x173,x172) % 58.52/59.21 [18]~P2(x181,x183)+P4(x181,x182)+~P2(x182,x183) % 58.52/59.21 %EqnAxiom % 58.52/59.21 % 58.52/59.21 %------------------------------------------- % 59.05/59.68 cnf(37,plain, % 59.05/59.68 (P2(a1,a3)+P2(a4,a3)), % 59.05/59.68 inference(scs_inference,[],[3,4,16,17,18,15])). % 59.05/59.69 cnf(39,plain, % 59.05/59.69 (P2(a4,a3)+~P2(a6,a5)), % 59.05/59.69 inference(scs_inference,[],[3,4,16,17,18,15,13])). % 59.05/59.69 cnf(40,plain, % 59.05/59.69 (P2(a6,a2)+P2(a4,a3)), % 59.05/59.69 inference(scs_inference,[],[3,4,16,17,18,15,13,14])). % 59.05/59.69 cnf(377456,plain, % 59.05/59.69 ($false), % 59.05/59.69 inference(scs_inference,[],[7,12,4,17,18,37,39,40]), % 59.05/59.69 ['proof']). % 59.35/59.95 % SZS output end Proof % 59.35/59.95 % Total time :58.000000s %------------------------------------------------------------------------------