%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT054-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n003.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.46s 58.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT054-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n003.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 13:26:39 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.25/0.50 start to proof:theBenchmark
% 58.46/58.66 %-------------------------------------------
% 58.46/58.66 % File :CSE---1.7
% 58.46/58.66 % Problem :theBenchmark
% 58.46/58.66 % Transform :cnf
% 58.46/58.66 % Format :tptp:raw
% 58.46/58.66 % Command :java -jar mcs_scs.jar %d %s
% 58.46/58.66
% 58.46/58.66 % Result :Theorem 58.168065s
% 58.46/58.66 % Output :CNFRefutation 58.168065s
% 58.46/58.66 %-------------------------------------------
% 58.46/58.66 %--------------------------------------------------------------------------
% 58.46/58.66 % File : MGT054-1 : TPTP v9.3.0. Released v2.4.0.
% 58.46/58.66 % Domain : Management (Organisation Theory)
% 58.46/58.66 % Problem : Hazard of mortality increases in a drifting environment
% 58.46/58.66 % Version : [Han98] axioms.
% 58.46/58.66 % English : An unendowed organization's hazard of mortality increases with
% 58.46/58.66 % age in a drifting environment.
% 58.46/58.66
% 58.46/58.66 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 58.46/58.66 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 58.46/58.66 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 58.46/58.66 % Source : [TPTP]
% 58.46/58.66 % Names :
% 58.46/58.66
% 58.46/58.66 % Status : Unsatisfiable
% 58.46/58.66 % 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.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.06 v5.0.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.11 v2.4.0
% 58.46/58.66 % Syntax : Number of clauses : 32 ( 7 unt; 11 nHn; 25 RR)
% 58.46/58.66 % Number of literals : 84 ( 9 equ; 43 neg)
% 58.46/58.66 % Maximal clause size : 5 ( 2 avg)
% 58.46/58.66 % Maximal term depth : 2 ( 1 avg)
% 58.46/58.66 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 58.46/58.66 % Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% 58.46/58.67 % Number of variables : 63 ( 5 sgn)
% 58.46/58.67 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.46/58.67
% 58.46/58.67 % Comments : See MGT042+1.p for the mnemonic names.
% 58.46/58.67 % : Created with tptp2X -f tptp -t clausify:otter MGT054+1.p
% 58.46/58.67 %--------------------------------------------------------------------------
% 58.46/58.67 include('Axioms/MGT001-0.ax').
% 58.46/58.67 %--------------------------------------------------------------------------
% 58.46/58.67 cnf(assumption_1_38,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | has_endowment(A)
% 58.46/58.67 | ~ has_immunity(A,B) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(assumption_3_39,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | ~ has_immunity(A,B)
% 58.46/58.67 | has_immunity(A,C)
% 58.46/58.67 | greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_40,axiom,
% 58.46/58.67 ( ~ dissimilar(A,B,C)
% 58.46/58.67 | organization(A) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_41,axiom,
% 58.46/58.67 ( ~ dissimilar(A,B,C)
% 58.46/58.67 | is_aligned(A,B)
% 58.46/58.67 | is_aligned(A,C) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_42,axiom,
% 58.46/58.67 ( ~ dissimilar(A,B,C)
% 58.46/58.67 | ~ is_aligned(A,B)
% 58.46/58.67 | ~ is_aligned(A,C) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_43,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | ~ is_aligned(A,B)
% 58.46/58.67 | is_aligned(A,B)
% 58.46/58.67 | dissimilar(A,B,C) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_44,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | ~ is_aligned(A,B)
% 58.46/58.67 | is_aligned(A,C)
% 58.46/58.67 | dissimilar(A,B,C) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_45,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | ~ is_aligned(A,B)
% 58.46/58.67 | is_aligned(A,C)
% 58.46/58.67 | dissimilar(A,C,B) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(definition_2_46,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | ~ is_aligned(A,B)
% 58.46/58.67 | is_aligned(A,B)
% 58.46/58.67 | dissimilar(A,C,B) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(assumption_13_47,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | age(A,B) != zero
% 58.46/58.67 | is_aligned(A,B) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(assumption_14_48,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | ~ is_aligned(A,B)
% 58.46/58.67 | is_aligned(A,C)
% 58.46/58.67 | greater(capability(A,B),capability(A,C)) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(assumption_15_49,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | age(A,B) != zero
% 58.46/58.67 | ~ greater(age(A,C),sigma)
% 58.46/58.67 | dissimilar(A,B,C) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(assumption_15_50,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | age(A,B) != zero
% 58.46/58.67 | ~ dissimilar(A,B,C)
% 58.46/58.67 | greater(age(A,C),sigma) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(assumption_16_51,axiom,
% 58.46/58.67 ( ~ organization(A)
% 58.46/58.67 | has_immunity(A,B)
% 58.46/58.67 | has_immunity(A,C)
% 58.46/58.67 | ~ greater(capability(A,C),capability(A,B))
% 58.46/58.67 | greater(hazard_of_mortality(A,B),hazard_of_mortality(A,C)) ) ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_52,negated_conjecture,
% 58.46/58.67 organization(sk1) ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_53,negated_conjecture,
% 58.46/58.67 ~ has_endowment(sk1) ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_54,negated_conjecture,
% 58.46/58.67 age(sk1,sk2) = zero ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_55,negated_conjecture,
% 58.46/58.67 smaller_or_equal(age(sk1,sk3),sigma) ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_56,negated_conjecture,
% 58.46/58.67 greater(age(sk1,sk4),sigma) ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_57,negated_conjecture,
% 58.46/58.67 greater(sigma,zero) ).
% 58.46/58.67
% 58.46/58.67 cnf(theorem_5_58,negated_conjecture,
% 58.46/58.67 ~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ).
% 58.46/58.67
% 58.46/58.67 %--------------------------------------------------------------------------
% 58.46/58.67 %-------------------------------------------
% 58.46/58.67 % Proof found
% 58.46/58.67 % SZS status Theorem for theBenchmark
% 58.46/58.67 % SZS output start Proof
% 58.46/58.67 %ClaNum:56(EqnAxiom:26)
% 58.46/58.67 %VarNum:142(SingletonVarNum:57)
% 58.46/58.67 %MaxLitNum:5
% 58.46/58.67 %MaxfuncDepth:1
% 58.46/58.67 %SharedTerms:18
% 58.46/58.67 %goalClause: 27 28 29 30 31 32 33
% 58.46/58.67 %singleGoalClaCount:7
% 58.46/58.67 [27]P1(a1)
% 58.46/58.68 [29]P2(a3,a7)
% 58.46/58.68 [32]~P4(a1)
% 58.46/58.68 [28]E(f2(a1,a6),a7)
% 58.46/58.68 [30]P8(f2(a1,a8),a3)
% 58.46/58.68 [31]P2(f2(a1,a9),a3)
% 58.46/58.68 [33]~P2(f4(a1,a9),f4(a1,a8))
% 58.46/58.68 [34]~E(x341,x342)+P8(x341,x342)
% 58.46/58.68 [35]~E(x351,x352)+P5(x351,x352)
% 58.46/58.68 [38]~P9(x381,x382)+P8(x381,x382)
% 58.46/58.68 [39]~P2(x392,x391)+P9(x391,x392)
% 58.46/58.68 [40]~P2(x401,x402)+P5(x401,x402)
% 58.46/58.68 [41]~P9(x412,x411)+P2(x411,x412)
% 58.46/58.68 [45]~P2(x452,x451)+~P2(x451,x452)
% 58.46/58.68 [47]P1(x471)+~P3(x471,x472,x473)
% 58.46/58.68 [36]P9(x361,x362)+P2(x361,x362)+E(x361,x362)
% 58.46/58.68 [37]~P1(x371)+P4(x371)+~P6(x371,x372)
% 58.46/58.68 [42]P9(x421,x422)+~P8(x421,x422)+E(x421,x422)
% 58.46/58.68 [43]P2(x431,x432)+~P5(x431,x432)+E(x431,x432)
% 58.46/58.68 [44]~P1(x441)+P7(x441,x442)+~E(f2(x441,x442),a7)
% 58.46/58.68 [46]~P2(x461,x463)+P2(x461,x462)+~P2(x463,x462)
% 58.46/58.68 [52]~P3(x521,x523,x522)+P7(x521,x522)+P7(x521,x523)
% 58.46/58.68 [53]~P3(x531,x533,x532)+~P7(x531,x532)+~P7(x531,x533)
% 58.46/58.68 [48]~P1(x481)+~P7(x481,x483)+P7(x481,x482)+P3(x481,x482,x483)
% 58.46/58.68 [49]~P1(x491)+~P7(x491,x493)+P7(x491,x492)+P3(x491,x493,x492)
% 58.46/58.68 [50]~P1(x501)+~P6(x501,x503)+P6(x501,x502)+P2(f4(x501,x502),f4(x501,x503))
% 58.46/58.68 [51]~P1(x511)+~P7(x511,x513)+P7(x511,x512)+P2(f5(x511,x513),f5(x511,x512))
% 58.46/58.68 [54]~P1(x541)+P3(x541,x542,x543)+~E(f2(x541,x542),a7)+~P2(f2(x541,x543),a3)
% 58.46/58.68 [55]~P1(x551)+~P3(x551,x553,x552)+P2(f2(x551,x552),a3)+~E(f2(x551,x553),a7)
% 58.46/58.68 [56]~P1(x561)+P6(x561,x562)+P6(x561,x563)+P2(f4(x561,x563),f4(x561,x562))+~P2(f5(x561,x562),f5(x561,x563))
% 58.46/58.68 %EqnAxiom
% 58.46/58.68 [1]E(x11,x11)
% 58.46/58.68 [2]E(x22,x21)+~E(x21,x22)
% 58.46/58.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.46/58.68 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 58.46/58.68 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 58.46/58.68 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 58.46/58.68 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 58.46/58.68 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83))
% 58.46/58.68 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92))
% 58.46/58.68 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 58.46/58.68 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 58.46/58.68 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 58.46/58.68 [13]P8(x132,x133)+~E(x131,x132)+~P8(x131,x133)
% 58.46/58.68 [14]P8(x143,x142)+~E(x141,x142)+~P8(x143,x141)
% 58.46/58.68 [15]P3(x152,x153,x154)+~E(x151,x152)+~P3(x151,x153,x154)
% 58.46/58.68 [16]P3(x163,x162,x164)+~E(x161,x162)+~P3(x163,x161,x164)
% 58.46/58.68 [17]P3(x173,x174,x172)+~E(x171,x172)+~P3(x173,x174,x171)
% 58.46/58.68 [18]~P4(x181)+P4(x182)+~E(x181,x182)
% 58.46/58.68 [19]P7(x192,x193)+~E(x191,x192)+~P7(x191,x193)
% 58.46/58.68 [20]P7(x203,x202)+~E(x201,x202)+~P7(x203,x201)
% 58.46/58.68 [21]P6(x212,x213)+~E(x211,x212)+~P6(x211,x213)
% 58.46/58.68 [22]P6(x223,x222)+~E(x221,x222)+~P6(x223,x221)
% 58.46/58.68 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233)
% 58.46/58.68 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241)
% 58.46/58.68 [25]P9(x252,x253)+~E(x251,x252)+~P9(x251,x253)
% 58.46/58.68 [26]P9(x263,x262)+~E(x261,x262)+~P9(x263,x261)
% 58.46/58.68
% 58.46/58.68 %-------------------------------------------
% 58.46/58.68 cnf(57,plain,
% 58.46/58.68 (P8(x571,x571)),
% 58.46/58.68 inference(equality_inference,[],[34])).
% 58.46/58.68 cnf(58,plain,
% 58.46/58.68 (P5(x581,x581)),
% 58.46/58.68 inference(equality_inference,[],[35])).
% 58.46/58.68 cnf(59,plain,
% 58.46/58.68 (E(a7,f2(a1,a6))),
% 58.46/58.68 inference(scs_inference,[],[28,2])).
% 58.46/58.68 cnf(62,plain,
% 58.46/58.68 (~P2(a7,a3)),
% 58.46/58.68 inference(scs_inference,[],[29,33,28,2,41,45])).
% 58.46/58.68 cnf(64,plain,
% 58.46/58.68 (~P6(a1,x641)),
% 58.46/58.68 inference(scs_inference,[],[27,29,32,33,28,2,41,45,37])).
% 58.46/58.68 cnf(66,plain,
% 58.46/58.68 (P7(a1,a6)),
% 58.46/58.68 inference(scs_inference,[],[27,29,32,33,28,2,41,45,37,44])).
% 58.46/58.68 cnf(69,plain,
% 58.46/58.68 (P2(a3,f2(a1,a6))),
% 58.46/58.68 inference(scs_inference,[],[27,29,32,33,28,31,2,41,45,37,44,11,12])).
% 58.46/58.68 cnf(71,plain,
% 58.46/58.68 (P8(x711,x711)),
% 58.46/58.68 inference(rename_variables,[],[57])).
% 58.46/58.68 cnf(79,plain,
% 58.46/58.68 (P5(x791,x791)),
% 58.46/58.68 inference(rename_variables,[],[58])).
% 58.46/58.68 cnf(82,plain,
% 58.46/58.68 (P3(a1,a6,a9)),
% 58.46/58.68 inference(scs_inference,[],[27,29,32,33,28,31,57,71,58,79,2,41,45,37,44,11,12,13,14,46,53,23,24,54])).
% 58.46/58.68 cnf(84,plain,
% 58.46/58.68 (~E(f2(a1,a9),f2(a1,a6))),
% 58.46/58.68 inference(scs_inference,[],[27,29,32,33,28,31,57,71,58,79,2,41,45,37,44,11,12,13,14,46,53,23,24,54,3])).
% 58.46/58.68 cnf(90,plain,
% 58.46/58.68 (~P9(a3,a7)),
% 58.46/58.68 inference(scs_inference,[],[62,41])).
% 58.46/58.68 cnf(92,plain,
% 58.46/58.68 (~P2(a3,f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[31,62,41,45])).
% 58.46/58.68 cnf(94,plain,
% 58.46/58.68 (~P2(a7,f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[31,62,41,45,46])).
% 58.46/58.68 cnf(96,plain,
% 58.46/58.68 (~E(a7,f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[29,31,62,41,45,46,12])).
% 58.46/58.68 cnf(98,plain,
% 58.46/58.68 (P9(a7,f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[29,31,66,62,41,45,46,12,19,36])).
% 58.46/58.68 cnf(100,plain,
% 58.46/58.68 (P7(a1,x1001)+~E(a6,x1001)),
% 58.46/58.68 inference(scs_inference,[],[29,31,66,62,41,45,46,12,19,36,20])).
% 58.46/58.68 cnf(103,plain,
% 58.46/58.68 (E(f2(a1,a8),a3)+P9(f2(a1,a8),a3)),
% 58.46/58.68 inference(scs_inference,[],[30,29,31,66,59,62,41,45,46,12,19,36,20,25,26,42])).
% 58.46/58.68 cnf(113,plain,
% 58.46/58.68 (~P9(f2(a1,a9),a3)),
% 58.46/58.68 inference(scs_inference,[],[69,92,45,41])).
% 58.46/58.68 cnf(115,plain,
% 58.46/58.68 (P2(f2(a1,a9),f2(a1,a6))),
% 58.46/58.68 inference(scs_inference,[],[31,69,92,45,41,46])).
% 58.46/58.68 cnf(128,plain,
% 58.46/58.68 (~P2(f2(a1,a6),f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[94,115,41,45])).
% 58.46/58.68 cnf(144,plain,
% 58.46/58.68 (~P9(f2(a1,a9),f2(a1,a6))),
% 58.46/58.68 inference(scs_inference,[],[128,41])).
% 58.46/58.68 cnf(146,plain,
% 58.46/58.68 (P2(x1461,a7)+~E(a3,x1461)),
% 58.46/58.68 inference(scs_inference,[],[29,128,41,11])).
% 58.46/58.68 cnf(220,plain,
% 58.46/58.68 (P8(f2(a1,a6),f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[98,59,38,13])).
% 58.46/58.68 cnf(221,plain,
% 58.46/58.68 (P8(a7,f2(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[28,220,13])).
% 58.46/58.68 cnf(223,plain,
% 58.46/58.68 (P6(a1,a9)+~P2(f5(a1,a8),f5(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[27,28,33,64,220,13,14,56])).
% 58.46/58.68 cnf(227,plain,
% 58.46/58.68 (~P2(f5(a1,a8),f5(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[64,223])).
% 58.46/58.68 cnf(233,plain,
% 58.46/58.68 (E(f5(a1,a9),f5(a1,a8))+P9(f5(a1,a8),f5(a1,a9))),
% 58.46/58.68 inference(scs_inference,[],[64,223,41,36,2])).
% 58.46/58.68 cnf(237,plain,
% 58.46/58.68 (~P7(a1,a8)+P7(a1,a9)),
% 58.46/58.68 inference(scs_inference,[],[27,221,227,14,51])).
% 58.46/58.68 cnf(240,plain,
% 58.46/58.68 (P8(a7,a3)),
% 58.46/58.68 inference(scs_inference,[],[29,39,38])).
% 58.46/58.68 cnf(242,plain,
% 58.46/58.68 (P8(a7,x2421)+~E(a3,x2421)),
% 58.46/58.68 inference(scs_inference,[],[59,240,13,14])).
% 58.46/58.68 cnf(244,plain,
% 58.46/58.68 (P5(a3,f2(a1,a6))),
% 58.46/58.68 inference(scs_inference,[],[29,59,40,24])).
% 58.46/58.68 cnf(245,plain,
% 58.46/58.68 (P5(a3,a7)),
% 58.46/58.68 inference(scs_inference,[],[28,244,24])).
% 58.46/58.68 cnf(251,plain,
% 58.46/58.68 (P5(x2511,a7)+~E(a3,x2511)),
% 58.46/58.68 inference(scs_inference,[],[245,23])).
% 58.46/58.68 cnf(258,plain,
% 58.46/58.68 (P7(a1,a9)+~E(a6,a8)),
% 58.46/58.68 inference(scs_inference,[],[237,100])).
% 58.46/58.68 cnf(313,plain,
% 58.46/58.68 (P2(a3,f2(a1,a8))+E(f2(a1,a8),a3)),
% 58.46/58.68 inference(scs_inference,[],[103,41])).
% 58.46/58.69 cnf(344,plain,
% 58.46/58.69 (P5(a3,f2(a1,a8))+P2(a3,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[58,313,23])).
% 58.46/58.69 cnf(407,plain,
% 58.46/58.69 (P2(f5(a1,a9),f5(a1,a8))+E(f5(a1,a9),f5(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[233,41])).
% 58.46/58.69 cnf(413,plain,
% 58.46/58.69 (P5(f5(a1,a9),f5(a1,a8))+E(f5(a1,a9),f5(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[407,40])).
% 58.46/58.69 cnf(414,plain,
% 58.46/58.69 (P5(x4141,f5(a1,a8))+~E(f5(a1,a9),x4141)+E(f5(a1,a9),f5(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[413,23])).
% 58.46/58.69 cnf(421,plain,
% 58.46/58.69 (~P3(a1,a8,a8)+P7(a1,a9)),
% 58.46/58.69 inference(scs_inference,[],[52,237])).
% 58.46/58.69 cnf(1244,plain,
% 58.46/58.69 (P5(f5(a1,a9),f5(a1,a8))+~E(f5(a1,a9),x12441)+P5(x12441,f5(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[35,414])).
% 58.46/58.69 cnf(1245,plain,
% 58.46/58.69 (P5(f5(a1,a9),f5(a1,a8))+P5(f5(a1,a9),f5(a1,a8))),
% 58.46/58.69 inference(equality_inference,[],[1244])).
% 58.46/58.69 cnf(1246,plain,
% 58.46/58.69 (P5(f5(a1,a9),f5(a1,a8))),
% 58.46/58.69 inference(factoring_inference,[],[1245])).
% 58.46/58.69 cnf(1247,plain,
% 58.46/58.69 (P5(f5(a1,a9),x12471)+~E(f5(a1,a8),x12471)),
% 58.46/58.69 inference(scs_inference,[],[1246,24])).
% 58.46/58.69 cnf(1284,plain,
% 58.46/58.69 (~P2(a3,a7)+P9(a7,x12841)+~E(a3,x12841)),
% 58.46/58.69 inference(scs_inference,[],[29,39,26])).
% 58.46/58.69 cnf(1286,plain,
% 58.46/58.69 (~E(a3,x12861)+P9(a7,x12861)),
% 58.46/58.69 inference(scs_inference,[],[29,1284])).
% 58.46/58.69 cnf(1287,plain,
% 58.46/58.69 (P9(a7,a7)+~E(a3,f2(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[28,29,1284,26])).
% 58.46/58.69 cnf(1393,plain,
% 58.46/58.69 (P2(a7,a7)+~E(a3,f2(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[41,1287])).
% 58.46/58.69 cnf(1421,plain,
% 58.46/58.69 (~E(a3,f2(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[45,1393])).
% 58.46/58.69 cnf(1423,plain,
% 58.46/58.69 (~P2(f5(a1,x14231),f5(a1,x14231))),
% 58.46/58.69 inference(scs_inference,[],[27,64,45,56])).
% 58.46/58.69 cnf(1424,plain,
% 58.46/58.69 (~P9(f5(a1,x14241),f5(a1,x14241))),
% 58.46/58.69 inference(scs_inference,[],[1423,41])).
% 58.46/58.69 cnf(1450,plain,
% 58.46/58.69 (~E(x14501,a6)+P7(a1,x14501)),
% 58.46/58.69 inference(scs_inference,[],[100,2])).
% 58.46/58.69 cnf(1467,plain,
% 58.46/58.69 (~E(a3,a7)),
% 58.46/58.69 inference(scs_inference,[],[1421,59,3])).
% 58.46/58.69 cnf(1669,plain,
% 58.46/58.69 (~E(x16691,a3)+P2(x16691,a7)),
% 58.46/58.69 inference(scs_inference,[],[146,2])).
% 58.46/58.69 cnf(1671,plain,
% 58.46/58.69 (~P2(a7,x16711)+~E(a3,x16711)),
% 58.46/58.69 inference(scs_inference,[],[146,45])).
% 58.46/58.69 cnf(1705,plain,
% 58.46/58.69 (P7(a1,a9)+~E(a8,a6)),
% 58.46/58.69 inference(scs_inference,[],[237,1450])).
% 58.46/58.69 cnf(1713,plain,
% 58.46/58.69 (P7(a1,a9)+~E(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[27,237,44])).
% 58.46/58.69 cnf(1735,plain,
% 58.46/58.69 (P7(a1,a9)+P3(a1,a6,a8)),
% 58.46/58.69 inference(scs_inference,[],[66,27,237,49])).
% 58.46/58.69 cnf(1739,plain,
% 58.46/58.69 (P7(a1,a9)+P3(a1,a8,a6)),
% 58.46/58.69 inference(scs_inference,[],[66,27,237,48])).
% 58.46/58.69 cnf(1741,plain,
% 58.46/58.69 (~E(x17411,a3)+P8(a7,x17411)),
% 58.46/58.69 inference(scs_inference,[],[242,2])).
% 58.46/58.69 cnf(1743,plain,
% 58.46/58.69 (~E(x17431,a3)+P5(x17431,a7)),
% 58.46/58.69 inference(scs_inference,[],[251,2])).
% 58.46/58.69 cnf(1769,plain,
% 58.46/58.69 (~E(x17691,a3)+P9(a7,x17691)),
% 58.46/58.69 inference(scs_inference,[],[1286,2])).
% 58.46/58.69 cnf(1781,plain,
% 58.46/58.69 (~P2(a7,x17811)+~E(x17811,a3)),
% 58.46/58.69 inference(scs_inference,[],[1669,45])).
% 58.46/58.69 cnf(1783,plain,
% 58.46/58.69 (P9(f2(a1,a8),a3)+P2(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[1669,103])).
% 58.46/58.69 cnf(1784,plain,
% 58.46/58.69 (P2(a3,f2(a1,a8))+P2(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[1783,41])).
% 58.46/58.69 cnf(1788,plain,
% 58.46/58.69 (~E(a7,a3)),
% 58.46/58.69 inference(scs_inference,[],[1669,1781])).
% 58.46/58.69 cnf(1792,plain,
% 58.46/58.69 (~P9(x17921,a7)+~E(a3,x17921)),
% 58.46/58.69 inference(scs_inference,[],[1671,41])).
% 58.46/58.69 cnf(1803,plain,
% 58.46/58.69 (P9(f2(a1,a8),a3)+P8(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[1741,103])).
% 58.46/58.69 cnf(1804,plain,
% 58.46/58.69 (P2(a3,f2(a1,a8))+P8(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[1803,41])).
% 58.46/58.69 cnf(1809,plain,
% 58.46/58.69 (P9(f2(a1,a8),a3)+P5(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[1743,103])).
% 58.46/58.69 cnf(1810,plain,
% 58.46/58.69 (P2(a3,f2(a1,a8))+P5(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[1809,41])).
% 58.46/58.69 cnf(1814,plain,
% 58.46/58.69 (P9(f2(a1,a8),a3)+P9(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[1769,103])).
% 58.46/58.69 cnf(1815,plain,
% 58.46/58.69 (P2(a3,f2(a1,a8))+P9(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[1814,41])).
% 58.46/58.69 cnf(1825,plain,
% 58.46/58.69 (P9(f2(a1,a8),a3)+~P2(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[1781,103])).
% 58.46/58.69 cnf(1826,plain,
% 58.46/58.69 (P2(a3,f2(a1,a8))+~P2(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[1825,41])).
% 58.46/58.69 cnf(1830,plain,
% 58.46/58.69 (~E(x18301,a3)+~P9(x18301,a7)),
% 58.46/58.69 inference(scs_inference,[],[1792,2])).
% 58.46/58.69 cnf(1846,plain,
% 58.46/58.69 (P9(f2(a1,a8),a3)+~P9(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[1830,103])).
% 58.46/58.69 cnf(1847,plain,
% 58.46/58.69 (P2(a3,f2(a1,a8))+~P9(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[1846,41])).
% 58.46/58.69 cnf(1894,plain,
% 58.46/58.69 (P2(f5(a1,a6),f5(a1,a9))),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51])).
% 58.46/58.69 cnf(1896,plain,
% 58.46/58.69 (~P7(a1,a8)),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51,237])).
% 58.46/58.69 cnf(1900,plain,
% 58.46/58.69 (P3(a1,a6,a8)),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51,237,258,1705,421,1735])).
% 58.46/58.69 cnf(1902,plain,
% 58.46/58.69 (~E(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51,237,258,1705,421,1735,1739,1713])).
% 58.46/58.69 cnf(1905,plain,
% 58.46/58.69 (P9(f5(a1,a9),f5(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51,237,258,1705,421,1735,1739,1713,40,39])).
% 58.46/58.69 cnf(1907,plain,
% 58.46/58.69 (~P2(f5(a1,a9),f5(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51,237,258,1705,421,1735,1739,1713,40,39,45])).
% 58.46/58.69 cnf(1909,plain,
% 58.46/58.69 (~E(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[96,144,94,84,82,59,66,27,53,43,42,14,48,51,237,258,1705,421,1735,1739,1713,40,39,45,2])).
% 58.46/58.69 cnf(1926,plain,
% 58.46/58.69 (~P5(a7,a3)),
% 58.46/58.69 inference(scs_inference,[],[1788,62,43])).
% 58.46/58.69 cnf(1928,plain,
% 58.46/58.69 (~P2(f5(a1,a8),f5(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[1788,1894,62,227,43,46])).
% 58.46/58.69 cnf(1930,plain,
% 58.46/58.69 (~P8(a3,a7)),
% 58.46/58.69 inference(scs_inference,[],[1467,1788,1894,90,62,227,43,46,42])).
% 58.46/58.69 cnf(1932,plain,
% 58.46/58.69 (~E(f5(a1,a9),f5(a1,a6))),
% 58.46/58.69 inference(scs_inference,[],[1467,1788,1894,1423,90,62,227,43,46,42,12])).
% 58.46/58.69 cnf(1936,plain,
% 58.46/58.69 (P2(f2(a1,a8),a3)),
% 58.46/58.69 inference(scs_inference,[],[28,1467,1788,1900,1894,1905,1424,1423,90,62,227,27,43,46,42,12,26,55])).
% 58.46/58.69 cnf(1938,plain,
% 58.46/58.69 (P2(f5(a1,a6),f5(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,66,27,43,46,42,12,26,55,51])).
% 58.46/58.69 cnf(1942,plain,
% 58.46/58.69 (P9(a3,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,66,27,43,46,42,12,26,55,51,40,39])).
% 58.46/58.69 cnf(1944,plain,
% 58.46/58.69 (~P2(a3,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,66,27,43,46,42,12,26,55,51,40,39,45])).
% 58.46/58.69 cnf(1947,plain,
% 58.46/58.69 (~P5(f2(a1,a6),a3)),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,59,66,27,43,46,42,12,26,55,51,40,39,45,21,23])).
% 58.46/58.69 cnf(1951,plain,
% 58.46/58.69 (P9(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,59,66,27,43,46,42,12,26,55,51,40,39,45,21,23,1784,1804,1810,1815])).
% 58.46/58.69 cnf(1952,plain,
% 58.46/58.69 (~P2(a7,f2(a1,a8))),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,59,66,27,43,46,42,12,26,55,51,40,39,45,21,23,1784,1804,1810,1815,1826])).
% 58.46/58.69 cnf(1953,plain,
% 58.46/58.69 (~P9(f2(a1,a8),a7)),
% 58.46/58.69 inference(scs_inference,[],[28,1896,1467,1788,1900,1894,1905,1424,1423,90,62,227,59,66,27,43,46,42,12,26,55,51,40,39,45,21,23,1784,1804,1810,1815,1826,1847])).
% 58.46/58.70 cnf(1960,plain,
% 58.46/58.70 (E(f2(a1,a8),a3)),
% 58.46/58.70 inference(scs_inference,[],[1944,313])).
% 58.46/58.70 cnf(1961,plain,
% 58.46/58.70 (P5(a3,f2(a1,a8))),
% 58.46/58.70 inference(scs_inference,[],[1944,344])).
% 58.46/58.70 cnf(1977,plain,
% 58.46/58.70 (~P9(f2(a1,a8),f2(a1,a6))),
% 58.46/58.70 inference(scs_inference,[],[28,1932,1938,1907,1936,1952,1953,1902,1909,69,59,40,39,3,43,46,42,11,26])).
% 58.46/58.70 cnf(1979,plain,
% 58.46/58.70 (~E(f5(a1,a8),f5(a1,a6))),
% 58.46/58.70 inference(scs_inference,[],[28,1930,1932,1938,1907,1936,1952,1953,1902,1909,69,59,40,39,3,43,46,42,11,26,14,1247])).
% 58.46/58.70 cnf(1982,plain,
% 58.46/58.70 (~E(f2(a1,a8),f2(a1,a6))),
% 58.46/58.70 inference(scs_inference,[],[28,1930,1932,1938,1907,1936,1952,1953,1902,1909,69,59,40,39,3,43,46,42,11,26,14,1247,38,2])).
% 58.46/58.70 cnf(1984,plain,
% 58.46/58.70 (P9(f2(a1,a6),f2(a1,a8))),
% 58.46/58.70 inference(scs_inference,[],[28,1930,1932,1938,1907,1936,1951,1952,1953,1902,1909,69,59,40,39,3,43,46,42,11,26,14,1247,38,2,17,25])).
% 58.46/58.70 cnf(2000,plain,
% 58.46/58.70 (~P2(f2(a1,a8),f2(a1,a8))),
% 58.46/58.70 inference(scs_inference,[],[1926,1960,1979,1928,1984,1977,1982,1944,38,2,24,43,42,11])).
% 58.46/58.70 cnf(2001,plain,
% 58.46/58.70 (~P9(f2(a1,a9),f2(a1,a8))),
% 58.46/58.70 inference(scs_inference,[],[1926,1960,1979,1928,1984,1977,1982,1944,113,38,2,24,43,42,11,26])).
% 58.46/58.70 cnf(2010,plain,
% 58.46/58.70 ($false),
% 58.46/58.70 inference(scs_inference,[],[2001,2000,1961,1947,1942,1944,1936,1960,25,24,43,12]),
% 58.46/58.70 ['proof']).
% 58.46/58.70 % SZS output end Proof
% 58.46/58.70 % Total time :58.168065s
%------------------------------------------------------------------------------