%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT062-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:22 AM UTC 2026
% Result : Unsatisfiable 128.75s 128.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT062-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.01 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 7 13:38:41 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.09/0.38 start to proof:theBenchmark
% 128.65/128.90 %-------------------------------------------
% 128.65/128.90 % File :CSE---1.7
% 128.65/128.90 % Problem :theBenchmark
% 128.65/128.90 % Transform :cnf
% 128.65/128.90 % Format :tptp:raw
% 128.65/128.90 % Command :java -jar mcs_scs.jar %d %s
% 128.65/128.90
% 128.65/128.90 % Result :Theorem 128.502970s
% 128.65/128.90 % Output :CNFRefutation 128.502970s
% 128.65/128.90 %-------------------------------------------
% 128.75/128.90 %--------------------------------------------------------------------------
% 128.75/128.90 % File : MGT062-1 : TPTP v9.3.0. Released v2.4.0.
% 128.75/128.90 % Domain : Management (Organisation Theory)
% 128.75/128.90 % Problem : Condictions for decreasing hazard of mortality
% 128.75/128.90 % Version : [Han98] axioms.
% 128.75/128.90 % English : If environmental drift destroys alignment exactly when advantage
% 128.75/128.90 % can be gained from occupancy of a robust position, then the
% 128.75/128.90 % hazard of mortality for an unendowed organization with a robust
% 128.75/128.90 % position decreases with age.
% 128.75/128.90
% 128.75/128.90 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 128.75/128.90 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 128.75/128.90 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 128.75/128.90 % Source : [TPTP]
% 128.75/128.90 % Names :
% 128.75/128.90
% 128.75/128.90 % Status : Unsatisfiable
% 128.75/128.90 % Rating : 0.17 v9.3.0, 0.18 v9.1.0, 0.10 v9.0.0, 0.20 v8.2.0, 0.14 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.18 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.10 v5.5.0, 0.30 v5.4.0, 0.35 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.35 v5.0.0, 0.21 v4.1.0, 0.23 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.31 v3.1.0, 0.18 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.44 v2.4.0
% 128.75/128.90 % Syntax : Number of clauses : 44 ( 10 unt; 16 nHn; 36 RR)
% 128.75/128.90 % Number of literals : 117 ( 16 equ; 55 neg)
% 128.75/128.90 % Maximal clause size : 5 ( 2 avg)
% 128.75/128.90 % Maximal term depth : 3 ( 1 avg)
% 128.75/128.90 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty)
% 128.75/128.90 % Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% 128.75/128.90 % Number of variables : 72 ( 5 sgn)
% 128.75/128.90 % SPC : CNF_UNS_RFO_SEQ_NHN
% 128.75/128.90
% 128.75/128.90 % Comments : See MGT042+1.p for the mnemonic names.
% 128.75/128.90 % : Created with tptp2X -f tptp -t clausify:otter MGT062+1.p
% 128.75/128.90 %--------------------------------------------------------------------------
% 128.75/128.90 include('Axioms/MGT001-0.ax').
% 128.75/128.90 %--------------------------------------------------------------------------
% 128.75/128.90 cnf(assumption_1_39,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | has_endowment(A)
% 128.75/128.90 | ~ has_immunity(A,B) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_40,axiom,
% 128.75/128.90 ( ~ dissimilar(A,B,C)
% 128.75/128.90 | organization(A) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_41,axiom,
% 128.75/128.90 ( ~ dissimilar(A,B,C)
% 128.75/128.90 | is_aligned(A,B)
% 128.75/128.90 | is_aligned(A,C) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_42,axiom,
% 128.75/128.90 ( ~ dissimilar(A,B,C)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | ~ is_aligned(A,C) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_43,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | is_aligned(A,B)
% 128.75/128.90 | dissimilar(A,B,C) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_44,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | is_aligned(A,C)
% 128.75/128.90 | dissimilar(A,B,C) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_45,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | is_aligned(A,C)
% 128.75/128.90 | dissimilar(A,C,B) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_2_46,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | is_aligned(A,B)
% 128.75/128.90 | dissimilar(A,C,B) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_13_47,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | age(A,B) != zero
% 128.75/128.90 | is_aligned(A,B) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_15_48,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | age(A,B) != zero
% 128.75/128.90 | ~ greater(age(A,C),sigma)
% 128.75/128.90 | dissimilar(A,B,C) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_15_49,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | age(A,B) != zero
% 128.75/128.90 | ~ dissimilar(A,B,C)
% 128.75/128.90 | greater(age(A,C),sigma) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_4_50,axiom,
% 128.75/128.90 ( ~ robust_position(A)
% 128.75/128.90 | ~ smaller_or_equal(age(A,B),tau)
% 128.75/128.90 | ~ positional_advantage(A,B) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_4_51,axiom,
% 128.75/128.90 ( ~ robust_position(A)
% 128.75/128.90 | ~ greater(age(A,B),tau)
% 128.75/128.90 | positional_advantage(A,B) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_4_52,axiom,
% 128.75/128.90 ( smaller_or_equal(age(A,sk1(A)),tau)
% 128.75/128.90 | greater(age(A,sk1(A)),tau)
% 128.75/128.90 | robust_position(A) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_4_53,axiom,
% 128.75/128.90 ( smaller_or_equal(age(A,sk1(A)),tau)
% 128.75/128.90 | ~ positional_advantage(A,sk1(A))
% 128.75/128.90 | robust_position(A) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_4_54,axiom,
% 128.75/128.90 ( positional_advantage(A,sk1(A))
% 128.75/128.90 | greater(age(A,sk1(A)),tau)
% 128.75/128.90 | robust_position(A) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(definition_4_55,axiom,
% 128.75/128.90 ( positional_advantage(A,sk1(A))
% 128.75/128.90 | ~ positional_advantage(A,sk1(A))
% 128.75/128.90 | robust_position(A) ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_17_56,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | ~ has_immunity(A,B)
% 128.75/128.90 | hazard_of_mortality(A,B) = very_low ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_17_57,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | has_immunity(A,B)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | ~ positional_advantage(A,B)
% 128.75/128.90 | hazard_of_mortality(A,B) = low ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_17_58,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | has_immunity(A,B)
% 128.75/128.90 | is_aligned(A,B)
% 128.75/128.90 | ~ positional_advantage(A,B)
% 128.75/128.90 | hazard_of_mortality(A,B) = mod1 ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_17_59,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | has_immunity(A,B)
% 128.75/128.90 | ~ is_aligned(A,B)
% 128.75/128.90 | positional_advantage(A,B)
% 128.75/128.90 | hazard_of_mortality(A,B) = mod2 ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_17_60,axiom,
% 128.75/128.90 ( ~ organization(A)
% 128.75/128.90 | has_immunity(A,B)
% 128.75/128.90 | is_aligned(A,B)
% 128.75/128.90 | positional_advantage(A,B)
% 128.75/128.90 | hazard_of_mortality(A,B) = high ) ).
% 128.75/128.90
% 128.75/128.90 cnf(assumption_19_61,axiom,
% 128.75/128.90 greater(mod2,mod1) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_62,negated_conjecture,
% 128.75/128.90 organization(sk2) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_63,negated_conjecture,
% 128.75/128.90 robust_position(sk2) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_64,negated_conjecture,
% 128.75/128.90 ~ has_endowment(sk2) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_65,negated_conjecture,
% 128.75/128.90 age(sk2,sk3) = zero ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_66,negated_conjecture,
% 128.75/128.90 greater(sigma,zero) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_67,negated_conjecture,
% 128.75/128.90 greater(tau,zero) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_68,negated_conjecture,
% 128.75/128.90 sigma = tau ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_69,negated_conjecture,
% 128.75/128.90 smaller_or_equal(age(sk2,sk4),sigma) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_70,negated_conjecture,
% 128.75/128.90 greater(age(sk2,sk5),sigma) ).
% 128.75/128.90
% 128.75/128.90 cnf(theorem_8_71,negated_conjecture,
% 128.75/128.90 ( ~ smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
% 128.75/128.90 | hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ).
% 128.75/128.90
% 128.75/128.90 %--------------------------------------------------------------------------
% 128.75/128.90 %-------------------------------------------
% 128.75/128.90 % Proof found
% 128.75/128.90 % SZS status Theorem for theBenchmark
% 128.75/128.90 % SZS output start Proof
% 128.75/128.90 %ClaNum:69(EqnAxiom:28)
% 128.75/128.90 %VarNum:177(SingletonVarNum:65)
% 128.75/128.90 %MaxLitNum:5
% 128.75/128.90 %MaxfuncDepth:2
% 128.75/128.90 %SharedTerms:30
% 128.75/128.90 %goalClause: 29 30 31 32 33 34 36 37 38 66
% 128.75/128.90 %singleGoalClaCount:9
% 128.75/128.90 [29]E(a1,a2)
% 128.75/128.90 [30]P1(a9)
% 128.75/128.90 [31]P8(a9)
% 128.75/128.90 [33]P2(a2,a14)
% 128.75/128.90 [34]P2(a1,a14)
% 128.75/128.90 [35]P2(a4,a5)
% 128.75/128.90 [38]~P4(a9)
% 128.75/128.90 [32]E(f3(a9,a11),a14)
% 128.75/128.90 [36]P10(f3(a9,a12),a2)
% 128.75/128.90 [37]P2(f3(a9,a13),a2)
% 128.75/128.90 [66]~P11(f6(a9,a13),f6(a9,a12))+~E(f6(a9,a12),f6(a9,a11))
% 128.75/128.90 [39]~E(x391,x392)+P10(x391,x392)
% 128.75/128.90 [40]~E(x401,x402)+P5(x401,x402)
% 128.75/128.90 [43]~P11(x431,x432)+P10(x431,x432)
% 128.75/128.90 [44]~P2(x442,x441)+P11(x441,x442)
% 128.75/128.90 [45]~P2(x451,x452)+P5(x451,x452)
% 128.75/128.90 [46]~P11(x462,x461)+P2(x461,x462)
% 128.75/128.90 [51]~P2(x512,x511)+~P2(x511,x512)
% 128.75/128.90 [60]P1(x601)+~P3(x601,x602,x603)
% 128.75/128.90 [56]P8(x561)+P9(x561,f10(x561))+P2(f3(x561,f10(x561)),a1)
% 128.75/128.90 [59]P8(x591)+~P9(x591,f10(x591))+P10(f3(x591,f10(x591)),a1)
% 128.75/128.90 [64]P8(x641)+P10(f3(x641,f10(x641)),a1)+P2(f3(x641,f10(x641)),a1)
% 128.75/128.90 [41]P11(x411,x412)+P2(x411,x412)+E(x411,x412)
% 128.75/128.90 [42]~P1(x421)+P4(x421)+~P6(x421,x422)
% 128.75/128.90 [47]P11(x471,x472)+~P10(x471,x472)+E(x471,x472)
% 128.75/128.90 [48]P2(x481,x482)+~P5(x481,x482)+E(x481,x482)
% 128.75/128.90 [49]~P1(x491)+~P6(x491,x492)+E(f6(x491,x492),a15)
% 128.75/128.90 [50]~P1(x501)+P7(x501,x502)+~E(f3(x501,x502),a14)
% 128.75/128.90 [58]~P8(x581)+P9(x581,x582)+~P2(f3(x581,x582),a1)
% 128.75/128.90 [61]~P8(x611)+~P9(x611,x612)+~P10(f3(x611,x612),a1)
% 128.75/128.90 [52]~P2(x521,x523)+P2(x521,x522)+~P2(x523,x522)
% 128.75/128.90 [65]~P3(x651,x653,x652)+P7(x651,x652)+P7(x651,x653)
% 128.75/128.90 [67]~P3(x671,x673,x672)+~P7(x671,x672)+~P7(x671,x673)
% 128.75/128.90 [62]~P1(x621)+~P7(x621,x623)+P7(x621,x622)+P3(x621,x622,x623)
% 128.75/128.90 [63]~P1(x631)+~P7(x631,x633)+P7(x631,x632)+P3(x631,x633,x632)
% 128.75/128.90 [68]~P1(x681)+P3(x681,x682,x683)+~E(f3(x681,x682),a14)+~P2(f3(x681,x683),a2)
% 128.75/128.90 [69]~P1(x691)+~P3(x691,x693,x692)+P2(f3(x691,x692),a2)+~E(f3(x691,x693),a14)
% 128.75/128.90 [53]P6(x531,x532)+P7(x531,x532)+P9(x531,x532)+~P1(x531)+E(f6(x531,x532),a7)
% 128.75/128.90 [54]P6(x541,x542)+P7(x541,x542)+~P1(x541)+~P9(x541,x542)+E(f6(x541,x542),a5)
% 128.75/128.90 [55]P6(x551,x552)+P9(x551,x552)+~P1(x551)+~P7(x551,x552)+E(f6(x551,x552),a4)
% 128.75/128.90 [57]P6(x571,x572)+~P1(x571)+~P7(x571,x572)+~P9(x571,x572)+E(f6(x571,x572),a8)
% 128.75/128.90 %EqnAxiom
% 128.75/128.90 [1]E(x11,x11)
% 128.75/128.90 [2]E(x22,x21)+~E(x21,x22)
% 128.75/128.90 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 128.75/128.90 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 128.75/128.90 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 128.75/128.90 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 128.75/128.90 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 128.75/128.90 [8]~E(x81,x82)+E(f10(x81),f10(x82))
% 128.75/128.90 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 128.75/128.90 [10]~P8(x101)+P8(x102)+~E(x101,x102)
% 128.75/128.90 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 128.75/128.90 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 128.75/128.90 [13]P7(x132,x133)+~E(x131,x132)+~P7(x131,x133)
% 128.75/128.90 [14]P7(x143,x142)+~E(x141,x142)+~P7(x143,x141)
% 128.75/128.90 [15]P3(x152,x153,x154)+~E(x151,x152)+~P3(x151,x153,x154)
% 128.75/128.90 [16]P3(x163,x162,x164)+~E(x161,x162)+~P3(x163,x161,x164)
% 128.75/128.90 [17]P3(x173,x174,x172)+~E(x171,x172)+~P3(x173,x174,x171)
% 128.75/128.90 [18]P10(x182,x183)+~E(x181,x182)+~P10(x181,x183)
% 128.75/128.90 [19]P10(x193,x192)+~E(x191,x192)+~P10(x193,x191)
% 128.75/128.90 [20]P9(x202,x203)+~E(x201,x202)+~P9(x201,x203)
% 128.75/128.90 [21]P9(x213,x212)+~E(x211,x212)+~P9(x213,x211)
% 128.75/128.90 [22]~P4(x221)+P4(x222)+~E(x221,x222)
% 128.75/128.91 [23]P6(x232,x233)+~E(x231,x232)+~P6(x231,x233)
% 128.75/128.91 [24]P6(x243,x242)+~E(x241,x242)+~P6(x243,x241)
% 128.75/128.91 [25]P5(x252,x253)+~E(x251,x252)+~P5(x251,x253)
% 128.75/128.91 [26]P5(x263,x262)+~E(x261,x262)+~P5(x263,x261)
% 128.75/128.91 [27]P11(x272,x273)+~E(x271,x272)+~P11(x271,x273)
% 128.75/128.91 [28]P11(x283,x282)+~E(x281,x282)+~P11(x283,x281)
% 128.75/128.91
% 128.75/128.91 %-------------------------------------------
% 128.75/128.91 cnf(70,plain,
% 128.75/128.91 (P10(x701,x701)),
% 128.75/128.91 inference(equality_inference,[],[39])).
% 128.75/128.91 cnf(71,plain,
% 128.75/128.91 (P5(x711,x711)),
% 128.75/128.91 inference(equality_inference,[],[40])).
% 128.75/128.91 cnf(72,plain,
% 128.75/128.91 (E(a2,a1)),
% 128.75/128.91 inference(scs_inference,[],[29,2])).
% 128.75/128.91 cnf(73,plain,
% 128.75/128.91 (~P2(a14,a2)),
% 128.75/128.91 inference(scs_inference,[],[29,33,2,51])).
% 128.75/128.91 cnf(76,plain,
% 128.75/128.91 (P2(f3(a9,a13),a1)),
% 128.75/128.91 inference(scs_inference,[],[29,33,37,2,51,11,12])).
% 128.75/128.91 cnf(77,plain,
% 128.75/128.91 (P10(a2,a1)),
% 128.75/128.91 inference(scs_inference,[],[29,33,37,70,2,51,11,12,18])).
% 128.75/128.91 cnf(79,plain,
% 128.75/128.91 (P10(f3(a9,a12),a1)),
% 128.75/128.91 inference(scs_inference,[],[29,33,36,37,70,2,51,11,12,18,19])).
% 128.75/128.91 cnf(80,plain,
% 128.75/128.91 (~P6(a9,x801)),
% 128.75/128.91 inference(scs_inference,[],[29,30,33,38,36,37,70,2,51,11,12,18,19,42])).
% 128.75/128.91 cnf(82,plain,
% 128.75/128.91 (P7(a9,a11)),
% 128.75/128.91 inference(scs_inference,[],[29,30,33,38,32,36,37,70,2,51,11,12,18,19,42,50])).
% 128.75/128.91 cnf(84,plain,
% 128.75/128.91 (P2(f3(a9,a13),a14)),
% 128.75/128.91 inference(scs_inference,[],[29,30,33,38,32,36,37,70,2,51,11,12,18,19,42,50,52])).
% 128.75/128.91 cnf(86,plain,
% 128.75/128.91 (P9(a9,a13)),
% 128.75/128.91 inference(scs_inference,[],[29,30,31,33,38,32,36,37,70,2,51,11,12,18,19,42,50,52,58])).
% 128.75/128.91 cnf(88,plain,
% 128.75/128.91 (~P9(a9,a12)),
% 128.75/128.91 inference(scs_inference,[],[29,30,31,33,38,32,36,37,70,2,51,11,12,18,19,42,50,52,58,61])).
% 128.75/128.91 cnf(94,plain,
% 128.75/128.91 (P5(x941,x941)),
% 128.75/128.91 inference(rename_variables,[],[71])).
% 128.75/128.91 cnf(97,plain,
% 128.75/128.91 (P3(a9,a11,a13)),
% 128.75/128.91 inference(scs_inference,[],[29,30,31,33,38,32,36,37,70,71,94,2,51,11,12,18,19,42,50,52,58,61,67,21,25,26,68])).
% 128.75/128.91 cnf(101,plain,
% 128.75/128.91 (~E(f3(a9,a13),f3(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[29,30,31,33,38,32,36,37,70,71,94,2,51,11,12,18,19,42,50,52,58,61,67,21,25,26,68,46,3])).
% 128.75/128.91 cnf(111,plain,
% 128.75/128.91 (E(a14,f3(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[34,32,51,2])).
% 128.75/128.91 cnf(112,plain,
% 128.75/128.91 (~P2(a14,f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[34,32,37,73,51,2,52])).
% 128.75/128.91 cnf(114,plain,
% 128.75/128.91 (P2(a1,f3(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[34,32,37,73,51,2,52,12])).
% 128.75/128.91 cnf(119,plain,
% 128.75/128.91 (E(f3(a9,a12),a2)+P11(f3(a9,a12),a2)),
% 128.75/128.91 inference(scs_inference,[],[29,34,36,32,37,70,73,51,2,52,12,19,46,47])).
% 128.75/128.91 cnf(121,plain,
% 128.75/128.91 (P2(a2,f3(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[29,34,36,32,37,70,73,51,2,52,12,19,46,47,11])).
% 128.75/128.91 cnf(122,plain,
% 128.75/128.91 (P9(x1221,a13)+~E(a9,x1221)),
% 128.75/128.91 inference(scs_inference,[],[29,34,36,32,37,70,73,86,51,2,52,12,19,46,47,11,20])).
% 128.75/128.91 cnf(131,plain,
% 128.75/128.91 (~P2(a2,f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[37,112,46,51])).
% 128.75/128.91 cnf(133,plain,
% 128.75/128.91 (P2(f3(a9,a13),f3(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[37,76,114,112,46,51,52])).
% 128.75/128.91 cnf(135,plain,
% 128.75/128.91 (~E(a14,f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[33,37,76,114,112,46,51,52,12])).
% 128.75/128.91 cnf(145,plain,
% 128.75/128.91 (~P2(a1,f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[76,131,46,51])).
% 128.75/128.91 cnf(165,plain,
% 128.75/128.91 (~P2(f3(a9,a11),a1)),
% 128.75/128.91 inference(scs_inference,[],[114,145,46,51])).
% 128.75/128.91 cnf(179,plain,
% 128.75/128.91 (~P2(f3(a9,a11),a2)),
% 128.75/128.91 inference(scs_inference,[],[121,165,46,51])).
% 128.75/128.91 cnf(181,plain,
% 128.75/128.91 (~P2(f3(a9,a11),f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[76,121,165,46,51,52])).
% 128.75/128.91 cnf(184,plain,
% 128.75/128.91 (E(f3(a9,a11),a1)+P11(f3(a9,a11),a1)),
% 128.75/128.91 inference(scs_inference,[],[76,121,97,165,46,51,52,16,41])).
% 128.75/128.91 cnf(193,plain,
% 128.75/128.91 (~P11(f3(a9,a13),f3(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[181,46])).
% 128.75/128.91 cnf(195,plain,
% 128.75/128.91 (~P2(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[181,35,46,51])).
% 128.75/128.91 cnf(200,plain,
% 128.75/128.91 (P10(x2001,a1)+~E(f3(a9,a12),x2001)),
% 128.75/128.91 inference(scs_inference,[],[32,79,181,179,35,46,51,10,41,18])).
% 128.75/128.91 cnf(204,plain,
% 128.75/128.91 (E(a14,a2)+P11(f3(a9,a11),a2)),
% 128.75/128.91 inference(scs_inference,[],[32,79,111,133,181,179,35,46,51,10,41,18,52,22,3])).
% 128.75/128.91 cnf(209,plain,
% 128.75/128.91 (E(a5,a4)+P11(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[179,195,46,41])).
% 128.75/128.91 cnf(211,plain,
% 128.75/128.91 (P2(a4,a4)+P11(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[179,195,35,46,41,12])).
% 128.75/128.91 cnf(212,plain,
% 128.75/128.91 (E(a4,a5)+P11(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[179,195,35,46,41,12,2])).
% 128.75/128.91 cnf(251,plain,
% 128.75/128.91 (P2(a4,x2511)+~E(a5,x2511)),
% 128.75/128.91 inference(scs_inference,[],[72,84,35,10,11,12])).
% 128.75/128.91 cnf(254,plain,
% 128.75/128.91 (P2(x2541,a5)+~E(a4,x2541)),
% 128.75/128.91 inference(scs_inference,[],[35,11])).
% 128.75/128.91 cnf(291,plain,
% 128.75/128.91 (P10(a14,a2)),
% 128.75/128.91 inference(scs_inference,[],[33,44,43])).
% 128.75/128.91 cnf(293,plain,
% 128.75/128.91 (P10(a14,a1)),
% 128.75/128.91 inference(scs_inference,[],[111,72,291,18,19])).
% 128.75/128.91 cnf(294,plain,
% 128.75/128.91 (P5(a1,a14)),
% 128.75/128.91 inference(scs_inference,[],[33,72,45,25])).
% 128.75/128.91 cnf(298,plain,
% 128.75/128.91 (~P9(a9,a11)),
% 128.75/128.91 inference(scs_inference,[],[29,31,111,293,294,25,26,18,61])).
% 128.75/128.91 cnf(310,plain,
% 128.75/128.91 (P10(a5,a4)+E(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[209,43])).
% 128.75/128.91 cnf(311,plain,
% 128.75/128.91 (P10(a5,a4)+P2(a4,a4)),
% 128.75/128.91 inference(scs_inference,[],[211,43])).
% 128.75/128.91 cnf(312,plain,
% 128.75/128.91 (P10(a5,a4)+E(a4,a5)),
% 128.75/128.91 inference(scs_inference,[],[212,43])).
% 128.75/128.91 cnf(318,plain,
% 128.75/128.91 (P10(a5,a4)+E(f6(a5,x3181),f6(a4,x3181))),
% 128.75/128.91 inference(scs_inference,[],[310,6])).
% 128.75/128.91 cnf(321,plain,
% 128.75/128.91 (P10(a5,x3211)+~E(a4,x3211)+E(a4,a5)),
% 128.75/128.91 inference(scs_inference,[],[312,19])).
% 128.75/128.91 cnf(326,plain,
% 128.75/128.91 (E(f10(a14),f10(f3(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[32,8,2])).
% 128.75/128.91 cnf(327,plain,
% 128.75/128.91 (E(f10(f3(a9,a11)),f10(a14))),
% 128.75/128.91 inference(scs_inference,[],[326,2])).
% 128.75/128.91 cnf(352,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+E(a2,a14)),
% 128.75/128.91 inference(scs_inference,[],[204,2])).
% 128.75/128.91 cnf(367,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+E(a2,a14)),
% 128.75/128.91 inference(scs_inference,[],[72,352,28])).
% 128.75/128.91 cnf(388,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+E(f3(a2,x3881),f3(a14,x3881))),
% 128.75/128.91 inference(scs_inference,[],[367,4])).
% 128.75/128.91 cnf(395,plain,
% 128.75/128.91 (P11(f3(a9,a12),a2)+P5(a2,f3(a9,a12))),
% 128.75/128.91 inference(scs_inference,[],[71,119,25])).
% 128.75/128.91 cnf(398,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+E(f6(f3(a9,a11),x3981),f6(a1,x3981))),
% 128.75/128.91 inference(scs_inference,[],[184,6])).
% 128.75/128.91 cnf(410,plain,
% 128.75/128.91 (P10(a5,x4101)+~E(a4,x4101)+E(f6(a5,x4102),f6(a4,x4102))),
% 128.75/128.91 inference(scs_inference,[],[318,19])).
% 128.75/128.91 cnf(416,plain,
% 128.75/128.91 (P2(a2,f3(a9,a12))+P5(a2,f3(a9,a12))),
% 128.75/128.91 inference(scs_inference,[],[395,46])).
% 128.75/128.91 cnf(437,plain,
% 128.75/128.91 (P5(a2,f3(a9,a12))),
% 128.75/128.91 inference(scs_inference,[],[416,45])).
% 128.75/128.91 cnf(504,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+E(f3(a2,x5041),f3(a14,x5041))),
% 128.75/128.91 inference(scs_inference,[],[29,388,28])).
% 128.75/128.91 cnf(514,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+P5(f3(a2,x5141),f3(a14,x5141))),
% 128.75/128.91 inference(scs_inference,[],[504,40])).
% 128.75/128.91 cnf(518,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+P5(f3(a2,x5181),f3(a14,x5181))),
% 128.75/128.91 inference(scs_inference,[],[72,514,28])).
% 128.75/128.91 cnf(519,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+P5(f3(a2,x5191),x5192)+~E(f3(a14,x5191),x5192)),
% 128.75/128.91 inference(scs_inference,[],[518,26])).
% 128.75/128.91 cnf(526,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+E(f6(f3(a9,a11),x5261),f6(a1,x5261))),
% 128.75/128.91 inference(scs_inference,[],[29,398,28])).
% 128.75/128.91 cnf(535,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+E(f6(a1,x5351),f6(f3(a9,a11),x5351))),
% 128.75/128.91 inference(scs_inference,[],[526,2])).
% 128.75/128.91 cnf(545,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+E(f6(a1,x5451),f6(f3(a9,a11),x5451))),
% 128.75/128.91 inference(scs_inference,[],[72,535,28])).
% 128.75/128.91 cnf(550,plain,
% 128.75/128.91 (P11(f3(a9,a11),a1)+P10(f6(a1,x5501),f6(f3(a9,a11),x5501))),
% 128.75/128.91 inference(scs_inference,[],[545,39])).
% 128.75/128.91 cnf(551,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+P10(f6(a1,x5511),f6(f3(a9,a11),x5511))),
% 128.75/128.91 inference(scs_inference,[],[29,550,28])).
% 128.75/128.91 cnf(552,plain,
% 128.75/128.91 (P11(f3(a9,a11),a2)+P10(x5521,f6(f3(a9,a11),x5522))+~E(f6(a1,x5522),x5521)),
% 128.75/128.91 inference(scs_inference,[],[551,18])).
% 128.75/128.91 cnf(578,plain,
% 128.75/128.91 (P7(a9,a13)+E(f6(a9,a11),a4)),
% 128.75/128.91 inference(scs_inference,[],[97,298,30,80,65,55])).
% 128.75/128.91 cnf(579,plain,
% 128.75/128.91 (E(a4,f6(a9,a11))+P7(a9,a13)),
% 128.75/128.91 inference(scs_inference,[],[578,2])).
% 128.75/128.91 cnf(580,plain,
% 128.75/128.91 (E(f3(a4,x5801),f3(f6(a9,a11),x5801))+P7(a9,a13)),
% 128.75/128.91 inference(scs_inference,[],[579,4])).
% 128.75/128.91 cnf(581,plain,
% 128.75/128.91 (E(f3(x5811,f3(a4,x5812)),f3(x5811,f3(f6(a9,a11),x5812)))+P7(a9,a13)),
% 128.75/128.91 inference(scs_inference,[],[580,5])).
% 128.75/128.91 cnf(1093,plain,
% 128.75/128.91 (E(f3(f10(a14),x10931),f3(f10(f3(a9,a11)),x10931))),
% 128.75/128.91 inference(scs_inference,[],[327,2,4])).
% 128.75/128.91 cnf(1094,plain,
% 128.75/128.91 (E(f3(x10941,a14),f3(x10941,f3(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[32,2,5])).
% 128.75/128.91 cnf(1216,plain,
% 128.75/128.91 (E(f6(a14,x12161),f6(f3(a9,a11),x12161))),
% 128.75/128.91 inference(scs_inference,[],[32,2,6])).
% 128.75/128.91 cnf(1217,plain,
% 128.75/128.91 (E(f6(f3(a9,a11),x12171),f6(a14,x12171))),
% 128.75/128.91 inference(scs_inference,[],[1216,2])).
% 128.75/128.91 cnf(1536,plain,
% 128.75/128.91 (E(f6(x15361,a14),f6(x15361,f3(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[32,2,7])).
% 128.75/128.91 cnf(1537,plain,
% 128.75/128.91 (E(f6(x15371,f3(a9,a11)),f6(x15371,a14))),
% 128.75/128.91 inference(scs_inference,[],[1536,2])).
% 128.75/128.91 cnf(1877,plain,
% 128.75/128.91 (E(f3(f3(x18771,f3(a9,a11)),x18772),f3(f3(x18771,a14),x18772))),
% 128.75/128.91 inference(scs_inference,[],[1094,2,4])).
% 128.75/128.91 cnf(1880,plain,
% 128.75/128.91 (E(a4,f6(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[82,298,30,80,2,55])).
% 128.75/128.91 cnf(1881,plain,
% 128.75/128.91 (P2(f6(a9,a11),a5)),
% 128.75/128.91 inference(scs_inference,[],[1880,254])).
% 128.75/128.91 cnf(1886,plain,
% 128.75/128.91 (E(f6(a9,a11),a4)),
% 128.75/128.91 inference(scs_inference,[],[1880,254,51,46,2])).
% 128.75/128.91 cnf(1936,plain,
% 128.75/128.91 (P2(f6(a9,a11),x19361)+~E(a5,x19361)),
% 128.75/128.91 inference(scs_inference,[],[1881,12])).
% 128.75/128.91 cnf(2282,plain,
% 128.75/128.91 (P11(a5,f6(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[1880,44,254])).
% 128.75/128.91 cnf(2283,plain,
% 128.75/128.91 (P11(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[1886,2282,28])).
% 128.75/128.91 cnf(2284,plain,
% 128.75/128.91 (P11(x22841,f6(a9,a11))+~E(a5,x22841)),
% 128.75/128.91 inference(scs_inference,[],[1886,2282,28,27])).
% 128.75/128.91 cnf(2286,plain,
% 128.75/128.91 (P11(a14,a1)),
% 128.75/128.91 inference(scs_inference,[],[33,72,44,28])).
% 128.75/128.91 cnf(2287,plain,
% 128.75/128.91 (P11(a14,a2)),
% 128.75/128.91 inference(scs_inference,[],[29,2286,28])).
% 128.75/128.91 cnf(2288,plain,
% 128.75/128.91 (P11(x22881,a4)+~E(a5,x22881)),
% 128.75/128.91 inference(scs_inference,[],[29,2283,2286,28,27])).
% 128.75/128.91 cnf(2290,plain,
% 128.75/128.91 (P5(f6(a9,a11),a5)),
% 128.75/128.91 inference(scs_inference,[],[1880,45,254])).
% 128.75/128.91 cnf(2291,plain,
% 128.75/128.91 (P5(a4,a5)),
% 128.75/128.91 inference(scs_inference,[],[1886,2290,25])).
% 128.75/128.91 cnf(2292,plain,
% 128.75/128.91 (P5(f6(a9,a11),x22921)+~E(a5,x22921)),
% 128.75/128.91 inference(scs_inference,[],[1886,2290,25,26])).
% 128.75/128.91 cnf(2297,plain,
% 128.75/128.91 (P5(a4,x22971)+~E(a5,x22971)),
% 128.75/128.91 inference(scs_inference,[],[2291,26])).
% 128.75/128.91 cnf(2302,plain,
% 128.75/128.91 (P5(f3(a9,a13),a2)),
% 128.75/128.91 inference(scs_inference,[],[32,30,97,45,69])).
% 128.75/128.91 cnf(2309,plain,
% 128.75/128.91 (P5(f3(f10(a14),a13),a2)+~E(a9,f10(f3(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[36,72,327,1094,1537,1880,1881,82,97,437,179,2302,26,25,4,410,321,552,519,41,47,52,48,15,14,3])).
% 128.75/128.91 cnf(2314,plain,
% 128.75/128.91 (P5(f3(f10(a14),a13),a1)+~E(a9,f10(f3(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[72,2309,26])).
% 128.75/128.91 cnf(2326,plain,
% 128.75/128.91 (P5(x23261,a1)+~E(f3(f10(a14),a13),x23261)+~E(a9,f10(f3(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[2314,25])).
% 128.75/128.91 cnf(2599,plain,
% 128.75/128.91 (P10(a5,a4)),
% 128.75/128.91 inference(scs_inference,[],[51,311])).
% 128.75/128.91 cnf(2600,plain,
% 128.75/128.91 (P10(a5,f6(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[1880,2599,19])).
% 128.75/128.91 cnf(2601,plain,
% 128.75/128.91 (P10(x26011,a4)+~E(a5,x26011)),
% 128.75/128.91 inference(scs_inference,[],[1880,2599,19,18])).
% 128.75/128.91 cnf(2609,plain,
% 128.75/128.91 (P10(x26091,f6(a9,a11))+~E(a5,x26091)),
% 128.75/128.91 inference(scs_inference,[],[2600,18])).
% 128.75/128.91 cnf(2728,plain,
% 128.75/128.91 (~P10(f3(a9,a13),a1)),
% 128.75/128.91 inference(scs_inference,[],[31,122,61])).
% 128.75/128.91 cnf(2729,plain,
% 128.75/128.91 (~E(f3(a9,a12),f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[2728,200])).
% 128.75/128.91 cnf(2851,plain,
% 128.75/128.91 (E(f6(f6(a9,a11),x28511),f6(a4,x28511))),
% 128.75/128.91 inference(scs_inference,[],[1886,8,6])).
% 128.75/128.91 cnf(2859,plain,
% 128.75/128.91 (E(f3(f6(a9,a11),x28591),f3(a4,x28591))),
% 128.75/128.91 inference(scs_inference,[],[114,1886,8,6,7,39,40,44,4])).
% 128.75/128.91 cnf(2860,plain,
% 128.75/128.91 (E(f3(x28601,f6(a9,a11)),f3(x28601,a4))),
% 128.75/128.91 inference(scs_inference,[],[114,1886,8,6,7,39,40,44,4,5])).
% 128.75/128.91 cnf(2862,plain,
% 128.75/128.91 (~P7(a9,a13)),
% 128.75/128.91 inference(scs_inference,[],[2729,114,1886,97,82,8,6,7,39,40,44,4,5,2,67])).
% 128.75/128.91 cnf(2864,plain,
% 128.75/128.91 (~P2(f3(a9,a12),a1)),
% 128.75/128.91 inference(scs_inference,[],[2729,114,88,31,1886,97,82,8,6,7,39,40,44,4,5,2,67,58])).
% 128.75/128.91 cnf(2877,plain,
% 128.75/128.91 (E(f6(a9,a13),a5)),
% 128.75/128.91 inference(scs_inference,[],[30,2287,2729,193,77,2728,101,135,114,88,112,80,31,1217,1886,86,97,111,72,82,8,6,7,39,40,44,4,5,2,67,58,47,48,3,27,18,19,62,54])).
% 128.75/128.91 cnf(2888,plain,
% 128.75/128.91 (E(f3(a4,x28881),f3(f6(a9,a11),x28881))),
% 128.75/128.91 inference(scs_inference,[],[2862,580])).
% 128.75/128.91 cnf(2889,plain,
% 128.75/128.91 (E(f3(x28891,f3(a4,x28892)),f3(x28891,f3(f6(a9,a11),x28892)))),
% 128.75/128.91 inference(scs_inference,[],[2862,581])).
% 128.75/128.91 cnf(2892,plain,
% 128.75/128.91 (E(f6(f6(a9,a13),x28921),f6(a5,x28921))),
% 128.75/128.91 inference(scs_inference,[],[2877,6])).
% 128.75/128.91 cnf(2898,plain,
% 128.75/128.91 (E(f6(x28981,f6(a9,a13)),f6(x28981,a5))),
% 128.75/128.91 inference(scs_inference,[],[2877,6,8,39,40,7])).
% 128.75/128.91 cnf(2899,plain,
% 128.75/128.91 (E(f3(f6(a9,a13),x28991),f3(a5,x28991))),
% 128.75/128.91 inference(scs_inference,[],[2877,6,8,39,40,7,4])).
% 128.75/128.91 cnf(2921,plain,
% 128.75/128.91 (E(f6(a4,x29211),f6(f6(a9,a11),x29211))),
% 128.75/128.91 inference(scs_inference,[],[1880,6])).
% 128.75/128.91 cnf(2927,plain,
% 128.75/128.91 (E(f6(x29271,a4),f6(x29271,f6(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[2859,1880,6,8,39,40,7])).
% 128.75/128.91 cnf(2928,plain,
% 128.75/128.91 (E(f3(a2,x29281),f3(a1,x29281))),
% 128.75/128.91 inference(scs_inference,[],[2859,1880,72,6,8,39,40,7,4])).
% 128.75/128.91 cnf(2929,plain,
% 128.75/128.91 (E(f3(x29291,a4),f3(x29291,f6(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[2859,1880,72,6,8,39,40,7,4,5])).
% 128.75/128.91 cnf(2933,plain,
% 128.75/128.91 (~P2(f3(a9,a12),a2)),
% 128.75/128.91 inference(scs_inference,[],[2864,2859,2860,1880,72,6,8,39,40,7,4,5,3,12])).
% 128.75/128.91 cnf(2942,plain,
% 128.75/128.91 (E(f6(a2,x29421),f6(a1,x29421))),
% 128.75/128.91 inference(scs_inference,[],[72,6])).
% 128.75/128.91 cnf(2943,plain,
% 128.75/128.91 (E(f10(a2),f10(a1))),
% 128.75/128.91 inference(scs_inference,[],[72,6,8])).
% 128.75/128.91 cnf(2944,plain,
% 128.75/128.91 (P5(f3(a2,x29441),f3(a1,x29441))),
% 128.75/128.91 inference(scs_inference,[],[2928,72,6,8,40])).
% 128.75/128.91 cnf(2946,plain,
% 128.75/128.91 (P10(f3(a2,x29461),f3(a1,x29461))),
% 128.75/128.91 inference(scs_inference,[],[2928,72,6,8,40,39])).
% 128.75/128.91 cnf(2948,plain,
% 128.75/128.91 (E(f6(x29481,a2),f6(x29481,a1))),
% 128.75/128.91 inference(scs_inference,[],[2928,72,6,8,40,39,7])).
% 128.75/128.91 cnf(2949,plain,
% 128.75/128.91 (E(f3(a1,x29491),f3(a2,x29491))),
% 128.75/128.91 inference(scs_inference,[],[2928,72,29,6,8,40,39,7,4])).
% 128.75/128.91 cnf(2950,plain,
% 128.75/128.91 (E(f3(x29501,a2),f3(x29501,a1))),
% 128.75/128.91 inference(scs_inference,[],[2928,72,29,6,8,40,39,7,4,5])).
% 128.75/128.91 cnf(2963,plain,
% 128.75/128.91 (E(f6(a1,x29631),f6(a2,x29631))),
% 128.75/128.91 inference(scs_inference,[],[29,6])).
% 128.75/128.91 cnf(2964,plain,
% 128.75/128.91 (E(f10(a1),f10(a2))),
% 128.75/128.91 inference(scs_inference,[],[29,6,8])).
% 128.75/128.91 cnf(2969,plain,
% 128.75/128.91 (E(f6(x29691,a1),f6(x29691,a2))),
% 128.75/128.91 inference(scs_inference,[],[2948,29,6,8,40,39,7])).
% 128.75/128.91 cnf(2970,plain,
% 128.75/128.91 (E(f3(x29701,a1),f3(x29701,a2))),
% 128.75/128.91 inference(scs_inference,[],[2948,29,6,8,40,39,7,5])).
% 128.75/128.91 cnf(2986,plain,
% 128.75/128.91 (E(f3(a1,a2),f3(a2,a1))),
% 128.75/128.91 inference(scs_inference,[],[2943,2949,2950,39,40,3])).
% 128.75/128.91 cnf(2998,plain,
% 128.75/128.91 (E(f6(a1,a1),f6(a2,a2))),
% 128.75/128.91 inference(scs_inference,[],[2964,2963,2969,39,40,3])).
% 128.75/128.91 cnf(3012,plain,
% 128.75/128.91 (E(f6(a1,f6(a9,a13)),f6(a2,a5))),
% 128.75/128.91 inference(scs_inference,[],[2998,2898,2963,39,40,3])).
% 128.75/128.91 cnf(3024,plain,
% 128.75/128.91 (E(f3(f6(a9,a13),a1),f3(a5,a2))),
% 128.75/128.91 inference(scs_inference,[],[3012,2970,2899,39,40,3])).
% 128.75/128.91 cnf(3037,plain,
% 128.75/128.91 (E(f6(a2,a4),f6(a1,f6(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[3024,2927,2942,39,40,3])).
% 128.75/128.91 cnf(3055,plain,
% 128.75/128.91 (E(f3(a4,a2),f3(f6(a9,a11),a1))),
% 128.75/128.91 inference(scs_inference,[],[2946,3037,2986,2888,2950,39,40,19,3])).
% 128.75/128.91 cnf(3071,plain,
% 128.75/128.91 (E(f6(f6(a9,a13),a1),f6(a5,a2))),
% 128.75/128.91 inference(scs_inference,[],[3055,2969,2892,39,40,3])).
% 128.75/128.91 cnf(3087,plain,
% 128.75/128.91 (~P2(f3(a9,a12),f3(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[3071,2933,37,39,40,52])).
% 128.75/128.91 cnf(3358,plain,
% 128.75/128.91 (P10(f6(f6(a9,a11),x33581),f6(a4,x33581))),
% 128.75/128.91 inference(scs_inference,[],[2851,39])).
% 128.75/128.91 cnf(3474,plain,
% 128.75/128.91 (P5(f3(a4,x34741),f3(f6(a9,a11),x34741))),
% 128.75/128.91 inference(scs_inference,[],[2888,39,40])).
% 128.75/128.91 cnf(3506,plain,
% 128.75/128.91 (E(f6(f3(a9,a11),a1),f6(a14,a2))),
% 128.75/128.91 inference(scs_inference,[],[2860,2969,1217,39,40,3])).
% 128.75/128.91 cnf(3551,plain,
% 128.75/128.91 (P10(f3(x35511,a4),f3(x35511,f6(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[2929,39])).
% 128.75/128.91 cnf(3553,plain,
% 128.75/128.91 (P5(f3(x35531,a4),f3(x35531,f6(a9,a11)))),
% 128.75/128.91 inference(scs_inference,[],[2929,39,40])).
% 128.75/128.91 cnf(4552,plain,
% 128.75/128.91 (~P7(a9,a12)+E(f6(a9,a12),a4)),
% 128.75/128.91 inference(scs_inference,[],[88,80,30,55])).
% 128.75/128.91 cnf(5890,plain,
% 128.75/128.91 (E(f3(f3(x58901,f3(a9,a11)),x58902),f3(f3(x58901,a14),x58902))),
% 128.75/128.91 inference(rename_variables,[],[1877])).
% 128.75/128.91 cnf(5891,plain,
% 128.75/128.91 (P10(f3(x58911,a4),f3(x58911,f6(a9,a11)))),
% 128.75/128.91 inference(rename_variables,[],[3551])).
% 128.75/128.91 cnf(5893,plain,
% 128.75/128.91 (E(f3(f3(x58931,f3(a9,a11)),x58932),f3(f3(x58931,a14),x58932))),
% 128.75/128.91 inference(rename_variables,[],[1877])).
% 128.75/128.91 cnf(5894,plain,
% 128.75/128.91 (P5(f3(x58941,a4),f3(x58941,f6(a9,a11)))),
% 128.75/128.91 inference(rename_variables,[],[3553])).
% 128.75/128.91 cnf(5898,plain,
% 128.75/128.91 (E(f3(f3(x58981,f3(a9,a11)),x58982),f3(f3(x58981,a14),x58982))),
% 128.75/128.91 inference(rename_variables,[],[1877])).
% 128.75/128.91 cnf(5901,plain,
% 128.75/128.91 (E(f3(f3(x59011,f3(a9,a11)),x59012),f3(f3(x59011,a14),x59012))),
% 128.75/128.91 inference(rename_variables,[],[1877])).
% 128.75/128.91 cnf(5903,plain,
% 128.75/128.91 (E(f3(f3(x59031,f3(a9,a11)),f3(a4,x59032)),f3(f3(x59031,a14),f3(f6(a9,a11),x59032)))),
% 128.75/128.91 inference(scs_inference,[],[3551,5891,3553,5894,1877,5890,5893,5898,5901,2889,1093,39,40,5,6,7,8,4,19,26,2326,25,18,3])).
% 128.75/128.91 cnf(5914,plain,
% 128.75/128.91 (E(f6(f3(f3(x59141,f3(a9,a11)),f3(a4,x59142)),x59143),f6(f3(f3(x59141,a14),f3(f6(a9,a11),x59142)),x59143))),
% 128.75/128.91 inference(scs_inference,[],[5903,39,40,5,6])).
% 128.75/128.91 cnf(5917,plain,
% 128.75/128.91 (E(f3(f3(f3(x59171,f3(a9,a11)),f3(a4,x59172)),x59173),f3(f3(f3(x59171,a14),f3(f6(a9,a11),x59172)),x59173))),
% 128.75/128.91 inference(scs_inference,[],[5903,39,40,5,6,7,8,4])).
% 128.75/128.91 cnf(5962,plain,
% 128.75/128.91 (E(a5,f6(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[2877,2])).
% 128.75/128.91 cnf(5978,plain,
% 128.75/128.91 (E(f3(x59781,a14),f3(x59781,f3(a9,a11)))),
% 128.75/128.91 inference(rename_variables,[],[1094])).
% 128.75/128.91 cnf(5986,plain,
% 128.75/128.91 (E(f3(x59861,a14),f3(x59861,f3(a9,a11)))),
% 128.75/128.91 inference(rename_variables,[],[1094])).
% 128.75/128.91 cnf(5994,plain,
% 128.75/128.91 (E(f6(a9,a12),a4)),
% 128.75/128.91 inference(scs_inference,[],[32,30,82,1094,5978,5986,2877,1537,1216,2862,2969,3087,2933,2946,2944,3358,3474,2,46,2288,2284,251,1936,2292,2297,2601,2609,3,26,18,65,25,19,69,63,4552])).
% 128.75/128.91 cnf(6031,plain,
% 128.75/128.91 (E(f6(a4,f3(a9,a11)),f6(f6(a9,a11),a14))),
% 128.75/128.91 inference(scs_inference,[],[1537,3506,2921,2864,2,46,3])).
% 128.75/128.91 cnf(6572,plain,
% 128.75/128.91 (E(f6(f3(f3(x65721,a14),f3(f6(a9,a11),x65722)),x65723),f6(f3(f3(x65721,f3(a9,a11)),f3(a4,x65722)),x65723))),
% 128.75/128.91 inference(scs_inference,[],[5914,2])).
% 128.75/128.91 cnf(6580,plain,
% 128.75/128.91 (E(a4,f6(a9,a12))),
% 128.75/128.91 inference(scs_inference,[],[5994,2])).
% 128.75/128.91 cnf(6585,plain,
% 128.75/128.91 (P2(f6(a9,a12),f6(a9,a13))),
% 128.75/128.91 inference(scs_inference,[],[1537,5962,5994,6572,2,254,3,12])).
% 128.75/128.91 cnf(6597,plain,
% 128.75/128.91 (E(f6(a9,a11),f6(a9,a12))),
% 128.75/128.91 inference(scs_inference,[],[1886,6580,6031,6585,2,51,3])).
% 128.75/128.91 cnf(6603,plain,
% 128.75/128.91 (E(f6(a9,a12),f6(a9,a11))),
% 128.75/128.91 inference(scs_inference,[],[6597,2])).
% 128.75/128.91 cnf(6610,plain,
% 128.75/128.91 (~P11(f6(a9,a13),f6(a9,a12))),
% 128.75/128.91 inference(scs_inference,[],[6603,66])).
% 128.75/128.91 cnf(6619,plain,
% 128.75/128.91 ($false),
% 128.75/128.91 inference(scs_inference,[],[5917,6585,6610,2,44]),
% 128.75/128.91 ['proof']).
% 128.75/128.91 % SZS output end Proof
% 128.75/128.91 % Total time :128.502970s
%------------------------------------------------------------------------------