%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT061-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:22 AM UTC 2026
% Result : Unsatisfiable 58.78s 58.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT061-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.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % 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:37:54 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.32/0.51 start to proof:theBenchmark
% 58.78/58.95 %-------------------------------------------
% 58.78/58.95 % File :CSE---1.7
% 58.78/58.95 % Problem :theBenchmark
% 58.78/58.95 % Transform :cnf
% 58.78/58.95 % Format :tptp:raw
% 58.78/58.95 % Command :java -jar mcs_scs.jar %d %s
% 58.78/58.95
% 58.78/58.95 % Result :Theorem 58.450660s
% 58.78/58.95 % Output :CNFRefutation 58.450660s
% 58.78/58.95 %-------------------------------------------
% 58.78/58.95 %--------------------------------------------------------------------------
% 58.78/58.95 % File : MGT061-1 : TPTP v9.3.0. Released v2.4.0.
% 58.78/58.95 % Domain : Management (Organisation Theory)
% 58.78/58.95 % Problem : Conditions for an in reasing hazard of mortality
% 58.78/58.95 % Version : [Han98] axioms.
% 58.78/58.95 % English : The hazard of mortality increases with age for an unendowed
% 58.78/58.95 % organization with a fragile position in drifting environments.
% 58.78/58.95
% 58.78/58.95 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 58.78/58.95 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 58.78/58.95 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 58.78/58.95 % Source : [TPTP]
% 58.78/58.95 % Names :
% 58.78/58.95
% 58.78/58.95 % Status : Unsatisfiable
% 58.78/58.95 % Rating : 0.08 v9.3.0, 0.09 v9.1.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.07 v6.4.0, 0.00 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.30 v5.3.0, 0.28 v5.2.0, 0.19 v5.1.0, 0.18 v5.0.0, 0.07 v4.1.0, 0.15 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.22 v2.5.0, 0.33 v2.4.0
% 58.78/58.95 % Syntax : Number of clauses : 46 ( 12 unt; 16 nHn; 38 RR)
% 58.78/58.95 % Number of literals : 119 ( 15 equ; 55 neg)
% 58.78/58.95 % Maximal clause size : 5 ( 2 avg)
% 58.78/58.95 % Maximal term depth : 3 ( 1 avg)
% 58.78/58.95 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty)
% 58.78/58.95 % Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% 58.78/58.95 % Number of variables : 72 ( 5 sgn)
% 58.78/58.95 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.78/58.95
% 58.78/58.95 % Comments : See MGT042+1.p for the mnemonic names.
% 58.78/58.95 % : Created with tptp2X -f tptp -t clausify:otter MGT061+1.p
% 58.78/58.96 %--------------------------------------------------------------------------
% 58.78/58.96 include('Axioms/MGT001-0.ax').
% 58.78/58.96 %--------------------------------------------------------------------------
% 58.78/58.96 cnf(assumption_1_39,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | has_endowment(A)
% 58.78/58.96 | ~ has_immunity(A,B) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_40,axiom,
% 58.78/58.96 ( ~ dissimilar(A,B,C)
% 58.78/58.96 | organization(A) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_41,axiom,
% 58.78/58.96 ( ~ dissimilar(A,B,C)
% 58.78/58.96 | is_aligned(A,B)
% 58.78/58.96 | is_aligned(A,C) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_42,axiom,
% 58.78/58.96 ( ~ dissimilar(A,B,C)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | ~ is_aligned(A,C) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_43,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | is_aligned(A,B)
% 58.78/58.96 | dissimilar(A,B,C) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_44,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | is_aligned(A,C)
% 58.78/58.96 | dissimilar(A,B,C) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_45,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | is_aligned(A,C)
% 58.78/58.96 | dissimilar(A,C,B) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_2_46,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | is_aligned(A,B)
% 58.78/58.96 | dissimilar(A,C,B) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_13_47,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | age(A,B) != zero
% 58.78/58.96 | is_aligned(A,B) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_15_48,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | age(A,B) != zero
% 58.78/58.96 | ~ greater(age(A,C),sigma)
% 58.78/58.96 | dissimilar(A,B,C) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_15_49,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | age(A,B) != zero
% 58.78/58.96 | ~ dissimilar(A,B,C)
% 58.78/58.96 | greater(age(A,C),sigma) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_3_50,axiom,
% 58.78/58.96 ( ~ fragile_position(A)
% 58.78/58.96 | ~ smaller_or_equal(age(A,B),sigma)
% 58.78/58.96 | positional_advantage(A,B) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_3_51,axiom,
% 58.78/58.96 ( ~ fragile_position(A)
% 58.78/58.96 | ~ greater(age(A,B),sigma)
% 58.78/58.96 | ~ positional_advantage(A,B) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_3_52,axiom,
% 58.78/58.96 ( smaller_or_equal(age(A,sk1(A)),sigma)
% 58.78/58.96 | greater(age(A,sk1(A)),sigma)
% 58.78/58.96 | fragile_position(A) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_3_53,axiom,
% 58.78/58.96 ( smaller_or_equal(age(A,sk1(A)),sigma)
% 58.78/58.96 | positional_advantage(A,sk1(A))
% 58.78/58.96 | fragile_position(A) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_3_54,axiom,
% 58.78/58.96 ( ~ positional_advantage(A,sk1(A))
% 58.78/58.96 | greater(age(A,sk1(A)),sigma)
% 58.78/58.96 | fragile_position(A) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(definition_3_55,axiom,
% 58.78/58.96 ( ~ positional_advantage(A,sk1(A))
% 58.78/58.96 | positional_advantage(A,sk1(A))
% 58.78/58.96 | fragile_position(A) ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_17_56,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | ~ has_immunity(A,B)
% 58.78/58.96 | hazard_of_mortality(A,B) = very_low ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_17_57,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | has_immunity(A,B)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | ~ positional_advantage(A,B)
% 58.78/58.96 | hazard_of_mortality(A,B) = low ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_17_58,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | has_immunity(A,B)
% 58.78/58.96 | is_aligned(A,B)
% 58.78/58.96 | ~ positional_advantage(A,B)
% 58.78/58.96 | hazard_of_mortality(A,B) = mod1 ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_17_59,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | has_immunity(A,B)
% 58.78/58.96 | ~ is_aligned(A,B)
% 58.78/58.96 | positional_advantage(A,B)
% 58.78/58.96 | hazard_of_mortality(A,B) = mod2 ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_17_60,axiom,
% 58.78/58.96 ( ~ organization(A)
% 58.78/58.96 | has_immunity(A,B)
% 58.78/58.96 | is_aligned(A,B)
% 58.78/58.96 | positional_advantage(A,B)
% 58.78/58.96 | hazard_of_mortality(A,B) = high ) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_18a_61,axiom,
% 58.78/58.96 greater(high,mod1) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_18b_62,axiom,
% 58.78/58.96 greater(mod1,low) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_18c_63,axiom,
% 58.78/58.96 greater(low,very_low) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_18d_64,axiom,
% 58.78/58.96 greater(high,mod2) ).
% 58.78/58.96
% 58.78/58.96 cnf(assumption_18e_65,axiom,
% 58.78/58.96 greater(mod2,low) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_66,negated_conjecture,
% 58.78/58.96 organization(sk2) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_67,negated_conjecture,
% 58.78/58.96 fragile_position(sk2) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_68,negated_conjecture,
% 58.78/58.96 ~ has_endowment(sk2) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_69,negated_conjecture,
% 58.78/58.96 age(sk2,sk3) = zero ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_70,negated_conjecture,
% 58.78/58.96 greater(sigma,zero) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_71,negated_conjecture,
% 58.78/58.96 smaller_or_equal(age(sk2,sk4),sigma) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_72,negated_conjecture,
% 58.78/58.96 greater(age(sk2,sk5),sigma) ).
% 58.78/58.96
% 58.78/58.96 cnf(theorem_7_73,negated_conjecture,
% 58.78/58.96 ( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
% 58.78/58.96 | hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ).
% 58.78/58.96
% 58.78/58.96 %--------------------------------------------------------------------------
% 58.78/58.96 %-------------------------------------------
% 58.78/58.96 % Proof found
% 58.78/58.96 % SZS status Theorem for theBenchmark
% 58.78/58.96 % SZS output start Proof
% 58.78/58.96 %ClaNum:71(EqnAxiom:28)
% 58.78/58.96 %VarNum:177(SingletonVarNum:65)
% 58.78/58.96 %MaxLitNum:5
% 58.78/58.96 %MaxfuncDepth:2
% 58.78/58.96 %SharedTerms:31
% 58.78/58.96 %goalClause: 29 30 31 32 38 39 40 68
% 58.78/58.96 %singleGoalClaCount:7
% 58.78/58.96 [29]P1(a1)
% 58.78/58.96 [30]P2(a1)
% 58.78/58.96 [32]P4(a3,a11)
% 58.78/58.96 [33]P4(a4,a12)
% 58.78/58.96 [34]P4(a7,a4)
% 58.78/58.96 [35]P4(a8,a4)
% 58.78/58.96 [36]P4(a5,a7)
% 58.78/58.96 [37]P4(a5,a8)
% 58.78/58.96 [40]~P5(a1)
% 58.78/58.96 [31]E(f2(a1,a10),a11)
% 58.78/58.96 [38]P9(f2(a1,a13),a3)
% 58.78/58.96 [39]P4(f2(a1,a14),a3)
% 58.78/58.96 [68]~P4(f6(a1,a14),f6(a1,a13))+~E(f6(a1,a13),f6(a1,a10))
% 58.78/58.96 [41]~E(x411,x412)+P9(x411,x412)
% 58.78/58.96 [42]~E(x421,x422)+P6(x421,x422)
% 58.78/58.96 [45]~P10(x451,x452)+P9(x451,x452)
% 58.78/58.97 [46]~P4(x462,x461)+P10(x461,x462)
% 58.78/58.97 [47]~P4(x471,x472)+P6(x471,x472)
% 58.78/58.97 [48]~P10(x482,x481)+P4(x481,x482)
% 58.78/58.97 [53]~P4(x532,x531)+~P4(x531,x532)
% 58.78/58.97 [62]P1(x621)+~P3(x621,x622,x623)
% 58.78/58.97 [58]P2(x581)+P11(x581,f9(x581))+P9(f2(x581,f9(x581)),a3)
% 58.78/58.97 [61]P2(x611)+~P11(x611,f9(x611))+P4(f2(x611,f9(x611)),a3)
% 58.78/58.97 [66]P2(x661)+P9(f2(x661,f9(x661)),a3)+P4(f2(x661,f9(x661)),a3)
% 58.78/58.97 [43]P10(x431,x432)+P4(x431,x432)+E(x431,x432)
% 58.78/58.97 [44]~P1(x441)+P5(x441)+~P7(x441,x442)
% 58.78/58.97 [49]P10(x491,x492)+~P9(x491,x492)+E(x491,x492)
% 58.78/58.97 [50]P4(x501,x502)+~P6(x501,x502)+E(x501,x502)
% 58.78/58.97 [51]~P1(x511)+~P7(x511,x512)+E(f6(x511,x512),a12)
% 58.78/58.97 [52]~P1(x521)+P8(x521,x522)+~E(f2(x521,x522),a11)
% 58.78/58.97 [60]~P2(x601)+P11(x601,x602)+~P9(f2(x601,x602),a3)
% 58.78/58.97 [63]~P2(x631)+~P11(x631,x632)+~P4(f2(x631,x632),a3)
% 58.78/58.97 [54]~P4(x541,x543)+P4(x541,x542)+~P4(x543,x542)
% 58.78/58.97 [67]~P3(x671,x673,x672)+P8(x671,x672)+P8(x671,x673)
% 58.78/58.97 [69]~P3(x691,x693,x692)+~P8(x691,x692)+~P8(x691,x693)
% 58.78/58.97 [64]~P1(x641)+~P8(x641,x643)+P8(x641,x642)+P3(x641,x642,x643)
% 58.78/58.97 [65]~P1(x651)+~P8(x651,x653)+P8(x651,x652)+P3(x651,x653,x652)
% 58.78/58.97 [70]~P1(x701)+P3(x701,x702,x703)+~E(f2(x701,x702),a11)+~P4(f2(x701,x703),a3)
% 58.78/58.97 [71]~P1(x711)+~P3(x711,x713,x712)+P4(f2(x711,x712),a3)+~E(f2(x711,x713),a11)
% 58.78/58.97 [55]P7(x551,x552)+P8(x551,x552)+P11(x551,x552)+~P1(x551)+E(f6(x551,x552),a5)
% 58.78/58.97 [56]P7(x561,x562)+P8(x561,x562)+~P1(x561)+~P11(x561,x562)+E(f6(x561,x562),a7)
% 58.78/58.97 [57]P7(x571,x572)+P11(x571,x572)+~P1(x571)+~P8(x571,x572)+E(f6(x571,x572),a8)
% 58.78/58.97 [59]P7(x591,x592)+~P1(x591)+~P8(x591,x592)+~P11(x591,x592)+E(f6(x591,x592),a4)
% 58.78/58.97 %EqnAxiom
% 58.78/58.97 [1]E(x11,x11)
% 58.78/58.97 [2]E(x22,x21)+~E(x21,x22)
% 58.78/58.97 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.78/58.97 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 58.78/58.97 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 58.78/58.97 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 58.78/58.97 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 58.78/58.97 [8]~E(x81,x82)+E(f9(x81),f9(x82))
% 58.78/58.97 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 58.78/58.97 [10]~P2(x101)+P2(x102)+~E(x101,x102)
% 58.78/58.97 [11]P4(x112,x113)+~E(x111,x112)+~P4(x111,x113)
% 58.78/58.97 [12]P4(x123,x122)+~E(x121,x122)+~P4(x123,x121)
% 58.78/58.97 [13]P8(x132,x133)+~E(x131,x132)+~P8(x131,x133)
% 58.78/58.97 [14]P8(x143,x142)+~E(x141,x142)+~P8(x143,x141)
% 58.78/58.97 [15]P3(x152,x153,x154)+~E(x151,x152)+~P3(x151,x153,x154)
% 58.78/58.97 [16]P3(x163,x162,x164)+~E(x161,x162)+~P3(x163,x161,x164)
% 58.78/58.97 [17]P3(x173,x174,x172)+~E(x171,x172)+~P3(x173,x174,x171)
% 58.78/58.97 [18]P9(x182,x183)+~E(x181,x182)+~P9(x181,x183)
% 58.78/58.97 [19]P9(x193,x192)+~E(x191,x192)+~P9(x193,x191)
% 58.78/58.97 [20]P11(x202,x203)+~E(x201,x202)+~P11(x201,x203)
% 58.78/58.97 [21]P11(x213,x212)+~E(x211,x212)+~P11(x213,x211)
% 58.78/58.97 [22]P6(x222,x223)+~E(x221,x222)+~P6(x221,x223)
% 58.78/58.97 [23]P6(x233,x232)+~E(x231,x232)+~P6(x233,x231)
% 58.78/58.97 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243)
% 58.78/58.97 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251)
% 58.78/58.97 [26]P10(x262,x263)+~E(x261,x262)+~P10(x261,x263)
% 58.78/58.97 [27]P10(x273,x272)+~E(x271,x272)+~P10(x273,x271)
% 58.78/58.97 [28]~P5(x281)+P5(x282)+~E(x281,x282)
% 58.78/58.97
% 58.78/58.97 %-------------------------------------------
% 58.78/58.97 cnf(72,plain,
% 58.78/58.97 (P9(x721,x721)),
% 58.78/58.97 inference(equality_inference,[],[41])).
% 58.78/58.97 cnf(73,plain,
% 58.78/58.97 (P6(x731,x731)),
% 58.78/58.97 inference(equality_inference,[],[42])).
% 58.78/58.97 cnf(74,plain,
% 58.78/58.97 (E(a11,f2(a1,a10))),
% 58.78/58.97 inference(scs_inference,[],[31,2])).
% 58.78/58.97 cnf(75,plain,
% 58.78/58.97 (~P4(a11,a3)),
% 58.78/58.97 inference(scs_inference,[],[32,31,2,53])).
% 58.78/58.97 cnf(77,plain,
% 58.78/58.97 (~P7(a1,x771)),
% 58.78/58.97 inference(scs_inference,[],[29,32,40,31,2,53,44])).
% 58.78/58.97 cnf(79,plain,
% 58.78/58.97 (P8(a1,a10)),
% 58.78/58.97 inference(scs_inference,[],[29,32,40,31,2,53,44,52])).
% 58.78/58.97 cnf(81,plain,
% 58.78/58.97 (P11(a1,a13)),
% 58.78/58.97 inference(scs_inference,[],[29,30,32,40,31,38,2,53,44,52,60])).
% 58.78/58.97 cnf(83,plain,
% 58.78/58.97 (~P11(a1,a14)),
% 58.78/58.97 inference(scs_inference,[],[29,30,32,40,31,38,39,2,53,44,52,60,63])).
% 58.78/58.97 cnf(86,plain,
% 58.78/58.97 (P4(a3,f2(a1,a10))),
% 58.78/58.97 inference(scs_inference,[],[29,30,32,40,31,38,39,2,53,44,52,60,63,11,12])).
% 58.78/58.97 cnf(92,plain,
% 58.78/58.97 (P9(x921,x921)),
% 58.78/58.97 inference(rename_variables,[],[72])).
% 58.78/58.97 cnf(97,plain,
% 58.78/58.97 (P6(x971,x971)),
% 58.78/58.97 inference(rename_variables,[],[73])).
% 58.78/58.97 cnf(100,plain,
% 58.78/58.97 (P3(a1,a10,a14)),
% 58.78/58.97 inference(scs_inference,[],[29,30,32,40,31,38,39,72,92,73,97,2,53,44,52,60,63,11,12,54,69,18,19,21,22,23,70])).
% 58.78/58.97 cnf(102,plain,
% 58.78/58.97 (~P10(a3,a11)),
% 58.78/58.97 inference(scs_inference,[],[29,30,32,40,31,38,39,72,92,73,97,2,53,44,52,60,63,11,12,54,69,18,19,21,22,23,70,48])).
% 58.78/58.97 cnf(104,plain,
% 58.78/58.97 (~E(f2(a1,a14),f2(a1,a10))),
% 58.78/58.97 inference(scs_inference,[],[29,30,32,40,31,38,39,72,92,73,97,2,53,44,52,60,63,11,12,54,69,18,19,21,22,23,70,48,3])).
% 58.78/58.97 cnf(113,plain,
% 58.78/58.97 (~P10(f2(a1,a14),a3)),
% 58.78/58.97 inference(scs_inference,[],[39,53,48])).
% 58.78/58.97 cnf(115,plain,
% 58.78/58.97 (~P4(a11,f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[39,75,53,48,54])).
% 58.78/58.97 cnf(117,plain,
% 58.78/58.97 (~E(a11,f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[32,39,75,53,48,54,12])).
% 58.78/58.97 cnf(125,plain,
% 58.78/58.97 (~P10(f2(a1,a14),a11)),
% 58.78/58.97 inference(scs_inference,[],[115,48])).
% 58.78/58.97 cnf(127,plain,
% 58.78/58.97 (~P4(f2(a1,a10),a3)),
% 58.78/58.97 inference(scs_inference,[],[86,115,48,53])).
% 58.78/58.97 cnf(129,plain,
% 58.78/58.97 (P4(f2(a1,a14),f2(a1,a10))),
% 58.78/58.97 inference(scs_inference,[],[39,86,115,48,53,54])).
% 58.78/58.97 cnf(131,plain,
% 58.78/58.97 (P10(a11,f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[39,86,115,117,48,53,54,43])).
% 58.78/58.97 cnf(142,plain,
% 58.78/58.97 (~P4(f2(a1,a10),f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[129,53])).
% 58.78/58.97 cnf(146,plain,
% 58.78/58.97 (P4(a7,a12)),
% 58.78/58.97 inference(scs_inference,[],[129,127,33,34,53,48,54])).
% 58.78/58.97 cnf(150,plain,
% 58.78/58.97 (E(f2(a1,a14),a3)+~E(f2(a1,a13),f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[38,30,83,113,129,127,33,34,53,48,54,18,60,49])).
% 58.78/58.97 cnf(163,plain,
% 58.78/58.97 (~P4(a4,a8)),
% 58.78/58.97 inference(scs_inference,[],[142,35,48,53])).
% 58.78/58.97 cnf(165,plain,
% 58.78/58.97 (P4(a5,a4)),
% 58.78/58.97 inference(scs_inference,[],[142,35,37,48,53,54])).
% 58.78/58.97 cnf(167,plain,
% 58.78/58.97 (~E(a5,a4)),
% 58.78/58.97 inference(scs_inference,[],[142,35,37,48,53,54,11])).
% 58.78/58.97 cnf(168,plain,
% 58.78/58.97 (~E(a12,a8)),
% 58.78/58.97 inference(scs_inference,[],[142,35,37,33,48,53,54,11,12])).
% 58.78/58.97 cnf(172,plain,
% 58.78/58.97 (P11(x1721,a13)+~E(a1,x1721)),
% 58.78/58.97 inference(scs_inference,[],[38,81,100,131,142,35,37,33,48,53,54,11,12,19,27,15,20])).
% 58.78/58.97 cnf(180,plain,
% 58.78/58.97 (~P4(a7,a5)),
% 58.78/58.97 inference(scs_inference,[],[36,53])).
% 58.78/58.97 cnf(184,plain,
% 58.78/58.97 (P4(a5,a12)),
% 58.78/58.97 inference(scs_inference,[],[36,146,163,53,48,54])).
% 58.78/58.97 cnf(186,plain,
% 58.78/58.97 (~E(a12,a5)),
% 58.78/58.97 inference(scs_inference,[],[36,146,163,53,48,54,12])).
% 58.78/58.97 cnf(195,plain,
% 58.78/58.97 (~P4(a8,a5)),
% 58.78/58.97 inference(scs_inference,[],[37,180,48,53])).
% 58.78/58.97 cnf(197,plain,
% 58.78/58.97 (~P4(a4,a5)),
% 58.78/58.97 inference(scs_inference,[],[37,180,163,48,53,54])).
% 58.78/58.97 cnf(199,plain,
% 58.78/58.97 (~E(a4,a5)),
% 58.78/58.97 inference(scs_inference,[],[37,180,163,34,48,53,54,12])).
% 58.78/58.97 cnf(208,plain,
% 58.78/58.97 (~P4(a12,a5)),
% 58.78/58.97 inference(scs_inference,[],[184,53])).
% 58.78/58.97 cnf(212,plain,
% 58.78/58.97 (P10(a4,a5)),
% 58.78/58.97 inference(scs_inference,[],[184,195,197,199,53,48,43])).
% 58.78/58.97 cnf(223,plain,
% 58.78/58.97 (P10(a12,a5)),
% 58.78/58.97 inference(scs_inference,[],[186,208,33,48,53,43])).
% 58.78/58.97 cnf(225,plain,
% 58.78/58.97 (~E(a5,a12)),
% 58.78/58.97 inference(scs_inference,[],[165,186,208,33,48,53,43,11])).
% 58.78/58.97 cnf(231,plain,
% 58.78/58.97 (~P4(a4,a7)),
% 58.78/58.97 inference(scs_inference,[],[34,53])).
% 58.78/58.97 cnf(243,plain,
% 58.78/58.97 (~P4(a12,a7)),
% 58.78/58.97 inference(scs_inference,[],[197,146,48,53])).
% 58.78/58.97 cnf(272,plain,
% 58.78/58.97 (~P10(a7,a4)),
% 58.78/58.97 inference(scs_inference,[],[231,48])).
% 58.78/58.97 cnf(276,plain,
% 58.78/58.97 (E(a3,a11)+P10(a11,a3)),
% 58.78/58.97 inference(scs_inference,[],[75,231,48,43,2])).
% 58.78/58.97 cnf(295,plain,
% 58.78/58.97 (P9(f2(a1,a10),f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[131,74,45,18])).
% 58.78/58.97 cnf(296,plain,
% 58.78/58.97 (P9(a11,f2(a1,a14))),
% 58.78/58.97 inference(scs_inference,[],[31,295,18])).
% 58.78/58.97 cnf(303,plain,
% 58.78/58.97 (P10(x3031,a5)+~E(a4,x3031)),
% 58.78/58.97 inference(scs_inference,[],[212,296,19,26])).
% 58.78/58.97 cnf(329,plain,
% 58.78/58.97 (P10(a8,a5)+P10(a4,a8)),
% 58.78/58.97 inference(scs_inference,[],[212,163,43,26])).
% 58.78/58.97 cnf(331,plain,
% 58.78/58.97 (P10(a4,a8)+~E(a12,a4)),
% 58.78/58.97 inference(scs_inference,[],[212,163,168,43,26,2,3])).
% 58.78/58.97 cnf(357,plain,
% 58.78/58.97 (P4(x3571,a12)+~E(a4,x3571)),
% 58.78/58.97 inference(scs_inference,[],[33,11])).
% 58.78/58.97 cnf(389,plain,
% 58.78/58.97 (P4(a5,x3891)+~E(a4,x3891)),
% 58.78/58.97 inference(scs_inference,[],[165,12])).
% 58.78/58.97 cnf(407,plain,
% 58.78/58.97 (~E(a12,a7)),
% 58.78/58.97 inference(scs_inference,[],[33,231,12])).
% 58.78/58.97 cnf(419,plain,
% 58.78/58.97 (P9(a11,a3)+E(a3,a11)),
% 58.78/58.97 inference(scs_inference,[],[276,45])).
% 58.78/58.97 cnf(423,plain,
% 58.78/58.97 (P9(a4,a8)+P10(a8,a5)),
% 58.78/58.97 inference(scs_inference,[],[329,45])).
% 58.78/58.97 cnf(425,plain,
% 58.78/58.97 (P9(a4,a8)+~E(a12,a4)),
% 58.78/58.97 inference(scs_inference,[],[331,45])).
% 58.78/58.97 cnf(434,plain,
% 58.78/58.97 (P9(f2(a1,a10),a3)+E(a3,a11)),
% 58.78/58.97 inference(scs_inference,[],[74,419,18])).
% 58.78/58.97 cnf(438,plain,
% 58.78/58.97 (P9(a8,a5)+P9(a4,a8)),
% 58.78/58.97 inference(scs_inference,[],[423,45])).
% 58.78/58.97 cnf(441,plain,
% 58.78/58.97 (P9(x4411,a8)+~E(a4,x4411)+~E(a12,a4)),
% 58.78/58.97 inference(scs_inference,[],[425,18])).
% 58.78/58.97 cnf(451,plain,
% 58.78/58.97 (P9(x4511,a8)+~E(a4,x4511)+P9(a8,a5)),
% 58.78/58.97 inference(scs_inference,[],[438,18])).
% 58.78/58.97 cnf(472,plain,
% 58.78/58.97 (P11(a1,a10)+E(a3,a11)),
% 58.78/58.97 inference(scs_inference,[],[30,434,60])).
% 58.78/58.97 cnf(473,plain,
% 58.78/58.97 (E(a3,a11)+E(f6(a1,a10),a4)),
% 58.78/58.97 inference(scs_inference,[],[29,79,77,472,59])).
% 58.78/58.97 cnf(489,plain,
% 58.78/58.97 (E(f2(f6(a1,a10),x4891),f2(a4,x4891))+E(a3,a11)),
% 58.78/58.97 inference(scs_inference,[],[473,4])).
% 58.78/58.97 cnf(782,plain,
% 58.78/58.97 (E(f2(x7821,a11),f2(x7821,f2(a1,a10)))),
% 58.78/58.97 inference(scs_inference,[],[31,2,5])).
% 58.78/58.97 cnf(783,plain,
% 58.78/58.97 (E(f2(x7831,f2(a1,a10)),f2(x7831,a11))),
% 58.78/58.97 inference(scs_inference,[],[782,2])).
% 58.78/58.97 cnf(906,plain,
% 58.78/58.97 (E(f6(a11,x9061),f6(f2(a1,a10),x9061))),
% 58.78/58.97 inference(scs_inference,[],[31,2,6])).
% 58.78/58.97 cnf(907,plain,
% 58.78/58.97 (E(f6(f2(a1,a10),x9071),f6(a11,x9071))),
% 58.78/58.97 inference(scs_inference,[],[906,2])).
% 58.78/58.97 cnf(942,plain,
% 58.78/58.97 (P6(x9421,x9421)),
% 58.78/58.97 inference(rename_variables,[],[73])).
% 58.78/58.97 cnf(945,plain,
% 58.78/58.97 (P9(f2(x9451,f2(a1,a10)),f2(x9451,a11))),
% 58.78/58.97 inference(scs_inference,[],[782,73,942,72,22,23,18])).
% 58.78/58.98 cnf(989,plain,
% 58.78/58.98 (E(f6(x9891,a11),f6(x9891,f2(a1,a10)))),
% 58.78/58.98 inference(scs_inference,[],[31,2,7])).
% 58.78/58.98 cnf(990,plain,
% 58.78/58.98 (E(f6(x9901,f2(a1,a10)),f6(x9901,a11))),
% 58.78/58.98 inference(scs_inference,[],[989,2])).
% 58.78/58.98 cnf(991,plain,
% 58.78/58.98 (E(f6(f2(a1,a10),a11),f6(a11,f2(a1,a10)))),
% 58.78/58.98 inference(scs_inference,[],[907,989,2,3])).
% 58.78/58.98 cnf(1002,plain,
% 58.78/58.98 (E(f6(f2(a1,a10),f2(a1,a10)),f6(a11,a11))),
% 58.78/58.98 inference(scs_inference,[],[907,990,991,2,3])).
% 58.78/58.98 cnf(1011,plain,
% 58.78/58.98 (E(f6(a11,a11),f6(f2(a1,a10),f2(a1,a10)))),
% 58.78/58.98 inference(scs_inference,[],[1002,2])).
% 58.78/58.98 cnf(1165,plain,
% 58.78/58.98 (~P9(f2(a1,a14),a11)),
% 58.78/58.98 inference(scs_inference,[],[117,125,2,49])).
% 58.78/58.98 cnf(1166,plain,
% 58.78/58.98 (~P6(f2(a1,a10),f2(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[104,142,2,50])).
% 58.78/58.98 cnf(1167,plain,
% 58.78/58.98 (P8(a1,a14)+E(a5,f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[83,29,77,2,55])).
% 58.78/58.98 cnf(1178,plain,
% 58.78/58.98 (~P8(a1,a13)+E(a4,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[81,29,77,2,59])).
% 58.78/58.98 cnf(1190,plain,
% 58.78/58.98 (~E(f2(a1,a14),a3)),
% 58.78/58.98 inference(scs_inference,[],[30,83,41,60])).
% 58.78/58.98 cnf(1191,plain,
% 58.78/58.98 (~E(f2(a1,a13),f2(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[1190,150])).
% 58.78/58.98 cnf(1193,plain,
% 58.78/58.98 (P9(f6(a1,a14),a5)+P8(a1,a14)),
% 58.78/58.98 inference(scs_inference,[],[83,29,77,41,55])).
% 58.78/58.98 cnf(1222,plain,
% 58.78/58.98 (P9(f6(a1,a13),a4)+~P8(a1,a13)),
% 58.78/58.98 inference(scs_inference,[],[81,29,77,41,59])).
% 58.78/58.98 cnf(1231,plain,
% 58.78/58.98 (P6(f6(a1,a14),a5)+P8(a1,a14)),
% 58.78/58.98 inference(scs_inference,[],[83,29,77,42,55])).
% 58.78/58.98 cnf(1253,plain,
% 58.78/58.98 (P6(f6(a1,a13),a4)+~P8(a1,a13)),
% 58.78/58.98 inference(scs_inference,[],[81,29,77,42,59])).
% 58.78/58.98 cnf(1355,plain,
% 58.78/58.98 (P6(a5,a12)),
% 58.78/58.98 inference(scs_inference,[],[223,48,47])).
% 58.78/58.98 cnf(1372,plain,
% 58.78/58.98 (~P9(a3,f2(a1,a10))+E(a3,f2(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[127,48,49])).
% 58.78/58.98 cnf(1373,plain,
% 58.78/58.98 (E(a3,a11)+~P9(a3,f2(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[31,1372,3])).
% 58.78/58.98 cnf(1374,plain,
% 58.78/58.98 (P4(a11,a11)+~P9(a3,f2(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[32,1373,11])).
% 58.78/58.98 cnf(1390,plain,
% 58.78/58.98 (~P9(a3,f2(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[53,1374])).
% 58.78/58.98 cnf(1391,plain,
% 58.78/58.98 (~E(a3,f2(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1390,41])).
% 58.78/58.98 cnf(1421,plain,
% 58.78/58.98 (~E(a3,a11)),
% 58.78/58.98 inference(scs_inference,[],[1391,74,3])).
% 58.78/58.98 cnf(1422,plain,
% 58.78/58.98 (E(f6(a1,a10),a4)),
% 58.78/58.98 inference(scs_inference,[],[1391,74,3,473])).
% 58.78/58.98 cnf(1423,plain,
% 58.78/58.98 (E(f2(f6(a1,a10),x14231),f2(a4,x14231))),
% 58.78/58.98 inference(scs_inference,[],[1391,74,3,473,489])).
% 58.78/58.98 cnf(1424,plain,
% 58.78/58.98 (E(a4,f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1391,74,3,473,489,2])).
% 58.78/58.98 cnf(1427,plain,
% 58.78/58.98 (P4(f6(a1,a10),a12)),
% 58.78/58.98 inference(scs_inference,[],[1391,74,33,3,473,489,2,441,11])).
% 58.78/58.98 cnf(1428,plain,
% 58.78/58.98 (P10(f6(a1,a10),a5)),
% 58.78/58.98 inference(scs_inference,[],[1391,74,33,212,3,473,489,2,441,11,26])).
% 58.78/58.98 cnf(1429,plain,
% 58.78/58.98 (P4(a5,f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1391,74,33,165,212,3,473,489,2,441,11,26,12])).
% 58.78/58.98 cnf(1439,plain,
% 58.78/58.98 (~P4(f6(a1,a10),a5)),
% 58.78/58.98 inference(scs_inference,[],[1429,53])).
% 58.78/58.98 cnf(1441,plain,
% 58.78/58.98 (~P10(a5,f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1429,53,48])).
% 58.78/58.98 cnf(1443,plain,
% 58.78/58.98 (E(f2(a4,x14431),f2(f6(a1,a10),x14431))),
% 58.78/58.98 inference(scs_inference,[],[1423,1429,53,48,2])).
% 58.78/58.98 cnf(1444,plain,
% 58.78/58.98 (E(f2(f6(a1,a10),f2(a1,a10)),f2(a4,a11))),
% 58.78/58.98 inference(scs_inference,[],[783,1423,1429,53,48,2,3])).
% 58.78/58.98 cnf(1455,plain,
% 58.78/58.98 (E(f2(a4,f2(a1,a10)),f2(f6(a1,a10),a11))),
% 58.78/58.98 inference(scs_inference,[],[783,1443,1444,2,3])).
% 58.78/58.98 cnf(1462,plain,
% 58.78/58.98 (~E(a5,f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[167,1422,1455,2,3])).
% 58.78/58.98 cnf(1675,plain,
% 58.78/58.98 (~P8(a1,a13)+E(f6(a1,a13),a4)),
% 58.78/58.98 inference(scs_inference,[],[100,81,77,62,59])).
% 58.78/58.98 cnf(1733,plain,
% 58.78/58.98 (~P4(f2(a1,a13),a3)),
% 58.78/58.98 inference(scs_inference,[],[30,172,63])).
% 58.78/58.98 cnf(1736,plain,
% 58.78/58.98 (~P4(f2(a1,a13),f2(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[39,1733,48,54])).
% 58.78/58.98 cnf(1738,plain,
% 58.78/58.98 (~E(f2(a1,a14),f2(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[39,1733,48,54,11])).
% 58.78/58.98 cnf(1742,plain,
% 58.78/58.98 (P10(f2(a1,a13),f2(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[31,39,29,1733,1191,48,54,11,71,5,43])).
% 58.78/58.98 cnf(1745,plain,
% 58.78/58.98 (P8(a1,a13)),
% 58.78/58.98 inference(scs_inference,[],[31,39,29,79,1733,1191,48,54,11,71,5,43,27,65])).
% 58.78/58.98 cnf(1759,plain,
% 58.78/58.98 (E(a4,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1745,1178])).
% 58.78/58.98 cnf(1760,plain,
% 58.78/58.98 (P9(f6(a1,a13),a4)),
% 58.78/58.98 inference(scs_inference,[],[1745,1222])).
% 58.78/58.98 cnf(1761,plain,
% 58.78/58.98 (P6(f6(a1,a13),a4)),
% 58.78/58.98 inference(scs_inference,[],[1745,1253])).
% 58.78/58.98 cnf(1762,plain,
% 58.78/58.98 (E(f6(a1,a13),a4)),
% 58.78/58.98 inference(scs_inference,[],[1745,1675])).
% 58.78/58.98 cnf(1764,plain,
% 58.78/58.98 (P4(f6(a1,a13),a12)),
% 58.78/58.98 inference(scs_inference,[],[1759,357])).
% 58.78/58.98 cnf(1765,plain,
% 58.78/58.98 (P4(a5,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1759,357,389])).
% 58.78/58.98 cnf(1766,plain,
% 58.78/58.98 (P10(f6(a1,a13),a5)),
% 58.78/58.98 inference(scs_inference,[],[1759,357,389,303])).
% 58.78/58.98 cnf(1769,plain,
% 58.78/58.98 (~P10(f2(a1,a14),f2(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1759,1736,357,389,303,53,48])).
% 58.78/58.98 cnf(1771,plain,
% 58.78/58.98 (~E(a5,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1762,1759,167,1736,357,389,303,53,48,3])).
% 58.78/58.98 cnf(1778,plain,
% 58.78/58.98 (E(f6(a1,a13),f6(a1,a10))+P4(f6(a1,a13),f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1424,1762,1761,1760,1759,167,1736,357,389,303,53,48,3,23,19,451,22,18,50])).
% 58.78/58.98 cnf(1780,plain,
% 58.78/58.98 (E(f6(a1,a13),f6(a1,a10))+P10(f6(a1,a13),f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1424,1762,1761,1760,1759,167,1736,357,389,303,53,48,3,23,19,451,22,18,50,49])).
% 58.78/58.98 cnf(1790,plain,
% 58.78/58.98 (~P4(f6(a1,a13),a5)),
% 58.78/58.98 inference(scs_inference,[],[1765,53])).
% 58.78/58.98 cnf(1799,plain,
% 58.78/58.98 (~P10(a5,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1790,48])).
% 58.78/58.98 cnf(1923,plain,
% 58.78/58.98 (P6(f2(a4,x19231),f2(f6(a1,a10),x19231))),
% 58.78/58.98 inference(scs_inference,[],[1443,1759,8,4,6,7,42])).
% 58.78/58.98 cnf(1929,plain,
% 58.78/58.98 (P10(a12,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1766,1764,1443,1759,8,4,6,7,42,47,45,46])).
% 58.78/58.98 cnf(1934,plain,
% 58.78/58.98 (P4(f2(a1,a14),f2(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[1766,1764,1742,1443,1759,8,4,6,7,42,47,45,46,41,5,48])).
% 58.78/58.98 cnf(1942,plain,
% 58.78/58.98 (~P6(f6(a1,a10),a5)),
% 58.78/58.98 inference(scs_inference,[],[30,1462,1766,1764,1742,1439,199,1443,1759,83,100,79,8,4,6,7,42,47,45,46,41,5,48,2,69,60,3,50])).
% 58.78/58.98 cnf(1944,plain,
% 58.78/58.98 (~P9(a5,f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[30,1462,1771,1799,1766,1764,1742,1439,199,1443,1759,83,100,79,8,4,6,7,42,47,45,46,41,5,48,2,69,60,3,50,49])).
% 58.78/58.98 cnf(1954,plain,
% 58.78/58.98 (E(f6(a1,a14),a5)),
% 58.78/58.98 inference(scs_inference,[],[30,1462,1771,1799,1766,1764,272,1742,1439,199,1165,1166,1745,231,1443,1759,1762,83,77,74,100,29,79,31,8,4,6,7,42,47,45,46,41,5,48,2,69,60,3,50,49,27,11,22,19,64,65,55])).
% 58.78/58.98 cnf(1957,plain,
% 58.78/58.98 (E(a5,f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[30,1462,1771,1799,1766,1764,272,1742,1439,199,1165,1166,1745,231,1443,1759,1762,83,77,74,100,29,79,31,8,4,6,7,42,47,45,46,41,5,48,2,69,60,3,50,49,27,11,22,19,64,65,55,1167])).
% 58.78/58.98 cnf(1961,plain,
% 58.78/58.98 (~P10(f6(a1,a14),f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[30,1462,1771,1799,1766,1764,272,1742,1439,199,1165,1166,1745,1011,231,1443,1759,1762,83,77,74,100,29,79,31,8,4,6,7,42,47,45,46,41,5,48,2,69,60,3,50,49,27,11,22,19,64,65,55,1167,1193,1231,24,26])).
% 58.78/58.98 cnf(1962,plain,
% 58.78/58.98 (~P4(f6(a1,a10),f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[30,1462,1771,1799,1766,1764,272,1742,1439,199,1165,1166,1745,1011,231,1443,1759,1762,83,77,74,100,29,79,31,8,4,6,7,42,47,45,46,41,5,48,2,69,60,3,50,49,27,11,22,19,64,65,55,1167,1193,1231,24,26,12])).
% 58.78/58.98 cnf(1973,plain,
% 58.78/58.98 (E(f2(a5,x19731),f2(f6(a1,a14),x19731))),
% 58.78/58.98 inference(scs_inference,[],[1934,1957,47,4])).
% 58.78/58.98 cnf(1980,plain,
% 58.78/58.98 (P10(a12,f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1929,1934,1957,1427,47,4,6,42,45,8,46])).
% 58.78/58.98 cnf(1985,plain,
% 58.78/58.98 (E(f2(x19851,a5),f2(x19851,f6(a1,a14)))),
% 58.78/58.98 inference(scs_inference,[],[1929,1934,1957,1427,47,4,6,42,45,8,46,7,41,5])).
% 58.78/58.98 cnf(1987,plain,
% 58.78/58.98 (~E(f6(a1,a14),a12)),
% 58.78/58.98 inference(scs_inference,[],[1929,1190,1934,1957,1427,225,47,4,6,42,45,8,46,7,41,5,2,3])).
% 58.78/58.98 cnf(1992,plain,
% 58.78/58.98 (~P4(a12,f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[407,1929,1190,1962,1934,1957,1738,1769,1427,225,243,47,4,6,42,45,8,46,7,41,5,2,3,50,49,54])).
% 58.78/58.98 cnf(1996,plain,
% 58.78/58.98 (P4(f6(a1,a14),f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[407,1929,1190,1961,1962,1934,1957,1738,1769,1441,1427,225,1954,1765,243,1759,47,4,6,42,45,8,46,7,41,5,2,3,50,49,54,27,26,11])).
% 58.78/58.98 cnf(1998,plain,
% 58.78/58.98 (~P4(f6(a1,a13),f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[407,1929,1190,1961,1962,1934,1957,1738,1769,1441,1427,225,1954,1765,1790,243,1355,1759,47,4,6,42,45,8,46,7,41,5,2,3,50,49,54,27,26,11,22,12])).
% 58.78/58.98 cnf(1999,plain,
% 58.78/58.98 (~P6(f6(a1,a10),f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[407,1929,1190,1961,1962,1934,1957,1942,1738,1769,1441,1427,225,1954,1765,1790,243,1355,1759,47,4,6,42,45,8,46,7,41,5,2,3,50,49,54,27,26,11,22,12,23])).
% 58.78/58.98 cnf(2000,plain,
% 58.78/58.98 (~P9(f6(a1,a14),f6(a1,a13))),
% 58.78/58.98 inference(scs_inference,[],[407,1929,1190,1961,1962,1934,1957,1944,1942,1738,1769,1441,1427,225,1954,1765,1790,243,1355,1759,47,4,6,42,45,8,46,7,41,5,2,3,50,49,54,27,26,11,22,12,23,18])).
% 58.78/58.98 cnf(2010,plain,
% 58.78/58.98 (~E(f6(a1,a13),f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1996,68])).
% 58.78/58.98 cnf(2018,plain,
% 58.78/58.98 (E(f2(f6(a1,a14),x20181),f2(a5,x20181))),
% 58.78/58.98 inference(scs_inference,[],[1996,1954,47,4])).
% 58.78/58.98 cnf(2024,plain,
% 58.78/58.98 (E(f9(f6(a1,a14)),f9(a5))),
% 58.78/58.98 inference(scs_inference,[],[1980,1996,1973,1954,47,4,6,45,42,8])).
% 58.78/58.98 cnf(2025,plain,
% 58.78/58.98 (P10(f6(a1,a13),f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[1980,1996,1973,1954,47,4,6,45,42,8,46])).
% 58.78/58.98 cnf(2033,plain,
% 58.78/58.98 (E(f2(a5,x20331),f2(f6(a1,a14),x20331))),
% 58.78/58.98 inference(rename_variables,[],[1973])).
% 58.78/58.98 cnf(2034,plain,
% 58.78/58.98 (E(f2(x20341,a5),f2(x20341,f6(a1,a14)))),
% 58.78/58.98 inference(rename_variables,[],[1985])).
% 58.78/58.98 cnf(2039,plain,
% 58.78/58.98 (P4(f6(a1,a14),a12)),
% 58.78/58.98 inference(scs_inference,[],[1421,1980,1996,1987,1992,1973,1985,1764,102,1954,47,4,6,45,42,8,46,7,41,5,2,3,50,49,54])).
% 58.78/58.98 cnf(2051,plain,
% 58.78/58.98 (P4(f6(a1,a14),f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[1421,1980,1998,1996,2000,1999,1987,1992,1973,2033,1985,2034,1923,1428,945,1764,102,1954,1957,1759,1424,47,4,6,45,42,8,46,7,41,5,2,3,50,49,54,27,11,22,23,18,19,48])).
% 58.78/58.98 cnf(2058,plain,
% 58.78/58.98 (P4(f6(a1,a13),f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[2010,1778])).
% 58.78/58.98 cnf(2059,plain,
% 58.78/58.98 (P10(f6(a1,a13),f6(a1,a10))),
% 58.78/58.98 inference(scs_inference,[],[2010,1780])).
% 58.78/58.98 cnf(2068,plain,
% 58.78/58.98 (P10(a12,f6(a1,a14))),
% 58.78/58.98 inference(scs_inference,[],[2025,2051,2039,2018,1762,47,4,6,42,45,46])).
% 58.78/58.98 cnf(2118,plain,
% 58.78/58.98 ($false),
% 58.78/58.98 inference(scs_inference,[],[2058,2059,2068,2024,1429,35,1422,47,6,46,45,42,8,7,41,5,53,48]),
% 58.78/58.98 ['proof']).
% 58.78/58.98 % SZS output end Proof
% 58.78/58.98 % Total time :58.450660s
%------------------------------------------------------------------------------