%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN566-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 : n025.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 58.57s 58.63s % Output : CNFRefutation 58.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN566-1 : TPTP v8.2.0. Released v2.5.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.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:38:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 58.48/58.62 %------------------------------------------- % 58.48/58.62 % File :CSE---1.7 % 58.48/58.62 % Problem :theBenchmark % 58.48/58.62 % Transform :cnf % 58.48/58.62 % Format :tptp:raw % 58.48/58.62 % Command :java -jar mcs_scs.jar %d %s % 58.48/58.62 % 58.48/58.62 % Result :Theorem 58.000000s % 58.48/58.62 % Output :CNFRefutation 58.000000s % 58.48/58.62 %------------------------------------------- % 58.57/58.63 %-------------------------------------------------------------------------- % 58.57/58.63 % File : SYN566-1 : TPTP v8.2.0. Released v2.5.0. % 58.57/58.63 % Domain : Syntactic % 58.57/58.63 % Problem : Harrison problem 2967 % 58.57/58.63 % Version : Especial. % 58.57/58.63 % English : % 58.57/58.63 % 58.57/58.63 % Refs : [Har01] Email to G. Sutcliffe % 58.57/58.63 % Source : [Har01] % 58.57/58.63 % Names : % 58.57/58.63 % 58.57/58.63 % Status : Unsatisfiable % 58.57/58.63 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v2.5.0 % 58.57/58.63 % Syntax : Number of clauses : 19 ( 8 unt; 0 nHn; 15 RR) % 58.57/58.63 % Number of literals : 40 ( 0 equ; 22 neg) % 58.57/58.63 % Maximal clause size : 4 ( 2 avg) % 58.57/58.63 % Maximal term depth : 3 ( 1 avg) % 58.57/58.63 % Number of predicates : 6 ( 6 usr; 0 prp; 2-2 aty) % 58.57/58.63 % Number of functors : 8 ( 8 usr; 5 con; 0-1 aty) % 58.57/58.63 % Number of variables : 35 ( 0 sgn) % 58.57/58.63 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.57/58.63 % 58.57/58.63 % Comments : % 58.57/58.63 %-------------------------------------------------------------------------- % 58.57/58.63 cnf(p9_1,negated_conjecture, % 58.57/58.63 p9(X25,X25) ). % 58.57/58.63 % 58.57/58.63 cnf(p2_2,negated_conjecture, % 58.57/58.63 p2(X4,X4) ). % 58.57/58.63 % 58.57/58.63 cnf(p3_3,negated_conjecture, % 58.57/58.63 p3(X11,X11) ). % 58.57/58.63 % 58.57/58.63 cnf(p7_4,negated_conjecture, % 58.57/58.63 p7(X16,X16) ). % 58.57/58.63 % 58.57/58.63 cnf(p10_5,negated_conjecture, % 58.57/58.63 p10(c15,c11) ). % 58.57/58.63 % 58.57/58.63 cnf(p8_6,negated_conjecture, % 58.57/58.63 p8(c12,c13) ). % 58.57/58.63 % 58.57/58.63 cnf(p2_7,negated_conjecture, % 58.57/58.63 p2(c14,f6(c15)) ). % 58.57/58.63 % 58.57/58.63 cnf(p3_8,negated_conjecture, % 58.57/58.63 p3(c13,f4(c14)) ). % 58.57/58.63 % 58.57/58.63 cnf(p3_9,negated_conjecture, % 58.57/58.63 ( p3(f4(X14),f4(X15)) % 58.57/58.63 | ~ p2(X14,X15) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p2_10,negated_conjecture, % 58.57/58.63 ( p2(f5(X7),f5(X8)) % 58.57/58.63 | ~ p2(X7,X8) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p2_11,negated_conjecture, % 58.57/58.63 ( p2(f6(X9),f6(X10)) % 58.57/58.63 | ~ p2(X9,X10) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p9_12,negated_conjecture, % 58.57/58.63 ( p9(X26,X27) % 58.57/58.63 | ~ p9(X25,X26) % 58.57/58.63 | ~ p9(X25,X27) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p2_13,negated_conjecture, % 58.57/58.63 ( p2(X5,X6) % 58.57/58.63 | ~ p2(X4,X5) % 58.57/58.63 | ~ p2(X4,X6) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p3_14,negated_conjecture, % 58.57/58.63 ( p3(X12,X13) % 58.57/58.63 | ~ p3(X11,X12) % 58.57/58.63 | ~ p3(X11,X13) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p7_15,negated_conjecture, % 58.57/58.63 ( p7(X17,X18) % 58.57/58.63 | ~ p7(X16,X17) % 58.57/58.63 | ~ p7(X16,X18) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p8_16,negated_conjecture, % 58.57/58.63 ( p8(X19,f4(f5(X20))) % 58.57/58.63 | ~ p8(X19,f4(f6(X20))) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p10_17,negated_conjecture, % 58.57/58.63 ( p10(X0,X1) % 58.57/58.63 | ~ p2(X2,X0) % 58.57/58.63 | ~ p9(X3,X1) % 58.57/58.63 | ~ p10(X2,X3) ) ). % 58.57/58.63 % 58.57/58.63 cnf(p8_18,negated_conjecture, % 58.57/58.63 ( p8(X21,X22) % 58.57/58.63 | ~ p7(X24,X21) % 58.57/58.63 | ~ p8(X24,X23) % 58.57/58.63 | ~ p3(X23,X22) ) ). % 58.57/58.63 % 58.57/58.63 cnf(not_p10_19,negated_conjecture, % 58.57/58.63 ( ~ p10(X28,c11) % 58.57/58.63 | ~ p8(c12,X30) % 58.57/58.63 | ~ p3(X30,f4(X29)) % 58.57/58.63 | ~ p2(X29,f5(X28)) ) ). % 58.57/58.63 % 58.57/58.63 %-------------------------------------------------------------------------- % 58.57/58.63 %------------------------------------------- % 58.57/58.63 % Proof found % 58.57/58.63 % SZS status Theorem for theBenchmark % 58.57/58.63 % SZS output start Proof % 58.57/58.64 %ClaNum:19(EqnAxiom:0) % 58.57/58.64 %VarNum:70(SingletonVarNum:35) % 58.57/58.64 %MaxLitNum:4 % 58.57/58.64 %MaxfuncDepth:2 % 58.57/58.64 %SharedTerms:11 % 58.57/58.64 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 % 58.57/58.64 %singleGoalClaCount:8 % 58.57/58.64 [1]P1(a1,a2) % 58.57/58.64 [2]P2(a3,a4) % 58.57/58.64 [7]P3(a5,f6(a1)) % 58.57/58.64 [8]P4(a4,f7(a5)) % 58.57/58.64 [3]P6(x31,x31) % 58.57/58.64 [4]P3(x41,x41) % 58.57/58.64 [5]P4(x51,x51) % 58.57/58.64 [6]P5(x61,x61) % 58.57/58.64 [9]~P3(x91,x92)+P3(f6(x91),f6(x92)) % 58.57/58.64 [10]~P3(x101,x102)+P3(f8(x101),f8(x102)) % 58.57/58.64 [11]~P3(x111,x112)+P4(f7(x111),f7(x112)) % 58.57/58.64 [18]~P2(x181,f7(f6(x182)))+P2(x181,f7(f8(x182))) % 58.57/58.64 [12]~P6(x123,x121)+P6(x121,x122)+~P6(x123,x122) % 58.57/58.64 [13]~P3(x133,x131)+P3(x131,x132)+~P3(x133,x132) % 58.57/58.64 [14]~P4(x143,x141)+P4(x141,x142)+~P4(x143,x142) % 58.57/58.64 [15]~P5(x153,x151)+P5(x151,x152)+~P5(x153,x152) % 58.57/58.64 [19]~P4(x192,f7(x193))+~P1(x191,a2)+~P3(x193,f8(x191))+~P2(a3,x192) % 58.57/58.64 [16]~P1(x164,x163)+P1(x161,x162)+~P6(x163,x162)+~P3(x164,x161) % 58.57/58.64 [17]~P2(x174,x173)+P2(x171,x172)+~P4(x173,x172)+~P5(x174,x171) % 58.57/58.64 %EqnAxiom % 58.57/58.64 % 58.57/58.64 %------------------------------------------- % 58.57/58.65 cnf(41,plain, % 58.57/58.65 (~P2(a3,f7(f6(a1)))), % 58.57/58.65 inference(scs_inference,[],[4,5,1,18,19])). % 58.57/58.65 cnf(42,plain, % 58.57/58.65 (P4(f7(a5),a4)), % 58.57/58.65 inference(scs_inference,[],[8,5,14])). % 58.57/58.65 cnf(148,plain, % 58.57/58.65 ($false), % 58.57/58.65 inference(scs_inference,[],[2,42,41,6,7,9,10,11,17,14]), % 58.57/58.65 ['proof']). % 58.57/58.65 % SZS output end Proof % 58.57/58.65 % Total time :58.000000s %------------------------------------------------------------------------------