%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT065-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 : n017.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:23 AM UTC 2026
% Result : Unsatisfiable 281.52s 281.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT065-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.06/0.35 % Computer : n017.cluster.edu
% 0.06/0.35 % Model : x86_64 x86_64
% 0.06/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.35 % Memory : 8046.5625MB
% 0.06/0.35 % OS : Linux 6.8.0-71-generic
% 0.06/0.35 % CPULimit : 300
% 0.06/0.35 % WCLimit : 300
% 0.06/0.35 % DateTime : Mon Sep 7 13:41:54 UTC 2026
% 0.06/0.35 % CPUTime :
% 0.25/0.51 start to proof:theBenchmark
% 281.52/281.58 %-------------------------------------------
% 281.52/281.58 % File :CSE---1.7
% 281.52/281.58 % Problem :theBenchmark
% 281.52/281.58 % Transform :cnf
% 281.52/281.58 % Format :tptp:raw
% 281.52/281.58 % Command :java -jar mcs_scs.jar %d %s
% 281.52/281.58
% 281.52/281.58 % Result :Theorem 281.052948s
% 281.52/281.58 % Output :CNFRefutation 281.052948s
% 281.52/281.58 %-------------------------------------------
% 281.52/281.58 %--------------------------------------------------------------------------
% 281.52/281.58 % File : MGT065-1 : TPTP v9.3.0. Released v2.4.0.
% 281.52/281.58 % Domain : Management (Organisation Theory)
% 281.52/281.58 % Problem : Long-run hazard of mortality
% 281.52/281.58 % Version : [Han98] axioms.
% 281.52/281.58 % English : The long-run hazard of mortality for an endowed organization with
% 281.52/281.58 % either a fragile or a robust position in a drifting environment
% 281.52/281.58 % exceeds the hazard near founding.
% 281.52/281.58
% 281.52/281.58 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 281.52/281.58 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 281.52/281.58 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 281.52/281.58 % Source : [TPTP]
% 281.52/281.58 % Names :
% 281.52/281.58
% 281.52/281.58 % Status : Unsatisfiable
% 281.52/281.58 % Rating : 0.08 v9.3.0, 0.09 v9.1.0, 0.10 v9.0.0, 0.15 v8.2.0, 0.14 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.18 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.29 v6.0.0, 0.20 v5.5.0, 0.35 v5.3.0, 0.22 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0, 0.15 v4.0.1, 0.09 v4.0.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0, 0.31 v3.1.0, 0.45 v2.7.0, 0.25 v2.6.0, 0.22 v2.5.0, 0.33 v2.4.0
% 281.52/281.58 % Syntax : Number of clauses : 52 ( 17 unt; 17 nHn; 46 RR)
% 281.52/281.58 % Number of literals : 129 ( 15 equ; 57 neg)
% 281.52/281.58 % Maximal clause size : 5 ( 2 avg)
% 281.52/281.58 % Maximal term depth : 3 ( 1 avg)
% 281.52/281.58 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 281.52/281.58 % Number of functors : 16 ( 16 usr; 13 con; 0-2 aty)
% 281.52/281.58 % Number of variables : 71 ( 4 sgn)
% 281.52/281.58 % SPC : CNF_UNS_RFO_SEQ_NHN
% 281.52/281.58
% 281.52/281.58 % Comments : See MGT042+1.p for the mnemonic names.
% 281.52/281.58 % : Created with tptp2X -f tptp -t clausify:otter MGT065+1.p
% 281.52/281.58 %--------------------------------------------------------------------------
% 281.52/281.58 include('Axioms/MGT001-0.ax').
% 281.52/281.58 %--------------------------------------------------------------------------
% 281.52/281.58 cnf(definition_1_40,axiom,
% 281.52/281.58 ( ~ has_endowment(A)
% 281.52/281.58 | organization(A) ) ).
% 281.52/281.58
% 281.52/281.58 cnf(definition_1_41,axiom,
% 281.52/281.58 ( ~ has_endowment(A)
% 281.52/281.58 | ~ smaller_or_equal(age(A,B),eta)
% 281.52/281.58 | has_immunity(A,B) ) ).
% 281.52/281.58
% 281.52/281.58 cnf(definition_1_42,axiom,
% 281.52/281.58 ( ~ has_endowment(A)
% 281.52/281.58 | ~ greater(age(A,B),eta)
% 281.52/281.58 | ~ has_immunity(A,B) ) ).
% 281.52/281.58
% 281.52/281.58 cnf(definition_1_43,axiom,
% 281.52/281.58 ( ~ organization(A)
% 281.52/281.58 | smaller_or_equal(age(A,sk1(A)),eta)
% 281.52/281.58 | greater(age(A,sk1(A)),eta)
% 281.52/281.58 | has_endowment(A) ) ).
% 281.52/281.58
% 281.52/281.58 cnf(definition_1_44,axiom,
% 281.52/281.58 ( ~ organization(A)
% 281.52/281.58 | smaller_or_equal(age(A,sk1(A)),eta)
% 281.52/281.58 | has_immunity(A,sk1(A))
% 281.52/281.58 | has_endowment(A) ) ).
% 281.52/281.58
% 281.52/281.58 cnf(definition_1_45,axiom,
% 281.52/281.58 ( ~ organization(A)
% 281.52/281.58 | ~ has_immunity(A,sk1(A))
% 281.52/281.58 | greater(age(A,sk1(A)),eta)
% 281.52/281.58 | has_endowment(A) ) ).
% 281.52/281.58
% 281.52/281.58 cnf(definition_1_46,axiom,
% 281.52/281.58 ( ~ organization(A)
% 281.52/281.59 | ~ has_immunity(A,sk1(A))
% 281.52/281.59 | has_immunity(A,sk1(A))
% 281.52/281.59 | has_endowment(A) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_47,axiom,
% 281.52/281.59 ( ~ dissimilar(A,B,C)
% 281.52/281.59 | organization(A) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_48,axiom,
% 281.52/281.59 ( ~ dissimilar(A,B,C)
% 281.52/281.59 | is_aligned(A,B)
% 281.52/281.59 | is_aligned(A,C) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_49,axiom,
% 281.52/281.59 ( ~ dissimilar(A,B,C)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | ~ is_aligned(A,C) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_50,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | is_aligned(A,B)
% 281.52/281.59 | dissimilar(A,B,C) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_51,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | is_aligned(A,C)
% 281.52/281.59 | dissimilar(A,B,C) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_52,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | is_aligned(A,C)
% 281.52/281.59 | dissimilar(A,C,B) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(definition_2_53,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | is_aligned(A,B)
% 281.52/281.59 | dissimilar(A,C,B) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_13_54,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | age(A,B) != zero
% 281.52/281.59 | is_aligned(A,B) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_15_55,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | age(A,B) != zero
% 281.52/281.59 | ~ greater(age(A,C),sigma)
% 281.52/281.59 | dissimilar(A,B,C) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_15_56,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | age(A,B) != zero
% 281.52/281.59 | ~ dissimilar(A,B,C)
% 281.52/281.59 | greater(age(A,C),sigma) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_17_57,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | ~ has_immunity(A,B)
% 281.52/281.59 | hazard_of_mortality(A,B) = very_low ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_17_58,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | has_immunity(A,B)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | ~ positional_advantage(A,B)
% 281.52/281.59 | hazard_of_mortality(A,B) = low ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_17_59,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | has_immunity(A,B)
% 281.52/281.59 | is_aligned(A,B)
% 281.52/281.59 | ~ positional_advantage(A,B)
% 281.52/281.59 | hazard_of_mortality(A,B) = mod1 ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_17_60,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | has_immunity(A,B)
% 281.52/281.59 | ~ is_aligned(A,B)
% 281.52/281.59 | positional_advantage(A,B)
% 281.52/281.59 | hazard_of_mortality(A,B) = mod2 ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_17_61,axiom,
% 281.52/281.59 ( ~ organization(A)
% 281.52/281.59 | has_immunity(A,B)
% 281.52/281.59 | is_aligned(A,B)
% 281.52/281.59 | positional_advantage(A,B)
% 281.52/281.59 | hazard_of_mortality(A,B) = high ) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_18a_62,axiom,
% 281.52/281.59 greater(high,mod1) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_18b_63,axiom,
% 281.52/281.59 greater(mod1,low) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_18c_64,axiom,
% 281.52/281.59 greater(low,very_low) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_18d_65,axiom,
% 281.52/281.59 greater(high,mod2) ).
% 281.52/281.59
% 281.52/281.59 cnf(assumption_18e_66,axiom,
% 281.52/281.59 greater(mod2,low) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_67,negated_conjecture,
% 281.52/281.59 organization(sk2) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_68,negated_conjecture,
% 281.52/281.59 ( robust_position(sk2)
% 281.52/281.59 | fragile_position(sk2) ) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_69,negated_conjecture,
% 281.52/281.59 has_endowment(sk2) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_70,negated_conjecture,
% 281.52/281.59 age(sk2,sk3) = zero ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_71,negated_conjecture,
% 281.52/281.59 greater(sigma,zero) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_72,negated_conjecture,
% 281.52/281.59 greater(tau,zero) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_73,negated_conjecture,
% 281.52/281.59 greater(eta,zero) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_74,negated_conjecture,
% 281.52/281.59 smaller_or_equal(age(sk2,sk4),sigma) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_75,negated_conjecture,
% 281.52/281.59 smaller_or_equal(age(sk2,sk4),tau) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_76,negated_conjecture,
% 281.52/281.59 smaller_or_equal(age(sk2,sk4),eta) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_77,negated_conjecture,
% 281.52/281.59 greater(age(sk2,sk5),sigma) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_78,negated_conjecture,
% 281.52/281.59 greater(age(sk2,sk5),tau) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_79,negated_conjecture,
% 281.52/281.59 greater(age(sk2,sk5),eta) ).
% 281.52/281.59
% 281.52/281.59 cnf(theorem_11_80,negated_conjecture,
% 281.52/281.59 ( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
% 281.52/281.59 | hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ).
% 281.52/281.59
% 281.52/281.59 %--------------------------------------------------------------------------
% 281.52/281.59 %-------------------------------------------
% 281.52/281.59 % Proof found
% 281.52/281.59 % SZS status Theorem for theBenchmark
% 281.52/281.59 % SZS output start Proof
% 281.52/281.59 %ClaNum:78(EqnAxiom:29)
% 281.52/281.59 %VarNum:178(SingletonVarNum:64)
% 281.52/281.59 %MaxLitNum:5
% 281.52/281.59 %MaxfuncDepth:2
% 281.52/281.59 %SharedTerms:40
% 281.52/281.59 %goalClause: 30 31 32 33 34 40 41 42 43 44 45 46 47 75
% 281.52/281.59 %singleGoalClaCount:12
% 281.52/281.59 [30]P1(a1)
% 281.52/281.59 [31]P6(a1)
% 281.52/281.59 [33]P2(a3,a12)
% 281.52/281.59 [34]P2(a4,a12)
% 281.52/281.59 [35]P2(a5,a13)
% 281.52/281.59 [36]P2(a8,a5)
% 281.52/281.59 [37]P2(a9,a5)
% 281.52/281.59 [38]P2(a6,a8)
% 281.52/281.59 [39]P2(a6,a9)
% 281.52/281.59 [40]P2(a14,a12)
% 281.52/281.59 [32]E(f2(a1,a11),a12)
% 281.52/281.59 [41]P9(f2(a1,a15),a3)
% 281.52/281.59 [42]P9(f2(a1,a15),a4)
% 281.52/281.59 [43]P9(f2(a1,a15),a14)
% 281.52/281.59 [44]P2(f2(a1,a16),a3)
% 281.52/281.59 [45]P2(f2(a1,a16),a4)
% 281.52/281.59 [46]P2(f2(a1,a16),a14)
% 281.52/281.59 [47]P10(a1)+P3(a1)
% 281.52/281.59 [75]~P2(f7(a1,a16),f7(a1,a15))+~E(f7(a1,a15),f7(a1,a11))
% 281.52/281.59 [48]~P1(x481)+P6(x481)
% 281.52/281.59 [49]~E(x491,x492)+P9(x491,x492)
% 281.52/281.59 [50]~E(x501,x502)+P5(x501,x502)
% 281.52/281.59 [52]~P12(x521,x522)+P9(x521,x522)
% 281.52/281.59 [53]~P2(x532,x531)+P12(x531,x532)
% 281.52/281.59 [54]~P2(x541,x542)+P5(x541,x542)
% 281.52/281.59 [55]~P12(x552,x551)+P2(x551,x552)
% 281.52/281.59 [60]~P2(x602,x601)+~P2(x601,x602)
% 281.52/281.59 [68]P6(x681)+~P4(x681,x682,x683)
% 281.52/281.59 [51]P12(x511,x512)+P2(x511,x512)+E(x511,x512)
% 281.52/281.59 [56]P12(x561,x562)+~P9(x561,x562)+E(x561,x562)
% 281.52/281.59 [57]P2(x571,x572)+~P5(x571,x572)+E(x571,x572)
% 281.52/281.59 [58]~P6(x581)+~P7(x581,x582)+E(f7(x581,x582),a13)
% 281.52/281.59 [59]~P6(x591)+P8(x591,x592)+~E(f2(x591,x592),a12)
% 281.52/281.59 [66]~P1(x661)+P7(x661,x662)+~P9(f2(x661,x662),a3)
% 281.52/281.59 [69]~P1(x691)+~P7(x691,x692)+~P2(f2(x691,x692),a3)
% 281.52/281.59 [61]~P2(x611,x613)+P2(x611,x612)+~P2(x613,x612)
% 281.52/281.59 [74]~P4(x741,x743,x742)+P8(x741,x742)+P8(x741,x743)
% 281.52/281.59 [76]~P4(x761,x763,x762)+~P8(x761,x762)+~P8(x761,x763)
% 281.52/281.59 [67]~P6(x671)+P1(x671)+P7(x671,f10(x671))+P9(f2(x671,f10(x671)),a3)
% 281.52/281.59 [70]~P6(x701)+P1(x701)+~P7(x701,f10(x701))+P2(f2(x701,f10(x701)),a3)
% 281.52/281.59 [73]~P6(x731)+P1(x731)+P9(f2(x731,f10(x731)),a3)+P2(f2(x731,f10(x731)),a3)
% 281.52/281.59 [71]~P6(x711)+~P8(x711,x713)+P8(x711,x712)+P4(x711,x712,x713)
% 281.52/281.59 [72]~P6(x721)+~P8(x721,x723)+P8(x721,x722)+P4(x721,x723,x722)
% 281.52/281.60 [77]~P6(x771)+P4(x771,x772,x773)+~E(f2(x771,x772),a12)+~P2(f2(x771,x773),a4)
% 281.52/281.60 [78]~P6(x781)+~P4(x781,x783,x782)+P2(f2(x781,x782),a4)+~E(f2(x781,x783),a12)
% 281.52/281.60 [62]P7(x621,x622)+P8(x621,x622)+P11(x621,x622)+~P6(x621)+E(f7(x621,x622),a6)
% 281.52/281.60 [63]P7(x631,x632)+P8(x631,x632)+~P6(x631)+~P11(x631,x632)+E(f7(x631,x632),a8)
% 281.52/281.60 [64]P7(x641,x642)+P11(x641,x642)+~P6(x641)+~P8(x641,x642)+E(f7(x641,x642),a9)
% 281.52/281.60 [65]P7(x651,x652)+~P6(x651)+~P8(x651,x652)+~P11(x651,x652)+E(f7(x651,x652),a5)
% 281.52/281.60 %EqnAxiom
% 281.52/281.60 [1]E(x11,x11)
% 281.52/281.60 [2]E(x22,x21)+~E(x21,x22)
% 281.52/281.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 281.52/281.60 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 281.52/281.60 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 281.52/281.60 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63))
% 281.52/281.60 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72))
% 281.52/281.60 [8]~E(x81,x82)+E(f10(x81),f10(x82))
% 281.52/281.60 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 281.52/281.60 [10]~P6(x101)+P6(x102)+~E(x101,x102)
% 281.52/281.60 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 281.52/281.60 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 281.52/281.60 [13]P8(x132,x133)+~E(x131,x132)+~P8(x131,x133)
% 281.52/281.60 [14]P8(x143,x142)+~E(x141,x142)+~P8(x143,x141)
% 281.52/281.60 [15]P11(x152,x153)+~E(x151,x152)+~P11(x151,x153)
% 281.52/281.60 [16]P11(x163,x162)+~E(x161,x162)+~P11(x163,x161)
% 281.52/281.60 [17]P4(x172,x173,x174)+~E(x171,x172)+~P4(x171,x173,x174)
% 281.52/281.60 [18]P4(x183,x182,x184)+~E(x181,x182)+~P4(x183,x181,x184)
% 281.52/281.60 [19]P4(x193,x194,x192)+~E(x191,x192)+~P4(x193,x194,x191)
% 281.52/281.60 [20]P7(x202,x203)+~E(x201,x202)+~P7(x201,x203)
% 281.52/281.60 [21]P7(x213,x212)+~E(x211,x212)+~P7(x213,x211)
% 281.52/281.60 [22]P9(x222,x223)+~E(x221,x222)+~P9(x221,x223)
% 281.52/281.60 [23]P9(x233,x232)+~E(x231,x232)+~P9(x233,x231)
% 281.52/281.60 [24]P12(x242,x243)+~E(x241,x242)+~P12(x241,x243)
% 281.52/281.60 [25]P12(x253,x252)+~E(x251,x252)+~P12(x253,x251)
% 281.52/281.60 [26]~P3(x261)+P3(x262)+~E(x261,x262)
% 281.52/281.60 [27]~P10(x271)+P10(x272)+~E(x271,x272)
% 281.52/281.60 [28]P5(x282,x283)+~E(x281,x282)+~P5(x281,x283)
% 281.52/281.60 [29]P5(x293,x292)+~E(x291,x292)+~P5(x293,x291)
% 281.52/281.60
% 281.52/281.60 %-------------------------------------------
% 281.52/281.60 cnf(79,plain,
% 281.52/281.60 (P9(x791,x791)),
% 281.52/281.60 inference(equality_inference,[],[49])).
% 281.52/281.60 cnf(80,plain,
% 281.52/281.60 (P5(x801,x801)),
% 281.52/281.60 inference(equality_inference,[],[50])).
% 281.52/281.60 cnf(81,plain,
% 281.52/281.60 (E(a12,f2(a1,a11))),
% 281.52/281.60 inference(scs_inference,[],[32,2])).
% 281.52/281.60 cnf(84,plain,
% 281.52/281.60 (P8(a1,a11)),
% 281.52/281.60 inference(scs_inference,[],[31,33,32,2,60,59])).
% 281.52/281.60 cnf(86,plain,
% 281.52/281.60 (P7(a1,a15)),
% 281.52/281.60 inference(scs_inference,[],[30,31,33,32,41,2,60,59,66])).
% 281.52/281.60 cnf(88,plain,
% 281.52/281.60 (~P7(a1,a16)),
% 281.52/281.60 inference(scs_inference,[],[30,31,33,32,41,44,2,60,59,66,69])).
% 281.63/281.60 cnf(91,plain,
% 281.63/281.60 (P2(a3,f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[30,31,33,32,41,44,2,60,59,66,69,11,12])).
% 281.63/281.60 cnf(92,plain,
% 281.63/281.60 (P2(f2(a1,a16),a12)),
% 281.63/281.60 inference(scs_inference,[],[30,31,33,32,41,44,2,60,59,66,69,11,12,61])).
% 281.63/281.60 cnf(96,plain,
% 281.63/281.60 (~E(a15,a16)),
% 281.63/281.60 inference(scs_inference,[],[30,31,33,32,41,44,2,60,59,66,69,11,12,61,76,21])).
% 281.63/281.60 cnf(98,plain,
% 281.63/281.60 (P9(x981,x981)),
% 281.63/281.60 inference(rename_variables,[],[79])).
% 281.63/281.60 cnf(102,plain,
% 281.63/281.60 (P5(x1021,x1021)),
% 281.63/281.60 inference(rename_variables,[],[80])).
% 281.63/281.60 cnf(105,plain,
% 281.63/281.60 (P4(a1,a11,a16)),
% 281.63/281.60 inference(scs_inference,[],[30,31,33,45,32,41,44,79,98,80,102,2,60,59,66,69,11,12,61,76,21,22,23,28,29,77])).
% 281.63/281.60 cnf(109,plain,
% 281.63/281.60 (~E(f2(a1,a16),f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[30,31,33,45,32,41,44,79,98,80,102,2,60,59,66,69,11,12,61,76,21,22,23,28,29,77,55,3])).
% 281.63/281.60 cnf(115,plain,
% 281.63/281.60 (E(f2(a1,a15),a14)+P12(f2(a1,a15),a14)),
% 281.63/281.60 inference(scs_inference,[],[30,31,33,43,45,32,41,44,79,98,80,102,2,60,59,66,69,11,12,61,76,21,22,23,28,29,77,55,3,9,19,10,51,56])).
% 281.63/281.60 cnf(123,plain,
% 281.63/281.60 (P2(a4,f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[34,81,60,12])).
% 281.63/281.60 cnf(124,plain,
% 281.63/281.60 (~P2(a12,f2(a1,a16))),
% 281.63/281.60 inference(scs_inference,[],[34,45,81,60,12,61])).
% 281.63/281.60 cnf(140,plain,
% 281.63/281.60 (~P2(a3,f2(a1,a16))),
% 281.63/281.60 inference(scs_inference,[],[44,124,55,60])).
% 281.63/281.60 cnf(142,plain,
% 281.63/281.60 (P2(f2(a1,a16),f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[44,91,124,55,60,61])).
% 281.63/281.60 cnf(144,plain,
% 281.63/281.60 (P2(a14,f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[44,40,81,91,124,55,60,61,12])).
% 281.63/281.60 cnf(153,plain,
% 281.63/281.60 (~P2(a4,f2(a1,a16))),
% 281.63/281.60 inference(scs_inference,[],[45,140,55,60])).
% 281.63/281.60 cnf(155,plain,
% 281.63/281.60 (P2(a8,a13)),
% 281.63/281.60 inference(scs_inference,[],[45,140,35,36,55,60,61])).
% 281.63/281.60 cnf(173,plain,
% 281.63/281.60 (~P2(a14,f2(a1,a16))),
% 281.63/281.60 inference(scs_inference,[],[46,153,55,60])).
% 281.63/281.60 cnf(191,plain,
% 281.63/281.60 (~P2(a12,a14)),
% 281.63/281.60 inference(scs_inference,[],[40,173,55,60])).
% 281.63/281.60 cnf(193,plain,
% 281.63/281.60 (P2(a6,a13)),
% 281.63/281.60 inference(scs_inference,[],[40,173,38,155,55,60,61])).
% 281.63/281.60 cnf(201,plain,
% 281.63/281.60 (~P2(f2(a1,a11),a4)),
% 281.63/281.60 inference(scs_inference,[],[123,191,55,60])).
% 281.63/281.60 cnf(210,plain,
% 281.63/281.60 (~P2(f2(a1,a11),a14)),
% 281.63/281.60 inference(scs_inference,[],[144,201,55,60])).
% 281.63/281.60 cnf(212,plain,
% 281.63/281.60 (~P2(f2(a1,a11),f2(a1,a16))),
% 281.63/281.60 inference(scs_inference,[],[45,144,201,55,60,61])).
% 281.63/281.60 cnf(224,plain,
% 281.63/281.60 (~P12(f2(a1,a16),f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[212,55])).
% 281.63/281.60 cnf(226,plain,
% 281.63/281.60 (~P2(f2(a1,a11),a3)),
% 281.63/281.60 inference(scs_inference,[],[91,212,55,60])).
% 281.63/281.60 cnf(234,plain,
% 281.63/281.60 (~P2(a13,a8)),
% 281.63/281.60 inference(scs_inference,[],[155,210,55,60])).
% 281.63/281.60 cnf(236,plain,
% 281.63/281.60 (~E(a6,a13)),
% 281.63/281.60 inference(scs_inference,[],[155,210,38,55,60,11])).
% 281.63/281.60 cnf(237,plain,
% 281.63/281.60 (~P2(a13,a6)),
% 281.63/281.60 inference(scs_inference,[],[155,210,38,55,60,11,61])).
% 281.63/281.60 cnf(247,plain,
% 281.63/281.60 (~P2(a13,a5)),
% 281.63/281.60 inference(scs_inference,[],[35,226,55,60])).
% 281.63/281.60 cnf(249,plain,
% 281.63/281.60 (~E(a8,a13)),
% 281.63/281.60 inference(scs_inference,[],[35,36,226,55,60,11])).
% 281.63/281.60 cnf(256,plain,
% 281.63/281.60 (~P2(a5,a9)),
% 281.63/281.60 inference(scs_inference,[],[37,237,55,60])).
% 281.63/281.60 cnf(258,plain,
% 281.63/281.60 (P2(a9,a13)),
% 281.63/281.60 inference(scs_inference,[],[37,35,237,55,60,61])).
% 281.63/281.60 cnf(260,plain,
% 281.63/281.60 (~E(a9,a13)),
% 281.63/281.60 inference(scs_inference,[],[37,35,237,247,55,60,61,11])).
% 281.63/281.60 cnf(261,plain,
% 281.63/281.60 (~E(a13,a9)),
% 281.63/281.60 inference(scs_inference,[],[37,35,237,247,55,60,61,11,12])).
% 281.63/281.60 cnf(262,plain,
% 281.63/281.60 (E(a13,a6)+P12(a13,a6)),
% 281.63/281.60 inference(scs_inference,[],[37,35,237,247,55,60,61,11,12,51])).
% 281.63/281.60 cnf(265,plain,
% 281.63/281.60 (~P12(a8,a13)),
% 281.63/281.60 inference(scs_inference,[],[234,55])).
% 281.63/281.60 cnf(267,plain,
% 281.63/281.60 (~P2(a5,a8)),
% 281.63/281.60 inference(scs_inference,[],[36,234,55,60])).
% 281.63/281.60 cnf(269,plain,
% 281.63/281.60 (~P2(a5,a6)),
% 281.63/281.60 inference(scs_inference,[],[36,234,256,39,55,60,61])).
% 281.63/281.60 cnf(279,plain,
% 281.63/281.60 (~P2(a8,a6)),
% 281.63/281.60 inference(scs_inference,[],[38,267,55,60])).
% 281.63/281.60 cnf(281,plain,
% 281.63/281.60 (~E(a13,a8)),
% 281.63/281.60 inference(scs_inference,[],[35,38,267,55,60,12])).
% 281.63/281.60 cnf(292,plain,
% 281.63/281.60 (P12(a13,a8)),
% 281.63/281.60 inference(scs_inference,[],[39,269,281,234,55,60,51])).
% 281.63/281.60 cnf(295,plain,
% 281.63/281.60 (P12(a13,a6)),
% 281.63/281.60 inference(scs_inference,[],[35,39,269,281,234,55,60,51,12,262])).
% 281.63/281.60 cnf(296,plain,
% 281.63/281.60 (P12(x2961,a8)+~E(a13,x2961)),
% 281.63/281.60 inference(scs_inference,[],[35,39,269,281,234,55,60,51,12,262,24])).
% 281.63/281.60 cnf(301,plain,
% 281.63/281.60 (~P12(a6,a8)),
% 281.63/281.60 inference(scs_inference,[],[279,55])).
% 281.63/281.60 cnf(303,plain,
% 281.63/281.60 (~P2(a13,a9)),
% 281.63/281.60 inference(scs_inference,[],[258,279,55,60])).
% 281.63/281.60 cnf(305,plain,
% 281.63/281.60 (P12(a13,a9)),
% 281.63/281.60 inference(scs_inference,[],[258,261,279,55,60,51])).
% 281.63/281.60 cnf(324,plain,
% 281.63/281.60 (~P12(a9,a13)),
% 281.63/281.60 inference(scs_inference,[],[303,55])).
% 281.63/281.60 cnf(330,plain,
% 281.63/281.60 (~P12(a5,a13)),
% 281.63/281.60 inference(scs_inference,[],[247,55])).
% 281.63/281.60 cnf(474,plain,
% 281.63/281.60 (~P2(a13,f2(a1,a16))+~E(a6,a12)),
% 281.63/281.60 inference(scs_inference,[],[32,41,105,92,191,193,11,12,60,9,56,18,61])).
% 281.63/281.60 cnf(629,plain,
% 281.63/281.60 (~E(a12,a6)+~P2(a13,f2(a1,a16))),
% 281.63/281.60 inference(scs_inference,[],[474,2])).
% 281.63/281.60 cnf(655,plain,
% 281.63/281.60 (~P12(f2(a1,a16),a13)+~E(a12,a6)),
% 281.63/281.60 inference(scs_inference,[],[629,55])).
% 281.63/281.60 cnf(672,plain,
% 281.63/281.60 (~E(a6,a12)+~P12(f2(a1,a16),a13)),
% 281.63/281.60 inference(scs_inference,[],[655,2])).
% 281.63/281.60 cnf(684,plain,
% 281.63/281.60 (~E(a6,f2(a1,a11))+~P12(f2(a1,a16),a13)),
% 281.63/281.60 inference(scs_inference,[],[32,672,3])).
% 281.63/281.60 cnf(691,plain,
% 281.63/281.60 (P12(f2(a1,a15),a14)+E(f2(f2(a1,a15),x6911),f2(a14,x6911))),
% 281.63/281.60 inference(scs_inference,[],[115,4])).
% 281.63/281.60 cnf(747,plain,
% 281.63/281.60 (~P2(a13,f2(a1,a16))+~E(a6,f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[684,53])).
% 281.63/281.60 cnf(763,plain,
% 281.63/281.60 (~P2(x7631,f2(a1,a16))+~E(x7631,a13)+~E(a6,f2(a1,a11))),
% 281.63/281.60 inference(scs_inference,[],[747,11])).
% 281.63/281.60 cnf(788,plain,
% 281.63/281.60 (P2(a14,f2(a1,a15))+E(f2(f2(a1,a15),x7881),f2(a14,x7881))),
% 281.63/281.60 inference(scs_inference,[],[691,55])).
% 281.63/281.60 cnf(798,plain,
% 281.63/281.60 (P9(f2(f2(a1,a15),x7981),f2(a14,x7981))+P2(a14,f2(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[788,49])).
% 281.63/281.60 cnf(803,plain,
% 281.63/281.60 (P9(x8031,f2(a14,x8032))+~E(f2(f2(a1,a15),x8032),x8031)+P2(a14,f2(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[798,22])).
% 281.63/281.60 cnf(932,plain,
% 281.63/281.60 (E(f7(a1,a15),a13)),
% 281.63/281.60 inference(scs_inference,[],[30,86,48,58])).
% 281.63/281.60 cnf(933,plain,
% 281.63/281.60 (E(a13,f7(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[932,2])).
% 281.63/281.60 cnf(934,plain,
% 281.63/281.60 (~E(a9,f7(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[260,932,2,3])).
% 281.63/281.60 cnf(935,plain,
% 281.63/281.60 (P12(f7(a1,a15),a6)),
% 281.63/281.60 inference(scs_inference,[],[260,932,295,2,3,24])).
% 281.63/281.60 cnf(936,plain,
% 281.63/281.60 (P2(a6,f7(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[260,932,193,295,2,3,24,12])).
% 281.63/281.60 cnf(937,plain,
% 281.63/281.60 (P12(f7(a1,a15),a8)),
% 281.63/281.60 inference(scs_inference,[],[260,932,193,295,2,3,24,12,296])).
% 281.63/281.60 cnf(938,plain,
% 281.63/281.60 (~P2(f7(a1,a15),a6)),
% 281.63/281.60 inference(scs_inference,[],[260,932,193,295,2,3,24,12,296,60])).
% 281.63/281.60 cnf(942,plain,
% 281.63/281.60 (~P12(a6,f7(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[260,932,193,295,2,3,24,12,296,60,763,55])).
% 281.63/281.60 cnf(952,plain,
% 281.63/281.60 (~E(a6,f7(a1,a15))),
% 281.63/281.60 inference(scs_inference,[],[236,932,3])).
% 281.63/281.60 cnf(953,plain,
% 281.63/281.60 (~E(f7(a1,a15),a6)),
% 281.63/281.60 inference(scs_inference,[],[236,932,301,937,3,24])).
% 281.63/281.60 cnf(955,plain,
% 281.63/281.61 (~P2(x9551,a6)+P2(x9551,f7(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[936,933,236,932,301,937,3,24,9,61])).
% 281.63/281.61 cnf(961,plain,
% 281.63/281.61 (P2(x9611,f7(a1,a15))+~E(a6,x9611)),
% 281.63/281.61 inference(scs_inference,[],[936,933,236,932,301,935,937,3,24,9,61,27,25,10,26,11])).
% 281.63/281.61 cnf(2696,plain,
% 281.63/281.61 (E(f2(a13,x26961),f2(f7(a1,a15),x26961))),
% 281.63/281.61 inference(scs_inference,[],[935,258,933,52,54,8,4])).
% 281.63/281.61 cnf(2697,plain,
% 281.63/281.61 (E(f7(a13,x26971),f7(f7(a1,a15),x26971))),
% 281.63/281.61 inference(scs_inference,[],[935,258,933,52,54,8,4,6])).
% 281.63/281.61 cnf(2698,plain,
% 281.63/281.61 (E(f7(x26981,a13),f7(x26981,f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[935,258,933,52,54,8,4,6,7])).
% 281.63/281.61 cnf(2699,plain,
% 281.63/281.61 (P12(f2(a1,a11),a4)),
% 281.63/281.61 inference(scs_inference,[],[935,258,123,933,52,54,8,4,6,7,53])).
% 281.63/281.61 cnf(2701,plain,
% 281.63/281.61 (E(f2(x27011,a13),f2(x27011,f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[935,258,123,933,52,54,8,4,6,7,53,5])).
% 281.63/281.61 cnf(2703,plain,
% 281.63/281.61 (P2(a8,f7(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[96,935,258,123,937,933,52,54,8,4,6,7,53,5,2,55])).
% 281.63/281.61 cnf(2708,plain,
% 281.63/281.61 (~P8(a1,a16)),
% 281.63/281.61 inference(scs_inference,[],[96,952,942,281,935,258,123,937,933,105,84,52,54,8,4,6,7,53,5,2,55,3,56,76])).
% 281.63/281.61 cnf(2710,plain,
% 281.63/281.61 (~P2(f2(a1,a15),a3)),
% 281.63/281.61 inference(scs_inference,[],[30,96,952,942,281,935,258,123,937,933,86,105,84,52,54,8,4,6,7,53,5,2,55,3,56,76,69])).
% 281.63/281.61 cnf(2729,plain,
% 281.63/281.61 (~E(a3,f2(a1,a16))),
% 281.63/281.61 inference(scs_inference,[],[30,96,952,942,938,330,281,303,935,258,123,937,88,79,933,86,932,105,84,953,31,52,54,8,4,6,7,53,5,2,55,3,56,76,69,11,66,57,25,28,23,71,49,50,60,16,22])).
% 281.63/281.61 cnf(2731,plain,
% 281.63/281.61 (P2(a9,f7(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[30,96,952,942,938,330,281,303,935,258,123,937,88,79,933,86,932,105,84,953,31,52,54,8,4,6,7,53,5,2,55,3,56,76,69,11,66,57,25,28,23,71,49,50,60,16,22,12])).
% 281.63/281.61 cnf(2740,plain,
% 281.63/281.61 (P12(f7(a1,a15),a9)),
% 281.63/281.61 inference(scs_inference,[],[2731,53])).
% 281.63/281.61 cnf(2746,plain,
% 281.63/281.61 (E(f7(x27461,f7(a1,a15)),f7(x27461,a13))),
% 281.63/281.61 inference(scs_inference,[],[2699,2731,2697,932,53,49,52,7])).
% 281.63/281.61 cnf(2747,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),x27471),f2(a13,x27471))),
% 281.63/281.61 inference(scs_inference,[],[2699,2731,2697,932,53,49,52,7,4])).
% 281.63/281.61 cnf(2748,plain,
% 281.63/281.61 (E(f10(f7(a1,a15)),f10(a13))),
% 281.63/281.61 inference(scs_inference,[],[2699,2731,2697,932,53,49,52,7,4,8])).
% 281.63/281.61 cnf(2749,plain,
% 281.63/281.61 (P5(f7(a13,x27491),f7(f7(a1,a15),x27491))),
% 281.63/281.61 inference(scs_inference,[],[2699,2731,2697,932,53,49,52,7,4,8,50])).
% 281.63/281.61 cnf(2753,plain,
% 281.63/281.61 (E(f7(f7(a1,a15),x27531),f7(a13,x27531))),
% 281.63/281.61 inference(scs_inference,[],[2699,2731,2697,932,53,49,52,7,4,8,50,54,6])).
% 281.63/281.61 cnf(2755,plain,
% 281.63/281.61 (E(f2(x27551,f7(a1,a15)),f2(x27551,a13))),
% 281.63/281.61 inference(scs_inference,[],[934,2699,2731,2697,932,53,49,52,7,4,8,50,54,6,2,5])).
% 281.63/281.61 cnf(2758,plain,
% 281.63/281.61 (E(f7(a13,a13),f7(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[934,2699,2731,2697,2698,324,260,932,53,49,52,7,4,8,50,54,6,2,5,56,3])).
% 281.63/281.61 cnf(2759,plain,
% 281.63/281.61 (E(f7(a13,x27591),f7(f7(a1,a15),x27591))),
% 281.63/281.61 inference(rename_variables,[],[2697])).
% 281.63/281.61 cnf(2761,plain,
% 281.63/281.61 (P12(a12,a4)),
% 281.63/281.61 inference(scs_inference,[],[934,2699,2731,2697,2698,324,260,932,32,53,49,52,7,4,8,50,54,6,2,5,56,3,24])).
% 281.63/281.61 cnf(2764,plain,
% 281.63/281.61 (~P12(a9,f7(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[934,2699,2731,2697,2759,2698,324,260,79,932,32,53,49,52,7,4,8,50,54,6,2,5,56,3,24,22,25])).
% 281.63/281.61 cnf(2775,plain,
% 281.63/281.61 (P12(a14,f2(a1,a16))),
% 281.63/281.61 inference(scs_inference,[],[46,53])).
% 281.63/281.61 cnf(2781,plain,
% 281.63/281.61 (P9(f7(x27811,f7(a1,a15)),f7(x27811,a13))),
% 281.63/281.61 inference(scs_inference,[],[2761,2746,46,53,52,50,49])).
% 281.63/281.61 cnf(2785,plain,
% 281.63/281.61 (E(f7(x27851,a12),f7(x27851,f2(a1,a11)))),
% 281.63/281.61 inference(scs_inference,[],[2761,2746,2703,46,81,53,52,50,49,54,7])).
% 281.63/281.61 cnf(2786,plain,
% 281.63/281.61 (E(f10(a12),f10(f2(a1,a11)))),
% 281.63/281.61 inference(scs_inference,[],[2761,2746,2703,46,81,53,52,50,49,54,7,8])).
% 281.63/281.61 cnf(2787,plain,
% 281.63/281.61 (E(f7(a12,x27871),f7(f2(a1,a11),x27871))),
% 281.63/281.61 inference(scs_inference,[],[2761,2746,2703,46,81,53,52,50,49,54,7,8,6])).
% 281.63/281.61 cnf(2788,plain,
% 281.63/281.61 (E(f2(a12,x27881),f2(f2(a1,a11),x27881))),
% 281.63/281.61 inference(scs_inference,[],[2761,2746,2703,46,81,53,52,50,49,54,7,8,6,4])).
% 281.63/281.61 cnf(2790,plain,
% 281.63/281.61 (E(f2(x27901,a12),f2(x27901,f2(a1,a11)))),
% 281.63/281.61 inference(scs_inference,[],[2761,2729,2746,2703,46,81,53,52,50,49,54,7,8,6,4,2,5])).
% 281.63/281.61 cnf(2793,plain,
% 281.63/281.61 (E(f7(f7(a1,a15),f7(a1,a15)),f7(a13,a13))),
% 281.63/281.61 inference(scs_inference,[],[2761,2729,2764,2746,2753,2703,934,46,81,53,52,50,49,54,7,8,6,4,2,5,56,3])).
% 281.63/281.61 cnf(2818,plain,
% 281.63/281.61 (E(f7(x28181,f2(a1,a11)),f7(x28181,a12))),
% 281.63/281.61 inference(scs_inference,[],[2775,2793,144,32,53,50,49,52,7])).
% 281.63/281.61 cnf(2819,plain,
% 281.63/281.61 (E(f10(f2(a1,a11)),f10(a12))),
% 281.63/281.61 inference(scs_inference,[],[2775,2793,144,32,53,50,49,52,7,8])).
% 281.63/281.61 cnf(2822,plain,
% 281.63/281.61 (E(f2(f2(a1,a11),x28221),f2(a12,x28221))),
% 281.63/281.61 inference(scs_inference,[],[2775,2793,155,144,32,53,50,49,52,7,8,54,4])).
% 281.63/281.61 cnf(2823,plain,
% 281.63/281.61 (E(f7(f2(a1,a11),x28231),f7(a12,x28231))),
% 281.63/281.61 inference(scs_inference,[],[2775,2793,155,144,32,53,50,49,52,7,8,54,4,6])).
% 281.63/281.61 cnf(2824,plain,
% 281.63/281.61 (E(f2(x28241,f2(a1,a11)),f2(x28241,a12))),
% 281.63/281.61 inference(scs_inference,[],[2775,2793,155,144,32,53,50,49,52,7,8,54,4,6,5])).
% 281.63/281.61 cnf(2825,plain,
% 281.63/281.61 (~P2(f2(a1,a15),f2(a1,a16))),
% 281.63/281.61 inference(scs_inference,[],[2775,2710,2793,155,144,44,32,53,50,49,52,7,8,54,4,6,5,61])).
% 281.63/281.61 cnf(2847,plain,
% 281.63/281.61 (P12(f2(a1,a11),a3)),
% 281.63/281.61 inference(scs_inference,[],[91,53])).
% 281.63/281.61 cnf(2859,plain,
% 281.63/281.61 (E(f7(f2(a1,a11),f2(a1,a11)),f7(a12,a12))),
% 281.63/281.61 inference(scs_inference,[],[2748,2818,2823,2740,224,109,123,91,53,49,52,50,54,56,3])).
% 281.63/281.61 cnf(2873,plain,
% 281.63/281.61 (P9(f2(a1,a11),a3)),
% 281.63/281.61 inference(scs_inference,[],[2847,40,53,52])).
% 281.63/281.61 cnf(2883,plain,
% 281.63/281.61 (E(f2(f2(a1,a11),f2(a1,a11)),f2(a12,a12))),
% 281.63/281.61 inference(scs_inference,[],[2847,2819,2822,2824,249,265,40,53,52,50,49,54,56,3])).
% 281.63/281.61 cnf(2909,plain,
% 281.63/281.61 (E(f2(a13,a12),f2(f7(a1,a15),f2(a1,a11)))),
% 281.63/281.61 inference(scs_inference,[],[2883,2859,2790,2696,292,936,37,80,53,50,49,52,54,29,3])).
% 281.63/281.61 cnf(2922,plain,
% 281.63/281.61 (P12(a5,a8)),
% 281.63/281.61 inference(scs_inference,[],[2786,36,49,53])).
% 281.63/281.61 cnf(2926,plain,
% 281.63/281.61 (P5(f7(a12,x29261),f7(f2(a1,a11),x29261))),
% 281.63/281.61 inference(scs_inference,[],[2786,2787,305,36,49,53,52,50])).
% 281.63/281.61 cnf(2952,plain,
% 281.63/281.61 (P9(f7(a13,a13),f7(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[2922,2758,52,49])).
% 281.63/281.61 cnf(2954,plain,
% 281.63/281.61 (P12(a12,a3)),
% 281.63/281.61 inference(scs_inference,[],[2922,2758,33,52,49,53])).
% 281.63/281.61 cnf(2967,plain,
% 281.63/281.61 (P12(a9,a6)),
% 281.63/281.61 inference(scs_inference,[],[39,53])).
% 281.63/281.61 cnf(2971,plain,
% 281.63/281.61 (P9(f7(x29711,f2(a1,a11)),f7(x29711,a12))),
% 281.63/281.61 inference(scs_inference,[],[2954,2818,39,53,52,49])).
% 281.63/281.61 cnf(2975,plain,
% 281.63/281.61 (P5(f7(x29751,f2(a1,a11)),f7(x29751,a12))),
% 281.63/281.61 inference(scs_inference,[],[2954,2818,144,39,53,52,49,54,50])).
% 281.63/281.61 cnf(2977,plain,
% 281.63/281.61 (~E(f2(a1,a16),f2(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[2954,2818,2710,144,39,44,53,52,49,54,50,11])).
% 281.63/281.61 cnf(2979,plain,
% 281.63/281.61 (~E(f2(a1,a15),f2(a1,a16))),
% 281.63/281.61 inference(scs_inference,[],[2954,2818,2710,265,144,39,44,932,53,52,49,54,50,11,25,2])).
% 281.63/281.61 cnf(2986,plain,
% 281.63/281.61 (P9(f7(f2(a1,a11),x29861),f7(a12,x29861))),
% 281.63/281.61 inference(scs_inference,[],[2823,49])).
% 281.63/281.61 cnf(2988,plain,
% 281.63/281.61 (P12(a8,a6)),
% 281.63/281.61 inference(scs_inference,[],[2823,38,49,53])).
% 281.63/281.61 cnf(2992,plain,
% 281.63/281.61 (P5(f2(f2(a1,a11),x29921),f2(a12,x29921))),
% 281.63/281.61 inference(scs_inference,[],[2967,2822,2823,38,49,53,52,50])).
% 281.63/281.61 cnf(3000,plain,
% 281.63/281.61 (P2(f2(a1,a16),f2(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[2967,2979,2822,2823,2825,34,38,49,53,52,50,54,51,57,55])).
% 281.63/281.61 cnf(3012,plain,
% 281.63/281.61 (P12(a13,a5)),
% 281.63/281.61 inference(scs_inference,[],[2988,2824,35,52,49,53])).
% 281.63/281.61 cnf(3020,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),f2(a1,a11)),f2(a13,a12))),
% 281.63/281.61 inference(scs_inference,[],[2988,3000,2824,938,2747,35,52,49,53,54,50,61,3])).
% 281.63/281.61 cnf(3026,plain,
% 281.63/281.61 (P12(a4,f2(a1,a16))),
% 281.63/281.61 inference(scs_inference,[],[45,53])).
% 281.63/281.61 cnf(3042,plain,
% 281.63/281.61 (P12(f7(a1,a15),a5)),
% 281.63/281.61 inference(scs_inference,[],[3012,2992,3020,2859,2755,91,45,79,933,53,52,49,50,54,29,23,17,24])).
% 281.63/281.61 cnf(3049,plain,
% 281.63/281.61 (P2(a5,f7(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[3042,55])).
% 281.63/281.61 cnf(3057,plain,
% 281.63/281.61 (P5(f7(x30571,a13),f7(x30571,f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[3026,3042,2698,2788,37,55,49,52,54,50])).
% 281.63/281.61 cnf(3161,plain,
% 281.63/281.61 (E(f7(f2(a1,a11),f7(a1,a15)),f7(a12,a13))),
% 281.63/281.61 inference(scs_inference,[],[2909,2823,2696,2746,38,50,49,54,3])).
% 281.63/281.61 cnf(3189,plain,
% 281.63/281.61 (P9(f2(f7(a1,a15),x31891),f2(a13,x31891))),
% 281.63/281.61 inference(scs_inference,[],[2788,2747,50,49])).
% 281.63/281.61 cnf(3195,plain,
% 281.63/281.61 (~P9(f2(a1,a16),f2(a1,a15))+P12(f2(a1,a16),f2(a1,a15))),
% 281.63/281.61 inference(scs_inference,[],[3161,2781,2977,2788,2747,142,50,49,54,22,56])).
% 281.63/281.61 cnf(3204,plain,
% 281.63/281.61 (P5(f7(f2(a1,a11),x32041),f7(a12,x32041))),
% 281.63/281.61 inference(scs_inference,[],[2823,50])).
% 281.63/281.61 cnf(3206,plain,
% 281.63/281.61 (P9(f7(a12,x32061),f7(f2(a1,a11),x32061))),
% 281.63/281.61 inference(scs_inference,[],[2823,2787,50,49])).
% 281.63/281.61 cnf(3231,plain,
% 281.63/281.61 (P5(f2(x32311,f7(a1,a15)),f2(x32311,a13))),
% 281.63/281.61 inference(scs_inference,[],[2755,50])).
% 281.63/281.61 cnf(3820,plain,
% 281.63/281.61 (E(f2(a13,a13),f2(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[2696,2701,3])).
% 281.63/281.61 cnf(5674,plain,
% 281.63/281.61 (E(f7(x56741,f7(f2(a1,a11),f7(a1,a15))),f7(x56741,f7(a12,a13)))),
% 281.63/281.61 inference(scs_inference,[],[3161,7])).
% 281.63/281.61 cnf(5676,plain,
% 281.63/281.61 (E(f7(f7(f2(a1,a11),f7(a1,a15)),x56761),f7(f7(a12,a13),x56761))),
% 281.63/281.61 inference(scs_inference,[],[3161,7,8,6])).
% 281.63/281.61 cnf(5677,plain,
% 281.63/281.61 (E(f2(f7(f2(a1,a11),f7(a1,a15)),x56771),f2(f7(a12,a13),x56771))),
% 281.63/281.61 inference(scs_inference,[],[3161,7,8,6,4])).
% 281.63/281.61 cnf(5678,plain,
% 281.63/281.61 (E(f2(x56781,f7(f2(a1,a11),f7(a1,a15))),f2(x56781,f7(a12,a13)))),
% 281.63/281.61 inference(scs_inference,[],[3161,7,8,6,4,5])).
% 281.63/281.61 cnf(5683,plain,
% 281.63/281.61 (E(f7(f7(a1,a15),a12),f7(a13,f2(a1,a11)))),
% 281.63/281.61 inference(scs_inference,[],[3204,3161,2753,2785,7,8,6,4,5,50,29,3])).
% 281.63/281.61 cnf(5686,plain,
% 281.63/281.61 (P9(f7(a12,f7(f2(a1,a11),f7(a1,a15))),f7(a12,f7(a12,a13)))),
% 281.63/281.61 inference(scs_inference,[],[3204,3161,2753,2785,7,8,6,4,5,50,29,3,49])).
% 281.63/281.61 cnf(5688,plain,
% 281.63/281.61 (P9(f7(a12,f7(a12,a13)),f7(f2(a1,a11),f7(f2(a1,a11),f7(a1,a15))))),
% 281.63/281.61 inference(scs_inference,[],[3204,3206,3161,2753,2785,7,8,6,4,5,50,29,3,49,22])).
% 281.63/281.61 cnf(5693,plain,
% 281.63/281.61 (P9(f7(f2(a1,a11),f7(f2(a1,a11),f7(a1,a15))),f7(a12,f7(a12,a13)))),
% 281.63/281.61 inference(scs_inference,[],[3204,2986,3206,3161,2753,2701,2785,7,8,6,4,5,50,29,3,49,22,803,23])).
% 281.63/281.61 cnf(5695,plain,
% 281.63/281.61 (P5(f7(a12,f7(a12,a13)),f7(f2(a1,a11),f7(f2(a1,a11),f7(a1,a15))))),
% 281.63/281.61 inference(scs_inference,[],[3204,2926,2986,3206,3161,2753,2701,2785,7,8,6,4,5,50,29,3,49,22,803,23,28])).
% 281.63/281.61 cnf(5700,plain,
% 281.63/281.61 (E(f7(x57001,f7(f7(a1,a15),a12)),f7(x57001,f7(a13,f2(a1,a11))))),
% 281.63/281.61 inference(scs_inference,[],[5683,49,7])).
% 281.63/281.61 cnf(5704,plain,
% 281.63/281.61 (E(f2(x57041,f7(f7(a1,a15),a12)),f2(x57041,f7(a13,f2(a1,a11))))),
% 281.63/281.61 inference(scs_inference,[],[5683,49,7,8,6,4,5])).
% 281.63/281.61 cnf(5709,plain,
% 281.63/281.61 (E(f7(a13,f2(a1,a11)),f7(f7(a1,a15),a12))),
% 281.63/281.61 inference(scs_inference,[],[5683,2])).
% 281.63/281.61 cnf(5713,plain,
% 281.63/281.61 (P7(a1,a11)),
% 281.63/281.61 inference(scs_inference,[],[30,5683,2825,2873,2,55,3195,66])).
% 281.63/281.61 cnf(5717,plain,
% 281.63/281.61 (E(f7(x57171,a12),f7(x57171,f2(a1,a11)))),
% 281.63/281.61 inference(rename_variables,[],[2785])).
% 281.63/281.61 cnf(5721,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),a13),f2(a13,f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[30,2701,2785,5717,2747,5683,2825,2986,2926,2873,2,55,3195,66,28,23,3])).
% 281.63/281.61 cnf(5744,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),x57441),f2(a13,x57441))),
% 281.63/281.61 inference(rename_variables,[],[2747])).
% 281.63/281.61 cnf(5748,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),a12),f2(a13,f2(a1,a11)))),
% 281.63/281.61 inference(scs_inference,[],[2787,2747,5744,2790,2710,5674,2781,3231,2,55,28,23,3])).
% 281.63/281.61 cnf(5795,plain,
% 281.63/281.61 (E(f7(a12,x57951),f7(f2(a1,a11),x57951))),
% 281.63/281.61 inference(rename_variables,[],[2787])).
% 281.63/281.61 cnf(5799,plain,
% 281.63/281.61 (E(f7(a12,f7(a1,a15)),f7(f2(a1,a11),a13))),
% 281.63/281.61 inference(scs_inference,[],[2701,2787,5795,2746,5676,3189,3057,2,28,23,3])).
% 281.63/281.61 cnf(5815,plain,
% 281.63/281.61 (E(f2(f7(a12,a13),x58151),f2(f7(f2(a1,a11),f7(a1,a15)),x58151))),
% 281.63/281.61 inference(scs_inference,[],[5677,2])).
% 281.63/281.61 cnf(5841,plain,
% 281.63/281.61 (E(f2(x58411,f7(a12,a13)),f2(x58411,f7(f2(a1,a11),f7(a1,a15))))),
% 281.63/281.61 inference(scs_inference,[],[5678,2])).
% 281.63/281.61 cnf(5846,plain,
% 281.63/281.61 (E(f7(a12,x58461),f7(f2(a1,a11),x58461))),
% 281.63/281.61 inference(rename_variables,[],[2787])).
% 281.63/281.61 cnf(5847,plain,
% 281.63/281.61 (E(f7(a12,f7(f2(a1,a11),f7(a1,a15))),f7(f2(a1,a11),f7(a12,a13)))),
% 281.63/281.61 inference(scs_inference,[],[2785,2787,5846,5674,5678,5693,2749,2,28,23,3])).
% 281.63/281.61 cnf(5870,plain,
% 281.63/281.61 (E(f7(a12,x58701),f7(f2(a1,a11),x58701))),
% 281.63/281.61 inference(rename_variables,[],[2787])).
% 281.63/281.61 cnf(5876,plain,
% 281.63/281.61 (P5(f7(a12,f7(a12,a13)),f7(a12,f7(f2(a1,a11),f7(a1,a15))))),
% 281.63/281.61 inference(scs_inference,[],[2785,2787,5870,2823,5676,5721,5686,5695,2,28,23,3,29])).
% 281.63/281.61 cnf(5894,plain,
% 281.63/281.61 (E(f2(f7(f2(a1,a11),f7(a1,a15)),a13),f2(f7(a12,a13),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[2701,2787,2823,5677,5688,5799,5876,2,28,23,3])).
% 281.63/281.61 cnf(5919,plain,
% 281.63/281.61 (E(f2(a13,f2(a1,a11)),f2(f7(a1,a15),a12))),
% 281.63/281.61 inference(scs_inference,[],[5748,2])).
% 281.63/281.61 cnf(5920,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),f7(f2(a1,a11),f7(a1,a15))),f2(a13,f7(a12,a13)))),
% 281.63/281.61 inference(scs_inference,[],[2747,5678,5748,2,3])).
% 281.63/281.61 cnf(5931,plain,
% 281.63/281.61 (E(f7(a12,f7(f7(a1,a15),a12)),f7(f2(a1,a11),f7(a13,f2(a1,a11))))),
% 281.63/281.61 inference(scs_inference,[],[2787,5847,5700,2,3])).
% 281.63/281.61 cnf(5970,plain,
% 281.63/281.61 (E(f2(x59701,f7(a13,f2(a1,a11))),f2(x59701,f7(f7(a1,a15),a12)))),
% 281.63/281.61 inference(scs_inference,[],[5704,2])).
% 281.63/281.61 cnf(5991,plain,
% 281.63/281.61 (E(f2(f7(a12,a13),a13),f2(f7(f2(a1,a11),f7(a1,a15)),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[2701,5894,5815,2,3])).
% 281.63/281.61 cnf(6001,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),f7(a12,a13)),f2(a13,f7(f2(a1,a11),f7(a1,a15))))),
% 281.63/281.61 inference(scs_inference,[],[2747,5920,5841,2,3])).
% 281.63/281.61 cnf(6041,plain,
% 281.63/281.61 (E(f2(f7(a1,a15),f7(a13,f2(a1,a11))),f2(a13,f7(f7(a1,a15),a12)))),
% 281.63/281.61 inference(scs_inference,[],[2747,5991,5970,2,3])).
% 281.63/281.61 cnf(6774,plain,
% 281.63/281.61 (P2(x67741,f7(a1,a15))+~E(a5,x67741)),
% 281.63/281.61 inference(scs_inference,[],[2701,6041,3049,26,27,11])).
% 281.63/281.61 cnf(6783,plain,
% 281.63/281.61 (P2(x67831,f7(a1,a15))+~E(a8,x67831)),
% 281.63/281.61 inference(scs_inference,[],[2785,6001,2703,26,27,11])).
% 281.63/281.61 cnf(6792,plain,
% 281.63/281.61 (P2(x67921,f7(a1,a15))+~E(a9,x67921)),
% 281.63/281.61 inference(scs_inference,[],[2747,5931,2731,26,27,11])).
% 281.63/281.61 cnf(7065,plain,
% 281.63/281.61 (E(f7(a1,a11),a13)),
% 281.63/281.61 inference(scs_inference,[],[31,5713,58])).
% 281.63/281.61 cnf(7069,plain,
% 281.63/281.61 (E(f7(x70691,f7(a1,a11)),f7(x70691,a13))),
% 281.63/281.61 inference(scs_inference,[],[31,5713,58,49,7])).
% 281.63/281.61 cnf(7071,plain,
% 281.63/281.61 (E(f7(f7(a1,a11),x70711),f7(a13,x70711))),
% 281.63/281.61 inference(scs_inference,[],[31,5713,58,49,7,8,6])).
% 281.63/281.61 cnf(7072,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),x70721),f2(a13,x70721))),
% 281.63/281.61 inference(scs_inference,[],[31,5713,58,49,7,8,6,4])).
% 281.63/281.61 cnf(7073,plain,
% 281.63/281.61 (E(f2(x70731,f7(a1,a11)),f2(x70731,a13))),
% 281.63/281.61 inference(scs_inference,[],[31,5713,58,49,7,8,6,4,5])).
% 281.63/281.61 cnf(7087,plain,
% 281.63/281.61 (P5(f2(x70871,f7(a1,a11)),f2(x70871,a13))),
% 281.63/281.61 inference(scs_inference,[],[7073,49,50])).
% 281.63/281.61 cnf(7256,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a11)),f2(a13,a13))),
% 281.63/281.61 inference(scs_inference,[],[7072,7073,3])).
% 281.63/281.61 cnf(7311,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a11)),f2(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[7256,3820,3])).
% 281.63/281.61 cnf(7351,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a11)),f2(f7(a1,a15),a13))),
% 281.63/281.61 inference(scs_inference,[],[7311,2755,3])).
% 281.63/281.61 cnf(7390,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a11)),f2(a13,f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[7351,5721,21,3])).
% 281.63/281.61 cnf(7473,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a15)),f2(a13,a13))),
% 281.63/281.61 inference(scs_inference,[],[7072,2755,3])).
% 281.63/281.61 cnf(7515,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a15)),f2(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[7473,3820,3])).
% 281.63/281.61 cnf(7533,plain,
% 281.63/281.61 (E(f2(f7(a1,a11),f7(a1,a15)),f2(f7(a1,a15),a13))),
% 281.63/281.61 inference(scs_inference,[],[7515,2755,24,3])).
% 281.63/281.61 cnf(7562,plain,
% 281.63/281.61 (E(f7(f2(a1,a11),f7(a1,a11)),f7(a12,a13))),
% 281.63/281.61 inference(scs_inference,[],[7069,2823,3])).
% 281.63/281.61 cnf(7679,plain,
% 281.63/281.61 (E(f7(f2(a1,a11),f7(a1,a11)),f7(a12,f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[79,7562,7533,2698,22,3])).
% 281.63/281.61 cnf(7720,plain,
% 281.63/281.61 (E(f7(a13,f7(a1,a11)),f7(f7(a1,a15),a13))),
% 281.63/281.61 inference(scs_inference,[],[7069,2697,3])).
% 281.63/281.61 cnf(7772,plain,
% 281.63/281.61 (E(f7(a13,f7(a1,a11)),f7(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.61 inference(scs_inference,[],[7720,2698,3])).
% 281.63/281.61 cnf(7817,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),a13),f7(a13,f7(a1,a15)))),
% 281.63/281.62 inference(scs_inference,[],[7071,2698,3])).
% 281.63/281.62 cnf(7868,plain,
% 281.63/281.62 (E(f7(a13,f7(a1,a15)),f7(f7(a1,a11),a13))),
% 281.63/281.62 inference(scs_inference,[],[7817,2])).
% 281.63/281.62 cnf(7869,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),f7(a1,a11)),f7(a13,f7(a1,a15)))),
% 281.63/281.62 inference(scs_inference,[],[7817,7069,2,3])).
% 281.63/281.62 cnf(7871,plain,
% 281.63/281.62 (P5(f2(a13,f7(a1,a15)),f2(f7(a1,a11),a13))),
% 281.63/281.62 inference(scs_inference,[],[7087,7817,7390,7069,2,3,28])).
% 281.63/281.62 cnf(7885,plain,
% 281.63/281.62 (E(f7(a13,f7(a1,a15)),f7(f7(a1,a11),f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[7869,2])).
% 281.63/281.62 cnf(7886,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),f7(a1,a11)),f7(f7(a1,a15),a13))),
% 281.63/281.62 inference(scs_inference,[],[7869,7720,7071,2,3])).
% 281.63/281.62 cnf(7903,plain,
% 281.63/281.62 (E(f7(f7(a1,a15),a13),f7(f7(a1,a11),f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[7886,2])).
% 281.63/281.62 cnf(7904,plain,
% 281.63/281.62 (E(f7(a13,f7(a1,a15)),f7(f7(a1,a15),a13))),
% 281.63/281.62 inference(scs_inference,[],[7886,7885,2,3])).
% 281.63/281.62 cnf(7919,plain,
% 281.63/281.62 (E(f7(f7(a1,a15),a13),f7(a13,f7(a1,a15)))),
% 281.63/281.62 inference(scs_inference,[],[7904,2])).
% 281.63/281.62 cnf(7920,plain,
% 281.63/281.62 (E(f7(a12,f7(a1,a11)),f7(a12,f7(a1,a15)))),
% 281.63/281.62 inference(scs_inference,[],[7904,7679,2787,2,3])).
% 281.63/281.62 cnf(7941,plain,
% 281.63/281.62 (E(f7(f7(a1,a15),a13),f7(f7(a1,a11),a13))),
% 281.63/281.62 inference(scs_inference,[],[7919,7868,7920,2,3])).
% 281.63/281.62 cnf(7956,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),a13),f7(f7(a1,a15),a13))),
% 281.63/281.62 inference(scs_inference,[],[7941,2])).
% 281.63/281.62 cnf(7957,plain,
% 281.63/281.62 (E(f2(f7(a1,a11),a13),f2(f7(a1,a15),a13))),
% 281.63/281.62 inference(scs_inference,[],[7941,7533,2701,2,3])).
% 281.63/281.62 cnf(7975,plain,
% 281.63/281.62 (E(f2(f7(a1,a15),a13),f2(f7(a1,a11),a13))),
% 281.63/281.62 inference(scs_inference,[],[7957,2])).
% 281.63/281.62 cnf(7993,plain,
% 281.63/281.62 (E(f2(f7(a1,a11),a13),f2(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.62 inference(scs_inference,[],[7772,7515,2701,2,3])).
% 281.63/281.62 cnf(8012,plain,
% 281.63/281.62 (E(f7(f7(a1,a15),a13),f7(a13,f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[7993,7903,7071,2,3])).
% 281.63/281.62 cnf(8029,plain,
% 281.63/281.62 (E(f7(a13,f7(a1,a15)),f7(a13,f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[8012,7904,7679,2,3])).
% 281.63/281.62 cnf(8049,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),a13),f7(a13,f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[8029,8012,7956,2,3])).
% 281.63/281.62 cnf(8088,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),a13),f7(f7(a1,a15),f7(a1,a15)))),
% 281.63/281.62 inference(scs_inference,[],[8049,7772,7562,2,3])).
% 281.63/281.62 cnf(8107,plain,
% 281.63/281.62 (E(f7(f7(a1,a15),f7(a1,a15)),f7(f7(a1,a11),a13))),
% 281.63/281.62 inference(scs_inference,[],[8088,2])).
% 281.63/281.62 cnf(8129,plain,
% 281.63/281.62 (E(f2(f7(a1,a11),f2(a1,a11)),f2(f7(a1,a15),a12))),
% 281.63/281.62 inference(scs_inference,[],[7533,7072,5919,2,3])).
% 281.63/281.62 cnf(8147,plain,
% 281.63/281.62 (E(f2(f7(a1,a11),a12),f2(f7(a1,a15),a12))),
% 281.63/281.62 inference(scs_inference,[],[8129,2790,2,3])).
% 281.63/281.62 cnf(8163,plain,
% 281.63/281.62 (E(f7(f7(a1,a11),f2(a1,a11)),f7(f7(a1,a15),a12))),
% 281.63/281.62 inference(scs_inference,[],[8147,7071,5709,2,3])).
% 281.63/281.62 cnf(8188,plain,
% 281.63/281.62 (P9(f7(f7(a1,a15),a12),f7(f7(a1,a11),a12))),
% 281.63/281.62 inference(scs_inference,[],[8163,8107,2952,2975,2971,2785,2,3,28,23,22])).
% 281.63/281.62 cnf(8345,plain,
% 281.63/281.62 (E(a13,f7(a1,a11))),
% 281.63/281.62 inference(scs_inference,[],[7065,2])).
% 281.63/281.62 cnf(8478,plain,
% 281.63/281.62 (E(f2(f7(a1,a15),a13),f2(f7(a1,a11),f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[7351,2])).
% 281.63/281.62 cnf(8531,plain,
% 281.63/281.62 (E(f2(f7(a1,a15),f7(a1,a11)),f2(f7(a1,a11),a13))),
% 281.63/281.62 inference(scs_inference,[],[2701,7073,2785,7975,7515,7871,8188,4,5,8,6,7,2,29,22,3])).
% 281.63/281.62 cnf(8636,plain,
% 281.63/281.62 (E(f2(f2(f7(a1,a15),x86361),x86362),f2(f2(a13,x86361),x86362))),
% 281.63/281.62 inference(scs_inference,[],[2747,4])).
% 281.63/281.62 cnf(8693,plain,
% 281.63/281.62 (E(f2(f2(x86931,f7(a1,a15)),x86932),f2(f2(x86931,a13),x86932))),
% 281.63/281.62 inference(scs_inference,[],[2755,4])).
% 281.63/281.62 cnf(8696,plain,
% 281.63/281.62 (E(f7(x86961,f2(x86962,f7(a1,a15))),f7(x86961,f2(x86962,a13)))),
% 281.63/281.62 inference(scs_inference,[],[2755,4,5,8,7])).
% 281.63/281.62 cnf(8826,plain,
% 281.63/281.62 (P5(f2(f2(f7(a1,a15),x88261),x88262),f2(f2(a13,x88261),x88262))),
% 281.63/281.62 inference(scs_inference,[],[8478,8636,49,50])).
% 281.63/281.62 cnf(8907,plain,
% 281.63/281.62 (E(f7(f2(f7(a1,a15),f7(a1,a11)),x89071),f7(f2(f7(a1,a11),a13),x89071))),
% 281.63/281.62 inference(scs_inference,[],[8531,8693,49,50,4,7,5,8,6])).
% 281.63/281.62 cnf(8911,plain,
% 281.63/281.62 (P9(f7(x89111,f2(x89112,f7(a1,a15))),f7(x89111,f2(x89112,a13)))),
% 281.63/281.62 inference(scs_inference,[],[8696,49])).
% 281.63/281.62 cnf(9274,plain,
% 281.63/281.62 (P5(f2(f2(f7(a1,a15),x92741),x92742),f2(f2(a13,x92741),x92742))),
% 281.63/281.62 inference(rename_variables,[],[8826])).
% 281.63/281.62 cnf(9275,plain,
% 281.63/281.62 (E(f2(x92751,f7(a1,a11)),f2(x92751,a13))),
% 281.63/281.62 inference(rename_variables,[],[7073])).
% 281.63/281.62 cnf(9277,plain,
% 281.63/281.62 (P9(f7(x92771,f2(x92772,f7(a1,a15))),f7(x92771,f2(x92772,a13)))),
% 281.63/281.62 inference(rename_variables,[],[8911])).
% 281.63/281.62 cnf(9278,plain,
% 281.63/281.62 (E(f7(a13,x92781),f7(f7(a1,a15),x92781))),
% 281.63/281.62 inference(rename_variables,[],[2697])).
% 281.63/281.62 cnf(9279,plain,
% 281.63/281.62 (E(f7(a1,a15),f7(a1,a11))),
% 281.63/281.62 inference(scs_inference,[],[7073,2697,932,2823,3820,8345,8907,8826,8911,4,8,7,6,5,2,29,22,3])).
% 281.63/281.62 cnf(9286,plain,
% 281.63/281.62 (~P2(f7(a1,a16),f7(a1,a15))),
% 281.63/281.62 inference(scs_inference,[],[7073,9275,2697,9278,932,2823,3820,8345,8907,8826,9274,8911,9277,4,8,7,6,5,2,29,22,3,28,23,75])).
% 281.63/281.62 cnf(9288,plain,
% 281.63/281.62 (~E(a8,f7(a1,a16))),
% 281.63/281.62 inference(scs_inference,[],[7073,9275,2697,9278,932,2823,3820,8345,8907,8826,9274,8911,9277,4,8,7,6,5,2,29,22,3,28,23,75,6774,6783])).
% 281.63/281.62 cnf(9290,plain,
% 281.63/281.62 (~P2(f7(a1,a16),a6)),
% 281.63/281.62 inference(scs_inference,[],[7073,9275,2697,9278,932,2823,3820,8345,8907,8826,9274,8911,9277,4,8,7,6,5,2,29,22,3,28,23,75,6774,6783,6792,955])).
% 281.63/281.62 cnf(9292,plain,
% 281.63/281.62 (~E(a6,f7(a1,a16))),
% 281.63/281.62 inference(scs_inference,[],[7073,9275,2697,9278,932,2823,3820,8345,8907,8826,9274,8911,9277,4,8,7,6,5,2,29,22,3,28,23,75,6774,6783,6792,955,961])).
% 281.63/281.62 cnf(9293,plain,
% 281.63/281.62 (~P12(f7(a1,a15),f7(a1,a16))),
% 281.63/281.62 inference(scs_inference,[],[7073,9275,2697,9278,932,2823,3820,8345,8907,8826,9274,8911,9277,4,8,7,6,5,2,29,22,3,28,23,75,6774,6783,6792,955,961,55])).
% 281.63/281.62 cnf(9302,plain,
% 281.63/281.62 (~P12(a6,f7(a1,a16))),
% 281.63/281.62 inference(scs_inference,[],[9290,55])).
% 281.63/281.62 cnf(9523,plain,
% 281.63/281.62 (E(f2(f7(a1,a11),a13),f2(f7(a1,a15),f7(a1,a11)))),
% 281.63/281.62 inference(scs_inference,[],[2818,2824,8531,4,7,8,5,6,2])).
% 281.63/281.62 cnf(9613,plain,
% 281.63/281.62 ($false),
% 281.63/281.62 inference(scs_inference,[],[9286,31,9288,9292,9523,9279,2731,933,79,88,9302,9293,2708,7,4,6,5,50,49,2,12,24,51,56,61,22,63,62]),
% 281.63/281.62 ['proof']).
% 281.63/281.62 % SZS output end Proof
% 281.63/281.62 % Total time :281.052948s
%------------------------------------------------------------------------------