%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM004-1 : TPTP v8.2.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 04:52:42 EDT 2024 % Result : Unsatisfiable 59.70s 59.77s % Output : CNFRefutation 59.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : COM004-1 : TPTP v8.2.0. Released v1.1.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n022.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Fri Jun 21 00:06:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.54/0.57 start to proof:theBenchmark % 59.70/59.76 %------------------------------------------- % 59.70/59.76 % File :CSE---1.7 % 59.70/59.76 % Problem :theBenchmark % 59.70/59.76 % Transform :cnf % 59.70/59.76 % Format :tptp:raw % 59.70/59.76 % Command :java -jar mcs_scs.jar %d %s % 59.70/59.76 % 59.70/59.76 % Result :Theorem 59.150000s % 59.70/59.76 % Output :CNFRefutation 59.150000s % 59.70/59.76 %------------------------------------------- % 59.70/59.76 %-------------------------------------------------------------------------- % 59.70/59.76 % File : COM004-1 : TPTP v8.2.0. Released v1.1.0. % 59.70/59.76 % Domain : Computing Theory % 59.70/59.76 % Problem : Part of completeness of resolution % 59.70/59.76 % Version : Especial. % 59.70/59.76 % English : Part of [Bun83]'s proof of the completeness of resolution uses % 59.70/59.76 % the notion of failure nodes. This proves a special case when a % 59.70/59.76 % parent is the empty failure node. % 59.70/59.76 % 59.70/59.76 % Refs : [Bun83] Bundy (1983), The Computer Modelling of Mathematical R % 59.70/59.76 % Source : [TPTP] % 59.70/59.76 % Names : % 59.70/59.76 % 59.70/59.76 % Status : Unsatisfiable % 59.70/59.76 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v3.3.0, 0.14 v3.1.0, 0.00 v2.0.0 % 59.70/59.76 % Syntax : Number of clauses : 9 ( 8 unt; 0 nHn; 6 RR) % 59.70/59.76 % Number of literals : 13 ( 2 equ; 5 neg) % 59.70/59.76 % Maximal clause size : 5 ( 1 avg) % 59.70/59.76 % Maximal term depth : 3 ( 1 avg) % 59.70/59.76 % Number of predicates : 4 ( 3 usr; 0 prp; 2-2 aty) % 59.70/59.76 % Number of functors : 10 ( 10 usr; 5 con; 0-2 aty) % 59.70/59.76 % Number of variables : 10 ( 1 sgn) % 59.70/59.76 % SPC : CNF_UNS_RFO_SEQ_HRN % 59.70/59.76 % 59.70/59.76 % Comments : % 59.70/59.76 %-------------------------------------------------------------------------- % 59.70/59.76 cnf(make_node,axiom, % 59.70/59.76 ( failure_node(parent_of(X,Y),or(C,D)) % 59.70/59.76 | ~ failure_node(X,or(C,P)) % 59.70/59.76 | ~ failure_node(Y,or(D,Q)) % 59.70/59.76 | ~ contradictory(P,Q) % 59.70/59.76 | ~ siblings(X,Y) ) ). % 59.70/59.76 % 59.70/59.76 cnf(not_x_contradicts_x,axiom, % 59.70/59.76 contradictory(negate(X),X) ). % 59.70/59.76 % 59.70/59.76 cnf(x_contradicts_not_x,axiom, % 59.70/59.76 contradictory(X,negate(X)) ). % 59.70/59.76 % 59.70/59.76 cnf(n_left_and_n_right_are_siblings,axiom, % 59.70/59.76 siblings(left_child_of(X),right_child_of(X)) ). % 59.70/59.76 % 59.70/59.76 %----Stuff for the theorem % 59.70/59.76 cnf(n_left_is_atom,hypothesis, % 59.70/59.76 failure_node(n_left,or(empty,atom)) ). % 59.70/59.76 % 59.70/59.76 cnf(n_right_is_not_atom,hypothesis, % 59.70/59.76 failure_node(n_right,or(empty,negate(atom))) ). % 59.70/59.76 % 59.70/59.76 cnf(n_left_equals_left_child_of_n,hypothesis, % 59.70/59.76 n_left = left_child_of(n) ). % 59.70/59.76 % 59.70/59.76 cnf(n_right_equals_right_child_of_n,hypothesis, % 59.70/59.76 n_right = right_child_of(n) ). % 59.70/59.76 % 59.70/59.76 %----The goal to be proved. % 59.70/59.76 cnf(goal_is_there_an_empty_node,negated_conjecture, % 59.70/59.76 ~ failure_node(Z,or(empty,empty)) ). % 59.70/59.76 % 59.70/59.76 %-------------------------------------------------------------------------- % 59.70/59.77 %------------------------------------------- % 59.70/59.77 % Proof found % 59.70/59.77 % SZS status Theorem for theBenchmark % 59.70/59.77 % SZS output start Proof % 59.76/59.77 %ClaNum:25(EqnAxiom:16) % 59.76/59.77 %VarNum:21(SingletonVarNum:10) % 59.76/59.77 %MaxLitNum:5 % 59.76/59.77 %MaxfuncDepth:2 % 59.76/59.77 %SharedTerms:15 % 59.76/59.77 %goalClause: 24 % 59.76/59.77 %singleGoalClaCount:1 % 59.76/59.77 [17]E(f2(a1),a5) % 59.76/59.77 [18]E(f6(a1),a7) % 59.76/59.77 [22]P3(a5,f9(a3,a4)) % 59.76/59.77 [23]P3(a7,f9(a3,f8(a4))) % 59.76/59.77 [19]P1(x191,f8(x191)) % 59.76/59.77 [20]P1(f8(x201),x201) % 59.76/59.77 [21]P2(f2(x211),f6(x211)) % 59.76/59.77 [24]~P3(x241,f9(a3,a3)) % 59.76/59.77 [25]~P2(x251,x252)+~P1(x255,x256)+~P3(x252,f9(x254,x256))+~P3(x251,f9(x253,x255))+P3(f10(x251,x252),f9(x253,x254)) % 59.76/59.77 %EqnAxiom % 59.76/59.77 [1]E(x11,x11) % 59.76/59.77 [2]E(x22,x21)+~E(x21,x22) % 59.76/59.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.76/59.77 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 59.76/59.77 [5]~E(x51,x52)+E(f6(x51),f6(x52)) % 59.76/59.77 [6]~E(x61,x62)+E(f8(x61),f8(x62)) % 59.76/59.77 [7]~E(x71,x72)+E(f9(x71,x73),f9(x72,x73)) % 59.76/59.77 [8]~E(x81,x82)+E(f9(x83,x81),f9(x83,x82)) % 59.76/59.77 [9]~E(x91,x92)+E(f10(x91,x93),f10(x92,x93)) % 59.76/59.77 [10]~E(x101,x102)+E(f10(x103,x101),f10(x103,x102)) % 59.76/59.77 [11]P1(x112,x113)+~E(x111,x112)+~P1(x111,x113) % 59.76/59.77 [12]P1(x123,x122)+~E(x121,x122)+~P1(x123,x121) % 59.76/59.77 [13]P3(x132,x133)+~E(x131,x132)+~P3(x131,x133) % 59.76/59.77 [14]P3(x143,x142)+~E(x141,x142)+~P3(x143,x141) % 59.76/59.77 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 59.76/59.77 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 59.76/59.77 % 59.76/59.77 %------------------------------------------- % 59.76/59.77 cnf(34,plain, % 59.76/59.77 (P2(a5,f6(a1))), % 59.76/59.77 inference(scs_inference,[],[24,19,20,21,17,22,2,13,11,12,14,15])). % 59.76/59.77 cnf(45,plain, % 59.76/59.77 (P2(a5,a7)), % 59.76/59.77 inference(scs_inference,[],[34,18,2,16])). % 59.76/59.77 cnf(1255,plain, % 59.76/59.77 (E(f10(f2(a1),x12551),f10(a5,x12551))), % 59.76/59.77 inference(scs_inference,[],[17,9])). % 59.76/59.77 cnf(1256,plain, % 59.76/59.77 (E(f10(x12561,f2(a1)),f10(x12561,a5))), % 59.76/59.77 inference(scs_inference,[],[17,9,10])). % 59.76/59.77 cnf(1273,plain, % 59.76/59.77 ($false), % 59.76/59.77 inference(scs_inference,[],[24,1256,1255,45,22,23,19,3,25]), % 59.76/59.77 ['proof']). % 59.76/59.77 % SZS output end Proof % 59.76/59.77 % Total time :59.150000s %------------------------------------------------------------------------------