%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT051-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 : n029.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:21 AM UTC 2026
% Result : Unsatisfiable 58.91s 59.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT051-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.07/0.33 % Computer : n029.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 7 13:22:12 UTC 2026
% 0.07/0.33 % CPUTime :
% 0.25/0.50 start to proof:theBenchmark
% 58.78/59.03 %-------------------------------------------
% 58.78/59.03 % File :CSE---1.7
% 58.78/59.03 % Problem :theBenchmark
% 58.78/59.03 % Transform :cnf
% 58.78/59.03 % Format :tptp:raw
% 58.78/59.03 % Command :java -jar mcs_scs.jar %d %s
% 58.78/59.03
% 58.78/59.03 % Result :Theorem 58.536760s
% 58.78/59.03 % Output :CNFRefutation 58.536760s
% 58.78/59.03 %-------------------------------------------
% 58.91/59.03 %--------------------------------------------------------------------------
% 58.91/59.03 % File : MGT051-1 : TPTP v9.3.0. Released v2.4.0.
% 58.91/59.03 % Domain : Management (Organisation Theory)
% 58.91/59.03 % Problem : Conditions for constant then increasing hazard of mortality
% 58.91/59.03 % Version : [Han98] axioms.
% 58.91/59.03 % English : An endowed organization's hazard of mortality remains constant
% 58.91/59.03 % during the period of immunity and increases monotonically with
% 58.91/59.03 % age once immunity ends.
% 58.91/59.03
% 58.91/59.03 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 58.91/59.03 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 58.91/59.03 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 58.91/59.03 % Source : [TPTP]
% 58.91/59.03 % Names :
% 58.91/59.03
% 58.91/59.03 % Status : Unsatisfiable
% 58.91/59.03 % Rating : 0.17 v9.3.0, 0.05 v9.0.0, 0.10 v8.1.0, 0.16 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.27 v6.4.0, 0.20 v6.3.0, 0.27 v6.2.0, 0.30 v6.1.0, 0.36 v6.0.0, 0.40 v5.4.0, 0.45 v5.3.0, 0.44 v5.2.0, 0.38 v5.1.0, 0.35 v5.0.0, 0.36 v4.1.0, 0.23 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.29 v3.2.0, 0.38 v3.1.0, 0.27 v2.7.0, 0.33 v2.6.0, 0.56 v2.5.0, 0.67 v2.4.0
% 58.91/59.03 % Syntax : Number of clauses : 38 ( 6 unt; 11 nHn; 34 RR)
% 58.91/59.03 % Number of literals : 110 ( 17 equ; 58 neg)
% 58.91/59.03 % Maximal clause size : 6 ( 2 avg)
% 58.91/59.03 % Maximal term depth : 3 ( 1 avg)
% 58.91/59.03 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 58.91/59.03 % Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% 58.91/59.03 % Number of variables : 71 ( 4 sgn)
% 58.91/59.03 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.91/59.03
% 58.91/59.03 % Comments : See MGT042+1.p for the mnemonic names.
% 58.91/59.03 % : Created with tptp2X -f tptp -t clausify:otter MGT051+1.p
% 58.91/59.03 %--------------------------------------------------------------------------
% 58.91/59.03 include('Axioms/MGT001-0.ax').
% 58.91/59.03 %--------------------------------------------------------------------------
% 58.91/59.03 cnf(definition_1_41,axiom,
% 58.91/59.03 ( ~ has_endowment(A)
% 58.91/59.03 | organization(A) ) ).
% 58.91/59.03
% 58.91/59.03 cnf(definition_1_42,axiom,
% 58.91/59.03 ( ~ has_endowment(A)
% 58.91/59.03 | ~ smaller_or_equal(age(A,B),eta)
% 58.91/59.03 | has_immunity(A,B) ) ).
% 58.91/59.03
% 58.91/59.03 cnf(definition_1_43,axiom,
% 58.91/59.03 ( ~ has_endowment(A)
% 58.91/59.03 | ~ greater(age(A,B),eta)
% 58.91/59.03 | ~ has_immunity(A,B) ) ).
% 58.91/59.03
% 58.91/59.03 cnf(definition_1_44,axiom,
% 58.91/59.03 ( ~ organization(A)
% 58.91/59.03 | smaller_or_equal(age(A,sk1(A)),eta)
% 58.91/59.03 | greater(age(A,sk1(A)),eta)
% 58.91/59.03 | has_endowment(A) ) ).
% 58.91/59.03
% 58.91/59.03 cnf(definition_1_45,axiom,
% 58.91/59.03 ( ~ organization(A)
% 58.91/59.03 | smaller_or_equal(age(A,sk1(A)),eta)
% 58.91/59.03 | has_immunity(A,sk1(A))
% 58.91/59.03 | has_endowment(A) ) ).
% 58.91/59.03
% 58.91/59.03 cnf(definition_1_46,axiom,
% 58.91/59.03 ( ~ organization(A)
% 58.91/59.03 | ~ has_immunity(A,sk1(A))
% 58.91/59.03 | greater(age(A,sk1(A)),eta)
% 58.91/59.03 | has_endowment(A) ) ).
% 58.91/59.03
% 58.91/59.03 cnf(definition_1_47,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ has_immunity(A,sk1(A))
% 58.91/59.04 | has_immunity(A,sk1(A))
% 58.91/59.04 | has_endowment(A) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_2_48,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ has_immunity(A,B)
% 58.91/59.04 | ~ has_immunity(A,C)
% 58.91/59.04 | hazard_of_mortality(A,B) = hazard_of_mortality(A,C) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_3_49,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ has_immunity(A,B)
% 58.91/59.04 | has_immunity(A,C)
% 58.91/59.04 | greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_4_50,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | has_immunity(A,B)
% 58.91/59.04 | has_immunity(A,C)
% 58.91/59.04 | ~ greater(capability(A,C),capability(A,B))
% 58.91/59.04 | ~ greater_or_equal(position(A,C),position(A,B))
% 58.91/59.04 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_4_51,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | has_immunity(A,B)
% 58.91/59.04 | has_immunity(A,C)
% 58.91/59.04 | ~ greater_or_equal(capability(A,C),capability(A,B))
% 58.91/59.04 | ~ greater(position(A,C),position(A,B))
% 58.91/59.04 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_4_52,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | has_immunity(A,B)
% 58.91/59.04 | has_immunity(A,C)
% 58.91/59.04 | capability(A,C) != capability(A,B)
% 58.91/59.04 | position(A,C) != position(A,B)
% 58.91/59.04 | hazard_of_mortality(A,C) = hazard_of_mortality(A,B) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_5_53,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 58.91/59.04 | ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))
% 58.91/59.04 | greater(capability(A,B),capability(A,C)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_5_54,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 58.91/59.04 | ~ greater(internal_friction(A,B),internal_friction(A,C))
% 58.91/59.04 | smaller(capability(A,B),capability(A,C)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_5_55,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | stock_of_knowledge(A,B) != stock_of_knowledge(A,C)
% 58.91/59.04 | internal_friction(A,B) != internal_friction(A,C)
% 58.91/59.04 | capability(A,B) = capability(A,C) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_6_56,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ greater(external_ties(A,B),external_ties(A,C))
% 58.91/59.04 | greater(position(A,B),position(A,C)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_6_57,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | external_ties(A,B) != external_ties(A,C)
% 58.91/59.04 | position(A,B) = position(A,C) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_10_58,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | stock_of_knowledge(A,B) = stock_of_knowledge(A,C) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_11_59,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | external_ties(A,B) = external_ties(A,C) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(assumption_12_60,axiom,
% 58.91/59.04 ( ~ organization(A)
% 58.91/59.04 | ~ greater(age(A,B),age(A,C))
% 58.91/59.04 | greater(internal_friction(A,B),internal_friction(A,C)) ) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_61,negated_conjecture,
% 58.91/59.04 organization(sk2) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_62,negated_conjecture,
% 58.91/59.04 has_endowment(sk2) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_63,negated_conjecture,
% 58.91/59.04 smaller_or_equal(age(sk2,sk3),age(sk2,sk4)) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_64,negated_conjecture,
% 58.91/59.04 smaller_or_equal(age(sk2,sk4),eta) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_65,negated_conjecture,
% 58.91/59.04 greater(age(sk2,sk5),eta) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_66,negated_conjecture,
% 58.91/59.04 greater(age(sk2,sk6),age(sk2,sk5)) ).
% 58.91/59.04
% 58.91/59.04 cnf(theorem_4_67,negated_conjecture,
% 58.91/59.04 ( ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))
% 58.91/59.04 | ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
% 58.91/59.04 | hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ).
% 58.91/59.04
% 58.91/59.04 %--------------------------------------------------------------------------
% 58.91/59.04 %-------------------------------------------
% 58.91/59.04 % Proof found
% 58.91/59.04 % SZS status Theorem for theBenchmark
% 58.91/59.04 % SZS output start Proof
% 58.91/59.04 %ClaNum:67(EqnAxiom:30)
% 58.91/59.04 %VarNum:227(SingletonVarNum:70)
% 58.91/59.04 %MaxLitNum:6
% 58.91/59.04 %MaxfuncDepth:2
% 58.91/59.04 %SharedTerms:23
% 58.91/59.04 %goalClause: 31 32 33 34 35 36 63
% 58.91/59.04 %singleGoalClaCount:6
% 58.91/59.04 [31]P1(a1)
% 58.91/59.04 [32]P4(a1)
% 58.91/59.04 [33]P6(f2(a1,a10),a3)
% 58.91/59.04 [34]P2(f2(a1,a12),a3)
% 58.91/59.04 [35]P6(f2(a1,a11),f2(a1,a10))
% 58.91/59.04 [36]P2(f2(a1,a13),f2(a1,a12))
% 58.91/59.04 [37]~P1(x371)+P4(x371)
% 58.91/59.04 [38]~E(x381,x382)+P6(x381,x382)
% 58.91/59.04 [39]~E(x391,x392)+P3(x391,x392)
% 58.91/59.04 [43]~P7(x431,x432)+P6(x431,x432)
% 58.91/59.04 [44]~P2(x442,x441)+P7(x441,x442)
% 58.91/59.04 [45]~P2(x451,x452)+P3(x451,x452)
% 58.91/59.04 [46]~P7(x462,x461)+P2(x461,x462)
% 58.91/59.04 [49]~P2(x492,x491)+~P2(x491,x492)
% 58.91/59.04 [41]~P4(x411)+E(f14(x411,x412),f14(x411,x413))
% 58.91/59.04 [42]~P4(x421)+E(f5(x421,x422),f5(x421,x423))
% 58.91/59.04 [63]~P2(f7(a1,a12),f7(a1,a10))+~P2(f7(a1,a13),f7(a1,a12))+~E(f7(a1,a11),f7(a1,a10))
% 58.91/59.04 [40]P7(x401,x402)+P2(x401,x402)+E(x401,x402)
% 58.91/59.04 [47]P7(x471,x472)+~P6(x471,x472)+E(x471,x472)
% 58.91/59.04 [48]P2(x481,x482)+~P3(x481,x482)+E(x481,x482)
% 58.91/59.04 [53]~P1(x531)+P5(x531,x532)+~P6(f2(x531,x532),a3)
% 58.91/59.04 [55]~P1(x551)+~P5(x551,x552)+~P2(f2(x551,x552),a3)
% 58.91/59.04 [50]~P2(x501,x503)+P2(x501,x502)+~P2(x503,x502)
% 58.91/59.04 [51]~P4(x511)+~E(f5(x511,x512),f5(x511,x513))+E(f6(x511,x512),f6(x511,x513))
% 58.91/59.04 [61]~P4(x611)+~P2(f5(x611,x612),f5(x611,x613))+P2(f6(x611,x612),f6(x611,x613))
% 58.91/59.04 [62]~P4(x621)+~P2(f2(x621,x622),f2(x621,x623))+P2(f8(x621,x622),f8(x621,x623))
% 58.91/59.04 [54]~P4(x541)+P1(x541)+P5(x541,f9(x541))+P6(f2(x541,f9(x541)),a3)
% 58.91/59.04 [56]~P4(x561)+P1(x561)+~P5(x561,f9(x561))+P2(f2(x561,f9(x561)),a3)
% 58.91/59.04 [58]~P4(x581)+P1(x581)+P6(f2(x581,f9(x581)),a3)+P2(f2(x581,f9(x581)),a3)
% 58.91/59.04 [52]~P4(x521)+~P5(x521,x523)+~P5(x521,x522)+E(f7(x521,x522),f7(x521,x523))
% 58.91/59.04 [57]~P4(x571)+~P5(x571,x573)+P5(x571,x572)+P2(f7(x571,x572),f7(x571,x573))
% 58.91/59.04 [59]~P4(x591)+~E(f14(x591,x592),f14(x591,x593))+~E(f8(x591,x592),f8(x591,x593))+E(f4(x591,x592),f4(x591,x593))
% 58.91/59.04 [64]~P4(x641)+~P6(f14(x641,x642),f14(x641,x643))+~P2(f8(x641,x642),f8(x641,x643))+P7(f4(x641,x642),f4(x641,x643))
% 58.91/59.04 [65]~P4(x651)+~P6(f8(x651,x652),f8(x651,x653))+~P2(f14(x651,x652),f14(x651,x653))+P2(f4(x651,x652),f4(x651,x653))
% 58.91/59.04 [60]P5(x601,x603)+P5(x601,x602)+~P4(x601)+~E(f4(x601,x602),f4(x601,x603))+~E(f6(x601,x602),f6(x601,x603))+E(f7(x601,x602),f7(x601,x603))
% 58.91/59.04 [66]~P4(x661)+P5(x661,x662)+P5(x661,x663)+P7(f7(x661,x662),f7(x661,x663))+~P3(f4(x661,x662),f4(x661,x663))+~P2(f6(x661,x662),f6(x661,x663))
% 58.91/59.04 [67]~P4(x671)+P5(x671,x672)+P5(x671,x673)+P7(f7(x671,x672),f7(x671,x673))+~P3(f6(x671,x672),f6(x671,x673))+~P2(f4(x671,x672),f4(x671,x673))
% 58.91/59.04 %EqnAxiom
% 58.91/59.04 [1]E(x11,x11)
% 58.91/59.04 [2]E(x22,x21)+~E(x21,x22)
% 58.91/59.04 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.91/59.04 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 58.91/59.04 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 58.91/59.04 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 58.91/59.04 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 58.91/59.04 [8]~E(x81,x82)+E(f14(x81,x83),f14(x82,x83))
% 58.91/59.04 [9]~E(x91,x92)+E(f14(x93,x91),f14(x93,x92))
% 58.91/59.04 [10]~E(x101,x102)+E(f6(x101,x103),f6(x102,x103))
% 58.91/59.04 [11]~E(x111,x112)+E(f6(x113,x111),f6(x113,x112))
% 58.91/59.04 [12]~E(x121,x122)+E(f7(x121,x123),f7(x122,x123))
% 58.91/59.04 [13]~E(x131,x132)+E(f7(x133,x131),f7(x133,x132))
% 58.91/59.04 [14]~E(x141,x142)+E(f8(x141,x143),f8(x142,x143))
% 58.91/59.04 [15]~E(x151,x152)+E(f8(x153,x151),f8(x153,x152))
% 58.91/59.04 [16]~E(x161,x162)+E(f9(x161),f9(x162))
% 58.91/59.04 [17]~E(x171,x172)+E(f5(x171,x173),f5(x172,x173))
% 58.91/59.04 [18]~E(x181,x182)+E(f5(x183,x181),f5(x183,x182))
% 58.91/59.04 [19]~P1(x191)+P1(x192)+~E(x191,x192)
% 58.91/59.04 [20]~P4(x201)+P4(x202)+~E(x201,x202)
% 58.91/59.04 [21]P6(x212,x213)+~E(x211,x212)+~P6(x211,x213)
% 58.91/59.04 [22]P6(x223,x222)+~E(x221,x222)+~P6(x223,x221)
% 58.91/59.04 [23]P2(x232,x233)+~E(x231,x232)+~P2(x231,x233)
% 58.91/59.04 [24]P2(x243,x242)+~E(x241,x242)+~P2(x243,x241)
% 58.91/59.04 [25]P7(x252,x253)+~E(x251,x252)+~P7(x251,x253)
% 58.91/59.04 [26]P7(x263,x262)+~E(x261,x262)+~P7(x263,x261)
% 58.91/59.04 [27]P5(x272,x273)+~E(x271,x272)+~P5(x271,x273)
% 58.91/59.04 [28]P5(x283,x282)+~E(x281,x282)+~P5(x283,x281)
% 58.91/59.04 [29]P3(x292,x293)+~E(x291,x292)+~P3(x291,x293)
% 58.91/59.04 [30]P3(x303,x302)+~E(x301,x302)+~P3(x303,x301)
% 58.91/59.04
% 58.91/59.04 %-------------------------------------------
% 58.91/59.04 cnf(68,plain,
% 58.91/59.04 (P6(x681,x681)),
% 58.91/59.04 inference(equality_inference,[],[38])).
% 58.91/59.04 cnf(69,plain,
% 58.91/59.04 (P3(x691,x691)),
% 58.91/59.04 inference(equality_inference,[],[39])).
% 58.91/59.04 cnf(73,plain,
% 58.91/59.04 (P5(a1,a10)),
% 58.91/59.04 inference(scs_inference,[],[31,36,33,49,53])).
% 58.91/59.04 cnf(75,plain,
% 58.91/59.04 (~P5(a1,a12)),
% 58.91/59.04 inference(scs_inference,[],[31,36,33,34,49,53,55])).
% 58.91/59.04 cnf(77,plain,
% 58.91/59.04 (P2(f2(a1,a13),a3)),
% 58.91/59.04 inference(scs_inference,[],[31,36,33,34,49,53,55,50])).
% 58.91/59.04 cnf(79,plain,
% 58.91/59.04 (~E(a3,f2(a1,a13))),
% 58.91/59.04 inference(scs_inference,[],[31,36,33,34,49,53,55,50,24])).
% 58.91/59.04 cnf(80,plain,
% 58.91/59.04 (~E(a10,a12)),
% 58.91/59.04 inference(scs_inference,[],[31,36,33,34,49,53,55,50,24,28])).
% 58.91/59.05 cnf(97,plain,
% 58.91/59.05 (~P2(a3,f2(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[34,49])).
% 58.91/59.05 cnf(99,plain,
% 58.91/59.05 (~P2(a3,f2(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[34,36,49,50])).
% 58.91/59.05 cnf(101,plain,
% 58.91/59.05 (~P5(a1,a13)),
% 58.91/59.05 inference(scs_inference,[],[31,34,36,77,49,50,55])).
% 58.91/59.05 cnf(103,plain,
% 58.91/59.05 (~E(f2(a1,a13),a3)),
% 58.91/59.05 inference(scs_inference,[],[31,34,36,77,49,50,55,23])).
% 58.91/59.05 cnf(121,plain,
% 58.91/59.05 (~P7(f2(a1,a13),a3)),
% 58.91/59.05 inference(scs_inference,[],[99,46])).
% 58.91/59.05 cnf(125,plain,
% 58.91/59.05 (~E(a10,a13)),
% 58.91/59.05 inference(scs_inference,[],[73,101,79,99,46,40,28])).
% 58.91/59.05 cnf(129,plain,
% 58.91/59.05 (E(f2(a1,a10),a3)+P7(f2(a1,a10),a3)),
% 58.91/59.05 inference(scs_inference,[],[33,73,101,79,99,46,40,28,25,26,27,47])).
% 58.91/59.05 cnf(140,plain,
% 58.91/59.05 (P3(f2(a1,a10),f2(a1,a11))+P7(f2(a1,a11),f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[35,69,47,29])).
% 58.91/59.05 cnf(144,plain,
% 58.91/59.05 (E(f2(a1,a10),f2(a1,a11))+P7(f2(a1,a11),f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[35,69,68,47,29,21,2])).
% 58.91/59.05 cnf(161,plain,
% 58.91/59.05 (P3(x1611,x1612)+~E(x1612,x1611)),
% 58.91/59.05 inference(scs_inference,[],[69,29])).
% 58.91/59.05 cnf(168,plain,
% 58.91/59.05 (P5(a1,a11)+~E(f2(a1,a10),a3)),
% 58.91/59.05 inference(scs_inference,[],[31,35,22,53])).
% 58.91/59.05 cnf(178,plain,
% 58.91/59.05 (P2(x1781,a3)+~E(f2(a1,a12),x1781)),
% 58.91/59.05 inference(scs_inference,[],[34,23])).
% 58.91/59.05 cnf(186,plain,
% 58.91/59.05 (P6(x1861,a3)+~E(f2(a1,a10),x1861)),
% 58.91/59.05 inference(scs_inference,[],[33,21])).
% 58.91/59.05 cnf(190,plain,
% 58.91/59.05 (P6(x1901,x1902)+~E(x1902,x1901)),
% 58.91/59.05 inference(scs_inference,[],[68,21])).
% 58.91/59.05 cnf(194,plain,
% 58.91/59.05 (E(f14(a1,x1941),f14(a1,x1942))),
% 58.91/59.05 inference(scs_inference,[],[31,37,41])).
% 58.91/59.05 cnf(196,plain,
% 58.91/59.05 (P6(f14(a1,x1961),f14(a1,x1962))),
% 58.91/59.05 inference(scs_inference,[],[194,161,190])).
% 58.91/59.05 cnf(224,plain,
% 58.91/59.05 (P7(f2(a1,a10),a3)+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[168,129])).
% 58.91/59.05 cnf(228,plain,
% 58.91/59.05 (P2(a3,f2(a1,a10))+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[224,46])).
% 58.91/59.05 cnf(230,plain,
% 58.91/59.05 (~P2(f2(a1,a10),a3)+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[228,49])).
% 58.91/59.05 cnf(231,plain,
% 58.91/59.05 (~E(f2(a1,a12),f2(a1,a10))+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[230,178])).
% 58.91/59.05 cnf(250,plain,
% 58.91/59.05 (~E(f2(a1,a10),f2(a1,a12))+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[231,2])).
% 58.91/59.05 cnf(253,plain,
% 58.91/59.05 (P2(f2(a1,a10),f2(a1,a12))+P7(f2(a1,a10),f2(a1,a12))+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[250,40])).
% 58.91/59.05 cnf(276,plain,
% 58.91/59.05 (P2(f2(a1,a10),f2(a1,a11))+P3(f2(a1,a10),f2(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[140,46])).
% 58.91/59.05 cnf(278,plain,
% 58.91/59.05 (P2(f2(a1,a10),f2(a1,a11))+E(f2(a1,a10),f2(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[144,46])).
% 58.91/59.05 cnf(287,plain,
% 58.91/59.05 (P3(f2(a1,a10),f2(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[276,45])).
% 58.91/59.05 cnf(293,plain,
% 58.91/59.05 (P3(f2(a1,a10),x2931)+~E(f2(a1,a11),x2931)),
% 58.91/59.05 inference(scs_inference,[],[287,30])).
% 58.91/59.05 cnf(297,plain,
% 58.91/59.05 (~P2(f2(a1,a11),f2(a1,a10))+E(f2(a1,a10),f2(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[278,49])).
% 58.91/59.05 cnf(301,plain,
% 58.91/59.05 (~P2(f2(a1,a11),f2(a1,a10))+P6(f2(a1,a11),a3)),
% 58.91/59.05 inference(scs_inference,[],[297,186])).
% 58.91/59.05 cnf(314,plain,
% 58.91/59.05 (P2(f6(a1,x3141),f6(a1,x3142))+~P2(f5(a1,x3141),f5(a1,x3142))),
% 58.91/59.05 inference(scs_inference,[],[31,61,37])).
% 58.91/59.05 cnf(315,plain,
% 58.91/59.05 (~P7(f5(a1,x3151),f5(a1,x3152))+P2(f6(a1,x3152),f6(a1,x3151))),
% 58.91/59.05 inference(scs_inference,[],[314,46])).
% 58.91/59.05 cnf(316,plain,
% 58.91/59.05 (~P7(f5(a1,x3161),f5(a1,x3161))),
% 58.91/59.05 inference(scs_inference,[],[315,49])).
% 58.91/59.05 cnf(317,plain,
% 58.91/59.05 (~P2(f5(a1,x3171),f5(a1,x3171))),
% 58.91/59.05 inference(scs_inference,[],[316,44])).
% 58.91/59.05 cnf(319,plain,
% 58.91/59.05 (P2(f2(a1,a10),a3)+P7(f2(a1,a10),f2(a1,a12))+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[34,253,50])).
% 58.91/59.05 cnf(324,plain,
% 58.91/59.05 (~P5(a1,a11)+~P2(f7(a1,a13),f7(a1,a12))+~P2(f7(a1,a12),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[32,73,63,52])).
% 58.91/59.05 cnf(325,plain,
% 58.91/59.05 (~E(a10,a11)+~P2(f7(a1,a13),f7(a1,a12))+~P2(f7(a1,a12),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[73,324,28])).
% 58.91/59.05 cnf(326,plain,
% 58.91/59.05 (~E(a11,a10)+~P2(f7(a1,a13),f7(a1,a12))+~P2(f7(a1,a12),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[325,2])).
% 58.91/59.05 cnf(327,plain,
% 58.91/59.05 (~P2(f7(a1,a13),f7(a1,a12))+~E(a11,a10)),
% 58.91/59.05 inference(scs_inference,[],[32,73,75,326,57])).
% 58.91/59.05 cnf(328,plain,
% 58.91/59.05 (~P7(f7(a1,a12),f7(a1,a13))+~E(a11,a10)),
% 58.91/59.05 inference(scs_inference,[],[327,46])).
% 58.91/59.05 cnf(334,plain,
% 58.91/59.05 (E(f5(a1,x3341),f5(a1,x3342))),
% 58.91/59.05 inference(scs_inference,[],[31,37,42])).
% 58.91/59.05 cnf(345,plain,
% 58.91/59.05 (E(f6(a1,x3451),f6(a1,x3452))),
% 58.91/59.05 inference(scs_inference,[],[31,334,37,51])).
% 58.91/59.05 cnf(346,plain,
% 58.91/59.05 (P3(f6(a1,x3461),f6(a1,x3462))),
% 58.91/59.05 inference(scs_inference,[],[345,161])).
% 58.91/59.05 cnf(357,plain,
% 58.91/59.05 (P2(f8(a1,a13),f8(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[31,36,37,62])).
% 58.91/59.05 cnf(358,plain,
% 58.91/59.05 (~P2(f8(a1,a12),f8(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[357,49])).
% 58.91/59.05 cnf(360,plain,
% 58.91/59.05 (P7(f4(a1,a13),f4(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[32,196,357,49,64])).
% 58.91/59.05 cnf(368,plain,
% 58.91/59.05 (P7(f8(a1,a12),f8(a1,a13))+~E(f8(a1,a13),f8(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[32,196,357,49,64,46,40,24,23])).
% 58.91/59.05 cnf(417,plain,
% 58.91/59.05 (P7(x4171,f8(a1,a13))+~E(f8(a1,a12),x4171)+~E(f8(a1,a13),f8(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[368,25])).
% 58.91/59.05 cnf(449,plain,
% 58.91/59.05 (~E(x4491,f8(a1,a12))+~E(f8(a1,a13),f8(a1,a12))+P7(x4491,f8(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[417,2])).
% 58.91/59.05 cnf(451,plain,
% 58.91/59.05 (~E(a13,a12)+P7(f8(a1,a13),f8(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[449,15])).
% 58.91/59.05 cnf(452,plain,
% 58.91/59.05 (~E(a12,a13)+P7(f8(a1,a13),f8(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[451,2])).
% 58.91/59.05 cnf(453,plain,
% 58.91/59.05 (P2(f8(a1,a13),f8(a1,a13))+~E(a12,a13)),
% 58.91/59.05 inference(scs_inference,[],[452,46])).
% 58.91/59.05 cnf(454,plain,
% 58.91/59.05 (~E(a12,a13)),
% 58.91/59.05 inference(scs_inference,[],[453,49])).
% 58.91/59.05 cnf(461,plain,
% 58.91/59.05 (P2(f7(a1,a13),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[31,73,101,37,57])).
% 58.91/59.05 cnf(4969,plain,
% 58.91/59.05 (E(f7(x49691,f14(a1,x49692)),f7(x49691,f14(a1,x49693)))),
% 58.91/59.05 inference(scs_inference,[],[194,2,13])).
% 58.91/59.05 cnf(5000,plain,
% 58.91/59.05 (P2(f4(a1,a12),f4(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[4969,461,334,360,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46])).
% 58.91/59.05 cnf(5004,plain,
% 58.91/59.05 (P7(f7(a1,a10),f7(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[4969,461,334,360,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44])).
% 58.91/59.05 cnf(5009,plain,
% 58.91/59.05 (~E(a13,a12)),
% 58.91/59.05 inference(scs_inference,[],[454,4969,461,334,360,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2])).
% 58.91/59.05 cnf(5010,plain,
% 58.91/59.05 (~P2(f2(a1,a10),a3)),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,461,334,360,73,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55])).
% 58.91/59.05 cnf(5015,plain,
% 58.91/59.05 (E(f5(a1,x50151),f5(a1,x50152))),
% 58.91/59.05 inference(rename_variables,[],[334])).
% 58.91/59.05 cnf(5018,plain,
% 58.91/59.05 (~P2(f2(a1,a10),f2(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,317,316,79,99,461,334,5015,77,360,73,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55,48,26,23,50])).
% 58.91/59.05 cnf(5020,plain,
% 58.91/59.05 (~P6(f2(a1,a12),a3)),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,317,316,79,99,461,334,5015,77,360,75,73,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55,48,26,23,50,53])).
% 58.91/59.05 cnf(5024,plain,
% 58.91/59.05 (P2(f7(a1,a12),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,317,121,316,79,99,461,103,334,5015,77,360,75,73,32,345,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55,48,26,23,50,53,47,57])).
% 58.91/59.05 cnf(5026,plain,
% 58.91/59.05 (P7(f7(a1,a12),f7(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,317,121,316,79,99,461,103,334,5015,77,346,360,75,73,32,345,101,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55,48,26,23,50,53,47,57,67])).
% 58.91/59.05 cnf(5029,plain,
% 58.91/59.05 (~E(a11,a10)),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,317,121,316,79,99,461,103,334,5015,77,346,360,75,73,32,345,101,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55,48,26,23,50,53,47,57,67,328])).
% 58.91/59.05 cnf(5030,plain,
% 58.91/59.05 (~E(a3,f2(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[31,454,4969,317,121,316,79,99,461,103,334,5015,77,346,360,75,73,32,345,101,38,39,43,45,16,4,6,7,8,9,10,11,12,14,17,18,46,49,44,15,5,13,2,55,48,26,23,50,53,47,57,67,328,190])).
% 58.91/59.05 cnf(5043,plain,
% 58.91/59.05 (~P2(f7(a1,a13),f7(a1,a12))+~E(f7(a1,a11),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[5024,63])).
% 58.91/59.05 cnf(5044,plain,
% 58.91/59.05 (P7(f2(a1,a10),f2(a1,a12))+P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[5010,319])).
% 58.91/59.05 cnf(5045,plain,
% 58.91/59.05 (~P2(f7(a1,a13),f7(a1,a12))+~P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[5024,324])).
% 58.91/59.05 cnf(5051,plain,
% 58.91/59.05 (P2(f7(a1,a13),f7(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[5000,5004,5026,43,45,46])).
% 58.91/59.05 cnf(5055,plain,
% 58.91/59.05 (P7(f7(a1,a10),f7(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[5000,5004,5024,5026,43,45,46,49,44])).
% 58.91/59.05 cnf(5062,plain,
% 58.91/59.05 (~E(f2(a1,a13),f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[5029,5000,5004,5030,5024,5026,5010,5020,97,68,77,43,45,46,49,44,2,48,22,23])).
% 58.91/59.05 cnf(5063,plain,
% 58.91/59.05 (~P5(a1,a11)),
% 58.91/59.05 inference(scs_inference,[],[5029,5000,5004,5030,5024,5026,5010,5020,97,68,77,43,45,46,49,44,2,48,22,23,5045])).
% 58.91/59.05 cnf(5066,plain,
% 58.91/59.05 (P7(f2(a1,a10),f2(a1,a12))),
% 58.91/59.05 inference(scs_inference,[],[5009,5029,5000,5004,5030,5024,5026,5010,5020,97,68,77,43,45,46,49,44,2,48,22,23,5045,5043,3,5044])).
% 58.91/59.05 cnf(5071,plain,
% 58.91/59.05 (P2(a3,f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[5063,228])).
% 58.91/59.05 cnf(5080,plain,
% 58.91/59.05 (P2(f2(a1,a12),f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[5055,5051,5066,45,43,46])).
% 58.91/59.05 cnf(5084,plain,
% 58.91/59.05 (P7(f8(a1,a12),f8(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[5055,5051,5066,357,45,43,46,49,44])).
% 58.91/59.05 cnf(5091,plain,
% 58.91/59.05 (~P6(f2(a1,a11),a3)),
% 58.91/59.05 inference(scs_inference,[],[31,5063,5062,5055,5018,5051,5066,357,32,45,43,46,49,44,2,62,48,53])).
% 58.91/59.05 cnf(5095,plain,
% 58.91/59.05 (P2(f7(a1,a11),f7(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[31,5063,5062,5055,5018,5051,5066,357,73,32,45,43,46,49,44,2,62,48,53,50,57])).
% 58.91/59.05 cnf(5097,plain,
% 58.91/59.05 (~E(f2(a1,a11),f2(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[31,5063,5062,5055,5018,5051,5066,357,73,32,45,43,46,49,44,2,62,48,53,50,57,293])).
% 58.91/59.05 cnf(5101,plain,
% 58.91/59.05 (~E(f2(a1,a11),a3)),
% 58.91/59.05 inference(scs_inference,[],[31,5063,5062,5055,5018,5051,5066,358,68,334,357,73,32,45,43,46,49,44,2,62,48,53,50,57,293,190,27,24,22])).
% 58.91/59.05 cnf(5103,plain,
% 58.91/59.05 (P7(f2(a1,a10),f2(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[31,5063,5062,5055,5018,5051,5066,358,68,334,357,73,32,45,43,46,49,44,2,62,48,53,50,57,293,190,27,24,22,40])).
% 58.91/59.05 cnf(5112,plain,
% 58.91/59.05 (~P2(f2(a1,a11),f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[5091,301])).
% 58.91/59.05 cnf(5120,plain,
% 58.91/59.05 (P2(f2(a1,a13),f2(a1,a10))),
% 58.91/59.05 inference(scs_inference,[],[5084,5103,5080,43,45,46])).
% 58.91/59.05 cnf(5201,plain,
% 58.91/59.05 (~P2(f2(a1,a11),f2(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[5112,80,5103,5120,5095,45,43,2,50])).
% 58.91/59.05 cnf(5216,plain,
% 58.91/59.05 (P7(f2(a1,a11),f2(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[5201,125,5026,5097,5024,43,45,2,40])).
% 58.91/59.05 cnf(5220,plain,
% 58.91/59.05 (P2(f2(a1,a13),f2(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[5201,125,5026,5097,5024,43,45,2,40,48,46])).
% 58.91/59.05 cnf(5241,plain,
% 58.91/59.05 (P2(f8(a1,a13),f8(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[5216,5220,32,45,43,62])).
% 58.91/59.05 cnf(5283,plain,
% 58.91/59.05 (P2(f4(a1,a11),f4(a1,a13))),
% 58.91/59.05 inference(scs_inference,[],[5241,196,36,32,45,64,46])).
% 58.91/59.05 cnf(5305,plain,
% 58.91/59.05 (P2(f7(a1,a13),f7(a1,a11))),
% 58.91/59.05 inference(scs_inference,[],[5283,5063,346,32,101,45,67,46])).
% 58.91/59.05 cnf(5317,plain,
% 58.91/59.05 (~P2(f2(a1,a11),a3)),
% 58.91/59.05 inference(scs_inference,[],[5305,5112,5071,45,50])).
% 58.91/59.05 cnf(5332,plain,
% 58.91/59.05 ($false),
% 58.91/59.05 inference(scs_inference,[],[5317,5091,5101,357,45,40,46,43]),
% 58.91/59.05 ['proof']).
% 58.91/59.05 % SZS output end Proof
% 58.91/59.05 % Total time :58.536760s
%------------------------------------------------------------------------------