%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS013-1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n011.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:14 EDT 2024 % Result : Unsatisfiable 116.12s 116.36s % Output : CNFRefutation 116.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : KRS013-1 : TPTP v8.2.0. Released v2.0.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 14:11:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.49/0.57 start to proof:theBenchmark % 116.12/116.34 %------------------------------------------- % 116.12/116.34 % File :CSE---1.7 % 116.12/116.34 % Problem :theBenchmark % 116.12/116.34 % Transform :cnf % 116.12/116.34 % Format :tptp:raw % 116.12/116.34 % Command :java -jar mcs_scs.jar %d %s % 116.12/116.34 % 116.12/116.34 % Result :Theorem 115.600000s % 116.12/116.34 % Output :CNFRefutation 115.600000s % 116.12/116.34 %------------------------------------------- % 116.12/116.36 %-------------------------------------------------------------------------- % 116.12/116.36 % File : KRS013-1 : TPTP v8.2.0. Released v2.0.0. % 116.12/116.36 % Domain : Knowledge Representation % 116.12/116.36 % Problem : Paramasivam problem T-Box 4b % 116.12/116.36 % Version : Especial. % 116.12/116.36 % English : f subsumes e. % 116.12/116.36 % 116.12/116.36 % Refs : [PP95] Paramasivam & Plaisted (1995), Automated Deduction Tec % 116.12/116.36 % Source : [PP95] % 116.12/116.36 % Names : Problem 4(b) [PP95] % 116.12/116.36 % 116.12/116.36 % Status : Unsatisfiable % 116.12/116.36 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v2.1.0 % 116.12/116.36 % Syntax : Number of clauses : 33 ( 2 unt; 12 nHn; 26 RR) % 116.12/116.36 % Number of literals : 82 ( 0 equ; 38 neg) % 116.12/116.36 % Maximal clause size : 4 ( 2 avg) % 116.12/116.36 % Maximal term depth : 2 ( 1 avg) % 116.12/116.36 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty) % 116.12/116.36 % Number of functors : 12 ( 12 usr; 1 con; 0-1 aty) % 116.12/116.36 % Number of variables : 42 ( 0 sgn) % 116.12/116.36 % SPC : CNF_UNS_RFO_NEQ_NHN % 116.12/116.36 % 116.12/116.36 % Comments : % 116.12/116.36 %-------------------------------------------------------------------------- % 116.12/116.36 cnf(clause_1,negated_conjecture, % 116.12/116.36 e(exist) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_2,negated_conjecture, % 116.12/116.36 ~ f(exist) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_3,axiom, % 116.12/116.36 ( t2least(X1) % 116.12/116.36 | ~ c(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_4,axiom, % 116.12/116.36 ( c(X1) % 116.12/116.36 | ~ t2least(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_5,axiom, % 116.12/116.36 ( ~ t2least(X1) % 116.12/116.36 | ~ equalish(u1r2(X1),u1r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_6,axiom, % 116.12/116.36 ( t(X1,u1r1(X1)) % 116.12/116.36 | ~ t2least(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_7,axiom, % 116.12/116.36 ( t(X1,u1r2(X1)) % 116.12/116.36 | ~ t2least(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_8,axiom, % 116.12/116.36 ( t2least(X1) % 116.12/116.36 | equalish(X3,X2) % 116.12/116.36 | ~ t(X1,X3) % 116.12/116.36 | ~ t(X1,X2) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_9,axiom, % 116.12/116.36 ( t1most(X1) % 116.12/116.36 | ~ d(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_10,axiom, % 116.12/116.36 ( d(X1) % 116.12/116.36 | ~ t1most(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_11,axiom, % 116.12/116.36 ( equalish(X3,X2) % 116.12/116.36 | ~ t1most(X1) % 116.12/116.36 | ~ t(X1,X3) % 116.12/116.36 | ~ t(X1,X2) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_12,axiom, % 116.12/116.36 ( t1most(X1) % 116.12/116.36 | ~ equalish(u3r2(X1),u3r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_13,axiom, % 116.12/116.36 ( t1most(X1) % 116.12/116.36 | t(X1,u3r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_14,axiom, % 116.12/116.36 ( t1most(X1) % 116.12/116.36 | t(X1,u3r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_15,axiom, % 116.12/116.36 ( d(X3) % 116.12/116.36 | ~ e(X1) % 116.12/116.36 | ~ r(X1,X3) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_16,axiom, % 116.12/116.36 ( c(X2) % 116.12/116.36 | ~ e(X1) % 116.12/116.36 | ~ r(X1,X2) % 116.12/116.36 | ~ s2least(X2) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_17,axiom, % 116.12/116.36 ( e(X1) % 116.12/116.36 | ~ c(u4r1(X1)) % 116.12/116.36 | ~ d(u4r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_18,axiom, % 116.12/116.36 ( e(X1) % 116.12/116.36 | r(X1,u4r2(X1)) % 116.12/116.36 | ~ c(u4r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_19,axiom, % 116.12/116.36 ( e(X1) % 116.12/116.36 | s2least(u4r1(X1)) % 116.12/116.36 | ~ d(u4r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_20,axiom, % 116.12/116.36 ( e(X1) % 116.12/116.36 | s2least(u4r1(X1)) % 116.12/116.36 | r(X1,u4r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_21,axiom, % 116.12/116.36 ( e(X1) % 116.12/116.36 | r(X1,u4r1(X1)) % 116.12/116.36 | ~ d(u4r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_22,axiom, % 116.12/116.36 ( e(X1) % 116.12/116.36 | r(X1,u4r1(X1)) % 116.12/116.36 | r(X1,u4r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_23,axiom, % 116.12/116.36 ( ~ s2least(X1) % 116.12/116.36 | ~ equalish(u5r2(X1),u5r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_24,axiom, % 116.12/116.36 ( s(X1,u5r1(X1)) % 116.12/116.36 | ~ s2least(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_25,axiom, % 116.12/116.36 ( s(X1,u5r2(X1)) % 116.12/116.36 | ~ s2least(X1) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_26,axiom, % 116.12/116.36 ( s2least(X1) % 116.12/116.36 | equalish(X3,X2) % 116.12/116.36 | ~ s(X1,X3) % 116.12/116.36 | ~ s(X1,X2) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_27,axiom, % 116.12/116.36 ( s1most(X2) % 116.12/116.36 | ~ f(X1) % 116.12/116.36 | ~ r(X1,X2) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_28,axiom, % 116.12/116.36 ( f(X1) % 116.12/116.36 | ~ s1most(u6r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_29,axiom, % 116.12/116.36 ( f(X1) % 116.12/116.36 | r(X1,u6r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_30,axiom, % 116.12/116.36 ( equalish(X3,X2) % 116.12/116.36 | ~ s1most(X1) % 116.12/116.36 | ~ s(X1,X3) % 116.12/116.36 | ~ s(X1,X2) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_31,axiom, % 116.12/116.36 ( s1most(X1) % 116.12/116.36 | ~ equalish(u7r2(X1),u7r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_32,axiom, % 116.12/116.36 ( s1most(X1) % 116.12/116.36 | s(X1,u7r1(X1)) ) ). % 116.12/116.36 % 116.12/116.36 cnf(clause_33,axiom, % 116.12/116.36 ( s1most(X1) % 116.12/116.36 | s(X1,u7r2(X1)) ) ). % 116.12/116.36 % 116.12/116.36 %-------------------------------------------------------------------------- % 116.12/116.36 %------------------------------------------- % 116.12/116.36 % Proof found % 116.12/116.36 % SZS status Theorem for theBenchmark % 116.12/116.36 % SZS output start Proof % 116.12/116.37 %ClaNum:33(EqnAxiom:0) % 116.12/116.37 %VarNum:113(SingletonVarNum:42) % 116.12/116.37 %MaxLitNum:4 % 116.12/116.37 %MaxfuncDepth:1 % 116.12/116.37 %SharedTerms:3 % 116.12/116.37 %goalClause: 1 2 % 116.12/116.37 %singleGoalClaCount:2 % 116.12/116.37 [1]P1(a1) % 116.12/116.37 [2]~P4(a1) % 116.12/116.37 [3]~P2(x31)+P6(x31) % 116.12/116.37 [4]~P6(x41)+P2(x41) % 116.12/116.37 [5]~P3(x51)+P7(x51) % 116.12/116.37 [6]~P7(x61)+P3(x61) % 116.12/116.37 [7]P4(x71)+~P8(f2(x71)) % 116.12/116.37 [8]P4(x81)+P9(x81,f2(x81)) % 116.12/116.37 [9]P7(x91)+P11(x91,f3(x91)) % 116.12/116.37 [10]P7(x101)+P11(x101,f4(x101)) % 116.12/116.37 [11]P8(x111)+P10(x111,f11(x111)) % 116.12/116.37 [12]P8(x121)+P10(x121,f12(x121)) % 116.12/116.37 [13]~P6(x131)+P11(x131,f5(x131)) % 116.12/116.37 [14]~P6(x141)+P11(x141,f6(x141)) % 116.12/116.37 [15]~P12(x151)+P10(x151,f7(x151)) % 116.12/116.37 [16]~P12(x161)+P10(x161,f8(x161)) % 116.12/116.37 [26]P7(x261)+~P5(f3(x261),f4(x261)) % 116.12/116.37 [27]P8(x271)+~P5(f11(x271),f12(x271)) % 116.12/116.37 [28]~P6(x281)+~P5(f5(x281),f6(x281)) % 116.12/116.37 [29]~P12(x291)+~P5(f7(x291),f8(x291)) % 116.12/116.37 [17]P1(x171)+P12(f9(x171))+~P3(f10(x171)) % 116.12/116.37 [20]P1(x201)+P9(x201,f10(x201))+P12(f9(x201)) % 116.12/116.37 [21]P1(x211)+~P2(f9(x211))+~P3(f10(x211)) % 116.12/116.37 [23]P1(x231)+P9(x231,f9(x231))+~P3(f10(x231)) % 116.12/116.37 [24]P1(x241)+P9(x241,f10(x241))+~P2(f9(x241)) % 116.12/116.37 [25]P1(x251)+P9(x251,f9(x251))+P9(x251,f10(x251)) % 116.12/116.37 [18]~P9(x182,x181)+P3(x181)+~P1(x182) % 116.12/116.37 [19]~P9(x192,x191)+P8(x191)+~P4(x192) % 116.12/116.37 [22]~P12(x221)+~P9(x222,x221)+P2(x221)+~P1(x222) % 116.12/116.37 [30]~P11(x301,x303)+~P11(x301,x302)+P6(x301)+P5(x302,x303) % 116.12/116.37 [31]~P10(x311,x313)+~P10(x311,x312)+P12(x311)+P5(x312,x313) % 116.12/116.37 [32]~P11(x323,x322)+~P11(x323,x321)+P5(x321,x322)+~P7(x323) % 116.12/116.37 [33]~P10(x333,x332)+~P10(x333,x331)+P5(x331,x332)+~P8(x333) % 116.12/116.37 %EqnAxiom % 116.12/116.37 % 116.12/116.37 %------------------------------------------- % 116.26/116.41 cnf(37,plain, % 116.26/116.41 (P8(x371)+~P9(x372,x371)+P9(x372,f2(x372))), % 116.26/116.41 inference(scs_inference,[],[8,19])). % 116.26/116.41 cnf(38,plain, % 116.26/116.41 (P3(x381)+P11(x381,f3(x381))), % 116.26/116.41 inference(scs_inference,[],[9,6])). % 116.26/116.41 cnf(39,plain, % 116.26/116.41 (P3(x391)+P11(x391,f4(x391))), % 116.26/116.41 inference(scs_inference,[],[10,6])). % 116.26/116.41 cnf(41,plain, % 116.26/116.41 (P10(f2(a1),f12(f2(a1)))), % 116.26/116.41 inference(scs_inference,[],[2,12,7])). % 116.26/116.41 cnf(42,plain, % 116.26/116.41 (~P2(x421)+P11(x421,f5(x421))), % 116.26/116.41 inference(scs_inference,[],[13,3])). % 116.26/116.41 cnf(43,plain, % 116.26/116.41 (~P2(x431)+P11(x431,f6(x431))), % 116.26/116.41 inference(scs_inference,[],[14,3])). % 116.26/116.41 cnf(48,plain, % 116.26/116.41 (P11(x481,f5(x481))+~P12(x481)+~P9(a1,x481)), % 116.26/116.41 inference(scs_inference,[],[1,42,22])). % 116.26/116.41 cnf(49,plain, % 116.26/116.41 (P11(x491,f6(x491))+~P12(x491)+~P9(a1,x491)), % 116.26/116.41 inference(scs_inference,[],[1,43,22])). % 116.26/116.41 cnf(51,plain, % 116.26/116.41 (~P5(f11(f2(a1)),f12(f2(a1)))), % 116.26/116.41 inference(scs_inference,[],[2,27,7])). % 116.26/116.41 cnf(52,plain, % 116.26/116.41 (~P2(x521)+~P5(f5(x521),f6(x521))), % 116.26/116.41 inference(scs_inference,[],[28,3])). % 116.26/116.41 cnf(55,plain, % 116.26/116.41 (~P5(f5(x551),f6(x551))+~P12(x551)+~P9(a1,x551)), % 116.26/116.41 inference(scs_inference,[],[1,52,22])). % 116.26/116.41 cnf(56,plain, % 116.26/116.41 (P7(x561)+~P9(a1,x561)), % 116.26/116.41 inference(scs_inference,[],[1,18,5])). % 116.26/116.41 cnf(60,plain, % 116.26/116.41 (P8(x601)+~P9(a1,x601)+P7(f2(a1))), % 116.26/116.41 inference(scs_inference,[],[37,56])). % 116.26/116.41 cnf(61,plain, % 116.26/116.41 (P8(f2(a1))+P7(f2(a1))), % 116.26/116.41 inference(scs_inference,[],[2,60,8])). % 116.26/116.41 cnf(62,plain, % 116.26/116.41 (P7(f2(a1))), % 116.26/116.41 inference(scs_inference,[],[2,61,7])). % 116.26/116.41 cnf(69,plain, % 116.26/116.41 (~P11(f2(a1),f4(x691))+P7(x691)+~P11(f2(a1),f3(x691))), % 116.26/116.41 inference(scs_inference,[],[62,32,26])). % 116.26/116.41 cnf(70,plain, % 116.26/116.41 (P3(x701)+~P11(f2(a1),f3(x701))+~P11(f2(a1),f4(x701))), % 116.26/116.41 inference(scs_inference,[],[69,6])). % 116.26/116.41 cnf(71,plain, % 116.26/116.41 (P3(f2(a1))+~P11(f2(a1),f4(f2(a1)))), % 116.26/116.41 inference(scs_inference,[],[70,38])). % 116.26/116.41 cnf(72,plain, % 116.26/116.41 (P3(f2(a1))), % 116.26/116.41 inference(scs_inference,[],[71,39])). % 116.26/116.41 cnf(81,plain, % 116.26/116.41 (P5(x811,x812)+~P11(f2(a1),x812)+~P11(f2(a1),x811)), % 116.26/116.41 inference(scs_inference,[],[72,5,32])). % 116.26/116.41 cnf(88,plain, % 116.26/116.41 (~P4(x881)+~P9(x881,f2(a1))), % 116.26/116.41 inference(scs_inference,[],[2,7,19])). % 116.26/116.41 cnf(90,plain, % 116.26/116.41 (~P9(x901,f2(a1))+~P8(f2(x901))), % 116.26/116.41 inference(scs_inference,[],[7,88])). % 116.26/116.41 cnf(96,plain, % 116.26/116.41 (~P8(f2(a1))), % 116.26/116.41 inference(scs_inference,[],[2,8,90])). % 116.26/116.41 cnf(69303,plain, % 116.26/116.41 (P9(a1,f2(a1))), % 116.26/116.41 inference(scs_inference,[],[2,8])). % 116.26/116.41 cnf(102496,plain, % 116.26/116.41 (P12(f2(a1))), % 116.26/116.41 inference(scs_inference,[],[96,51,41,11,31])). % 116.26/116.41 cnf(102507,plain, % 116.26/116.41 ($false), % 116.26/116.41 inference(scs_inference,[],[102496,69303,62,48,49,55,81,32]), % 116.26/116.41 ['proof']). % 116.33/116.47 % SZS output end Proof % 116.33/116.47 % Total time :115.600000s %------------------------------------------------------------------------------