%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT062+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 : n019.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:22 AM UTC 2026
% Result : Theorem 127.97s 128.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT062+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 13:37:52 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.23/0.51 start to proof:theBenchmark
% 127.97/128.07 %-------------------------------------------
% 127.97/128.07 % File :CSE---1.7
% 127.97/128.07 % Problem :theBenchmark
% 127.97/128.07 % Transform :cnf
% 127.97/128.07 % Format :tptp:raw
% 127.97/128.07 % Command :java -jar mcs_scs.jar %d %s
% 127.97/128.07
% 127.97/128.07 % Result :Theorem 127.568245s
% 127.97/128.07 % Output :CNFRefutation 127.568245s
% 127.97/128.07 %-------------------------------------------
% 127.97/128.08 %--------------------------------------------------------------------------
% 127.97/128.08 % File : MGT062+1 : TPTP v9.3.0. Released v2.4.0.
% 127.97/128.08 % Domain : Management (Organisation Theory)
% 127.97/128.08 % Problem : Condictions for decreasing hazard of mortality
% 127.97/128.08 % Version : [Han98] axioms.
% 127.97/128.08 % English : If environmental drift destroys alignment exactly when advantage
% 127.97/128.08 % can be gained from occupancy of a robust position, then the
% 127.97/128.08 % hazard of mortality for an unendowed organization with a robust
% 127.97/128.08 % position decreases with age.
% 127.97/128.08
% 127.97/128.08 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 127.97/128.08 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 127.97/128.08 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 127.97/128.08 % Source : [Kam00]
% 127.97/128.08 % Names : THEOREM 8 [Han98]
% 127.97/128.08
% 127.97/128.08 % Status : Theorem
% 127.97/128.08 % Rating : 0.17 v9.3.0, 0.27 v9.1.0, 0.21 v9.0.0, 0.31 v8.2.0, 0.25 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.20 v6.1.0, 0.33 v6.0.0, 0.35 v5.5.0, 0.44 v5.4.0, 0.43 v5.3.0, 0.44 v5.2.0, 0.35 v5.1.0, 0.38 v4.1.0, 0.35 v4.0.0, 0.33 v3.7.0, 0.35 v3.5.0, 0.32 v3.4.0, 0.21 v3.2.0, 0.36 v3.1.0, 0.56 v2.7.0, 0.33 v2.4.0
% 127.97/128.08 % Syntax : Number of formulae : 14 ( 1 unt; 0 def)
% 127.97/128.08 % Number of atoms : 63 ( 13 equ)
% 127.97/128.08 % Maximal formula atoms : 16 ( 4 avg)
% 127.97/128.08 % Number of connectives : 60 ( 11 ~; 4 |; 24 &)
% 127.97/128.08 % ( 7 <=>; 14 =>; 0 <=; 0 <~>)
% 127.97/128.08 % Maximal formula depth : 14 ( 6 avg)
% 127.97/128.08 % Maximal term depth : 2 ( 1 avg)
% 127.97/128.08 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty)
% 127.97/128.08 % Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% 127.97/128.08 % Number of variables : 31 ( 31 !; 0 ?)
% 127.97/128.08 % SPC : FOF_THM_RFO_SEQ
% 127.97/128.08
% 127.97/128.08 % Comments : See MGT042+1.p for the mnemonic names.
% 127.97/128.08 %--------------------------------------------------------------------------
% 127.97/128.08 include('Axioms/MGT001+0.ax').
% 127.97/128.08 %--------------------------------------------------------------------------
% 127.97/128.08 %----Problem Axioms
% 127.97/128.08 %----An unendowed organization never possesses immunity.
% 127.97/128.08 fof(assumption_1,axiom,
% 127.97/128.08 ! [X,T] :
% 127.97/128.08 ( ( organization(X)
% 127.97/128.08 & ~ has_endowment(X) )
% 127.97/128.08 => ~ has_immunity(X,T) ) ).
% 127.97/128.08
% 127.97/128.08 %----Two states of the environment are dissimilar for an organization
% 127.97/128.08 %----if and only if the organization cannot be aligned to both.
% 127.97/128.08 %----
% 127.97/128.08 %----Added quantification over X.
% 127.97/128.08 fof(definition_2,axiom,
% 127.97/128.08 ! [X,T0,T] :
% 127.97/128.08 ( dissimilar(X,T0,T)
% 127.97/128.08 <=> ( organization(X)
% 127.97/128.08 & ~ ( is_aligned(X,T0)
% 127.97/128.08 <=> is_aligned(X,T) ) ) ) ).
% 127.97/128.08
% 127.97/128.08 %----An organization is aligned with the state of the environment at
% 127.97/128.08 %----its time of founding.
% 127.97/128.08 fof(assumption_13,axiom,
% 127.97/128.08 ! [X,T] :
% 127.97/128.08 ( ( organization(X)
% 127.97/128.08 & age(X,T) = zero )
% 127.97/128.08 => is_aligned(X,T) ) ).
% 127.97/128.08
% 127.97/128.08 %----Environmental drift: the environments at times separated by more
% 127.97/128.08 %----than `sigma' are dissimilar.
% 127.97/128.08 fof(assumption_15,axiom,
% 127.97/128.08 ! [X,T0,T] :
% 127.97/128.08 ( ( organization(X)
% 127.97/128.08 & age(X,T0) = zero )
% 127.97/128.08 => ( greater(age(X,T),sigma)
% 127.97/128.08 <=> dissimilar(X,T0,T) ) ) ).
% 127.97/128.08
% 127.97/128.08 %----An organization's position is robust if and only if it provides
% 127.97/128.08 %----positional advantage only after age `tau'.
% 127.97/128.08 %----
% 127.97/128.08 %----Text says fragile_position(X) instead of robust_position(X).
% 127.97/128.08 %----Interchanged ~ positional_advantage(X,T) and positional_advantage(X,T).
% 127.97/128.08 fof(definition_4,axiom,
% 127.97/128.08 ! [X] :
% 127.97/128.08 ( robust_position(X)
% 127.97/128.08 <=> ! [T] :
% 127.97/128.08 ( ( smaller_or_equal(age(X,T),tau)
% 127.97/128.08 => ~ positional_advantage(X,T) )
% 127.97/128.08 & ( greater(age(X,T),tau)
% 127.97/128.08 => positional_advantage(X,T) ) ) ) ).
% 127.97/128.08
% 127.97/128.08 %----An organization's immunity. alignment of capability with the
% 127.97/128.08 %----current state of the environment and positional advantage jointly
% 127.97/128.08 %----affect the hazard of mortality with the following ordinal scaling:
% 127.97/128.08 fof(assumption_17,axiom,
% 127.97/128.08 ! [X,T] :
% 127.97/128.08 ( organization(X)
% 127.97/128.08 => ( ( has_immunity(X,T)
% 127.97/128.08 => hazard_of_mortality(X,T) = very_low )
% 127.97/128.08 & ( ~ has_immunity(X,T)
% 127.97/128.08 => ( ( ( is_aligned(X,T)
% 127.97/128.08 & positional_advantage(X,T) )
% 127.97/128.08 => hazard_of_mortality(X,T) = low )
% 127.97/128.08 & ( ( ~ is_aligned(X,T)
% 127.97/128.08 & positional_advantage(X,T) )
% 127.97/128.08 => hazard_of_mortality(X,T) = mod1 )
% 127.97/128.08 & ( ( is_aligned(X,T)
% 127.97/128.08 & ~ positional_advantage(X,T) )
% 127.97/128.08 => hazard_of_mortality(X,T) = mod2 )
% 127.97/128.08 & ( ( ~ is_aligned(X,T)
% 127.97/128.08 & ~ positional_advantage(X,T) )
% 127.97/128.08 => hazard_of_mortality(X,T) = high ) ) ) ) ) ).
% 127.97/128.08
% 127.97/128.08 %----Position dominates alignment:
% 127.97/128.08 fof(assumption_19,axiom,
% 127.97/128.08 greater(mod2,mod1) ).
% 127.97/128.08
% 127.97/128.08 %----Problem theorems
% 127.97/128.08 %----Robust position without endowment when (`sigma' = `tau'): If
% 127.97/128.08 %----environmental drift destroys alignment exactly when advantage can
% 127.97/128.08 %----be gained from occupancy of a robust position (`sigma' = `tau'), then
% 127.97/128.08 %----the hazard of mortality for an unendowed organization with a
% 127.97/128.08 %----robust position decreases with age.
% 127.97/128.08 %----From D2, D4 and A1, A13, A15, A17 (text says D1,2 and A1,2,13-15,17-19;
% 127.97/128.08 %----also needs D<, D<=).
% 127.97/128.08 %----
% 127.97/128.08 %----Added (`sigma' = `tau') in antecedent
% 127.97/128.08 %----and (hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)).
% 127.97/128.09 fof(theorem_8,conjecture,
% 127.97/128.09 ! [X,T0,T1,T2] :
% 127.97/128.09 ( ( organization(X)
% 127.97/128.09 & robust_position(X)
% 127.97/128.09 & ~ has_endowment(X)
% 127.97/128.09 & age(X,T0) = zero
% 127.97/128.09 & greater(sigma,zero)
% 127.97/128.09 & greater(tau,zero)
% 127.97/128.09 & sigma = tau
% 127.97/128.09 & smaller_or_equal(age(X,T1),sigma)
% 127.97/128.09 & greater(age(X,T2),sigma) )
% 127.97/128.09 => ( smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))
% 127.97/128.09 & hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ).
% 127.97/128.09
% 127.97/128.09 %--------------------------------------------------------------------------
% 127.97/128.09 %-------------------------------------------
% 127.97/128.09 % Proof found
% 127.97/128.09 % SZS status Theorem for theBenchmark
% 127.97/128.09 % SZS output start Proof
% 127.97/128.09 %ClaNum:74(EqnAxiom:31)
% 127.97/128.09 %VarNum:183(SingletonVarNum:68)
% 127.97/128.09 %MaxLitNum:4
% 127.97/128.09 %MaxfuncDepth:2
% 127.97/128.09 %SharedTerms:30
% 127.97/128.09 %goalClause: 32 33 34 35 36 37 39 40 41 71
% 127.97/128.09 %singleGoalClaCount:9
% 127.97/128.09 [32]E(a1,a2)
% 127.97/128.09 [33]P1(a3)
% 127.97/128.09 [34]P9(a3)
% 127.97/128.09 [36]P2(a2,a15)
% 127.97/128.09 [37]P2(a1,a15)
% 127.97/128.09 [38]P2(a8,a9)
% 127.97/128.09 [41]~P5(a3)
% 127.97/128.09 [35]E(f4(a3,a7),a15)
% 127.97/128.09 [39]P11(f4(a3,a10),a2)
% 127.97/128.09 [40]P2(f4(a3,a11),a2)
% 127.97/128.09 [71]~P12(f12(a3,a11),f12(a3,a10))+~E(f12(a3,a10),f12(a3,a7))
% 127.97/128.09 [42]~E(x421,x422)+P11(x421,x422)
% 127.97/128.09 [43]~E(x431,x432)+P6(x431,x432)
% 127.97/128.09 [47]~P12(x471,x472)+P11(x471,x472)
% 127.97/128.09 [48]~P2(x482,x481)+P12(x481,x482)
% 127.97/128.09 [49]~P2(x491,x492)+P6(x491,x492)
% 127.97/128.09 [50]~P12(x502,x501)+P2(x501,x502)
% 127.97/128.09 [55]~P2(x552,x551)+~P2(x551,x552)
% 127.97/128.09 [65]P1(x651)+~P4(x651,x652,x653)
% 127.97/128.09 [56]P9(x561)+P10(x561,f5(x561))+~P10(x561,f6(x561))
% 127.97/128.09 [61]P9(x611)+P10(x611,f5(x611))+P2(f4(x611,f6(x611)),a1)
% 127.97/128.09 [64]P9(x641)+~P10(x641,f6(x641))+P11(f4(x641,f5(x641)),a1)
% 127.97/128.09 [69]P9(x691)+P11(f4(x691,f5(x691)),a1)+P2(f4(x691,f6(x691)),a1)
% 127.97/128.09 [44]P12(x441,x442)+P2(x441,x442)+E(x441,x442)
% 127.97/128.09 [45]~P1(x451)+P5(x451)+~P7(x451,x452)
% 127.97/128.09 [46]P3(x461,x462)+~P1(x461)+P7(x461,x462)
% 127.97/128.09 [51]P12(x511,x512)+~P11(x511,x512)+E(x511,x512)
% 127.97/128.09 [52]P2(x521,x522)+~P6(x521,x522)+E(x521,x522)
% 127.97/128.09 [53]~P1(x531)+~P7(x531,x532)+E(f12(x531,x532),a16)
% 127.97/128.09 [54]~P1(x541)+P8(x541,x542)+~E(f4(x541,x542),a15)
% 127.97/128.09 [62]~P9(x621)+P10(x621,x622)+~P2(f4(x621,x622),a1)
% 127.97/128.09 [66]~P9(x661)+~P10(x661,x662)+~P11(f4(x661,x662),a1)
% 127.97/128.09 [57]~P2(x571,x573)+P2(x571,x572)+~P2(x573,x572)
% 127.97/128.09 [70]~P4(x701,x703,x702)+P8(x701,x702)+P8(x701,x703)
% 127.97/128.09 [72]~P4(x721,x723,x722)+~P8(x721,x722)+~P8(x721,x723)
% 127.97/128.09 [58]P8(x581,x582)+P10(x581,x582)+~P3(x581,x582)+E(f12(x581,x582),a13)
% 127.97/128.09 [59]P8(x591,x592)+~P10(x591,x592)+~P3(x591,x592)+E(f12(x591,x592),a9)
% 127.97/128.09 [60]P10(x601,x602)+~P8(x601,x602)+~P3(x601,x602)+E(f12(x601,x602),a8)
% 127.97/128.09 [63]~P8(x631,x632)+~P10(x631,x632)+~P3(x631,x632)+E(f12(x631,x632),a14)
% 127.97/128.09 [67]~P1(x671)+~P8(x671,x673)+P8(x671,x672)+P4(x671,x672,x673)
% 127.97/128.09 [68]~P1(x681)+~P8(x681,x683)+P8(x681,x682)+P4(x681,x683,x682)
% 127.97/128.09 [73]~P1(x731)+P4(x731,x732,x733)+~E(f4(x731,x732),a15)+~P2(f4(x731,x733),a2)
% 127.97/128.09 [74]~P1(x741)+~P4(x741,x743,x742)+P2(f4(x741,x742),a2)+~E(f4(x741,x743),a15)
% 127.97/128.09 %EqnAxiom
% 127.97/128.09 [1]E(x11,x11)
% 127.97/128.09 [2]E(x22,x21)+~E(x21,x22)
% 127.97/128.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 127.97/128.09 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 127.97/128.09 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 127.97/128.09 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63))
% 127.97/128.09 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72))
% 127.97/128.09 [8]~E(x81,x82)+E(f6(x81),f6(x82))
% 127.97/128.09 [9]~E(x91,x92)+E(f5(x91),f5(x92))
% 127.97/128.09 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 127.97/128.09 [11]~P9(x111)+P9(x112)+~E(x111,x112)
% 127.97/128.09 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 127.97/128.09 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 127.97/128.09 [14]P11(x142,x143)+~E(x141,x142)+~P11(x141,x143)
% 127.97/128.09 [15]P11(x153,x152)+~E(x151,x152)+~P11(x153,x151)
% 127.97/128.09 [16]P8(x162,x163)+~E(x161,x162)+~P8(x161,x163)
% 127.97/128.09 [17]P8(x173,x172)+~E(x171,x172)+~P8(x173,x171)
% 127.97/128.09 [18]P10(x182,x183)+~E(x181,x182)+~P10(x181,x183)
% 127.97/128.09 [19]P10(x193,x192)+~E(x191,x192)+~P10(x193,x191)
% 127.97/128.09 [20]P4(x202,x203,x204)+~E(x201,x202)+~P4(x201,x203,x204)
% 127.97/128.09 [21]P4(x213,x212,x214)+~E(x211,x212)+~P4(x213,x211,x214)
% 127.97/128.09 [22]P4(x223,x224,x222)+~E(x221,x222)+~P4(x223,x224,x221)
% 127.97/128.09 [23]~P5(x231)+P5(x232)+~E(x231,x232)
% 127.97/128.09 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243)
% 127.97/128.09 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251)
% 127.97/128.09 [26]P6(x262,x263)+~E(x261,x262)+~P6(x261,x263)
% 127.97/128.09 [27]P6(x273,x272)+~E(x271,x272)+~P6(x273,x271)
% 127.97/128.09 [28]P12(x282,x283)+~E(x281,x282)+~P12(x281,x283)
% 127.97/128.09 [29]P12(x293,x292)+~E(x291,x292)+~P12(x293,x291)
% 127.97/128.09 [30]P3(x302,x303)+~E(x301,x302)+~P3(x301,x303)
% 127.97/128.09 [31]P3(x313,x312)+~E(x311,x312)+~P3(x313,x311)
% 127.97/128.09
% 127.97/128.09 %-------------------------------------------
% 127.97/128.09 cnf(75,plain,
% 127.97/128.09 (P11(x751,x751)),
% 127.97/128.09 inference(equality_inference,[],[42])).
% 127.97/128.09 cnf(76,plain,
% 127.97/128.09 (P6(x761,x761)),
% 127.97/128.09 inference(equality_inference,[],[43])).
% 127.97/128.09 cnf(77,plain,
% 127.97/128.09 (E(a2,a1)),
% 127.97/128.09 inference(scs_inference,[],[32,2])).
% 127.97/128.09 cnf(78,plain,
% 127.97/128.09 (~P2(a15,a2)),
% 127.97/128.09 inference(scs_inference,[],[32,36,2,55])).
% 127.97/128.09 cnf(80,plain,
% 127.97/128.09 (~E(f4(a3,a11),a15)),
% 127.97/128.09 inference(scs_inference,[],[32,36,40,2,55,12])).
% 127.97/128.09 cnf(81,plain,
% 127.97/128.09 (P2(f4(a3,a11),a1)),
% 127.97/128.09 inference(scs_inference,[],[32,36,40,2,55,12,13])).
% 127.97/128.09 cnf(87,plain,
% 127.97/128.09 (P3(a3,x871)),
% 127.97/128.09 inference(scs_inference,[],[32,33,36,41,39,40,75,2,55,12,13,14,15,45,46])).
% 127.97/128.09 cnf(89,plain,
% 127.97/128.09 (P8(a3,a7)),
% 127.97/128.09 inference(scs_inference,[],[32,33,36,41,35,39,40,75,2,55,12,13,14,15,45,46,54])).
% 127.97/128.09 cnf(91,plain,
% 127.97/128.09 (P2(f4(a3,a11),a15)),
% 127.97/128.09 inference(scs_inference,[],[32,33,36,41,35,39,40,75,2,55,12,13,14,15,45,46,54,57])).
% 127.97/128.09 cnf(93,plain,
% 127.97/128.09 (P10(a3,a11)),
% 127.97/128.09 inference(scs_inference,[],[32,33,34,36,41,35,39,40,75,2,55,12,13,14,15,45,46,54,57,62])).
% 127.97/128.09 cnf(95,plain,
% 127.97/128.09 (~P10(a3,a10)),
% 127.97/128.09 inference(scs_inference,[],[32,33,34,36,41,35,39,40,75,2,55,12,13,14,15,45,46,54,57,62,66])).
% 127.97/128.09 cnf(99,plain,
% 127.97/128.09 (~E(a11,a10)),
% 127.97/128.09 inference(scs_inference,[],[32,33,34,36,41,35,39,40,75,2,55,12,13,14,15,45,46,54,57,62,66,72,19])).
% 127.97/128.09 cnf(101,plain,
% 127.97/128.09 (P6(x1011,x1011)),
% 127.97/128.09 inference(rename_variables,[],[76])).
% 127.97/128.09 cnf(104,plain,
% 127.97/128.09 (P4(a3,a7,a11)),
% 127.97/128.09 inference(scs_inference,[],[32,33,34,36,41,35,39,40,75,76,101,2,55,12,13,14,15,45,46,54,57,62,66,72,19,26,27,73])).
% 127.97/128.09 cnf(108,plain,
% 127.97/128.09 (~E(f4(a3,a11),f4(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[32,33,34,36,41,35,39,40,75,76,101,2,55,12,13,14,15,45,46,54,57,62,66,72,19,26,27,73,50,3])).
% 127.97/128.09 cnf(118,plain,
% 127.97/128.09 (E(a15,f4(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[37,35,55,50,2])).
% 127.97/128.09 cnf(119,plain,
% 127.97/128.09 (~P2(a15,f4(a3,a11))),
% 127.97/128.09 inference(scs_inference,[],[37,35,40,78,55,50,2,57])).
% 127.97/128.09 cnf(123,plain,
% 127.97/128.09 (P2(a1,f4(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[32,37,35,40,75,78,55,50,2,57,15,13])).
% 127.97/128.09 cnf(125,plain,
% 127.97/128.09 (P2(a2,f4(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[32,37,35,40,75,78,93,55,50,2,57,15,13,18,12])).
% 127.97/128.09 cnf(136,plain,
% 127.97/128.09 (~P2(a2,f4(a3,a11))),
% 127.97/128.09 inference(scs_inference,[],[40,55])).
% 127.97/128.09 cnf(138,plain,
% 127.97/128.09 (~P12(f4(a3,a11),a15)),
% 127.97/128.09 inference(scs_inference,[],[40,119,55,50])).
% 127.97/128.09 cnf(140,plain,
% 127.97/128.09 (P2(f4(a3,a11),f4(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[40,81,123,119,55,50,57])).
% 127.97/128.09 cnf(142,plain,
% 127.97/128.09 (~E(a15,f4(a3,a11))),
% 127.97/128.09 inference(scs_inference,[],[36,40,81,123,119,55,50,57,13])).
% 127.97/128.09 cnf(170,plain,
% 127.97/128.09 (~P2(f4(a3,a7),a1)),
% 127.97/128.09 inference(scs_inference,[],[123,55])).
% 127.97/128.09 cnf(185,plain,
% 127.97/128.09 (~P2(f4(a3,a7),f4(a3,a11))),
% 127.97/128.09 inference(scs_inference,[],[81,125,170,50,55,57])).
% 127.97/128.09 cnf(195,plain,
% 127.97/128.09 (~P12(f4(a3,a11),f4(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[185,38,55,50])).
% 127.97/128.09 cnf(281,plain,
% 127.97/128.09 (P2(x2811,a9)+~E(a8,x2811)),
% 127.97/128.09 inference(scs_inference,[],[77,38,11,12])).
% 127.97/128.09 cnf(305,plain,
% 127.97/128.09 (P11(a15,a1)),
% 127.97/128.09 inference(scs_inference,[],[37,48,47])).
% 127.97/128.09 cnf(308,plain,
% 127.97/128.09 (~P10(a3,a7)),
% 127.97/128.09 inference(scs_inference,[],[32,34,118,305,15,14,66])).
% 127.97/128.09 cnf(549,plain,
% 127.97/128.09 (~P3(a3,a11)+P8(a3,a11)+E(f12(a3,a11),a9)),
% 127.97/128.09 inference(scs_inference,[],[87,81,34,59,62])).
% 127.97/128.09 cnf(552,plain,
% 127.97/128.09 (E(a9,f12(a3,a11))+P8(a3,a11)),
% 127.97/128.09 inference(scs_inference,[],[87,549,2])).
% 127.97/128.09 cnf(1143,plain,
% 127.97/128.09 (E(f4(a15,x11431),f4(f4(a3,a7),x11431))),
% 127.97/128.09 inference(scs_inference,[],[35,2,4])).
% 127.97/128.09 cnf(1144,plain,
% 127.97/128.09 (E(f4(f4(a3,a7),x11441),f4(a15,x11441))),
% 127.97/128.09 inference(scs_inference,[],[1143,2])).
% 127.97/128.09 cnf(1155,plain,
% 127.97/128.09 (E(f4(x11551,a15),f4(x11551,f4(a3,a7)))),
% 127.97/128.09 inference(scs_inference,[],[35,2,5])).
% 127.97/128.09 cnf(1156,plain,
% 127.97/128.09 (E(f4(x11561,f4(a3,a7)),f4(x11561,a15))),
% 127.97/128.09 inference(scs_inference,[],[1155,2])).
% 127.97/128.09 cnf(1157,plain,
% 127.97/128.09 (E(f4(f4(a3,a7),a15),f4(a15,f4(a3,a7)))),
% 127.97/128.09 inference(scs_inference,[],[1144,1155,2,3])).
% 127.97/128.09 cnf(1169,plain,
% 127.97/128.09 (E(f4(a15,a15),f4(f4(a3,a7),f4(a3,a7)))),
% 127.97/128.09 inference(scs_inference,[],[1143,1157,1155,2,3])).
% 127.97/128.09 cnf(1180,plain,
% 127.97/128.09 (E(f4(f4(a3,a7),f4(a3,a7)),f4(a15,a15))),
% 127.97/128.09 inference(scs_inference,[],[1169,2])).
% 127.97/128.09 cnf(1371,plain,
% 127.97/128.09 (E(f12(a15,x13711),f12(f4(a3,a7),x13711))),
% 127.97/128.09 inference(scs_inference,[],[35,2,6])).
% 127.97/128.09 cnf(1423,plain,
% 127.97/128.09 (E(f12(x14231,a15),f12(x14231,f4(a3,a7)))),
% 127.97/128.09 inference(scs_inference,[],[35,2,7])).
% 127.97/128.09 cnf(1597,plain,
% 127.97/128.09 (P6(x15971,x15971)),
% 127.97/128.09 inference(rename_variables,[],[76])).
% 127.97/128.09 cnf(1600,plain,
% 127.97/128.09 (P6(f12(x16001,f4(a3,a7)),f12(x16001,a15))),
% 127.97/128.09 inference(scs_inference,[],[1423,76,1597,75,27,15,26])).
% 127.97/128.09 cnf(1719,plain,
% 127.97/128.09 (E(f5(a15),f5(f4(a3,a7)))),
% 127.97/128.09 inference(scs_inference,[],[35,2,9])).
% 127.97/128.09 cnf(1772,plain,
% 127.97/128.09 (E(a8,f12(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[89,87,308,2,60])).
% 127.97/128.09 cnf(1773,plain,
% 127.97/128.09 (P2(f12(a3,a7),a9)),
% 127.97/128.09 inference(scs_inference,[],[1772,281])).
% 127.97/128.09 cnf(1774,plain,
% 127.97/128.09 (~P2(a9,f12(a3,a7))),
% 127.97/128.09 inference(scs_inference,[],[1772,281,55])).
% 127.97/128.09 cnf(1776,plain,
% 127.97/128.09 (~P12(f12(a3,a7),a9)),
% 127.97/128.09 inference(scs_inference,[],[1772,281,55,50])).
% 127.97/128.09 cnf(1778,plain,
% 127.97/128.09 (E(f12(a3,a7),a8)),
% 127.97/128.09 inference(scs_inference,[],[1772,281,55,50,2])).
% 127.97/128.09 cnf(2047,plain,
% 127.97/128.09 (~E(f4(a3,a11),a1)),
% 127.97/128.09 inference(scs_inference,[],[34,93,42,66])).
% 127.97/128.09 cnf(2052,plain,
% 127.97/128.10 (~E(f4(a3,a11),a2)),
% 127.97/128.10 inference(scs_inference,[],[2047,77,3])).
% 127.97/128.10 cnf(2116,plain,
% 127.97/128.10 (E(f4(f12(a3,a7),x21161),f4(a8,x21161))),
% 127.97/128.10 inference(scs_inference,[],[1778,8,9,4])).
% 127.97/128.10 cnf(2125,plain,
% 127.97/128.10 (E(f4(x21251,f12(a3,a7)),f4(x21251,a8))),
% 127.97/128.10 inference(scs_inference,[],[91,1773,1719,1778,8,9,4,6,7,43,49,48,5])).
% 127.97/128.10 cnf(2127,plain,
% 127.97/128.10 (~P8(a3,a11)),
% 127.97/128.10 inference(scs_inference,[],[99,91,1773,1719,1778,104,89,8,9,4,6,7,43,49,48,5,2,72])).
% 127.97/128.10 cnf(2129,plain,
% 127.97/128.10 (~P2(f4(a3,a10),a1)),
% 127.97/128.10 inference(scs_inference,[],[99,95,91,1773,1719,34,1778,104,89,8,9,4,6,7,43,49,48,5,2,72,62])).
% 127.97/128.10 cnf(2139,plain,
% 127.97/128.10 (P12(a9,a8)),
% 127.97/128.10 inference(scs_inference,[],[99,195,108,95,142,91,1773,119,1156,1719,34,1778,93,104,89,8,9,4,6,7,43,49,48,5,2,72,62,66,3,52,51,29])).
% 127.97/128.10 cnf(2141,plain,
% 127.97/128.10 (E(f12(a3,a11),a9)),
% 127.97/128.10 inference(scs_inference,[],[99,195,108,95,142,91,1773,119,1156,1719,34,1778,93,87,104,77,89,8,9,4,6,7,43,49,48,5,2,72,62,66,3,52,51,29,15,59])).
% 127.97/128.10 cnf(2148,plain,
% 127.97/128.10 (E(a9,f12(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[33,99,195,108,95,142,91,1773,119,1156,1719,34,1778,93,87,104,77,89,8,9,4,6,7,43,49,48,5,2,72,62,66,3,52,51,29,15,59,67,42,552])).
% 127.97/128.10 cnf(2150,plain,
% 127.97/128.10 (~P2(f4(a3,a10),a2)),
% 127.97/128.10 inference(scs_inference,[],[33,99,195,1180,108,95,142,91,1773,119,1156,1719,34,1778,93,87,104,77,89,8,9,4,6,7,43,49,48,5,2,72,62,66,3,52,51,29,15,59,67,42,552,24,13])).
% 127.97/128.10 cnf(2151,plain,
% 127.97/128.10 (~P2(f12(a3,a11),f12(a3,a7))),
% 127.97/128.10 inference(scs_inference,[],[33,99,195,1180,108,95,142,1774,91,1773,119,1156,1719,34,1778,93,87,104,77,89,8,9,4,6,7,43,49,48,5,2,72,62,66,3,52,51,29,15,59,67,42,552,24,13,12])).
% 127.97/128.10 cnf(2152,plain,
% 127.97/128.10 (P12(f12(a3,a11),f12(a3,a7))),
% 127.97/128.10 inference(scs_inference,[],[33,99,195,1180,108,95,142,1774,91,1773,119,1156,1719,34,1778,93,87,104,77,89,8,9,4,6,7,43,49,48,5,2,72,62,66,3,52,51,29,15,59,67,42,552,24,13,12,28])).
% 127.97/128.10 cnf(2178,plain,
% 127.97/128.10 (E(f12(f12(a3,a11),x21781),f12(a9,x21781))),
% 127.97/128.10 inference(scs_inference,[],[2141,1773,43,49,8,9,6])).
% 127.97/128.10 cnf(2182,plain,
% 127.97/128.10 (E(f12(x21821,f12(a3,a11)),f12(x21821,a9))),
% 127.97/128.10 inference(scs_inference,[],[2141,1773,43,49,8,9,6,42,4,7])).
% 127.97/128.10 cnf(2183,plain,
% 127.97/128.10 (E(f4(x21831,f12(a3,a11)),f4(x21831,a9))),
% 127.97/128.10 inference(scs_inference,[],[2141,1773,43,49,8,9,6,42,4,7,5])).
% 127.97/128.10 cnf(2184,plain,
% 127.97/128.10 (P2(f12(a3,a7),f12(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[2152,2141,1773,43,49,8,9,6,42,4,7,5,50])).
% 127.97/128.10 cnf(2194,plain,
% 127.97/128.10 (~P2(f12(a3,a11),a8)),
% 127.97/128.10 inference(scs_inference,[],[2052,2151,2152,2141,2116,2125,138,80,1773,136,1772,43,49,8,9,6,42,4,7,5,50,2,3,52,51,13])).
% 127.97/128.10 cnf(2196,plain,
% 127.97/128.10 (~E(f4(a3,a11),f4(a3,a10))),
% 127.97/128.10 inference(scs_inference,[],[2052,2151,2152,2150,2141,2116,2125,1776,138,80,1773,136,1772,40,43,49,8,9,6,42,4,7,5,50,2,3,52,51,13,29,12])).
% 127.97/128.10 cnf(2197,plain,
% 127.97/128.10 (P12(f12(a3,a11),a8)),
% 127.97/128.10 inference(scs_inference,[],[2139,2052,2151,2152,2150,2141,2148,2116,2125,1776,138,80,1773,136,1772,40,43,49,8,9,6,42,4,7,5,50,2,3,52,51,13,29,12,28])).
% 127.97/128.10 cnf(2215,plain,
% 127.97/128.10 (E(f12(a9,x22151),f12(f12(a3,a11),x22151))),
% 127.97/128.10 inference(scs_inference,[],[2184,2178,2148,43,49,42,9,8,6])).
% 127.97/128.10 cnf(2218,plain,
% 127.97/128.10 (E(f4(x22181,a9),f4(x22181,f12(a3,a11)))),
% 127.97/128.10 inference(scs_inference,[],[2184,2178,2148,43,49,42,9,8,6,4,7,5])).
% 127.97/128.10 cnf(2219,plain,
% 127.97/128.10 (P2(a8,f12(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[2184,2197,2178,2148,43,49,42,9,8,6,4,7,5,50])).
% 127.97/128.10 cnf(2221,plain,
% 127.97/128.10 (~E(f4(a3,a10),f4(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[2184,2196,2197,2178,2148,43,49,42,9,8,6,4,7,5,50,2])).
% 127.97/128.10 cnf(2222,plain,
% 127.97/128.10 (E(f12(f12(a3,a11),f12(a3,a11)),f12(a9,a9))),
% 127.97/128.10 inference(scs_inference,[],[2184,2196,2197,2178,2182,2148,43,49,42,9,8,6,4,7,5,50,2,3])).
% 127.97/128.10 cnf(2239,plain,
% 127.97/128.10 (E(f12(a8,x22391),f12(f12(a3,a7),x22391))),
% 127.97/128.10 inference(scs_inference,[],[2219,2222,1772,49,42,43,9,6])).
% 127.97/128.10 cnf(2243,plain,
% 127.97/128.10 (E(f4(x22431,a8),f4(x22431,f12(a3,a7)))),
% 127.97/128.10 inference(scs_inference,[],[2219,2222,1772,49,42,43,9,6,8,4,7,5])).
% 127.97/128.10 cnf(2264,plain,
% 127.97/128.10 (E(f4(a2,x22641),f4(a1,x22641))),
% 127.97/128.10 inference(scs_inference,[],[2239,140,77,43,42,49,9,4])).
% 127.97/128.10 cnf(2266,plain,
% 127.97/128.10 (E(f12(a2,x22661),f12(a1,x22661))),
% 127.97/128.10 inference(scs_inference,[],[2239,140,77,43,42,49,9,4,8,6])).
% 127.97/128.10 cnf(2267,plain,
% 127.97/128.10 (E(f12(x22671,a2),f12(x22671,a1))),
% 127.97/128.10 inference(scs_inference,[],[2239,140,77,43,42,49,9,4,8,6,7])).
% 127.97/128.10 cnf(2268,plain,
% 127.97/128.10 (E(f4(x22681,a2),f4(x22681,a1))),
% 127.97/128.10 inference(scs_inference,[],[2239,140,77,43,42,49,9,4,8,6,7,5])).
% 127.97/128.10 cnf(2285,plain,
% 127.97/128.10 (E(f12(a1,x22851),f12(a2,x22851))),
% 127.97/128.10 inference(scs_inference,[],[2264,81,32,42,49,43,9,8,6])).
% 127.97/128.10 cnf(2286,plain,
% 127.97/128.10 (E(f4(a1,x22861),f4(a2,x22861))),
% 127.97/128.10 inference(scs_inference,[],[2264,81,32,42,49,43,9,8,6,4])).
% 127.97/128.10 cnf(2287,plain,
% 127.97/128.10 (E(f12(x22871,a1),f12(x22871,a2))),
% 127.97/128.10 inference(scs_inference,[],[2264,81,32,42,49,43,9,8,6,4,7])).
% 127.97/128.10 cnf(2288,plain,
% 127.97/128.10 (E(f4(x22881,a1),f4(x22881,a2))),
% 127.97/128.10 inference(scs_inference,[],[2264,81,32,42,49,43,9,8,6,4,7,5])).
% 127.97/128.10 cnf(2301,plain,
% 127.97/128.10 (E(f12(a1,a1),f12(a2,a2))),
% 127.97/128.10 inference(scs_inference,[],[2285,2287,38,49,43,42,3])).
% 127.97/128.10 cnf(2302,plain,
% 127.97/128.10 (E(f12(a1,x23021),f12(a2,x23021))),
% 127.97/128.10 inference(rename_variables,[],[2285])).
% 127.97/128.10 cnf(2305,plain,
% 127.97/128.10 (E(f12(a1,x23051),f12(a2,x23051))),
% 127.97/128.10 inference(rename_variables,[],[2285])).
% 127.97/128.10 cnf(2308,plain,
% 127.97/128.10 (~P2(f4(a3,a10),f4(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[2129,2285,2302,2305,2287,1600,81,38,49,43,42,3,27,19,57])).
% 127.97/128.10 cnf(2320,plain,
% 127.97/128.10 (E(f4(a1,a1),f4(a2,a2))),
% 127.97/128.10 inference(scs_inference,[],[2301,2286,2288,40,43,42,49,3])).
% 127.97/128.10 cnf(2346,plain,
% 127.97/128.10 (P12(f4(a3,a10),f4(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[2194,2320,2266,2267,2308,2221,76,42,43,3,26,52,44])).
% 127.97/128.10 cnf(2638,plain,
% 127.97/128.10 (P11(f4(x26381,f12(a3,a11)),f4(x26381,a9))),
% 127.97/128.10 inference(scs_inference,[],[2183,42])).
% 127.97/128.10 cnf(2640,plain,
% 127.97/128.10 (P6(f4(x26401,f12(a3,a11)),f4(x26401,a9))),
% 127.97/128.10 inference(scs_inference,[],[2183,42,43])).
% 127.97/128.10 cnf(2698,plain,
% 127.97/128.10 (P11(f12(x26981,f12(a3,a11)),f12(x26981,a9))),
% 127.97/128.10 inference(scs_inference,[],[2182,42])).
% 127.97/128.10 cnf(2700,plain,
% 127.97/128.10 (P6(f12(x27001,f12(a3,a11)),f12(x27001,a9))),
% 127.97/128.10 inference(scs_inference,[],[2182,42,43])).
% 127.97/128.10 cnf(2812,plain,
% 127.97/128.10 (P6(f4(x28121,a2),f4(x28121,a1))),
% 127.97/128.10 inference(scs_inference,[],[2268,43])).
% 127.97/128.10 cnf(3210,plain,
% 127.97/128.10 (~P8(a3,a10)+E(f12(a3,a10),a8)),
% 127.97/128.10 inference(scs_inference,[],[95,87,60])).
% 127.97/128.10 cnf(3678,plain,
% 127.97/128.10 (E(f4(a1,a15),f4(a2,f4(a3,a7)))),
% 127.97/128.10 inference(scs_inference,[],[2286,1155,3])).
% 127.97/128.10 cnf(3760,plain,
% 127.97/128.10 (E(f4(a15,a8),f4(f4(a3,a7),f12(a3,a7)))),
% 127.97/128.10 inference(scs_inference,[],[2243,1143,3])).
% 127.97/128.10 cnf(3975,plain,
% 127.97/128.10 (E(f4(f4(a3,a7),x39751),f4(a15,x39751))),
% 127.97/128.10 inference(rename_variables,[],[1144])).
% 127.97/128.10 cnf(3984,plain,
% 127.97/128.10 (E(f12(a15,x39841),f12(f4(a3,a7),x39841))),
% 127.97/128.10 inference(rename_variables,[],[1371])).
% 127.97/128.10 cnf(3993,plain,
% 127.97/128.10 (P8(a3,a10)),
% 127.97/128.10 inference(scs_inference,[],[35,33,89,1371,3984,1144,3975,1423,2127,3678,2215,2308,2150,2346,2640,2700,2638,2698,2,50,26,3,14,15,70,27,74,28,68])).
% 127.97/128.10 cnf(4005,plain,
% 127.97/128.10 (E(f12(a3,a10),a8)),
% 127.97/128.10 inference(scs_inference,[],[3993,3210])).
% 127.97/128.10 cnf(4124,plain,
% 127.97/128.10 (E(f4(f4(a3,a7),x41241),f4(a15,x41241))),
% 127.97/128.10 inference(rename_variables,[],[1144])).
% 127.97/128.10 cnf(4125,plain,
% 127.97/128.10 (E(f4(f4(a3,a7),a9),f4(a15,f12(a3,a11)))),
% 127.97/128.10 inference(scs_inference,[],[1144,4124,3760,2218,2812,2,26,3])).
% 127.97/128.10 cnf(4478,plain,
% 127.97/128.10 (E(f12(a3,a7),f12(a3,a10))),
% 127.97/128.10 inference(scs_inference,[],[1778,4005,2,281,55,50,3])).
% 127.97/128.10 cnf(4479,plain,
% 127.97/128.10 (P2(f12(a3,a10),f12(a3,a11))),
% 127.97/128.10 inference(scs_inference,[],[2148,1778,4005,2,281,55,50,3,13])).
% 127.97/128.10 cnf(4488,plain,
% 127.97/128.10 (E(f12(a3,a10),f12(a3,a7))),
% 127.97/128.10 inference(scs_inference,[],[4478,2])).
% 127.97/128.10 cnf(4498,plain,
% 127.97/128.10 (~P12(f12(a3,a11),f12(a3,a10))),
% 127.97/128.10 inference(scs_inference,[],[4488,71])).
% 127.97/128.10 cnf(4508,plain,
% 127.97/128.10 ($false),
% 127.97/128.10 inference(scs_inference,[],[4479,4125,4498,2,48]),
% 127.97/128.10 ['proof']).
% 127.97/128.10 % SZS output end Proof
% 127.97/128.10 % Total time :127.568245s
%------------------------------------------------------------------------------