%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT005+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n007.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 : Theorem 66.35s 66.54s % 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.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.07/0.34 % Computer : n007.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Mon Sep 7 11:34:26 UTC 2026 % 0.07/0.34 % CPUTime : % 0.23/0.50 start to proof:theBenchmark % 66.35/66.53 %------------------------------------------- % 66.35/66.53 % File :CSE---1.7 % 66.35/66.53 % Problem :theBenchmark % 66.35/66.53 % Transform :cnf % 66.35/66.53 % Format :tptp:raw % 66.35/66.53 % Command :java -jar mcs_scs.jar %d %s % 66.35/66.53 % 66.35/66.53 % Result :Theorem 66.041954s % 66.35/66.53 % Output :CNFRefutation 66.041954s % 66.35/66.53 %------------------------------------------- % 66.35/66.53 %-------------------------------------------------------------------------- % 66.35/66.53 % File : MGT005+1 : TPTP v9.3.0. Released v2.0.0. % 66.35/66.53 % Domain : Management (Organisation Theory) % 66.35/66.53 % Problem : Complexity increases the risk of death due to reorganization. % 66.35/66.53 % Version : [PB+94] axioms. % 66.35/66.53 % English : % 66.35/66.53 % 66.35/66.53 % Refs : [PB+92] Peli et al. (1992), A Logical Approach to Formalizing % 66.35/66.53 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 66.35/66.53 % : [Kam94] Kamps (1994), Email to G. Sutcliffe % 66.35/66.53 % Source : [Kam94] % 66.35/66.53 % Names : THEOREM 5 [PB+92] % 66.35/66.53 % 66.35/66.53 % Status : Theorem % 66.35/66.53 % Rating : 0.30 v9.3.0, 0.36 v9.1.0, 0.27 v9.0.0, 0.31 v8.2.0, 0.28 v8.1.0, 0.22 v7.5.0, 0.28 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.28 v6.1.0, 0.37 v6.0.0, 0.35 v5.5.0, 0.37 v5.4.0, 0.36 v5.3.0, 0.44 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.0, 0.33 v3.7.0, 0.14 v3.5.0, 0.11 v3.4.0, 0.08 v3.3.0, 0.22 v3.2.0, 0.33 v3.1.0, 0.50 v2.7.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.50 v2.1.0 % 66.35/66.53 % Syntax : Number of formulae : 11 ( 0 unt; 0 def) % 66.35/66.53 % Number of atoms : 83 ( 2 equ) % 66.35/66.53 % Maximal formula atoms : 19 ( 7 avg) % 66.35/66.53 % Number of connectives : 76 ( 4 ~; 1 |; 62 &) % 66.35/66.53 % ( 0 <=>; 9 =>; 0 <=; 0 <~>) % 66.35/66.53 % Maximal formula depth : 31 ( 13 avg) % 66.35/66.53 % Maximal term depth : 1 ( 1 avg) % 66.35/66.53 % Number of predicates : 9 ( 8 usr; 0 prp; 2-3 aty) % 66.35/66.53 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 66.35/66.53 % Number of variables : 62 ( 61 !; 1 ?) % 66.35/66.53 % SPC : FOF_THM_RFO_SEQ % 66.35/66.53 % 66.35/66.53 % Comments : mp11, mp12 and mp13 correspond to mp10, mp11 and mp12 % 66.35/66.53 % respectively from [PB+92] % 66.35/66.53 %-------------------------------------------------------------------------- % 66.35/66.53 %----Problem axioms % 66.35/66.53 fof(mp6_1,axiom, % 66.35/66.53 ! [X,Y] : % 66.35/66.53 ~ ( greater(X,Y) % 66.35/66.53 & X = Y ) ). % 66.35/66.53 % 66.35/66.53 fof(mp6_2,axiom, % 66.35/66.53 ! [X,Y] : % 66.35/66.53 ~ ( greater(X,Y) % 66.35/66.53 & greater(Y,X) ) ). % 66.35/66.53 % 66.35/66.54 fof(mp11,axiom, % 66.35/66.54 ! [X,Y,Z] : % 66.35/66.54 ( ( greater(X,Y) % 66.35/66.54 & greater(Y,Z) ) % 66.35/66.54 => greater(X,Z) ) ). % 66.35/66.54 % 66.35/66.54 fof(mp12,axiom, % 66.35/66.54 ! [X,T] : % 66.35/66.54 ( organization(X,T) % 66.35/66.54 => ? [P] : survival_chance(X,P,T) ) ). % 66.35/66.54 % 66.35/66.54 fof(mp13,axiom, % 66.35/66.54 ! [X,T,T1,T2] : % 66.35/66.54 ( ( organization(X,T1) % 66.35/66.54 & organization(X,T2) % 66.35/66.54 & greater(T,T1) % 66.35/66.54 & greater(T2,T) ) % 66.35/66.54 => organization(X,T) ) ). % 66.35/66.54 % 66.35/66.54 fof(mp7,axiom, % 66.35/66.54 ! [X,Ta,Tb] : % 66.35/66.54 ( reorganization(X,Ta,Tb) % 66.35/66.54 => greater(Tb,Ta) ) ). % 66.35/66.54 % 66.35/66.54 fof(t3_FOL,hypothesis, % 66.35/66.54 ! [X,P1,P2,T1,T2] : % 66.35/66.54 ( ( organization(X,T1) % 66.35/66.54 & organization(X,T2) % 66.35/66.54 & reorganization_free(X,T1,T2) % 66.35/66.54 & survival_chance(X,P1,T1) % 66.35/66.54 & survival_chance(X,P2,T2) % 66.35/66.54 & greater(T2,T1) ) % 66.35/66.54 => greater(P2,P1) ) ). % 66.35/66.54 % 66.35/66.54 %----t4_FOL - alias a9_FOL % 66.35/66.54 fof(t4_FOL,hypothesis, % 66.35/66.54 ! [X,P1,P2,T1,T2,Ta,Tb] : % 66.35/66.54 ( ( organization(X,T1) % 66.35/66.54 & organization(X,T2) % 66.35/66.54 & reorganization(X,Ta,Tb) % 66.35/66.54 & survival_chance(X,P1,T1) % 66.35/66.54 & survival_chance(X,P2,T2) % 66.35/66.54 & ~ greater(Ta,T1) % 66.35/66.54 & greater(T2,T1) % 66.35/66.54 & ~ greater(T2,Tb) ) % 66.35/66.54 => greater(P1,P2) ) ). % 66.35/66.54 % 66.35/66.54 %----Complexity increases the expected duration of reorganization. % 66.35/66.54 fof(a10_FOL,hypothesis, % 66.35/66.54 ! [X,Y,Re,C,C1,C2,Ta,Tb,Tc] : % 66.35/66.54 ( ( organization(X,Ta) % 66.35/66.54 & organization(Y,Ta) % 66.35/66.54 & organization(Y,Tc) % 66.35/66.54 & class(X,C,Ta) % 66.35/66.54 & class(Y,C,Ta) % 66.35/66.54 & reorganization(X,Ta,Tb) % 66.35/66.54 & reorganization(Y,Ta,Tc) % 66.35/66.54 & reorganization_type(X,Re,Ta) % 66.35/66.54 & reorganization_type(Y,Re,Ta) % 66.35/66.54 & complexity(X,C1,Ta) % 66.35/66.54 & complexity(Y,C2,Ta) % 66.35/66.54 & greater(C2,C1) ) % 66.35/66.54 => greater(Tc,Tb) ) ). % 66.35/66.54 % 66.35/66.54 %----Complexity is no survival advantage during reorganization. % 66.35/66.54 fof(a11_FOL,hypothesis, % 66.35/66.54 ! [X,Y,Re,C,P,P1,P2,C1,C2,Ta,Tb,Tc] : % 66.35/66.54 ( ( organization(X,Ta) % 66.35/66.54 & organization(Y,Ta) % 66.35/66.54 & organization(X,Tb) % 66.35/66.54 & organization(Y,Tb) % 66.35/66.54 & class(X,C,Ta) % 66.35/66.54 & class(Y,C,Ta) % 66.35/66.54 & survival_chance(X,P,Ta) % 66.35/66.54 & survival_chance(Y,P,Ta) % 66.35/66.54 & reorganization(X,Ta,Tb) % 66.35/66.54 & reorganization(Y,Ta,Tc) % 66.35/66.54 & reorganization_type(X,Re,Ta) % 66.35/66.54 & reorganization_type(Y,Re,Ta) % 66.35/66.54 & survival_chance(X,P1,Tb) % 66.35/66.54 & survival_chance(Y,P2,Tb) % 66.35/66.54 & complexity(X,C1,Ta) % 66.35/66.54 & complexity(Y,C2,Ta) % 66.35/66.54 & greater(C2,C1) ) % 66.35/66.54 => ( greater(P1,P2) % 66.35/66.54 | P1 = P2 ) ) ). % 66.35/66.54 % 66.35/66.54 fof(t5_FOL,conjecture, % 66.35/66.54 ! [X,Y,Re,C,P,P1,P2,C1,C2,Ta,Tb,Tc] : % 66.35/66.54 ( ( organization(X,Ta) % 66.35/66.54 & organization(Y,Ta) % 66.35/66.54 & organization(X,Tc) % 66.35/66.54 & organization(Y,Tc) % 66.35/66.54 & class(X,C,Ta) % 66.35/66.54 & class(Y,C,Ta) % 66.35/66.54 & survival_chance(X,P,Ta) % 66.35/66.54 & survival_chance(Y,P,Ta) % 66.35/66.54 & reorganization(X,Ta,Tb) % 66.35/66.54 & reorganization(Y,Ta,Tc) % 66.35/66.54 & reorganization_type(X,Re,Ta) % 66.35/66.54 & reorganization_type(Y,Re,Ta) % 66.35/66.54 & reorganization_free(X,Tb,Tc) % 66.35/66.54 & survival_chance(X,P1,Tc) % 66.35/66.54 & survival_chance(Y,P2,Tc) % 66.35/66.54 & complexity(X,C1,Ta) % 66.35/66.54 & complexity(Y,C2,Ta) % 66.35/66.54 & greater(C2,C1) ) % 66.35/66.54 => greater(P1,P2) ) ). % 66.35/66.54 % 66.35/66.54 %-------------------------------------------------------------------------- % 66.35/66.54 %------------------------------------------- % 66.35/66.54 % Proof found % 66.35/66.54 % SZS status Theorem for theBenchmark % 66.35/66.54 % SZS output start Proof % 66.35/66.54 %ClaNum:56(EqnAxiom:27) % 66.35/66.54 %VarNum:157(SingletonVarNum:49) % 66.35/66.54 %MaxLitNum:19 % 66.35/66.54 %MaxfuncDepth:1 % 66.35/66.54 %SharedTerms:31 % 66.35/66.54 %goalClause: 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 % 66.35/66.54 %singleGoalClaCount:19 % 66.35/66.54 [28]P1(a1,a2) % 66.35/66.54 [29]P4(a3,a4) % 66.35/66.54 [30]P4(a3,a5) % 66.35/66.54 [31]P4(a8,a4) % 66.35/66.54 [32]P4(a8,a5) % 66.35/66.54 [33]P5(a3,a9,a4) % 66.35/66.54 [34]P5(a3,a12,a5) % 66.35/66.54 [35]P5(a8,a9,a4) % 66.35/66.54 [36]P5(a8,a13,a5) % 66.35/66.54 [37]P6(a3,a4,a6) % 66.35/66.54 [38]P6(a8,a4,a5) % 66.35/66.54 [39]P7(a3,a6,a5) % 66.35/66.54 [40]P2(a3,a10,a4) % 66.35/66.54 [41]P2(a8,a10,a4) % 66.35/66.54 [42]P8(a3,a11,a4) % 66.35/66.54 [43]P8(a8,a11,a4) % 66.35/66.54 [44]P3(a3,a2,a4) % 66.35/66.54 [45]P3(a8,a1,a4) % 66.35/66.54 [46]~P1(a12,a13) % 66.35/66.54 [47]~P1(x471,x472)+~E(x471,x472) % 66.35/66.54 [48]~P1(x482,x481)+~P1(x481,x482) % 66.35/66.54 [51]~P4(x511,x512)+P5(x511,f7(x511,x512),x512) % 66.35/66.54 [50]P1(x501,x502)+~P6(x503,x502,x501) % 66.35/66.54 [49]~P1(x491,x493)+P1(x491,x492)+~P1(x493,x492) % 66.35/66.54 [52]~P4(x521,x524)+~P4(x521,x523)+P4(x521,x522)+~P1(x522,x523)+~P1(x524,x522) % 66.35/66.54 [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) % 66.35/66.54 [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) % 66.35/66.54 [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) % 66.35/66.54 [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) % 66.35/66.54 %EqnAxiom % 66.35/66.54 [1]E(x11,x11) % 66.35/66.54 [2]E(x22,x21)+~E(x21,x22) % 66.35/66.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 66.35/66.54 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43)) % 66.35/66.54 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52)) % 66.35/66.54 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63) % 66.35/66.54 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71) % 66.35/66.54 [8]P4(x82,x83)+~E(x81,x82)+~P4(x81,x83) % 66.35/66.54 [9]P4(x93,x92)+~E(x91,x92)+~P4(x93,x91) % 66.35/66.54 [10]P8(x102,x103,x104)+~E(x101,x102)+~P8(x101,x103,x104) % 66.35/66.54 [11]P8(x113,x112,x114)+~E(x111,x112)+~P8(x113,x111,x114) % 66.35/66.54 [12]P8(x123,x124,x122)+~E(x121,x122)+~P8(x123,x124,x121) % 66.35/66.54 [13]P5(x132,x133,x134)+~E(x131,x132)+~P5(x131,x133,x134) % 66.35/66.54 [14]P5(x143,x142,x144)+~E(x141,x142)+~P5(x143,x141,x144) % 66.35/66.54 [15]P5(x153,x154,x152)+~E(x151,x152)+~P5(x153,x154,x151) % 66.35/66.54 [16]P2(x162,x163,x164)+~E(x161,x162)+~P2(x161,x163,x164) % 66.35/66.54 [17]P2(x173,x172,x174)+~E(x171,x172)+~P2(x173,x171,x174) % 66.35/66.54 [18]P2(x183,x184,x182)+~E(x181,x182)+~P2(x183,x184,x181) % 66.35/66.54 [19]P6(x192,x193,x194)+~E(x191,x192)+~P6(x191,x193,x194) % 66.35/66.54 [20]P6(x203,x202,x204)+~E(x201,x202)+~P6(x203,x201,x204) % 66.35/66.54 [21]P6(x213,x214,x212)+~E(x211,x212)+~P6(x213,x214,x211) % 66.35/66.54 [22]P3(x222,x223,x224)+~E(x221,x222)+~P3(x221,x223,x224) % 66.35/66.54 [23]P3(x233,x232,x234)+~E(x231,x232)+~P3(x233,x231,x234) % 66.35/66.54 [24]P3(x243,x244,x242)+~E(x241,x242)+~P3(x243,x244,x241) % 66.35/66.54 [25]P7(x252,x253,x254)+~E(x251,x252)+~P7(x251,x253,x254) % 66.35/66.54 [26]P7(x263,x262,x264)+~E(x261,x262)+~P7(x263,x261,x264) % 66.35/66.54 [27]P7(x273,x274,x272)+~E(x271,x272)+~P7(x273,x274,x271) % 66.35/66.54 % 66.35/66.54 %------------------------------------------- % 66.35/66.54 cnf(57,plain, % 66.35/66.54 (~P1(x571,x571)), % 66.35/66.54 inference(equality_inference,[],[47])). % 66.35/66.54 cnf(58,plain, % 66.35/66.54 (~P1(a2,a1)), % 66.35/66.54 inference(scs_inference,[],[28,48])). % 66.35/66.54 cnf(60,plain, % 66.35/66.54 (~P6(x601,x602,x602)), % 66.35/66.54 inference(scs_inference,[],[28,57,48,50])). % 66.35/66.54 cnf(63,plain, % 66.35/66.54 (~P1(x631,x631)), % 66.35/66.54 inference(rename_variables,[],[57])). % 66.35/66.54 cnf(66,plain, % 66.35/66.54 (P4(x661,a4)+~E(a3,x661)), % 66.35/66.54 inference(scs_inference,[],[28,57,63,29,48,50,6,7,8])). % 66.35/66.54 cnf(81,plain, % 66.35/66.54 (~P6(x811,x812,x812)), % 66.35/66.54 inference(rename_variables,[],[60])). % 66.35/66.54 cnf(82,plain, % 66.35/66.54 (~E(a6,a4)), % 66.35/66.54 inference(scs_inference,[],[37,46,60,81,50,20,21])). % 66.35/66.55 cnf(130,plain, % 66.35/66.55 (P4(x1301,a4)+~E(a8,x1301)), % 66.35/66.55 inference(scs_inference,[],[38,31,43,41,12,19,11,18,8])). % 66.35/66.55 cnf(164,plain, % 66.35/66.55 (P4(x1641,a5)+~E(a8,x1641)), % 66.35/66.55 inference(scs_inference,[],[36,32,15,8])). % 66.35/66.55 cnf(282,plain, % 66.35/66.55 (P5(x2821,f7(x2821,a4),a4)+~E(a3,x2821)), % 66.35/66.55 inference(scs_inference,[],[51,66])). % 66.35/66.55 cnf(283,plain, % 66.35/66.55 (P5(a3,f7(a3,a4),a4)), % 66.35/66.55 inference(equality_inference,[],[282])). % 66.35/66.55 cnf(862,plain, % 66.35/66.55 (~P1(a5,a6)+~P4(a3,a6)+~P5(a3,a12,a6)), % 66.35/66.55 inference(scs_inference,[],[31,39,34,30,57,28,53])). % 66.35/66.55 cnf(2710,plain, % 66.35/66.55 (P5(x27101,f7(x27101,a4),a4)+~E(a8,x27101)), % 66.35/66.55 inference(scs_inference,[],[130,51])). % 66.35/66.55 cnf(2711,plain, % 66.35/66.55 (P5(a8,f7(a8,a4),a4)), % 66.35/66.55 inference(equality_inference,[],[2710])). % 66.35/66.55 cnf(3547,plain, % 66.35/66.55 (P5(x35471,f7(x35471,a5),a5)+~E(a8,x35471)), % 66.35/66.55 inference(scs_inference,[],[164,51])). % 66.35/66.55 cnf(3548,plain, % 66.35/66.55 (P5(a8,f7(a8,a5),a5)), % 66.35/66.55 inference(equality_inference,[],[3547])). % 66.35/66.55 cnf(6820,plain, % 66.35/66.55 (~P1(x68201,a13)+~E(x68201,a12)), % 66.35/66.55 inference(scs_inference,[],[46,6])). % 66.35/66.55 cnf(6827,plain, % 66.35/66.55 (~P1(x68271,a13)+~P1(a12,x68271)), % 66.35/66.55 inference(scs_inference,[],[46,49])). % 66.35/66.55 cnf(6839,plain, % 66.35/66.55 (~P1(a12,x68391)+~E(x68391,a13)), % 66.35/66.55 inference(scs_inference,[],[46,82,3,7])). % 66.35/66.55 cnf(10580,plain, % 66.35/66.55 (P5(a3,f7(a3,a5),a5)), % 66.35/66.55 inference(scs_inference,[],[30,51])). % 66.35/66.55 cnf(10582,plain, % 66.35/66.55 (P1(a5,a4)), % 66.35/66.55 inference(scs_inference,[],[38,30,51,50])). % 66.35/66.55 cnf(10595,plain, % 66.35/66.55 (P1(a6,a4)), % 66.35/66.55 inference(scs_inference,[],[37,50])). % 66.35/66.55 cnf(10597,plain, % 66.35/66.55 (~P1(a4,a6)), % 66.35/66.55 inference(scs_inference,[],[57,37,50,49])). % 66.35/66.55 cnf(10605,plain, % 66.35/66.55 (P1(a5,a6)), % 66.35/66.55 inference(scs_inference,[],[28,38,37,31,29,44,32,45,42,41,40,43,55])). % 66.35/66.55 cnf(10607,plain, % 66.35/66.55 (~P1(a6,a5)), % 66.35/66.55 inference(scs_inference,[],[28,38,37,31,29,44,32,45,42,41,40,43,55,48])). % 66.35/66.55 cnf(10612,plain, % 66.35/66.55 (~P4(a3,a6)+~P5(a3,a12,a6)), % 66.35/66.55 inference(scs_inference,[],[10605,862])). % 66.35/66.55 cnf(10613,plain, % 66.35/66.55 (P4(a3,a6)), % 66.35/66.55 inference(scs_inference,[],[10605,10595,29,30,52])). % 66.35/66.55 cnf(10617,plain, % 66.35/66.55 (P5(a3,f7(a3,a6),a6)), % 66.35/66.55 inference(scs_inference,[],[10605,10580,10595,10582,283,29,30,52,53,51])). % 66.35/66.55 cnf(10628,plain, % 66.35/66.55 (P1(a5,a5)+P1(a9,a13)), % 66.35/66.55 inference(scs_inference,[],[10613,10617,10582,35,36,38,57,31,32,10612,14,13,54])). % 66.35/66.55 cnf(10633,plain, % 66.35/66.55 (~P1(x106331,x106331)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(10643,plain, % 66.35/66.55 (~P1(a12,a9)), % 66.35/66.55 inference(scs_inference,[],[10617,10613,10605,10580,57,10633,30,39,10628,47,48,7,53,6820,6827])). % 66.35/66.55 cnf(10668,plain, % 66.35/66.55 (P1(a12,f7(a3,a6))), % 66.35/66.55 inference(scs_inference,[],[10617,10605,10613,30,34,39,53])). % 66.35/66.55 cnf(10673,plain, % 66.35/66.55 (~P1(f7(a3,a6),a12)), % 66.35/66.55 inference(scs_inference,[],[10617,10605,10613,30,34,39,53,6839,47,48])). % 66.35/66.55 cnf(10675,plain, % 66.35/66.55 (~P1(f7(a3,a6),a9)), % 66.35/66.55 inference(scs_inference,[],[10643,10617,10605,10613,30,34,39,53,6839,47,48,49])). % 66.35/66.55 cnf(10677,plain, % 66.35/66.55 (P1(a4,a4)+P1(f7(a3,a4),f7(a3,a6))), % 66.35/66.55 inference(scs_inference,[],[10643,10617,10605,10595,10613,283,57,37,29,30,34,39,53,6839,47,48,49,54])). % 66.35/66.55 cnf(10681,plain, % 66.35/66.55 (P1(f7(a3,a4),f7(a3,a6))), % 66.35/66.55 inference(scs_inference,[],[57,10677])). % 66.35/66.55 cnf(10749,plain, % 66.35/66.55 (P1(a9,f7(a8,a5))), % 66.35/66.55 inference(scs_inference,[],[3548,10582,35,38,57,31,32,54,47])). % 66.35/66.55 cnf(10860,plain, % 66.35/66.55 (P1(x108601,f7(a8,a5))+~P4(a8,a6)+~P5(a8,x108601,a6)), % 66.35/66.55 inference(scs_inference,[],[10597,3548,10605,35,38,57,31,32,54])). % 66.35/66.55 cnf(10978,plain, % 66.35/66.55 (~P1(x109781,x109781)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(10980,plain, % 66.35/66.55 (P1(a9,x109801)+~P4(a8,a6)+~P5(a8,x109801,a6)), % 66.35/66.55 inference(scs_inference,[],[31,10607,10595,283,35,10613,38,57,10978,29,54])). % 66.35/66.55 cnf(11273,plain, % 66.35/66.55 (~P1(x112731,x112731)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(11275,plain, % 66.35/66.55 (P1(x112751,f7(a8,a5))+~P1(a5,a9)+~P4(a8,a9)+~P5(a8,x112751,a9)+~P6(a8,f7(a3,a6),a5)), % 66.35/66.55 inference(scs_inference,[],[10675,3548,57,11273,32,54])). % 66.35/66.55 cnf(11307,plain, % 66.35/66.55 (~P1(f7(a3,a6),a13)), % 66.35/66.55 inference(scs_inference,[],[46,10668,49])). % 66.35/66.55 cnf(11357,plain, % 66.35/66.55 (~P1(x113571,x113571)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(11358,plain, % 66.35/66.55 (~P4(a8,a6)+~P5(a8,f7(a3,a6),a6)), % 66.35/66.55 inference(scs_inference,[],[58,32,11307,10749,10605,10597,36,38,57,11357,11275,53,54])). % 66.35/66.55 cnf(11459,plain, % 66.35/66.55 (~P1(x114591,x114591)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(11461,plain, % 66.35/66.55 (P1(f7(a8,a4),x114611)+~P4(a8,a6)+~P5(a8,x114611,a6)), % 66.35/66.55 inference(scs_inference,[],[10673,10681,10595,10607,2711,38,57,11459,31,54])). % 66.35/66.55 cnf(11462,plain, % 66.35/66.55 (~P4(a8,a6)+~P5(a8,f7(a8,a4),a6)), % 66.35/66.55 inference(scs_inference,[],[57,11461])). % 66.35/66.55 cnf(11639,plain, % 66.35/66.55 (P4(a8,a6)), % 66.35/66.55 inference(scs_inference,[],[31,10605,10595,32,52])). % 66.35/66.55 cnf(11643,plain, % 66.35/66.55 (P5(a8,f7(a8,a6),a6)), % 66.35/66.55 inference(scs_inference,[],[31,10605,10595,32,52,11358,11462,51])). % 66.35/66.55 cnf(11667,plain, % 66.35/66.55 (P1(x116671,f7(a8,a5))+~P5(a8,x116671,a6)), % 66.35/66.55 inference(scs_inference,[],[11639,10860])). % 66.35/66.55 cnf(11668,plain, % 66.35/66.55 (P1(a9,x116681)+~P5(a8,x116681,a6)), % 66.35/66.55 inference(scs_inference,[],[11639,10980])). % 66.35/66.55 cnf(11671,plain, % 66.35/66.55 (P1(f7(a8,a4),x116711)+~P5(a8,x116711,a6)), % 66.35/66.55 inference(scs_inference,[],[11639,11461])). % 66.35/66.55 cnf(11685,plain, % 66.35/66.55 (~P1(x116851,x116851)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(11688,plain, % 66.35/66.55 (~P1(x116881,x116881)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(11690,plain, % 66.35/66.55 (~P1(x116901,x116901)), % 66.35/66.55 inference(rename_variables,[],[57])). % 66.35/66.55 cnf(11694,plain, % 66.35/66.55 (~P1(a12,f7(a8,a6))), % 66.35/66.55 inference(scs_inference,[],[11639,11643,10605,10597,36,32,57,11685,11688,11690,38,11668,11667,11671,47,48,49,6,7,54,6827])). % 66.35/66.55 cnf(11728,plain, % 66.35/66.55 (~P1(f7(a3,a6),f7(a8,a6))), % 66.35/66.55 inference(scs_inference,[],[11694,10668,49])). % 66.35/66.55 cnf(11730,plain, % 66.35/66.55 (~E(f7(a3,a6),f7(a8,a6))), % 66.35/66.55 inference(scs_inference,[],[11694,10668,49,7])). % 66.35/66.55 cnf(11754,plain, % 66.35/66.55 ($false), % 66.35/66.55 inference(scs_inference,[],[11730,11728,11639,11643,31,45,10617,35,33,28,40,42,41,43,10613,44,38,37,29,56]), % 66.35/66.55 ['proof']). % 66.35/66.55 % SZS output end Proof % 66.35/66.55 % Total time :66.041954s %------------------------------------------------------------------------------