%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS015-1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n005.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 10:08:15 EDT 2024 % Result : Unsatisfiable 116.19s 116.72s % Output : CNFRefutation 116.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS015-1 : TPTP v8.2.0. Released v2.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n005.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 : Wed Jun 19 12:09:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.58 start to proof:theBenchmark % 116.19/116.69 %------------------------------------------- % 116.19/116.69 % File :CSE---1.7 % 116.19/116.69 % Problem :theBenchmark % 116.19/116.69 % Transform :cnf % 116.19/116.69 % Format :tptp:raw % 116.19/116.69 % Command :java -jar mcs_scs.jar %d %s % 116.19/116.69 % 116.19/116.69 % Result :Theorem 115.600000s % 116.19/116.69 % Output :CNFRefutation 115.600000s % 116.19/116.69 %------------------------------------------- % 116.19/116.71 %-------------------------------------------------------------------------- % 116.19/116.71 % File : KRS015-1 : TPTP v8.2.0. Released v2.0.0. % 116.19/116.71 % Domain : Knowledge Representation % 116.19/116.71 % Problem : Paramasivam problem T-Box 5b % 116.19/116.71 % Version : Especial. % 116.19/116.71 % English : e exists. % 116.19/116.71 % 116.19/116.71 % Refs : [PP95] Paramasivam & Plaisted (1995), Automated Deduction Tec % 116.19/116.71 % Source : [PP95] % 116.19/116.71 % Names : Problem 5(b) [PP95] % 116.19/116.71 % 116.19/116.71 % Status : Unsatisfiable % 116.19/116.71 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.00 v2.1.0 % 116.19/116.71 % Syntax : Number of clauses : 26 ( 1 unt; 10 nHn; 24 RR) % 116.19/116.71 % Number of literals : 91 ( 0 equ; 47 neg) % 116.19/116.71 % Maximal clause size : 6 ( 3 avg) % 116.19/116.71 % Maximal term depth : 2 ( 1 avg) % 116.19/116.71 % Number of predicates : 9 ( 9 usr; 0 prp; 1-2 aty) % 116.19/116.71 % Number of functors : 9 ( 9 usr; 1 con; 0-1 aty) % 116.19/116.71 % Number of variables : 41 ( 8 sgn) % 116.19/116.71 % SPC : CNF_UNS_RFO_NEQ_NHN % 116.19/116.71 % 116.19/116.71 % Comments : % 116.19/116.71 %-------------------------------------------------------------------------- % 116.19/116.71 cnf(clause_1,negated_conjecture, % 116.19/116.71 e(exist) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_2,axiom, % 116.19/116.71 ( t2least(X1) % 116.19/116.71 | ~ c(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_3,axiom, % 116.19/116.71 ( c(X1) % 116.19/116.71 | ~ t2least(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_4,axiom, % 116.19/116.71 ( ~ t2least(X1) % 116.19/116.71 | ~ equalish(u1r2(X1),u1r1(X1)) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_5,axiom, % 116.19/116.71 ( t(X1,u1r1(X1)) % 116.19/116.71 | ~ t2least(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_6,axiom, % 116.19/116.71 ( t(X1,u1r2(X1)) % 116.19/116.71 | ~ t2least(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_7,axiom, % 116.19/116.71 ( t2least(X1) % 116.19/116.71 | equalish(X3,X2) % 116.19/116.71 | ~ t(X1,X3) % 116.19/116.71 | ~ t(X1,X2) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_8,axiom, % 116.19/116.71 ( t1most(X1) % 116.19/116.71 | ~ d(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_9,axiom, % 116.19/116.71 ( d(X1) % 116.19/116.71 | ~ t1most(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_10,axiom, % 116.19/116.71 ( equalish(X3,X2) % 116.19/116.71 | ~ t1most(X1) % 116.19/116.71 | ~ t(X1,X3) % 116.19/116.71 | ~ t(X1,X2) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_11,axiom, % 116.19/116.71 ( t1most(X1) % 116.19/116.71 | ~ equalish(u3r2(X1),u3r1(X1)) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_12,axiom, % 116.19/116.71 ( t1most(X1) % 116.19/116.71 | t(X1,u3r1(X1)) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_13,axiom, % 116.19/116.71 ( t1most(X1) % 116.19/116.71 | t(X1,u3r2(X1)) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_14,axiom, % 116.19/116.71 ( r(X1,u4r4(X1)) % 116.19/116.71 | ~ e(X1) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_15,axiom, % 116.19/116.71 ( s(X1,X4) % 116.19/116.71 | ~ e(X1) % 116.19/116.71 | ~ r(X1,X4) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_16,axiom, % 116.19/116.71 ( r(X1,X4) % 116.19/116.71 | ~ e(X1) % 116.19/116.71 | ~ s(X1,X4) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_17,axiom, % 116.19/116.71 ( d(X3) % 116.19/116.71 | ~ e(X1) % 116.19/116.71 | ~ s(X1,X3) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_18,axiom, % 116.19/116.71 ( c(X2) % 116.19/116.71 | ~ e(X1) % 116.19/116.71 | ~ r(X1,X2) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_19,axiom, % 116.19/116.71 ( e(X1) % 116.19/116.71 | s(X1,u4r3(X1)) % 116.19/116.71 | r(X1,u4r3(X1)) % 116.19/116.71 | ~ c(u4r1(X1)) % 116.19/116.71 | ~ d(u4r2(X1)) % 116.19/116.71 | ~ r(X1,X5) ) ). % 116.19/116.71 % 116.19/116.71 cnf(clause_20,axiom, % 116.19/116.71 ( e(X1) % 116.19/116.72 | ~ c(u4r1(X1)) % 116.19/116.72 | ~ d(u4r2(X1)) % 116.19/116.72 | ~ r(X1,u4r3(X1)) % 116.19/116.72 | ~ s(X1,u4r3(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 cnf(clause_21,axiom, % 116.19/116.72 ( e(X1) % 116.19/116.72 | s(X1,u4r2(X1)) % 116.19/116.72 | s(X1,u4r3(X1)) % 116.19/116.72 | r(X1,u4r3(X1)) % 116.19/116.72 | ~ c(u4r1(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 cnf(clause_22,axiom, % 116.19/116.72 ( e(X1) % 116.19/116.72 | s(X1,u4r2(X1)) % 116.19/116.72 | ~ c(u4r1(X1)) % 116.19/116.72 | ~ r(X1,u4r3(X1)) % 116.19/116.72 | ~ s(X1,u4r3(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 cnf(clause_23,axiom, % 116.19/116.72 ( e(X1) % 116.19/116.72 | r(X1,u4r1(X1)) % 116.19/116.72 | s(X1,u4r3(X1)) % 116.19/116.72 | r(X1,u4r3(X1)) % 116.19/116.72 | ~ d(u4r2(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 cnf(clause_24,axiom, % 116.19/116.72 ( e(X1) % 116.19/116.72 | r(X1,u4r1(X1)) % 116.19/116.72 | ~ d(u4r2(X1)) % 116.19/116.72 | ~ r(X1,u4r3(X1)) % 116.19/116.72 | ~ s(X1,u4r3(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 cnf(clause_25,axiom, % 116.19/116.72 ( e(X1) % 116.19/116.72 | r(X1,u4r1(X1)) % 116.19/116.72 | s(X1,u4r2(X1)) % 116.19/116.72 | s(X1,u4r3(X1)) % 116.19/116.72 | r(X1,u4r3(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 cnf(clause_26,axiom, % 116.19/116.72 ( e(X1) % 116.19/116.72 | r(X1,u4r1(X1)) % 116.19/116.72 | s(X1,u4r2(X1)) % 116.19/116.72 | ~ r(X1,u4r3(X1)) % 116.19/116.72 | ~ s(X1,u4r3(X1)) % 116.19/116.72 | ~ r(X1,X5) ) ). % 116.19/116.72 % 116.19/116.72 %-------------------------------------------------------------------------- % 116.19/116.72 %------------------------------------------- % 116.19/116.72 % Proof found % 116.19/116.72 % SZS status Theorem for theBenchmark % 116.19/116.72 % SZS output start Proof % 116.19/116.72 %ClaNum:26(EqnAxiom:0) % 116.19/116.72 %VarNum:141(SingletonVarNum:41) % 116.19/116.72 %MaxLitNum:6 % 116.19/116.72 %MaxfuncDepth:1 % 116.19/116.72 %SharedTerms:2 % 116.19/116.72 %goalClause: 1 % 116.19/116.72 %singleGoalClaCount:1 % 116.19/116.72 [1]P1(a1) % 116.19/116.72 [2]~P2(x21)+P4(x21) % 116.19/116.72 [3]~P4(x31)+P2(x31) % 116.19/116.72 [4]~P3(x41)+P5(x41) % 116.19/116.72 [5]~P5(x51)+P3(x51) % 116.19/116.72 [6]P5(x61)+P6(x61,f2(x61)) % 116.19/116.72 [7]P5(x71)+P6(x71,f3(x71)) % 116.19/116.72 [8]~P4(x81)+P6(x81,f4(x81)) % 116.19/116.72 [9]~P4(x91)+P6(x91,f5(x91)) % 116.19/116.72 [10]~P1(x101)+P7(x101,f6(x101)) % 116.19/116.72 [15]P5(x151)+~P8(f2(x151),f3(x151)) % 116.19/116.72 [16]~P4(x161)+~P8(f4(x161),f5(x161)) % 116.19/116.72 [11]~P7(x112,x111)+P2(x111)+~P1(x112) % 116.19/116.72 [12]~P9(x122,x121)+P3(x121)+~P1(x122) % 116.19/116.73 [13]~P1(x131)+~P9(x131,x132)+P7(x131,x132) % 116.19/116.73 [14]~P1(x141)+~P7(x141,x142)+P9(x141,x142) % 116.19/116.73 [17]~P6(x171,x173)+~P6(x171,x172)+P4(x171)+P8(x172,x173) % 116.19/116.73 [18]~P6(x183,x182)+~P6(x183,x181)+P8(x181,x182)+~P5(x183) % 116.19/116.73 [19]P1(x191)+~P7(x191,x192)+P7(x191,f7(x191))+P9(x191,f7(x191))+~P2(f8(x191))+~P3(f9(x191)) % 116.19/116.73 [20]P1(x201)+~P7(x201,x202)+P7(x201,f7(x201))+P7(x201,f8(x201))+P9(x201,f7(x201))+~P3(f9(x201)) % 116.19/116.73 [21]P1(x211)+~P7(x211,x212)+P7(x211,f7(x211))+P9(x211,f7(x211))+P9(x211,f9(x211))+~P2(f8(x211)) % 116.19/116.73 [22]P1(x221)+~P7(x221,x222)+P7(x221,f7(x221))+P7(x221,f8(x221))+P9(x221,f7(x221))+P9(x221,f9(x221)) % 116.19/116.73 [23]P1(x231)+~P7(x231,x232)+~P7(x231,f7(x231))+~P9(x231,f7(x231))+~P2(f8(x231))+~P3(f9(x231)) % 116.19/116.73 [24]P1(x241)+~P7(x241,x242)+P7(x241,f8(x241))+~P7(x241,f7(x241))+~P9(x241,f7(x241))+~P3(f9(x241)) % 116.19/116.73 [25]P1(x251)+~P7(x251,x252)+P9(x251,f9(x251))+~P7(x251,f7(x251))+~P9(x251,f7(x251))+~P2(f8(x251)) % 116.19/116.73 [26]P1(x261)+~P7(x261,x262)+P7(x261,f8(x261))+P9(x261,f9(x261))+~P7(x261,f7(x261))+~P9(x261,f7(x261)) % 116.19/116.73 %EqnAxiom % 116.19/116.73 % 116.19/116.73 %------------------------------------------- % 116.32/116.78 cnf(33,plain, % 116.32/116.78 (P2(f6(a1))), % 116.32/116.78 inference(scs_inference,[],[1,10,11])). % 116.32/116.78 cnf(38,plain, % 116.32/116.78 (P5(x381)+~P9(a1,x381)), % 116.32/116.78 inference(scs_inference,[],[1,12,4])). % 116.32/116.78 cnf(39,plain, % 116.32/116.78 (P3(x391)+~P9(a1,x391)), % 116.32/116.78 inference(scs_inference,[],[38,5])). % 116.32/116.78 cnf(40,plain, % 116.32/116.78 (P3(x401)+~P7(a1,x401)), % 116.32/116.78 inference(scs_inference,[],[1,39,14])). % 116.32/116.78 cnf(41,plain, % 116.32/116.78 (P5(x411)+~P7(a1,x411)), % 116.32/116.78 inference(scs_inference,[],[40,4])). % 116.32/116.78 cnf(42,plain, % 116.32/116.78 (P5(f6(a1))), % 116.32/116.78 inference(scs_inference,[],[1,41,10])). % 116.32/116.78 cnf(43,plain, % 116.32/116.78 (P2(x431)+~P9(a1,x431)), % 116.32/116.78 inference(scs_inference,[],[1,13,11])). % 116.32/116.78 cnf(44,plain, % 116.32/116.78 (P4(x441)+~P9(a1,x441)), % 116.32/116.78 inference(scs_inference,[],[43,2])). % 116.32/116.78 cnf(53,plain, % 116.32/116.78 (P6(f6(a1),f5(f6(a1)))), % 116.32/116.78 inference(scs_inference,[],[33,2,9])). % 116.32/116.78 cnf(3342,plain, % 116.32/116.78 (P4(f6(a1))), % 116.32/116.78 inference(scs_inference,[],[33,2])). % 116.32/116.78 cnf(47952,plain, % 116.32/116.78 (~P9(a1,x479521)+~P8(f4(x479521),f5(x479521))), % 116.32/116.78 inference(scs_inference,[],[44,16])). % 116.32/116.78 cnf(47968,plain, % 116.32/116.78 (~P6(f6(a1),f5(x479681))+~P6(f6(a1),f4(x479681))+~P9(a1,x479681)), % 116.32/116.78 inference(scs_inference,[],[42,47952,18])). % 116.32/116.78 cnf(47984,plain, % 116.32/116.78 (~P6(f6(a1),f5(f6(a1)))+~P9(a1,f6(a1))), % 116.32/116.78 inference(scs_inference,[],[3342,47968,8])). % 116.32/116.78 cnf(48197,plain, % 116.32/116.78 (P9(a1,f6(a1))), % 116.32/116.78 inference(scs_inference,[],[1,10,14])). % 116.32/116.78 cnf(48199,plain, % 116.32/116.78 (~P6(f6(a1),f5(f6(a1)))), % 116.32/116.78 inference(scs_inference,[],[48197,47984])). % 116.32/116.78 cnf(90922,plain, % 116.32/116.78 ($false), % 116.32/116.78 inference(scs_inference,[],[53,48199]), % 116.32/116.78 ['proof']). % 116.45/116.87 % SZS output end Proof % 116.45/116.87 % Total time :115.600000s %------------------------------------------------------------------------------