%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN559-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:58 EDT 2024 % Result : Unsatisfiable 0.56s 0.83s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN559-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n001.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 22:42:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.55/0.58 start to proof:theBenchmark % 0.56/0.83 %------------------------------------------- % 0.56/0.83 % File :CSE---1.7 % 0.56/0.83 % Problem :theBenchmark % 0.56/0.83 % Transform :cnf % 0.56/0.83 % Format :tptp:raw % 0.56/0.83 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.83 % 0.56/0.83 % Result :Theorem 0.200000s % 0.56/0.83 % Output :CNFRefutation 0.200000s % 0.56/0.83 %------------------------------------------- % 0.56/0.83 %-------------------------------------------------------------------------- % 0.56/0.83 % File : SYN559-1 : TPTP v8.2.0. Released v2.5.0. % 0.56/0.83 % Domain : Syntactic % 0.56/0.83 % Problem : Harrison problem 2418 % 0.56/0.83 % Version : Especial. % 0.56/0.83 % English : % 0.56/0.83 % 0.56/0.83 % Refs : [Har01] Email to G. Sutcliffe % 0.56/0.83 % Source : [Har01] % 0.56/0.83 % Names : % 0.56/0.83 % 0.56/0.83 % Status : Unsatisfiable % 0.56/0.83 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.00 v2.5.0 % 0.56/0.83 % Syntax : Number of clauses : 14 ( 6 unt; 0 nHn; 13 RR) % 0.56/0.83 % Number of literals : 32 ( 0 equ; 19 neg) % 0.56/0.83 % Maximal clause size : 4 ( 2 avg) % 0.56/0.83 % Maximal term depth : 3 ( 1 avg) % 0.56/0.83 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty) % 0.56/0.83 % Number of functors : 11 ( 11 usr; 7 con; 0-2 aty) % 0.56/0.83 % Number of variables : 28 ( 0 sgn) % 0.56/0.83 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.56/0.83 % 0.56/0.83 % Comments : % 0.56/0.83 %-------------------------------------------------------------------------- % 0.56/0.83 cnf(p2_1,negated_conjecture, % 0.56/0.83 p2(X0,X0) ). % 0.56/0.83 % 0.56/0.83 cnf(p8_2,negated_conjecture, % 0.56/0.83 p8(c13,c9) ). % 0.56/0.83 % 0.56/0.83 cnf(p7_3,negated_conjecture, % 0.56/0.83 p7(c10,c13) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_4,negated_conjecture, % 0.56/0.83 p2(f6(c9,c13),c14) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_5,negated_conjecture, % 0.56/0.83 p2(f5(c14,c10),c15) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_6,negated_conjecture, % 0.56/0.83 p2(f3(f4(c11),c12),c15) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_7,negated_conjecture, % 0.56/0.83 ( p2(f4(X7),f4(X8)) % 0.56/0.83 | ~ p2(X7,X8) ) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_8,negated_conjecture, % 0.56/0.83 ( p2(X1,X2) % 0.56/0.83 | ~ p2(X0,X1) % 0.56/0.83 | ~ p2(X0,X2) ) ). % 0.56/0.83 % 0.56/0.83 cnf(p8_9,negated_conjecture, % 0.56/0.83 ( p8(X21,X22) % 0.56/0.83 | ~ p2(X24,X22) % 0.56/0.83 | ~ p8(X23,X24) % 0.56/0.83 | ~ p2(X23,X21) ) ). % 0.56/0.83 % 0.56/0.83 cnf(p7_10,negated_conjecture, % 0.56/0.83 ( p7(X17,X18) % 0.56/0.83 | ~ p2(X20,X18) % 0.56/0.83 | ~ p7(X19,X20) % 0.56/0.83 | ~ p2(X19,X17) ) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_11,negated_conjecture, % 0.56/0.83 ( p2(f3(X3,X4),f3(X5,X6)) % 0.56/0.83 | ~ p2(X3,X5) % 0.56/0.83 | ~ p2(X4,X6) ) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_12,negated_conjecture, % 0.56/0.83 ( p2(f6(X13,X14),f6(X15,X16)) % 0.56/0.83 | ~ p2(X13,X15) % 0.56/0.83 | ~ p2(X14,X16) ) ). % 0.56/0.83 % 0.56/0.83 cnf(p2_13,negated_conjecture, % 0.56/0.83 ( p2(f5(X9,X10),f5(X11,X12)) % 0.56/0.83 | ~ p2(X9,X11) % 0.56/0.83 | ~ p2(X10,X12) ) ). % 0.56/0.83 % 0.56/0.83 cnf(not_p8_14,negated_conjecture, % 0.56/0.83 ( ~ p8(X26,c9) % 0.56/0.83 | ~ p7(c10,X26) % 0.56/0.83 | ~ p2(f6(c9,X26),X25) % 0.56/0.83 | ~ p2(f5(X25,c10),f3(f4(c11),c12)) ) ). % 0.56/0.83 % 0.56/0.83 %-------------------------------------------------------------------------- % 0.56/0.83 %------------------------------------------- % 0.56/0.83 % Proof found % 0.56/0.83 % SZS status Theorem for theBenchmark % 0.56/0.83 % SZS output start Proof % 0.56/0.83 %ClaNum:14(EqnAxiom:0) % 0.56/0.83 %VarNum:57(SingletonVarNum:28) % 0.56/0.83 %MaxLitNum:4 % 0.56/0.83 %MaxfuncDepth:2 % 0.56/0.83 %SharedTerms:16 % 0.56/0.83 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 % 0.56/0.83 %singleGoalClaCount:6 % 0.56/0.83 [1]P1(a1,a5) % 0.56/0.83 [2]P2(a2,a1) % 0.56/0.83 [4]P3(f8(a5,a1),a6) % 0.56/0.83 [5]P3(f9(a6,a2),a7) % 0.56/0.83 [6]P3(f11(f10(a3),a4),a7) % 0.56/0.83 [3]P3(x31,x31) % 0.56/0.83 [7]~P3(x71,x72)+P3(f10(x71),f10(x72)) % 0.56/0.83 [8]~P3(x83,x81)+P3(x81,x82)+~P3(x83,x82) % 0.56/0.83 [11]~P3(x112,x114)+~P3(x111,x113)+P3(f8(x111,x112),f8(x113,x114)) % 0.56/0.83 [12]~P3(x122,x124)+~P3(x121,x123)+P3(f9(x121,x122),f9(x123,x124)) % 0.56/0.83 [13]~P3(x132,x134)+~P3(x131,x133)+P3(f11(x131,x132),f11(x133,x134)) % 0.56/0.83 [14]~P2(a2,x141)+~P1(x141,a5)+~P3(f8(a5,x141),x142)+~P3(f9(x142,a2),f11(f10(a3),a4)) % 0.56/0.83 [9]~P1(x93,x94)+P1(x91,x92)+~P3(x93,x91)+~P3(x94,x92) % 0.56/0.83 [10]~P2(x103,x104)+P2(x101,x102)+~P3(x103,x101)+~P3(x104,x102) % 0.56/0.83 %EqnAxiom % 0.56/0.83 % 0.56/0.83 %------------------------------------------- % 0.56/0.83 cnf(67,plain, % 0.56/0.84 (P3(a7,f9(a6,a2))), % 0.56/0.84 inference(scs_inference,[],[5,3,8])). % 0.56/0.84 cnf(87,plain, % 0.56/0.84 (P3(a7,f11(f10(a3),a4))), % 0.56/0.84 inference(scs_inference,[],[6,3,8])). % 0.56/0.84 cnf(205,plain, % 0.56/0.84 (~P3(a5,x2051)+P1(a1,x2051)), % 0.56/0.84 inference(scs_inference,[],[1,3,9])). % 0.56/0.84 cnf(211,plain, % 0.56/0.84 (~P3(f9(a6,a2),f11(f10(a3),a4))), % 0.56/0.84 inference(scs_inference,[],[3,4,2,205,14])). % 0.56/0.84 cnf(213,plain, % 0.56/0.84 ($false), % 0.56/0.84 inference(scs_inference,[],[67,87,211,8]), % 0.56/0.84 ['proof']). % 0.56/0.84 % SZS output end Proof % 0.56/0.84 % Total time :0.200000s %------------------------------------------------------------------------------