%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN571-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:06:00 EDT 2024 % Result : Unsatisfiable 9.21s 9.27s % Output : CNFRefutation 9.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN571-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/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 21:39:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.46/0.57 start to proof:theBenchmark % 9.21/9.26 %------------------------------------------- % 9.21/9.26 % File :CSE---1.7 % 9.21/9.26 % Problem :theBenchmark % 9.21/9.26 % Transform :cnf % 9.21/9.26 % Format :tptp:raw % 9.21/9.26 % Command :java -jar mcs_scs.jar %d %s % 9.21/9.26 % 9.21/9.26 % Result :Theorem 8.630000s % 9.21/9.26 % Output :CNFRefutation 8.630000s % 9.21/9.26 %------------------------------------------- % 9.21/9.27 %-------------------------------------------------------------------------- % 9.21/9.27 % File : SYN571-1 : TPTP v8.2.0. Released v2.5.0. % 9.21/9.27 % Domain : Syntactic % 9.21/9.27 % Problem : Harrison problem 3108 % 9.21/9.27 % Version : Especial. % 9.21/9.27 % English : % 9.21/9.27 % 9.21/9.27 % Refs : [Har01] Email to G. Sutcliffe % 9.21/9.27 % Source : [Har01] % 9.21/9.27 % Names : % 9.21/9.27 % 9.21/9.27 % Status : Unsatisfiable % 9.21/9.27 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.1.0, 0.33 v7.0.0, 0.50 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 9.21/9.27 % Syntax : Number of clauses : 20 ( 6 unt; 1 nHn; 15 RR) % 9.21/9.27 % Number of literals : 41 ( 0 equ; 22 neg) % 9.21/9.27 % Maximal clause size : 4 ( 2 avg) % 9.21/9.27 % Maximal term depth : 5 ( 1 avg) % 9.21/9.27 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty) % 9.21/9.27 % Number of functors : 10 ( 10 usr; 3 con; 0-2 aty) % 9.21/9.27 % Number of variables : 46 ( 2 sgn) % 9.21/9.27 % SPC : CNF_UNS_RFO_NEQ_NHN % 9.21/9.27 % 9.21/9.27 % Comments : % 9.21/9.27 %-------------------------------------------------------------------------- % 9.21/9.27 cnf(p4_1,negated_conjecture, % 9.21/9.27 p4(X26,X26) ). % 9.21/9.27 % 9.21/9.27 cnf(p2_2,negated_conjecture, % 9.21/9.27 p2(X11,X11) ). % 9.21/9.27 % 9.21/9.27 cnf(p11_3,negated_conjecture, % 9.21/9.27 p11(f5(X10),c14) ). % 9.21/9.27 % 9.21/9.27 cnf(not_p11_4,negated_conjecture, % 9.21/9.27 ~ p11(c13,f5(X40)) ). % 9.21/9.27 % 9.21/9.27 cnf(p11_5,negated_conjecture, % 9.21/9.27 ( p11(X4,X5) % 9.21/9.27 | p11(X5,X4) ) ). % 9.21/9.27 % 9.21/9.27 cnf(not_p11_6,negated_conjecture, % 9.21/9.27 ~ p11(X39,f3(X39,f5(f6(f7(c12))))) ). % 9.21/9.27 % 9.21/9.27 cnf(p11_7,negated_conjecture, % 9.21/9.27 ( p11(c14,X9) % 9.21/9.27 | ~ p11(f5(f10(X9)),X9) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p4_8,negated_conjecture, % 9.21/9.27 ( p4(f7(X33),f7(X34)) % 9.21/9.27 | ~ p4(X33,X34) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p2_9,negated_conjecture, % 9.21/9.27 ( p2(f5(X18),f5(X19)) % 9.21/9.27 | ~ p4(X18,X19) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p4_10,negated_conjecture, % 9.21/9.27 ( p4(f10(X29),f10(X30)) % 9.21/9.27 | ~ p2(X29,X30) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p4_11,negated_conjecture, % 9.21/9.27 ( p4(f6(X31),f6(X32)) % 9.21/9.27 | ~ p4(X31,X32) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p2_12,negated_conjecture, % 9.21/9.27 ( p2(X12,X13) % 9.21/9.27 | ~ p2(X11,X12) % 9.21/9.27 | ~ p2(X11,X13) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p4_13,negated_conjecture, % 9.21/9.27 ( p4(X27,X28) % 9.21/9.27 | ~ p4(X26,X27) % 9.21/9.27 | ~ p4(X26,X28) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p2_14,negated_conjecture, % 9.21/9.27 p2(f9(f5(X24),f5(X25)),f5(f8(X24,X25))) ). % 9.21/9.27 % 9.21/9.27 cnf(p11_15,negated_conjecture, % 9.21/9.27 ( p11(X6,f3(X7,X8)) % 9.21/9.27 | ~ p11(f9(X6,X8),X7) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p11_16,negated_conjecture, % 9.21/9.27 ( p11(f9(X6,X8),X7) % 9.21/9.27 | ~ p11(X6,f3(X7,X8)) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p11_17,negated_conjecture, % 9.21/9.27 ( p11(X0,X1) % 9.21/9.27 | ~ p2(X2,X0) % 9.21/9.27 | ~ p2(X3,X1) % 9.21/9.27 | ~ p11(X2,X3) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p4_18,negated_conjecture, % 9.21/9.27 ( p4(f8(X35,X36),f8(X37,X38)) % 9.21/9.27 | ~ p4(X35,X37) % 9.21/9.27 | ~ p4(X36,X38) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p2_19,negated_conjecture, % 9.21/9.27 ( p2(f3(X14,X15),f3(X16,X17)) % 9.21/9.27 | ~ p2(X14,X16) % 9.21/9.27 | ~ p2(X15,X17) ) ). % 9.21/9.27 % 9.21/9.27 cnf(p2_20,negated_conjecture, % 9.21/9.27 ( p2(f9(X20,X21),f9(X22,X23)) % 9.21/9.27 | ~ p2(X20,X22) % 9.21/9.27 | ~ p2(X21,X23) ) ). % 9.21/9.27 % 9.21/9.27 %-------------------------------------------------------------------------- % 9.21/9.27 %------------------------------------------- % 9.21/9.27 % Proof found % 9.21/9.27 % SZS status Theorem for theBenchmark % 9.21/9.27 % SZS output start Proof % 9.21/9.28 %ClaNum:20(EqnAxiom:0) % 9.21/9.28 %VarNum:91(SingletonVarNum:46) % 9.21/9.28 %MaxLitNum:4 % 9.21/9.28 %MaxfuncDepth:4 % 9.21/9.28 %SharedTerms:6 % 9.21/9.28 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 % 9.21/9.28 %singleGoalClaCount:6 % 9.21/9.28 [1]P1(x11,x11) % 9.21/9.28 [2]P2(x21,x21) % 9.21/9.28 [3]P3(f1(x31),a2) % 9.21/9.28 [5]~P3(a3,f1(x51)) % 9.21/9.28 [6]~P3(x61,f5(x61,f1(f10(f9(a4))))) % 9.21/9.28 [4]P2(f7(f1(x41),f1(x42)),f1(f8(x41,x42))) % 9.21/9.28 [14]P3(a2,x141)+~P3(f1(f6(x141)),x141) % 9.21/9.28 [7]P3(x72,x71)+P3(x71,x72) % 9.21/9.28 [8]~P1(x81,x82)+P1(f9(x81),f9(x82)) % 9.21/9.28 [9]~P1(x91,x92)+P1(f10(x91),f10(x92)) % 9.21/9.28 [10]~P2(x101,x102)+P1(f6(x101),f6(x102)) % 9.21/9.28 [11]~P1(x111,x112)+P2(f1(x111),f1(x112)) % 9.21/9.28 [16]~P3(f7(x161,x163),x162)+P3(x161,f5(x162,x163)) % 9.21/9.28 [17]~P3(x171,f5(x173,x172))+P3(f7(x171,x172),x173) % 9.21/9.28 [12]~P1(x123,x121)+P1(x121,x122)+~P1(x123,x122) % 9.21/9.28 [13]~P2(x133,x131)+P2(x131,x132)+~P2(x133,x132) % 9.21/9.28 [18]~P1(x182,x184)+~P1(x181,x183)+P1(f8(x181,x182),f8(x183,x184)) % 9.21/9.28 [19]~P2(x192,x194)+~P2(x191,x193)+P2(f5(x191,x192),f5(x193,x194)) % 9.21/9.28 [20]~P2(x202,x204)+~P2(x201,x203)+P2(f7(x201,x202),f7(x203,x204)) % 9.21/9.28 [15]~P3(x154,x153)+P3(x151,x152)+~P2(x153,x152)+~P2(x154,x151) % 9.21/9.28 %EqnAxiom % 9.21/9.28 % 9.21/9.28 %------------------------------------------- % 9.21/9.28 cnf(21,plain, % 9.21/9.28 (P3(f1(x211),a3)), % 9.21/9.28 inference(scs_inference,[],[5,7])). % 9.21/9.28 cnf(26,plain, % 9.21/9.28 (~P3(f7(x261,f1(f10(f9(a4)))),x261)), % 9.21/9.28 inference(scs_inference,[],[3,5,6,7,14,16])). % 9.21/9.28 cnf(33,plain, % 9.21/9.28 (P2(f1(f8(x331,x332)),f7(f1(x331),f1(x332)))), % 9.21/9.28 inference(scs_inference,[],[26,21,4,2,7,14,13])). % 9.21/9.28 cnf(39,plain, % 9.21/9.28 (P3(f7(f1(x391),f1(x392)),a2)), % 9.21/9.28 inference(scs_inference,[],[3,33,2,15])). % 9.21/9.28 cnf(206,plain, % 9.21/9.28 ($false), % 9.21/9.28 inference(scs_inference,[],[6,39,14,16]), % 9.21/9.28 ['proof']). % 9.21/9.28 % SZS output end Proof % 9.21/9.28 % Total time :8.630000s %------------------------------------------------------------------------------