%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN555-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 : n021.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:57 EDT 2024 % Result : Unsatisfiable 0.15s 0.52s % Output : CNFRefutation 0.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SYN555-1 : TPTP v8.2.0. Released v2.5.0. % 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.29 % Computer : n021.cluster.edu % 0.07/0.29 % Model : x86_64 x86_64 % 0.07/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.29 % Memory : 8042.1875MB % 0.07/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.30 % CPULimit : 300 % 0.07/0.30 % WCLimit : 300 % 0.07/0.30 % DateTime : Mon Jun 24 00:11:09 EDT 2024 % 0.07/0.30 % CPUTime : % 0.15/0.49 start to proof:theBenchmark % 0.15/0.52 %------------------------------------------- % 0.15/0.52 % File :CSE---1.7 % 0.15/0.52 % Problem :theBenchmark % 0.15/0.52 % Transform :cnf % 0.15/0.52 % Format :tptp:raw % 0.15/0.52 % Command :java -jar mcs_scs.jar %d %s % 0.15/0.52 % 0.15/0.52 % Result :Theorem 0.000000s % 0.15/0.52 % Output :CNFRefutation 0.000000s % 0.15/0.52 %------------------------------------------- % 0.15/0.52 %-------------------------------------------------------------------------- % 0.15/0.52 % File : SYN555-1 : TPTP v8.2.0. Released v2.5.0. % 0.15/0.52 % Domain : Syntactic % 0.15/0.52 % Problem : Harrison problem 2162 % 0.15/0.52 % Version : Especial. % 0.15/0.52 % English : % 0.15/0.52 % 0.15/0.52 % Refs : [Har01] Email to G. Sutcliffe % 0.15/0.52 % Source : [Har01] % 0.15/0.52 % Names : % 0.15/0.52 % 0.15/0.52 % Status : Unsatisfiable % 0.15/0.52 % Rating : 0.00 v5.3.0, 0.05 v5.2.0, 0.00 v2.5.0 % 0.15/0.52 % Syntax : Number of clauses : 12 ( 6 unt; 0 nHn; 8 RR) % 0.15/0.52 % Number of literals : 26 ( 0 equ; 15 neg) % 0.15/0.52 % Maximal clause size : 4 ( 2 avg) % 0.15/0.52 % Maximal term depth : 3 ( 1 avg) % 0.15/0.52 % Number of predicates : 3 ( 3 usr; 0 prp; 2-2 aty) % 0.15/0.52 % Number of functors : 6 ( 6 usr; 4 con; 0-3 aty) % 0.15/0.52 % Number of variables : 28 ( 0 sgn) % 0.15/0.52 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.15/0.52 % 0.15/0.52 % Comments : % 0.15/0.52 %-------------------------------------------------------------------------- % 0.15/0.52 cnf(p2_1,negated_conjecture, % 0.15/0.52 p2(X0,X0) ). % 0.15/0.52 % 0.15/0.52 cnf(p4_2,negated_conjecture, % 0.15/0.52 p4(X12,X12) ). % 0.15/0.52 % 0.15/0.52 cnf(p3_3,negated_conjecture, % 0.15/0.52 p3(X3,X3) ). % 0.15/0.52 % 0.15/0.52 cnf(p4_4,negated_conjecture, % 0.15/0.52 p4(f5(c7,c10,c9),c9) ). % 0.15/0.52 % 0.15/0.52 cnf(not_p4_5,negated_conjecture, % 0.15/0.52 ~ p4(f5(c7,c10,c8),c8) ). % 0.15/0.52 % 0.15/0.52 cnf(p4_6,negated_conjecture, % 0.15/0.52 p4(f5(c7,X24,c8),f5(c7,X24,c9)) ). % 0.15/0.52 % 0.15/0.52 cnf(p2_7,negated_conjecture, % 0.15/0.52 ( p2(X1,X2) % 0.15/0.52 | ~ p2(X0,X1) % 0.15/0.52 | ~ p2(X0,X2) ) ). % 0.15/0.52 % 0.15/0.52 cnf(p4_8,negated_conjecture, % 0.15/0.52 ( p4(X13,X14) % 0.15/0.52 | ~ p4(X12,X13) % 0.15/0.52 | ~ p4(X12,X14) ) ). % 0.15/0.52 % 0.15/0.52 cnf(p3_9,negated_conjecture, % 0.15/0.52 ( p3(X4,X5) % 0.15/0.52 | ~ p3(X3,X4) % 0.15/0.52 | ~ p3(X3,X5) ) ). % 0.15/0.52 % 0.15/0.52 cnf(p3_10,negated_conjecture, % 0.15/0.52 ( p3(f6(X6,X7,X8),f6(X9,X10,X11)) % 0.15/0.52 | ~ p4(X8,X11) % 0.15/0.52 | ~ p4(X7,X10) % 0.15/0.52 | ~ p3(X6,X9) ) ). % 0.15/0.52 % 0.15/0.52 cnf(p4_11,negated_conjecture, % 0.15/0.52 ( p4(f5(X15,X16,X17),f5(X18,X19,X20)) % 0.15/0.52 | ~ p3(X16,X19) % 0.15/0.52 | ~ p4(X17,X20) % 0.15/0.52 | ~ p2(X15,X18) ) ). % 0.15/0.52 % 0.15/0.52 cnf(p4_12,negated_conjecture, % 0.15/0.52 ( p4(f5(c7,X21,X22),X22) % 0.15/0.52 | ~ p4(f5(c7,X21,X23),X23) % 0.15/0.52 | ~ p4(f5(c7,f6(X21,X23,X22),X23),f5(c7,f6(X21,X23,X22),X22)) ) ). % 0.15/0.52 % 0.15/0.52 %-------------------------------------------------------------------------- % 0.15/0.52 %------------------------------------------- % 0.15/0.52 % Proof found % 0.15/0.52 % SZS status Theorem for theBenchmark % 0.15/0.52 % SZS output start Proof % 0.15/0.52 %ClaNum:12(EqnAxiom:0) % 0.15/0.52 %VarNum:64(SingletonVarNum:28) % 0.15/0.52 %MaxLitNum:4 % 0.15/0.52 %MaxfuncDepth:2 % 0.15/0.52 %SharedTerms:8 % 0.15/0.52 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 % 0.15/0.52 %singleGoalClaCount:6 % 0.15/0.52 [4]P2(f5(a1,a2,a3),a3) % 0.15/0.52 [6]~P2(f5(a1,a2,a4),a4) % 0.15/0.52 [1]P1(x11,x11) % 0.15/0.53 [2]P2(x21,x21) % 0.15/0.53 [3]P3(x31,x31) % 0.15/0.53 [5]P2(f5(a1,x51,a4),f5(a1,x51,a3)) % 0.15/0.53 [7]~P1(x73,x71)+P1(x71,x72)+~P1(x73,x72) % 0.15/0.53 [8]~P2(x83,x81)+P2(x81,x82)+~P2(x83,x82) % 0.15/0.53 [9]~P3(x93,x91)+P3(x91,x92)+~P3(x93,x92) % 0.15/0.53 [12]P2(f5(a1,x121,x122),x122)+~P2(f5(a1,x121,x123),x123)+~P2(f5(a1,f6(x121,x123,x122),x123),f5(a1,f6(x121,x123,x122),x122)) % 0.15/0.53 [10]~P1(x101,x104)+~P2(x103,x106)+~P3(x102,x105)+P2(f5(x101,x102,x103),f5(x104,x105,x106)) % 0.15/0.53 [11]~P2(x113,x116)+~P2(x112,x115)+~P3(x111,x114)+P3(f6(x111,x112,x113),f6(x114,x115,x116)) % 0.15/0.53 %EqnAxiom % 0.15/0.53 % 0.15/0.53 %------------------------------------------- % 0.15/0.53 cnf(19,plain, % 0.15/0.53 ($false), % 0.15/0.53 inference(scs_inference,[],[5,2,6,4,8,12]), % 0.15/0.53 ['proof']). % 0.15/0.53 % SZS output end Proof % 0.15/0.53 % Total time :0.000000s %------------------------------------------------------------------------------