%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS010-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 : n024.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 2.85s 2.93s % Output : CNFRefutation 2.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : KRS010-1 : TPTP v8.2.0. Released v2.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jun 19 12:31:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.22/0.57 start to proof:theBenchmark % 2.85/2.92 %------------------------------------------- % 2.85/2.92 % File :CSE---1.7 % 2.85/2.92 % Problem :theBenchmark % 2.85/2.92 % Transform :cnf % 2.85/2.92 % Format :tptp:raw % 2.85/2.92 % Command :java -jar mcs_scs.jar %d %s % 2.85/2.92 % 2.85/2.92 % Result :Theorem 2.290000s % 2.85/2.92 % Output :CNFRefutation 2.290000s % 2.85/2.92 %------------------------------------------- % 2.85/2.92 %-------------------------------------------------------------------------- % 2.85/2.92 % File : KRS010-1 : TPTP v8.2.0. Released v2.0.0. % 2.85/2.92 % Domain : Knowledge Representation % 2.85/2.92 % Problem : Paramasivam problem T-Box 3d % 2.85/2.92 % Version : Especial. % 2.85/2.92 % English : f subsumes e. % 2.85/2.92 % 2.85/2.92 % Refs : [PP95] Paramasivam & Plaisted (1995), Automated Deduction Tec % 2.85/2.92 % Source : [PP95] % 2.85/2.92 % Names : Problem 3(d) [PP95] % 2.85/2.92 % 2.85/2.92 % Status : Unsatisfiable % 2.85/2.92 % Rating : 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v2.5.0, 0.20 v2.4.0, 0.00 v2.1.0 % 2.85/2.92 % Syntax : Number of clauses : 31 ( 2 unt; 12 nHn; 31 RR) % 2.85/2.92 % Number of literals : 95 ( 0 equ; 51 neg) % 2.85/2.92 % Maximal clause size : 7 ( 3 avg) % 2.85/2.92 % Maximal term depth : 2 ( 1 avg) % 2.85/2.92 % Number of predicates : 8 ( 8 usr; 0 prp; 1-2 aty) % 2.85/2.92 % Number of functors : 9 ( 9 usr; 1 con; 0-1 aty) % 2.85/2.92 % Number of variables : 37 ( 0 sgn) % 2.85/2.92 % SPC : CNF_UNS_RFO_NEQ_NHN % 2.85/2.92 % 2.85/2.92 % Comments : % 2.85/2.92 %-------------------------------------------------------------------------- % 2.85/2.92 cnf(clause_1,negated_conjecture, % 2.85/2.92 e(exist) ). % 2.85/2.92 % 2.85/2.92 cnf(clause_2,negated_conjecture, % 2.85/2.92 ~ f(exist) ). % 2.85/2.92 % 2.85/2.92 cnf(clause_3,axiom, % 2.85/2.92 ( c(X1) % 2.85/2.92 | d(X1) % 2.85/2.92 | ~ a(X1) ) ). % 2.85/2.92 % 2.85/2.92 cnf(clause_4,axiom, % 2.85/2.92 ( a(X1) % 2.85/2.92 | ~ d(X1) ) ). % 2.85/2.92 % 2.85/2.92 cnf(clause_5,axiom, % 2.85/2.92 ( a(X1) % 2.85/2.92 | ~ c(X1) ) ). % 2.85/2.92 % 2.85/2.92 cnf(clause_6,axiom, % 2.85/2.92 ( equalish(X4,X3) % 2.85/2.92 | ~ e(X1) % 2.85/2.92 | ~ r(X1,X4) % 2.85/2.92 | ~ r(X1,X3) % 2.85/2.92 | ~ c(X4) % 2.85/2.92 | ~ c(X3) ) ). % 2.85/2.92 % 2.85/2.92 cnf(clause_7,axiom, % 2.85/2.93 ( r3least(X1) % 2.85/2.93 | ~ e(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_8,axiom, % 2.85/2.93 ( a(X2) % 2.85/2.93 | ~ e(X1) % 2.85/2.93 | ~ r(X1,X2) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_9,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | ~ a(u1r1(X1)) % 2.85/2.93 | ~ r3least(X1) % 2.85/2.93 | ~ equalish(u1r3(X1),u1r2(X1)) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_10,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | c(u1r2(X1)) % 2.85/2.93 | ~ a(u1r1(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_11,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | c(u1r3(X1)) % 2.85/2.93 | ~ a(u1r1(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_12,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r2(X1)) % 2.85/2.93 | ~ a(u1r1(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_13,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r3(X1)) % 2.85/2.93 | ~ a(u1r1(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_14,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r1(X1)) % 2.85/2.93 | ~ r3least(X1) % 2.85/2.93 | ~ equalish(u1r3(X1),u1r2(X1)) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_15,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r1(X1)) % 2.85/2.93 | c(u1r2(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_16,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r1(X1)) % 2.85/2.93 | c(u1r3(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_17,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r1(X1)) % 2.85/2.93 | r(X1,u1r2(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_18,axiom, % 2.85/2.93 ( e(X1) % 2.85/2.93 | r(X1,u1r1(X1)) % 2.85/2.93 | r(X1,u1r3(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_19,axiom, % 2.85/2.93 ( ~ r3least(X1) % 2.85/2.93 | ~ equalish(u2r2(X1),u2r1(X1)) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_20,axiom, % 2.85/2.93 ( ~ r3least(X1) % 2.85/2.93 | ~ equalish(u2r3(X1),u2r1(X1)) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_21,axiom, % 2.85/2.93 ( ~ r3least(X1) % 2.85/2.93 | ~ equalish(u2r3(X1),u2r2(X1)) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_22,axiom, % 2.85/2.93 ( r(X1,u2r1(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_23,axiom, % 2.85/2.93 ( r(X1,u2r2(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_24,axiom, % 2.85/2.93 ( r(X1,u2r3(X1)) % 2.85/2.93 | ~ r3least(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_25,axiom, % 2.85/2.93 ( r3least(X1) % 2.85/2.93 | equalish(X4,X3) % 2.85/2.93 | equalish(X4,X2) % 2.85/2.93 | equalish(X3,X2) % 2.85/2.93 | ~ r(X1,X4) % 2.85/2.93 | ~ r(X1,X3) % 2.85/2.93 | ~ r(X1,X2) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_26,axiom, % 2.85/2.93 ( d(u3r1(X1)) % 2.85/2.93 | ~ f(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_27,axiom, % 2.85/2.93 ( d(u3r2(X1)) % 2.85/2.93 | ~ f(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_28,axiom, % 2.85/2.93 ( ~ f(X1) % 2.85/2.93 | ~ equalish(u3r2(X1),u3r1(X1)) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_29,axiom, % 2.85/2.93 ( r(X1,u3r1(X1)) % 2.85/2.93 | ~ f(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_30,axiom, % 2.85/2.93 ( r(X1,u3r2(X1)) % 2.85/2.93 | ~ f(X1) ) ). % 2.85/2.93 % 2.85/2.93 cnf(clause_31,axiom, % 2.85/2.93 ( f(X1) % 2.85/2.93 | equalish(X3,X2) % 2.85/2.93 | ~ r(X1,X3) % 2.85/2.93 | ~ r(X1,X2) % 2.85/2.93 | ~ d(X3) % 2.85/2.93 | ~ d(X2) ) ). % 2.85/2.93 % 2.85/2.93 %-------------------------------------------------------------------------- % 2.85/2.93 %------------------------------------------- % 2.85/2.93 % Proof found % 2.85/2.93 % SZS status Theorem for theBenchmark % 2.85/2.93 % SZS output start Proof % 2.85/2.93 %ClaNum:31(EqnAxiom:0) % 2.85/2.93 %VarNum:126(SingletonVarNum:37) % 2.85/2.93 %MaxLitNum:7 % 2.85/2.93 %MaxfuncDepth:1 % 2.85/2.93 %SharedTerms:3 % 2.85/2.93 %goalClause: 1 2 % 2.85/2.93 %singleGoalClaCount:2 % 2.85/2.93 [1]P1(a1) % 2.85/2.93 [2]~P5(a1) % 2.85/2.93 [3]~P3(x31)+P2(x31) % 2.85/2.93 [4]~P4(x41)+P2(x41) % 2.85/2.93 [5]~P1(x51)+P7(x51) % 2.85/2.93 [7]~P5(x71)+P4(f2(x71)) % 2.85/2.93 [8]~P5(x81)+P4(f9(x81)) % 2.85/2.93 [9]~P7(x91)+P8(x91,f3(x91)) % 2.85/2.93 [10]~P7(x101)+P8(x101,f4(x101)) % 2.85/2.93 [11]~P7(x111)+P8(x111,f8(x111)) % 2.85/2.93 [12]~P5(x121)+P8(x121,f2(x121)) % 2.85/2.93 [13]~P5(x131)+P8(x131,f9(x131)) % 2.85/2.93 [21]~P5(x211)+~P6(f9(x211),f2(x211)) % 2.85/2.93 [22]~P7(x221)+~P6(f3(x221),f4(x221)) % 2.85/2.93 [23]~P7(x231)+~P6(f8(x231),f3(x231)) % 2.85/2.93 [24]~P7(x241)+~P6(f8(x241),f4(x241)) % 2.85/2.93 [6]P4(x61)+~P2(x61)+P3(x61) % 2.85/2.93 [14]~P8(x142,x141)+P2(x141)+~P1(x142) % 2.85/2.93 [15]~P7(x151)+P1(x151)+P3(f5(x151))+~P2(f6(x151)) % 2.85/2.93 [16]~P7(x161)+P1(x161)+P3(f7(x161))+~P2(f6(x161)) % 2.85/2.93 [17]~P7(x171)+P1(x171)+P8(x171,f6(x171))+P3(f5(x171)) % 2.85/2.93 [18]~P7(x181)+P1(x181)+P8(x181,f6(x181))+P3(f7(x181)) % 2.85/2.93 [19]~P7(x191)+P1(x191)+P8(x191,f5(x191))+~P2(f6(x191)) % 2.85/2.93 [20]~P7(x201)+P1(x201)+P8(x201,f7(x201))+~P2(f6(x201)) % 2.85/2.93 [25]~P7(x251)+P1(x251)+P8(x251,f6(x251))+P8(x251,f5(x251)) % 2.85/2.93 [26]~P7(x261)+P1(x261)+P8(x261,f6(x261))+P8(x261,f7(x261)) % 2.85/2.93 [27]~P7(x271)+P1(x271)+~P6(f5(x271),f7(x271))+~P2(f6(x271)) % 2.85/2.93 [28]~P7(x281)+P1(x281)+P8(x281,f6(x281))+~P6(f5(x281),f7(x281)) % 2.85/2.93 [29]~P4(x293)+~P4(x292)+~P8(x291,x293)+~P8(x291,x292)+P5(x291)+P6(x292,x293) % 2.85/2.93 [30]~P3(x302)+~P3(x301)+~P8(x303,x302)+~P8(x303,x301)+P6(x301,x302)+~P1(x303) % 2.85/2.93 [31]P6(x314,x312)+~P8(x311,x313)+~P8(x311,x312)+~P8(x311,x314)+P7(x311)+P6(x312,x313)+P6(x314,x313) % 2.85/2.93 %EqnAxiom % 2.85/2.93 % 2.85/2.93 %------------------------------------------- % 2.85/2.94 cnf(34,plain, % 2.85/2.94 (P8(a1,f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,5,9])). % 2.85/2.94 cnf(67,plain, % 2.85/2.94 (P8(a1,f4(a1))), % 2.85/2.94 inference(scs_inference,[],[1,10,5])). % 2.85/2.94 cnf(74,plain, % 2.85/2.94 (P8(a1,f8(a1))), % 2.85/2.94 inference(scs_inference,[],[1,11,5])). % 2.85/2.94 cnf(99,plain, % 2.85/2.94 (~P6(f3(a1),f4(a1))), % 2.85/2.94 inference(scs_inference,[],[1,22,5])). % 2.85/2.94 cnf(100,plain, % 2.85/2.94 (~P4(f4(a1))+~P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[2,99,67,34,29])). % 2.85/2.94 cnf(107,plain, % 2.85/2.94 (~P3(f4(a1))+~P3(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,99,67,34,30])). % 2.85/2.94 cnf(120,plain, % 2.85/2.94 (~P6(f8(a1),f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,23,5])). % 2.85/2.94 cnf(121,plain, % 2.85/2.94 (~P4(f3(a1))+~P4(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[2,34,120,74,29])). % 2.85/2.94 cnf(127,plain, % 2.85/2.94 (~P2(f3(a1))+P3(f3(a1))+~P4(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[121,6])). % 2.85/2.94 cnf(128,plain, % 2.85/2.94 (~P3(f3(a1))+~P3(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[1,34,120,74,30])). % 2.85/2.94 cnf(141,plain, % 2.85/2.94 (~P6(f8(a1),f4(a1))), % 2.85/2.94 inference(scs_inference,[],[1,24,5])). % 2.85/2.94 cnf(144,plain, % 2.85/2.94 (~P3(f4(a1))+~P3(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[2,1,74,141,67,29,30])). % 2.85/2.94 cnf(174,plain, % 2.85/2.94 (P3(f3(a1))+~P8(a1,f3(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,34,14,6])). % 2.85/2.94 cnf(175,plain, % 2.85/2.94 (P3(f3(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[34,174])). % 2.85/2.94 cnf(178,plain, % 2.85/2.94 (~P3(f8(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,34,99,67,174,30,128])). % 2.85/2.94 cnf(181,plain, % 2.85/2.94 (P2(f3(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[175,3])). % 2.85/2.94 cnf(351,plain, % 2.85/2.94 (~P2(f8(a1))+P4(f8(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[178,6])). % 2.85/2.94 cnf(442,plain, % 2.85/2.94 (P2(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[181,4])). % 2.85/2.94 cnf(443,plain, % 2.85/2.94 (P3(f3(a1))+~P4(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[442,127])). % 2.85/2.94 cnf(523,plain, % 2.85/2.94 (~P4(f8(a1))+~P3(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[443,107])). % 2.85/2.94 cnf(705,plain, % 2.85/2.94 (~P2(f8(a1))+P3(f8(a1))+~P3(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[523,6])). % 2.85/2.94 cnf(1158,plain, % 2.85/2.94 (P4(f8(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,74,351,14])). % 2.85/2.94 cnf(1249,plain, % 2.85/2.94 (P4(f8(a1))+~P4(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[1158,100])). % 2.85/2.94 cnf(1340,plain, % 2.85/2.94 (~P2(f4(a1))+P3(f4(a1))+P4(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[1249,6])). % 2.85/2.94 cnf(1612,plain, % 2.85/2.94 (P3(f8(a1))+~P3(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[1,74,705,14])). % 2.85/2.94 cnf(1703,plain, % 2.85/2.94 (P2(f8(a1))+~P3(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[1612,3])). % 2.85/2.94 cnf(1794,plain, % 2.85/2.94 (~P2(f4(a1))+P4(f4(a1))+P2(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[1703,6])). % 2.85/2.94 cnf(1885,plain, % 2.85/2.94 (P3(f4(a1))+P4(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[1,67,1340,14])). % 2.85/2.94 cnf(1976,plain, % 2.85/2.94 (P4(f8(a1))+~P3(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1885,107])). % 2.85/2.94 cnf(2067,plain, % 2.85/2.94 (P2(f8(a1))+~P3(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1976,4])). % 2.85/2.94 cnf(2158,plain, % 2.85/2.94 (P2(f8(a1))+P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[2067,175])). % 2.85/2.94 cnf(2249,plain, % 2.85/2.94 (P2(f8(a1))+~P4(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[2158,100])). % 2.85/2.94 cnf(2340,plain, % 2.85/2.94 (~P2(f4(a1))+P2(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[2249,1794])). % 2.85/2.94 cnf(2431,plain, % 2.85/2.94 (P2(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[1,67,2340,14])). % 2.85/2.94 cnf(2434,plain, % 2.85/2.94 (P3(f8(a1))+~P4(f4(a1))), % 2.85/2.94 inference(scs_inference,[],[74,2,2431,141,67,6,29])). % 2.85/2.94 cnf(2612,plain, % 2.85/2.94 (~P4(f4(a1))+~P3(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[2434,128])). % 2.85/2.94 cnf(2794,plain, % 2.85/2.94 (~P2(f4(a1))+P3(f4(a1))+~P3(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[2612,6])). % 2.85/2.94 cnf(3340,plain, % 2.85/2.94 (P3(f4(a1))+~P3(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[1,67,2794,14])). % 2.85/2.94 cnf(4603,plain, % 2.85/2.94 (P2(f4(a1))+P4(f8(a1))), % 2.85/2.94 inference(scs_inference,[],[3,1885])). % 2.85/2.94 cnf(4694,plain, % 2.85/2.94 (P2(f4(a1))+~P4(f3(a1))), % 2.85/2.94 inference(scs_inference,[],[4603,121])). % 2.85/2.94 cnf(4785,plain, % 2.85/2.94 (P3(f4(a1))+P4(f4(a1))+~P4(f3(a1))), % 2.85/2.95 inference(scs_inference,[],[4694,6])). % 2.85/2.95 cnf(4876,plain, % 2.85/2.95 (P4(f4(a1))+~P4(f3(a1))+~P3(f8(a1))), % 2.85/2.95 inference(scs_inference,[],[4785,144])). % 2.85/2.95 cnf(4967,plain, % 2.85/2.95 (~P3(f8(a1))+~P4(f3(a1))), % 2.85/2.95 inference(scs_inference,[],[4876,100])). % 2.85/2.95 cnf(5058,plain, % 2.85/2.95 (~P3(f8(a1))+P3(f3(a1))), % 2.85/2.95 inference(scs_inference,[],[4967,175])). % 2.85/2.95 cnf(5149,plain, % 2.85/2.95 (P3(f3(a1))+~P3(f4(a1))), % 2.85/2.95 inference(scs_inference,[],[5058,1612])). % 2.85/2.95 cnf(5240,plain, % 2.85/2.95 (~P3(f4(a1))), % 2.85/2.95 inference(scs_inference,[],[5149,107])). % 2.85/2.95 cnf(5243,plain, % 2.85/2.95 (P4(f8(a1))), % 2.85/2.95 inference(scs_inference,[],[5240,1885])). % 2.85/2.95 cnf(5244,plain, % 2.85/2.95 (~P3(f3(a1))), % 2.85/2.95 inference(scs_inference,[],[5240,3340])). % 2.85/2.95 cnf(5258,plain, % 2.85/2.95 ($false), % 2.85/2.95 inference(scs_inference,[],[5244,5243,443]), % 2.85/2.95 ['proof']). % 2.85/2.95 % SZS output end Proof % 2.85/2.95 % Total time :2.290000s %------------------------------------------------------------------------------