%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS002-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 : n022.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:12 EDT 2024 % Result : Unsatisfiable 0.53s 0.69s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : KRS002-1 : TPTP v8.2.0. Released v2.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n022.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 12:23:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 0.53/0.68 %------------------------------------------- % 0.53/0.68 % File :CSE---1.7 % 0.53/0.68 % Problem :theBenchmark % 0.53/0.68 % Transform :cnf % 0.53/0.68 % Format :tptp:raw % 0.53/0.68 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.68 % 0.53/0.68 % Result :Theorem 0.070000s % 0.53/0.68 % Output :CNFRefutation 0.070000s % 0.53/0.68 %------------------------------------------- % 0.53/0.69 %-------------------------------------------------------------------------- % 0.53/0.69 % File : KRS002-1 : TPTP v8.2.0. Released v2.0.0. % 0.53/0.69 % Domain : Knowledge Representation % 0.53/0.69 % Problem : Paramasivam problem T-Box 1b % 0.53/0.69 % Version : Especial. % 0.53/0.69 % English : e exists. % 0.53/0.69 % 0.53/0.69 % Refs : [PP95] Paramasivam & Plaisted (1995), Automated Deduction Tec % 0.53/0.69 % Source : [PP95] % 0.53/0.69 % Names : Problem 1(b) [PP95] % 0.53/0.69 % 0.53/0.69 % Status : Unsatisfiable % 0.53/0.69 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v2.1.0 % 0.53/0.69 % Syntax : Number of clauses : 18 ( 1 unt; 4 nHn; 16 RR) % 0.53/0.69 % Number of literals : 44 ( 0 equ; 23 neg) % 0.53/0.69 % Maximal clause size : 4 ( 2 avg) % 0.53/0.69 % Maximal term depth : 2 ( 1 avg) % 0.53/0.69 % Number of predicates : 8 ( 8 usr; 0 prp; 1-2 aty) % 0.53/0.69 % Number of functors : 7 ( 7 usr; 1 con; 0-1 aty) % 0.53/0.69 % Number of variables : 25 ( 2 sgn) % 0.53/0.69 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.53/0.69 % 0.53/0.69 % Comments : % 0.53/0.69 %-------------------------------------------------------------------------- % 0.53/0.69 cnf(clause_1,negated_conjecture, % 0.53/0.69 e(exist) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_2,axiom, % 0.53/0.69 ( s2least(X1) % 0.53/0.69 | ~ c(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_3,axiom, % 0.53/0.69 ( c(X1) % 0.53/0.69 | ~ s2least(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_4,axiom, % 0.53/0.69 ( ~ s2least(X1) % 0.53/0.69 | ~ equalish(u1r2(X1),u1r1(X1)) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_5,axiom, % 0.53/0.69 ( s(X1,u1r1(X1)) % 0.53/0.69 | ~ s2least(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_6,axiom, % 0.53/0.69 ( s(X1,u1r2(X1)) % 0.53/0.69 | ~ s2least(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_7,axiom, % 0.53/0.69 ( s2least(X1) % 0.53/0.69 | equalish(X3,X2) % 0.53/0.69 | ~ s(X1,X3) % 0.53/0.69 | ~ s(X1,X2) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_8,axiom, % 0.53/0.69 ( s1most(X1) % 0.53/0.69 | ~ d(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_9,axiom, % 0.53/0.69 ( d(X1) % 0.53/0.69 | ~ s1most(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_10,axiom, % 0.53/0.69 ( equalish(X3,X2) % 0.53/0.69 | ~ s1most(X1) % 0.53/0.69 | ~ s(X1,X3) % 0.53/0.69 | ~ s(X1,X2) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_11,axiom, % 0.53/0.69 ( s1most(X1) % 0.53/0.69 | ~ equalish(u3r2(X1),u3r1(X1)) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_12,axiom, % 0.53/0.69 ( s1most(X1) % 0.53/0.69 | s(X1,u3r1(X1)) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_13,axiom, % 0.53/0.69 ( s1most(X1) % 0.53/0.69 | s(X1,u3r2(X1)) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_14,axiom, % 0.53/0.69 ( r(X1,u4r2(X1)) % 0.53/0.69 | ~ e(X1) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_15,axiom, % 0.53/0.69 ( d(X2) % 0.53/0.69 | ~ e(X1) % 0.53/0.69 | ~ r(X1,X2) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_16,axiom, % 0.53/0.69 ( c(X2) % 0.53/0.69 | ~ e(X1) % 0.53/0.69 | ~ r(X1,X2) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_17,axiom, % 0.53/0.69 ( e(X1) % 0.53/0.69 | ~ c(u4r1(X1)) % 0.53/0.69 | ~ d(u4r1(X1)) % 0.53/0.69 | ~ r(X1,X3) ) ). % 0.53/0.69 % 0.53/0.69 cnf(clause_18,axiom, % 0.53/0.69 ( e(X1) % 0.53/0.69 | r(X1,u4r1(X1)) % 0.53/0.69 | ~ r(X1,X3) ) ). % 0.53/0.69 % 0.53/0.69 %-------------------------------------------------------------------------- % 0.53/0.69 %------------------------------------------- % 0.53/0.69 % Proof found % 0.53/0.69 % SZS status Theorem for theBenchmark % 0.53/0.69 % SZS output start Proof % 0.53/0.69 %ClaNum:18(EqnAxiom:0) % 0.53/0.69 %VarNum:61(SingletonVarNum:25) % 0.53/0.69 %MaxLitNum:4 % 0.53/0.70 %MaxfuncDepth:1 % 0.53/0.70 %SharedTerms:2 % 0.53/0.70 %goalClause: 1 % 0.53/0.70 %singleGoalClaCount:1 % 0.53/0.70 [1]P1(a1) % 0.53/0.70 [2]~P2(x21)+P4(x21) % 0.53/0.70 [3]~P4(x31)+P2(x31) % 0.53/0.70 [4]~P3(x41)+P5(x41) % 0.53/0.70 [5]~P5(x51)+P3(x51) % 0.53/0.70 [6]P5(x61)+P6(x61,f2(x61)) % 0.53/0.70 [7]P5(x71)+P6(x71,f3(x71)) % 0.53/0.70 [8]~P4(x81)+P6(x81,f4(x81)) % 0.53/0.70 [9]~P4(x91)+P6(x91,f5(x91)) % 0.53/0.70 [10]~P1(x101)+P7(x101,f6(x101)) % 0.53/0.70 [13]P5(x131)+~P8(f2(x131),f3(x131)) % 0.53/0.70 [15]~P4(x151)+~P8(f4(x151),f5(x151)) % 0.53/0.70 [11]~P7(x112,x111)+P2(x111)+~P1(x112) % 0.53/0.70 [12]~P7(x122,x121)+P3(x121)+~P1(x122) % 0.53/0.70 [14]P1(x141)+~P7(x141,x142)+P7(x141,f7(x141)) % 0.53/0.70 [16]P1(x161)+~P7(x161,x162)+~P2(f7(x161))+~P3(f7(x161)) % 0.53/0.70 [17]~P6(x171,x173)+~P6(x171,x172)+P4(x171)+P8(x172,x173) % 0.53/0.70 [18]~P6(x183,x182)+~P6(x183,x181)+P8(x181,x182)+~P5(x183) % 0.53/0.70 %EqnAxiom % 0.53/0.70 % 0.53/0.70 %------------------------------------------- % 0.53/0.70 cnf(23,plain, % 0.53/0.70 (~P2(x231)+P6(x231,f4(x231))), % 0.53/0.70 inference(scs_inference,[],[8,2])). % 0.53/0.70 cnf(24,plain, % 0.53/0.70 (~P2(x241)+P6(x241,f5(x241))), % 0.53/0.70 inference(scs_inference,[],[9,2])). % 0.53/0.70 cnf(26,plain, % 0.53/0.70 (P6(x261,f4(x261))+~P7(a1,x261)), % 0.53/0.70 inference(scs_inference,[],[1,23,11])). % 0.53/0.70 cnf(27,plain, % 0.53/0.70 (P6(x271,f5(x271))+~P7(a1,x271)), % 0.53/0.70 inference(scs_inference,[],[1,24,11])). % 0.53/0.70 cnf(29,plain, % 0.53/0.70 (~P2(x291)+~P8(f4(x291),f5(x291))), % 0.53/0.70 inference(scs_inference,[],[15,2])). % 0.53/0.70 cnf(30,plain, % 0.53/0.70 (P6(f6(a1),f4(f6(a1)))), % 0.53/0.70 inference(scs_inference,[],[1,26,10])). % 0.53/0.70 cnf(33,plain, % 0.53/0.70 (P5(x331)+~P7(a1,x331)), % 0.53/0.70 inference(scs_inference,[],[1,12,4])). % 0.53/0.70 cnf(34,plain, % 0.53/0.70 (P3(x341)+~P7(a1,x341)), % 0.53/0.70 inference(scs_inference,[],[33,5])). % 0.53/0.70 cnf(35,plain, % 0.53/0.70 (P3(f6(a1))), % 0.53/0.70 inference(scs_inference,[],[1,34,10])). % 0.53/0.70 cnf(45,plain, % 0.53/0.70 (P4(x451)+~P7(a1,x451)), % 0.53/0.70 inference(scs_inference,[],[1,2,11])). % 0.53/0.70 cnf(46,plain, % 0.53/0.70 (P2(x461)+~P7(a1,x461)), % 0.53/0.70 inference(scs_inference,[],[45,3])). % 0.53/0.70 cnf(47,plain, % 0.53/0.70 (~P8(f4(x471),f5(x471))+~P7(a1,x471)), % 0.53/0.70 inference(scs_inference,[],[46,29])). % 0.53/0.70 cnf(48,plain, % 0.53/0.70 (~P5(f6(a1))+~P6(f6(a1),f5(f6(a1)))+~P7(a1,f6(a1))), % 0.53/0.70 inference(scs_inference,[],[30,47,18])). % 0.53/0.70 cnf(49,plain, % 0.53/0.70 (~P5(f6(a1))+~P7(a1,f6(a1))), % 0.53/0.70 inference(scs_inference,[],[48,27])). % 0.53/0.70 cnf(50,plain, % 0.53/0.70 (~P5(f6(a1))), % 0.53/0.70 inference(scs_inference,[],[1,49,10])). % 0.53/0.70 cnf(51,plain, % 0.53/0.70 ($false), % 0.53/0.70 inference(scs_inference,[],[35,50,4]), % 0.53/0.70 ['proof']). % 0.53/0.70 % SZS output end Proof % 0.53/0.70 % Total time :0.070000s %------------------------------------------------------------------------------