%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN558-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n026.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 19:05:58 EDT 2024 % Result : Unsatisfiable 4.84s 4.90s % Output : CNFRefutation 4.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN558-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.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 : Sun Jun 23 18:21:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.48/0.58 start to proof:theBenchmark % 4.84/4.90 %------------------------------------------- % 4.84/4.90 % File :CSE---1.7 % 4.84/4.90 % Problem :theBenchmark % 4.84/4.90 % Transform :cnf % 4.84/4.90 % Format :tptp:raw % 4.84/4.90 % Command :java -jar mcs_scs.jar %d %s % 4.84/4.90 % 4.84/4.90 % Result :Theorem 4.260000s % 4.84/4.90 % Output :CNFRefutation 4.260000s % 4.84/4.90 %------------------------------------------- % 4.84/4.90 %-------------------------------------------------------------------------- % 4.84/4.90 % File : SYN558-1 : TPTP v8.2.0. Released v2.5.0. % 4.84/4.90 % Domain : Syntactic % 4.84/4.90 % Problem : Harrison problem 2379 % 4.84/4.90 % Version : Especial. % 4.84/4.90 % English : % 4.84/4.90 % 4.84/4.90 % Refs : [Har01] Email to G. Sutcliffe % 4.84/4.90 % Source : [Har01] % 4.84/4.90 % Names : % 4.84/4.90 % 4.84/4.90 % Status : Unsatisfiable % 4.84/4.90 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.5.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v2.5.0 % 4.84/4.90 % Syntax : Number of clauses : 14 ( 6 unt; 0 nHn; 10 RR) % 4.84/4.90 % Number of literals : 33 ( 0 equ; 20 neg) % 4.84/4.90 % Maximal clause size : 5 ( 2 avg) % 4.84/4.90 % Maximal term depth : 2 ( 1 avg) % 4.84/4.90 % Number of predicates : 4 ( 4 usr; 0 prp; 2-3 aty) % 4.84/4.90 % Number of functors : 5 ( 5 usr; 4 con; 0-1 aty) % 4.84/4.90 % Number of variables : 30 ( 1 sgn) % 4.84/4.90 % SPC : CNF_UNS_RFO_NEQ_HRN % 4.84/4.90 % 4.84/4.90 % Comments : % 4.84/4.90 %-------------------------------------------------------------------------- % 4.84/4.90 cnf(p2_1,negated_conjecture, % 4.84/4.90 p2(X0,X0) ). % 4.84/4.90 % 4.84/4.90 cnf(p4_2,negated_conjecture, % 4.84/4.90 p4(X8,X8) ). % 4.84/4.90 % 4.84/4.90 cnf(p6_3,negated_conjecture, % 4.84/4.90 p6(c7,f3(X21)) ). % 4.84/4.90 % 4.84/4.90 cnf(p5_4,negated_conjecture, % 4.84/4.90 p5(c7,c10,c9) ). % 4.84/4.90 % 4.84/4.90 cnf(p5_5,negated_conjecture, % 4.84/4.90 p5(c7,c10,c8) ). % 4.84/4.90 % 4.84/4.90 cnf(p5_6,negated_conjecture, % 4.84/4.90 p5(c7,X21,f3(X21)) ). % 4.84/4.90 % 4.84/4.90 cnf(p2_7,negated_conjecture, % 4.84/4.90 ( p2(f3(X6),f3(X7)) % 4.84/4.90 | ~ p2(X6,X7) ) ). % 4.84/4.90 % 4.84/4.90 cnf(not_p5_8,negated_conjecture, % 4.84/4.90 ( ~ p5(c7,c8,X26) % 4.84/4.90 | ~ p5(c7,c9,X26) ) ). % 4.84/4.90 % 4.84/4.90 cnf(p2_9,negated_conjecture, % 4.84/4.90 ( p2(X1,X2) % 4.84/4.90 | ~ p2(X0,X1) % 4.84/4.90 | ~ p2(X0,X2) ) ). % 4.84/4.90 % 4.84/4.90 cnf(p4_10,negated_conjecture, % 4.84/4.90 ( p4(X9,X10) % 4.84/4.90 | ~ p4(X8,X9) % 4.84/4.90 | ~ p4(X8,X10) ) ). % 4.84/4.90 % 4.84/4.90 cnf(p5_11,negated_conjecture, % 4.84/4.90 ( p5(X11,X12,X13) % 4.84/4.90 | ~ p5(X11,X12,X14) % 4.84/4.90 | ~ p5(X11,X14,X13) ) ). % 4.84/4.90 % 4.84/4.90 cnf(p6_12,negated_conjecture, % 4.84/4.90 ( p6(X22,X23) % 4.84/4.90 | ~ p4(X25,X22) % 4.84/4.90 | ~ p6(X25,X24) % 4.84/4.90 | ~ p2(X24,X23) ) ). % 4.84/4.90 % 4.84/4.90 cnf(p2_13,negated_conjecture, % 4.84/4.90 ( p2(X3,X4) % 4.84/4.90 | ~ p6(c7,X4) % 4.84/4.90 | ~ p6(c7,X3) % 4.84/4.90 | ~ p5(c7,X5,X4) % 4.84/4.90 | ~ p5(c7,X5,X3) ) ). % 4.84/4.90 % 4.84/4.90 cnf(p5_14,negated_conjecture, % 4.84/4.90 ( p5(X15,X16,X17) % 4.84/4.90 | ~ p2(X18,X16) % 4.84/4.90 | ~ p2(X19,X17) % 4.84/4.90 | ~ p4(X20,X15) % 4.84/4.90 | ~ p5(X20,X18,X19) ) ). % 4.84/4.90 % 4.84/4.90 %-------------------------------------------------------------------------- % 4.84/4.90 %------------------------------------------- % 4.84/4.90 % Proof found % 4.84/4.90 % SZS status Theorem for theBenchmark % 4.84/4.90 % SZS output start Proof % 4.84/4.90 %ClaNum:14(EqnAxiom:0) % 4.84/4.90 %VarNum:62(SingletonVarNum:30) % 4.84/4.90 %MaxLitNum:5 % 4.84/4.90 %MaxfuncDepth:1 % 4.84/4.90 %SharedTerms:6 % 4.84/4.90 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 % 4.84/4.90 %singleGoalClaCount:6 % 4.84/4.90 [4]P4(a1,a2,a4) % 4.84/4.90 [5]P4(a1,a2,a5) % 4.84/4.90 [1]P1(x11,x11) % 4.84/4.90 [2]P2(x21,x21) % 4.84/4.90 [3]P3(a1,f3(x31)) % 4.84/4.90 [6]P4(a1,x61,f3(x61)) % 4.84/4.90 [11]~P4(a1,a5,x111)+~P4(a1,a4,x111) % 4.84/4.90 [7]~P1(x71,x72)+P1(f3(x71),f3(x72)) % 4.84/4.90 [8]~P1(x83,x81)+P1(x81,x82)+~P1(x83,x82) % 4.84/4.90 [9]~P2(x93,x91)+P2(x91,x92)+~P2(x93,x92) % 4.84/4.90 [14]~P4(x141,x142,x144)+P4(x141,x142,x143)+~P4(x141,x144,x143) % 4.84/4.90 [10]~P3(x104,x103)+P3(x101,x102)+~P1(x103,x102)+~P2(x104,x101) % 4.84/4.90 [13]P1(x131,x132)+~P4(a1,x133,x131)+~P4(a1,x133,x132)+~P3(a1,x132)+~P3(a1,x131) % 4.84/4.90 [12]~P4(x126,x125,x124)+P4(x121,x122,x123)+~P1(x124,x123)+~P1(x125,x122)+~P2(x126,x121) % 4.84/4.90 %EqnAxiom % 4.84/4.90 % 4.84/4.90 %------------------------------------------- % 4.84/4.91 cnf(15,plain, % 4.84/4.91 (~P4(a1,a5,f3(a4))), % 4.84/4.91 inference(scs_inference,[],[6,11])). % 4.84/4.91 cnf(16,plain, % 4.84/4.91 (P4(a1,x161,f3(x161))), % 4.84/4.91 inference(rename_variables,[],[6])). % 4.84/4.91 cnf(18,plain, % 4.84/4.91 (P4(a1,a2,f3(a4))), % 4.84/4.91 inference(scs_inference,[],[6,16,4,11,14])). % 4.84/4.91 cnf(36,plain, % 4.84/4.91 (P4(a1,a2,f3(a5))), % 4.84/4.91 inference(scs_inference,[],[5,6,14])). % 4.84/4.91 cnf(128,plain, % 4.84/4.91 (~P1(f3(a5),f3(a4))), % 4.84/4.91 inference(scs_inference,[],[1,15,6,2,12])). % 4.84/4.91 cnf(135,plain, % 4.84/4.91 (~P3(a1,f3(a4))), % 4.84/4.91 inference(scs_inference,[],[128,1,3,36,18,8,13])). % 4.84/4.91 cnf(136,plain, % 4.84/4.91 ($false), % 4.84/4.91 inference(scs_inference,[],[135,3]), % 4.84/4.91 ['proof']). % 4.84/4.91 % SZS output end Proof % 4.84/4.91 % Total time :4.260000s %------------------------------------------------------------------------------