%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT047-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 : n012.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:20 AM UTC 2026
% Result : Unsatisfiable 62.49s 62.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT047-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.01 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Mon Sep 7 13:12:41 UTC 2026
% 0.04/0.29 % CPUTime :
% 0.07/0.38 start to proof:theBenchmark
% 62.49/62.74 %-------------------------------------------
% 62.49/62.74 % File :CSE---1.7
% 62.49/62.74 % Problem :theBenchmark
% 62.49/62.74 % Transform :cnf
% 62.49/62.74 % Format :tptp:raw
% 62.49/62.74 % Command :java -jar mcs_scs.jar %d %s
% 62.49/62.74
% 62.49/62.74 % Result :Theorem 62.361465s
% 62.49/62.74 % Output :CNFRefutation 62.361465s
% 62.49/62.74 %-------------------------------------------
% 62.49/62.74 %--------------------------------------------------------------------------
% 62.49/62.74 % File : MGT047-1 : TPTP v9.3.0. Released v2.4.0.
% 62.49/62.74 % Domain : Management (Organisation Theory)
% 62.49/62.74 % Problem : Conditions for changing hazard of mortality
% 62.49/62.74 % Version : [Han98] axioms.
% 62.49/62.74 % English : An endowed organization's hazard of mortality is constant during
% 62.49/62.74 % its period of immunity, jumps when its immunity ends, and
% 62.49/62.74 % decreases with further aging but remains above the level during
% 62.49/62.74 % the immunity period.
% 62.49/62.74
% 62.49/62.74 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 62.49/62.74 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 62.49/62.74 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 62.49/62.74 % Source : [TPTP]
% 62.49/62.74 % Names :
% 62.49/62.74
% 62.49/62.74 % Status : Unsatisfiable
% 62.49/62.74 % Rating : 0.17 v9.3.0, 0.05 v9.0.0, 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.35 v5.4.0, 0.40 v5.3.0, 0.39 v5.2.0, 0.31 v5.1.0, 0.29 v5.0.0, 0.21 v4.1.0, 0.15 v4.0.1, 0.27 v4.0.0, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0, 0.31 v3.1.0, 0.27 v2.7.0, 0.33 v2.5.0, 0.56 v2.4.0
% 62.49/62.74 % Syntax : Number of clauses : 38 ( 6 unt; 11 nHn; 35 RR)
% 62.49/62.74 % Number of literals : 111 ( 16 equ; 59 neg)
% 62.49/62.74 % Maximal clause size : 6 ( 2 avg)
% 62.49/62.74 % Maximal term depth : 3 ( 1 avg)
% 62.49/62.74 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 62.49/62.74 % Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% 62.49/62.74 % Number of variables : 71 ( 2 sgn)
% 62.49/62.74 % SPC : CNF_UNS_RFO_SEQ_NHN
% 62.49/62.74
% 62.49/62.74 % Comments : See MGT042+1.p for the mnemonic names.
% 62.49/62.74 % : Created with tptp2X -f tptp -t clausify:otter MGT047+1.p
% 62.49/62.74 %--------------------------------------------------------------------------
% 62.49/62.74 include('Axioms/MGT001-0.ax').
% 62.49/62.74 %--------------------------------------------------------------------------
% 62.49/62.74 cnf(definition_1_41,axiom,
% 62.49/62.74 ( ~ has_endowment(A)
% 62.49/62.74 | organization(A) ) ).
% 62.49/62.74
% 62.49/62.74 cnf(definition_1_42,axiom,
% 62.49/62.74 ( ~ has_endowment(A)
% 62.49/62.74 | ~ smaller_or_equal(age(A,B),eta)
% 62.49/62.74 | has_immunity(A,B) ) ).
% 62.49/62.74
% 62.49/62.74 cnf(definition_1_43,axiom,
% 62.49/62.74 ( ~ has_endowment(A)
% 62.49/62.74 | ~ greater(age(A,B),eta)
% 62.49/62.74 | ~ has_immunity(A,B) ) ).
% 62.49/62.74
% 62.49/62.74 cnf(definition_1_44,axiom,
% 62.49/62.74 ( ~ organization(A)
% 62.49/62.74 | smaller_or_equal(age(A,sk1(A)),eta)
% 62.49/62.74 | greater(age(A,sk1(A)),eta)
% 62.49/62.75 | has_endowment(A) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(definition_1_45,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | smaller_or_equal(age(A,sk1(A)),eta)
% 62.49/62.75 | has_immunity(A,sk1(A))
% 62.49/62.75 | has_endowment(A) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(definition_1_46,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ has_immunity(A,sk1(A))
% 62.49/62.75 | greater(age(A,sk1(A)),eta)
% 62.49/62.75 | has_endowment(A) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(definition_1_47,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ has_immunity(A,sk1(A))
% 62.49/62.75 | has_immunity(A,sk1(A))
% 62.49/62.75 | has_endowment(A) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_2_48,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ has_immunity(A,B)
% 62.49/62.75 | ~ has_immunity(A,C)
% 62.49/62.75 | hazard_of_mortality(A,B) = hazard_of_mortality(A,C) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_3_49,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ has_immunity(A,B)
% 62.49/62.75 | has_immunity(A,C)
% 62.49/62.75 | greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_4_50,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | has_immunity(A,B)
% 62.49/62.75 | has_immunity(A,C)
% 62.49/62.75 | ~ greater(capability(A,C),capability(A,B))
% 62.49/62.75 | ~ greater_or_equal(position(A,C),position(A,B))
% 62.49/62.75 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_4_51,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | has_immunity(A,B)
% 62.49/62.75 | has_immunity(A,C)
% 62.49/62.75 | ~ greater_or_equal(capability(A,C),capability(A,B))
% 62.49/62.75 | ~ greater(position(A,C),position(A,B))
% 62.49/62.75 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_4_52,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | has_immunity(A,B)
% 62.49/62.75 | has_immunity(A,C)
% 62.49/62.75 | capability(A,C) != capability(A,B)
% 62.49/62.75 | position(A,C) != position(A,B)
% 62.49/62.75 | hazard_of_mortality(A,C) = hazard_of_mortality(A,B) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_5_53,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 62.49/62.75 | ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))
% 62.49/62.75 | greater(capability(A,B),capability(A,C)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_5_54,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 62.49/62.75 | ~ greater(internal_friction(A,B),internal_friction(A,C))
% 62.49/62.75 | smaller(capability(A,B),capability(A,C)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_5_55,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | stock_of_knowledge(A,B) != stock_of_knowledge(A,C)
% 62.49/62.75 | internal_friction(A,B) != internal_friction(A,C)
% 62.49/62.75 | capability(A,B) = capability(A,C) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_6_56,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ greater(external_ties(A,B),external_ties(A,C))
% 62.49/62.75 | greater(position(A,B),position(A,C)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_6_57,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | external_ties(A,B) != external_ties(A,C)
% 62.49/62.75 | position(A,B) = position(A,C) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_7_58,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ greater(age(A,B),age(A,C))
% 62.49/62.75 | greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_8_59,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | ~ greater(age(A,B),age(A,C))
% 62.49/62.75 | greater(external_ties(A,B),external_ties(A,C)) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(assumption_9_60,axiom,
% 62.49/62.75 ( ~ organization(A)
% 62.49/62.75 | internal_friction(A,B) = internal_friction(A,C) ) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_61,negated_conjecture,
% 62.49/62.75 organization(sk2) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_62,negated_conjecture,
% 62.49/62.75 has_endowment(sk2) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_63,negated_conjecture,
% 62.49/62.75 smaller_or_equal(age(sk2,sk3),age(sk2,sk4)) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_64,negated_conjecture,
% 62.49/62.75 smaller_or_equal(age(sk2,sk4),eta) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_65,negated_conjecture,
% 62.49/62.75 greater(age(sk2,sk5),eta) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_66,negated_conjecture,
% 62.49/62.75 greater(age(sk2,sk6),age(sk2,sk5)) ).
% 62.49/62.75
% 62.49/62.75 cnf(theorem_2_67,negated_conjecture,
% 62.49/62.75 ( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))
% 62.49/62.75 | ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))
% 62.49/62.75 | hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ).
% 62.49/62.75
% 62.49/62.75 %--------------------------------------------------------------------------
% 62.49/62.75 %-------------------------------------------
% 62.49/62.75 % Proof found
% 62.49/62.75 % SZS status Theorem for theBenchmark
% 62.49/62.75 % SZS output start Proof
% 62.49/62.75 %ClaNum:67(EqnAxiom:30)
% 62.49/62.75 %VarNum:231(SingletonVarNum:70)
% 62.49/62.75 %MaxLitNum:6
% 62.49/62.75 %MaxfuncDepth:2
% 62.49/62.75 %SharedTerms:23
% 62.49/62.75 %goalClause: 31 32 33 34 35 36 63
% 62.49/62.75 %singleGoalClaCount:6
% 62.49/62.75 [31]P1(a1)
% 62.49/62.75 [32]P4(a1)
% 62.49/62.75 [33]P6(f2(a1,a10),a3)
% 62.49/62.75 [34]P2(f2(a1,a12),a3)
% 62.49/62.75 [35]P6(f2(a1,a11),f2(a1,a10))
% 62.49/62.75 [36]P2(f2(a1,a13),f2(a1,a12))
% 62.49/62.75 [37]~P1(x371)+P4(x371)
% 62.49/62.75 [38]~E(x381,x382)+P6(x381,x382)
% 62.49/62.75 [39]~E(x391,x392)+P3(x391,x392)
% 62.49/62.75 [42]~P7(x421,x422)+P6(x421,x422)
% 62.49/62.75 [43]~P2(x432,x431)+P7(x431,x432)
% 62.49/62.75 [44]~P2(x441,x442)+P3(x441,x442)
% 62.49/62.75 [45]~P7(x452,x451)+P2(x451,x452)
% 62.49/62.75 [48]~P2(x482,x481)+~P2(x481,x482)
% 62.49/62.75 [41]~P4(x411)+E(f5(x411,x412),f5(x411,x413))
% 62.49/62.75 [63]~P2(f7(a1,a13),f7(a1,a10))+~E(f7(a1,a11),f7(a1,a10))+~P2(f7(a1,a12),f7(a1,a13))
% 62.49/62.75 [40]P7(x401,x402)+P2(x401,x402)+E(x401,x402)
% 62.49/62.75 [46]P7(x461,x462)+~P6(x461,x462)+E(x461,x462)
% 62.49/62.75 [47]P2(x471,x472)+~P3(x471,x472)+E(x471,x472)
% 62.49/62.75 [52]~P1(x521)+P5(x521,x522)+~P6(f2(x521,x522),a3)
% 62.49/62.75 [54]~P1(x541)+~P5(x541,x542)+~P2(f2(x541,x542),a3)
% 62.49/62.75 [49]~P2(x491,x493)+P2(x491,x492)+~P2(x493,x492)
% 62.49/62.75 [50]~P4(x501)+~E(f6(x501,x502),f6(x501,x503))+E(f8(x501,x502),f8(x501,x503))
% 62.49/62.75 [60]~P4(x601)+~P2(f6(x601,x602),f6(x601,x603))+P2(f8(x601,x602),f8(x601,x603))
% 62.49/62.75 [61]~P4(x611)+~P2(f2(x611,x612),f2(x611,x613))+P2(f14(x611,x612),f14(x611,x613))
% 62.49/62.75 [62]~P4(x621)+~P2(f2(x621,x622),f2(x621,x623))+P2(f6(x621,x622),f6(x621,x623))
% 62.49/62.75 [53]~P4(x531)+P1(x531)+P5(x531,f9(x531))+P6(f2(x531,f9(x531)),a3)
% 62.49/62.75 [55]~P4(x551)+P1(x551)+~P5(x551,f9(x551))+P2(f2(x551,f9(x551)),a3)
% 62.49/62.75 [57]~P4(x571)+P1(x571)+P6(f2(x571,f9(x571)),a3)+P2(f2(x571,f9(x571)),a3)
% 62.49/62.75 [51]~P4(x511)+~P5(x511,x513)+~P5(x511,x512)+E(f7(x511,x512),f7(x511,x513))
% 62.49/62.75 [56]~P4(x561)+~P5(x561,x563)+P5(x561,x562)+P2(f7(x561,x562),f7(x561,x563))
% 62.49/62.75 [58]~P4(x581)+~E(f14(x581,x582),f14(x581,x583))+~E(f5(x581,x582),f5(x581,x583))+E(f4(x581,x582),f4(x581,x583))
% 62.49/62.75 [64]~P4(x641)+~P6(f14(x641,x642),f14(x641,x643))+~P2(f5(x641,x642),f5(x641,x643))+P7(f4(x641,x642),f4(x641,x643))
% 62.49/62.75 [65]~P4(x651)+~P6(f5(x651,x652),f5(x651,x653))+~P2(f14(x651,x652),f14(x651,x653))+P2(f4(x651,x652),f4(x651,x653))
% 62.49/62.75 [59]P5(x591,x593)+P5(x591,x592)+~P4(x591)+~E(f4(x591,x592),f4(x591,x593))+~E(f8(x591,x592),f8(x591,x593))+E(f7(x591,x592),f7(x591,x593))
% 62.49/62.75 [66]~P4(x661)+P5(x661,x662)+P5(x661,x663)+P7(f7(x661,x662),f7(x661,x663))+~P3(f4(x661,x662),f4(x661,x663))+~P2(f8(x661,x662),f8(x661,x663))
% 62.49/62.75 [67]~P4(x671)+P5(x671,x672)+P5(x671,x673)+P7(f7(x671,x672),f7(x671,x673))+~P3(f8(x671,x672),f8(x671,x673))+~P2(f4(x671,x672),f4(x671,x673))
% 62.49/62.75 %EqnAxiom
% 62.49/62.75 [1]E(x11,x11)
% 62.49/62.75 [2]E(x22,x21)+~E(x21,x22)
% 62.49/62.75 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 62.49/62.75 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 62.49/62.75 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 62.49/62.75 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 62.49/62.75 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 62.49/62.75 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 62.49/62.75 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 62.49/62.75 [10]~E(x101,x102)+E(f8(x101,x103),f8(x102,x103))
% 62.49/62.75 [11]~E(x111,x112)+E(f8(x113,x111),f8(x113,x112))
% 62.49/62.75 [12]~E(x121,x122)+E(f6(x121,x123),f6(x122,x123))
% 62.49/62.75 [13]~E(x131,x132)+E(f6(x133,x131),f6(x133,x132))
% 62.49/62.75 [14]~E(x141,x142)+E(f7(x141,x143),f7(x142,x143))
% 62.49/62.75 [15]~E(x151,x152)+E(f7(x153,x151),f7(x153,x152))
% 62.49/62.75 [16]~E(x161,x162)+E(f14(x161,x163),f14(x162,x163))
% 62.49/62.75 [17]~E(x171,x172)+E(f14(x173,x171),f14(x173,x172))
% 62.49/62.75 [18]~E(x181,x182)+E(f9(x181),f9(x182))
% 62.49/62.75 [19]~P1(x191)+P1(x192)+~E(x191,x192)
% 62.49/62.75 [20]~P4(x201)+P4(x202)+~E(x201,x202)
% 62.49/62.75 [21]P6(x212,x213)+~E(x211,x212)+~P6(x211,x213)
% 62.49/62.75 [22]P6(x223,x222)+~E(x221,x222)+~P6(x223,x221)
% 62.49/62.75 [23]P2(x232,x233)+~E(x231,x232)+~P2(x231,x233)
% 62.49/62.75 [24]P2(x243,x242)+~E(x241,x242)+~P2(x243,x241)
% 62.49/62.75 [25]P5(x252,x253)+~E(x251,x252)+~P5(x251,x253)
% 62.49/62.75 [26]P5(x263,x262)+~E(x261,x262)+~P5(x263,x261)
% 62.49/62.75 [27]P7(x272,x273)+~E(x271,x272)+~P7(x271,x273)
% 62.49/62.75 [28]P7(x283,x282)+~E(x281,x282)+~P7(x283,x281)
% 62.49/62.75 [29]P3(x292,x293)+~E(x291,x292)+~P3(x291,x293)
% 62.49/62.75 [30]P3(x303,x302)+~E(x301,x302)+~P3(x303,x301)
% 62.49/62.75
% 62.49/62.75 %-------------------------------------------
% 62.49/62.75 cnf(68,plain,
% 62.49/62.75 (P6(x681,x681)),
% 62.49/62.75 inference(equality_inference,[],[38])).
% 62.49/62.75 cnf(69,plain,
% 62.49/62.75 (P3(x691,x691)),
% 62.49/62.75 inference(equality_inference,[],[39])).
% 62.49/62.75 cnf(73,plain,
% 62.49/62.75 (P5(a1,a10)),
% 62.49/62.75 inference(scs_inference,[],[31,36,33,48,52])).
% 62.49/62.75 cnf(75,plain,
% 62.49/62.75 (~P5(a1,a12)),
% 62.49/62.75 inference(scs_inference,[],[31,36,33,34,48,52,54])).
% 62.49/62.75 cnf(77,plain,
% 62.49/62.75 (P2(f2(a1,a13),a3)),
% 62.49/62.75 inference(scs_inference,[],[31,36,33,34,48,52,54,49])).
% 62.49/62.75 cnf(79,plain,
% 62.49/62.75 (~E(a3,f2(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[31,36,33,34,48,52,54,49,24])).
% 62.49/62.75 cnf(97,plain,
% 62.49/62.75 (~P2(a3,f2(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[34,48])).
% 62.49/62.75 cnf(99,plain,
% 62.49/62.75 (~P5(a1,a13)),
% 62.49/62.75 inference(scs_inference,[],[31,34,77,48,54])).
% 62.49/62.75 cnf(101,plain,
% 62.49/62.75 (~P2(a3,f2(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[31,34,36,77,48,54,49])).
% 62.49/62.75 cnf(105,plain,
% 62.49/62.75 (~E(f2(a1,a13),a3)),
% 62.49/62.75 inference(scs_inference,[],[31,34,36,77,79,48,54,49,40,23])).
% 62.49/62.75 cnf(110,plain,
% 62.49/62.75 (E(f2(a1,a11),f2(a1,a10))+P7(f2(a1,a11),f2(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[31,34,35,36,77,79,48,54,49,40,23,45,27,28,46])).
% 62.49/62.75 cnf(112,plain,
% 62.49/62.75 (P3(f2(a1,a11),f2(a1,a10))+P7(f2(a1,a11),f2(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[31,34,35,36,77,79,69,48,54,49,40,23,45,27,28,46,30])).
% 62.49/62.75 cnf(114,plain,
% 62.49/62.75 (E(x1141,f2(a1,a10))+P7(f2(a1,a11),f2(a1,a10))+~E(x1141,f2(a1,a11))),
% 62.49/62.75 inference(scs_inference,[],[31,34,35,33,36,73,77,79,69,48,54,49,40,23,45,46,30,3])).
% 62.49/62.75 cnf(118,plain,
% 62.49/62.75 (~P7(f2(a1,a13),a3)),
% 62.49/62.75 inference(scs_inference,[],[101,45])).
% 62.49/62.75 cnf(120,plain,
% 62.49/62.75 (E(f2(a1,a10),a3)+P7(f2(a1,a10),a3)),
% 62.49/62.75 inference(scs_inference,[],[33,101,45,46])).
% 62.49/62.75 cnf(168,plain,
% 62.49/62.75 (P3(x1681,x1682)+~E(x1682,x1681)),
% 62.49/62.75 inference(scs_inference,[],[69,29])).
% 62.49/62.75 cnf(176,plain,
% 62.49/62.75 (P6(x1761,a3)+~E(f2(a1,a10),x1761)),
% 62.49/62.75 inference(scs_inference,[],[33,73,25,22,21])).
% 62.49/62.75 cnf(183,plain,
% 62.49/62.75 (P5(a1,a11)+~E(f2(a1,a10),a3)),
% 62.49/62.75 inference(scs_inference,[],[31,35,22,52])).
% 62.49/62.75 cnf(190,plain,
% 62.49/62.75 (P6(x1901,f2(a1,a10))+~E(f2(a1,a11),x1901)),
% 62.49/62.75 inference(scs_inference,[],[35,21])).
% 62.49/62.75 cnf(195,plain,
% 62.49/62.75 (P6(x1951,x1952)+~E(x1952,x1951)),
% 62.49/62.75 inference(scs_inference,[],[68,21])).
% 62.49/62.75 cnf(200,plain,
% 62.49/62.75 (E(f5(a1,x2001),f5(a1,x2002))),
% 62.49/62.75 inference(scs_inference,[],[31,37,41])).
% 62.49/62.75 cnf(202,plain,
% 62.49/62.75 (P6(f5(a1,x2021),f5(a1,x2022))),
% 62.49/62.75 inference(scs_inference,[],[200,168,195])).
% 62.49/62.75 cnf(203,plain,
% 62.49/62.75 (~P1(f5(a1,x2031))+P1(f5(a1,x2032))),
% 62.49/62.75 inference(scs_inference,[],[200,168,195,19])).
% 62.49/62.75 cnf(204,plain,
% 62.49/62.75 (~P4(f5(a1,x2041))+P4(f5(a1,x2042))),
% 62.49/62.75 inference(scs_inference,[],[200,168,195,19,20])).
% 62.49/62.75 cnf(243,plain,
% 62.49/62.75 (P7(f2(a1,a10),a3)+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[183,120])).
% 62.49/62.75 cnf(245,plain,
% 62.49/62.75 (P4(f5(a1,x2451))+~P1(f5(a1,x2452))),
% 62.49/62.75 inference(scs_inference,[],[203,37])).
% 62.49/62.75 cnf(246,plain,
% 62.49/62.75 (~P4(f5(a1,x2461))+E(f5(f5(a1,x2462),x2463),f5(f5(a1,x2462),x2464))),
% 62.49/62.75 inference(scs_inference,[],[204,41])).
% 62.49/62.75 cnf(248,plain,
% 62.49/62.75 (P2(a3,f2(a1,a10))+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[243,45])).
% 62.49/62.75 cnf(250,plain,
% 62.49/62.75 (E(f5(f5(a1,x2501),x2502),f5(f5(a1,x2501),x2503))+~P1(f5(a1,x2504))),
% 62.49/62.75 inference(scs_inference,[],[245,246])).
% 62.49/62.75 cnf(252,plain,
% 62.49/62.75 (P3(a3,f2(a1,a10))+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[248,44])).
% 62.49/62.75 cnf(254,plain,
% 62.49/62.75 (P3(a3,x2541)+~E(f2(a1,a10),x2541)+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[252,30])).
% 62.49/62.75 cnf(325,plain,
% 62.49/62.75 (P7(f2(a1,a11),f2(a1,a10))+P6(f2(a1,a10),f2(a1,a11))),
% 62.49/62.75 inference(scs_inference,[],[110,195])).
% 62.49/62.75 cnf(326,plain,
% 62.49/62.75 (P2(f2(a1,a10),f2(a1,a11))+P3(f2(a1,a11),f2(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[112,45])).
% 62.49/62.75 cnf(329,plain,
% 62.49/62.75 (P2(f2(a1,a10),f2(a1,a11))+P6(f2(a1,a10),f2(a1,a11))),
% 62.49/62.75 inference(scs_inference,[],[325,45])).
% 62.49/62.75 cnf(335,plain,
% 62.49/62.75 (P6(f5(f5(a1,x3351),x3352),f5(f5(a1,x3351),x3353))+~P1(f5(a1,x3354))),
% 62.49/62.75 inference(scs_inference,[],[250,38])).
% 62.49/62.75 cnf(336,plain,
% 62.49/62.75 (P6(x3361,f5(f5(a1,x3362),x3363))+~E(f5(f5(a1,x3362),x3364),x3361)+~P1(f5(a1,x3365))),
% 62.49/62.75 inference(scs_inference,[],[335,21])).
% 62.49/62.75 cnf(348,plain,
% 62.49/62.75 (P2(f8(a1,x3481),f8(a1,x3482))+~P2(f6(a1,x3481),f6(a1,x3482))),
% 62.49/62.75 inference(scs_inference,[],[31,60,37])).
% 62.49/62.75 cnf(349,plain,
% 62.49/62.75 (P2(f8(a1,a13),f8(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[36,32,348,62])).
% 62.49/62.75 cnf(350,plain,
% 62.49/62.75 (~P2(f8(a1,a12),f8(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[349,48])).
% 62.49/62.75 cnf(352,plain,
% 62.49/62.75 (~P2(f6(a1,a12),f6(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[32,349,48,60])).
% 62.49/62.75 cnf(356,plain,
% 62.49/62.75 (~P2(x3561,f8(a1,a13))+P2(x3561,f8(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[32,349,48,60,45,49])).
% 62.49/62.75 cnf(361,plain,
% 62.49/62.75 (P7(f8(a1,a12),x3611)+~P2(x3611,f8(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[356,43])).
% 62.49/62.75 cnf(368,plain,
% 62.49/62.75 (P7(f8(a1,a12),f8(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[350,352,349,45,40,24,23,361])).
% 62.49/62.75 cnf(418,plain,
% 62.49/62.75 (P2(f14(a1,a13),f14(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[36,31,61,37])).
% 62.49/62.75 cnf(421,plain,
% 62.49/62.75 (P2(f4(a1,a13),f4(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[32,202,418,48,65])).
% 62.49/62.75 cnf(432,plain,
% 62.49/62.75 (~P2(f4(a1,a12),f4(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[421,48])).
% 62.49/62.75 cnf(434,plain,
% 62.49/62.75 (~P7(f4(a1,a13),f4(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[421,48,45])).
% 62.49/62.75 cnf(466,plain,
% 62.49/62.75 (P7(f4(a1,a12),f4(a1,a13))+~E(f4(a1,a13),f4(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[421,432,40,24,23])).
% 62.49/62.75 cnf(528,plain,
% 62.49/62.75 (P7(f4(a1,a12),x5281)+~E(f4(a1,a13),x5281)+~E(f4(a1,a13),f4(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[466,28])).
% 62.49/62.75 cnf(581,plain,
% 62.49/62.75 (P7(f4(a1,a12),f4(a1,a12))+~E(f14(a1,a13),f14(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[200,32,528,58])).
% 62.49/62.75 cnf(582,plain,
% 62.49/62.75 (~E(f4(a1,a12),f4(a1,a13))+~E(f14(a1,a13),f14(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[434,581,27])).
% 62.49/62.75 cnf(583,plain,
% 62.49/62.75 (~E(a12,a13)+~E(f14(a1,a13),f14(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[582,7])).
% 62.49/62.75 cnf(584,plain,
% 62.49/62.75 (~E(a13,a12)+~E(a12,a13)),
% 62.49/62.75 inference(scs_inference,[],[583,17])).
% 62.49/62.75 cnf(585,plain,
% 62.49/62.75 (~E(a12,a13)),
% 62.49/62.75 inference(scs_inference,[],[584,2])).
% 62.49/62.75 cnf(612,plain,
% 62.49/62.75 (~P5(a1,a11)+~P2(f7(a1,a12),f7(a1,a13))+~P2(f7(a1,a13),f7(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[32,73,63,51])).
% 62.49/62.75 cnf(2337,plain,
% 62.49/62.75 (E(f5(f5(a1,x23371),x23372),f5(f5(a1,x23373),x23372))),
% 62.49/62.75 inference(scs_inference,[],[200,2,8])).
% 62.49/62.75 cnf(5169,plain,
% 62.49/62.75 (~E(f2(a1,a10),f2(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[118,105,46,176])).
% 62.49/62.75 cnf(5364,plain,
% 62.49/62.75 (~E(x53641,f2(a1,a13))+~E(f2(a1,a10),x53641)),
% 62.49/62.75 inference(scs_inference,[],[5169,3])).
% 62.49/62.75 cnf(5457,plain,
% 62.49/62.75 (~E(a13,a10)),
% 62.49/62.75 inference(scs_inference,[],[5169,2,5])).
% 62.49/62.75 cnf(5469,plain,
% 62.49/62.75 (~E(x54691,a10)+~E(a13,x54691)),
% 62.49/62.75 inference(scs_inference,[],[585,5457,2,3])).
% 62.49/62.75 cnf(5615,plain,
% 62.49/62.75 (P3(f4(a1,a13),f4(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[421,368,42,44])).
% 62.49/62.75 cnf(5617,plain,
% 62.49/62.75 (P7(a3,f2(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[34,421,368,42,44,43])).
% 62.49/62.75 cnf(5882,plain,
% 62.49/62.75 (P7(f2(a1,a11),f2(a1,a10))+~E(a13,f2(a1,a11))+~E(f2(a1,a10),a10)),
% 62.49/62.75 inference(scs_inference,[],[5469,114])).
% 62.49/62.75 cnf(8337,plain,
% 62.49/62.75 (~E(x83371,a13)+~E(f2(a1,a10),f2(a1,x83371))),
% 62.49/62.75 inference(scs_inference,[],[5364,5])).
% 62.49/62.75 cnf(8400,plain,
% 62.49/62.75 (~P6(f2(a1,a12),a3)),
% 62.49/62.75 inference(scs_inference,[],[31,36,32,75,62,52])).
% 62.49/62.75 cnf(8404,plain,
% 62.49/62.75 (~E(a3,f2(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[31,79,101,68,36,32,75,62,52,47,21])).
% 62.49/62.75 cnf(8406,plain,
% 62.49/62.75 (~P2(f2(a1,a10),a3)),
% 62.49/62.75 inference(scs_inference,[],[31,79,101,68,36,73,32,75,62,52,47,21,54])).
% 62.49/62.75 cnf(8410,plain,
% 62.49/62.75 (P7(f7(a1,a13),f7(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[31,5615,79,101,68,349,99,36,73,32,75,62,52,47,21,54,56,66])).
% 62.49/62.75 cnf(8414,plain,
% 62.49/62.75 (~P2(f7(a1,a10),f7(a1,a13))),
% 62.49/62.75 inference(scs_inference,[],[31,5615,79,101,68,349,99,36,73,32,75,62,52,47,21,54,56,66,38,48])).
% 62.49/62.75 cnf(8416,plain,
% 62.49/62.75 (~P7(a3,f2(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[31,5615,79,101,68,349,99,36,73,32,75,62,52,47,21,54,56,66,38,48,45])).
% 62.49/62.75 cnf(8420,plain,
% 62.49/62.75 (~E(f2(a1,a12),f2(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[31,5617,5615,79,101,2337,68,349,99,36,73,32,75,62,52,47,21,54,56,66,38,48,45,336,28])).
% 62.49/62.75 cnf(8421,plain,
% 62.49/62.75 (~P2(f7(a1,a12),f7(a1,a13))+~P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[31,5617,5615,79,101,2337,68,349,99,36,73,32,75,62,52,47,21,54,56,66,38,48,45,336,28,612])).
% 62.49/62.75 cnf(8426,plain,
% 62.49/62.75 (~P3(a3,f2(a1,a12))),
% 62.49/62.75 inference(scs_inference,[],[8404,8414,97,45,47])).
% 62.49/62.75 cnf(8576,plain,
% 62.49/62.75 (~P6(a3,f2(a1,a10))+E(a3,f2(a1,a10))),
% 62.49/62.75 inference(scs_inference,[],[8416,46])).
% 62.49/62.75 cnf(8591,plain,
% 62.49/62.75 (~P3(f2(a1,a10),a3)+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[8426,8400,8406,47,22,29,183])).
% 62.49/62.75 cnf(8904,plain,
% 62.49/62.75 (~P2(a3,x89041)+P2(f2(a1,a13),x89041)),
% 62.49/62.75 inference(scs_inference,[],[77,49])).
% 62.49/62.75 cnf(9210,plain,
% 62.49/62.75 (~E(a3,f2(a1,a10))+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[8591,168])).
% 62.49/62.75 cnf(9212,plain,
% 62.49/62.75 (P7(x92121,f2(a1,a13))+~P2(a3,x92121)),
% 62.49/62.75 inference(scs_inference,[],[8904,43])).
% 62.49/62.75 cnf(9214,plain,
% 62.49/62.75 (~P6(a3,f2(a1,a10))+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[9210,8576])).
% 62.49/62.75 cnf(9218,plain,
% 62.49/62.75 (P6(x92181,f2(a1,a13))+~P2(a3,x92181)),
% 62.49/62.75 inference(scs_inference,[],[9212,42])).
% 62.49/62.75 cnf(9219,plain,
% 62.49/62.75 (~E(f2(a1,a11),a3)+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[9214,190])).
% 62.49/62.75 cnf(9224,plain,
% 62.49/62.75 (~E(a3,f2(a1,a11))+P5(a1,a11)),
% 62.49/62.75 inference(scs_inference,[],[9219,2])).
% 62.49/62.75 cnf(9232,plain,
% 62.49/62.76 (~E(f2(a1,x92321),f2(a1,a10))+~E(x92321,a13)),
% 62.49/62.76 inference(scs_inference,[],[8337,2])).
% 62.49/62.76 cnf(9237,plain,
% 62.49/62.76 (~P5(a1,a11)),
% 62.49/62.76 inference(scs_inference,[],[8410,8421,45])).
% 62.49/62.76 cnf(9240,plain,
% 62.49/62.76 (P2(a3,f2(a1,a10))),
% 62.49/62.76 inference(scs_inference,[],[9237,248])).
% 62.49/62.76 cnf(9242,plain,
% 62.49/62.76 (~E(f2(a1,a10),x92421)+P3(a3,x92421)),
% 62.49/62.76 inference(scs_inference,[],[9237,254])).
% 62.49/62.76 cnf(9243,plain,
% 62.49/62.76 (~P3(f2(a1,a10),a3)),
% 62.49/62.76 inference(scs_inference,[],[9237,8591])).
% 62.49/62.76 cnf(9245,plain,
% 62.49/62.76 (~P6(a3,f2(a1,a10))),
% 62.49/62.76 inference(scs_inference,[],[9237,9214])).
% 62.49/62.76 cnf(9246,plain,
% 62.49/62.76 (~E(f2(a1,a11),a3)),
% 62.49/62.76 inference(scs_inference,[],[9237,9219])).
% 62.49/62.76 cnf(9247,plain,
% 62.49/62.76 (~E(a3,f2(a1,a11))),
% 62.49/62.76 inference(scs_inference,[],[9237,9224])).
% 62.49/62.76 cnf(9254,plain,
% 62.49/62.76 (~P7(f2(a1,a11),a3)),
% 62.49/62.76 inference(scs_inference,[],[9237,31,73,32,52,56,48,42])).
% 62.49/62.76 cnf(9259,plain,
% 62.49/62.76 (~P2(a3,f2(a1,a11))),
% 62.49/62.76 inference(scs_inference,[],[9237,31,73,32,52,56,48,42,28,45,43])).
% 62.49/62.76 cnf(9295,plain,
% 62.49/62.76 (P2(f2(a1,a11),a3)),
% 62.49/62.76 inference(scs_inference,[],[9240,9246,9254,9259,9247,9218,47,49,40])).
% 62.49/62.76 cnf(9306,plain,
% 62.49/62.76 (E(f2(a1,a11),f2(a1,a10))),
% 62.49/62.76 inference(scs_inference,[],[9240,9246,9254,9259,9247,8420,35,9218,47,49,40,329,9242,326,45,5882,114,46])).
% 62.49/62.76 cnf(9309,plain,
% 62.49/62.76 (~P3(f2(a1,a11),a3)),
% 62.49/62.76 inference(scs_inference,[],[9240,9243,9245,9246,9254,9259,9247,8420,35,9218,47,49,40,329,9242,326,45,5882,114,46,22,29])).
% 62.49/62.76 cnf(9331,plain,
% 62.49/62.76 ($false),
% 62.49/62.76 inference(scs_inference,[],[9306,9295,9309,9232,44]),
% 62.49/62.76 ['proof']).
% 62.49/62.76 % SZS output end Proof
% 62.49/62.76 % Total time :62.361465s
%------------------------------------------------------------------------------