%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN601-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 : n020.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:04 EDT 2024 % Result : Unsatisfiable 117.33s 117.36s % Output : CNFRefutation 117.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.15 % Problem : SYN601-1 : TPTP v8.2.0. Released v2.5.0. % 0.09/0.15 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.37 % Computer : n020.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Sun Jun 23 21:22:54 EDT 2024 % 0.14/0.37 % CPUTime : % 0.56/0.59 start to proof:theBenchmark % 117.33/117.34 %------------------------------------------- % 117.33/117.34 % File :CSE---1.7 % 117.33/117.34 % Problem :theBenchmark % 117.33/117.34 % Transform :cnf % 117.33/117.34 % Format :tptp:raw % 117.33/117.34 % Command :java -jar mcs_scs.jar %d %s % 117.33/117.34 % 117.33/117.34 % Result :Theorem 116.650000s % 117.33/117.34 % Output :CNFRefutation 116.650000s % 117.33/117.34 %------------------------------------------- % 117.33/117.36 %-------------------------------------------------------------------------- % 117.33/117.36 % File : SYN601-1 : TPTP v8.2.0. Released v2.5.0. % 117.33/117.36 % Domain : Syntactic % 117.33/117.36 % Problem : Harrison problem 3799 % 117.33/117.36 % Version : Especial. % 117.33/117.36 % English : % 117.33/117.36 % 117.33/117.36 % Refs : [Har01] Email to G. Sutcliffe % 117.33/117.36 % Source : [Har01] % 117.33/117.36 % Names : % 117.33/117.36 % 117.33/117.36 % Status : Unsatisfiable % 117.33/117.36 % Rating : 0.18 v8.2.0, 0.14 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.29 v6.0.0, 0.44 v5.4.0, 0.39 v5.3.0, 0.40 v5.2.0, 0.54 v5.1.0, 0.44 v5.0.0, 0.40 v4.0.1, 0.57 v3.7.0, 0.43 v3.4.0, 0.20 v3.3.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0 % 117.33/117.36 % Syntax : Number of clauses : 30 ( 12 unt; 0 nHn; 25 RR) % 117.33/117.36 % Number of literals : 63 ( 0 equ; 35 neg) % 117.33/117.36 % Maximal clause size : 4 ( 2 avg) % 117.33/117.36 % Maximal term depth : 5 ( 1 avg) % 117.33/117.36 % Number of predicates : 8 ( 8 usr; 0 prp; 2-2 aty) % 117.33/117.36 % Number of functors : 16 ( 16 usr; 6 con; 0-3 aty) % 117.33/117.36 % Number of variables : 60 ( 0 sgn) % 117.33/117.36 % SPC : CNF_UNS_RFO_NEQ_HRN % 117.33/117.36 % 117.33/117.36 % Comments : % 117.33/117.36 %-------------------------------------------------------------------------- % 117.33/117.36 cnf(p10_1,negated_conjecture, % 117.33/117.36 p10(X0,X0) ). % 117.33/117.36 % 117.33/117.36 cnf(p9_2,negated_conjecture, % 117.33/117.36 p9(X52,X52) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_3,negated_conjecture, % 117.33/117.36 p3(X37,X37) ). % 117.33/117.36 % 117.33/117.36 cnf(p2_4,negated_conjecture, % 117.33/117.36 p2(X30,X30) ). % 117.33/117.36 % 117.33/117.36 cnf(p12_5,negated_conjecture, % 117.33/117.36 p12(X11,X11) ). % 117.33/117.36 % 117.33/117.36 cnf(p17_6,negated_conjecture, % 117.33/117.36 p17(c22,c23) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_7,negated_conjecture, % 117.33/117.36 p3(c22,c23) ). % 117.33/117.36 % 117.33/117.36 cnf(p18_8,negated_conjecture, % 117.33/117.36 p18(c22,f8(c21)) ). % 117.33/117.36 % 117.33/117.36 cnf(p17_9,negated_conjecture, % 117.33/117.36 p17(f5(f6(f7(c20))),f4(c21)) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_10,negated_conjecture, % 117.33/117.36 ( p3(f8(X50),f8(X51)) % 117.33/117.36 | ~ p2(X50,X51) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p10_11,negated_conjecture, % 117.33/117.36 ( p10(f16(X9),f16(X10)) % 117.33/117.36 | ~ p3(X9,X10) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_12,negated_conjecture, % 117.33/117.36 ( p3(f15(X40),f15(X41)) % 117.33/117.36 | ~ p2(X40,X41) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_13,negated_conjecture, % 117.33/117.36 ( p3(f4(X42),f4(X43)) % 117.33/117.36 | ~ p2(X42,X43) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_14,negated_conjecture, % 117.33/117.36 ( p3(f5(X44),f5(X45)) % 117.33/117.36 | ~ p3(X44,X45) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_15,negated_conjecture, % 117.33/117.36 ( p3(f6(X46),f6(X47)) % 117.33/117.36 | ~ p3(X46,X47) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_16,negated_conjecture, % 117.33/117.36 ( p3(f7(X48),f7(X49)) % 117.33/117.36 | ~ p3(X48,X49) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p10_17,negated_conjecture, % 117.33/117.36 ( p10(X1,X2) % 117.33/117.36 | ~ p10(X0,X1) % 117.33/117.36 | ~ p10(X0,X2) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p9_18,negated_conjecture, % 117.33/117.36 ( p9(X53,X54) % 117.33/117.36 | ~ p9(X52,X53) % 117.33/117.36 | ~ p9(X52,X54) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p3_19,negated_conjecture, % 117.33/117.36 ( p3(X38,X39) % 117.33/117.36 | ~ p3(X37,X38) % 117.33/117.36 | ~ p3(X37,X39) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p2_20,negated_conjecture, % 117.33/117.36 ( p2(X31,X32) % 117.33/117.36 | ~ p2(X30,X31) % 117.33/117.36 | ~ p2(X30,X32) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p12_21,negated_conjecture, % 117.33/117.36 ( p12(X12,X13) % 117.33/117.36 | ~ p12(X11,X12) % 117.33/117.36 | ~ p12(X11,X13) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p19_22,negated_conjecture, % 117.33/117.36 p19(c21,f11(f13(f15(c21),f14(f4(c21),c22)),c24,c25)) ). % 117.33/117.36 % 117.33/117.36 cnf(not_p19_23,negated_conjecture, % 117.33/117.36 ~ p19(c21,f11(f13(f15(c21),f14(f4(c21),c23)),c24,c25)) ). % 117.33/117.36 % 117.33/117.36 cnf(p19_24,negated_conjecture, % 117.33/117.36 ( p19(X26,X27) % 117.33/117.36 | ~ p19(X29,X28) % 117.33/117.36 | ~ p2(X29,X26) % 117.33/117.36 | ~ p10(X28,X27) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p17_25,negated_conjecture, % 117.33/117.36 ( p17(X18,X19) % 117.33/117.36 | ~ p3(X20,X18) % 117.33/117.36 | ~ p3(X21,X19) % 117.33/117.36 | ~ p17(X20,X21) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p18_26,negated_conjecture, % 117.33/117.36 ( p18(X22,X23) % 117.33/117.36 | ~ p3(X24,X22) % 117.33/117.36 | ~ p3(X25,X23) % 117.33/117.36 | ~ p18(X24,X25) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p12_27,negated_conjecture, % 117.33/117.36 ( p12(f14(X14,X15),f14(X16,X17)) % 117.33/117.36 | ~ p3(X14,X16) % 117.33/117.36 | ~ p3(X15,X17) ) ). % 117.33/117.36 % 117.33/117.36 cnf(p2_28,negated_conjecture, % 117.33/117.36 ( p2(f13(X33,X34),f13(X35,X36)) % 117.33/117.36 | ~ p12(X34,X36) % 117.33/117.36 | ~ p3(X33,X35) ) ). % 117.33/117.36 % 117.33/117.36 cnf(not_p10_29,negated_conjecture, % 117.33/117.36 ~ p10(f11(f13(f15(c21),f14(f4(c21),c23)),c24,c25),f16(f5(c20))) ). % 117.33/117.36 % 117.33/117.36 cnf(p10_30,negated_conjecture, % 117.33/117.36 ( p10(f11(X3,X4,X5),f11(X6,X7,X8)) % 117.33/117.36 | ~ p2(X3,X6) % 117.33/117.36 | ~ p9(X4,X7) % 117.33/117.36 | ~ p10(X5,X8) ) ). % 117.33/117.36 % 117.33/117.36 %-------------------------------------------------------------------------- % 117.33/117.36 %------------------------------------------- % 117.33/117.36 % Proof found % 117.33/117.36 % SZS status Theorem for theBenchmark % 117.33/117.36 % SZS output start Proof % 117.33/117.37 %ClaNum:30(EqnAxiom:0) % 117.33/117.37 %VarNum:120(SingletonVarNum:60) % 117.33/117.37 %MaxLitNum:4 % 117.33/117.37 %MaxfuncDepth:4 % 117.33/117.37 %SharedTerms:27 % 117.33/117.37 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 % 117.33/117.37 %singleGoalClaCount:12 % 117.33/117.37 [1]P1(a1,a4) % 117.33/117.37 [2]P2(a1,a4) % 117.33/117.37 [8]P6(a1,f5(a2)) % 117.33/117.37 [9]P2(f8(f7(f6(a3))),f9(a2)) % 117.33/117.37 [10]P7(a2,f15(f12(f10(a2),f11(f9(a2),a1)),a13,a14)) % 117.33/117.37 [11]~P7(a2,f15(f12(f10(a2),f11(f9(a2),a4)),a13,a14)) % 117.33/117.37 [12]~P3(f15(f12(f10(a2),f11(f9(a2),a4)),a13,a14),f16(f8(a3))) % 117.33/117.37 [3]P3(x31,x31) % 117.33/117.37 [4]P8(x41,x41) % 117.33/117.37 [5]P1(x51,x51) % 117.33/117.37 [6]P5(x61,x61) % 117.33/117.37 [7]P4(x71,x71) % 117.33/117.37 [13]~P1(x131,x132)+P3(f16(x131),f16(x132)) % 117.33/117.37 [14]~P5(x141,x142)+P1(f5(x141),f5(x142)) % 117.33/117.37 [15]~P1(x151,x152)+P1(f6(x151),f6(x152)) % 117.33/117.37 [16]~P1(x161,x162)+P1(f7(x161),f7(x162)) % 117.33/117.37 [17]~P1(x171,x172)+P1(f8(x171),f8(x172)) % 117.33/117.37 [18]~P5(x181,x182)+P1(f9(x181),f9(x182)) % 117.33/117.37 [19]~P5(x191,x192)+P1(f10(x191),f10(x192)) % 117.33/117.37 [20]~P3(x203,x201)+P3(x201,x202)+~P3(x203,x202) % 117.33/117.37 [21]~P8(x213,x211)+P8(x211,x212)+~P8(x213,x212) % 117.33/117.37 [22]~P1(x223,x221)+P1(x221,x222)+~P1(x223,x222) % 117.33/117.37 [23]~P5(x233,x231)+P5(x231,x232)+~P5(x233,x232) % 117.33/117.37 [24]~P4(x243,x241)+P4(x241,x242)+~P4(x243,x242) % 117.33/117.37 [28]~P1(x281,x283)+~P4(x282,x284)+P5(f12(x281,x282),f12(x283,x284)) % 117.33/117.37 [29]~P1(x292,x294)+~P1(x291,x293)+P4(f11(x291,x292),f11(x293,x294)) % 117.33/117.37 [25]~P2(x254,x253)+P2(x251,x252)+~P1(x253,x252)+~P1(x254,x251) % 117.33/117.37 [26]~P6(x264,x263)+P6(x261,x262)+~P1(x263,x262)+~P1(x264,x261) % 117.33/117.37 [27]~P7(x274,x273)+P7(x271,x272)+~P3(x273,x272)+~P5(x274,x271) % 117.33/117.37 [30]~P3(x303,x306)+~P8(x302,x305)+~P5(x301,x304)+P3(f15(x301,x302,x303),f15(x304,x305,x306)) % 117.33/117.37 %EqnAxiom % 117.33/117.37 % 117.33/117.37 %------------------------------------------- % 117.40/117.39 cnf(385,plain, % 117.40/117.39 (P4(f11(f6(a1),f6(a1)),f11(f6(a4),f6(a4)))), % 117.40/117.39 inference(scs_inference,[],[1,15,29])). % 117.40/117.39 cnf(390,plain, % 117.40/117.39 (P5(f12(f6(a1),f11(f6(a1),f6(a1))),f12(f6(a4),f11(f6(a4),f6(a4))))), % 117.40/117.39 inference(scs_inference,[],[1,385,15,28])). % 117.40/117.39 cnf(454,plain, % 117.40/117.39 (P5(f12(f6(a4),f11(f6(a4),f6(a4))),f12(f6(a1),f11(f6(a1),f6(a1))))), % 117.40/117.39 inference(scs_inference,[],[390,6,23])). % 117.40/117.39 cnf(544,plain, % 117.40/117.39 (P1(f8(f7(a1)),f8(f7(a4)))), % 117.40/117.39 inference(scs_inference,[],[1,16,17])). % 117.40/117.39 cnf(589,plain, % 117.40/117.39 (P1(f8(f7(a4)),f8(f7(a1)))), % 117.40/117.39 inference(scs_inference,[],[544,5,22])). % 117.40/117.39 cnf(645,plain, % 117.40/117.39 (P4(f11(f7(a1),f7(a1)),f11(f7(a4),f7(a4)))), % 117.40/117.39 inference(scs_inference,[],[1,16,29])). % 117.40/117.39 cnf(646,plain, % 117.40/117.39 (P4(f11(f7(a4),f7(a4)),f11(f7(a1),f7(a1)))), % 117.40/117.39 inference(scs_inference,[],[645,7,24])). % 117.40/117.39 cnf(945,plain, % 117.40/117.39 (P4(f11(f8(a1),f8(a1)),f11(f8(a4),f8(a4)))), % 117.40/117.39 inference(scs_inference,[],[1,17,29])). % 117.40/117.39 cnf(946,plain, % 117.40/117.39 (P4(f11(f8(a4),f8(a4)),f11(f8(a1),f8(a1)))), % 117.40/117.39 inference(scs_inference,[],[945,7,24])). % 117.40/117.39 cnf(1937,plain, % 117.40/117.39 (P5(f12(a4,f11(f7(a4),f7(a4))),f12(a4,f11(f7(a1),f7(a1))))), % 117.40/117.39 inference(scs_inference,[],[1,646,22,28])). % 117.40/117.39 cnf(1939,plain, % 117.40/117.39 (P5(f12(a4,f11(f8(a4),f8(a4))),f12(a4,f11(f8(a1),f8(a1))))), % 117.40/117.39 inference(scs_inference,[],[1,946,22,28])). % 117.40/117.39 cnf(5223,plain, % 117.40/117.39 (~P3(f15(f12(f10(a2),f11(f9(a2),a1)),a13,a14),f15(f12(f10(a2),f11(f9(a2),a4)),a13,a14))), % 117.40/117.39 inference(scs_inference,[],[1,10,11,454,7,6,13,14,15,16,17,18,19,28,29,27])). % 117.40/117.39 cnf(5591,plain, % 117.40/117.39 (P1(f7(f8(f7(a4))),f7(f8(f7(a1))))), % 117.40/117.39 inference(scs_inference,[],[589,1939,15,13,18,14,19,17,16])). % 117.40/117.39 cnf(5629,plain, % 117.40/117.39 (P4(f11(x56291,a1),f11(x56291,a4))), % 117.40/117.39 inference(scs_inference,[],[1,5591,1937,5,15,13,18,14,19,17,16,29])). % 117.40/117.39 cnf(6673,plain, % 117.40/117.39 (P5(f12(x66731,f11(x66732,a1)),f12(x66731,f11(x66732,a4)))), % 117.40/117.39 inference(scs_inference,[],[5,5629,28])). % 117.40/117.39 cnf(6870,plain, % 117.40/117.39 ($false), % 117.40/117.39 inference(scs_inference,[],[4,3,6673,5223,30]), % 117.40/117.39 ['proof']). % 117.40/117.40 % SZS output end Proof % 117.40/117.40 % Total time :116.650000s %------------------------------------------------------------------------------