%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN568-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 : n001.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:59 EDT 2024 % Result : Unsatisfiable 0.50s 0.59s % Output : CNFRefutation 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : SYN568-1 : TPTP v8.2.0. Released v2.5.0. % 0.05/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n001.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Sun Jun 23 22:47:39 EDT 2024 % 0.09/0.31 % CPUTime : % 0.48/0.55 start to proof:theBenchmark % 0.50/0.59 %------------------------------------------- % 0.50/0.59 % File :CSE---1.7 % 0.50/0.59 % Problem :theBenchmark % 0.50/0.59 % Transform :cnf % 0.50/0.59 % Format :tptp:raw % 0.50/0.59 % Command :java -jar mcs_scs.jar %d %s % 0.50/0.59 % 0.50/0.59 % Result :Theorem 0.000000s % 0.50/0.59 % Output :CNFRefutation 0.000000s % 0.50/0.59 %------------------------------------------- % 0.50/0.59 %-------------------------------------------------------------------------- % 0.50/0.59 % File : SYN568-1 : TPTP v8.2.0. Released v2.5.0. % 0.50/0.59 % Domain : Syntactic % 0.50/0.59 % Problem : Harrison problem 3076 % 0.50/0.59 % Version : Especial. % 0.50/0.59 % English : % 0.50/0.59 % 0.50/0.59 % Refs : [Har01] Email to G. Sutcliffe % 0.50/0.59 % Source : [Har01] % 0.50/0.59 % Names : % 0.50/0.59 % 0.50/0.59 % Status : Unsatisfiable % 0.50/0.59 % Rating : 0.00 v2.6.0, 0.33 v2.5.0 % 0.50/0.59 % Syntax : Number of clauses : 20 ( 6 unt; 2 nHn; 14 RR) % 0.50/0.59 % Number of literals : 44 ( 0 equ; 25 neg) % 0.50/0.59 % Maximal clause size : 4 ( 2 avg) % 0.50/0.59 % Maximal term depth : 5 ( 1 avg) % 0.50/0.59 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty) % 0.50/0.59 % Number of functors : 9 ( 9 usr; 3 con; 0-2 aty) % 0.50/0.59 % Number of variables : 41 ( 1 sgn) % 0.50/0.59 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.50/0.59 % 0.50/0.59 % Comments : % 0.50/0.59 %-------------------------------------------------------------------------- % 0.50/0.59 cnf(p2_1,negated_conjecture, % 0.50/0.59 p2(X17,X17) ). % 0.50/0.59 % 0.50/0.59 cnf(p3_2,negated_conjecture, % 0.50/0.59 p3(X28,X28) ). % 0.50/0.59 % 0.50/0.59 cnf(not_p11_3,negated_conjecture, % 0.50/0.59 ~ p11(f9(c13),f9(c14)) ). % 0.50/0.59 % 0.50/0.59 cnf(p11_4,negated_conjecture, % 0.50/0.59 p11(f5(f6(c12)),f9(X16)) ). % 0.50/0.59 % 0.50/0.59 cnf(p10_5,negated_conjecture, % 0.50/0.59 ( p10(X4,X5) % 0.50/0.59 | p11(X5,X4) ) ). % 0.50/0.59 % 0.50/0.59 cnf(not_p10_6,negated_conjecture, % 0.50/0.59 ( ~ p10(X4,X5) % 0.50/0.59 | ~ p11(X5,X4) ) ). % 0.50/0.59 % 0.50/0.59 cnf(not_p3_7,negated_conjecture, % 0.50/0.59 ~ p3(f6(f7(f8(c12))),f6(c12)) ). % 0.50/0.59 % 0.50/0.59 cnf(p3_8,negated_conjecture, % 0.50/0.59 ( p3(f8(X35),f8(X36)) % 0.50/0.59 | ~ p3(X35,X36) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p2_9,negated_conjecture, % 0.50/0.59 ( p2(f5(X24),f5(X25)) % 0.50/0.59 | ~ p3(X24,X25) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p2_10,negated_conjecture, % 0.50/0.59 ( p2(f9(X26),f9(X27)) % 0.50/0.59 | ~ p2(X26,X27) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p3_11,negated_conjecture, % 0.50/0.59 ( p3(f6(X31),f6(X32)) % 0.50/0.59 | ~ p3(X31,X32) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p3_12,negated_conjecture, % 0.50/0.59 ( p3(f7(X33),f7(X34)) % 0.50/0.59 | ~ p3(X33,X34) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p2_13,negated_conjecture, % 0.50/0.59 ( p2(X18,X19) % 0.50/0.59 | ~ p2(X17,X18) % 0.50/0.59 | ~ p2(X17,X19) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p3_14,negated_conjecture, % 0.50/0.59 ( p3(X29,X30) % 0.50/0.59 | ~ p3(X28,X29) % 0.50/0.59 | ~ p3(X28,X30) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p10_15,negated_conjecture, % 0.50/0.59 ( p10(X0,X1) % 0.50/0.59 | ~ p2(X2,X0) % 0.50/0.59 | ~ p2(X3,X1) % 0.50/0.59 | ~ p10(X2,X3) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p11_16,negated_conjecture, % 0.50/0.59 ( p11(X9,X10) % 0.50/0.59 | ~ p2(X11,X9) % 0.50/0.59 | ~ p2(X12,X10) % 0.50/0.59 | ~ p11(X11,X12) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p2_17,negated_conjecture, % 0.50/0.59 ( p2(f4(X20,X21),f4(X22,X23)) % 0.50/0.59 | ~ p2(X20,X22) % 0.50/0.59 | ~ p3(X21,X23) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p11_18,negated_conjecture, % 0.50/0.59 p11(f4(f9(c13),f6(f7(f8(c12)))),f4(f9(c14),f6(f7(f8(c12))))) ). % 0.50/0.59 % 0.50/0.59 cnf(p11_19,negated_conjecture, % 0.50/0.59 ( p11(f4(X13,X14),f4(X15,X14)) % 0.50/0.59 | ~ p11(X13,X15) % 0.50/0.59 | ~ p11(f5(f6(c12)),X13) ) ). % 0.50/0.59 % 0.50/0.59 cnf(p3_20,negated_conjecture, % 0.50/0.59 ( p3(X7,f6(c12)) % 0.50/0.59 | p10(f4(X6,X7),f4(X8,X7)) % 0.50/0.59 | ~ p10(X6,X8) % 0.50/0.59 | ~ p11(f5(f6(c12)),X6) ) ). % 0.50/0.59 % 0.50/0.59 %-------------------------------------------------------------------------- % 0.50/0.59 %------------------------------------------- % 0.50/0.59 % Proof found % 0.50/0.59 % SZS status Theorem for theBenchmark % 0.50/0.59 % SZS output start Proof % 0.50/0.59 %ClaNum:20(EqnAxiom:0) % 0.50/0.59 %VarNum:84(SingletonVarNum:41) % 0.50/0.59 %MaxLitNum:4 % 0.50/0.59 %MaxfuncDepth:4 % 0.50/0.59 %SharedTerms:15 % 0.50/0.59 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 % 0.50/0.59 %singleGoalClaCount:6 % 0.50/0.59 [5]~P2(f7(a4),f7(a6)) % 0.50/0.59 [6]~P4(f2(f9(f8(a1))),f2(a1)) % 0.50/0.59 [4]P2(f5(f7(a4),f2(f9(f8(a1)))),f5(f7(a6),f2(f9(f8(a1))))) % 0.50/0.59 [1]P1(x11,x11) % 0.50/0.59 [2]P4(x21,x21) % 0.50/0.60 [3]P2(f3(f2(a1)),f7(x31)) % 0.50/0.60 [7]P3(x72,x71)+P2(x71,x72) % 0.50/0.60 [8]~P3(x82,x81)+~P2(x81,x82) % 0.50/0.60 [9]~P1(x91,x92)+P1(f7(x91),f7(x92)) % 0.50/0.60 [10]~P4(x101,x102)+P1(f3(x101),f3(x102)) % 0.50/0.60 [11]~P4(x111,x112)+P4(f2(x111),f2(x112)) % 0.50/0.60 [12]~P4(x121,x122)+P4(f8(x121),f8(x122)) % 0.50/0.60 [13]~P4(x131,x132)+P4(f9(x131),f9(x132)) % 0.50/0.60 [14]~P1(x143,x141)+P1(x141,x142)+~P1(x143,x142) % 0.50/0.60 [15]~P4(x153,x151)+P4(x151,x152)+~P4(x153,x152) % 0.50/0.60 [19]~P2(x191,x193)+P2(f5(x191,x192),f5(x193,x192))+~P2(f3(f2(a1)),x191) % 0.50/0.60 [18]~P1(x181,x183)+~P4(x182,x184)+P1(f5(x181,x182),f5(x183,x184)) % 0.50/0.60 [20]~P3(x202,x203)+P3(f5(x202,x201),f5(x203,x201))+P4(x201,f2(a1))+~P2(f3(f2(a1)),x202) % 0.50/0.60 [16]~P2(x164,x163)+P2(x161,x162)+~P1(x163,x162)+~P1(x164,x161) % 0.50/0.60 [17]~P3(x174,x173)+P3(x171,x172)+~P1(x173,x172)+~P1(x174,x171) % 0.50/0.60 %EqnAxiom % 0.50/0.60 % 0.50/0.60 %------------------------------------------- % 0.50/0.60 cnf(27,plain, % 0.50/0.60 (P3(f5(f7(a6),f2(f9(f8(a1)))),f5(f7(a4),f2(f9(f8(a1)))))), % 0.50/0.60 inference(scs_inference,[],[5,3,6,7,8,11,20])). % 0.50/0.60 cnf(34,plain, % 0.50/0.60 ($false), % 0.50/0.60 inference(scs_inference,[],[27,4,8]), % 0.50/0.60 ['proof']). % 0.50/0.60 % SZS output end Proof % 0.50/0.60 % Total time :0.000000s %------------------------------------------------------------------------------