%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN580-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 : n028.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:01 EDT 2024 % Result : Unsatisfiable 0.56s 0.76s % Output : CNFRefutation 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN580-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.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 23:20:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.48/0.58 start to proof:theBenchmark % 0.56/0.75 %------------------------------------------- % 0.56/0.75 % File :CSE---1.7 % 0.56/0.75 % Problem :theBenchmark % 0.56/0.75 % Transform :cnf % 0.56/0.75 % Format :tptp:raw % 0.56/0.75 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.75 % 0.56/0.75 % Result :Theorem 0.130000s % 0.56/0.75 % Output :CNFRefutation 0.130000s % 0.56/0.75 %------------------------------------------- % 0.56/0.76 %-------------------------------------------------------------------------- % 0.56/0.76 % File : SYN580-1 : TPTP v8.2.0. Released v2.5.0. % 0.56/0.76 % Domain : Syntactic % 0.56/0.76 % Problem : Harrison problem 3332 % 0.56/0.76 % Version : Especial. % 0.56/0.76 % English : % 0.56/0.76 % 0.56/0.76 % Refs : [Har01] Email to G. Sutcliffe % 0.56/0.76 % Source : [Har01] % 0.56/0.76 % Names : % 0.56/0.76 % 0.56/0.76 % Status : Unsatisfiable % 0.56/0.76 % Rating : 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v2.5.0 % 0.56/0.76 % Syntax : Number of clauses : 23 ( 8 unt; 2 nHn; 17 RR) % 0.56/0.76 % Number of literals : 54 ( 0 equ; 30 neg) % 0.56/0.76 % Maximal clause size : 5 ( 2 avg) % 0.56/0.76 % Maximal term depth : 2 ( 1 avg) % 0.56/0.76 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty) % 0.56/0.76 % Number of functors : 8 ( 8 usr; 5 con; 0-1 aty) % 0.56/0.76 % Number of variables : 46 ( 0 sgn) % 0.56/0.76 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.56/0.76 % 0.56/0.76 % Comments : % 0.56/0.76 %-------------------------------------------------------------------------- % 0.56/0.76 cnf(p10_1,negated_conjecture, % 0.56/0.76 p10(X0,X0) ). % 0.56/0.76 % 0.56/0.76 cnf(p7_2,negated_conjecture, % 0.56/0.76 p7(X19,X19) ). % 0.56/0.76 % 0.56/0.76 cnf(p4_3,negated_conjecture, % 0.56/0.76 p4(X12,X12) ). % 0.56/0.76 % 0.56/0.76 cnf(p2_4,negated_conjecture, % 0.56/0.76 p2(X7,X7) ). % 0.56/0.76 % 0.56/0.76 cnf(p11_5,negated_conjecture, % 0.56/0.76 p11(c15,c16) ). % 0.56/0.76 % 0.56/0.76 cnf(p9_6,negated_conjecture, % 0.56/0.76 p9(c12,c13) ). % 0.56/0.76 % 0.56/0.76 cnf(p2_7,negated_conjecture, % 0.56/0.76 p2(c14,f3(c15)) ). % 0.56/0.76 % 0.56/0.76 cnf(not_p8_8,negated_conjecture, % 0.56/0.76 ~ p8(c12,c13,c14) ). % 0.56/0.76 % 0.56/0.76 cnf(p4_9,negated_conjecture, % 0.56/0.76 ( p4(f6(X17),f6(X18)) % 0.56/0.76 | ~ p2(X17,X18) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p2_10,negated_conjecture, % 0.56/0.76 ( p2(f3(X10),f3(X11)) % 0.56/0.76 | ~ p2(X10,X11) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p4_11,negated_conjecture, % 0.56/0.76 ( p4(f5(X15),f5(X16)) % 0.56/0.76 | ~ p2(X15,X16) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p10_12,negated_conjecture, % 0.56/0.76 ( p10(X1,X2) % 0.56/0.76 | ~ p10(X0,X1) % 0.56/0.76 | ~ p10(X0,X2) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p7_13,negated_conjecture, % 0.56/0.76 ( p7(X20,X21) % 0.56/0.76 | ~ p7(X19,X20) % 0.56/0.76 | ~ p7(X19,X21) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p4_14,negated_conjecture, % 0.56/0.76 ( p4(X13,X14) % 0.56/0.76 | ~ p4(X12,X13) % 0.56/0.76 | ~ p4(X12,X14) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p2_15,negated_conjecture, % 0.56/0.76 ( p2(X8,X9) % 0.56/0.76 | ~ p2(X7,X8) % 0.56/0.76 | ~ p2(X7,X9) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p8_16,negated_conjecture, % 0.56/0.76 ( p8(c12,X28,X29) % 0.56/0.76 | ~ p11(X29,c16) % 0.56/0.76 | ~ p9(c12,X28) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p9_17,negated_conjecture, % 0.56/0.76 ( p9(c12,f5(X31)) % 0.56/0.76 | p8(c12,X30,X31) % 0.56/0.76 | ~ p9(c12,X30) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p9_18,negated_conjecture, % 0.56/0.76 ( p9(c12,f6(X31)) % 0.56/0.76 | p8(c12,X30,f3(X31)) % 0.56/0.76 | ~ p9(c12,X30) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p9_19,negated_conjecture, % 0.56/0.76 ( p9(X32,X33) % 0.56/0.76 | ~ p7(X35,X32) % 0.56/0.76 | ~ p9(X35,X34) % 0.56/0.76 | ~ p4(X34,X33) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p11_20,negated_conjecture, % 0.56/0.76 ( p11(X3,X4) % 0.56/0.76 | ~ p11(X6,X5) % 0.56/0.76 | ~ p2(X6,X3) % 0.56/0.76 | ~ p10(X5,X4) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p8_21,negated_conjecture, % 0.56/0.76 ( p8(c12,X30,X31) % 0.56/0.76 | ~ p9(c12,X30) % 0.56/0.76 | ~ p8(c12,f5(X31),f3(X31)) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p8_22,negated_conjecture, % 0.56/0.76 ( p8(c12,X30,f3(X31)) % 0.56/0.76 | ~ p9(c12,X30) % 0.56/0.76 | ~ p8(c12,f6(X31),X31) ) ). % 0.56/0.76 % 0.56/0.76 cnf(p8_23,negated_conjecture, % 0.56/0.76 ( p8(X22,X23,X24) % 0.56/0.76 | ~ p2(X25,X24) % 0.56/0.76 | ~ p4(X26,X23) % 0.56/0.76 | ~ p7(X27,X22) % 0.56/0.76 | ~ p8(X27,X26,X25) ) ). % 0.56/0.76 % 0.56/0.76 %-------------------------------------------------------------------------- % 0.56/0.76 %------------------------------------------- % 0.56/0.76 % Proof found % 0.56/0.76 % SZS status Theorem for theBenchmark % 0.56/0.76 % SZS output start Proof % 0.56/0.76 %ClaNum:23(EqnAxiom:0) % 0.56/0.76 %VarNum:94(SingletonVarNum:46) % 0.56/0.76 %MaxLitNum:5 % 0.56/0.76 %MaxfuncDepth:1 % 0.56/0.76 %SharedTerms:10 % 0.56/0.76 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 % 0.56/0.76 %singleGoalClaCount:8 % 0.56/0.76 [1]P1(a1,a5) % 0.56/0.76 [2]P3(a2,a3) % 0.56/0.76 [8]~P7(a2,a3,a4) % 0.56/0.76 [7]P6(a4,f6(a1)) % 0.56/0.76 [3]P2(x31,x31) % 0.56/0.76 [4]P4(x41,x41) % 0.56/0.76 [5]P5(x51,x51) % 0.56/0.76 [6]P6(x61,x61) % 0.56/0.76 [9]~P6(x91,x92)+P5(f7(x91),f7(x92)) % 0.56/0.76 [10]~P6(x101,x102)+P5(f8(x101),f8(x102)) % 0.56/0.76 [11]~P6(x111,x112)+P6(f6(x111),f6(x112)) % 0.56/0.76 [19]P7(a2,x191,x192)+~P1(x192,a5)+~P3(a2,x191) % 0.56/0.76 [18]P7(a2,x181,x182)+~P3(a2,x181)+P3(a2,f8(x182)) % 0.56/0.76 [20]~P3(a2,x202)+P7(a2,x202,f6(x201))+P3(a2,f7(x201)) % 0.56/0.76 [21]~P3(a2,x211)+~P7(a2,f7(x212),x212)+P7(a2,x211,f6(x212)) % 0.56/0.76 [22]P7(a2,x221,x222)+~P3(a2,x221)+~P7(a2,f8(x222),f6(x222)) % 0.56/0.76 [12]~P2(x123,x121)+P2(x121,x122)+~P2(x123,x122) % 0.56/0.76 [13]~P4(x133,x131)+P4(x131,x132)+~P4(x133,x132) % 0.56/0.76 [14]~P5(x143,x141)+P5(x141,x142)+~P5(x143,x142) % 0.56/0.76 [15]~P6(x153,x151)+P6(x151,x152)+~P6(x153,x152) % 0.56/0.76 [16]~P1(x164,x163)+P1(x161,x162)+~P2(x163,x162)+~P6(x164,x161) % 0.58/0.76 [17]~P3(x173,x174)+P3(x171,x172)+~P4(x173,x171)+~P5(x174,x172) % 0.58/0.76 [23]~P7(x234,x235,x236)+P7(x231,x232,x233)+~P4(x234,x231)+~P5(x235,x232)+~P6(x236,x233) % 0.58/0.76 %EqnAxiom % 0.58/0.76 % 0.58/0.76 %------------------------------------------- % 0.58/0.77 cnf(27,plain, % 0.58/0.77 (P6(f6(a1),a4)), % 0.58/0.77 inference(scs_inference,[],[7,6,15])). % 0.58/0.77 cnf(32,plain, % 0.58/0.77 (~P7(x321,x322,a4)+P7(x321,x322,f6(a1))), % 0.58/0.77 inference(scs_inference,[],[3,5,7,4,6,15,16,23])). % 0.58/0.77 cnf(35,plain, % 0.58/0.77 (~P7(a2,a3,f6(a1))), % 0.58/0.77 inference(scs_inference,[],[27,4,8,5,23])). % 0.58/0.77 cnf(39,plain, % 0.58/0.77 (~P7(a2,f7(a1),a1)), % 0.58/0.77 inference(scs_inference,[],[2,27,4,8,5,23,21])). % 0.58/0.77 cnf(50,plain, % 0.58/0.77 (P7(a2,f8(f6(a1)),f6(x501))+P3(a2,f7(x501))), % 0.58/0.77 inference(scs_inference,[],[2,35,20,18])). % 0.58/0.77 cnf(51,plain, % 0.58/0.77 (P3(a2,f7(f6(a1)))), % 0.58/0.77 inference(scs_inference,[],[2,35,50,22])). % 0.58/0.77 cnf(57,plain, % 0.58/0.77 (P3(a2,f7(a4))), % 0.58/0.77 inference(scs_inference,[],[27,4,51,9,17])). % 0.58/0.77 cnf(60,plain, % 0.58/0.77 (~P7(x601,f7(f6(a1)),f6(a1))+P7(x601,f7(a4),a4)), % 0.58/0.77 inference(scs_inference,[],[27,4,9,23])). % 0.58/0.77 cnf(65,plain, % 0.58/0.77 (~P3(x651,f8(f6(a1)))+P3(x651,f8(a4))), % 0.58/0.77 inference(scs_inference,[],[27,4,10,17])). % 0.58/0.77 cnf(66,plain, % 0.58/0.77 (P3(a2,f8(a4))+P7(a2,f7(a4),f6(a1))), % 0.58/0.77 inference(scs_inference,[],[57,65,18])). % 0.58/0.77 cnf(67,plain, % 0.58/0.77 (P7(a2,f7(a4),f6(a1))+P7(a2,f8(a4),f6(x671))+P3(a2,f7(x671))), % 0.58/0.77 inference(scs_inference,[],[66,20])). % 0.58/0.77 cnf(68,plain, % 0.58/0.77 (P7(a2,f7(a4),a4)+P3(a2,f7(x681))+P7(a2,f8(a4),f6(x681))), % 0.58/0.77 inference(scs_inference,[],[4,5,27,67,23])). % 0.58/0.77 cnf(87,plain, % 0.58/0.77 (~P7(x871,x872,f6(f6(a1)))+P7(x871,x872,f6(a4))), % 0.58/0.77 inference(scs_inference,[],[27,4,5,11,23])). % 0.58/0.77 cnf(91,plain, % 0.58/0.77 (P3(a2,f8(a4))), % 0.58/0.77 inference(scs_inference,[],[35,2,32,18])). % 0.58/0.77 cnf(94,plain, % 0.58/0.77 (~P7(a2,f7(f6(a1)),a4)+P7(a2,f8(a4),f6(f6(a1)))), % 0.58/0.77 inference(scs_inference,[],[91,32,21])). % 0.58/0.77 cnf(97,plain, % 0.58/0.77 (~P7(a2,f8(a4),f6(a4))), % 0.58/0.77 inference(scs_inference,[],[35,2,32,22])). % 0.58/0.77 cnf(98,plain, % 0.58/0.77 (~P7(a2,f8(a4),f6(f6(a1)))), % 0.58/0.77 inference(scs_inference,[],[97,87])). % 0.58/0.77 cnf(101,plain, % 0.58/0.77 (~P7(a2,f7(a4),a4)), % 0.58/0.77 inference(scs_inference,[],[97,91,87,94,21])). % 0.58/0.77 cnf(103,plain, % 0.58/0.77 (~P7(a2,f7(f6(a1)),f6(a1))), % 0.58/0.77 inference(scs_inference,[],[97,91,87,94,21,60])). % 0.58/0.77 cnf(105,plain, % 0.58/0.77 (P7(a2,f8(a4),f6(x1051))+P3(a2,f7(x1051))), % 0.58/0.77 inference(scs_inference,[],[101,68])). % 0.58/0.77 cnf(106,plain, % 0.58/0.77 (P3(a2,f7(a1))), % 0.58/0.77 inference(scs_inference,[],[98,103,105,20])). % 0.58/0.77 cnf(107,plain, % 0.58/0.77 ($false), % 0.58/0.77 inference(scs_inference,[],[1,106,39,19]), % 0.58/0.77 ['proof']). % 0.58/0.77 % SZS output end Proof % 0.58/0.77 % Total time :0.130000s %------------------------------------------------------------------------------