%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT005-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:04:14 AM UTC 2026 % Result : Unsatisfiable 70.74s 70.94s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT005-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.34 % Computer : n004.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Mon Sep 7 11:38:15 UTC 2026 % 0.08/0.34 % CPUTime : % 0.24/0.50 start to proof:theBenchmark % 70.74/70.92 %------------------------------------------- % 70.74/70.92 % File :CSE---1.7 % 70.74/70.92 % Problem :theBenchmark % 70.74/70.92 % Transform :cnf % 70.74/70.92 % Format :tptp:raw % 70.74/70.92 % Command :java -jar mcs_scs.jar %d %s % 70.74/70.92 % 70.74/70.92 % Result :Theorem 70.360875s % 70.74/70.92 % Output :CNFRefutation 70.360875s % 70.74/70.92 %------------------------------------------- % 70.74/70.92 %-------------------------------------------------------------------------- % 70.74/70.92 % File : MGT005-1 : TPTP v9.3.0. Released v2.4.0. % 70.74/70.92 % Domain : Management (Organisation Theory) % 70.74/70.92 % Problem : Complexity increases the risk of death due to reorganization. % 70.74/70.92 % Version : [PB+94] axioms. % 70.74/70.92 % English : % 70.74/70.92 % 70.74/70.92 % Refs : [PB+92] Peli et al. (1992), A Logical Approach to Formalizing % 70.74/70.92 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 70.74/70.92 % : [Kam94] Kamps (1994), Email to G. Sutcliffe % 70.74/70.92 % Source : [TPTP] % 70.74/70.92 % Names : % 70.74/70.92 % 70.74/70.92 % Status : Unsatisfiable % 70.74/70.93 % Rating : 0.17 v9.3.0, 0.14 v9.1.0, 0.10 v9.0.0, 0.15 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.11 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.29 v6.0.0, 0.30 v5.3.0, 0.28 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.08 v4.0.1, 0.09 v4.0.0, 0.18 v3.7.0, 0.20 v3.5.0, 0.18 v3.4.0, 0.08 v3.3.0, 0.07 v3.2.0, 0.15 v3.1.0, 0.18 v2.7.0, 0.25 v2.6.0, 0.22 v2.5.0, 0.56 v2.4.0 % 70.74/70.93 % Syntax : Number of clauses : 29 ( 19 unt; 2 nHn; 29 RR) % 70.74/70.93 % Number of literals : 83 ( 2 equ; 54 neg) % 70.74/70.93 % Maximal clause size : 19 ( 2 avg) % 70.74/70.93 % Maximal term depth : 2 ( 1 avg) % 70.74/70.93 % Number of predicates : 9 ( 8 usr; 0 prp; 2-3 aty) % 70.74/70.93 % Number of functors : 13 ( 13 usr; 12 con; 0-2 aty) % 70.74/70.93 % Number of variables : 49 ( 2 sgn) % 70.74/70.93 % SPC : CNF_UNS_RFO_SEQ_NHN % 70.74/70.93 % 70.74/70.93 % Comments : mp11, mp12 and mp13 corrospond to mp10, mp11 and mp12 % 70.74/70.93 % respectively from [PB+92] % 70.74/70.93 % : Created with tptp2X -f tptp -t clausify:otter MGT005+1.p % 70.74/70.93 %-------------------------------------------------------------------------- % 70.74/70.93 cnf(mp6_1_26,axiom, % 70.74/70.93 ( ~ greater(A,B) % 70.74/70.93 | A != B ) ). % 70.74/70.93 % 70.74/70.93 cnf(mp6_2_27,axiom, % 70.74/70.93 ( ~ greater(A,B) % 70.74/70.93 | ~ greater(B,A) ) ). % 70.74/70.93 % 70.74/70.93 cnf(mp11_28,axiom, % 70.74/70.93 ( ~ greater(A,B) % 70.74/70.93 | ~ greater(B,C) % 70.74/70.93 | greater(A,C) ) ). % 70.74/70.93 % 70.74/70.93 cnf(mp12_29,axiom, % 70.74/70.93 ( ~ organization(A,B) % 70.74/70.93 | survival_chance(A,sk1(B,A),B) ) ). % 70.74/70.93 % 70.74/70.93 cnf(mp13_30,axiom, % 70.74/70.93 ( ~ organization(A,B) % 70.74/70.93 | ~ organization(A,C) % 70.74/70.93 | ~ greater(D,B) % 70.74/70.93 | ~ greater(C,D) % 70.74/70.93 | organization(A,D) ) ). % 70.74/70.93 % 70.74/70.93 cnf(mp7_31,axiom, % 70.74/70.93 ( ~ reorganization(A,B,C) % 70.74/70.93 | greater(C,B) ) ). % 70.74/70.93 % 70.74/70.93 cnf(t3_FOL_32,hypothesis, % 70.74/70.93 ( ~ organization(A,B) % 70.74/70.93 | ~ organization(A,C) % 70.74/70.93 | ~ reorganization_free(A,B,C) % 70.74/70.93 | ~ survival_chance(A,D,B) % 70.74/70.93 | ~ survival_chance(A,E,C) % 70.74/70.93 | ~ greater(C,B) % 70.74/70.93 | greater(E,D) ) ). % 70.74/70.93 % 70.74/70.93 cnf(t4_FOL_33,hypothesis, % 70.74/70.93 ( ~ organization(A,B) % 70.74/70.93 | ~ organization(A,C) % 70.74/70.93 | ~ reorganization(A,D,E) % 70.74/70.93 | ~ survival_chance(A,F,B) % 70.74/70.93 | ~ survival_chance(A,G,C) % 70.74/70.93 | greater(D,B) % 70.74/70.93 | ~ greater(C,B) % 70.74/70.93 | greater(C,E) % 70.74/70.93 | greater(F,G) ) ). % 70.74/70.93 % 70.74/70.93 cnf(a10_FOL_34,hypothesis, % 70.74/70.93 ( ~ organization(A,B) % 70.74/70.93 | ~ organization(C,B) % 70.74/70.93 | ~ organization(C,D) % 70.74/70.93 | ~ class(A,E,B) % 70.74/70.93 | ~ class(C,E,B) % 70.74/70.93 | ~ reorganization(A,B,F) % 70.74/70.93 | ~ reorganization(C,B,D) % 70.74/70.93 | ~ reorganization_type(A,G,B) % 70.74/70.93 | ~ reorganization_type(C,G,B) % 70.74/70.93 | ~ complexity(A,H,B) % 70.74/70.93 | ~ complexity(C,I,B) % 70.74/70.93 | ~ greater(I,H) % 70.74/70.93 | greater(D,F) ) ). % 70.74/70.93 % 70.74/70.93 cnf(a11_FOL_35,hypothesis, % 70.74/70.93 ( ~ organization(A,B) % 70.74/70.93 | ~ organization(C,B) % 70.74/70.93 | ~ organization(A,D) % 70.74/70.93 | ~ organization(C,D) % 70.74/70.93 | ~ class(A,E,B) % 70.74/70.93 | ~ class(C,E,B) % 70.74/70.93 | ~ survival_chance(A,F,B) % 70.74/70.93 | ~ survival_chance(C,F,B) % 70.74/70.93 | ~ reorganization(A,B,D) % 70.74/70.93 | ~ reorganization(C,B,G) % 70.74/70.93 | ~ reorganization_type(A,H,B) % 70.74/70.93 | ~ reorganization_type(C,H,B) % 70.74/70.93 | ~ survival_chance(A,I,D) % 70.74/70.93 | ~ survival_chance(C,J,D) % 70.74/70.93 | ~ complexity(A,K,B) % 70.74/70.93 | ~ complexity(C,L,B) % 70.74/70.93 | ~ greater(L,K) % 70.74/70.93 | greater(I,J) % 70.74/70.93 | I = J ) ). % 70.74/70.93 % 70.74/70.93 cnf(t5_FOL_36,negated_conjecture, % 70.74/70.93 organization(sk2,sk11) ). % 70.74/70.93 % 70.74/70.93 cnf(t5_FOL_37,negated_conjecture, % 70.74/70.93 organization(sk3,sk11) ). % 70.74/70.93 % 70.74/70.93 cnf(t5_FOL_38,negated_conjecture, % 70.74/70.93 organization(sk2,sk13) ). % 70.74/70.93 % 70.74/70.93 cnf(t5_FOL_39,negated_conjecture, % 70.74/70.93 organization(sk3,sk13) ). % 70.74/70.93 % 70.74/70.93 cnf(t5_FOL_40,negated_conjecture, % 70.74/70.93 class(sk2,sk5,sk11) ). % 70.74/70.93 % 70.74/70.94 cnf(t5_FOL_41,negated_conjecture, % 70.74/70.94 class(sk3,sk5,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_42,negated_conjecture, % 70.74/70.94 survival_chance(sk2,sk6,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_43,negated_conjecture, % 70.74/70.94 survival_chance(sk3,sk6,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_44,negated_conjecture, % 70.74/70.94 reorganization(sk2,sk11,sk12) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_45,negated_conjecture, % 70.74/70.94 reorganization(sk3,sk11,sk13) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_46,negated_conjecture, % 70.74/70.94 reorganization_type(sk2,sk4,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_47,negated_conjecture, % 70.74/70.94 reorganization_type(sk3,sk4,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_48,negated_conjecture, % 70.74/70.94 reorganization_free(sk2,sk12,sk13) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_49,negated_conjecture, % 70.74/70.94 survival_chance(sk2,sk7,sk13) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_50,negated_conjecture, % 70.74/70.94 survival_chance(sk3,sk8,sk13) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_51,negated_conjecture, % 70.74/70.94 complexity(sk2,sk9,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_52,negated_conjecture, % 70.74/70.94 complexity(sk3,sk10,sk11) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_53,negated_conjecture, % 70.74/70.94 greater(sk10,sk9) ). % 70.74/70.94 % 70.74/70.94 cnf(t5_FOL_54,negated_conjecture, % 70.74/70.94 ~ greater(sk7,sk8) ). % 70.74/70.94 % 70.74/70.94 %-------------------------------------------------------------------------- % 70.74/70.94 %------------------------------------------- % 70.74/70.94 % Proof found % 70.74/70.94 % SZS status Theorem for theBenchmark % 70.74/70.94 % SZS output start Proof % 70.74/70.94 %ClaNum:56(EqnAxiom:27) % 70.74/70.94 %VarNum:157(SingletonVarNum:49) % 70.74/70.94 %MaxLitNum:19 % 70.74/70.94 %MaxfuncDepth:1 % 70.74/70.94 %SharedTerms:31 % 70.74/70.94 %goalClause: 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 % 70.74/70.94 %singleGoalClaCount:19 % 70.74/70.94 [28]P1(a1,a3) % 70.74/70.94 [29]P4(a4,a5) % 70.74/70.94 [30]P4(a4,a6) % 70.74/70.94 [31]P4(a8,a5) % 70.74/70.94 [32]P4(a8,a6) % 70.74/70.94 [33]P5(a4,a9,a5) % 70.74/70.94 [34]P5(a4,a12,a6) % 70.74/70.94 [35]P5(a8,a9,a5) % 70.74/70.94 [36]P5(a8,a13,a6) % 70.74/70.94 [37]P6(a4,a5,a7) % 70.74/70.94 [38]P6(a8,a5,a6) % 70.74/70.94 [39]P7(a4,a7,a6) % 70.74/70.94 [40]P2(a4,a10,a5) % 70.74/70.94 [41]P2(a8,a10,a5) % 70.74/70.94 [42]P8(a4,a11,a5) % 70.74/70.94 [43]P8(a8,a11,a5) % 70.74/70.94 [44]P3(a4,a3,a5) % 70.74/70.94 [45]P3(a8,a1,a5) % 70.74/70.94 [46]~P1(a12,a13) % 70.74/70.94 [47]~P1(x471,x472)+~E(x471,x472) % 70.74/70.94 [48]~P1(x482,x481)+~P1(x481,x482) % 70.74/70.94 [51]~P4(x511,x512)+P5(x511,f2(x512,x511),x512) % 70.74/70.94 [50]P1(x501,x502)+~P6(x503,x502,x501) % 70.74/70.94 [49]~P1(x491,x493)+P1(x491,x492)+~P1(x493,x492) % 70.74/70.94 [52]~P4(x521,x524)+~P4(x521,x523)+P4(x521,x522)+~P1(x522,x523)+~P1(x524,x522) % 70.74/70.94 [53]~P4(x535,x534)+~P5(x535,x531,x533)+~P5(x535,x532,x534)+~P7(x535,x534,x533)+P1(x531,x532)+~P1(x533,x534)+~P4(x535,x533) % 70.74/70.94 [54]~P1(x545,x544)+~P4(x547,x544)+~P5(x547,x542,x545)+~P5(x547,x541,x544)+~P6(x547,x543,x546)+P1(x541,x542)+P1(x543,x544)+P1(x545,x546)+~P4(x547,x545) % 70.74/70.94 [55]~P6(x555,x556,x551)+~P6(x557,x556,x552)+~P2(x557,x558,x556)+~P8(x557,x559,x556)+~P3(x555,x553,x556)+~P3(x557,x554,x556)+P1(x551,x552)+~P1(x553,x554)+~P4(x555,x551)+~P2(x555,x558,x556)+~P8(x555,x559,x556)+~P4(x555,x556)+~P4(x557,x556) % 70.74/70.94 [56]~P5(x568,x561,x566)+~P3(x568,x564,x567)+~P3(x565,x563,x567)+~P8(x568,x5612,x567)+~P2(x568,x5611,x567)+~P6(x568,x567,x566)+~P5(x568,x569,x567)+~P5(x565,x562,x566)+~P4(x568,x567)+P1(x561,x562)+E(x561,x562)+~P1(x563,x564)+~P5(x565,x569,x567)+~P4(x565,x566)+~P6(x565,x567,x5610)+~P4(x565,x567)+~P2(x565,x5611,x567)+~P4(x568,x566)+~P8(x565,x5612,x567) % 70.74/70.94 %EqnAxiom % 70.74/70.94 [1]E(x11,x11) % 70.74/70.94 [2]E(x22,x21)+~E(x21,x22) % 70.74/70.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 70.74/70.94 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 70.74/70.94 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 70.74/70.94 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63) % 70.74/70.94 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71) % 70.74/70.94 [8]P4(x82,x83)+~E(x81,x82)+~P4(x81,x83) % 70.74/70.94 [9]P4(x93,x92)+~E(x91,x92)+~P4(x93,x91) % 70.74/70.94 [10]P8(x102,x103,x104)+~E(x101,x102)+~P8(x101,x103,x104) % 70.74/70.94 [11]P8(x113,x112,x114)+~E(x111,x112)+~P8(x113,x111,x114) % 70.74/70.94 [12]P8(x123,x124,x122)+~E(x121,x122)+~P8(x123,x124,x121) % 70.74/70.94 [13]P5(x132,x133,x134)+~E(x131,x132)+~P5(x131,x133,x134) % 70.74/70.94 [14]P5(x143,x142,x144)+~E(x141,x142)+~P5(x143,x141,x144) % 70.74/70.94 [15]P5(x153,x154,x152)+~E(x151,x152)+~P5(x153,x154,x151) % 70.74/70.94 [16]P2(x162,x163,x164)+~E(x161,x162)+~P2(x161,x163,x164) % 70.74/70.94 [17]P2(x173,x172,x174)+~E(x171,x172)+~P2(x173,x171,x174) % 70.74/70.94 [18]P2(x183,x184,x182)+~E(x181,x182)+~P2(x183,x184,x181) % 70.74/70.94 [19]P6(x192,x193,x194)+~E(x191,x192)+~P6(x191,x193,x194) % 70.74/70.94 [20]P6(x203,x202,x204)+~E(x201,x202)+~P6(x203,x201,x204) % 70.74/70.94 [21]P6(x213,x214,x212)+~E(x211,x212)+~P6(x213,x214,x211) % 70.74/70.94 [22]P3(x222,x223,x224)+~E(x221,x222)+~P3(x221,x223,x224) % 70.74/70.94 [23]P3(x233,x232,x234)+~E(x231,x232)+~P3(x233,x231,x234) % 70.74/70.94 [24]P3(x243,x244,x242)+~E(x241,x242)+~P3(x243,x244,x241) % 70.74/70.94 [25]P7(x252,x253,x254)+~E(x251,x252)+~P7(x251,x253,x254) % 70.74/70.94 [26]P7(x263,x262,x264)+~E(x261,x262)+~P7(x263,x261,x264) % 70.74/70.94 [27]P7(x273,x274,x272)+~E(x271,x272)+~P7(x273,x274,x271) % 70.74/70.94 % 70.74/70.94 %------------------------------------------- % 70.74/70.94 cnf(57,plain, % 70.74/70.94 (~P1(x571,x571)), % 70.74/70.94 inference(equality_inference,[],[47])). % 70.74/70.94 cnf(63,plain, % 70.74/70.94 (~P1(x631,x631)), % 70.74/70.94 inference(rename_variables,[],[57])). % 70.74/70.94 cnf(66,plain, % 70.74/70.94 (P4(x661,a5)+~E(a4,x661)), % 70.74/70.94 inference(scs_inference,[],[28,57,63,29,48,50,6,7,8])). % 70.74/70.94 cnf(162,plain, % 70.74/70.94 (P4(x1621,a6)+~E(a8,x1621)), % 70.74/70.94 inference(scs_inference,[],[34,32,33,31,15,9,13,8])). % 70.74/70.94 cnf(284,plain, % 70.74/70.94 (P5(x2841,f2(a5,x2841),a5)+~E(a4,x2841)), % 70.74/70.94 inference(scs_inference,[],[51,66])). % 70.74/70.94 cnf(285,plain, % 70.74/70.94 (P5(a4,f2(a5,a4),a5)), % 70.74/70.94 inference(equality_inference,[],[284])). % 70.74/70.94 cnf(3556,plain, % 70.74/70.94 (P5(x35561,f2(a6,x35561),a6)+~E(a8,x35561)), % 70.74/70.94 inference(scs_inference,[],[162,51])). % 70.74/70.94 cnf(3557,plain, % 70.74/70.94 (P5(a8,f2(a6,a8),a6)), % 70.74/70.94 inference(equality_inference,[],[3556])). % 70.74/70.94 cnf(6832,plain, % 70.74/70.94 (~P1(x68321,a13)+~P1(a12,x68321)), % 70.74/70.94 inference(scs_inference,[],[46,49])). % 70.74/70.94 cnf(10659,plain, % 70.74/70.94 (P1(a7,a5)), % 70.74/70.94 inference(scs_inference,[],[37,50])). % 70.74/70.94 cnf(10661,plain, % 70.74/70.94 (~P1(a5,a7)), % 70.74/70.95 inference(scs_inference,[],[57,37,50,49])). % 70.74/70.95 cnf(10664,plain, % 70.74/70.95 (P1(a6,a7)), % 70.74/70.95 inference(scs_inference,[],[28,57,32,37,44,29,38,31,45,43,41,42,40,50,49,55])). % 70.74/70.95 cnf(10725,plain, % 70.74/70.95 (~P4(a4,a7)+~P5(a4,a13,a7)), % 70.74/70.95 inference(scs_inference,[],[10664,46,34,30,39,53])). % 70.74/70.95 cnf(10746,plain, % 70.74/70.95 (~P4(a4,a7)+P1(a7,a7)+P1(f2(a5,a4),x107461)+~P5(a4,x107461,a7)), % 70.74/70.95 inference(scs_inference,[],[29,10659,285,57,37,54])). % 70.74/70.95 cnf(10748,plain, % 70.74/70.95 (~P4(a4,a7)+P1(f2(a5,a4),x107481)+~P5(a4,x107481,a7)), % 70.74/70.95 inference(scs_inference,[],[57,10746])). % 70.74/70.95 cnf(10749,plain, % 70.74/70.95 (~P4(a4,a7)+~P5(a4,f2(a5,a4),a7)), % 70.74/70.95 inference(scs_inference,[],[57,10748])). % 70.74/70.95 cnf(10829,plain, % 70.74/70.95 (P4(a8,a7)), % 70.74/70.95 inference(scs_inference,[],[31,10659,10664,32,52])). % 70.74/70.95 cnf(10831,plain, % 70.74/70.95 (P5(a8,f2(a7,a8),a7)), % 70.74/70.95 inference(scs_inference,[],[31,10659,10664,32,52,51])). % 70.74/70.95 cnf(10908,plain, % 70.74/70.95 (P1(a9,x109081)+~P4(a4,a7)+P1(a5,a5)+~P5(a4,x109081,a7)), % 70.74/70.95 inference(scs_inference,[],[32,10831,10829,10659,3557,33,57,37,29,54])). % 70.74/70.95 cnf(10911,plain, % 70.74/70.95 (~P4(a4,a7)+P1(a9,x109111)+~P5(a4,x109111,a7)), % 70.74/70.95 inference(scs_inference,[],[57,10908])). % 70.74/70.95 cnf(10913,plain, % 70.74/70.95 (~P1(x109131,x109131)), % 70.74/70.95 inference(rename_variables,[],[57])). % 70.74/70.95 cnf(10915,plain, % 70.74/70.95 (~P4(a4,a7)+~P5(a4,a9,a7)), % 70.74/70.95 inference(scs_inference,[],[10829,45,43,40,42,41,57,10913,37,44,29,28,31,55,10911])). % 70.74/70.95 cnf(10923,plain, % 70.74/70.95 (P1(f2(a7,a8),a13)), % 70.74/70.95 inference(scs_inference,[],[10661,10831,10829,10664,57,32,36,38,54])). % 70.74/70.95 cnf(10926,plain, % 70.74/70.95 (~P1(a12,f2(a7,a8))), % 70.74/70.95 inference(scs_inference,[],[10661,10831,10829,10664,57,32,36,38,54,6832])). % 70.74/70.95 cnf(11927,plain, % 70.74/70.95 (P4(a4,a7)), % 70.74/70.95 inference(scs_inference,[],[10664,10659,30,29,52])). % 70.74/70.95 cnf(11932,plain, % 70.74/70.95 (P5(a4,f2(a7,a4),a7)), % 70.74/70.95 inference(scs_inference,[],[10664,10659,30,29,52,10725,10915,10749,51])). % 70.74/70.95 cnf(11936,plain, % 70.74/70.95 (P1(a9,f2(a7,a4))), % 70.74/70.95 inference(scs_inference,[],[10664,10659,30,29,52,10725,10915,10749,51,10748,10911])). % 70.74/70.95 cnf(11996,plain, % 70.74/70.95 (~P5(a4,f2(a7,a8),a7)), % 70.74/70.95 inference(scs_inference,[],[10664,11927,10926,30,34,39,53])). % 70.74/70.95 cnf(12005,plain, % 70.74/70.95 (~E(f2(a7,a4),f2(a7,a8))), % 70.74/70.95 inference(scs_inference,[],[11996,11936,11932,57,15,7,14])). % 70.74/70.95 cnf(12073,plain, % 70.74/70.95 (P1(f2(a7,a4),f2(a7,a8))), % 70.74/70.95 inference(scs_inference,[],[12005,11932,11927,38,10831,33,29,45,40,10829,43,42,41,31,35,44,37,28,56])). % 70.74/70.95 cnf(12144,plain, % 70.74/70.95 (~P1(a12,f2(a7,a4))), % 70.74/70.95 inference(scs_inference,[],[12073,10923,49,6832])). % 70.74/70.95 cnf(12269,plain, % 70.74/70.95 ($false), % 70.74/70.95 inference(scs_inference,[],[12144,11932,10664,11927,30,34,39,53]), % 70.74/70.95 ['proof']). % 70.74/70.95 % SZS output end Proof % 70.74/70.95 % Total time :70.360875s %------------------------------------------------------------------------------