%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT064-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 : n010.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 230.04s 230.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT064-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:44:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.25/0.51 start to proof:theBenchmark
% 229.91/230.02 %-------------------------------------------
% 229.91/230.02 % File :CSE---1.7
% 229.91/230.02 % Problem :theBenchmark
% 229.91/230.02 % Transform :cnf
% 229.91/230.02 % Format :tptp:raw
% 229.91/230.02 % Command :java -jar mcs_scs.jar %d %s
% 229.91/230.02
% 229.91/230.02 % Result :Theorem 229.482490s
% 229.91/230.02 % Output :CNFRefutation 229.482490s
% 229.91/230.02 %-------------------------------------------
% 229.91/230.02 %--------------------------------------------------------------------------
% 229.91/230.02 % File : MGT064-1 : TPTP v9.3.0. Released v2.4.0.
% 229.91/230.02 % Domain : Management (Organisation Theory)
% 229.91/230.02 % Problem : Conditions for a decreasing then increasing hazard of mortality
% 229.91/230.02 % Version : [Han98] axioms.
% 229.91/230.02 % English : If advantage can be gained from occupancy of a robust position
% 229.91/230.02 % before environmental drift destroys alignment, then the hazard
% 229.91/230.02 % of mortality for an unendowed organization with a robust
% 229.91/230.02 % position initially decreases with age and then rises with
% 229.91/230.02 % further aging but remains below the initial level.
% 229.91/230.02
% 229.91/230.02 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 229.91/230.02 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 229.91/230.02 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 229.91/230.03 % Source : [TPTP]
% 229.91/230.03 % Names :
% 229.91/230.03
% 229.91/230.03 % Status : Unsatisfiable
% 229.91/230.03 % Rating : 0.25 v9.3.0, 0.14 v9.1.0, 0.10 v9.0.0, 0.15 v8.2.0, 0.14 v8.1.0, 0.11 v7.4.0, 0.18 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.29 v6.0.0, 0.30 v5.5.0, 0.55 v5.3.0, 0.44 v5.1.0, 0.53 v5.0.0, 0.43 v4.1.0, 0.38 v4.0.1, 0.27 v4.0.0, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.17 v3.3.0, 0.36 v3.2.0, 0.46 v3.1.0, 0.55 v2.7.0, 0.42 v2.6.0, 0.67 v2.5.0, 0.78 v2.4.0
% 229.91/230.03 % Syntax : Number of clauses : 58 ( 17 unt; 20 nHn; 50 RR)
% 229.91/230.03 % Number of literals : 149 ( 15 equ; 68 neg)
% 229.91/230.03 % Maximal clause size : 5 ( 2 avg)
% 229.91/230.03 % Maximal term depth : 3 ( 1 avg)
% 229.91/230.03 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty)
% 229.91/230.03 % Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% 229.91/230.03 % Number of variables : 81 ( 5 sgn)
% 229.91/230.03 % SPC : CNF_UNS_RFO_SEQ_NHN
% 229.91/230.03
% 229.91/230.03 % Comments : See MGT042+1.p for the mnemonic names.
% 229.91/230.03 % : Created with tptp2X -f tptp -t clausify:otter MGT064+1.p
% 229.91/230.03 %--------------------------------------------------------------------------
% 230.04/230.03 include('Axioms/MGT001-0.ax').
% 230.04/230.03 %--------------------------------------------------------------------------
% 230.04/230.03 cnf(definition_1_39,axiom,
% 230.04/230.03 ( ~ has_endowment(A)
% 230.04/230.03 | organization(A) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_1_40,axiom,
% 230.04/230.03 ( ~ has_endowment(A)
% 230.04/230.03 | ~ smaller_or_equal(age(A,B),eta)
% 230.04/230.03 | has_immunity(A,B) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_1_41,axiom,
% 230.04/230.03 ( ~ has_endowment(A)
% 230.04/230.03 | ~ greater(age(A,B),eta)
% 230.04/230.03 | ~ has_immunity(A,B) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_1_42,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | smaller_or_equal(age(A,sk1(A)),eta)
% 230.04/230.03 | greater(age(A,sk1(A)),eta)
% 230.04/230.03 | has_endowment(A) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_1_43,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | smaller_or_equal(age(A,sk1(A)),eta)
% 230.04/230.03 | has_immunity(A,sk1(A))
% 230.04/230.03 | has_endowment(A) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_1_44,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | ~ has_immunity(A,sk1(A))
% 230.04/230.03 | greater(age(A,sk1(A)),eta)
% 230.04/230.03 | has_endowment(A) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_1_45,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | ~ has_immunity(A,sk1(A))
% 230.04/230.03 | has_immunity(A,sk1(A))
% 230.04/230.03 | has_endowment(A) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(assumption_1_46,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | has_endowment(A)
% 230.04/230.03 | ~ has_immunity(A,B) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_47,axiom,
% 230.04/230.03 ( ~ dissimilar(A,B,C)
% 230.04/230.03 | organization(A) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_48,axiom,
% 230.04/230.03 ( ~ dissimilar(A,B,C)
% 230.04/230.03 | is_aligned(A,B)
% 230.04/230.03 | is_aligned(A,C) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_49,axiom,
% 230.04/230.03 ( ~ dissimilar(A,B,C)
% 230.04/230.03 | ~ is_aligned(A,B)
% 230.04/230.03 | ~ is_aligned(A,C) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_50,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | ~ is_aligned(A,B)
% 230.04/230.03 | is_aligned(A,B)
% 230.04/230.03 | dissimilar(A,B,C) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_51,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | ~ is_aligned(A,B)
% 230.04/230.03 | is_aligned(A,C)
% 230.04/230.03 | dissimilar(A,B,C) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_52,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | ~ is_aligned(A,B)
% 230.04/230.03 | is_aligned(A,C)
% 230.04/230.03 | dissimilar(A,C,B) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(definition_2_53,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | ~ is_aligned(A,B)
% 230.04/230.03 | is_aligned(A,B)
% 230.04/230.03 | dissimilar(A,C,B) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(assumption_13_54,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | age(A,B) != zero
% 230.04/230.03 | is_aligned(A,B) ) ).
% 230.04/230.03
% 230.04/230.03 cnf(assumption_15_55,axiom,
% 230.04/230.03 ( ~ organization(A)
% 230.04/230.03 | age(A,B) != zero
% 230.04/230.03 | ~ greater(age(A,C),sigma)
% 230.04/230.04 | dissimilar(A,B,C) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_15_56,axiom,
% 230.04/230.04 ( ~ organization(A)
% 230.04/230.04 | age(A,B) != zero
% 230.04/230.04 | ~ dissimilar(A,B,C)
% 230.04/230.04 | greater(age(A,C),sigma) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(definition_4_57,axiom,
% 230.04/230.04 ( ~ robust_position(A)
% 230.04/230.04 | ~ smaller_or_equal(age(A,B),tau)
% 230.04/230.04 | ~ positional_advantage(A,B) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(definition_4_58,axiom,
% 230.04/230.04 ( ~ robust_position(A)
% 230.04/230.04 | ~ greater(age(A,B),tau)
% 230.04/230.04 | positional_advantage(A,B) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(definition_4_59,axiom,
% 230.04/230.04 ( smaller_or_equal(age(A,sk2(A)),tau)
% 230.04/230.04 | greater(age(A,sk2(A)),tau)
% 230.04/230.04 | robust_position(A) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(definition_4_60,axiom,
% 230.04/230.04 ( smaller_or_equal(age(A,sk2(A)),tau)
% 230.04/230.04 | ~ positional_advantage(A,sk2(A))
% 230.04/230.04 | robust_position(A) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(definition_4_61,axiom,
% 230.04/230.04 ( positional_advantage(A,sk2(A))
% 230.04/230.04 | greater(age(A,sk2(A)),tau)
% 230.04/230.04 | robust_position(A) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(definition_4_62,axiom,
% 230.04/230.04 ( positional_advantage(A,sk2(A))
% 230.04/230.04 | ~ positional_advantage(A,sk2(A))
% 230.04/230.04 | robust_position(A) ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_17_63,axiom,
% 230.04/230.04 ( ~ organization(A)
% 230.04/230.04 | ~ has_immunity(A,B)
% 230.04/230.04 | hazard_of_mortality(A,B) = very_low ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_17_64,axiom,
% 230.04/230.04 ( ~ organization(A)
% 230.04/230.04 | has_immunity(A,B)
% 230.04/230.04 | ~ is_aligned(A,B)
% 230.04/230.04 | ~ positional_advantage(A,B)
% 230.04/230.04 | hazard_of_mortality(A,B) = low ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_17_65,axiom,
% 230.04/230.04 ( ~ organization(A)
% 230.04/230.04 | has_immunity(A,B)
% 230.04/230.04 | is_aligned(A,B)
% 230.04/230.04 | ~ positional_advantage(A,B)
% 230.04/230.04 | hazard_of_mortality(A,B) = mod1 ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_17_66,axiom,
% 230.04/230.04 ( ~ organization(A)
% 230.04/230.04 | has_immunity(A,B)
% 230.04/230.04 | ~ is_aligned(A,B)
% 230.04/230.04 | positional_advantage(A,B)
% 230.04/230.04 | hazard_of_mortality(A,B) = mod2 ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_17_67,axiom,
% 230.04/230.04 ( ~ organization(A)
% 230.04/230.04 | has_immunity(A,B)
% 230.04/230.04 | is_aligned(A,B)
% 230.04/230.04 | positional_advantage(A,B)
% 230.04/230.04 | hazard_of_mortality(A,B) = high ) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_18a_68,axiom,
% 230.04/230.04 greater(high,mod1) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_18b_69,axiom,
% 230.04/230.04 greater(mod1,low) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_18c_70,axiom,
% 230.04/230.04 greater(low,very_low) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_18d_71,axiom,
% 230.04/230.04 greater(high,mod2) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_18e_72,axiom,
% 230.04/230.04 greater(mod2,low) ).
% 230.04/230.04
% 230.04/230.04 cnf(assumption_19_73,axiom,
% 230.04/230.04 greater(mod2,mod1) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_74,negated_conjecture,
% 230.04/230.04 organization(sk3) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_75,negated_conjecture,
% 230.04/230.04 robust_position(sk3) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_76,negated_conjecture,
% 230.04/230.04 ~ has_endowment(sk3) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_77,negated_conjecture,
% 230.04/230.04 age(sk3,sk4) = zero ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_78,negated_conjecture,
% 230.04/230.04 greater(sigma,zero) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_79,negated_conjecture,
% 230.04/230.04 greater(tau,zero) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_80,negated_conjecture,
% 230.04/230.04 greater(sigma,tau) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_81,negated_conjecture,
% 230.04/230.04 smaller_or_equal(age(sk3,sk5),tau) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_82,negated_conjecture,
% 230.04/230.04 greater(age(sk3,sk6),tau) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_83,negated_conjecture,
% 230.04/230.04 smaller_or_equal(age(sk3,sk6),sigma) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_84,negated_conjecture,
% 230.04/230.04 greater(age(sk3,sk7),sigma) ).
% 230.04/230.04
% 230.04/230.04 cnf(theorem_10_85,negated_conjecture,
% 230.04/230.04 ( ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))
% 230.04/230.04 | ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))
% 230.04/230.04 | hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4) ) ).
% 230.04/230.04
% 230.04/230.04 %--------------------------------------------------------------------------
% 230.04/230.04 %-------------------------------------------
% 230.04/230.04 % Proof found
% 230.04/230.04 % SZS status Theorem for theBenchmark
% 230.04/230.04 % SZS output start Proof
% 230.04/230.04 %ClaNum:83(EqnAxiom:29)
% 230.04/230.04 %VarNum:201(SingletonVarNum:72)
% 230.04/230.04 %MaxLitNum:5
% 230.04/230.04 %MaxfuncDepth:2
% 230.04/230.04 %SharedTerms:42
% 230.04/230.04 %goalClause: 30 31 32 33 34 35 42 43 44 45 46 83
% 230.04/230.04 %singleGoalClaCount:11
% 230.04/230.04 [30]P1(a1)
% 230.04/230.04 [31]P8(a1)
% 230.04/230.04 [33]P2(a3,a13)
% 230.04/230.04 [34]P2(a3,a14)
% 230.04/230.04 [35]P2(a14,a13)
% 230.04/230.04 [36]P2(a4,a18)
% 230.04/230.04 [37]P2(a8,a4)
% 230.04/230.04 [38]P2(a9,a4)
% 230.04/230.04 [39]P2(a9,a8)
% 230.04/230.04 [40]P2(a5,a8)
% 230.04/230.04 [41]P2(a5,a9)
% 230.04/230.04 [46]~P4(a1)
% 230.04/230.05 [32]E(f2(a1,a12),a13)
% 230.04/230.05 [42]P10(f2(a1,a15),a14)
% 230.04/230.05 [43]P10(f2(a1,a16),a3)
% 230.04/230.05 [44]P2(f2(a1,a16),a14)
% 230.04/230.05 [45]P2(f2(a1,a17),a3)
% 230.04/230.05 [47]~P4(x471)+P1(x471)
% 230.04/230.05 [48]~E(x481,x482)+P10(x481,x482)
% 230.04/230.05 [49]~E(x491,x492)+P5(x491,x492)
% 230.04/230.05 [52]~P11(x521,x522)+P10(x521,x522)
% 230.04/230.05 [53]~P2(x532,x531)+P11(x531,x532)
% 230.04/230.05 [54]~P2(x541,x542)+P5(x541,x542)
% 230.04/230.05 [55]~P11(x552,x551)+P2(x551,x552)
% 230.04/230.05 [60]~P2(x602,x601)+~P2(x601,x602)
% 230.04/230.05 [71]P1(x711)+~P3(x711,x712,x713)
% 230.04/230.05 [83]~P11(f6(a1,a17),f6(a1,a15))+~E(f6(a1,a15),f6(a1,a12))+~P11(f6(a1,a16),f6(a1,a17))
% 230.04/230.05 [65]P8(x651)+P9(x651,f10(x651))+P2(f2(x651,f10(x651)),a14)
% 230.04/230.05 [70]P8(x701)+~P9(x701,f10(x701))+P10(f2(x701,f10(x701)),a14)
% 230.04/230.05 [77]P8(x771)+P10(f2(x771,f10(x771)),a14)+P2(f2(x771,f10(x771)),a14)
% 230.04/230.05 [50]P11(x501,x502)+P2(x501,x502)+E(x501,x502)
% 230.04/230.05 [51]~P1(x511)+P4(x511)+~P6(x511,x512)
% 230.04/230.05 [56]P11(x561,x562)+~P10(x561,x562)+E(x561,x562)
% 230.04/230.05 [57]P2(x571,x572)+~P5(x571,x572)+E(x571,x572)
% 230.04/230.05 [58]~P1(x581)+~P6(x581,x582)+E(f6(x581,x582),a18)
% 230.04/230.05 [59]~P1(x591)+P7(x591,x592)+~E(f2(x591,x592),a13)
% 230.04/230.05 [67]~P4(x671)+P6(x671,x672)+~P10(f2(x671,x672),a7)
% 230.04/230.05 [68]~P8(x681)+P9(x681,x682)+~P2(f2(x681,x682),a14)
% 230.04/230.05 [72]~P4(x721)+~P6(x721,x722)+~P2(f2(x721,x722),a7)
% 230.04/230.05 [73]~P8(x731)+~P9(x731,x732)+~P10(f2(x731,x732),a14)
% 230.04/230.05 [61]~P2(x611,x613)+P2(x611,x612)+~P2(x613,x612)
% 230.04/230.05 [79]~P3(x791,x793,x792)+P7(x791,x792)+P7(x791,x793)
% 230.04/230.05 [80]~P3(x801,x803,x802)+~P7(x801,x802)+~P7(x801,x803)
% 230.04/230.05 [69]~P1(x691)+P4(x691)+P6(x691,f11(x691))+P10(f2(x691,f11(x691)),a7)
% 230.04/230.05 [78]~P1(x781)+P4(x781)+P10(f2(x781,f11(x781)),a7)+P2(f2(x781,f11(x781)),a7)
% 230.04/230.05 [75]~P1(x751)+~P7(x751,x753)+P7(x751,x752)+P3(x751,x752,x753)
% 230.04/230.05 [76]~P1(x761)+~P7(x761,x763)+P7(x761,x762)+P3(x761,x763,x762)
% 230.04/230.05 [81]~P1(x811)+P3(x811,x812,x813)+~E(f2(x811,x812),a13)+~P2(f2(x811,x813),a3)
% 230.04/230.05 [82]~P1(x821)+~P3(x821,x823,x822)+P2(f2(x821,x822),a3)+~E(f2(x821,x823),a13)
% 230.04/230.05 [62]P6(x621,x622)+P7(x621,x622)+P9(x621,x622)+~P1(x621)+E(f6(x621,x622),a5)
% 230.04/230.05 [63]P6(x631,x632)+P7(x631,x632)+~P1(x631)+~P9(x631,x632)+E(f6(x631,x632),a8)
% 230.04/230.05 [64]P6(x641,x642)+P9(x641,x642)+~P1(x641)+~P7(x641,x642)+E(f6(x641,x642),a9)
% 230.04/230.05 [66]P6(x661,x662)+~P1(x661)+~P7(x661,x662)+~P9(x661,x662)+E(f6(x661,x662),a4)
% 230.04/230.05 %EqnAxiom
% 230.04/230.05 [1]E(x11,x11)
% 230.04/230.05 [2]E(x22,x21)+~E(x21,x22)
% 230.04/230.05 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 230.04/230.05 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 230.04/230.05 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 230.04/230.05 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 230.04/230.05 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 230.04/230.05 [8]~E(x81,x82)+E(f11(x81),f11(x82))
% 230.04/230.05 [9]~E(x91,x92)+E(f10(x91),f10(x92))
% 230.04/230.05 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 230.04/230.05 [11]~P8(x111)+P8(x112)+~E(x111,x112)
% 230.04/230.05 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 230.04/230.05 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 230.04/230.05 [14]P7(x142,x143)+~E(x141,x142)+~P7(x141,x143)
% 230.04/230.05 [15]P7(x153,x152)+~E(x151,x152)+~P7(x153,x151)
% 230.04/230.05 [16]P3(x162,x163,x164)+~E(x161,x162)+~P3(x161,x163,x164)
% 230.04/230.05 [17]P3(x173,x172,x174)+~E(x171,x172)+~P3(x173,x171,x174)
% 230.04/230.05 [18]P3(x183,x184,x182)+~E(x181,x182)+~P3(x183,x184,x181)
% 230.04/230.05 [19]~P4(x191)+P4(x192)+~E(x191,x192)
% 230.04/230.05 [20]P9(x202,x203)+~E(x201,x202)+~P9(x201,x203)
% 230.04/230.05 [21]P9(x213,x212)+~E(x211,x212)+~P9(x213,x211)
% 230.04/230.05 [22]P10(x222,x223)+~E(x221,x222)+~P10(x221,x223)
% 230.04/230.05 [23]P10(x233,x232)+~E(x231,x232)+~P10(x233,x231)
% 230.04/230.05 [24]P6(x242,x243)+~E(x241,x242)+~P6(x241,x243)
% 230.04/230.05 [25]P6(x253,x252)+~E(x251,x252)+~P6(x253,x251)
% 230.04/230.05 [26]P11(x262,x263)+~E(x261,x262)+~P11(x261,x263)
% 230.04/230.05 [27]P11(x273,x272)+~E(x271,x272)+~P11(x273,x271)
% 230.04/230.05 [28]P5(x282,x283)+~E(x281,x282)+~P5(x281,x283)
% 230.04/230.05 [29]P5(x293,x292)+~E(x291,x292)+~P5(x293,x291)
% 230.04/230.05
% 230.04/230.05 %-------------------------------------------
% 230.04/230.05 cnf(84,plain,
% 230.04/230.05 (P10(x841,x841)),
% 230.04/230.05 inference(equality_inference,[],[48])).
% 230.04/230.05 cnf(85,plain,
% 230.04/230.05 (P5(x851,x851)),
% 230.04/230.05 inference(equality_inference,[],[49])).
% 230.04/230.05 cnf(86,plain,
% 230.04/230.05 (E(a13,f2(a1,a12))),
% 230.04/230.05 inference(scs_inference,[],[32,2])).
% 230.04/230.05 cnf(87,plain,
% 230.04/230.05 (~P2(a13,a3)),
% 230.04/230.05 inference(scs_inference,[],[33,32,2,60])).
% 230.04/230.05 cnf(89,plain,
% 230.04/230.05 (~P6(a1,x891)),
% 230.04/230.05 inference(scs_inference,[],[30,33,46,32,2,60,51])).
% 230.04/230.05 cnf(91,plain,
% 230.04/230.05 (P7(a1,a12)),
% 230.04/230.05 inference(scs_inference,[],[30,33,46,32,2,60,51,59])).
% 230.04/230.05 cnf(93,plain,
% 230.04/230.05 (P9(a1,a16)),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,2,60,51,59,68])).
% 230.04/230.05 cnf(95,plain,
% 230.04/230.05 (~P9(a1,a15)),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,42,2,60,51,59,68,73])).
% 230.04/230.05 cnf(98,plain,
% 230.04/230.05 (P2(a3,f2(a1,a12))),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,42,45,2,60,51,59,68,73,12,13])).
% 230.04/230.05 cnf(99,plain,
% 230.04/230.05 (P2(f2(a1,a17),a13)),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,42,45,2,60,51,59,68,73,12,13,61])).
% 230.04/230.05 cnf(103,plain,
% 230.04/230.05 (~E(a16,a15)),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,42,45,2,60,51,59,68,73,12,13,61,80,21])).
% 230.04/230.05 cnf(105,plain,
% 230.04/230.05 (P10(x1051,x1051)),
% 230.04/230.05 inference(rename_variables,[],[84])).
% 230.04/230.05 cnf(109,plain,
% 230.04/230.05 (P5(x1091,x1091)),
% 230.04/230.05 inference(rename_variables,[],[85])).
% 230.04/230.05 cnf(112,plain,
% 230.04/230.05 (P3(a1,a12,a17)),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,42,45,84,105,85,109,2,60,51,59,68,73,12,13,61,80,21,22,23,28,29,81])).
% 230.04/230.05 cnf(116,plain,
% 230.04/230.05 (~E(f2(a1,a17),f2(a1,a12))),
% 230.04/230.05 inference(scs_inference,[],[30,31,33,46,44,32,42,45,84,105,85,109,2,60,51,59,68,73,12,13,61,80,21,22,23,28,29,81,55,3])).
% 230.04/230.05 cnf(125,plain,
% 230.04/230.05 (~P2(a14,a3)),
% 230.04/230.05 inference(scs_inference,[],[34,60])).
% 230.04/230.05 cnf(129,plain,
% 230.04/230.05 (P2(f2(a1,a17),a14)),
% 230.04/230.05 inference(scs_inference,[],[34,45,60,55,61])).
% 230.04/230.05 cnf(131,plain,
% 230.04/230.05 (P9(a1,a17)),
% 230.04/230.05 inference(scs_inference,[],[34,31,45,60,55,61,68])).
% 230.04/230.05 cnf(133,plain,
% 230.04/230.05 (~E(a17,a15)),
% 230.04/230.05 inference(scs_inference,[],[34,31,45,95,60,55,61,68,21])).
% 230.04/230.05 cnf(134,plain,
% 230.04/230.05 (~E(a13,a3)),
% 230.04/230.05 inference(scs_inference,[],[34,35,31,45,95,60,55,61,68,21,13])).
% 230.04/230.05 cnf(136,plain,
% 230.04/230.05 (P11(a13,a3)),
% 230.04/230.05 inference(scs_inference,[],[34,35,31,45,91,95,87,60,55,61,68,21,13,15,50])).
% 230.04/230.05 cnf(141,plain,
% 230.04/230.05 (~P2(a3,f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[45,60])).
% 230.04/230.05 cnf(145,plain,
% 230.04/230.05 (~P2(a14,f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[45,125,60,55,61])).
% 230.04/230.05 cnf(147,plain,
% 230.04/230.05 (~E(a13,f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[45,125,136,60,55,61,26])).
% 230.04/230.05 cnf(149,plain,
% 230.04/230.05 (~E(a14,f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[45,34,125,136,60,55,61,26,12,13])).
% 230.04/230.05 cnf(162,plain,
% 230.04/230.05 (~P2(a14,f2(a1,a16))),
% 230.04/230.05 inference(scs_inference,[],[44,60])).
% 230.04/230.05 cnf(166,plain,
% 230.04/230.05 (~P2(a13,f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[44,45,87,145,60,55,61])).
% 230.04/230.05 cnf(173,plain,
% 230.04/230.05 (P11(f2(a1,a12),f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[32,44,45,86,98,87,141,145,147,60,55,61,50,13,5,11,26])).
% 230.04/230.05 cnf(183,plain,
% 230.04/230.05 (~P2(a13,a14)),
% 230.04/230.05 inference(scs_inference,[],[35,60])).
% 230.04/230.05 cnf(185,plain,
% 230.04/230.05 (~P11(f2(a1,a16),a14)),
% 230.04/230.05 inference(scs_inference,[],[35,162,60,55])).
% 230.04/230.05 cnf(187,plain,
% 230.04/230.05 (~P2(a13,f2(a1,a16))),
% 230.04/230.05 inference(scs_inference,[],[44,35,162,60,55,61])).
% 230.04/230.05 cnf(189,plain,
% 230.04/230.05 (~E(f2(a1,a16),a13)),
% 230.04/230.05 inference(scs_inference,[],[44,35,162,60,55,61,12])).
% 230.04/230.05 cnf(190,plain,
% 230.04/230.05 (~E(a13,f2(a1,a16))),
% 230.04/230.05 inference(scs_inference,[],[44,35,162,60,55,61,12,13])).
% 230.04/230.05 cnf(192,plain,
% 230.04/230.05 (P11(a13,f2(a1,a16))),
% 230.04/230.05 inference(scs_inference,[],[44,35,136,162,60,55,61,12,13,27,50])).
% 230.04/230.05 cnf(203,plain,
% 230.04/230.05 (~P2(f2(a1,a12),a3)),
% 230.04/230.05 inference(scs_inference,[],[98,60])).
% 230.04/230.05 cnf(207,plain,
% 230.04/230.05 (P2(f2(a1,a16),a13)),
% 230.04/230.05 inference(scs_inference,[],[44,35,98,166,60,55,61])).
% 230.04/230.05 cnf(209,plain,
% 230.04/230.05 (~E(a3,a13)),
% 230.04/230.05 inference(scs_inference,[],[44,34,35,98,166,183,60,55,61,12])).
% 230.04/230.05 cnf(210,plain,
% 230.04/230.05 (P2(f2(a1,a17),f2(a1,a12))),
% 230.04/230.05 inference(scs_inference,[],[44,34,35,86,98,166,99,183,60,55,61,12,13])).
% 230.04/230.05 cnf(214,plain,
% 230.04/230.05 (~P2(f2(a1,a12),f2(a1,a17))),
% 230.04/230.05 inference(scs_inference,[],[210,60])).
% 230.04/230.05 cnf(218,plain,
% 230.04/230.05 (P2(a8,a18)),
% 230.04/230.05 inference(scs_inference,[],[210,187,36,37,60,55,61])).
% 230.04/230.05 cnf(220,plain,
% 230.04/230.05 (P2(f2(a1,a16),f2(a1,a12))),
% 230.04/230.06 inference(scs_inference,[],[86,210,187,207,36,37,60,55,61,13])).
% 230.04/230.06 cnf(227,plain,
% 230.04/230.06 (~P2(f2(a1,a12),f2(a1,a16))),
% 230.04/230.06 inference(scs_inference,[],[220,60])).
% 230.04/230.06 cnf(229,plain,
% 230.04/230.06 (~P11(a3,f2(a1,a12))),
% 230.04/230.06 inference(scs_inference,[],[220,203,60,55])).
% 230.04/230.06 cnf(231,plain,
% 230.04/230.06 (P2(a5,a4)),
% 230.04/230.06 inference(scs_inference,[],[220,203,38,41,60,55,61])).
% 230.04/230.06 cnf(236,plain,
% 230.04/230.06 (P2(x2361,a13)+~E(a14,x2361)),
% 230.04/230.06 inference(scs_inference,[],[35,220,173,203,38,41,141,60,55,61,27,50,12])).
% 230.04/230.06 cnf(241,plain,
% 230.04/230.06 (~P2(a8,a9)),
% 230.04/230.06 inference(scs_inference,[],[39,60])).
% 230.04/230.06 cnf(243,plain,
% 230.04/230.06 (~P11(f2(a1,a17),f2(a1,a12))),
% 230.04/230.06 inference(scs_inference,[],[214,39,60,55])).
% 230.04/230.06 cnf(245,plain,
% 230.04/230.06 (P2(a9,a18)),
% 230.04/230.06 inference(scs_inference,[],[214,39,218,60,55,61])).
% 230.04/230.06 cnf(247,plain,
% 230.04/230.06 (~E(a5,a8)),
% 230.04/230.06 inference(scs_inference,[],[214,39,218,41,60,55,61,12])).
% 230.04/230.06 cnf(248,plain,
% 230.04/230.06 (~E(a18,a9)),
% 230.04/230.06 inference(scs_inference,[],[214,39,218,41,60,55,61,12,13])).
% 230.04/230.06 cnf(250,plain,
% 230.04/230.06 (E(a13,a14)+P11(a13,a14)),
% 230.04/230.06 inference(scs_inference,[],[192,214,39,218,183,41,60,55,61,12,13,27,50])).
% 230.04/230.06 cnf(255,plain,
% 230.04/230.06 (~P2(a8,a5)),
% 230.04/230.06 inference(scs_inference,[],[40,60])).
% 230.04/230.06 cnf(257,plain,
% 230.04/230.06 (~P11(f2(a1,a16),f2(a1,a12))),
% 230.04/230.06 inference(scs_inference,[],[227,40,60,55])).
% 230.04/230.06 cnf(259,plain,
% 230.04/230.06 (P2(a5,a18)),
% 230.04/230.06 inference(scs_inference,[],[227,40,245,41,60,55,61])).
% 230.04/230.06 cnf(261,plain,
% 230.04/230.06 (~E(a4,a9)),
% 230.04/230.06 inference(scs_inference,[],[227,40,241,245,37,41,60,55,61,13])).
% 230.04/230.06 cnf(264,plain,
% 230.04/230.06 (E(a9,a8)+P11(a8,a9)),
% 230.04/230.06 inference(scs_inference,[],[227,40,241,245,37,41,60,55,61,13,50,2])).
% 230.04/230.06 cnf(268,plain,
% 230.04/230.06 (~P2(a4,a8)),
% 230.04/230.06 inference(scs_inference,[],[37,60])).
% 230.04/230.06 cnf(270,plain,
% 230.04/230.06 (~P11(a5,a8)),
% 230.04/230.06 inference(scs_inference,[],[37,255,60,55])).
% 230.04/230.06 cnf(272,plain,
% 230.04/230.06 (~E(f2(a1,a16),f2(a1,a12))),
% 230.04/230.06 inference(scs_inference,[],[32,189,37,255,60,55,3])).
% 230.04/230.06 cnf(273,plain,
% 230.04/230.06 (~P2(a4,a5)),
% 230.04/230.06 inference(scs_inference,[],[32,189,37,255,40,60,55,3,61])).
% 230.04/230.06 cnf(276,plain,
% 230.04/230.06 (~E(a4,a5)),
% 230.04/230.06 inference(scs_inference,[],[32,189,37,255,40,60,55,3,61,12,13])).
% 230.04/230.06 cnf(284,plain,
% 230.04/230.06 (~P2(a18,a8)),
% 230.04/230.06 inference(scs_inference,[],[218,60])).
% 230.04/230.06 cnf(286,plain,
% 230.04/230.06 (~P11(a8,a4)),
% 230.04/230.06 inference(scs_inference,[],[218,268,60,55])).
% 230.04/230.06 cnf(288,plain,
% 230.04/230.06 (~E(a3,f2(a1,a12))),
% 230.04/230.06 inference(scs_inference,[],[32,209,218,268,60,55,3])).
% 230.04/230.06 cnf(289,plain,
% 230.04/230.06 (~E(a9,a4)),
% 230.04/230.06 inference(scs_inference,[],[32,209,218,268,39,60,55,3,12])).
% 230.04/230.06 cnf(290,plain,
% 230.04/230.06 (~E(a18,a5)),
% 230.04/230.06 inference(scs_inference,[],[32,209,218,268,255,39,60,55,3,12,13])).
% 230.04/230.06 cnf(298,plain,
% 230.04/230.06 (~P2(a9,a5)),
% 230.04/230.06 inference(scs_inference,[],[41,60])).
% 230.04/230.06 cnf(300,plain,
% 230.04/230.06 (~P11(a5,a4)),
% 230.04/230.06 inference(scs_inference,[],[273,41,60,55])).
% 230.04/230.06 cnf(302,plain,
% 230.04/230.06 (~P2(a18,a5)),
% 230.04/230.06 inference(scs_inference,[],[273,41,284,40,60,55,61])).
% 230.04/230.06 cnf(306,plain,
% 230.04/230.06 (~E(a5,a18)),
% 230.04/230.06 inference(scs_inference,[],[273,41,284,290,40,60,55,61,50,12])).
% 230.04/230.06 cnf(307,plain,
% 230.04/230.06 (~E(a8,a5)),
% 230.04/230.06 inference(scs_inference,[],[273,41,284,290,40,39,60,55,61,50,12,13])).
% 230.04/230.06 cnf(315,plain,
% 230.04/230.06 (~P2(a4,a9)),
% 230.04/230.06 inference(scs_inference,[],[38,60])).
% 230.04/230.06 cnf(317,plain,
% 230.04/230.06 (~P11(a5,a9)),
% 230.04/230.06 inference(scs_inference,[],[298,38,60,55])).
% 230.04/230.06 cnf(321,plain,
% 230.04/230.06 (~E(a9,a18)),
% 230.04/230.06 inference(scs_inference,[],[298,307,38,284,255,39,60,55,50,12])).
% 230.04/230.06 cnf(329,plain,
% 230.04/230.06 (~P2(a18,a9)),
% 230.04/230.06 inference(scs_inference,[],[245,60])).
% 230.04/230.06 cnf(331,plain,
% 230.04/230.06 (~P11(a5,a18)),
% 230.04/230.06 inference(scs_inference,[],[302,245,60,55])).
% 230.04/230.06 cnf(333,plain,
% 230.04/230.06 (P11(a4,a9)),
% 230.04/230.06 inference(scs_inference,[],[261,302,315,245,60,55,50])).
% 230.04/230.06 cnf(340,plain,
% 230.04/230.06 (~P2(a18,a4)),
% 230.04/230.06 inference(scs_inference,[],[36,60])).
% 230.04/230.06 cnf(342,plain,
% 230.04/230.06 (~P11(a9,a18)),
% 230.04/230.06 inference(scs_inference,[],[329,36,60,55])).
% 230.04/230.06 cnf(344,plain,
% 230.04/230.06 (P11(a18,a9)),
% 230.04/230.06 inference(scs_inference,[],[248,329,36,60,55,50])).
% 230.04/230.06 cnf(346,plain,
% 230.04/230.06 (~E(a8,a18)),
% 230.04/230.06 inference(scs_inference,[],[37,248,329,36,60,55,50,12])).
% 230.04/230.06 cnf(347,plain,
% 230.04/230.06 (~P2(x3471,f2(a1,a16))+P2(x3471,a13)),
% 230.04/230.06 inference(scs_inference,[],[207,37,248,329,36,60,55,50,12,61])).
% 230.04/230.06 cnf(353,plain,
% 230.04/230.06 (~P11(a4,a18)),
% 230.04/230.06 inference(scs_inference,[],[340,55])).
% 230.04/230.06 cnf(362,plain,
% 230.04/230.06 (~P11(a9,a4)),
% 230.04/230.06 inference(scs_inference,[],[315,55])).
% 230.04/230.06 cnf(376,plain,
% 230.04/230.06 (~P11(a14,a13)),
% 230.04/230.06 inference(scs_inference,[],[183,55])).
% 230.04/230.06 cnf(384,plain,
% 230.04/230.06 (~P11(a9,a8)),
% 230.04/230.06 inference(scs_inference,[],[241,55])).
% 230.04/230.06 cnf(397,plain,
% 230.04/230.06 (~P11(a8,a18)),
% 230.04/230.06 inference(scs_inference,[],[284,55])).
% 230.04/230.06 cnf(407,plain,
% 230.04/230.06 (P11(a18,x4071)+~E(a9,x4071)),
% 230.04/230.06 inference(scs_inference,[],[344,27])).
% 230.04/230.06 cnf(412,plain,
% 230.04/230.06 (E(a18,a8)+P11(a18,a8)),
% 230.04/230.06 inference(scs_inference,[],[284,50])).
% 230.04/230.06 cnf(437,plain,
% 230.04/230.06 (~E(a18,a8)),
% 230.04/230.06 inference(scs_inference,[],[36,268,13])).
% 230.04/230.06 cnf(439,plain,
% 230.04/230.06 (P11(a18,x4391)+~E(a8,x4391)),
% 230.04/230.06 inference(scs_inference,[],[36,268,13,412,27])).
% 230.04/230.06 cnf(465,plain,
% 230.04/230.06 (P2(x4651,a18)+~E(a9,x4651)),
% 230.04/230.06 inference(scs_inference,[],[245,12])).
% 230.04/230.06 cnf(493,plain,
% 230.04/230.06 (P2(a5,x4931)+~E(a18,x4931)),
% 230.04/230.06 inference(scs_inference,[],[259,13])).
% 230.04/230.06 cnf(497,plain,
% 230.04/230.06 (P2(a5,x4971)+~E(a9,x4971)),
% 230.04/230.06 inference(scs_inference,[],[41,13])).
% 230.04/230.06 cnf(519,plain,
% 230.04/230.06 (E(a14,a13)+P11(a13,a14)),
% 230.04/230.06 inference(scs_inference,[],[250,2])).
% 230.04/230.06 cnf(521,plain,
% 230.04/230.06 (P10(a8,a9)+E(a9,a8)),
% 230.04/230.06 inference(scs_inference,[],[264,52])).
% 230.04/230.06 cnf(533,plain,
% 230.04/230.06 (P10(a13,a14)+E(a14,a13)),
% 230.04/230.06 inference(scs_inference,[],[519,52])).
% 230.04/230.06 cnf(535,plain,
% 230.04/230.06 (P10(x5351,a9)+~E(a8,x5351)+E(a9,a8)),
% 230.04/230.06 inference(scs_inference,[],[521,22])).
% 230.04/230.06 cnf(549,plain,
% 230.04/230.06 (P10(f2(a1,a12),a14)+E(a14,a13)),
% 230.04/230.06 inference(scs_inference,[],[86,533,22])).
% 230.04/230.06 cnf(564,plain,
% 230.04/230.06 (P2(a5,a13)+~E(a18,f2(a1,a16))),
% 230.04/230.06 inference(scs_inference,[],[347,493])).
% 230.04/230.06 cnf(577,plain,
% 230.04/230.06 (~P9(a1,a12)+E(a14,a13)),
% 230.04/230.06 inference(scs_inference,[],[31,549,73])).
% 230.04/230.06 cnf(581,plain,
% 230.04/230.06 (P11(a13,a5)+~E(a18,f2(a1,a16))),
% 230.04/230.06 inference(scs_inference,[],[564,53])).
% 230.04/230.06 cnf(723,plain,
% 230.04/230.06 (P7(a1,a17)+P9(a1,a12)+E(f6(a1,a12),a9)),
% 230.04/230.06 inference(scs_inference,[],[112,30,89,79,64])).
% 230.04/230.06 cnf(818,plain,
% 230.04/230.06 (~E(f6(a1,a12),f6(a1,a15))+~P11(f6(a1,a16),f6(a1,a17))+~P11(f6(a1,a17),f6(a1,a15))),
% 230.04/230.06 inference(scs_inference,[],[83,2])).
% 230.04/230.06 cnf(879,plain,
% 230.04/230.06 (E(f2(a13,x8791),f2(f2(a1,a12),x8791))),
% 230.04/230.06 inference(scs_inference,[],[32,2,4])).
% 230.04/230.06 cnf(880,plain,
% 230.04/230.06 (E(f2(f2(a1,a12),x8801),f2(a13,x8801))),
% 230.04/230.06 inference(scs_inference,[],[879,2])).
% 230.04/230.06 cnf(892,plain,
% 230.04/230.06 (P5(x8921,x8921)),
% 230.04/230.06 inference(rename_variables,[],[85])).
% 230.04/230.06 cnf(895,plain,
% 230.04/230.06 (P10(f2(f2(a1,a12),x8951),f2(a13,x8951))),
% 230.04/230.06 inference(scs_inference,[],[879,85,892,84,29,28,22])).
% 230.04/230.06 cnf(901,plain,
% 230.04/230.06 (E(f2(x9011,a13),f2(x9011,f2(a1,a12)))),
% 230.04/230.06 inference(scs_inference,[],[32,2,5])).
% 230.04/230.06 cnf(902,plain,
% 230.04/230.06 (E(f2(x9021,f2(a1,a12)),f2(x9021,a13))),
% 230.04/230.06 inference(scs_inference,[],[901,2])).
% 230.04/230.06 cnf(903,plain,
% 230.04/230.06 (E(f2(f2(a1,a12),a13),f2(a13,f2(a1,a12)))),
% 230.04/230.06 inference(scs_inference,[],[880,901,2,3])).
% 230.04/230.06 cnf(917,plain,
% 230.04/230.06 (E(f2(a13,a13),f2(f2(a1,a12),f2(a1,a12)))),
% 230.04/230.06 inference(scs_inference,[],[879,903,901,2,3])).
% 230.04/230.06 cnf(924,plain,
% 230.04/230.06 (E(f2(f2(a1,a12),f2(a1,a12)),f2(a13,a13))),
% 230.04/230.06 inference(scs_inference,[],[917,2])).
% 230.04/230.06 cnf(1033,plain,
% 230.04/230.06 (E(f6(a13,x10331),f6(f2(a1,a12),x10331))),
% 230.04/230.06 inference(scs_inference,[],[32,2,6])).
% 230.04/230.06 cnf(1034,plain,
% 230.04/230.06 (E(f6(f2(a1,a12),x10341),f6(a13,x10341))),
% 230.04/230.06 inference(scs_inference,[],[1033,2])).
% 230.04/230.06 cnf(1090,plain,
% 230.04/230.07 (E(f6(x10901,a13),f6(x10901,f2(a1,a12)))),
% 230.04/230.07 inference(scs_inference,[],[32,2,7])).
% 230.04/230.07 cnf(1091,plain,
% 230.04/230.07 (E(f6(x10911,f2(a1,a12)),f6(x10911,a13))),
% 230.04/230.07 inference(scs_inference,[],[1090,2])).
% 230.04/230.07 cnf(1092,plain,
% 230.04/230.07 (E(f6(f2(a1,a12),a13),f6(a13,f2(a1,a12)))),
% 230.04/230.07 inference(scs_inference,[],[1034,1090,2,3])).
% 230.04/230.07 cnf(1108,plain,
% 230.04/230.07 (E(f6(a13,f2(a1,a12)),f6(f2(a1,a12),a13))),
% 230.04/230.07 inference(scs_inference,[],[1092,2])).
% 230.04/230.07 cnf(1109,plain,
% 230.04/230.07 (E(f6(f2(a1,a12),f2(a1,a12)),f6(a13,a13))),
% 230.04/230.07 inference(scs_inference,[],[1034,1091,1092,2,3])).
% 230.04/230.07 cnf(1126,plain,
% 230.04/230.07 (E(f6(a13,a13),f6(f2(a1,a12),f2(a1,a12)))),
% 230.04/230.07 inference(scs_inference,[],[1109,2])).
% 230.04/230.07 cnf(1223,plain,
% 230.04/230.07 (P5(f2(x12231,a13),f2(x12231,f2(a1,a12)))),
% 230.04/230.07 inference(scs_inference,[],[901,85,29])).
% 230.04/230.07 cnf(1224,plain,
% 230.04/230.07 (P5(x12241,x12241)),
% 230.04/230.07 inference(rename_variables,[],[85])).
% 230.04/230.07 cnf(1225,plain,
% 230.04/230.07 (P5(f2(x12251,f2(a1,a12)),f2(x12251,a13))),
% 230.04/230.07 inference(scs_inference,[],[901,85,1224,29,28])).
% 230.04/230.07 cnf(1401,plain,
% 230.04/230.07 (E(f10(a13),f10(f2(a1,a12)))),
% 230.04/230.07 inference(scs_inference,[],[32,2,9])).
% 230.04/230.07 cnf(1458,plain,
% 230.04/230.07 (~P5(f2(a1,a12),f2(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[116,214,2,57])).
% 230.04/230.07 cnf(1459,plain,
% 230.04/230.07 (P2(a14,f2(a1,a12))),
% 230.04/230.07 inference(scs_inference,[],[32,35,2,13])).
% 230.04/230.07 cnf(1460,plain,
% 230.04/230.07 (~P2(f2(a1,a12),a14)),
% 230.04/230.07 inference(scs_inference,[],[1459,60])).
% 230.04/230.07 cnf(1476,plain,
% 230.04/230.07 (P11(a13,a14)+P2(a13,f2(a1,a12))),
% 230.04/230.07 inference(scs_inference,[],[1459,125,13,12,519])).
% 230.04/230.07 cnf(1478,plain,
% 230.04/230.07 (P2(a13,f2(a1,a12))+~P9(a1,a12)),
% 230.04/230.07 inference(scs_inference,[],[1459,125,13,12,519,549,577])).
% 230.04/230.07 cnf(1485,plain,
% 230.04/230.07 (P2(a13,f2(a1,a12))+P10(a13,a14)),
% 230.04/230.07 inference(scs_inference,[],[1476,52])).
% 230.04/230.07 cnf(1486,plain,
% 230.04/230.07 (P11(f2(a1,a12),a13)+~P9(a1,a12)),
% 230.04/230.07 inference(scs_inference,[],[1478,53])).
% 230.04/230.07 cnf(1487,plain,
% 230.04/230.07 (~P2(f2(a1,a12),a13)+P10(a13,a14)),
% 230.04/230.07 inference(scs_inference,[],[1485,60])).
% 230.04/230.07 cnf(1488,plain,
% 230.04/230.07 (~E(f2(a1,a12),a14)+~P9(a1,a12)),
% 230.04/230.07 inference(scs_inference,[],[376,1486,26])).
% 230.04/230.07 cnf(1489,plain,
% 230.04/230.07 (P10(f2(a1,a12),a14)+~P2(f2(a1,a12),a13)),
% 230.04/230.07 inference(scs_inference,[],[86,1487,22])).
% 230.04/230.07 cnf(1495,plain,
% 230.04/230.07 (~P9(a1,a12)+~P2(f2(a1,a12),a13)),
% 230.04/230.07 inference(scs_inference,[],[31,1489,73])).
% 230.04/230.07 cnf(1536,plain,
% 230.04/230.07 (E(f2(f2(f2(a1,a12),f2(a1,a12)),x15361),f2(f2(a13,a13),x15361))),
% 230.04/230.07 inference(scs_inference,[],[917,2,4])).
% 230.04/230.07 cnf(1537,plain,
% 230.04/230.07 (E(f2(x15371,f2(a13,a13)),f2(x15371,f2(f2(a1,a12),f2(a1,a12))))),
% 230.04/230.07 inference(scs_inference,[],[924,2,5])).
% 230.04/230.07 cnf(1539,plain,
% 230.04/230.07 (E(f6(x15391,f6(a13,x15392)),f6(x15391,f6(f2(a1,a12),x15392)))),
% 230.04/230.07 inference(scs_inference,[],[1034,2,7])).
% 230.04/230.07 cnf(1542,plain,
% 230.04/230.07 (E(f2(f6(a13,f2(a1,a12)),x15421),f2(f6(f2(a1,a12),a13),x15421))),
% 230.04/230.07 inference(scs_inference,[],[1092,2,4])).
% 230.04/230.07 cnf(1543,plain,
% 230.04/230.07 (E(f2(x15431,f6(f2(a1,a12),a13)),f2(x15431,f6(a13,f2(a1,a12))))),
% 230.04/230.07 inference(scs_inference,[],[1108,2,5])).
% 230.04/230.07 cnf(1544,plain,
% 230.04/230.07 (E(f6(f6(a13,a13),x15441),f6(f6(f2(a1,a12),f2(a1,a12)),x15441))),
% 230.04/230.07 inference(scs_inference,[],[1109,2,6])).
% 230.04/230.07 cnf(1551,plain,
% 230.04/230.07 (P7(a1,a17)+E(a8,f6(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[30,131,89,2,63])).
% 230.04/230.07 cnf(1556,plain,
% 230.04/230.07 (~P9(a1,a12)+E(a4,f6(a1,a12))),
% 230.04/230.07 inference(scs_inference,[],[30,91,89,2,66])).
% 230.04/230.07 cnf(1557,plain,
% 230.04/230.07 (E(a4,f6(a1,a12))+E(f6(a1,a12),a9)),
% 230.04/230.07 inference(scs_inference,[],[91,30,89,1556,64])).
% 230.04/230.07 cnf(1558,plain,
% 230.04/230.07 (E(f11(f6(a1,a12)),f11(a9))+E(a4,f6(a1,a12))),
% 230.04/230.07 inference(scs_inference,[],[1557,8])).
% 230.04/230.07 cnf(1560,plain,
% 230.04/230.07 (P7(a1,a16)+E(a8,f6(a1,a16))),
% 230.04/230.07 inference(scs_inference,[],[30,93,89,2,63])).
% 230.04/230.07 cnf(1564,plain,
% 230.04/230.07 (~P7(a1,a15)+E(a9,f6(a1,a15))),
% 230.04/230.07 inference(scs_inference,[],[95,30,89,2,64])).
% 230.04/230.07 cnf(1584,plain,
% 230.04/230.07 (P10(f6(a1,a12),a4)+~P9(a1,a12)),
% 230.04/230.07 inference(scs_inference,[],[30,91,89,48,66])).
% 230.04/230.07 cnf(1616,plain,
% 230.04/230.07 (P5(f6(a1,a12),a4)+~P9(a1,a12)),
% 230.04/230.07 inference(scs_inference,[],[30,91,89,49,66])).
% 230.04/230.07 cnf(1621,plain,
% 230.04/230.07 (P5(f6(a1,a17),a8)+P7(a1,a17)),
% 230.04/230.07 inference(scs_inference,[],[30,131,89,49,63])).
% 230.04/230.07 cnf(1629,plain,
% 230.04/230.07 (P5(f6(a1,a16),a8)+P7(a1,a16)),
% 230.04/230.07 inference(scs_inference,[],[30,93,89,49,63])).
% 230.04/230.07 cnf(1656,plain,
% 230.04/230.07 (P10(a13,a14)+E(a13,a14)),
% 230.04/230.07 inference(scs_inference,[],[52,250])).
% 230.04/230.07 cnf(1657,plain,
% 230.04/230.07 (P10(a13,a14)+E(f2(a13,x16571),f2(a14,x16571))),
% 230.04/230.07 inference(scs_inference,[],[1656,4])).
% 230.04/230.07 cnf(1658,plain,
% 230.04/230.07 (P10(f2(a1,a12),a14)+E(f2(a13,x16581),f2(a14,x16581))),
% 230.04/230.07 inference(scs_inference,[],[86,1657,22])).
% 230.04/230.07 cnf(1659,plain,
% 230.04/230.07 (~P9(a1,a12)+E(f2(a13,x16591),f2(a14,x16591))),
% 230.04/230.07 inference(scs_inference,[],[31,1658,73])).
% 230.04/230.07 cnf(1660,plain,
% 230.04/230.07 (E(f2(a13,x16601),f2(a14,x16601))+E(f6(a1,a12),a9)),
% 230.04/230.07 inference(scs_inference,[],[91,30,89,1659,64])).
% 230.04/230.07 cnf(1661,plain,
% 230.04/230.07 (E(a9,f6(a1,a12))+E(f2(a13,x16611),f2(a14,x16611))),
% 230.04/230.07 inference(scs_inference,[],[1660,2])).
% 230.04/230.07 cnf(1700,plain,
% 230.04/230.07 (P10(a18,x17001)+~E(a9,x17001)),
% 230.04/230.07 inference(scs_inference,[],[52,407])).
% 230.04/230.07 cnf(1745,plain,
% 230.04/230.07 (P10(a18,x17451)+~E(a8,x17451)),
% 230.04/230.07 inference(scs_inference,[],[52,439])).
% 230.04/230.07 cnf(1760,plain,
% 230.04/230.07 (P10(a13,a5)+~E(a18,f2(a1,a16))),
% 230.04/230.07 inference(scs_inference,[],[52,581])).
% 230.04/230.07 cnf(1761,plain,
% 230.04/230.07 (~E(f2(a1,a16),a18)+P10(a13,a5)),
% 230.04/230.07 inference(scs_inference,[],[1760,2])).
% 230.04/230.07 cnf(1762,plain,
% 230.04/230.07 (~E(x17621,a18)+~E(f2(a1,a16),x17621)+P10(a13,a5)),
% 230.04/230.07 inference(scs_inference,[],[1761,3])).
% 230.04/230.07 cnf(1882,plain,
% 230.04/230.07 (~P9(a1,a12)+E(f6(a1,a12),a4)),
% 230.04/230.07 inference(scs_inference,[],[112,91,89,71,66])).
% 230.04/230.07 cnf(1883,plain,
% 230.04/230.07 (E(f6(a1,a12),a4)+E(f6(a1,a12),a9)),
% 230.04/230.07 inference(scs_inference,[],[91,30,89,1882,64])).
% 230.04/230.07 cnf(1884,plain,
% 230.04/230.07 (E(a9,f6(a1,a12))+E(f6(a1,a12),a4)),
% 230.04/230.07 inference(scs_inference,[],[1883,2])).
% 230.04/230.07 cnf(1887,plain,
% 230.04/230.07 (P7(a1,a16)+E(f6(a1,a16),a8)),
% 230.04/230.07 inference(scs_inference,[],[112,93,89,71,63])).
% 230.04/230.07 cnf(1896,plain,
% 230.04/230.07 (~P7(a1,a15)+E(f6(a1,a15),a9)),
% 230.04/230.07 inference(scs_inference,[],[112,95,89,71,64])).
% 230.04/230.07 cnf(1907,plain,
% 230.04/230.07 (~P2(f2(a1,a15),a14)),
% 230.04/230.07 inference(scs_inference,[],[31,103,333,231,34,1401,95,52,49,54,53,2,68])).
% 230.04/230.07 cnf(1909,plain,
% 230.04/230.07 (~P7(a1,a17)),
% 230.04/230.07 inference(scs_inference,[],[31,103,333,231,34,1401,95,112,91,52,49,54,53,2,68,80])).
% 230.04/230.07 cnf(1911,plain,
% 230.04/230.07 (~P10(f2(a1,a16),a14)),
% 230.04/230.07 inference(scs_inference,[],[31,103,333,231,34,1401,95,93,112,91,52,49,54,53,2,68,80,73])).
% 230.04/230.07 cnf(1917,plain,
% 230.04/230.07 (~E(f2(a1,a17),f2(a1,a15))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1401,95,93,112,91,52,49,54,53,2,68,80,73,57,56,12])).
% 230.04/230.07 cnf(1921,plain,
% 230.04/230.07 (~E(a3,a14)),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,93,86,112,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23])).
% 230.04/230.07 cnf(1924,plain,
% 230.04/230.07 (E(f6(a1,a17),a8)),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63])).
% 230.04/230.07 cnf(1927,plain,
% 230.04/230.07 (P10(f6(a1,a17),a8)),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48])).
% 230.04/230.07 cnf(1929,plain,
% 230.04/230.07 (E(f11(f6(a1,a17)),f11(a8))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8])).
% 230.04/230.07 cnf(1930,plain,
% 230.04/230.07 (E(f10(f6(a1,a17)),f10(a8))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9])).
% 230.04/230.07 cnf(1931,plain,
% 230.04/230.07 (E(f2(f6(a1,a17),x19311),f2(a8,x19311))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4])).
% 230.04/230.07 cnf(1932,plain,
% 230.04/230.07 (E(f6(f6(a1,a17),x19321),f6(a8,x19321))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6])).
% 230.04/230.07 cnf(1933,plain,
% 230.04/230.07 (E(f6(x19331,f6(a1,a17)),f6(x19331,a8))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6,7])).
% 230.04/230.07 cnf(1934,plain,
% 230.04/230.07 (E(a8,f6(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6,7,1551])).
% 230.04/230.07 cnf(1935,plain,
% 230.04/230.07 (P5(f6(a1,a17),a8)),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6,7,1551,1621])).
% 230.04/230.07 cnf(1936,plain,
% 230.04/230.07 (E(f2(x19361,f6(a1,a17)),f2(x19361,a8))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6,7,1551,1621,5])).
% 230.04/230.07 cnf(1938,plain,
% 230.04/230.07 (E(f2(f6(a1,a17),f2(a1,a12)),f2(a8,a13))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,362,333,273,231,129,1126,902,34,1458,43,84,1401,95,89,93,131,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6,7,1551,1621,5,24,3])).
% 230.04/230.07 cnf(1944,plain,
% 230.04/230.07 (~P2(a4,f6(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[31,103,276,289,384,362,286,333,273,231,129,1126,902,34,268,1458,43,84,1401,95,89,93,131,85,86,112,30,91,52,49,54,53,2,68,80,73,57,56,12,28,22,23,75,63,48,8,9,4,6,7,1551,1621,5,24,3,26,29,27,13])).
% 230.04/230.07 cnf(1948,plain,
% 230.04/230.07 (E(f6(a1,a12),a9)+P9(a1,a12)),
% 230.04/230.07 inference(scs_inference,[],[1909,723])).
% 230.04/230.07 cnf(1953,plain,
% 230.04/230.07 (P5(f2(x19531,f6(a1,a17)),f2(x19531,a8))),
% 230.04/230.07 inference(scs_inference,[],[1936,49])).
% 230.04/230.07 cnf(1955,plain,
% 230.04/230.07 (E(f2(a8,x19551),f2(f6(a1,a17),x19551))),
% 230.04/230.07 inference(scs_inference,[],[1936,1934,49,4])).
% 230.04/230.07 cnf(1960,plain,
% 230.04/230.07 (E(f6(a8,x19601),f6(f6(a1,a17),x19601))),
% 230.04/230.07 inference(scs_inference,[],[1936,1934,38,36,49,4,53,54,6])).
% 230.04/230.07 cnf(1964,plain,
% 230.04/230.07 (P10(f2(x19641,f6(a1,a17)),f2(x19641,a8))),
% 230.04/230.07 inference(scs_inference,[],[1936,1934,38,36,49,4,53,54,6,52,9,48])).
% 230.04/230.07 cnf(1966,plain,
% 230.04/230.07 (E(f6(x19661,a8),f6(x19661,f6(a1,a17)))),
% 230.04/230.07 inference(scs_inference,[],[1936,1934,38,36,49,4,53,54,6,52,9,48,7])).
% 230.04/230.07 cnf(1967,plain,
% 230.04/230.07 (E(f11(a8),f11(f6(a1,a17)))),
% 230.04/230.07 inference(scs_inference,[],[1936,1934,38,36,49,4,53,54,6,52,9,48,7,8])).
% 230.04/230.07 cnf(1968,plain,
% 230.04/230.07 (E(f2(x19681,a8),f2(x19681,f6(a1,a17)))),
% 230.04/230.07 inference(scs_inference,[],[1936,1934,38,36,49,4,53,54,6,52,9,48,7,8,5])).
% 230.04/230.07 cnf(1972,plain,
% 230.04/230.07 (~P5(a13,f2(a1,a16))),
% 230.04/230.07 inference(scs_inference,[],[133,190,1944,1936,1934,187,38,36,49,4,53,54,6,52,9,48,7,8,5,2,61,57])).
% 230.04/230.07 cnf(1974,plain,
% 230.04/230.07 (~P10(a5,a8)),
% 230.04/230.07 inference(scs_inference,[],[133,247,190,1944,1936,270,1934,187,38,36,49,4,53,54,6,52,9,48,7,8,5,2,61,57,56])).
% 230.04/230.07 cnf(1976,plain,
% 230.04/230.07 (E(f2(f6(a1,a17),f6(a1,a17)),f2(a8,a8))),
% 230.04/230.07 inference(scs_inference,[],[133,247,190,1944,1936,1931,270,1934,187,38,36,49,4,53,54,6,52,9,48,7,8,5,2,61,57,56,3])).
% 230.04/230.07 cnf(1979,plain,
% 230.04/230.07 (~P11(f6(a1,a17),a18)),
% 230.04/230.07 inference(scs_inference,[],[133,247,190,1924,1944,1936,1931,270,1934,397,187,38,36,49,4,53,54,6,52,9,48,7,8,5,2,61,57,56,3,26])).
% 230.04/230.07 cnf(1981,plain,
% 230.04/230.07 (~P11(a5,f6(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[133,247,190,1924,1944,1936,1931,270,1934,397,187,38,241,36,49,4,53,54,6,52,9,48,7,8,5,2,61,57,56,3,26,12,27])).
% 230.04/230.07 cnf(1992,plain,
% 230.04/230.07 (P5(f6(x19921,f6(a1,a17)),f6(x19921,a8))),
% 230.04/230.07 inference(scs_inference,[],[1933,49])).
% 230.04/230.07 cnf(1996,plain,
% 230.04/230.07 (P11(a8,a9)),
% 230.04/230.07 inference(scs_inference,[],[1933,129,39,49,54,53])).
% 230.04/230.07 cnf(2000,plain,
% 230.04/230.07 (P10(f6(x20001,f6(a1,a17)),f6(x20001,a8))),
% 230.04/230.07 inference(scs_inference,[],[1933,129,39,49,54,53,52,48])).
% 230.04/230.07 cnf(2002,plain,
% 230.04/230.07 (~E(a14,a3)),
% 230.04/230.07 inference(scs_inference,[],[1921,1933,129,39,49,54,53,52,48,2])).
% 230.04/230.07 cnf(2003,plain,
% 230.04/230.07 (~P5(a13,a3)),
% 230.04/230.07 inference(scs_inference,[],[134,1921,1933,87,129,39,49,54,53,52,48,2,57])).
% 230.04/230.07 cnf(2005,plain,
% 230.04/230.07 (~P10(a9,a18)),
% 230.04/230.07 inference(scs_inference,[],[134,321,1921,1933,342,87,129,39,49,54,53,52,48,2,57,56])).
% 230.04/230.07 cnf(2007,plain,
% 230.04/230.07 (E(f6(f6(a1,a17),f6(a1,a17)),f6(a8,a8))),
% 230.04/230.07 inference(scs_inference,[],[134,321,1921,1933,1932,342,87,129,39,49,54,53,52,48,2,57,56,3])).
% 230.04/230.07 cnf(2010,plain,
% 230.04/230.07 (~P2(f6(a1,a17),a5)),
% 230.04/230.07 inference(scs_inference,[],[134,321,1921,1933,1932,342,87,129,255,1924,39,49,54,53,52,48,2,57,56,3,12])).
% 230.04/230.07 cnf(2012,plain,
% 230.04/230.07 (~E(f6(a1,a17),a5)),
% 230.04/230.07 inference(scs_inference,[],[134,321,1921,1974,1927,1972,1933,1932,342,87,129,255,1924,39,32,49,54,53,52,48,2,57,56,3,12,28,22])).
% 230.04/230.07 cnf(2028,plain,
% 230.04/230.07 (~E(f2(a1,a15),f2(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[1917,1929,1976,245,37,54,53,49,52,48,2])).
% 230.04/230.07 cnf(2029,plain,
% 230.04/230.07 (~P5(f6(a1,a17),a5)),
% 230.04/230.07 inference(scs_inference,[],[1917,2010,2012,1929,1976,245,37,54,53,49,52,48,2,57])).
% 230.04/230.07 cnf(2046,plain,
% 230.04/230.07 (P11(f2(a1,a12),a14)),
% 230.04/230.07 inference(scs_inference,[],[1459,53])).
% 230.04/230.07 cnf(2050,plain,
% 230.04/230.07 (P5(f6(f6(a1,a17),f6(a1,a17)),f6(a8,a8))),
% 230.04/230.07 inference(scs_inference,[],[2007,98,1459,53,54,49])).
% 230.04/230.07 cnf(2052,plain,
% 230.04/230.07 (P10(f2(a1,a12),a14)),
% 230.04/230.07 inference(scs_inference,[],[2007,98,1459,53,54,49,52])).
% 230.04/230.07 cnf(2057,plain,
% 230.04/230.07 (~P5(a18,a8)),
% 230.04/230.07 inference(scs_inference,[],[437,2007,2012,98,284,1459,53,54,49,52,48,2,57])).
% 230.04/230.07 cnf(2059,plain,
% 230.04/230.07 (P2(a5,f6(a1,a17))),
% 230.04/230.07 inference(scs_inference,[],[437,1981,2007,2012,98,284,1459,53,54,49,52,48,2,57,50])).
% 230.04/230.07 cnf(2063,plain,
% 230.04/230.07 (E(f2(a8,a8),f2(f6(a1,a17),f6(a1,a17)))),
% 230.04/230.07 inference(scs_inference,[],[306,437,1981,2007,1955,1968,331,2012,98,284,1459,53,54,49,52,48,2,57,50,56,3])).
% 230.04/230.07 cnf(2067,plain,
% 230.04/230.07 (~P5(a8,a5)),
% 230.04/230.07 inference(scs_inference,[],[306,437,1981,2029,2007,1955,1968,331,2012,98,284,1924,1934,1459,53,54,49,52,48,2,57,50,56,3,29,28])).
% 230.04/230.07 cnf(2087,plain,
% 230.04/230.07 (E(f6(a8,a8),f6(f6(a1,a17),f6(a1,a17)))),
% 230.04/230.08 inference(scs_inference,[],[149,2059,1938,1966,272,257,1960,145,54,53,49,52,48,57,56,3])).
% 230.04/230.08 cnf(2098,plain,
% 230.04/230.08 (P11(a13,a14)),
% 230.04/230.08 inference(scs_inference,[],[31,149,2046,2059,1938,1966,272,257,1225,1223,1960,145,131,86,32,54,53,49,52,48,57,56,3,29,28,23,24,73,26])).
% 230.04/230.08 cnf(2103,plain,
% 230.04/230.08 (P11(a9,a5)),
% 230.04/230.08 inference(scs_inference,[],[41,53])).
% 230.04/230.08 cnf(2109,plain,
% 230.04/230.08 (P5(f6(a8,a8),f6(f6(a1,a17),f6(a1,a17)))),
% 230.04/230.08 inference(scs_inference,[],[2098,2087,99,41,53,54,52,49])).
% 230.04/230.08 cnf(2111,plain,
% 230.04/230.08 (P10(f6(a8,a8),f6(f6(a1,a17),f6(a1,a17)))),
% 230.04/230.08 inference(scs_inference,[],[2098,2087,99,41,53,54,52,49,48])).
% 230.04/230.08 cnf(2117,plain,
% 230.04/230.08 (E(f2(a13,a8),f2(f2(a1,a12),f6(a1,a17)))),
% 230.04/230.08 inference(scs_inference,[],[2098,2087,2002,243,1968,99,116,125,41,879,53,54,52,49,48,57,56,3])).
% 230.04/230.08 cnf(2120,plain,
% 230.04/230.08 (~E(f6(a1,a17),a18)),
% 230.04/230.08 inference(scs_inference,[],[2098,2057,1935,2087,2002,243,1968,99,116,125,41,879,53,54,52,49,48,57,56,3,28])).
% 230.04/230.08 cnf(2127,plain,
% 230.04/230.08 (P2(f6(a1,a17),a18)),
% 230.04/230.08 inference(scs_inference,[],[2098,2057,1935,1979,2087,2002,243,1968,895,2059,1936,99,116,125,41,879,53,54,52,49,48,57,56,3,28,23,2,61,50])).
% 230.04/230.08 cnf(2138,plain,
% 230.04/230.08 (P11(a18,f6(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[2127,54,53])).
% 230.04/230.08 cnf(2142,plain,
% 230.04/230.08 (P10(a9,a5)),
% 230.04/230.08 inference(scs_inference,[],[2103,2127,2117,54,53,49,52])).
% 230.04/230.08 cnf(2146,plain,
% 230.04/230.08 (~P2(f2(a1,a15),f2(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[2103,1907,2127,2117,129,54,53,49,52,48,61])).
% 230.04/230.08 cnf(2152,plain,
% 230.04/230.08 (E(f6(a13,a8),f6(f2(a1,a12),f6(a1,a17)))),
% 230.04/230.08 inference(scs_inference,[],[2103,1907,2120,2127,2117,1966,1979,248,329,129,1033,54,53,49,52,48,61,57,56,3])).
% 230.04/230.08 cnf(2157,plain,
% 230.04/230.08 (~P10(a8,a18)),
% 230.04/230.08 inference(scs_inference,[],[2103,1907,2120,2127,2050,2117,1966,1979,248,329,1933,129,1934,1033,54,53,49,52,48,61,57,56,3,28,22])).
% 230.04/230.08 cnf(2182,plain,
% 230.04/230.08 (P11(f2(a1,a15),f2(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[2146,2138,2152,2028,207,45,53,54,52,49,48,57,50])).
% 230.04/230.08 cnf(2187,plain,
% 230.04/230.08 (E(f6(x21871,f6(a1,a17)),f6(x21871,a8))),
% 230.04/230.08 inference(rename_variables,[],[1933])).
% 230.04/230.08 cnf(2193,plain,
% 230.04/230.08 (P2(f2(a1,a17),f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2146,2138,1964,2109,2111,2152,2028,2003,229,288,1976,207,1933,2187,45,32,53,54,52,49,48,57,50,56,29,28,22,23,55])).
% 230.04/230.08 cnf(2208,plain,
% 230.04/230.08 (~P5(a4,a9)),
% 230.04/230.08 inference(scs_inference,[],[2182,2193,1967,2063,261,315,54,52,49,48,57])).
% 230.04/230.08 cnf(2254,plain,
% 230.04/230.08 (P10(f6(f6(a1,a17),x22541),f6(a8,x22541))),
% 230.04/230.08 inference(scs_inference,[],[1932,218,54,49,48])).
% 230.04/230.08 cnf(2261,plain,
% 230.04/230.08 (~P2(x22611,a5)+~E(x22611,a4)),
% 230.04/230.08 inference(scs_inference,[],[1992,1932,273,290,302,218,1033,54,49,48,57,28,12])).
% 230.04/230.08 cnf(2304,plain,
% 230.04/230.08 (P5(a9,a8)),
% 230.04/230.08 inference(scs_inference,[],[39,54])).
% 230.04/230.08 cnf(2328,plain,
% 230.04/230.08 (P5(a8,a4)),
% 230.04/230.08 inference(scs_inference,[],[37,54])).
% 230.04/230.08 cnf(2337,plain,
% 230.04/230.08 (~P2(x23371,a5)+~E(x23371,a9)),
% 230.04/230.08 inference(scs_inference,[],[2254,1930,298,1091,37,54,49,48,23,12])).
% 230.04/230.08 cnf(2343,plain,
% 230.04/230.08 (P9(a1,a12)+E(f2(f6(a1,a12),x23431),f2(a9,x23431))),
% 230.04/230.08 inference(scs_inference,[],[1948,4])).
% 230.04/230.08 cnf(2348,plain,
% 230.04/230.08 (P10(f2(f6(a1,a17),x23481),f2(a8,x23481))),
% 230.04/230.08 inference(scs_inference,[],[1931,36,54,49,48])).
% 230.04/230.08 cnf(2358,plain,
% 230.04/230.08 (P5(a5,a9)),
% 230.04/230.08 inference(scs_inference,[],[41,54])).
% 230.04/230.08 cnf(2440,plain,
% 230.04/230.08 (E(f2(a1,a12),a14)+~P5(f2(a1,a12),a14)),
% 230.04/230.08 inference(scs_inference,[],[1460,57])).
% 230.04/230.08 cnf(2571,plain,
% 230.04/230.08 (~E(a3,f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[34,1907,12])).
% 230.04/230.08 cnf(2572,plain,
% 230.04/230.08 (~P2(f2(a1,a15),a3)),
% 230.04/230.08 inference(scs_inference,[],[34,1907,12,61])).
% 230.04/230.08 cnf(2609,plain,
% 230.04/230.08 (~P11(x26091,a18)+~E(x26091,a4)),
% 230.04/230.08 inference(scs_inference,[],[353,1934,535,26])).
% 230.04/230.08 cnf(2697,plain,
% 230.04/230.08 (~P11(x26971,a18)+~E(x26971,a9)),
% 230.04/230.08 inference(scs_inference,[],[342,26])).
% 230.04/230.08 cnf(2723,plain,
% 230.04/230.08 (~P2(a18,x27231)+~E(x27231,a4)),
% 230.04/230.08 inference(scs_inference,[],[340,13])).
% 230.04/230.08 cnf(2754,plain,
% 230.04/230.08 (~E(f2(a1,a15),f2(a1,a16))),
% 230.04/230.08 inference(scs_inference,[],[42,1911,22])).
% 230.04/230.08 cnf(2764,plain,
% 230.04/230.08 (~E(f2(a1,a16),f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2754,2])).
% 230.04/230.08 cnf(2818,plain,
% 230.04/230.08 (~P5(f2(a1,a15),f2(a1,a16))+P2(f2(a1,a15),f2(a1,a16))),
% 230.04/230.08 inference(scs_inference,[],[2754,57])).
% 230.04/230.08 cnf(2899,plain,
% 230.04/230.08 (~P10(a3,f2(a1,a15))+P11(a3,f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2571,56])).
% 230.04/230.08 cnf(2920,plain,
% 230.04/230.08 (P2(f2(a1,a15),f2(a1,a16))+~P10(f2(a1,a16),f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2764,185,56,27,55])).
% 230.04/230.08 cnf(3141,plain,
% 230.04/230.08 (~P10(f2(a1,a16),f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[44,1907,61,2818,2920])).
% 230.04/230.08 cnf(3342,plain,
% 230.04/230.08 (~P2(a18,x33421)+~E(x33421,a9)),
% 230.04/230.08 inference(scs_inference,[],[329,13])).
% 230.04/230.08 cnf(3539,plain,
% 230.04/230.08 (~P11(a5,x35391)+~E(x35391,a4)),
% 230.04/230.08 inference(scs_inference,[],[300,27])).
% 230.04/230.08 cnf(3651,plain,
% 230.04/230.08 (~P11(a5,x36511)+~E(x36511,a9)),
% 230.04/230.08 inference(scs_inference,[],[317,27])).
% 230.04/230.08 cnf(3653,plain,
% 230.04/230.08 (~P6(a1,x36531)),
% 230.04/230.08 inference(rename_variables,[],[89])).
% 230.04/230.08 cnf(3669,plain,
% 230.04/230.08 (~P11(a5,f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[317,89,3653,30,91,27,64,66,2261,1488,1495,1556,1584,1616,1659,2440,2609,236,577,3539])).
% 230.04/230.08 cnf(3691,plain,
% 230.04/230.08 (~E(x36911,a18)+~E(a9,x36911)),
% 230.04/230.08 inference(scs_inference,[],[321,3])).
% 230.04/230.08 cnf(3695,plain,
% 230.04/230.08 (~E(f6(a1,a12),a9)+~E(f6(a1,a12),a18)),
% 230.04/230.08 inference(scs_inference,[],[321,3,1884,1661,2723,2])).
% 230.04/230.08 cnf(3928,plain,
% 230.04/230.08 (~P7(a1,a16)+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66])).
% 230.04/230.08 cnf(3931,plain,
% 230.04/230.08 (E(a8,f6(a1,a16))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560])).
% 230.04/230.08 cnf(3932,plain,
% 230.04/230.08 (P5(f6(a1,a16),a8)+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629])).
% 230.04/230.08 cnf(3933,plain,
% 230.04/230.08 (P10(a18,f6(a1,a16))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745])).
% 230.04/230.08 cnf(3935,plain,
% 230.04/230.08 (E(f2(x39351,a8),f2(x39351,f6(a1,a16)))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5])).
% 230.04/230.08 cnf(3936,plain,
% 230.04/230.08 (P5(a8,f6(a1,a16))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49])).
% 230.04/230.08 cnf(3938,plain,
% 230.04/230.08 (E(f2(a8,x39381),f2(f6(a1,a16),x39381))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49,4])).
% 230.04/230.08 cnf(3939,plain,
% 230.04/230.08 (E(f11(a8),f11(f6(a1,a16)))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49,4,8])).
% 230.04/230.08 cnf(3940,plain,
% 230.04/230.08 (E(f10(a8),f10(f6(a1,a16)))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49,4,8,9])).
% 230.04/230.08 cnf(3941,plain,
% 230.04/230.08 (E(f6(x39411,a8),f6(x39411,f6(a1,a16)))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49,4,8,9,7])).
% 230.04/230.08 cnf(3942,plain,
% 230.04/230.08 (P10(a8,f6(a1,a16))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49,4,8,9,7,48])).
% 230.04/230.08 cnf(3944,plain,
% 230.04/230.08 (E(f6(a8,x39441),f6(f6(a1,a16),x39441))+E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[89,93,30,66,1560,1629,1745,5,49,4,8,9,7,48,6])).
% 230.04/230.08 cnf(4198,plain,
% 230.04/230.08 (~E(x41981,a9)+~E(a18,x41981)),
% 230.04/230.08 inference(scs_inference,[],[248,3])).
% 230.04/230.08 cnf(4395,plain,
% 230.04/230.08 (~E(x43951,a4)+~E(a9,x43951)),
% 230.04/230.08 inference(scs_inference,[],[289,1090,13,3])).
% 230.04/230.08 cnf(4408,plain,
% 230.04/230.08 (E(f6(x44081,f2(f2(f2(a1,a12),f2(a1,a12)),x44082)),f6(x44081,f2(f2(a13,a13),x44082)))),
% 230.04/230.08 inference(scs_inference,[],[1536,5,49,4,8,9,7])).
% 230.04/230.08 cnf(4411,plain,
% 230.04/230.08 (E(f6(f2(f2(f2(a1,a12),f2(a1,a12)),x44111),x44112),f6(f2(f2(a13,a13),x44111),x44112))),
% 230.04/230.08 inference(scs_inference,[],[1536,5,49,4,8,9,7,48,6])).
% 230.04/230.08 cnf(4445,plain,
% 230.04/230.08 (E(f2(f2(a1,a12),x44451),f2(a13,x44451))),
% 230.04/230.08 inference(rename_variables,[],[880])).
% 230.04/230.08 cnf(4446,plain,
% 230.04/230.08 (~P9(a1,a12)),
% 230.04/230.08 inference(scs_inference,[],[31,880,1907,3669,1953,2052,3141,53,52,55,28,73])).
% 230.04/230.08 cnf(4449,plain,
% 230.04/230.08 (P2(f6(a1,a17),a4)),
% 230.04/230.08 inference(scs_inference,[],[1934,31,880,1907,3669,37,1953,2052,3141,1996,53,52,55,28,73,26,12])).
% 230.04/230.08 cnf(4452,plain,
% 230.04/230.08 (E(f6(a13,x44521),f6(f2(a1,a12),x44521))),
% 230.04/230.08 inference(rename_variables,[],[1033])).
% 230.04/230.08 cnf(4468,plain,
% 230.04/230.08 (E(f6(a1,a12),a9)),
% 230.04/230.08 inference(scs_inference,[],[30,32,1934,31,1033,4452,880,4445,1090,1932,1907,3669,39,37,2572,1909,1964,2000,1953,1992,2052,3141,1996,53,52,55,28,73,26,12,23,3,13,22,29,79,82,2,1948])).
% 230.04/230.08 cnf(4469,plain,
% 230.04/230.08 (~E(f6(a1,a12),a18)),
% 230.04/230.08 inference(scs_inference,[],[30,32,1934,31,1033,4452,880,4445,1090,1932,1907,3669,39,37,2572,1909,1964,2000,1953,1992,2052,3141,1996,53,52,55,28,73,26,12,23,3,13,22,29,79,82,2,1948,3695])).
% 230.04/230.08 cnf(4471,plain,
% 230.04/230.08 (P7(a1,a15)),
% 230.04/230.08 inference(scs_inference,[],[30,32,91,1934,31,1033,4452,880,4445,1090,1932,1907,3669,39,37,2572,1909,1964,2000,1953,1992,2052,3141,1996,53,52,55,28,73,26,12,23,3,13,22,29,79,82,2,1948,3695,19,76])).
% 230.04/230.08 cnf(4474,plain,
% 230.04/230.08 (~P11(f6(a1,a12),a18)),
% 230.04/230.08 inference(scs_inference,[],[30,32,91,1934,31,1033,4452,880,4445,1090,1932,1907,3669,39,37,2572,1909,1964,2000,1953,1992,2052,3141,1996,53,52,55,28,73,26,12,23,3,13,22,29,79,82,2,1948,3695,19,76,3342,2697])).
% 230.04/230.08 cnf(4476,plain,
% 230.04/230.08 (~P3(a1,a15,a15)),
% 230.04/230.08 inference(scs_inference,[],[30,32,91,1934,31,1033,4452,880,4445,1090,1932,1907,3669,39,37,2572,1909,1964,2000,1953,1992,2182,2052,3141,1996,53,52,55,28,73,26,12,23,3,13,22,29,79,82,2,1948,3695,19,76,3342,2697,27,80])).
% 230.04/230.08 cnf(4482,plain,
% 230.04/230.08 (E(a9,f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[4471,1564])).
% 230.04/230.08 cnf(4487,plain,
% 230.04/230.08 (E(f6(a1,a15),a9)),
% 230.04/230.08 inference(scs_inference,[],[4471,1896])).
% 230.04/230.08 cnf(4488,plain,
% 230.04/230.08 (E(f2(f6(a1,a12),x44881),f2(a9,x44881))),
% 230.04/230.08 inference(scs_inference,[],[4446,2343])).
% 230.04/230.08 cnf(4489,plain,
% 230.04/230.08 (~P11(f2(a1,a17),f2(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2146,55])).
% 230.04/230.08 cnf(4518,plain,
% 230.04/230.08 (~P2(a18,f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2572,4487,55,3342])).
% 230.04/230.08 cnf(4536,plain,
% 230.04/230.08 (E(f2(x45361,a13),f2(x45361,f2(a1,a12)))),
% 230.04/230.08 inference(rename_variables,[],[901])).
% 230.04/230.08 cnf(4540,plain,
% 230.04/230.08 (P2(f6(a1,a15),f6(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[1934,901,4536,1536,39,2572,2103,1537,2348,4487,4482,2304,55,3342,2,2697,2337,4395,3691,2899,1700,497,465,407,3651,28,26,12,23,3,13])).
% 230.04/230.08 cnf(4543,plain,
% 230.04/230.08 (~P2(a8,f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[1934,901,4536,1536,39,2572,2142,2358,2103,1537,2348,4487,4482,2304,55,3342,2,2697,2337,4395,3691,2899,1700,497,465,407,3651,28,26,12,23,3,13,22,29,60])).
% 230.04/230.08 cnf(4550,plain,
% 230.04/230.08 (~P2(f6(a1,a17),f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[4540,60])).
% 230.04/230.08 cnf(4556,plain,
% 230.04/230.08 (P2(f6(a1,a15),a4)),
% 230.04/230.08 inference(scs_inference,[],[1934,4482,38,4488,4540,4543,2328,60,55,2,28,12])).
% 230.04/230.08 cnf(4569,plain,
% 230.04/230.08 (~P2(a4,f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[4556,60])).
% 230.04/230.08 cnf(4591,plain,
% 230.04/230.08 (~P11(f6(a1,a15),a4)),
% 230.04/230.08 inference(scs_inference,[],[4569,55])).
% 230.04/230.08 cnf(4717,plain,
% 230.04/230.08 (E(f6(f2(f2(f2(a1,a12),f2(a1,a12)),x47171),a13),f6(f2(f2(a13,a13),x47171),f2(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[1090,4408,4411,2,3])).
% 230.04/230.08 cnf(4725,plain,
% 230.04/230.08 (E(f6(f2(f2(a13,a13),x47251),x47252),f6(f2(f2(f2(a1,a12),f2(a1,a12)),x47251),x47252))),
% 230.04/230.08 inference(scs_inference,[],[4411,2])).
% 230.04/230.08 cnf(4780,plain,
% 230.04/230.08 (E(f6(f2(f2(a13,a13),x47801),a13),f6(f2(f2(f2(a1,a12),f2(a1,a12)),x47801),f2(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[1090,4717,4725,2,3])).
% 230.04/230.08 cnf(4832,plain,
% 230.04/230.08 (E(f2(f6(a13,f2(a1,a12)),a13),f2(f6(f2(a1,a12),a13),f2(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[901,4780,1542,2,3])).
% 230.04/230.08 cnf(4849,plain,
% 230.04/230.08 (E(f2(x48491,f6(a13,f2(a1,a12))),f2(x48491,f6(f2(a1,a12),a13)))),
% 230.04/230.08 inference(scs_inference,[],[1543,2])).
% 230.04/230.08 cnf(4859,plain,
% 230.04/230.08 (E(f2(f2(a1,a12),f6(a13,f2(a1,a12))),f2(a13,f6(f2(a1,a12),a13)))),
% 230.04/230.08 inference(scs_inference,[],[880,4832,4849,2,3])).
% 230.04/230.08 cnf(4876,plain,
% 230.04/230.08 (E(f6(f6(f2(a1,a12),f2(a1,a12)),x48761),f6(f6(a13,a13),x48761))),
% 230.04/230.08 inference(scs_inference,[],[1544,2])).
% 230.04/230.08 cnf(4884,plain,
% 230.04/230.08 (E(f6(f6(f2(a1,a12),f2(a1,a12)),a13),f6(f6(a13,a13),f2(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[1090,1539,4876,2,3])).
% 230.04/230.08 cnf(4902,plain,
% 230.04/230.08 (~E(a4,f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[261,4884,4468,2,3])).
% 230.04/230.08 cnf(4907,plain,
% 230.04/230.08 (E(f11(f6(a1,a12)),f11(a9))),
% 230.04/230.08 inference(scs_inference,[],[4902,1558])).
% 230.04/230.08 cnf(4908,plain,
% 230.04/230.08 (E(a9,f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[4468,2])).
% 230.04/230.08 cnf(4910,plain,
% 230.04/230.08 (~E(f6(a1,a12),a4)),
% 230.04/230.08 inference(scs_inference,[],[4468,2,407,4395])).
% 230.04/230.08 cnf(4911,plain,
% 230.04/230.08 (P2(f6(a1,a12),a18)),
% 230.04/230.08 inference(scs_inference,[],[4468,2,407,4395,465])).
% 230.04/230.08 cnf(4914,plain,
% 230.04/230.08 (P2(a5,f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[4468,2,407,4395,465,1700,497])).
% 230.04/230.08 cnf(4915,plain,
% 230.04/230.08 (E(f6(a1,a15),f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[4487,4468,2,407,4395,465,1700,497,3])).
% 230.04/230.08 cnf(4920,plain,
% 230.04/230.08 (~P11(f6(a1,a16),f6(a1,a17))+~P11(f6(a1,a17),f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[4915,83])).
% 230.04/230.08 cnf(4922,plain,
% 230.04/230.08 (E(f6(a1,a12),f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[4915,2])).
% 230.04/230.08 cnf(4923,plain,
% 230.04/230.08 (E(x49231,f11(a9))+~E(x49231,f11(f6(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[4915,4907,2,3])).
% 230.04/230.08 cnf(4940,plain,
% 230.04/230.08 (~P11(f6(a1,a16),f6(a1,a17))+~P11(f6(a1,a17),f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[4922,818])).
% 230.04/230.08 cnf(4941,plain,
% 230.04/230.08 (E(f11(a9),f11(f6(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[4907,2])).
% 230.04/230.08 cnf(5084,plain,
% 230.04/230.08 (~E(a18,f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[2127,4550,4859,2,13])).
% 230.04/230.08 cnf(5526,plain,
% 230.04/230.08 (E(f2(x55261,f6(a1,a12)),f2(x55261,f6(a1,a15)))),
% 230.04/230.08 inference(scs_inference,[],[30,4922,4471,1909,4911,54,75,5])).
% 230.04/230.08 cnf(5529,plain,
% 230.04/230.08 (E(f10(f6(a1,a12)),f10(f6(a1,a15)))),
% 230.04/230.08 inference(scs_inference,[],[30,4941,4922,4471,1909,4911,54,75,5,49,9])).
% 230.04/230.08 cnf(5547,plain,
% 230.04/230.08 (~P2(a8,f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[30,4469,5084,4941,4922,4474,4550,4518,4471,1909,2208,4911,4914,4487,4468,1934,54,75,5,49,9,8,48,7,76,6,53,57,4198,56,13,4,29,12])).
% 230.04/230.08 cnf(5549,plain,
% 230.04/230.08 (~P11(f6(a1,a12),a4)),
% 230.04/230.08 inference(scs_inference,[],[30,4469,5084,4941,4922,4591,4474,4550,4518,4471,1909,2208,2005,4911,4914,4487,4468,1934,54,75,5,49,9,8,48,7,76,6,53,57,4198,56,13,4,29,12,22,26])).
% 230.04/230.08 cnf(5553,plain,
% 230.04/230.08 (P2(f6(a1,a12),a4)),
% 230.04/230.08 inference(scs_inference,[],[30,4469,5084,4941,4922,4910,4591,4489,4474,4550,4518,4471,1909,2208,2005,4911,4914,4487,4468,1934,54,75,5,49,9,8,48,7,76,6,53,57,4198,56,13,4,29,12,22,26,27,52,50])).
% 230.04/230.08 cnf(5555,plain,
% 230.04/230.08 (~P2(a4,f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[30,4469,5084,4941,4922,4910,4591,4489,4474,4550,4518,4471,1909,2208,2005,4911,4914,4487,4468,1934,54,75,5,49,9,8,48,7,76,6,53,57,4198,56,13,4,29,12,22,26,27,52,50,60])).
% 230.04/230.08 cnf(5566,plain,
% 230.04/230.08 (P5(f2(x55661,f6(a1,a12)),f2(x55661,f6(a1,a15)))),
% 230.04/230.08 inference(scs_inference,[],[5526,5553,54,49])).
% 230.04/230.08 cnf(5568,plain,
% 230.04/230.08 (P10(f2(x55681,f6(a1,a12)),f2(x55681,f6(a1,a15)))),
% 230.04/230.08 inference(scs_inference,[],[5526,5553,54,49,48])).
% 230.04/230.08 cnf(5570,plain,
% 230.04/230.08 (E(f2(x55701,f6(a1,a15)),f2(x55701,f6(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[5526,5553,4915,54,49,48,5])).
% 230.04/230.08 cnf(5571,plain,
% 230.04/230.08 (E(f10(f6(a1,a15)),f10(f6(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[5526,5553,4915,54,49,48,5,9])).
% 230.04/230.08 cnf(5572,plain,
% 230.04/230.08 (E(f6(f6(a1,a15),x55721),f6(f6(a1,a12),x55721))),
% 230.04/230.08 inference(scs_inference,[],[5526,5553,4915,54,49,48,5,9,6])).
% 230.04/230.08 cnf(5576,plain,
% 230.04/230.08 (E(f6(x55761,f6(a1,a15)),f6(x55761,f6(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[5526,5553,4915,54,49,48,5,9,6,8,53,7])).
% 230.04/230.08 cnf(5581,plain,
% 230.04/230.08 (E(f2(f6(a1,a15),x55811),f2(f6(a1,a12),x55811))),
% 230.04/230.08 inference(scs_inference,[],[5526,5549,5553,5555,4902,4910,4915,54,49,48,5,9,6,8,53,7,57,56,4])).
% 230.04/230.08 cnf(5586,plain,
% 230.04/230.08 (E(f11(f6(a1,a15)),f11(a9))),
% 230.04/230.08 inference(scs_inference,[],[85,84,5526,5529,5549,5553,5555,4902,4910,4915,54,49,48,5,9,6,8,53,7,57,56,4,29,22,4923])).
% 230.04/230.08 cnf(5606,plain,
% 230.04/230.08 (E(f2(x56061,f6(a1,a15)),f2(x56061,a9))),
% 230.04/230.08 inference(scs_inference,[],[5570,5571,4914,4487,54,48,49,5])).
% 230.04/230.08 cnf(5607,plain,
% 230.04/230.08 (E(f10(f6(a1,a15)),f10(a9))),
% 230.04/230.08 inference(scs_inference,[],[5570,5571,4914,4487,54,48,49,5,9])).
% 230.04/230.08 cnf(5609,plain,
% 230.04/230.08 (E(f11(a9),f11(f6(a1,a15)))),
% 230.04/230.08 inference(scs_inference,[],[5570,5571,4914,4487,4482,54,48,49,5,9,6,8])).
% 230.04/230.08 cnf(5627,plain,
% 230.04/230.08 (E(f10(f6(a1,a12)),f10(a9))),
% 230.04/230.08 inference(scs_inference,[],[5572,4468,49,48,9])).
% 230.04/230.08 cnf(5629,plain,
% 230.04/230.08 (P11(f6(a1,a17),f6(a1,a15))),
% 230.04/230.08 inference(scs_inference,[],[5572,4540,4468,49,48,9,5,53])).
% 230.04/230.08 cnf(5632,plain,
% 230.04/230.08 (E(f6(x56321,f6(a1,a12)),f6(x56321,a9))),
% 230.04/230.08 inference(scs_inference,[],[5572,4540,4468,49,48,9,5,53,6,7])).
% 230.04/230.08 cnf(5643,plain,
% 230.04/230.08 (~P11(f6(a1,a16),f6(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[5629,4920])).
% 230.04/230.08 cnf(5644,plain,
% 230.04/230.08 (~P11(f6(a1,a16),f6(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[5629,4940])).
% 230.04/230.08 cnf(5649,plain,
% 230.04/230.08 (E(f2(x56491,a9),f2(x56491,f6(a1,a12)))),
% 230.04/230.08 inference(scs_inference,[],[5576,4908,48,49,5])).
% 230.04/230.08 cnf(5651,plain,
% 230.04/230.08 (P11(a4,f6(a1,a17))),
% 230.04/230.08 inference(scs_inference,[],[5576,4449,4908,48,49,5,9,53])).
% 230.04/230.08 cnf(5653,plain,
% 230.04/230.08 (E(f6(a9,x56531),f6(f6(a1,a12),x56531))),
% 230.04/230.08 inference(scs_inference,[],[5576,4449,4908,48,49,5,9,53,6])).
% 230.04/230.08 cnf(5667,plain,
% 230.04/230.08 (~P11(f6(a1,a16),a8)),
% 230.04/230.08 inference(scs_inference,[],[5649,5643,1934,49,48,27])).
% 230.04/230.08 cnf(5668,plain,
% 230.04/230.08 (E(f10(a9),f10(f6(a1,a15)))),
% 230.04/230.08 inference(scs_inference,[],[5649,5643,4482,1934,49,48,27,9])).
% 230.04/230.08 cnf(5670,plain,
% 230.04/230.08 (E(f6(a9,x56701),f6(f6(a1,a15),x56701))),
% 230.04/230.08 inference(scs_inference,[],[5649,5643,4482,1934,49,48,27,9,5,6])).
% 230.04/230.08 cnf(5675,plain,
% 230.04/230.08 (E(f2(x56751,a9),f2(x56751,f6(a1,a12)))),
% 230.04/230.08 inference(rename_variables,[],[5649])).
% 230.04/230.08 cnf(5679,plain,
% 230.04/230.08 (~E(a4,f6(a1,a16))),
% 230.04/230.08 inference(scs_inference,[],[85,84,5651,5649,5675,5653,5643,5581,4482,1934,49,48,27,9,5,6,7,23,3,28,26])).
% 230.04/230.08 cnf(5715,plain,
% 230.04/230.08 (~E(f6(a1,a16),a4)),
% 230.04/230.08 inference(scs_inference,[],[5668,5679,49,48,2])).
% 230.04/230.08 cnf(5716,plain,
% 230.04/230.08 (E(f11(a8),f11(f6(a1,a16)))),
% 230.04/230.08 inference(scs_inference,[],[5668,5679,49,48,2,3939])).
% 230.04/230.08 cnf(5717,plain,
% 230.04/230.08 (E(f10(a8),f10(f6(a1,a16)))),
% 230.04/230.08 inference(scs_inference,[],[5668,5679,49,48,2,3939,3940])).
% 230.04/230.08 cnf(5719,plain,
% 230.04/230.08 (~P7(a1,a16)),
% 230.04/230.08 inference(scs_inference,[],[5668,5679,49,48,2,3939,3940,3942,3928])).
% 230.04/230.08 cnf(5723,plain,
% 230.04/230.08 (E(a8,f6(a1,a16))),
% 230.04/230.08 inference(scs_inference,[],[5668,5679,49,48,2,3939,3940,3942,3928,3944,3932,3933,3931])).
% 230.04/230.08 cnf(5725,plain,
% 230.04/230.08 (E(f6(a1,a16),a8)),
% 230.04/230.08 inference(scs_inference,[],[5668,5679,49,48,2,3939,3940,3942,3928,3944,3932,3933,3931,3938,1887])).
% 230.04/230.08 cnf(5730,plain,
% 230.04/230.08 (P3(a1,a15,a16)),
% 230.04/230.08 inference(scs_inference,[],[30,5668,5679,4471,49,48,2,3939,3940,3942,3928,3944,3932,3933,3931,3938,1887,3941,3936,3935,21,76])).
% 230.04/230.08 cnf(5732,plain,
% 230.04/230.08 (E(f11(f6(a1,a16)),f11(a8))),
% 230.04/230.08 inference(scs_inference,[],[30,5668,5679,4471,49,48,2,3939,3940,3942,3928,3944,3932,3933,3931,3938,1887,3941,3936,3935,21,76,8])).
% 230.04/230.08 cnf(5734,plain,
% 230.04/230.08 (E(f6(f6(a1,a16),x57341),f6(a8,x57341))),
% 230.04/230.08 inference(scs_inference,[],[30,5668,5679,4471,49,48,2,3939,3940,3942,3928,3944,3932,3933,3931,3938,1887,3941,3936,3935,21,76,8,9,6])).
% 230.04/230.08 cnf(5736,plain,
% 230.04/230.08 (E(f6(x57361,f6(a1,a16)),f6(x57361,a8))),
% 230.04/230.08 inference(scs_inference,[],[30,5668,5679,4471,49,48,2,3939,3940,3942,3928,3944,3932,3933,3931,3938,1887,3941,3936,3935,21,76,8,9,6,5,7])).
% 230.04/230.08 cnf(5753,plain,
% 230.04/230.08 (P3(a1,a12,a16)),
% 230.04/230.08 inference(scs_inference,[],[30,5719,4471,91,75,76])).
% 230.04/230.08 cnf(5761,plain,
% 230.04/230.08 (~P2(a4,f6(a1,a16))),
% 230.04/230.08 inference(scs_inference,[],[30,5719,5725,5734,5667,268,4471,91,1974,75,76,48,49,27,23,13])).
% 230.04/230.08 cnf(5763,plain,
% 230.04/230.08 (~P2(f6(a1,a16),f6(a1,a12))),
% 230.04/230.08 inference(scs_inference,[],[30,5719,5725,5734,5667,5547,268,4471,2057,91,1974,75,76,48,49,27,23,13,29,12])).
% 230.04/230.09 cnf(5766,plain,
% 230.04/230.09 (~P5(f6(a1,a16),a5)),
% 230.04/230.09 inference(scs_inference,[],[30,5719,5725,5734,5715,5667,5547,268,4471,2057,2067,91,2157,1974,75,76,48,49,27,23,13,29,12,3,22,28])).
% 230.04/230.09 cnf(5767,plain,
% 230.04/230.09 (~P11(a8,a8)),
% 230.04/230.09 inference(scs_inference,[],[30,5719,5725,5734,5715,5723,5667,5547,268,4471,2057,2067,91,2157,1974,75,76,48,49,27,23,13,29,12,3,22,28,26])).
% 230.04/230.09 cnf(5772,plain,
% 230.04/230.09 (~P10(a8,a4)),
% 230.04/230.09 inference(scs_inference,[],[30,5719,5725,5734,5715,5723,5730,5679,5667,5547,268,286,4471,2057,2067,91,2157,1974,75,76,48,49,27,23,13,29,12,3,22,28,26,82,57,56])).
% 230.04/230.09 cnf(5785,plain,
% 230.04/230.09 (P2(f2(a1,a16),a3)),
% 230.04/230.09 inference(scs_inference,[],[30,32,5753,82])).
% 230.04/230.09 cnf(5799,plain,
% 230.04/230.09 (P11(a3,f2(a1,a16))),
% 230.04/230.09 inference(scs_inference,[],[30,36,32,5716,5761,5753,5679,5719,91,82,54,75,61,48,49,50,53])).
% 230.04/230.09 cnf(5801,plain,
% 230.04/230.09 (~P2(a3,f2(a1,a16))),
% 230.04/230.09 inference(scs_inference,[],[30,36,32,5716,5761,5753,5679,5719,91,82,54,75,61,48,49,50,53,60])).
% 230.04/230.09 cnf(5808,plain,
% 230.04/230.09 (P5(x58081,x58081)),
% 230.04/230.09 inference(rename_variables,[],[85])).
% 230.04/230.09 cnf(5815,plain,
% 230.04/230.09 (~P11(f6(a1,a17),a8)),
% 230.04/230.09 inference(scs_inference,[],[30,85,5808,84,36,32,5772,5763,5716,5732,5767,5761,5766,5753,5679,5723,5725,5719,241,4915,346,1924,91,82,54,75,61,48,49,50,53,60,27,23,13,29,12,3,2,22,28,26])).
% 230.04/230.09 cnf(5818,plain,
% 230.04/230.09 (P2(f6(a1,a16),a4)),
% 230.04/230.09 inference(scs_inference,[],[30,85,5808,84,36,32,5772,5763,5716,5732,5767,5761,5766,5753,5679,5723,5725,5719,241,4915,346,1924,91,82,54,75,61,48,49,50,53,60,27,23,13,29,12,3,2,22,28,26,52,55])).
% 230.04/230.09 cnf(5843,plain,
% 230.04/230.09 (~P11(f6(a1,a17),f6(a1,a16))),
% 230.04/230.09 inference(scs_inference,[],[5815,5799,5818,5717,5725,52,54,48,49,27])).
% 230.04/230.09 cnf(6017,plain,
% 230.04/230.09 (E(f6(f6(a1,a16),f6(a1,a16)),f6(a8,a8))),
% 230.04/230.09 inference(scs_inference,[],[5734,5736,5670,49,48,3])).
% 230.04/230.09 cnf(6107,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+E(f2(x61071,f6(a1,a17)),f2(x61071,f6(a1,a16)))),
% 230.04/230.09 inference(scs_inference,[],[85,6017,5609,5843,48,49,28,50,5])).
% 230.04/230.09 cnf(6108,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+E(f6(x61081,f6(a1,a17)),f6(x61081,f6(a1,a16)))),
% 230.04/230.09 inference(scs_inference,[],[85,6017,5609,5843,48,49,28,50,5,7])).
% 230.04/230.09 cnf(6109,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+E(f2(f6(a1,a17),x61091),f2(f6(a1,a16),x61091))),
% 230.04/230.09 inference(scs_inference,[],[85,6017,5609,5843,48,49,28,50,5,7,4])).
% 230.04/230.09 cnf(6111,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+E(f10(f6(a1,a17)),f10(f6(a1,a16)))),
% 230.04/230.09 inference(scs_inference,[],[85,6017,5609,5843,48,49,28,50,5,7,4,21,9])).
% 230.04/230.09 cnf(6112,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+E(f11(f6(a1,a17)),f11(f6(a1,a16)))),
% 230.04/230.09 inference(scs_inference,[],[85,6017,5609,5843,48,49,28,50,5,7,4,21,9,8])).
% 230.04/230.09 cnf(6113,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+E(f6(f6(a1,a17),x61131),f6(f6(a1,a16),x61131))),
% 230.04/230.09 inference(scs_inference,[],[85,6017,5609,5843,48,49,28,50,5,7,4,21,9,8,6])).
% 230.04/230.09 cnf(6116,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+P10(f10(f6(a1,a15)),f10(a9))),
% 230.04/230.09 inference(scs_inference,[],[85,84,6017,5734,5609,5607,5843,4476,48,49,28,50,5,7,4,21,9,8,6,16,27,23])).
% 230.04/230.09 cnf(6118,plain,
% 230.04/230.09 (P2(f6(a1,a17),f6(a1,a16))+~P2(x61181,f2(a1,a16))+~E(x61181,a3)),
% 230.04/230.09 inference(scs_inference,[],[85,84,6017,5734,5609,5607,5843,5801,4476,48,49,28,50,5,7,4,21,9,8,6,16,27,23,12])).
% 230.04/230.09 cnf(6125,plain,
% 230.04/230.09 (E(f2(f6(a1,a15),f6(a1,a15)),f2(f6(a1,a12),a9))),
% 230.04/230.09 inference(scs_inference,[],[5627,5606,5581,48,49,3])).
% 230.04/230.09 cnf(6216,plain,
% 230.04/230.09 (E(f6(f6(a1,a16),f6(a1,a12)),f6(a8,a9))),
% 230.04/230.09 inference(scs_inference,[],[85,5734,5632,5586,48,49,29,3])).
% 230.04/230.09 cnf(6255,plain,
% 230.04/230.09 (E(f2(a1,a16),a3)),
% 230.04/230.09 inference(scs_inference,[],[5644,43,6216,5719,4915,5843,5801,5629,53,55,2,79,27,50,56])).
% 230.04/230.09 cnf(6258,plain,
% 230.04/230.09 (P5(f2(x62581,f6(a1,a12)),f2(x62581,f6(a1,a15)))),
% 230.04/230.09 inference(rename_variables,[],[5566])).
% 230.04/230.09 cnf(6260,plain,
% 230.04/230.09 (P10(f2(x62601,f6(a1,a12)),f2(x62601,f6(a1,a15)))),
% 230.04/230.09 inference(rename_variables,[],[5568])).
% 230.04/230.09 cnf(6263,plain,
% 230.04/230.09 (E(f2(f6(a1,a15),x62631),f2(f6(a1,a12),x62631))),
% 230.04/230.09 inference(rename_variables,[],[5581])).
% 230.04/230.09 cnf(6266,plain,
% 230.04/230.09 (E(f2(f6(a1,a15),x62661),f2(f6(a1,a12),x62661))),
% 230.04/230.09 inference(rename_variables,[],[5581])).
% 230.04/230.09 cnf(6287,plain,
% 230.04/230.09 (~E(a3,f2(a1,a16))),
% 230.04/230.09 inference(scs_inference,[],[5644,43,5566,6258,5568,6260,6216,6125,5581,6263,6266,5570,5785,5719,4915,5843,5801,5629,53,55,2,79,27,50,56,29,23,28,22,3,6107,6108,6109,6111,6112,6113,6116,4,7,8,9,6,5,1762,6118,13])).
% 230.04/230.09 cnf(6894,plain,
% 230.04/230.09 ($false),
% 230.04/230.09 inference(scs_inference,[],[6255,6287,2]),
% 230.04/230.09 ['proof']).
% 230.04/230.09 % SZS output end Proof
% 230.04/230.09 % Total time :229.482490s
%------------------------------------------------------------------------------