%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT042-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 : n026.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 17.12s 17.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT042-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.08/0.34 % Computer : n026.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:07:27 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.28/0.46 start to proof:theBenchmark
% 17.12/17.34 %-------------------------------------------
% 17.12/17.34 % File :CSE---1.7
% 17.12/17.34 % Problem :theBenchmark
% 17.12/17.34 % Transform :cnf
% 17.12/17.34 % Format :tptp:raw
% 17.12/17.34 % Command :java -jar mcs_scs.jar %d %s
% 17.12/17.34
% 17.12/17.34 % Result :Theorem 16.879676s
% 17.12/17.34 % Output :CNFRefutation 16.879676s
% 17.12/17.34 %-------------------------------------------
% 17.12/17.35 %--------------------------------------------------------------------------
% 17.12/17.35 % File : MGT042-1 : TPTP v9.3.0. Released v2.4.0.
% 17.12/17.35 % Domain : Management (Organisation Theory)
% 17.12/17.35 % Problem : Conditions for a lower hazard of mortality
% 17.12/17.35 % Version : [Han98] axioms.
% 17.12/17.35 % English : When an organization lacks immunity, increased collective
% 17.12/17.35 % knowledge and superior external ties lower its hazard of
% 17.12/17.35 % mortality when internal friction does not increase.
% 17.12/17.35
% 17.12/17.35 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 17.12/17.35 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 17.12/17.35 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 17.12/17.35 % Source : [TPTP]
% 17.12/17.35 % Names :
% 17.12/17.35
% 17.12/17.35 % Status : Unsatisfiable
% 17.12/17.35 % Rating : 0.08 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.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.18 v6.2.0, 0.20 v6.1.0, 0.29 v6.0.0, 0.40 v5.5.0, 0.55 v5.3.0, 0.56 v5.2.0, 0.50 v5.1.0, 0.59 v5.0.0, 0.50 v4.1.0, 0.31 v4.0.1, 0.36 v4.0.0, 0.27 v3.7.0, 0.20 v3.5.0, 0.18 v3.4.0, 0.17 v3.3.0, 0.36 v3.2.0, 0.46 v3.1.0, 0.55 v2.7.0, 0.50 v2.6.0, 0.56 v2.5.0, 0.67 v2.4.0
% 17.12/17.35 % Syntax : Number of clauses : 38 ( 3 unt; 15 nHn; 37 RR)
% 17.12/17.35 % Number of literals : 97 ( 13 equ; 44 neg)
% 17.12/17.35 % Maximal clause size : 6 ( 2 avg)
% 17.12/17.35 % Maximal term depth : 2 ( 1 avg)
% 17.12/17.35 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty)
% 17.12/17.35 % Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% 17.12/17.35 % Number of variables : 47 ( 0 sgn)
% 17.12/17.35 % SPC : CNF_UNS_RFO_SEQ_NHN
% 17.12/17.35
% 17.12/17.35 % Comments : The original text uses mnemonic names:
% 17.12/17.35 % Original: C/F/P: Arity: New name:
% 17.12/17.35 % zero-symbol c 0 zero
% 17.12/17.35 % eta-symbol c 0 eta
% 17.12/17.35 % sigma-symbol c 0 sigma
% 17.12/17.35 % tau-symbol c 0 tau
% 17.12/17.35 % very_low c 0 very_low
% 17.12/17.35 % low c 0 low
% 17.12/17.35 % mod1 c 0 mod1
% 17.12/17.35 % mod2 c 0 mod2
% 17.12/17.35 % high c 0 high
% 17.12/17.35 % A f 2 age
% 17.12/17.35 % H f 2 hazard_of_mortality
% 17.12/17.35 % C f 2 capability
% 17.12/17.35 % P f 2 position
% 17.12/17.35 % K f 2 stock_of_knowledge
% 17.12/17.35 % T f 2 external_ties
% 17.12/17.35 % F f 2 internal_friction
% 17.12/17.35 % O p 1 organization
% 17.12/17.35 % EN p 1 has_endowment
% 17.12/17.35 % IM p 2 has_immunity
% 17.12/17.35 % DS p 3 dissimilar
% 17.12/17.35 % AL p 2 is_aligned
% 17.12/17.35 % PA p 2 positional_advantage
% 17.12/17.35 % FG p 1 fragile_position
% 17.12/17.35 % RB p 1 robust_position
% 17.12/17.35 % : Created with tptp2X -f tptp -t clausify:otter MGT042+1.p
% 17.12/17.35 %--------------------------------------------------------------------------
% 17.12/17.35 include('Axioms/MGT001-0.ax').
% 17.12/17.35 %--------------------------------------------------------------------------
% 17.12/17.35 cnf(assumption_4_38,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | has_immunity(A,B)
% 17.12/17.35 | has_immunity(A,C)
% 17.12/17.35 | ~ greater(capability(A,C),capability(A,B))
% 17.12/17.35 | ~ greater_or_equal(position(A,C),position(A,B))
% 17.12/17.35 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_4_39,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | has_immunity(A,B)
% 17.12/17.35 | has_immunity(A,C)
% 17.12/17.35 | ~ greater_or_equal(capability(A,C),capability(A,B))
% 17.12/17.35 | ~ greater(position(A,C),position(A,B))
% 17.12/17.35 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_4_40,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | has_immunity(A,B)
% 17.12/17.35 | has_immunity(A,C)
% 17.12/17.35 | capability(A,C) != capability(A,B)
% 17.12/17.35 | position(A,C) != position(A,B)
% 17.12/17.35 | hazard_of_mortality(A,C) = hazard_of_mortality(A,B) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_5_41,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 17.12/17.35 | ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))
% 17.12/17.35 | greater(capability(A,B),capability(A,C)) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_5_42,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 17.12/17.35 | ~ greater(internal_friction(A,B),internal_friction(A,C))
% 17.12/17.35 | smaller(capability(A,B),capability(A,C)) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_5_43,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | stock_of_knowledge(A,B) != stock_of_knowledge(A,C)
% 17.12/17.35 | internal_friction(A,B) != internal_friction(A,C)
% 17.12/17.35 | capability(A,B) = capability(A,C) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_6_44,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | ~ greater(external_ties(A,B),external_ties(A,C))
% 17.12/17.35 | greater(position(A,B),position(A,C)) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(assumption_6_45,axiom,
% 17.12/17.35 ( ~ organization(A)
% 17.12/17.35 | external_ties(A,B) != external_ties(A,C)
% 17.12/17.35 | position(A,B) = position(A,C) ) ).
% 17.12/17.35
% 17.12/17.35 cnf(lemma_1_46,negated_conjecture,
% 17.12/17.35 organization(sk1) ).
% 17.12/17.35
% 17.12/17.35 cnf(lemma_1_47,negated_conjecture,
% 17.12/17.36 ~ has_immunity(sk1,sk2) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_48,negated_conjecture,
% 17.12/17.36 ~ has_immunity(sk1,sk3) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_49,negated_conjecture,
% 17.12/17.36 ( greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
% 17.12/17.36 | greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_50,negated_conjecture,
% 17.12/17.36 ( greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
% 17.12/17.36 | smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_51,negated_conjecture,
% 17.12/17.36 ( greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
% 17.12/17.36 | greater(external_ties(sk1,sk3),external_ties(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_52,negated_conjecture,
% 17.12/17.36 ( smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))
% 17.12/17.36 | greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_53,negated_conjecture,
% 17.12/17.36 ( greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))
% 17.12/17.36 | greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_54,negated_conjecture,
% 17.12/17.36 ( smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))
% 17.12/17.36 | smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_55,negated_conjecture,
% 17.12/17.36 ( smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))
% 17.12/17.36 | greater(external_ties(sk1,sk3),external_ties(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_56,negated_conjecture,
% 17.12/17.36 ( greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))
% 17.12/17.36 | smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_57,negated_conjecture,
% 17.12/17.36 ( greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))
% 17.12/17.36 | greater(external_ties(sk1,sk3),external_ties(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_58,negated_conjecture,
% 17.12/17.36 ( greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
% 17.12/17.36 | ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_59,negated_conjecture,
% 17.12/17.36 ( smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))
% 17.12/17.36 | ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_60,negated_conjecture,
% 17.12/17.36 ( greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))
% 17.12/17.36 | ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_61,negated_conjecture,
% 17.12/17.36 ( ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
% 17.12/17.36 | greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_62,negated_conjecture,
% 17.12/17.36 ( ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
% 17.12/17.36 | smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_63,negated_conjecture,
% 17.12/17.36 ( ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
% 17.12/17.36 | greater(external_ties(sk1,sk3),external_ties(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 cnf(lemma_1_64,negated_conjecture,
% 17.12/17.36 ( ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
% 17.12/17.36 | ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ) ).
% 17.12/17.36
% 17.12/17.36 %--------------------------------------------------------------------------
% 17.12/17.36 %-------------------------------------------
% 17.12/17.36 % Proof found
% 17.12/17.36 % SZS status Theorem for theBenchmark
% 17.12/17.36 % SZS output start Proof
% 17.12/17.36 %ClaNum:64(EqnAxiom:26)
% 17.12/17.36 %VarNum:160(SingletonVarNum:47)
% 17.12/17.36 %MaxLitNum:6
% 17.12/17.36 %MaxfuncDepth:1
% 17.12/17.36 %SharedTerms:20
% 17.12/17.36 %goalClause: 27 28 29 30 31 48 49 50 51
% 17.12/17.36 %singleGoalClaCount:5
% 17.12/17.36 [27]P1(a1)
% 17.12/17.36 [29]~P2(a1,a8)
% 17.12/17.36 [30]~P2(a1,a7)
% 17.12/17.36 [28]P5(f2(a1,a7),f2(a1,a8))
% 17.12/17.36 [31]~P6(f3(a1,a7),f3(a1,a8))
% 17.12/17.36 [48]P3(f9(a1,a7),f9(a1,a8))+P3(f4(a1,a7),f4(a1,a8))
% 17.12/17.36 [49]P4(f9(a1,a7),f9(a1,a8))+P3(f9(a1,a7),f9(a1,a8))
% 17.12/17.36 [50]P4(f4(a1,a7),f4(a1,a8))+P3(f4(a1,a7),f4(a1,a8))
% 17.12/17.36 [51]P4(f9(a1,a7),f9(a1,a8))+P4(f4(a1,a7),f4(a1,a8))
% 17.12/17.36 [32]~E(x321,x322)+P5(x321,x322)
% 17.12/17.36 [33]~E(x331,x332)+P3(x331,x332)
% 17.12/17.36 [35]~P6(x351,x352)+P5(x351,x352)
% 17.12/17.36 [36]~P4(x362,x361)+P6(x361,x362)
% 17.12/17.36 [37]~P4(x371,x372)+P3(x371,x372)
% 17.12/17.36 [38]~P6(x382,x381)+P4(x381,x382)
% 17.12/17.36 [41]~P4(x412,x411)+~P4(x411,x412)
% 17.12/17.36 [34]P6(x341,x342)+P4(x341,x342)+E(x341,x342)
% 17.12/17.36 [39]P6(x391,x392)+~P5(x391,x392)+E(x391,x392)
% 17.12/17.36 [40]P4(x401,x402)+~P3(x401,x402)+E(x401,x402)
% 17.12/17.36 [42]~P4(x421,x423)+P4(x421,x422)+~P4(x423,x422)
% 17.12/17.36 [43]~P1(x431)+~E(f4(x431,x432),f4(x431,x433))+E(f6(x431,x432),f6(x431,x433))
% 17.12/17.36 [60]~P1(x601)+~P4(f4(x601,x602),f4(x601,x603))+P4(f6(x601,x602),f6(x601,x603))
% 17.12/17.36 [52]~P1(x521)+~E(f9(x521,x522),f9(x521,x523))+~E(f2(x521,x522),f2(x521,x523))+E(f5(x521,x522),f5(x521,x523))
% 17.12/17.36 [61]~P1(x611)+~P5(f9(x611,x612),f9(x611,x613))+~P4(f2(x611,x612),f2(x611,x613))+P6(f5(x611,x612),f5(x611,x613))
% 17.12/17.36 [62]~P1(x621)+~P5(f2(x621,x622),f2(x621,x623))+~P4(f9(x621,x622),f9(x621,x623))+P4(f5(x621,x622),f5(x621,x623))
% 17.12/17.36 [59]P2(x591,x593)+P2(x591,x592)+~P1(x591)+~E(f5(x591,x592),f5(x591,x593))+~E(f6(x591,x592),f6(x591,x593))+E(f3(x591,x592),f3(x591,x593))
% 17.12/17.36 [63]~P1(x631)+P2(x631,x632)+P2(x631,x633)+P6(f3(x631,x632),f3(x631,x633))+~P3(f5(x631,x632),f5(x631,x633))+~P4(f6(x631,x632),f6(x631,x633))
% 17.12/17.36 [64]~P1(x641)+P2(x641,x642)+P2(x641,x643)+P6(f3(x641,x642),f3(x641,x643))+~P3(f6(x641,x642),f6(x641,x643))+~P4(f5(x641,x642),f5(x641,x643))
% 17.12/17.36 %EqnAxiom
% 17.12/17.36 [1]E(x11,x11)
% 17.12/17.36 [2]E(x22,x21)+~E(x21,x22)
% 17.12/17.36 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 17.12/17.36 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 17.12/17.36 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 17.12/17.36 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 17.12/17.36 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 17.12/17.36 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83))
% 17.12/17.36 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92))
% 17.12/17.36 [10]~E(x101,x102)+E(f6(x101,x103),f6(x102,x103))
% 17.12/17.36 [11]~E(x111,x112)+E(f6(x113,x111),f6(x113,x112))
% 17.12/17.36 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123))
% 17.12/17.36 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132))
% 17.12/17.36 [14]~E(x141,x142)+E(f4(x141,x143),f4(x142,x143))
% 17.12/17.36 [15]~E(x151,x152)+E(f4(x153,x151),f4(x153,x152))
% 17.12/17.36 [16]~P1(x161)+P1(x162)+~E(x161,x162)
% 17.12/17.36 [17]P5(x172,x173)+~E(x171,x172)+~P5(x171,x173)
% 17.12/17.36 [18]P5(x183,x182)+~E(x181,x182)+~P5(x183,x181)
% 17.12/17.36 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193)
% 17.12/17.36 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201)
% 17.12/17.36 [21]P6(x212,x213)+~E(x211,x212)+~P6(x211,x213)
% 17.12/17.36 [22]P6(x223,x222)+~E(x221,x222)+~P6(x223,x221)
% 17.12/17.36 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233)
% 17.12/17.36 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241)
% 17.12/17.36 [25]P3(x252,x253)+~E(x251,x252)+~P3(x251,x253)
% 17.12/17.36 [26]P3(x263,x262)+~E(x261,x262)+~P3(x263,x261)
% 17.12/17.36
% 17.12/17.36 %-------------------------------------------
% 17.12/17.36 cnf(65,plain,
% 17.12/17.36 (P5(x651,x651)),
% 17.12/17.36 inference(equality_inference,[],[32])).
% 17.12/17.36 cnf(66,plain,
% 17.12/17.36 (P3(x661,x661)),
% 17.12/17.36 inference(equality_inference,[],[33])).
% 17.12/17.36 cnf(83,plain,
% 17.12/17.36 (E(f2(a1,a7),f2(a1,a8))+P6(f2(a1,a7),f2(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[28,39])).
% 17.12/17.36 cnf(111,plain,
% 17.12/17.36 (P3(x1111,x1112)+~E(x1112,x1111)),
% 17.12/17.36 inference(scs_inference,[],[66,25])).
% 17.12/17.36 cnf(116,plain,
% 17.12/17.36 (~E(f5(a1,a8),f5(a1,a7))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[27,31,29,30,66,25,63,38,60])).
% 17.12/17.36 cnf(125,plain,
% 17.12/17.36 (~P4(f5(a1,a7),f5(a1,a8))+~P4(f6(a1,a7),f6(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[27,31,29,30,63,33,37])).
% 17.12/17.36 cnf(137,plain,
% 17.12/17.36 (~P4(f5(a1,a7),f5(a1,a8))+~E(f4(a1,a7),f4(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[27,31,29,30,64,33,43])).
% 17.12/17.36 cnf(143,plain,
% 17.12/17.36 (~P4(f4(a1,x1431),f4(a1,x1431))),
% 17.12/17.36 inference(scs_inference,[],[27,41,60])).
% 17.12/17.36 cnf(144,plain,
% 17.12/17.36 (~P6(f4(a1,x1441),f4(a1,x1441))),
% 17.12/17.36 inference(scs_inference,[],[143,38])).
% 17.12/17.36 cnf(169,plain,
% 17.12/17.36 (P3(f9(a1,a7),f9(a1,a8))+P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[51,37])).
% 17.12/17.36 cnf(188,plain,
% 17.12/17.36 (P4(f2(a1,a8),f2(a1,a7))+E(f2(a1,a7),f2(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[83,38])).
% 17.12/17.36 cnf(200,plain,
% 17.12/17.36 (~P4(f6(a1,a7),f6(a1,a8))+~P4(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[28,27,125,62])).
% 17.12/17.36 cnf(224,plain,
% 17.12/17.36 (P4(f2(a1,a8),f2(a1,a7))+E(f5(a1,a7),f5(a1,a8))+~E(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[27,188,52])).
% 17.12/17.36 cnf(235,plain,
% 17.12/17.36 (~P6(f6(a1,a8),f6(a1,a7))+~P4(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[200,38])).
% 17.12/17.36 cnf(248,plain,
% 17.12/17.36 (~P6(f6(a1,a8),f6(a1,a7))+P3(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[235,49])).
% 17.12/17.36 cnf(259,plain,
% 17.12/17.36 (~P4(f6(a1,a7),f6(a1,a8))+P3(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[248,36])).
% 17.12/17.36 cnf(260,plain,
% 17.12/17.36 (P3(f9(a1,a7),f9(a1,a8))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[27,259,60])).
% 17.12/17.36 cnf(261,plain,
% 17.12/17.36 (P3(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[260,169])).
% 17.12/17.36 cnf(266,plain,
% 17.12/17.36 (E(f9(a1,a7),f9(a1,a8))+~P3(f6(a1,a7),f6(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[28,31,29,30,27,261,40,62,64])).
% 17.12/17.36 cnf(268,plain,
% 17.12/17.36 (~P4(f6(a1,a7),f6(a1,a8))+E(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[28,31,29,30,27,261,40,62,64,200])).
% 17.12/17.36 cnf(292,plain,
% 17.12/17.36 (E(f9(a1,a7),f9(a1,a8))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[27,268,60])).
% 17.12/17.36 cnf(361,plain,
% 17.12/17.36 (E(f5(a1,x3611),f5(a1,x3612))+~E(f2(a1,x3612),f2(a1,x3611))+~E(f9(a1,x3612),f9(a1,x3611))),
% 17.12/17.36 inference(scs_inference,[],[27,2,52])).
% 17.12/17.36 cnf(367,plain,
% 17.12/17.36 (E(f6(a1,x3671),f6(a1,x3672))+~E(f4(a1,x3672),f4(a1,x3671))),
% 17.12/17.36 inference(scs_inference,[],[27,2,43])).
% 17.12/17.36 cnf(369,plain,
% 17.12/17.36 (~E(x3691,x3692)+E(f5(x3692,x3693),f5(x3691,x3693))),
% 17.12/17.36 inference(scs_inference,[],[2,6])).
% 17.12/17.36 cnf(408,plain,
% 17.12/17.36 (E(f9(a1,a8),f9(a1,a7))+P4(f9(a1,a7),f9(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[261,2,40])).
% 17.12/17.36 cnf(452,plain,
% 17.12/17.36 (E(f9(a1,a8),f9(a1,a7))+~P3(f6(a1,a7),f6(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[2,266])).
% 17.12/17.36 cnf(453,plain,
% 17.12/17.36 (~E(f6(a1,a7),f6(a1,a8))+E(f9(a1,a8),f9(a1,a7))),
% 17.12/17.36 inference(scs_inference,[],[452,33])).
% 17.12/17.36 cnf(454,plain,
% 17.12/17.36 (E(f9(a1,a8),f9(a1,a7))+~E(f4(a1,a8),f4(a1,a7))),
% 17.12/17.36 inference(scs_inference,[],[453,367])).
% 17.12/17.36 cnf(455,plain,
% 17.12/17.36 (~E(f4(a1,a7),f4(a1,a8))+E(f9(a1,a8),f9(a1,a7))),
% 17.12/17.36 inference(scs_inference,[],[454,2])).
% 17.12/17.36 cnf(482,plain,
% 17.12/17.36 (E(f9(a1,a7),f9(a1,a8))+~E(f4(a1,a7),f4(a1,a8))),
% 17.12/17.36 inference(scs_inference,[],[2,455])).
% 17.12/17.36 cnf(534,plain,
% 17.12/17.36 (~E(x5341,a1)+P1(x5341)),
% 17.12/17.36 inference(scs_inference,[],[27,2,16])).
% 17.12/17.36 cnf(536,plain,
% 17.12/17.37 (~P4(f9(a1,a7),f9(a1,a8))+P4(f5(a1,a7),f5(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[28,534,62])).
% 17.12/17.37 cnf(574,plain,
% 17.12/17.37 (~E(f4(a1,x5741),x5742)+~P6(f4(a1,x5741),x5742)),
% 17.12/17.37 inference(scs_inference,[],[144,2,22])).
% 17.12/17.37 cnf(576,plain,
% 17.12/17.37 (~E(f4(a1,x5761),x5762)+~P4(x5762,f4(a1,x5761))),
% 17.12/17.37 inference(scs_inference,[],[143,2,23])).
% 17.12/17.37 cnf(578,plain,
% 17.12/17.37 (~E(f4(a1,x5781),x5782)+~P4(f4(a1,x5781),x5782)),
% 17.12/17.37 inference(scs_inference,[],[143,2,24])).
% 17.12/17.37 cnf(582,plain,
% 17.12/17.37 (~E(f2(a1,x5821),f2(a1,x5822))+~E(f9(a1,x5822),f9(a1,x5821))+E(f5(a1,x5821),f5(a1,x5822))),
% 17.12/17.37 inference(scs_inference,[],[2,361])).
% 17.12/17.37 cnf(587,plain,
% 17.12/17.37 (E(f5(a1,x5871),f5(a1,x5872))+~E(f9(a1,x5871),f9(a1,x5872))+~E(f2(a1,x5872),f2(a1,x5871))),
% 17.12/17.37 inference(scs_inference,[],[2,582])).
% 17.12/17.37 cnf(608,plain,
% 17.12/17.37 (~E(f9(a1,x6081),f9(a1,x6082))+~P4(f2(a1,x6081),f2(a1,x6082))+P6(f5(a1,x6081),f5(a1,x6082))),
% 17.12/17.37 inference(scs_inference,[],[27,32,61])).
% 17.12/17.37 cnf(610,plain,
% 17.12/17.37 (P5(f6(a1,x6101),f6(a1,x6102))+~E(f4(a1,x6101),f4(a1,x6102))),
% 17.12/17.37 inference(scs_inference,[],[27,32,43])).
% 17.12/17.37 cnf(658,plain,
% 17.12/17.37 (P3(f6(a1,x6581),f6(a1,x6582))+~E(f4(a1,x6581),f4(a1,x6582))),
% 17.12/17.37 inference(scs_inference,[],[27,33,43])).
% 17.12/17.37 cnf(699,plain,
% 17.12/17.37 (P3(f5(a1,x6991),f5(a1,x6992))+~E(f9(a1,x6991),f9(a1,x6992))+~E(f2(a1,x6992),f2(a1,x6991))),
% 17.12/17.37 inference(scs_inference,[],[33,587])).
% 17.12/17.37 cnf(700,plain,
% 17.12/17.37 (P4(f9(a1,a7),f9(a1,a8))+~E(f2(a1,a8),f2(a1,a7))+P3(f5(a1,a7),f5(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[261,699,40])).
% 17.12/17.37 cnf(701,plain,
% 17.12/17.37 (P3(f5(a1,a7),f5(a1,a8))+~E(f2(a1,a8),f2(a1,a7))+P4(f5(a1,a7),f5(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[28,27,700,62])).
% 17.12/17.37 cnf(702,plain,
% 17.12/17.37 (P4(f5(a1,a7),f5(a1,a8))+~E(f2(a1,a8),f2(a1,a7))+~P4(f6(a1,a7),f6(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[31,27,30,29,701,63])).
% 17.12/17.37 cnf(703,plain,
% 17.12/17.37 (~P4(f6(a1,a7),f6(a1,a8))+~E(f2(a1,a8),f2(a1,a7))+~P3(f6(a1,a7),f6(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[31,27,30,29,702,64])).
% 17.12/17.37 cnf(704,plain,
% 17.12/17.37 (~P3(f6(a1,a7),f6(a1,a8))+~E(f2(a1,a8),f2(a1,a7))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[27,703,60])).
% 17.12/17.37 cnf(705,plain,
% 17.12/17.37 (~P4(f6(a1,a7),f6(a1,a8))+~E(f2(a1,a8),f2(a1,a7))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[704,37])).
% 17.12/17.37 cnf(706,plain,
% 17.12/17.37 (~E(f2(a1,a8),f2(a1,a7))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[27,705,60])).
% 17.12/17.37 cnf(707,plain,
% 17.12/17.37 (~E(f2(a1,a7),f2(a1,a8))+~P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[706,2])).
% 17.12/17.37 cnf(708,plain,
% 17.12/17.37 (~P6(f4(a1,a8),f4(a1,a7))+~E(f2(a1,a7),f2(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[707,38])).
% 17.12/17.37 cnf(709,plain,
% 17.12/17.37 (P6(f2(a1,a7),f2(a1,a8))+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[708,83])).
% 17.12/17.37 cnf(710,plain,
% 17.12/17.37 (P4(f2(a1,a8),f2(a1,a7))+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[709,38])).
% 17.12/17.37 cnf(722,plain,
% 17.12/17.37 (P6(f9(a1,a8),f9(a1,a7))+P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[36,51])).
% 17.12/17.37 cnf(723,plain,
% 17.12/17.37 (P6(x7231,f9(a1,a7))+~E(f9(a1,a8),x7231)+P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[722,21])).
% 17.12/17.37 cnf(759,plain,
% 17.12/17.37 (P5(x7591,x7592)+~P4(x7592,x7591)),
% 17.12/17.37 inference(scs_inference,[],[36,35])).
% 17.12/17.37 cnf(791,plain,
% 17.12/17.37 (P6(f6(a1,x7911),f6(a1,x7912))+~P4(f4(a1,x7912),f4(a1,x7911))),
% 17.12/17.37 inference(scs_inference,[],[27,36,60])).
% 17.12/17.37 cnf(792,plain,
% 17.12/17.37 (~P6(f4(a1,x7921),f4(a1,x7922))+P6(f6(a1,x7921),f6(a1,x7922))),
% 17.12/17.37 inference(scs_inference,[],[791,38])).
% 17.12/17.37 cnf(793,plain,
% 17.12/17.37 (P5(f6(a1,x7931),f6(a1,x7932))+~P6(f4(a1,x7931),f4(a1,x7932))),
% 17.12/17.37 inference(scs_inference,[],[792,35])).
% 17.12/17.37 cnf(823,plain,
% 17.12/17.37 (P3(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[37,50])).
% 17.12/17.37 cnf(827,plain,
% 17.12/17.37 (P5(x8271,x8271)),
% 17.12/17.37 inference(rename_variables,[],[65])).
% 17.12/17.37 cnf(847,plain,
% 17.12/17.37 (P4(f4(a1,a7),f4(a1,a8))+P6(f9(a1,a7),f9(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[823,66,65,827,40,18,17,25,137,367,576,578,610,658,455,482,574,38,2,723])).
% 17.12/17.37 cnf(894,plain,
% 17.12/17.37 (E(f9(a1,a7),f9(a1,a8))+P6(f9(a1,a7),f9(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[847,292])).
% 17.12/17.37 cnf(971,plain,
% 17.12/17.37 (P3(f6(a1,x9711),f6(a1,x9712))+~P4(f4(a1,x9711),f4(a1,x9712))),
% 17.12/17.37 inference(scs_inference,[],[27,37,60])).
% 17.12/17.37 cnf(972,plain,
% 17.12/17.37 (E(f4(a1,a7),f4(a1,a8))+P3(f6(a1,a7),f6(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[823,971,40])).
% 17.12/17.37 cnf(978,plain,
% 17.12/17.37 (~P4(x9781,x9782)+~P6(x9781,x9782)),
% 17.12/17.37 inference(scs_inference,[],[38,41])).
% 17.12/17.37 cnf(986,plain,
% 17.12/17.37 (~P6(f4(a1,a8),f4(a1,a7))+~E(f5(a1,a8),f5(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[38,116])).
% 17.12/17.37 cnf(987,plain,
% 17.12/17.37 (~E(f5(a1,a7),f5(a1,a8))+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[986,2])).
% 17.12/17.37 cnf(988,plain,
% 17.12/17.37 (~E(x9881,f5(a1,a8))+~E(f5(a1,a7),x9881)+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[987,3])).
% 17.12/17.37 cnf(1012,plain,
% 17.12/17.37 (~P6(f4(a1,x10121),f4(a1,x10122))+P4(f6(a1,x10122),f6(a1,x10121))),
% 17.12/17.37 inference(scs_inference,[],[27,38,60])).
% 17.12/17.37 cnf(1013,plain,
% 17.12/17.37 (~P6(f4(a1,a8),f4(a1,a7))+~P3(f5(a1,a7),f5(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[31,27,30,29,1012,63])).
% 17.12/17.37 cnf(1014,plain,
% 17.12/17.37 (~P4(f5(a1,a7),f5(a1,a8))+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1013,37])).
% 17.12/17.37 cnf(1015,plain,
% 17.12/17.37 (~P4(f9(a1,a7),f9(a1,a8))+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1014,536])).
% 17.12/17.37 cnf(1019,plain,
% 17.12/17.37 (~P6(f5(a1,a8),f5(a1,a7))+~P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[38,1014])).
% 17.12/17.37 cnf(1036,plain,
% 17.12/17.37 (P4(f6(a1,x10361),f6(a1,x10362))+~P4(f4(a1,x10361),f4(a1,x10362))),
% 17.12/17.37 inference(scs_inference,[],[38,791])).
% 17.12/17.37 cnf(1037,plain,
% 17.12/17.37 (E(f4(a1,a7),f4(a1,a8))+P4(f6(a1,a7),f6(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[823,1036,40])).
% 17.12/17.37 cnf(1043,plain,
% 17.12/17.37 (P4(f9(a1,a7),f9(a1,a7))+P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[38,847])).
% 17.12/17.37 cnf(1044,plain,
% 17.12/17.37 (P6(f4(a1,a8),f4(a1,a7))+P4(f9(a1,a7),f9(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1043,36])).
% 17.12/17.37 cnf(1045,plain,
% 17.12/17.37 (P4(f9(a1,a7),f9(a1,a7))+~E(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1044,574])).
% 17.12/17.37 cnf(1046,plain,
% 17.12/17.37 (~E(f4(a1,a7),f4(a1,a8))+P4(f9(a1,a7),f9(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1045,2])).
% 17.12/17.37 cnf(1051,plain,
% 17.12/17.37 (~P6(f9(a1,x10511),f9(a1,x10511))+P4(f5(a1,x10511),f5(a1,x10511))),
% 17.12/17.37 inference(scs_inference,[],[65,27,38,62])).
% 17.12/17.37 cnf(1052,plain,
% 17.12/17.37 (~P6(f9(a1,x10521),f9(a1,x10521))),
% 17.12/17.37 inference(scs_inference,[],[1051,41])).
% 17.12/17.37 cnf(1054,plain,
% 17.12/17.37 (E(f9(a1,a7),f9(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[1052,894])).
% 17.12/17.37 cnf(1058,plain,
% 17.12/17.37 (P6(f4(a1,a8),f4(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1052,36,1044])).
% 17.12/17.37 cnf(1060,plain,
% 17.12/17.37 (~E(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[1052,36,1044,1045,1046])).
% 17.12/17.37 cnf(1062,plain,
% 17.12/17.37 (~P4(f9(a1,a7),f9(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[1052,36,1044,1045,1046,988,1015])).
% 17.12/17.37 cnf(1070,plain,
% 17.12/17.37 (~E(f5(x10701,a7),f5(a1,a8))+~E(f5(a1,a7),f5(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[1052,36,1044,1045,1046,988,1015,369,709,710,793,972,986,987])).
% 17.12/17.37 cnf(1088,plain,
% 17.12/17.37 (~E(f5(a1,a7),f5(a1,a8))),
% 17.12/17.37 inference(factoring_inference,[],[1070])).
% 17.12/17.37 cnf(1089,plain,
% 17.12/17.37 (P4(f4(a1,a7),f4(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[1062,51])).
% 17.12/17.37 cnf(1091,plain,
% 17.12/17.37 (P4(f2(a1,a8),f2(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1054,1088,224])).
% 17.12/17.37 cnf(1104,plain,
% 17.12/17.37 (E(f9(a1,a8),f9(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1062,408])).
% 17.12/17.37 cnf(1150,plain,
% 17.12/17.37 (~P6(f5(a1,a8),f5(a1,a7))),
% 17.12/17.37 inference(scs_inference,[],[1058,1019])).
% 17.12/17.37 cnf(1152,plain,
% 17.12/17.37 (P4(f6(a1,a7),f6(a1,a8))),
% 17.12/17.37 inference(scs_inference,[],[1060,1037])).
% 17.12/17.37 cnf(1222,plain,
% 17.12/17.37 ($false),
% 17.12/17.37 inference(scs_inference,[],[1089,1054,1091,1104,1152,1150,759,791,978,111,38,608]),
% 17.12/17.37 ['proof']).
% 17.12/17.37 % SZS output end Proof
% 17.12/17.37 % Total time :16.879676s
%------------------------------------------------------------------------------