%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG039-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:00:48 EDT 2024
% Result : Unsatisfiable 10.09s 10.18s
% Output : CNFRefutation 10.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : RNG039-1 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 13:52:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 10.09/10.17 %-------------------------------------------
% 10.09/10.17 % File :CSE---1.7
% 10.09/10.17 % Problem :theBenchmark
% 10.09/10.17 % Transform :cnf
% 10.09/10.17 % Format :tptp:raw
% 10.09/10.17 % Command :java -jar mcs_scs.jar %d %s
% 10.09/10.17
% 10.09/10.17 % Result :Theorem 9.570000s
% 10.09/10.17 % Output :CNFRefutation 9.570000s
% 10.09/10.17 %-------------------------------------------
% 10.09/10.18 %--------------------------------------------------------------------------
% 10.09/10.18 % File : RNG039-1 : TPTP v8.2.0. Released v1.0.0.
% 10.09/10.18 % Domain : Ring Theory
% 10.09/10.18 % Problem : Ring property 2
% 10.09/10.18 % Version : [Wos65] axioms.
% 10.09/10.18 % English :
% 10.09/10.18
% 10.09/10.18 % Refs : [Wos65] Wos (1965), Unpublished Note
% 10.09/10.18 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 10.09/10.18 % Source : [SPRFN]
% 10.09/10.18 % Names : Problem 28 [Wos65]
% 10.09/10.18
% 10.09/10.18 % Status : Unsatisfiable
% 10.09/10.18 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.60 v2.0.0
% 10.09/10.18 % Syntax : Number of clauses : 60 ( 49 unt; 0 nHn; 40 RR)
% 10.09/10.18 % Number of literals : 93 ( 8 equ; 34 neg)
% 10.09/10.18 % Maximal clause size : 5 ( 1 avg)
% 10.09/10.18 % Maximal term depth : 2 ( 1 avg)
% 10.09/10.18 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 10.09/10.18 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 10.09/10.18 % Number of variables : 91 ( 1 sgn)
% 10.09/10.18 % SPC : CNF_UNS_RFO_SEQ_HRN
% 10.09/10.18
% 10.09/10.18 % Comments : These are the same axioms as in [MOW76].
% 10.09/10.18 %--------------------------------------------------------------------------
% 10.09/10.18 %----Include ring theory axioms
% 10.09/10.18 include('Axioms/RNG001-0.ax').
% 10.09/10.18 %--------------------------------------------------------------------------
% 10.09/10.18 cnf(absorbtion1,axiom,
% 10.09/10.18 sum(A,add(A,B),B) ).
% 10.09/10.18
% 10.09/10.18 cnf(absorbtion2,axiom,
% 10.09/10.18 sum(add(A,B),B,A) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause32,axiom,
% 10.09/10.18 sum(A,A,additive_identity) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause33,axiom,
% 10.09/10.18 add(A,additive_identity) = A ).
% 10.09/10.18
% 10.09/10.18 cnf(clause34,axiom,
% 10.09/10.18 add(A,A) = additive_identity ).
% 10.09/10.18
% 10.09/10.18 cnf(clause35,axiom,
% 10.09/10.18 multiply(A,A) = A ).
% 10.09/10.18
% 10.09/10.18 cnf(clause36,axiom,
% 10.09/10.18 multiply(a,b) = c ).
% 10.09/10.18
% 10.09/10.18 cnf(clause37,axiom,
% 10.09/10.18 multiply(b,a) = d ).
% 10.09/10.18
% 10.09/10.18 cnf(clause38,axiom,
% 10.09/10.18 sum(A,B,add(B,A)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause39,axiom,
% 10.09/10.18 product(a,c,c) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause40,axiom,
% 10.09/10.18 product(b,d,d) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause41,axiom,
% 10.09/10.18 product(c,b,c) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause42,axiom,
% 10.09/10.18 product(d,a,d) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause43,axiom,
% 10.09/10.18 product(A,multiply(A,B),multiply(A,B)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause44,axiom,
% 10.09/10.18 product(a,multiply(b,A),multiply(B,A)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause45,axiom,
% 10.09/10.18 product(a,b,multiply(c,b)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause46,axiom,
% 10.09/10.18 product(a,multiply(b,c),c) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause47,axiom,
% 10.09/10.18 product(b,multiply(a,A),multiply(d,A)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause48,axiom,
% 10.09/10.18 product(b,a,multiply(d,a)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause49,axiom,
% 10.09/10.18 product(b,multiply(a,d),d) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause50,axiom,
% 10.09/10.18 product(b,c,multiply(d,b)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause51,axiom,
% 10.09/10.18 product(a,d,multiply(c,a)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause52,axiom,
% 10.09/10.18 product(multiply(A,B),B,multiply(A,B)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause53,axiom,
% 10.09/10.18 product(multiply(A,a),b,multiply(A,c)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause54,axiom,
% 10.09/10.18 product(a,b,multiply(a,c)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause55,axiom,
% 10.09/10.18 product(multiply(c,a),b,c) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause56,axiom,
% 10.09/10.18 product(d,b,multiply(b,c)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause57,axiom,
% 10.09/10.18 product(multiply(A,b),a,multiply(A,d)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause58,axiom,
% 10.09/10.18 product(b,a,multiply(b,d)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause59,axiom,
% 10.09/10.18 product(multiply(d,b),a,d) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause60,axiom,
% 10.09/10.18 product(c,a,multiply(a,d)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause63,axiom,
% 10.09/10.18 product(a,add(b,a),add(c,a)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause64,axiom,
% 10.09/10.18 product(a,add(a,b),add(a,c)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause65,axiom,
% 10.09/10.18 product(b,add(a,b),add(d,b)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause66,axiom,
% 10.09/10.18 product(b,add(b,a),add(b,d)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause67,axiom,
% 10.09/10.18 product(add(a,b),b,add(c,b)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause68,axiom,
% 10.09/10.18 product(add(b,a),b,add(b,c)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause69,axiom,
% 10.09/10.18 product(add(b,a),a,add(d,a)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause70,axiom,
% 10.09/10.18 product(add(a,b),a,add(a,d)) ).
% 10.09/10.18
% 10.09/10.18 cnf(clause71,axiom,
% 10.09/10.18 product(A,A,A) ).
% 10.09/10.18
% 10.09/10.18 cnf(a_times_b,negated_conjecture,
% 10.09/10.18 product(a,b,c) ).
% 10.09/10.18
% 10.09/10.18 cnf(b_times_a,negated_conjecture,
% 10.09/10.18 product(b,a,d) ).
% 10.09/10.18
% 10.09/10.18 cnf(prove_c_equals_d,negated_conjecture,
% 10.09/10.18 c != d ).
% 10.09/10.18
% 10.09/10.18 %--------------------------------------------------------------------------
% 10.09/10.18 %-------------------------------------------
% 10.09/10.18 % Proof found
% 10.09/10.18 % SZS status Theorem for theBenchmark
% 10.09/10.18 % SZS output start Proof
% 10.09/10.19 %ClaNum:74(EqnAxiom:14)
% 10.09/10.19 %VarNum:189(SingletonVarNum:91)
% 10.09/10.19 %MaxLitNum:5
% 10.09/10.19 %MaxfuncDepth:1
% 10.09/10.19 %SharedTerms:54
% 10.09/10.19 %goalClause: 20 22 63
% 10.09/10.19 %singleGoalClaCount:3
% 10.09/10.19 [20]P1(a1,a2,a7)
% 10.09/10.19 [21]P1(a1,a7,a7)
% 10.09/10.19 [22]P1(a2,a1,a8)
% 10.09/10.19 [23]P1(a2,a8,a8)
% 10.09/10.19 [24]P1(a7,a2,a7)
% 10.09/10.19 [25]P1(a8,a1,a8)
% 10.09/10.19 [63]~E(a8,a7)
% 10.09/10.19 [15]E(f6(a1,a2),a7)
% 10.09/10.19 [16]E(f6(a2,a1),a8)
% 10.09/10.19 [32]P1(a1,a2,f6(a1,a7))
% 10.09/10.19 [33]P1(a1,a2,f6(a7,a2))
% 10.09/10.19 [34]P1(a1,a8,f6(a7,a1))
% 10.09/10.19 [35]P1(a2,a1,f6(a2,a8))
% 10.09/10.19 [36]P1(a2,a1,f6(a8,a1))
% 10.09/10.19 [37]P1(a2,a7,f6(a8,a2))
% 10.09/10.19 [38]P1(a7,a1,f6(a1,a8))
% 10.09/10.19 [39]P1(a8,a2,f6(a2,a7))
% 10.09/10.19 [40]P1(a1,f6(a2,a7),a7)
% 10.09/10.19 [41]P1(a2,f6(a1,a8),a8)
% 10.09/10.19 [42]P1(f6(a7,a1),a2,a7)
% 10.09/10.19 [43]P1(f6(a8,a2),a1,a8)
% 10.09/10.19 [49]P1(a1,f4(a1,a2),f4(a1,a7))
% 10.09/10.19 [50]P1(a1,f4(a2,a1),f4(a7,a1))
% 10.09/10.19 [51]P1(a2,f4(a1,a2),f4(a8,a2))
% 10.09/10.19 [52]P1(a2,f4(a2,a1),f4(a2,a8))
% 10.09/10.19 [53]P1(f4(a1,a2),a1,f4(a1,a8))
% 10.09/10.19 [54]P1(f4(a1,a2),a2,f4(a7,a2))
% 10.09/10.19 [55]P1(f4(a2,a1),a1,f4(a8,a1))
% 10.09/10.19 [56]P1(f4(a2,a1),a2,f4(a2,a7))
% 10.09/10.19 [26]P2(x261,x261,a3)
% 10.09/10.19 [27]P2(x271,a3,x271)
% 10.09/10.19 [28]P2(a3,x281,x281)
% 10.09/10.19 [29]P1(x291,x291,x291)
% 10.09/10.19 [17]E(f4(x171,a3),x171)
% 10.09/10.19 [18]E(f4(x181,x181),a3)
% 10.09/10.19 [19]E(f6(x191,x191),x191)
% 10.09/10.19 [30]P2(x301,f5(x301),a3)
% 10.09/10.19 [31]P2(f5(x311),x311,a3)
% 10.09/10.19 [57]P1(a2,f6(a1,x571),f6(a8,x571))
% 10.09/10.19 [58]P1(f6(x581,a1),a2,f6(x581,a7))
% 10.09/10.19 [59]P1(f6(x591,a2),a1,f6(x591,a8))
% 10.09/10.19 [44]P2(x441,x442,f4(x442,x441))
% 10.09/10.19 [45]P2(x451,x452,f4(x451,x452))
% 10.09/10.19 [46]P1(x461,x462,f6(x461,x462))
% 10.09/10.19 [47]P2(x471,f4(x471,x472),x472)
% 10.09/10.19 [48]P2(f4(x481,x482),x482,x481)
% 10.09/10.19 [60]P1(a1,f6(a2,x601),f6(x602,x601))
% 10.09/10.19 [61]P1(x611,f6(x611,x612),f6(x611,x612))
% 10.09/10.19 [62]P1(f6(x621,x622),x622,f6(x621,x622))
% 10.09/10.19 [64]~P2(x642,x641,x643)+P2(x641,x642,x643)
% 10.09/10.19 [65]~P2(x653,x654,x651)+E(x651,x652)+~P2(x653,x654,x652)
% 10.09/10.19 [66]~P1(x663,x664,x661)+E(x661,x662)+~P1(x663,x664,x662)
% 10.09/10.19 [67]~P2(x676,x674,x671)+P2(x671,x672,x673)+~P2(x674,x672,x675)+~P2(x676,x675,x673)
% 10.09/10.19 [68]~P2(x681,x686,x684)+P2(x681,x682,x683)+~P2(x684,x685,x683)+~P2(x686,x685,x682)
% 10.09/10.19 [69]~P1(x696,x694,x691)+P1(x691,x692,x693)+~P1(x694,x692,x695)+~P1(x696,x695,x693)
% 10.09/10.19 [70]~P1(x701,x706,x704)+P1(x701,x702,x703)+~P1(x704,x705,x703)+~P1(x706,x705,x702)
% 10.09/10.19 [71]~P1(x717,x715,x712)+~P1(x717,x714,x711)+P2(x711,x712,x713)+~P2(x714,x715,x716)+~P1(x717,x716,x713)
% 10.09/10.19 [72]~P1(x725,x727,x722)+~P1(x724,x727,x721)+P2(x721,x722,x723)+~P2(x724,x725,x726)+~P1(x726,x727,x723)
% 10.09/10.19 [73]~P1(x737,x732,x735)+~P1(x736,x732,x734)+P1(x731,x732,x733)+~P2(x734,x735,x733)+~P2(x736,x737,x731)
% 10.09/10.19 [74]~P1(x741,x747,x745)+~P1(x741,x746,x744)+P1(x741,x742,x743)+~P2(x744,x745,x743)+~P2(x746,x747,x742)
% 10.09/10.19 %EqnAxiom
% 10.09/10.19 [1]E(x11,x11)
% 10.09/10.19 [2]E(x22,x21)+~E(x21,x22)
% 10.09/10.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 10.09/10.19 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 10.09/10.19 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 10.09/10.19 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 10.09/10.19 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 10.09/10.19 [8]~E(x81,x82)+E(f5(x81),f5(x82))
% 10.09/10.19 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 10.09/10.19 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 10.09/10.19 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 10.09/10.19 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 10.09/10.19 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 10.09/10.19 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 10.09/10.19
% 10.09/10.19 %-------------------------------------------
% 10.09/10.19 cnf(75,plain,
% 10.09/10.19 (E(x751,f6(x751,x751))),
% 10.09/10.19 inference(scs_inference,[],[19,2])).
% 10.09/10.19 cnf(76,plain,
% 10.09/10.19 (E(a7,f6(a1,a2))),
% 10.09/10.19 inference(scs_inference,[],[20,46,19,2,66])).
% 10.09/10.19 cnf(77,plain,
% 10.09/10.19 (P1(x771,x772,f6(x771,x772))),
% 10.09/10.19 inference(rename_variables,[],[46])).
% 10.09/10.19 cnf(79,plain,
% 10.09/10.19 (P1(f6(a1,a1),a2,a7)),
% 10.09/10.19 inference(scs_inference,[],[20,46,19,2,66,9])).
% 10.09/10.19 cnf(80,plain,
% 10.09/10.19 (E(a3,f4(x801,x801))),
% 10.09/10.19 inference(scs_inference,[],[20,26,44,46,19,2,66,9,65])).
% 10.09/10.19 cnf(83,plain,
% 10.09/10.19 (E(f4(f6(a1,a1),a3),a1)),
% 10.09/10.19 inference(scs_inference,[],[20,26,44,46,19,17,2,66,9,65,3])).
% 10.09/10.19 cnf(84,plain,
% 10.09/10.19 (E(f6(x841,x841),x841)),
% 10.09/10.19 inference(rename_variables,[],[19])).
% 10.09/10.19 cnf(86,plain,
% 10.09/10.19 (P1(a2,f6(a1,a1),a8)),
% 10.09/10.19 inference(scs_inference,[],[20,22,26,44,46,19,17,2,66,9,65,3,10])).
% 10.09/10.19 cnf(87,plain,
% 10.09/10.19 (P1(f6(x871,x871),f6(x871,x871),x871)),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,26,44,46,19,84,17,2,66,9,65,3,10,11])).
% 10.09/10.19 cnf(88,plain,
% 10.09/10.19 (P1(x881,x881,x881)),
% 10.09/10.19 inference(rename_variables,[],[29])).
% 10.09/10.19 cnf(89,plain,
% 10.09/10.19 (P2(x891,f6(x891,x891),a3)),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,26,44,46,19,84,17,2,66,9,65,3,10,11,12])).
% 10.09/10.19 cnf(90,plain,
% 10.09/10.19 (P2(x901,x901,a3)),
% 10.09/10.19 inference(rename_variables,[],[26])).
% 10.09/10.19 cnf(91,plain,
% 10.09/10.19 (P2(f6(x911,x911),x911,a3)),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,26,90,44,46,19,84,17,2,66,9,65,3,10,11,12,13])).
% 10.09/10.19 cnf(92,plain,
% 10.09/10.19 (P2(x921,x921,a3)),
% 10.09/10.19 inference(rename_variables,[],[26])).
% 10.09/10.19 cnf(93,plain,
% 10.09/10.19 (P2(x931,x931,f4(f6(x932,x932),f6(x932,x932)))),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,26,90,92,44,46,19,84,17,2,66,9,65,3,10,11,12,13,14])).
% 10.09/10.19 cnf(94,plain,
% 10.09/10.19 (P1(f6(x941,x942),f6(a2,x942),f6(x941,x942))),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,88,26,90,92,44,46,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69])).
% 10.09/10.19 cnf(95,plain,
% 10.09/10.19 (P1(x951,x951,x951)),
% 10.09/10.19 inference(rename_variables,[],[29])).
% 10.09/10.19 cnf(97,plain,
% 10.09/10.19 (P1(a1,f6(a2,x971),f6(a7,f6(a2,x971)))),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,88,26,90,92,61,44,46,77,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70])).
% 10.09/10.19 cnf(98,plain,
% 10.09/10.19 (P1(x981,f6(x981,x982),f6(x981,x982))),
% 10.09/10.19 inference(rename_variables,[],[61])).
% 10.09/10.19 cnf(101,plain,
% 10.09/10.19 (P2(a3,f4(x1011,a3),x1011)),
% 10.09/10.19 inference(scs_inference,[],[20,22,29,88,26,90,92,61,44,46,77,48,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70,67])).
% 10.09/10.19 cnf(102,plain,
% 10.09/10.20 (P2(f4(x1021,x1022),x1022,x1021)),
% 10.09/10.20 inference(rename_variables,[],[48])).
% 10.09/10.20 cnf(103,plain,
% 10.09/10.20 (P2(x1031,x1031,a3)),
% 10.09/10.20 inference(rename_variables,[],[26])).
% 10.09/10.20 cnf(104,plain,
% 10.09/10.20 (P2(x1041,x1041,a3)),
% 10.09/10.20 inference(rename_variables,[],[26])).
% 10.09/10.20 cnf(106,plain,
% 10.09/10.20 (P2(f4(x1061,a3),x1061,a3)),
% 10.09/10.20 inference(scs_inference,[],[20,22,29,88,26,90,92,104,103,61,44,46,77,48,102,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70,67,68])).
% 10.09/10.20 cnf(108,plain,
% 10.09/10.20 (P2(x1081,x1081,a3)),
% 10.09/10.20 inference(rename_variables,[],[26])).
% 10.09/10.20 cnf(111,plain,
% 10.09/10.20 (P2(f6(x1111,a3),f6(x1111,a3),f6(x1111,a3))),
% 10.09/10.20 inference(scs_inference,[],[20,22,29,88,95,26,90,92,104,108,103,61,62,44,46,77,48,102,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70,67,68,71])).
% 10.09/10.20 cnf(114,plain,
% 10.09/10.20 (P1(x1141,x1141,x1141)),
% 10.09/10.20 inference(rename_variables,[],[29])).
% 10.09/10.20 cnf(115,plain,
% 10.09/10.20 (P2(x1151,x1151,a3)),
% 10.09/10.20 inference(rename_variables,[],[26])).
% 10.09/10.20 cnf(117,plain,
% 10.09/10.20 (P2(f6(a3,x1171),f6(a3,x1171),f6(a3,x1171))),
% 10.09/10.20 inference(scs_inference,[],[20,22,29,88,95,114,26,90,92,104,108,115,103,61,98,62,44,46,77,48,102,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70,67,68,71,72])).
% 10.09/10.20 cnf(120,plain,
% 10.09/10.20 (P1(x1201,x1201,x1201)),
% 10.09/10.20 inference(rename_variables,[],[29])).
% 10.09/10.20 cnf(121,plain,
% 10.09/10.20 (P2(x1211,x1211,a3)),
% 10.09/10.20 inference(rename_variables,[],[26])).
% 10.09/10.20 cnf(123,plain,
% 10.09/10.20 (P1(a3,x1231,a3)),
% 10.09/10.20 inference(scs_inference,[],[20,22,29,88,95,114,120,26,90,92,104,108,115,121,103,61,98,62,44,46,77,48,102,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70,67,68,71,72,73])).
% 10.09/10.20 cnf(125,plain,
% 10.09/10.20 (P2(x1251,x1251,a3)),
% 10.09/10.20 inference(rename_variables,[],[26])).
% 10.09/10.20 cnf(127,plain,
% 10.09/10.20 (P1(x1271,a3,a3)),
% 10.09/10.20 inference(scs_inference,[],[20,22,29,88,95,114,120,26,90,92,104,108,115,121,125,103,61,98,62,44,46,77,48,102,19,84,17,60,2,66,9,65,3,10,11,12,13,14,69,70,67,68,71,72,73,74])).
% 10.09/10.20 cnf(131,plain,
% 10.09/10.20 (E(a1,f4(f6(a1,a1),a3))),
% 10.09/10.20 inference(scs_inference,[],[83,2])).
% 10.09/10.20 cnf(132,plain,
% 10.09/10.20 (P1(f6(a2,a2),a1,a8)),
% 10.09/10.20 inference(scs_inference,[],[22,75,83,2,9])).
% 10.09/10.20 cnf(133,plain,
% 10.09/10.20 (E(x1331,f6(x1331,x1331))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(134,plain,
% 10.09/10.20 (P2(f6(f6(x1341,a3),f6(x1341,a3)),f6(x1341,a3),f6(x1341,a3))),
% 10.09/10.20 inference(scs_inference,[],[22,111,75,133,83,2,9,12])).
% 10.09/10.20 cnf(135,plain,
% 10.09/10.20 (E(x1351,f6(x1351,x1351))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(137,plain,
% 10.09/10.20 (E(x1371,f6(x1371,x1371))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(138,plain,
% 10.09/10.20 (P2(f6(x1381,a3),f6(f6(x1381,a3),f6(x1381,a3)),f6(x1381,a3))),
% 10.09/10.20 inference(scs_inference,[],[22,111,75,133,135,137,83,2,9,12,11,13])).
% 10.09/10.20 cnf(139,plain,
% 10.09/10.20 (E(x1391,f6(x1391,x1391))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(140,plain,
% 10.09/10.20 (E(f6(x1401,a3),f4(f6(x1402,x1402),f6(x1402,x1402)))),
% 10.09/10.20 inference(scs_inference,[],[22,111,75,133,135,137,93,83,2,9,12,11,13,65])).
% 10.09/10.20 cnf(141,plain,
% 10.09/10.20 (P2(x1411,x1411,f4(f6(x1412,x1412),f6(x1412,x1412)))),
% 10.09/10.20 inference(rename_variables,[],[93])).
% 10.09/10.20 cnf(143,plain,
% 10.09/10.20 (E(a7,f6(f6(a1,a2),f6(a1,a2)))),
% 10.09/10.20 inference(scs_inference,[],[22,111,76,75,133,135,137,139,93,83,2,9,12,11,13,65,3])).
% 10.09/10.20 cnf(144,plain,
% 10.09/10.20 (E(x1441,f6(x1441,x1441))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(145,plain,
% 10.09/10.20 (E(a3,f6(a3,x1451))),
% 10.09/10.20 inference(scs_inference,[],[22,111,76,123,75,133,135,137,139,93,83,61,2,9,12,11,13,65,3,66])).
% 10.09/10.20 cnf(150,plain,
% 10.09/10.20 (E(x1501,f6(x1501,x1501))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(151,plain,
% 10.09/10.20 (P1(a1,f6(a2,a2),a7)),
% 10.09/10.20 inference(scs_inference,[],[20,22,111,76,123,75,133,135,137,139,144,150,93,83,61,2,9,12,11,13,65,3,66,14,10])).
% 10.09/10.20 cnf(153,plain,
% 10.09/10.20 (P1(a1,a3,f6(a7,a3))),
% 10.09/10.20 inference(scs_inference,[],[20,22,111,76,123,127,75,133,135,137,139,144,150,93,83,61,46,2,9,12,11,13,65,3,66,14,10,70])).
% 10.09/10.20 cnf(155,plain,
% 10.09/10.20 (P1(x1551,x1552,f6(x1551,x1552))),
% 10.09/10.20 inference(rename_variables,[],[46])).
% 10.09/10.20 cnf(157,plain,
% 10.09/10.20 (P2(f4(f6(x1571,x1571),f6(x1571,x1571)),f4(x1572,a3),x1572)),
% 10.09/10.20 inference(scs_inference,[],[20,22,111,76,123,127,75,133,135,137,139,144,150,93,141,28,101,83,61,46,2,9,12,11,13,65,3,66,14,10,70,67])).
% 10.09/10.20 cnf(158,plain,
% 10.09/10.20 (P2(x1581,x1581,f4(f6(x1582,x1582),f6(x1582,x1582)))),
% 10.09/10.20 inference(rename_variables,[],[93])).
% 10.09/10.20 cnf(161,plain,
% 10.09/10.20 (P1(f6(a1,a8),a1,f6(a1,a8))),
% 10.09/10.20 inference(scs_inference,[],[20,22,111,76,123,127,75,133,135,137,139,144,150,93,141,28,38,101,83,29,61,46,2,9,12,11,13,65,3,66,14,10,70,67,69])).
% 10.09/10.20 cnf(167,plain,
% 10.09/10.20 (P1(f6(x1671,a3),f6(a2,a3),f4(f6(x1672,x1672),f6(x1672,x1672)))),
% 10.09/10.20 inference(scs_inference,[],[20,22,94,111,76,123,127,75,133,135,137,139,144,150,93,141,158,28,89,38,101,83,29,61,46,2,9,12,11,13,65,3,66,14,10,70,67,69,68,74])).
% 10.09/10.20 cnf(169,plain,
% 10.09/10.20 (P2(f6(x1691,a3),f6(x1691,a3),f6(x1691,a3))),
% 10.09/10.20 inference(rename_variables,[],[111])).
% 10.09/10.20 cnf(170,plain,
% 10.09/10.20 (P1(f6(x1701,x1702),f6(a2,x1702),f6(x1701,x1702))),
% 10.09/10.20 inference(rename_variables,[],[94])).
% 10.09/10.20 cnf(178,plain,
% 10.09/10.20 (P2(a7,a7,a7)+~P2(a2,a2,a2)),
% 10.09/10.20 inference(scs_inference,[],[20,22,94,170,111,169,76,123,127,75,133,135,137,139,144,150,93,141,158,28,89,91,38,101,83,29,61,46,155,2,9,12,11,13,65,3,66,14,10,70,67,69,68,74,73,71])).
% 10.09/10.20 cnf(182,plain,
% 10.09/10.20 (E(f6(a3,x1821),a3)),
% 10.09/10.20 inference(scs_inference,[],[145,2])).
% 10.09/10.20 cnf(183,plain,
% 10.09/10.20 (E(f6(a7,a3),a3)),
% 10.09/10.20 inference(scs_inference,[],[145,153,127,2,66])).
% 10.09/10.20 cnf(187,plain,
% 10.09/10.20 (P2(f6(a3,x1871),f6(a3,x1871),f6(a3,x1871))),
% 10.09/10.20 inference(rename_variables,[],[117])).
% 10.09/10.20 cnf(188,plain,
% 10.09/10.20 (E(f6(x1881,a3),f4(f6(x1882,x1882),f6(x1882,x1882)))),
% 10.09/10.20 inference(rename_variables,[],[140])).
% 10.09/10.20 cnf(189,plain,
% 10.09/10.20 (E(f4(x1891,x1891),f6(a3,x1892))),
% 10.09/10.20 inference(scs_inference,[],[117,145,153,127,140,18,2,66,12,3])).
% 10.09/10.20 cnf(190,plain,
% 10.09/10.20 (P2(f6(a3,a3),f4(f6(x1901,x1901),f6(x1901,x1901)),f6(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[117,187,145,153,127,140,188,18,2,66,12,3,13])).
% 10.09/10.20 cnf(191,plain,
% 10.09/10.20 (P2(f6(a3,x1911),f6(a3,x1911),f6(a3,x1911))),
% 10.09/10.20 inference(rename_variables,[],[117])).
% 10.09/10.20 cnf(194,plain,
% 10.09/10.20 (P2(x1941,x1942,f4(x1941,x1942))),
% 10.09/10.20 inference(rename_variables,[],[45])).
% 10.09/10.20 cnf(196,plain,
% 10.09/10.20 (P1(f6(x1961,a3),f6(a2,a3),a3)),
% 10.09/10.20 inference(scs_inference,[],[167,117,187,191,145,153,127,140,188,45,18,2,66,12,3,13,65,11])).
% 10.09/10.20 cnf(198,plain,
% 10.09/10.20 (P1(f4(f6(a1,a1),a3),a2,a7)),
% 10.09/10.20 inference(scs_inference,[],[20,167,117,187,191,145,153,127,140,188,45,131,18,2,66,12,3,13,65,11,9])).
% 10.09/10.20 cnf(199,plain,
% 10.09/10.20 (P2(f4(f6(x1991,x1991),f6(x1991,x1991)),f4(a3,a3),f6(a3,x1992))),
% 10.09/10.20 inference(scs_inference,[],[20,167,117,187,191,145,153,127,157,140,188,45,131,18,2,66,12,3,13,65,11,9,14])).
% 10.09/10.20 cnf(200,plain,
% 10.09/10.20 (P2(f4(f6(x2001,x2001),f6(x2001,x2001)),f4(x2002,a3),x2002)),
% 10.09/10.20 inference(rename_variables,[],[157])).
% 10.09/10.20 cnf(201,plain,
% 10.09/10.20 (P1(a2,f4(f6(a1,a1),a3),a8)),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,145,153,127,157,140,188,45,131,18,2,66,12,3,13,65,11,9,14,10])).
% 10.09/10.20 cnf(202,plain,
% 10.09/10.20 (P2(f6(a3,x2021),f4(f6(a3,x2021),a3),f6(a3,x2021))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,145,153,127,157,140,188,27,45,47,131,18,2,66,12,3,13,65,11,9,14,10,67])).
% 10.09/10.20 cnf(206,plain,
% 10.09/10.20 (P1(a3,a7,f6(a3,a2))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,127,157,140,188,27,45,47,131,18,46,2,66,12,3,13,65,11,9,14,10,67,70])).
% 10.09/10.20 cnf(207,plain,
% 10.09/10.20 (P1(a3,x2071,a3)),
% 10.09/10.20 inference(rename_variables,[],[123])).
% 10.09/10.20 cnf(208,plain,
% 10.09/10.20 (P1(x2081,x2082,f6(x2081,x2082))),
% 10.09/10.20 inference(rename_variables,[],[46])).
% 10.09/10.20 cnf(210,plain,
% 10.09/10.20 (P1(f6(a7,a3),x2101,f6(a7,a3))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,207,127,157,140,188,27,45,47,131,18,46,2,66,12,3,13,65,11,9,14,10,67,70,69])).
% 10.09/10.20 cnf(212,plain,
% 10.09/10.20 (P2(f4(f6(x2121,x2121),f6(x2121,x2121)),a3,f6(a3,x2122))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,207,127,157,200,140,188,27,45,47,106,131,18,46,2,66,12,3,13,65,11,9,14,10,67,70,69,68])).
% 10.09/10.20 cnf(216,plain,
% 10.09/10.20 (P1(a3,f6(a3,x2161),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,207,127,157,200,140,188,27,45,194,47,106,131,18,46,2,66,12,3,13,65,11,9,14,10,67,70,69,68,74])).
% 10.09/10.20 cnf(217,plain,
% 10.09/10.20 (P2(x2171,x2172,f4(x2171,x2172))),
% 10.09/10.20 inference(rename_variables,[],[45])).
% 10.09/10.20 cnf(219,plain,
% 10.09/10.20 (P1(a3,x2191,a3)),
% 10.09/10.20 inference(rename_variables,[],[123])).
% 10.09/10.20 cnf(221,plain,
% 10.09/10.20 (P2(a7,a7,f6(a1,f4(a2,a2)))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,207,127,157,200,140,188,27,45,194,217,47,106,131,18,46,208,2,66,12,3,13,65,11,9,14,10,67,70,69,68,74,71])).
% 10.09/10.20 cnf(222,plain,
% 10.09/10.20 (P1(x2221,x2222,f6(x2221,x2222))),
% 10.09/10.20 inference(rename_variables,[],[46])).
% 10.09/10.20 cnf(223,plain,
% 10.09/10.20 (P2(x2231,x2232,f4(x2231,x2232))),
% 10.09/10.20 inference(rename_variables,[],[45])).
% 10.09/10.20 cnf(225,plain,
% 10.09/10.20 (P2(a7,a7,f6(f4(a1,a1),a2))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,207,127,157,200,140,188,27,45,194,217,223,47,106,131,18,46,208,222,2,66,12,3,13,65,11,9,14,10,67,70,69,68,74,71,72])).
% 10.09/10.20 cnf(229,plain,
% 10.09/10.20 (P1(f6(a3,x2291),f4(f6(x2292,x2292),f6(x2292,x2292)),f6(a3,x2291))),
% 10.09/10.20 inference(scs_inference,[],[20,22,167,117,187,191,79,145,153,123,207,219,127,157,200,140,188,27,45,194,217,223,47,106,131,18,29,46,208,222,2,66,12,3,13,65,11,9,14,10,67,70,69,68,74,71,72,73])).
% 10.09/10.20 cnf(233,plain,
% 10.09/10.20 (E(a3,f6(a7,a3))),
% 10.09/10.20 inference(scs_inference,[],[183,2])).
% 10.09/10.20 cnf(235,plain,
% 10.09/10.20 (E(f6(a7,a3),f6(f6(a7,a3),x2351))),
% 10.09/10.20 inference(scs_inference,[],[210,183,221,76,61,2,12,66])).
% 10.09/10.20 cnf(236,plain,
% 10.09/10.20 (P1(x2361,f6(x2361,x2362),f6(x2361,x2362))),
% 10.09/10.20 inference(rename_variables,[],[61])).
% 10.09/10.20 cnf(237,plain,
% 10.09/10.20 (P1(f6(a7,a3),x2371,f6(a7,a3))),
% 10.09/10.20 inference(rename_variables,[],[210])).
% 10.09/10.20 cnf(241,plain,
% 10.09/10.20 (E(x2411,f6(x2411,x2411))),
% 10.09/10.20 inference(rename_variables,[],[75])).
% 10.09/10.20 cnf(244,plain,
% 10.09/10.20 (E(f6(a3,x2441),f4(f6(x2442,x2442),f6(x2442,x2442)))),
% 10.09/10.20 inference(scs_inference,[],[161,210,183,221,76,212,75,241,27,61,2,12,66,13,9,11,65])).
% 10.09/10.20 cnf(245,plain,
% 10.09/10.20 (P2(x2451,a3,x2451)),
% 10.09/10.20 inference(rename_variables,[],[27])).
% 10.09/10.20 cnf(247,plain,
% 10.09/10.20 (E(f4(f6(a7,a3),a3),a3)),
% 10.09/10.20 inference(scs_inference,[],[161,210,183,221,76,212,75,241,27,17,61,2,12,66,13,9,11,65,3])).
% 10.09/10.20 cnf(249,plain,
% 10.09/10.20 (P2(x2491,f5(x2491),f6(a3,x2492))),
% 10.09/10.20 inference(scs_inference,[],[161,210,183,221,76,145,212,30,75,241,27,17,61,2,12,66,13,9,11,65,3,14])).
% 10.09/10.20 cnf(253,plain,
% 10.09/10.20 (P1(f6(a7,a3),x2531,f6(a7,a3))),
% 10.09/10.20 inference(rename_variables,[],[210])).
% 10.09/10.20 cnf(256,plain,
% 10.09/10.20 (P2(f6(a3,x2561),f5(a3),f6(a3,x2561))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,183,221,76,145,189,212,30,75,241,27,17,61,46,2,12,66,13,9,11,65,3,14,10,70,67])).
% 10.09/10.20 cnf(259,plain,
% 10.09/10.20 (P1(f4(a3,a3),f4(f6(x2591,x2591),f6(x2591,x2591)),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,216,183,221,76,145,189,212,30,75,241,27,17,61,46,2,12,66,13,9,11,65,3,14,10,70,67,69])).
% 10.09/10.20 cnf(260,plain,
% 10.09/10.20 (P1(a3,f6(a3,x2601),f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[216])).
% 10.09/10.20 cnf(262,plain,
% 10.09/10.20 (P2(f6(a3,a3),f6(a3,x2621),f4(f4(a3,a3),f6(a3,a3)))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,216,183,221,76,145,190,199,189,212,30,75,241,27,44,17,61,46,2,12,66,13,9,11,65,3,14,10,70,67,69,68])).
% 10.09/10.20 cnf(264,plain,
% 10.09/10.20 (P2(x2641,x2642,f4(x2642,x2641))),
% 10.09/10.20 inference(rename_variables,[],[44])).
% 10.09/10.20 cnf(266,plain,
% 10.09/10.20 (P1(a3,f6(a1,f4(a2,a2)),f6(a3,a2))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,216,183,221,206,76,123,145,190,199,189,212,30,75,241,27,245,44,17,61,46,2,12,66,13,9,11,65,3,14,10,70,67,69,68,74])).
% 10.09/10.20 cnf(270,plain,
% 10.09/10.20 (P2(f4(a3,a3),f4(a3,a3),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,216,260,183,221,206,117,76,123,145,190,199,189,212,30,75,241,27,245,44,17,61,46,2,12,66,13,9,11,65,3,14,10,70,67,69,68,74,71])).
% 10.09/10.20 cnf(273,plain,
% 10.09/10.20 (P2(f6(a7,a3),f6(a7,a3),f6(f6(a7,a3),x2731))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,253,216,260,183,221,206,117,76,123,145,111,190,199,189,212,30,75,241,27,245,44,17,61,236,46,2,12,66,13,9,11,65,3,14,10,70,67,69,68,74,71,72])).
% 10.09/10.20 cnf(279,plain,
% 10.09/10.20 (P1(f6(a1,f4(a2,a2)),a3,f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[229,161,210,237,253,216,260,183,221,206,117,76,123,127,145,111,190,199,189,212,30,75,241,27,245,44,264,17,61,236,46,2,12,66,13,9,11,65,3,14,10,70,67,69,68,74,71,72,73])).
% 10.09/10.20 cnf(284,plain,
% 10.09/10.20 (E(f6(f6(a7,a3),x2841),f6(a7,a3))),
% 10.09/10.20 inference(scs_inference,[],[235,2])).
% 10.09/10.20 cnf(285,plain,
% 10.09/10.20 (E(f6(a3,x2851),f5(a3))),
% 10.09/10.20 inference(scs_inference,[],[235,249,28,2,65])).
% 10.09/10.20 cnf(289,plain,
% 10.09/10.20 (P2(f6(a3,x2891),f4(a3,a3),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[270,235,249,189,28,2,65,12])).
% 10.09/10.20 cnf(290,plain,
% 10.09/10.20 (E(f4(x2901,x2901),f6(a3,x2902))),
% 10.09/10.20 inference(rename_variables,[],[189])).
% 10.09/10.20 cnf(292,plain,
% 10.09/10.20 (P1(f6(a3,x2921),f4(f6(x2922,x2922),f6(x2922,x2922)),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[270,259,235,249,233,189,290,28,2,65,12,3,9])).
% 10.09/10.20 cnf(293,plain,
% 10.09/10.20 (E(f4(x2931,x2931),f6(a3,x2932))),
% 10.09/10.20 inference(rename_variables,[],[189])).
% 10.09/10.20 cnf(294,plain,
% 10.09/10.20 (P2(f4(a3,a3),f4(a3,a3),f6(a3,x2941))),
% 10.09/10.20 inference(scs_inference,[],[270,259,235,249,233,189,290,293,28,2,65,12,3,9,14])).
% 10.09/10.20 cnf(295,plain,
% 10.09/10.20 (E(f4(x2951,x2951),f6(a3,x2952))),
% 10.09/10.20 inference(rename_variables,[],[189])).
% 10.09/10.20 cnf(296,plain,
% 10.09/10.20 (P2(f4(a3,a3),f6(a3,x2961),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[270,259,235,249,233,189,290,293,295,28,2,65,12,3,9,14,13])).
% 10.09/10.20 cnf(297,plain,
% 10.09/10.20 (E(f4(x2971,x2971),f6(a3,x2972))),
% 10.09/10.20 inference(rename_variables,[],[189])).
% 10.09/10.20 cnf(299,plain,
% 10.09/10.20 (E(f4(x2991,x2991),f6(a3,x2992))),
% 10.09/10.20 inference(rename_variables,[],[189])).
% 10.09/10.20 cnf(302,plain,
% 10.09/10.20 (P2(f6(a3,x3021),f4(f5(a3),f5(a3)),f6(a3,x3021))),
% 10.09/10.20 inference(scs_inference,[],[270,259,235,249,256,233,189,290,293,295,297,299,28,47,2,65,12,3,9,14,13,11,10,67])).
% 10.09/10.20 cnf(309,plain,
% 10.09/10.20 (P1(f4(a3,a3),x3091,f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[270,259,279,235,198,210,123,249,256,233,189,290,293,295,297,299,28,47,46,2,65,12,3,9,14,13,11,10,67,70,69])).
% 10.09/10.20 cnf(311,plain,
% 10.09/10.20 (P2(f6(a7,a3),f4(f6(x3111,x3111),f6(x3111,x3111)),f6(a7,a3))),
% 10.09/10.20 inference(scs_inference,[],[273,270,259,279,235,198,210,123,134,249,256,233,93,189,290,293,295,297,299,28,47,46,2,65,12,3,9,14,13,11,10,67,70,69,68])).
% 10.09/10.20 cnf(328,plain,
% 10.09/10.20 (E(f5(a3),f6(a3,x3281))),
% 10.09/10.20 inference(scs_inference,[],[285,2])).
% 10.09/10.20 cnf(330,plain,
% 10.09/10.20 (E(f6(x3301,a3),a3)),
% 10.09/10.20 inference(scs_inference,[],[225,76,138,285,89,2,12,65])).
% 10.09/10.20 cnf(334,plain,
% 10.09/10.20 (P1(f6(x3341,x3342),f6(a2,x3342),f6(x3341,x3342))),
% 10.09/10.20 inference(rename_variables,[],[94])).
% 10.09/10.20 cnf(337,plain,
% 10.09/10.20 (P1(f6(x3371,x3372),f6(a2,x3372),f6(x3371,x3372))),
% 10.09/10.20 inference(rename_variables,[],[94])).
% 10.09/10.20 cnf(338,plain,
% 10.09/10.20 (E(f6(f6(a7,a3),x3381),a3)),
% 10.09/10.20 inference(scs_inference,[],[94,334,225,235,183,76,284,138,285,89,2,12,65,9,13,11,3])).
% 10.09/10.20 cnf(339,plain,
% 10.09/10.20 (P2(f4(a3,a3),f4(a3,a3),f6(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.20 inference(scs_inference,[],[94,334,225,235,183,270,76,284,138,285,89,75,2,12,65,9,13,11,3,14])).
% 10.09/10.20 cnf(341,plain,
% 10.09/10.20 (P1(f6(x3411,a1),a8,f6(x3411,a1))),
% 10.09/10.20 inference(scs_inference,[],[94,334,337,225,235,183,270,76,284,138,285,16,89,75,2,12,65,9,13,11,3,14,10])).
% 10.09/10.20 cnf(342,plain,
% 10.09/10.20 (P1(f6(x3421,x3422),f6(a2,x3422),f6(x3421,x3422))),
% 10.09/10.20 inference(rename_variables,[],[94])).
% 10.09/10.20 cnf(347,plain,
% 10.09/10.20 (P1(f4(a3,a3),x3471,f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[309])).
% 10.09/10.20 cnf(352,plain,
% 10.09/10.20 (P2(f6(a7,a3),x3521,f4(f6(a7,a3),f4(x3521,a3)))),
% 10.09/10.20 inference(scs_inference,[],[94,334,337,342,279,309,266,225,235,183,270,76,127,311,284,294,138,285,16,157,89,45,75,2,12,65,9,13,11,3,14,10,69,70,67,68])).
% 10.09/10.20 cnf(356,plain,
% 10.09/10.20 (P1(f6(a3,x3561),x3562,f6(a3,x3561))),
% 10.09/10.20 inference(scs_inference,[],[94,334,337,342,279,309,347,266,225,235,183,270,76,127,311,284,294,138,285,16,157,89,45,75,2,12,65,9,13,11,3,14,10,69,70,67,68,73])).
% 10.09/10.20 cnf(358,plain,
% 10.09/10.20 (P1(f4(a3,a3),f6(a3,x3581),f6(a3,x3581))),
% 10.09/10.20 inference(scs_inference,[],[94,334,337,342,279,309,347,266,225,235,183,270,76,127,311,284,294,138,285,16,157,89,45,75,2,12,65,9,13,11,3,14,10,69,70,67,68,73,74])).
% 10.09/10.20 cnf(366,plain,
% 10.09/10.20 (E(f6(a3,x3661),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[358,309,143,2,66])).
% 10.09/10.20 cnf(367,plain,
% 10.09/10.20 (P1(f4(a3,a3),x3671,f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[309])).
% 10.09/10.20 cnf(369,plain,
% 10.09/10.20 (E(f4(f6(a7,a3),f4(a3,a3)),f6(a7,a3))),
% 10.09/10.20 inference(scs_inference,[],[358,309,352,143,27,2,66,65])).
% 10.09/10.20 cnf(374,plain,
% 10.09/10.20 (P2(f6(a3,x3741),f6(a3,x3741),f6(a3,x3741))),
% 10.09/10.20 inference(rename_variables,[],[117])).
% 10.09/10.20 cnf(375,plain,
% 10.09/10.20 (P2(f6(a3,x3751),f4(f6(x3752,x3752),f6(x3752,x3752)),f6(a3,x3751))),
% 10.09/10.20 inference(scs_inference,[],[358,309,117,374,352,244,143,27,2,66,65,12,13])).
% 10.09/10.20 cnf(376,plain,
% 10.09/10.20 (P2(f6(a3,x3761),f6(a3,x3761),f6(a3,x3761))),
% 10.09/10.20 inference(rename_variables,[],[117])).
% 10.09/10.20 cnf(377,plain,
% 10.09/10.20 (E(f6(f6(a7,a3),x3771),f6(a3,x3772))),
% 10.09/10.20 inference(scs_inference,[],[358,309,117,374,145,352,244,338,143,27,2,66,65,12,13,3])).
% 10.09/10.20 cnf(378,plain,
% 10.09/10.20 (P1(f6(a3,x3781),f6(a3,x3782),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[216,358,309,117,374,145,352,244,338,143,27,2,66,65,12,13,3,9])).
% 10.09/10.20 cnf(379,plain,
% 10.09/10.20 (P2(f6(a3,x3791),f4(a3,a3),f6(a3,x3792))),
% 10.09/10.20 inference(scs_inference,[],[216,358,309,117,374,145,352,289,244,338,143,189,27,2,66,65,12,13,3,9,14])).
% 10.09/10.20 cnf(380,plain,
% 10.09/10.20 (E(f4(x3801,x3801),f6(a3,x3802))),
% 10.09/10.20 inference(rename_variables,[],[189])).
% 10.09/10.20 cnf(384,plain,
% 10.09/10.20 (P1(a3,f6(a3,x3841),f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[216])).
% 10.09/10.20 cnf(385,plain,
% 10.09/10.20 (P1(f6(a1,f4(a2,a2)),f4(a3,a3),f6(a3,x3851))),
% 10.09/10.20 inference(scs_inference,[],[216,384,279,358,309,117,374,145,352,289,244,338,143,189,380,27,2,66,65,12,13,3,9,14,11,10,70])).
% 10.09/10.20 cnf(388,plain,
% 10.09/10.20 (P2(a3,f6(a3,x3881),a3)),
% 10.09/10.20 inference(scs_inference,[],[216,384,279,358,309,117,374,376,145,352,289,244,338,143,31,189,380,27,2,66,65,12,13,3,9,14,11,10,70,67])).
% 10.09/10.20 cnf(392,plain,
% 10.09/10.20 (P1(f4(a3,a3),a3,f6(a3,x3921))),
% 10.09/10.20 inference(scs_inference,[],[216,384,292,279,356,358,309,117,374,376,145,127,352,289,244,338,143,31,189,380,27,2,66,65,12,13,3,9,14,11,10,70,67,69])).
% 10.09/10.20 cnf(393,plain,
% 10.09/10.20 (P1(f6(a3,x3931),x3932,f6(a3,x3931))),
% 10.09/10.20 inference(rename_variables,[],[356])).
% 10.09/10.20 cnf(404,plain,
% 10.09/10.20 (P2(f6(a3,x4041),f6(a3,x4041),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[216,384,292,279,356,393,358,273,309,367,117,374,376,145,127,352,262,289,244,338,143,31,48,189,380,27,26,2,66,65,12,13,3,9,14,11,10,70,67,69,68,74,71])).
% 10.09/10.20 cnf(416,plain,
% 10.09/10.20 (E(f6(a7,a3),f4(f6(a7,a3),f4(a3,a3)))),
% 10.09/10.20 inference(scs_inference,[],[369,2])).
% 10.09/10.20 cnf(417,plain,
% 10.09/10.20 (E(f4(a3,a3),f4(f6(x4171,x4171),f6(x4171,x4171)))),
% 10.09/10.20 inference(scs_inference,[],[404,369,93,2,65])).
% 10.09/10.20 cnf(418,plain,
% 10.09/10.20 (P2(x4181,x4181,f4(f6(x4182,x4182),f6(x4182,x4182)))),
% 10.09/10.20 inference(rename_variables,[],[93])).
% 10.09/10.20 cnf(420,plain,
% 10.09/10.20 (P2(f4(a3,a3),a3,f6(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.20 inference(scs_inference,[],[404,369,339,93,17,2,65,13])).
% 10.09/10.20 cnf(421,plain,
% 10.09/10.20 (E(f4(x4211,a3),x4211)),
% 10.09/10.20 inference(rename_variables,[],[17])).
% 10.09/10.20 cnf(422,plain,
% 10.09/10.20 (P1(f4(a3,a3),f6(a2,x4221),f6(a3,x4221))),
% 10.09/10.20 inference(scs_inference,[],[94,404,366,369,339,93,17,2,65,13,9])).
% 10.09/10.20 cnf(423,plain,
% 10.09/10.20 (P1(f6(x4231,x4232),f6(a2,x4232),f6(x4231,x4232))),
% 10.09/10.20 inference(rename_variables,[],[94])).
% 10.09/10.20 cnf(424,plain,
% 10.09/10.20 (P2(f6(a7,a3),f6(a7,a3),f6(a3,x4241))),
% 10.09/10.20 inference(scs_inference,[],[94,404,366,273,369,339,377,93,17,2,65,13,9,14])).
% 10.09/10.20 cnf(427,plain,
% 10.09/10.20 (P2(f6(a3,x4271),f6(a3,x4271),f6(a3,x4271))),
% 10.09/10.20 inference(rename_variables,[],[117])).
% 10.09/10.20 cnf(432,plain,
% 10.09/10.20 (P1(a3,f6(a3,x4321),f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[216])).
% 10.09/10.20 cnf(433,plain,
% 10.09/10.20 (P2(f4(a3,a3),f6(a3,x4331),f4(f6(x4332,x4332),f6(x4332,x4332)))),
% 10.09/10.20 inference(scs_inference,[],[216,292,94,404,366,273,117,427,145,369,339,377,182,93,418,17,421,2,65,13,9,14,12,3,11,10,67])).
% 10.09/10.20 cnf(435,plain,
% 10.09/10.20 (P2(f6(a3,x4351),f6(a3,x4351),f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[404])).
% 10.09/10.20 cnf(444,plain,
% 10.09/10.20 (P2(f6(a3,x4441),f6(a3,x4442),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[216,432,292,94,279,404,435,366,309,273,117,427,123,270,145,369,339,377,379,182,93,418,17,421,2,65,13,9,14,12,3,11,10,67,70,69,68])).
% 10.09/10.20 cnf(447,plain,
% 10.09/10.20 (P1(f6(a3,x4471),f4(a3,a3),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[216,432,292,94,279,404,435,366,356,309,273,117,427,123,270,145,369,339,377,379,182,93,418,17,421,2,65,13,9,14,12,3,11,10,67,70,69,68,74])).
% 10.09/10.20 cnf(448,plain,
% 10.09/10.20 (P2(f6(a3,x4481),f6(a3,x4481),f4(a3,a3))),
% 10.09/10.20 inference(rename_variables,[],[404])).
% 10.09/10.20 cnf(459,plain,
% 10.09/10.20 (P2(f6(a7,a1),f6(a7,a1),f6(a7,a1))+~P2(f6(a2,a2),f6(a2,a2),f6(a2,a2))),
% 10.09/10.20 inference(scs_inference,[],[216,432,292,94,423,279,132,404,435,448,366,356,309,273,117,427,123,270,145,369,339,34,377,379,196,182,93,418,89,17,421,2,65,13,9,14,12,3,11,10,67,70,69,68,74,73,72,71])).
% 10.09/10.20 cnf(461,plain,
% 10.09/10.20 (E(f4(f6(x4611,x4611),f6(x4611,x4611)),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[417,2])).
% 10.09/10.20 cnf(462,plain,
% 10.09/10.20 (E(f6(f4(a3,a3),f4(a3,a3)),a3)),
% 10.09/10.20 inference(scs_inference,[],[417,420,106,2,65])).
% 10.09/10.20 cnf(465,plain,
% 10.09/10.20 (P2(f4(a3,a3),f4(f6(x4651,x4651),f6(x4651,x4651)),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[270,417,420,106,2,65,13])).
% 10.09/10.20 cnf(466,plain,
% 10.09/10.20 (P2(f6(a7,a3),f6(a7,a3),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[366,270,417,424,420,106,2,65,13,14])).
% 10.09/10.20 cnf(467,plain,
% 10.09/10.20 (P2(f6(a7,a3),f6(a7,a3),f6(a3,x4671))),
% 10.09/10.20 inference(rename_variables,[],[424])).
% 10.09/10.20 cnf(469,plain,
% 10.09/10.20 (E(f6(x4691,a3),f6(a3,x4692))),
% 10.09/10.20 inference(scs_inference,[],[216,366,270,145,417,424,420,330,106,2,65,13,14,11,3])).
% 10.09/10.20 cnf(470,plain,
% 10.09/10.20 (P1(f4(f6(x4701,x4701),f6(x4701,x4701)),a3,f6(a3,x4702))),
% 10.09/10.20 inference(scs_inference,[],[216,392,366,270,145,417,424,420,330,106,2,65,13,14,11,3,9])).
% 10.09/10.20 cnf(471,plain,
% 10.09/10.20 (P2(f4(f6(x4711,x4711),f6(x4711,x4711)),f4(a3,a3),f4(a3,a3))),
% 10.09/10.20 inference(scs_inference,[],[216,392,366,270,145,417,424,420,330,106,2,65,13,14,11,3,9,12])).
% 10.09/10.20 cnf(474,plain,
% 10.09/10.20 (P1(f6(x4741,a7),a2,f6(x4741,a7))),
% 10.09/10.20 inference(scs_inference,[],[292,216,392,366,270,145,58,417,424,420,330,106,18,29,2,65,13,14,11,3,9,12,10,69])).
% 10.09/10.20 cnf(480,plain,
% 10.09/10.20 (P2(f6(a3,x4801),f6(a7,a3),f6(a3,x4801))),
% 10.09/10.20 inference(scs_inference,[],[292,279,216,392,266,356,366,270,111,145,58,417,424,467,420,330,106,18,29,2,65,13,14,11,3,9,12,10,69,70,67])).
% 10.09/10.21 cnf(491,plain,
% 10.09/10.21 (P1(f6(a7,a3),f6(a3,x4911),f6(a3,x4911))),
% 10.09/10.21 inference(scs_inference,[],[292,279,216,392,266,356,225,210,366,270,127,111,145,58,417,424,467,433,444,420,330,106,44,18,29,2,65,13,14,11,3,9,12,10,69,70,67,68,73,74])).
% 10.09/10.21 cnf(498,plain,
% 10.09/10.21 (E(f6(a3,x4981),f6(x4982,a3))),
% 10.09/10.21 inference(scs_inference,[],[469,2])).
% 10.09/10.21 cnf(499,plain,
% 10.09/10.21 (E(f6(f4(a1,a1),a2),f4(a7,a7))),
% 10.09/10.21 inference(scs_inference,[],[225,469,45,2,65])).
% 10.09/10.21 cnf(503,plain,
% 10.09/10.21 (E(x5031,f6(x5031,x5031))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(505,plain,
% 10.09/10.21 (E(x5051,f6(x5051,x5051))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(507,plain,
% 10.09/10.21 (E(x5071,f6(x5071,x5071))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(509,plain,
% 10.09/10.21 (E(x5091,f6(x5091,x5091))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(512,plain,
% 10.09/10.21 (E(f6(f4(a3,a3),f4(a3,a3)),f6(a3,x5121))),
% 10.09/10.21 inference(scs_inference,[],[216,392,225,270,145,466,469,462,45,75,503,505,507,509,2,65,13,9,11,12,14,3])).
% 10.09/10.21 cnf(520,plain,
% 10.09/10.21 (P1(f6(x5201,a8),a1,f6(x5201,a8))),
% 10.09/10.21 inference(scs_inference,[],[279,216,392,309,225,270,111,145,59,466,469,462,45,75,503,505,507,509,29,2,65,13,9,11,12,14,3,10,67,70,69])).
% 10.09/10.21 cnf(523,plain,
% 10.09/10.21 (P2(f6(a7,a3),f6(a3,x5231),f6(a3,x5231))),
% 10.09/10.21 inference(scs_inference,[],[279,216,392,309,225,270,111,145,59,466,480,469,462,424,45,75,503,505,507,509,29,2,65,13,9,11,12,14,3,10,67,70,69,68])).
% 10.09/10.21 cnf(538,plain,
% 10.09/10.21 (E(f4(a7,a7),f6(f4(a1,a1),a2))),
% 10.09/10.21 inference(scs_inference,[],[499,2])).
% 10.09/10.21 cnf(539,plain,
% 10.09/10.21 (E(f4(f4(x5391,a3),a3),x5391)),
% 10.09/10.21 inference(scs_inference,[],[44,499,101,2,65])).
% 10.09/10.21 cnf(540,plain,
% 10.09/10.21 (P2(x5401,x5402,f4(x5402,x5401))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(543,plain,
% 10.09/10.21 (E(f4(x5431,x5431),f6(a3,x5432))),
% 10.09/10.21 inference(rename_variables,[],[189])).
% 10.09/10.21 cnf(544,plain,
% 10.09/10.21 (P2(f4(a3,a3),f4(f6(x5441,x5441),f6(x5441,x5441)),f6(a3,x5442))),
% 10.09/10.21 inference(scs_inference,[],[465,471,44,499,101,189,543,2,65,13,14])).
% 10.09/10.21 cnf(545,plain,
% 10.09/10.21 (E(f4(x5451,x5451),f6(a3,x5452))),
% 10.09/10.21 inference(rename_variables,[],[189])).
% 10.09/10.21 cnf(547,plain,
% 10.09/10.21 (E(f4(x5471,x5471),f6(a3,x5472))),
% 10.09/10.21 inference(rename_variables,[],[189])).
% 10.09/10.21 cnf(549,plain,
% 10.09/10.21 (E(f4(x5491,x5491),f6(a3,x5492))),
% 10.09/10.21 inference(rename_variables,[],[189])).
% 10.09/10.21 cnf(555,plain,
% 10.09/10.21 (P1(a7,f6(a2,a2),a7)),
% 10.09/10.21 inference(scs_inference,[],[292,392,94,235,145,465,471,44,151,499,498,101,189,543,545,547,549,2,65,13,14,11,9,3,12,10,69])).
% 10.09/10.21 cnf(569,plain,
% 10.09/10.21 (P2(f6(x5691,a7),f6(x5691,a7),f6(x5691,a7))+~P2(a2,a2,a2)),
% 10.09/10.21 inference(scs_inference,[],[292,216,392,94,447,117,474,235,145,465,471,388,379,212,44,540,151,499,498,101,189,543,545,547,549,2,65,13,14,11,9,3,12,10,69,70,67,68,74,71])).
% 10.09/10.21 cnf(575,plain,
% 10.09/10.21 (E(f4(a3,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[270,44,512,2,65])).
% 10.09/10.21 cnf(576,plain,
% 10.09/10.21 (P2(x5761,x5762,f4(x5762,x5761))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(581,plain,
% 10.09/10.21 (E(f4(x5811,a3),x5811)),
% 10.09/10.21 inference(rename_variables,[],[17])).
% 10.09/10.21 cnf(582,plain,
% 10.09/10.21 (E(f4(f4(a3,a3),a3),f6(a3,x5821))),
% 10.09/10.21 inference(scs_inference,[],[378,270,145,311,44,461,512,539,17,2,65,13,11,3])).
% 10.09/10.21 cnf(584,plain,
% 10.09/10.21 (P2(f4(a3,a3),f6(a3,x5841),a3)),
% 10.09/10.21 inference(scs_inference,[],[378,270,145,296,311,44,461,512,539,17,581,2,65,13,11,3,14])).
% 10.09/10.21 cnf(585,plain,
% 10.09/10.21 (E(f4(x5851,a3),x5851)),
% 10.09/10.21 inference(rename_variables,[],[17])).
% 10.09/10.21 cnf(587,plain,
% 10.09/10.21 (E(f4(x5871,a3),x5871)),
% 10.09/10.21 inference(rename_variables,[],[17])).
% 10.09/10.21 cnf(597,plain,
% 10.09/10.21 (P2(x5971,f4(x5971,x5972),x5972)),
% 10.09/10.21 inference(rename_variables,[],[47])).
% 10.09/10.21 cnf(600,plain,
% 10.09/10.21 (P1(f6(a7,a3),x6001,f6(a7,a3))),
% 10.09/10.21 inference(rename_variables,[],[210])).
% 10.09/10.21 cnf(601,plain,
% 10.09/10.21 (P1(f6(a7,a3),f6(a3,x6011),f6(a3,x6011))),
% 10.09/10.21 inference(rename_variables,[],[491])).
% 10.09/10.21 cnf(603,plain,
% 10.09/10.21 (P2(f4(a3,a3),x6031,x6031)),
% 10.09/10.21 inference(scs_inference,[],[292,378,392,422,132,270,491,356,210,145,296,311,47,597,27,44,461,512,539,131,17,581,585,587,2,65,13,11,3,14,12,9,10,70,67,69,68])).
% 10.09/10.21 cnf(607,plain,
% 10.09/10.21 (P2(f6(a3,a3),f6(a3,a3),f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[292,378,392,422,132,270,491,601,356,111,210,600,145,296,311,47,597,27,44,461,512,539,131,17,581,585,587,2,65,13,11,3,14,12,9,10,70,67,69,68,71])).
% 10.09/10.21 cnf(616,plain,
% 10.09/10.21 (P2(a7,a7,f6(a3,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,292,378,392,422,132,270,491,601,356,111,210,600,145,46,296,311,47,597,27,26,44,576,461,512,539,131,17,581,585,587,2,65,13,11,3,14,12,9,10,70,67,69,68,71,73,72])).
% 10.09/10.21 cnf(625,plain,
% 10.09/10.21 (E(f6(x6251,a3),f4(f6(x6251,a3),f6(x6251,a3)))),
% 10.09/10.21 inference(scs_inference,[],[111,44,575,2,65])).
% 10.09/10.21 cnf(629,plain,
% 10.09/10.21 (E(f6(a3,x6291),f4(a3,a3))),
% 10.09/10.21 inference(rename_variables,[],[366])).
% 10.09/10.21 cnf(630,plain,
% 10.09/10.21 (E(f4(f6(a7,a3),a3),f6(a3,x6301))),
% 10.09/10.21 inference(scs_inference,[],[111,607,366,145,44,575,247,2,65,13,3])).
% 10.09/10.21 cnf(631,plain,
% 10.09/10.21 (P2(f4(a3,a3),f6(a3,a3),f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[111,607,366,629,145,44,575,247,2,65,13,3,12])).
% 10.09/10.21 cnf(640,plain,
% 10.09/10.21 (P1(a8,f4(f6(a1,a1),a3),a8)),
% 10.09/10.21 inference(scs_inference,[],[378,392,447,111,607,366,629,235,145,44,29,575,201,247,2,65,13,3,12,11,9,14,10,67,69])).
% 10.09/10.21 cnf(643,plain,
% 10.09/10.21 (P1(f6(a3,x6431),f4(a3,a3),f6(a3,x6432))),
% 10.09/10.21 inference(scs_inference,[],[378,392,447,309,111,607,366,629,235,145,44,29,575,201,247,2,65,13,3,12,11,9,14,10,67,69,70])).
% 10.09/10.21 cnf(648,plain,
% 10.09/10.21 (P2(a7,a7,f6(a1,a3))),
% 10.09/10.21 inference(scs_inference,[],[20,378,392,447,309,111,607,366,629,235,145,46,471,26,44,29,575,201,584,247,2,65,13,3,12,11,9,14,10,67,69,70,68,71])).
% 10.09/10.21 cnf(652,plain,
% 10.09/10.21 (P1(a1,f6(a3,a2),f6(a3,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,378,392,447,309,111,607,616,366,629,235,145,46,471,26,21,44,29,575,201,584,247,2,65,13,3,12,11,9,14,10,67,69,70,68,71,74])).
% 10.09/10.21 cnf(660,plain,
% 10.09/10.21 (E(f6(a3,x6601),f4(f6(a7,a3),a3))),
% 10.09/10.21 inference(scs_inference,[],[630,2])).
% 10.09/10.21 cnf(661,plain,
% 10.09/10.21 (P2(a7,f6(a1,a2),f6(a1,a3))),
% 10.09/10.21 inference(scs_inference,[],[648,76,630,2,13])).
% 10.09/10.21 cnf(662,plain,
% 10.09/10.21 (E(f5(a3),a3)),
% 10.09/10.21 inference(scs_inference,[],[648,76,28,630,30,2,13,65])).
% 10.09/10.21 cnf(667,plain,
% 10.09/10.21 (P1(a3,f6(a2,x6671),f6(a3,x6671))),
% 10.09/10.21 inference(scs_inference,[],[422,648,76,28,630,30,18,2,13,65,12,9])).
% 10.09/10.21 cnf(671,plain,
% 10.09/10.21 (E(f6(x6711,a3),f4(f6(x6711,a3),f6(x6711,a3)))),
% 10.09/10.21 inference(rename_variables,[],[625])).
% 10.09/10.21 cnf(673,plain,
% 10.09/10.21 (P1(f4(f6(x6731,x6731),f6(x6731,x6731)),a3,f6(a3,x6732))),
% 10.09/10.21 inference(rename_variables,[],[470])).
% 10.09/10.21 cnf(679,plain,
% 10.09/10.21 (P1(f6(a3,x6791),f6(a3,x6792),f6(a3,x6793))),
% 10.09/10.21 inference(scs_inference,[],[63,292,392,422,470,673,640,648,76,366,341,28,15,630,625,671,30,18,2,13,65,12,9,3,14,11,10,69,70])).
% 10.09/10.21 cnf(701,plain,
% 10.09/10.21 (E(f4(a3,a3),f6(f4(a3,a3),x7011))),
% 10.09/10.21 inference(scs_inference,[],[309,61,582,2,66])).
% 10.09/10.21 cnf(702,plain,
% 10.09/10.21 (P1(x7021,f6(x7021,x7022),f6(x7021,x7022))),
% 10.09/10.21 inference(rename_variables,[],[61])).
% 10.09/10.21 cnf(703,plain,
% 10.09/10.21 (P1(f4(a3,a3),x7031,f4(a3,a3))),
% 10.09/10.21 inference(rename_variables,[],[309])).
% 10.09/10.21 cnf(707,plain,
% 10.09/10.21 (E(x7071,f6(x7071,x7071))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(711,plain,
% 10.09/10.21 (P1(f4(a3,a3),x7111,f6(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[309,703,616,366,76,61,582,75,707,2,66,13,9,14,12,11])).
% 10.09/10.21 cnf(716,plain,
% 10.09/10.21 (P1(f6(x7161,x7162),f6(a2,x7162),f6(x7161,x7162))),
% 10.09/10.21 inference(rename_variables,[],[94])).
% 10.09/10.21 cnf(719,plain,
% 10.09/10.21 (P1(f4(a3,a3),x7191,f4(a3,a3))),
% 10.09/10.21 inference(rename_variables,[],[309])).
% 10.09/10.21 cnf(725,plain,
% 10.09/10.21 (P1(a8,f6(a2,a1),a8)),
% 10.09/10.21 inference(scs_inference,[],[309,703,132,94,716,616,366,76,61,46,465,471,538,86,582,80,140,157,75,707,2,66,13,9,14,12,11,3,10,70,67,69])).
% 10.09/10.21 cnf(730,plain,
% 10.09/10.21 (P2(f4(a3,a3),f4(a3,a3),f6(f6(a3,x7301),x7302))),
% 10.09/10.21 inference(scs_inference,[],[309,703,719,132,94,716,616,366,76,61,702,46,465,471,294,631,538,86,582,80,140,157,75,707,2,66,13,9,14,12,11,3,10,70,67,69,68,72])).
% 10.09/10.21 cnf(735,plain,
% 10.09/10.21 (P1(a7,f6(a3,a2),f6(a3,a2))),
% 10.09/10.21 inference(scs_inference,[],[309,703,719,132,94,716,616,366,76,61,702,46,465,471,294,29,631,538,86,582,80,140,157,75,707,2,66,13,9,14,12,11,3,10,70,67,69,68,72,74])).
% 10.09/10.21 cnf(744,plain,
% 10.09/10.21 (E(f6(f6(a3,x7441),x7442),f4(a3,a3))),
% 10.09/10.21 inference(scs_inference,[],[701,730,603,2,65])).
% 10.09/10.21 cnf(748,plain,
% 10.09/10.21 (P2(f6(x7481,a3),f6(x7481,a3),f6(x7481,a3))),
% 10.09/10.21 inference(rename_variables,[],[111])).
% 10.09/10.21 cnf(751,plain,
% 10.09/10.21 (P1(f4(a3,a3),x7511,f6(f4(a3,a3),x7512))),
% 10.09/10.21 inference(scs_inference,[],[309,111,701,730,235,366,202,603,2,65,13,14,11])).
% 10.09/10.21 cnf(753,plain,
% 10.09/10.21 (E(f6(a3,x7531),f6(f4(a3,a3),x7532))),
% 10.09/10.21 inference(scs_inference,[],[392,309,111,701,730,235,366,202,603,2,65,13,14,11,9,3])).
% 10.09/10.21 cnf(761,plain,
% 10.09/10.21 (P1(a8,f6(a2,a2),a2)),
% 10.09/10.21 inference(scs_inference,[],[392,309,132,474,111,748,701,730,235,366,202,603,60,48,87,75,2,65,13,14,11,9,3,12,10,67,69])).
% 10.09/10.21 cnf(777,plain,
% 10.09/10.21 (P2(f6(a3,x7771),f6(a3,x7771),f6(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[392,309,132,474,111,748,648,210,701,730,235,366,202,28,47,603,544,29,60,48,87,711,75,2,65,13,14,11,9,3,12,10,67,69,70,68,74,71])).
% 10.09/10.21 cnf(785,plain,
% 10.09/10.21 (E(a3,f5(a3))),
% 10.09/10.21 inference(scs_inference,[],[662,2])).
% 10.09/10.21 cnf(787,plain,
% 10.09/10.21 (P2(f6(a3,x7871),f6(a3,x7871),f6(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.21 inference(rename_variables,[],[777])).
% 10.09/10.21 cnf(799,plain,
% 10.09/10.21 (P1(f6(a7,a3),x7991,f6(a7,a3))),
% 10.09/10.21 inference(rename_variables,[],[210])).
% 10.09/10.21 cnf(800,plain,
% 10.09/10.21 (P1(x8001,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(803,plain,
% 10.09/10.21 (P1(f4(a3,a3),x8031,f4(a3,a3))),
% 10.09/10.21 inference(rename_variables,[],[309])).
% 10.09/10.21 cnf(808,plain,
% 10.09/10.21 (P2(x8081,a3,x8081)),
% 10.09/10.21 inference(rename_variables,[],[27])).
% 10.09/10.21 cnf(812,plain,
% 10.09/10.21 (P2(x8121,a3,x8121)),
% 10.09/10.21 inference(rename_variables,[],[27])).
% 10.09/10.21 cnf(814,plain,
% 10.09/10.21 (P2(a3,a3,f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[132,309,216,127,800,422,725,210,799,777,787,730,701,366,145,302,388,27,808,812,101,31,662,753,75,2,13,11,3,14,12,10,9,69,70,67,68,71])).
% 10.09/10.21 cnf(826,plain,
% 10.09/10.21 (~P2(a8,a8,a8)+P2(a7,a7,a7)),
% 10.09/10.21 inference(scs_inference,[],[132,309,803,216,127,800,422,111,725,210,799,777,787,761,730,701,366,145,302,388,27,808,812,26,101,31,662,753,75,2,13,11,3,14,12,10,9,69,70,67,68,71,74,72,178])).
% 10.09/10.21 cnf(830,plain,
% 10.09/10.21 (E(f4(a3,a3),f6(f6(a3,x8301),x8302))),
% 10.09/10.21 inference(scs_inference,[],[744,2])).
% 10.09/10.21 cnf(833,plain,
% 10.09/10.21 (P1(f6(a3,x8331),x8332,f6(a3,x8331))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(836,plain,
% 10.09/10.21 (P1(f6(x8361,x8362),f6(a2,x8362),f6(x8361,x8362))),
% 10.09/10.21 inference(rename_variables,[],[94])).
% 10.09/10.21 cnf(840,plain,
% 10.09/10.21 (P1(f4(a3,a3),x8401,f6(a3,x8402))),
% 10.09/10.21 inference(scs_inference,[],[356,833,94,814,235,366,145,744,660,625,2,13,11,14,10,3,9])).
% 10.09/10.21 cnf(841,plain,
% 10.09/10.21 (P1(f6(a3,x8411),x8412,f6(a3,x8411))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(843,plain,
% 10.09/10.21 (P1(a2,f6(a2,a2),a2)),
% 10.09/10.21 inference(scs_inference,[],[356,833,94,836,814,761,235,366,145,744,660,625,2,13,11,14,10,3,9,12,69])).
% 10.09/10.21 cnf(846,plain,
% 10.09/10.21 (P2(a3,a3,f6(a3,x8461))),
% 10.09/10.21 inference(scs_inference,[],[356,833,94,836,814,761,235,366,145,388,523,744,660,625,2,13,11,14,10,3,9,12,69,68])).
% 10.09/10.21 cnf(849,plain,
% 10.09/10.21 (P2(f6(a7,a3),f4(x8491,a3),x8491)),
% 10.09/10.21 inference(scs_inference,[],[356,833,94,836,814,761,235,366,145,28,388,101,523,744,660,625,2,13,11,14,10,3,9,12,69,68,67])).
% 10.09/10.21 cnf(852,plain,
% 10.09/10.21 (P1(a2,f6(a3,a2),f6(a8,f6(a3,a2)))),
% 10.09/10.21 inference(scs_inference,[],[22,356,833,94,836,652,814,761,235,366,145,46,28,388,101,523,744,660,625,2,13,11,14,10,3,9,12,69,68,67,70])).
% 10.09/10.21 cnf(860,plain,
% 10.09/10.21 (P2(f6(a3,x8601),f6(a3,x8601),f6(f4(a3,a3),x8602))),
% 10.09/10.21 inference(scs_inference,[],[22,392,356,833,841,94,836,111,652,814,761,235,366,145,46,28,388,26,101,523,751,744,660,625,2,13,11,14,10,3,9,12,69,68,67,70,73,71])).
% 10.09/10.21 cnf(863,plain,
% 10.09/10.21 (P1(x8631,f6(a7,a3),f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[22,392,356,833,841,127,94,836,111,652,814,761,235,366,145,46,28,388,26,101,523,751,744,660,625,2,13,11,14,10,3,9,12,69,68,67,70,73,71,74])).
% 10.09/10.21 cnf(865,plain,
% 10.09/10.21 (E(f4(a3,a3),f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[22,392,309,356,833,841,127,94,836,111,652,814,761,235,366,145,46,28,388,26,101,523,751,744,660,625,2,13,11,14,10,3,9,12,69,68,67,70,73,71,74,66])).
% 10.09/10.21 cnf(868,plain,
% 10.09/10.21 (P2(f6(a8,x8681),f6(a8,x8681),f6(a8,x8681))+~P2(a2,a2,a2)),
% 10.09/10.21 inference(scs_inference,[],[22,392,309,356,833,841,127,94,836,111,652,814,761,235,366,145,46,28,388,26,101,523,57,751,744,660,625,2,13,11,14,10,3,9,12,69,68,67,70,73,71,74,66,72])).
% 10.09/10.21 cnf(872,plain,
% 10.09/10.21 (P2(f6(a3,x8721),f6(a3,x8721),f6(f4(a3,a3),x8722))),
% 10.09/10.21 inference(rename_variables,[],[860])).
% 10.09/10.21 cnf(877,plain,
% 10.09/10.21 (E(f6(x8771,a3),f6(a3,x8772))),
% 10.09/10.21 inference(rename_variables,[],[469])).
% 10.09/10.21 cnf(880,plain,
% 10.09/10.21 (P2(a7,a7,f6(a3,x8801))),
% 10.09/10.21 inference(scs_inference,[],[309,94,648,865,860,872,366,469,877,2,13,11,9,10,12,14])).
% 10.09/10.21 cnf(882,plain,
% 10.09/10.21 (E(f4(a3,a3),f6(f6(a7,a3),x8821))),
% 10.09/10.21 inference(scs_inference,[],[309,94,648,865,860,872,235,366,469,877,2,13,11,9,10,12,14,3])).
% 10.09/10.21 cnf(883,plain,
% 10.09/10.21 (P1(f4(a3,a3),x8831,a3)),
% 10.09/10.21 inference(scs_inference,[],[309,356,216,94,648,123,865,860,872,235,366,469,877,2,13,11,9,10,12,14,3,69])).
% 10.09/10.21 cnf(887,plain,
% 10.09/10.21 (P1(a1,f6(a8,f6(a3,a2)),f6(a3,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,309,356,216,94,648,123,865,735,860,872,852,235,366,469,877,2,13,11,9,10,12,14,3,69,70])).
% 10.09/10.21 cnf(900,plain,
% 10.09/10.21 (P2(f6(x9001,a3),f6(x9001,a3),f6(x9001,a3))),
% 10.09/10.21 inference(rename_variables,[],[111])).
% 10.09/10.21 cnf(904,plain,
% 10.09/10.21 (P2(f4(a3,a3),f4(a3,a3),f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[20,309,356,216,94,111,648,123,863,865,735,860,872,852,730,814,235,366,89,101,26,47,44,31,469,877,2,13,11,9,10,12,14,3,69,70,67,68,73,72])).
% 10.09/10.21 cnf(907,plain,
% 10.09/10.21 (P1(f4(a3,a3),x9071,f4(a3,a3))),
% 10.09/10.21 inference(rename_variables,[],[309])).
% 10.09/10.21 cnf(909,plain,
% 10.09/10.21 (P2(f4(a3,a3),f4(a3,a3),f6(f4(a3,a3),x9091))),
% 10.09/10.21 inference(scs_inference,[],[20,309,907,356,216,94,111,900,648,123,863,865,735,860,872,852,730,814,235,366,89,101,26,47,44,31,751,469,877,2,13,11,9,10,12,14,3,69,70,67,68,73,72,71])).
% 10.09/10.21 cnf(920,plain,
% 10.09/10.21 (P1(x9201,a3,f6(a3,x9202))),
% 10.09/10.21 inference(scs_inference,[],[127,909,865,145,882,2,13,11])).
% 10.09/10.21 cnf(924,plain,
% 10.09/10.21 (E(f4(a3,a3),f4(f6(a7,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[127,470,491,904,909,865,235,145,882,416,2,13,11,10,14,9,3])).
% 10.09/10.21 cnf(926,plain,
% 10.09/10.21 (P1(f4(a7,a2),f6(a2,a2),f4(a7,a2))),
% 10.09/10.21 inference(scs_inference,[],[127,470,491,904,909,843,865,235,145,882,416,54,2,13,11,10,14,9,3,12,69])).
% 10.09/10.21 cnf(935,plain,
% 10.09/10.21 (P1(a2,f6(a7,f6(a2,a1)),a8)),
% 10.09/10.21 inference(scs_inference,[],[22,127,111,470,491,725,904,909,843,97,865,814,235,145,27,249,31,882,416,54,2,13,11,10,14,9,3,12,69,67,68,70])).
% 10.09/10.21 cnf(938,plain,
% 10.09/10.21 (P1(f6(a3,a3),x9381,f4(f6(x9382,x9382),f6(x9382,x9382)))),
% 10.09/10.21 inference(scs_inference,[],[22,356,127,111,470,491,725,904,909,843,97,865,814,235,145,27,249,93,31,882,416,54,2,13,11,10,14,9,3,12,69,67,68,70,73])).
% 10.09/10.21 cnf(940,plain,
% 10.09/10.21 (P2(f6(x9401,a3),f6(x9401,a3),f6(x9401,a3))),
% 10.09/10.21 inference(rename_variables,[],[111])).
% 10.09/10.21 cnf(943,plain,
% 10.09/10.21 (P1(f4(a3,a3),f6(x9431,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[22,309,356,127,111,940,470,491,725,904,909,843,97,865,814,235,145,27,44,249,93,31,882,416,54,2,13,11,10,14,9,3,12,69,67,68,70,73,74])).
% 10.09/10.21 cnf(953,plain,
% 10.09/10.21 (E(a3,f6(x9531,a3))),
% 10.09/10.21 inference(scs_inference,[],[127,62,924,2,66])).
% 10.09/10.21 cnf(955,plain,
% 10.09/10.21 (P1(x9551,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(957,plain,
% 10.09/10.21 (E(f5(f4(a3,a3)),a3)),
% 10.09/10.21 inference(scs_inference,[],[127,603,30,62,924,2,66,65])).
% 10.09/10.21 cnf(965,plain,
% 10.09/10.21 (E(f6(a3,x9651),f4(f6(a7,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[127,216,904,701,366,480,603,30,62,924,2,66,65,11,13,14,3])).
% 10.09/10.21 cnf(973,plain,
% 10.09/10.21 (P1(x9731,f4(a3,a3),f4(a3,a3))),
% 10.09/10.21 inference(scs_inference,[],[127,955,94,216,491,555,935,904,701,76,366,480,603,30,62,924,2,66,65,11,13,14,3,10,12,9,69,70])).
% 10.09/10.21 cnf(976,plain,
% 10.09/10.21 (P2(x9761,x9762,f4(x9761,x9762))),
% 10.09/10.21 inference(rename_variables,[],[45])).
% 10.09/10.21 cnf(978,plain,
% 10.09/10.21 (P2(f6(x9781,a3),x9782,x9782)),
% 10.09/10.21 inference(scs_inference,[],[127,955,94,216,491,111,555,935,904,701,76,366,480,603,296,47,45,976,30,62,924,2,66,65,11,13,14,3,10,12,9,69,70,68,67])).
% 10.09/10.21 cnf(980,plain,
% 10.09/10.21 (P2(x9801,x9802,f4(x9801,x9802))),
% 10.09/10.21 inference(rename_variables,[],[45])).
% 10.09/10.21 cnf(985,plain,
% 10.09/10.21 (P1(x9851,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(987,plain,
% 10.09/10.21 (P2(a3,a3,f6(f4(a3,a3),x9871))),
% 10.09/10.21 inference(scs_inference,[],[127,955,985,94,216,491,111,555,935,904,701,76,814,366,480,603,296,47,45,976,980,30,751,62,924,2,66,65,11,13,14,3,10,12,9,69,70,68,67,73,71])).
% 10.09/10.21 cnf(1000,plain,
% 10.09/10.21 (E(f6(a3,x10001),f6(f6(a3,x10001),x10002))),
% 10.09/10.21 inference(scs_inference,[],[356,61,965,2,66])).
% 10.09/10.21 cnf(1002,plain,
% 10.09/10.21 (P1(f6(a3,x10021),x10022,f6(a3,x10021))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1004,plain,
% 10.09/10.21 (E(f6(f4(a3,a3),x10041),a3)),
% 10.09/10.21 inference(scs_inference,[],[356,987,61,28,965,2,66,65])).
% 10.09/10.21 cnf(1005,plain,
% 10.09/10.21 (P2(a3,x10051,x10051)),
% 10.09/10.21 inference(rename_variables,[],[28])).
% 10.09/10.21 cnf(1007,plain,
% 10.09/10.21 (P1(x10071,a3,f6(x10072,a3))),
% 10.09/10.21 inference(scs_inference,[],[356,127,953,987,61,28,965,2,66,65,11])).
% 10.09/10.21 cnf(1009,plain,
% 10.09/10.21 (E(f5(f4(a3,a3)),f6(x10091,a3))),
% 10.09/10.21 inference(scs_inference,[],[356,127,953,987,61,28,965,957,2,66,65,11,13,3])).
% 10.09/10.21 cnf(1010,plain,
% 10.09/10.21 (P1(x10101,f6(x10102,a3),a3)),
% 10.09/10.21 inference(scs_inference,[],[356,127,953,987,61,28,965,957,2,66,65,11,13,3,10])).
% 10.09/10.21 cnf(1014,plain,
% 10.09/10.21 (P1(f4(a2,a7),f6(a2,a2),f4(a2,a7))),
% 10.09/10.21 inference(scs_inference,[],[356,127,216,953,987,843,865,61,465,28,965,957,56,2,66,65,11,13,3,10,12,14,9,69])).
% 10.09/10.21 cnf(1017,plain,
% 10.09/10.21 (P1(f6(a3,x10171),x10172,f6(a3,x10171))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1018,plain,
% 10.09/10.21 (P1(x10181,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1031,plain,
% 10.09/10.21 (P2(f6(a3,x10311),f6(a3,x10311),f6(a7,a3))),
% 10.09/10.21 inference(scs_inference,[],[356,1002,1017,127,1018,216,648,279,863,953,987,843,860,909,865,61,465,603,28,1005,101,26,93,965,957,56,2,66,65,11,13,3,10,12,14,9,69,70,68,67,73,72])).
% 10.09/10.21 cnf(1044,plain,
% 10.09/10.21 (E(f6(a1,a3),f4(a7,a7))),
% 10.09/10.21 inference(scs_inference,[],[648,1000,45,2,65])).
% 10.09/10.21 cnf(1045,plain,
% 10.09/10.21 (P2(x10451,x10452,f4(x10451,x10452))),
% 10.09/10.21 inference(rename_variables,[],[45])).
% 10.09/10.21 cnf(1048,plain,
% 10.09/10.21 (P2(f6(a3,x10481),f6(a3,x10481),f6(a7,a3))),
% 10.09/10.21 inference(rename_variables,[],[1031])).
% 10.09/10.21 cnf(1050,plain,
% 10.09/10.21 (P1(f6(x10501,a7),a2,f6(x10501,a7))),
% 10.09/10.21 inference(rename_variables,[],[474])).
% 10.09/10.21 cnf(1051,plain,
% 10.09/10.21 (E(f6(a3,x10511),f6(f6(a3,x10511),x10512))),
% 10.09/10.21 inference(rename_variables,[],[1000])).
% 10.09/10.21 cnf(1055,plain,
% 10.09/10.21 (P2(f6(a3,x10551),f6(a3,x10551),f6(a7,a3))),
% 10.09/10.21 inference(rename_variables,[],[1031])).
% 10.09/10.21 cnf(1057,plain,
% 10.09/10.21 (E(f6(a3,x10571),f6(f6(a3,x10571),x10572))),
% 10.09/10.21 inference(rename_variables,[],[1000])).
% 10.09/10.21 cnf(1063,plain,
% 10.09/10.21 (P1(f4(a1,a8),a1,f4(a1,a8))),
% 10.09/10.21 inference(scs_inference,[],[474,1050,216,648,1031,1048,1055,1000,1051,1057,953,235,45,29,53,2,65,13,11,10,12,3,14,9,69])).
% 10.09/10.21 cnf(1066,plain,
% 10.09/10.21 (P1(a1,f4(a3,a3),f6(a7,f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[20,474,1050,216,648,973,1031,1048,1055,1000,1051,1057,953,235,46,45,29,53,2,65,13,11,10,12,3,14,9,69,70])).
% 10.09/10.21 cnf(1068,plain,
% 10.09/10.21 (P1(x10681,x10682,f6(x10681,x10682))),
% 10.09/10.21 inference(rename_variables,[],[46])).
% 10.09/10.21 cnf(1077,plain,
% 10.09/10.21 (P1(f6(a1,a3),a3,f4(f6(a7,a3),f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[20,474,1050,127,216,648,973,1031,1048,1055,1000,1051,1057,953,235,46,1068,375,256,388,45,1045,29,53,352,2,65,13,11,10,12,3,14,9,69,70,68,67,73])).
% 10.09/10.21 cnf(1082,plain,
% 10.09/10.21 (P2(f6(a3,x10821),f6(a3,x10821),f6(a3,x10822))),
% 10.09/10.21 inference(scs_inference,[],[20,474,1050,356,127,216,648,973,1031,1048,1055,1000,1051,1057,953,235,46,1068,375,256,388,45,1045,29,920,53,352,2,65,13,11,10,12,3,14,9,69,70,68,67,73,72])).
% 10.09/10.21 cnf(1094,plain,
% 10.09/10.21 (E(f4(a7,a7),f6(a1,a3))),
% 10.09/10.21 inference(scs_inference,[],[1044,2])).
% 10.09/10.21 cnf(1095,plain,
% 10.09/10.21 (E(f5(f4(a3,a3)),f6(a3,x10951))),
% 10.09/10.21 inference(scs_inference,[],[603,249,1044,2,65])).
% 10.09/10.21 cnf(1099,plain,
% 10.09/10.21 (P2(f6(a3,x10991),f6(f6(a3,x10991),x10992),f6(a3,x10993))),
% 10.09/10.21 inference(scs_inference,[],[1082,1000,603,249,1044,2,65,13])).
% 10.09/10.21 cnf(1100,plain,
% 10.09/10.21 (P2(f6(a3,x11001),f6(a3,x11001),f6(a3,x11002))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1101,plain,
% 10.09/10.21 (P1(f6(a3,x11011),x11012,f6(f6(a3,x11011),x11013))),
% 10.09/10.21 inference(scs_inference,[],[356,1082,1000,603,249,1044,2,65,13,11])).
% 10.09/10.21 cnf(1102,plain,
% 10.09/10.21 (P1(f6(a3,x11021),x11022,f6(a3,x11021))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1105,plain,
% 10.09/10.21 (E(f6(f4(a3,a3),x11051),f6(x11052,a3))),
% 10.09/10.21 inference(scs_inference,[],[356,79,1082,1000,953,603,249,1044,1004,75,2,65,13,11,10,3])).
% 10.09/10.21 cnf(1107,plain,
% 10.09/10.21 (P2(f6(a3,x11071),f6(a3,x11071),f6(a3,x11072))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1108,plain,
% 10.09/10.21 (P2(f6(f6(a3,x11081),x11082),f6(a3,x11081),f6(a3,x11083))),
% 10.09/10.21 inference(scs_inference,[],[356,79,1082,1100,1107,1000,953,603,249,1044,1004,75,2,65,13,11,10,3,14,12])).
% 10.09/10.21 cnf(1109,plain,
% 10.09/10.21 (P2(f6(a3,x11091),f6(a3,x11091),f6(a3,x11092))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1111,plain,
% 10.09/10.21 (P1(f6(a3,x11111),x11112,f6(a3,x11111))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1112,plain,
% 10.09/10.21 (P1(f4(a8,a1),a1,f4(a8,a1))),
% 10.09/10.21 inference(scs_inference,[],[356,1102,79,1082,1100,1107,1000,953,603,249,29,1044,1004,55,75,2,65,13,11,10,3,14,12,9,69])).
% 10.09/10.21 cnf(1116,plain,
% 10.09/10.21 (P1(f6(a3,x11161),x11162,f6(a3,x11161))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1117,plain,
% 10.09/10.21 (P1(x11171,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1125,plain,
% 10.09/10.21 (P2(f6(a3,x11251),f6(a3,x11251),f6(a3,x11252))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1127,plain,
% 10.09/10.21 (P2(f6(a3,x11271),f6(a3,x11271),f6(x11272,a3))),
% 10.09/10.21 inference(scs_inference,[],[356,1102,1111,1116,127,79,1082,1100,1107,1109,1125,1077,1031,1000,987,953,603,28,26,249,29,1007,1044,1004,55,75,2,65,13,11,10,3,14,12,9,69,70,68,67,72])).
% 10.09/10.21 cnf(1132,plain,
% 10.09/10.21 (P1(x11321,f6(a3,x11322),f6(a3,x11322))),
% 10.09/10.21 inference(scs_inference,[],[356,1102,1111,1116,127,1117,79,1082,1100,1107,1109,1125,1077,1031,1000,987,953,603,28,26,249,29,1007,1044,1004,846,55,75,2,65,13,11,10,3,14,12,9,69,70,68,67,72,74])).
% 10.09/10.21 cnf(1140,plain,
% 10.09/10.21 (E(f6(x11401,a3),f6(f4(a3,a3),x11402))),
% 10.09/10.21 inference(scs_inference,[],[1105,2])).
% 10.09/10.21 cnf(1141,plain,
% 10.09/10.21 (P2(f6(a3,x11411),f6(f6(a3,x11411),x11412),f6(x11413,a3))),
% 10.09/10.21 inference(scs_inference,[],[1127,1000,1105,2,13])).
% 10.09/10.21 cnf(1142,plain,
% 10.09/10.21 (P2(f6(a3,x11421),f6(a3,x11421),f6(x11422,a3))),
% 10.09/10.21 inference(rename_variables,[],[1127])).
% 10.09/10.21 cnf(1143,plain,
% 10.09/10.21 (E(f5(a3),f6(x11431,a3))),
% 10.09/10.21 inference(scs_inference,[],[1127,1000,953,1105,662,2,13,3])).
% 10.09/10.21 cnf(1145,plain,
% 10.09/10.21 (P1(a7,f6(a2,a2),f6(a1,a2))),
% 10.09/10.21 inference(scs_inference,[],[555,385,1127,865,1000,953,76,1105,662,2,13,3,10,11])).
% 10.09/10.21 cnf(1148,plain,
% 10.09/10.21 (P2(f6(f6(a3,x11481),x11482),f6(a3,x11481),f6(x11483,a3))),
% 10.09/10.21 inference(scs_inference,[],[555,385,1127,1142,865,1000,953,76,480,1105,662,2,13,3,10,11,14,12])).
% 10.09/10.21 cnf(1149,plain,
% 10.09/10.21 (P2(f6(a3,x11491),f6(a3,x11491),f6(x11492,a3))),
% 10.09/10.21 inference(rename_variables,[],[1127])).
% 10.09/10.21 cnf(1159,plain,
% 10.09/10.21 (P1(f6(a2,a2),a8,a8)),
% 10.09/10.21 inference(scs_inference,[],[132,94,555,725,385,648,1127,1142,865,1000,953,76,480,26,45,29,1105,51,662,75,2,13,3,10,11,14,12,9,68,69,70])).
% 10.09/10.21 cnf(1166,plain,
% 10.09/10.21 (P1(f6(x11661,a3),a2,f6(x11661,a3))),
% 10.09/10.21 inference(scs_inference,[],[132,474,94,555,725,385,648,1127,1142,1149,865,1000,953,76,480,26,89,47,45,29,1105,51,662,75,2,13,3,10,11,14,12,9,68,69,70,67,73])).
% 10.09/10.21 cnf(1179,plain,
% 10.09/10.21 (E(f6(x11791,a3),f5(f4(a3,a3)))),
% 10.09/10.21 inference(scs_inference,[],[1009,2])).
% 10.09/10.21 cnf(1180,plain,
% 10.09/10.21 (E(a3,f6(f6(a3,x11801),x11802))),
% 10.09/10.21 inference(scs_inference,[],[127,1101,1009,2,66])).
% 10.09/10.21 cnf(1181,plain,
% 10.09/10.21 (P1(f6(a3,x11811),x11812,f6(f6(a3,x11811),x11813))),
% 10.09/10.21 inference(rename_variables,[],[1101])).
% 10.09/10.21 cnf(1182,plain,
% 10.09/10.21 (P1(x11821,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1184,plain,
% 10.09/10.21 (E(f4(f4(x11841,a3),f6(a7,a3)),x11841)),
% 10.09/10.21 inference(scs_inference,[],[127,44,849,1101,1009,2,66,65])).
% 10.09/10.21 cnf(1189,plain,
% 10.09/10.21 (E(f6(x11891,a3),f6(f4(a3,a3),x11892))),
% 10.09/10.21 inference(rename_variables,[],[1140])).
% 10.09/10.21 cnf(1190,plain,
% 10.09/10.21 (P1(x11901,f6(a7,a3),f6(f6(a7,a3),x11902))),
% 10.09/10.21 inference(scs_inference,[],[127,863,648,730,865,235,44,849,1101,1140,1009,2,66,65,13,14,11])).
% 10.09/10.21 cnf(1203,plain,
% 10.09/10.21 (P1(x12031,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1206,plain,
% 10.09/10.21 (P1(a7,a8,f6(a7,a1))),
% 10.09/10.21 inference(scs_inference,[],[132,127,1182,555,94,309,863,840,648,909,730,865,235,366,46,603,27,44,849,1101,830,1140,1189,1009,2,66,65,13,14,11,3,12,10,9,68,69,70])).
% 10.09/10.21 cnf(1216,plain,
% 10.09/10.21 (P1(x12161,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1218,plain,
% 10.09/10.21 (P2(a3,a3,f6(x12181,a3))),
% 10.09/10.21 inference(scs_inference,[],[132,127,1182,1203,1216,555,94,309,863,840,648,909,730,987,865,235,366,46,603,27,30,44,47,1007,849,1101,1181,830,1140,1189,1009,2,66,65,13,14,11,3,12,10,9,68,69,70,67,71,72])).
% 10.09/10.21 cnf(1221,plain,
% 10.09/10.21 (P1(x12211,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1223,plain,
% 10.09/10.21 (P1(x12231,f6(x12232,a3),f6(x12232,a3))),
% 10.09/10.21 inference(scs_inference,[],[132,127,1182,1203,1216,1221,555,94,309,863,840,648,909,730,987,865,235,366,46,603,27,30,44,47,1007,849,1101,1181,830,1140,1189,1009,2,66,65,13,14,11,3,12,10,9,68,69,70,67,71,72,74])).
% 10.09/10.21 cnf(1229,plain,
% 10.09/10.21 (E(f6(f6(a3,x12291),x12292),a3)),
% 10.09/10.21 inference(scs_inference,[],[1180,2])).
% 10.09/10.21 cnf(1230,plain,
% 10.09/10.21 (E(f6(x12301,a3),f6(a2,a3))),
% 10.09/10.21 inference(scs_inference,[],[94,1223,1180,2,66])).
% 10.09/10.21 cnf(1234,plain,
% 10.09/10.21 (P2(a3,f6(f6(a3,x12341),x12342),f6(x12343,a3))),
% 10.09/10.21 inference(scs_inference,[],[94,1223,1180,1218,2,66,13])).
% 10.09/10.21 cnf(1239,plain,
% 10.09/10.21 (E(f4(f4(a3,a3),f6(a7,a3)),f6(x12391,a3))),
% 10.09/10.21 inference(scs_inference,[],[127,94,648,1223,1180,1218,953,1184,1179,2,66,13,11,14,12,3])).
% 10.09/10.21 cnf(1242,plain,
% 10.09/10.21 (P1(f6(f4(a3,a3),x12421),x12422,f6(a3,x12423))),
% 10.09/10.21 inference(scs_inference,[],[127,94,840,648,1223,1180,1218,701,953,1184,1179,2,66,13,11,14,12,3,10,9])).
% 10.09/10.21 cnf(1251,plain,
% 10.09/10.21 (P2(f6(x12511,a3),f4(a3,a3),f6(x12511,a3))),
% 10.09/10.21 inference(scs_inference,[],[22,127,94,840,648,973,1223,1066,1166,1180,1218,843,904,273,701,953,101,603,1184,1179,2,66,13,11,14,12,3,10,9,69,68,70,67])).
% 10.09/10.21 cnf(1269,plain,
% 10.09/10.21 (E(f6(f4(a3,a3),a7),f6(a3,x12691))),
% 10.09/10.21 inference(scs_inference,[],[474,1242,1230,2,66])).
% 10.09/10.21 cnf(1273,plain,
% 10.09/10.21 (P2(f6(a2,a3),f6(a3,a3),f6(a3,x12731))),
% 10.09/10.21 inference(scs_inference,[],[474,1082,1242,1230,2,66,12])).
% 10.09/10.21 cnf(1274,plain,
% 10.09/10.21 (P2(f6(a3,x12741),f6(a3,x12741),f6(a3,x12742))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1275,plain,
% 10.09/10.21 (E(f6(x12751,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1277,plain,
% 10.09/10.21 (P2(f6(a3,x12771),f6(a3,x12771),f6(a3,x12772))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1278,plain,
% 10.09/10.21 (E(f6(x12781,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1281,plain,
% 10.09/10.21 (E(f6(x12811,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1283,plain,
% 10.09/10.21 (P1(f6(a3,x12831),x12832,f6(a3,x12831))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1284,plain,
% 10.09/10.21 (E(f6(x12841,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1286,plain,
% 10.09/10.21 (P1(f6(a2,a3),x12861,f6(a3,a3))),
% 10.09/10.21 inference(scs_inference,[],[474,520,356,1283,648,1082,1274,1242,1230,1275,1278,1281,1284,953,1229,131,2,66,12,13,10,14,11,3,9])).
% 10.09/10.21 cnf(1287,plain,
% 10.09/10.21 (P1(f6(a3,x12871),x12872,f6(a3,x12871))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1294,plain,
% 10.09/10.21 (P2(a3,x12941,x12941)),
% 10.09/10.21 inference(rename_variables,[],[28])).
% 10.09/10.21 cnf(1295,plain,
% 10.09/10.21 (P2(a3,a3,f6(x12951,a3))),
% 10.09/10.21 inference(rename_variables,[],[1218])).
% 10.09/10.21 cnf(1303,plain,
% 10.09/10.21 (P2(f6(x13031,a3),f4(x13032,a3),x13032)),
% 10.09/10.21 inference(scs_inference,[],[474,127,520,356,1283,1287,840,679,667,648,1082,1274,1277,1218,1295,1242,943,1230,1275,1278,1281,1284,953,28,1294,101,1229,131,2,66,12,13,10,14,11,3,9,69,68,70,67])).
% 10.09/10.21 cnf(1321,plain,
% 10.09/10.21 (E(f6(f4(a3,a3),a8),f6(a3,x13211))),
% 10.09/10.21 inference(scs_inference,[],[520,1242,1095,2,66])).
% 10.09/10.21 cnf(1373,plain,
% 10.09/10.21 (E(f4(f5(x13731),x13731),f6(a3,x13732))),
% 10.09/10.21 inference(scs_inference,[],[44,249,1239,2,65])).
% 10.09/10.21 cnf(1375,plain,
% 10.09/10.21 (P2(x13751,x13752,f4(x13752,x13751))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1378,plain,
% 10.09/10.21 (P2(f6(a3,x13781),f6(a3,x13781),f6(f4(a3,a3),x13782))),
% 10.09/10.21 inference(rename_variables,[],[860])).
% 10.09/10.21 cnf(1379,plain,
% 10.09/10.21 (E(f6(x13791,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1383,plain,
% 10.09/10.21 (E(f6(x13831,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1387,plain,
% 10.09/10.21 (E(f6(x13871,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1392,plain,
% 10.09/10.21 (P1(f6(x13921,a8),a1,f6(x13921,a8))),
% 10.09/10.21 inference(rename_variables,[],[520])).
% 10.09/10.21 cnf(1397,plain,
% 10.09/10.21 (P1(a1,f6(a2,f6(a2,a2)),a7)),
% 10.09/10.21 inference(scs_inference,[],[20,555,79,520,840,679,1321,883,860,1378,1230,1379,1383,1387,273,76,46,44,249,1239,785,957,2,65,12,11,13,3,14,10,9,69,70])).
% 10.09/10.21 cnf(1403,plain,
% 10.09/10.21 (P2(f6(a3,x14031),f6(a3,x14031),f6(x14032,a3))),
% 10.09/10.21 inference(rename_variables,[],[1127])).
% 10.09/10.21 cnf(1408,plain,
% 10.09/10.21 (P2(x14081,x14082,f4(x14082,x14081))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1413,plain,
% 10.09/10.21 (P2(f6(a2,a3),f6(a2,a3),f6(a3,a3))),
% 10.09/10.21 inference(scs_inference,[],[20,555,79,520,1392,840,94,679,1127,1403,1218,1321,883,1286,860,1378,1230,1379,1383,1387,273,76,46,44,1375,1408,465,249,28,1251,1239,785,957,2,65,12,11,13,3,14,10,9,69,70,68,67,73,71])).
% 10.09/10.21 cnf(1427,plain,
% 10.09/10.21 (E(f4(a3,a3),f6(x14271,a3))),
% 10.09/10.21 inference(scs_inference,[],[309,1223,1373,2,66])).
% 10.09/10.21 cnf(1428,plain,
% 10.09/10.21 (P1(x14281,f6(x14282,a3),f6(x14282,a3))),
% 10.09/10.21 inference(rename_variables,[],[1223])).
% 10.09/10.21 cnf(1429,plain,
% 10.09/10.21 (P1(f4(a3,a3),x14291,f4(a3,a3))),
% 10.09/10.21 inference(rename_variables,[],[309])).
% 10.09/10.21 cnf(1431,plain,
% 10.09/10.21 (E(f4(f5(x14311),x14311),a3)),
% 10.09/10.21 inference(scs_inference,[],[309,1223,44,30,1373,2,66,65])).
% 10.09/10.21 cnf(1433,plain,
% 10.09/10.21 (P2(x14331,x14332,f4(x14332,x14331))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1435,plain,
% 10.09/10.21 (E(f4(f4(a3,a3),f6(a7,a3)),f6(a3,x14351))),
% 10.09/10.21 inference(scs_inference,[],[309,1223,145,44,30,1373,1184,2,66,65,3])).
% 10.09/10.21 cnf(1439,plain,
% 10.09/10.21 (E(f6(x14391,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1441,plain,
% 10.09/10.21 (E(f6(x14411,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1444,plain,
% 10.09/10.21 (E(f6(x14441,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1450,plain,
% 10.09/10.21 (P1(f6(x14501,x14502),f6(a2,x14502),f6(x14501,x14502))),
% 10.09/10.21 inference(rename_variables,[],[94])).
% 10.09/10.21 cnf(1464,plain,
% 10.09/10.21 (P2(f4(a3,a3),f4(a3,a3),f6(x14641,a3))),
% 10.09/10.21 inference(scs_inference,[],[725,309,1429,94,1450,1132,1223,1428,904,1397,1269,1230,1439,1441,1444,273,145,46,480,44,1433,296,58,30,48,1251,1373,1184,75,2,66,65,3,10,12,14,11,13,9,69,70,68,67,72])).
% 10.09/10.21 cnf(1474,plain,
% 10.09/10.21 (P2(f4(a2,a7),f4(a2,a7),f4(a2,a7))+~P2(f6(a2,a2),f6(a2,a2),f6(a2,a2))),
% 10.09/10.21 inference(scs_inference,[],[725,520,309,1429,94,1450,1132,1127,1223,1428,904,1014,1397,1269,1230,1439,1441,1444,273,145,46,480,44,1433,93,296,58,30,48,1251,1373,1184,75,2,66,65,3,10,12,14,11,13,9,69,70,68,67,72,73,71])).
% 10.09/10.21 cnf(1477,plain,
% 10.09/10.21 (E(f4(a3,f4(x14771,a3)),x14771)),
% 10.09/10.21 inference(scs_inference,[],[1427,45,101,2,65])).
% 10.09/10.21 cnf(1478,plain,
% 10.09/10.21 (P2(x14781,x14782,f4(x14781,x14782))),
% 10.09/10.21 inference(rename_variables,[],[45])).
% 10.09/10.21 cnf(1481,plain,
% 10.09/10.21 (P1(f4(a3,a3),x14811,f6(x14812,a3))),
% 10.09/10.21 inference(scs_inference,[],[309,1464,1427,45,101,2,65,12,11])).
% 10.09/10.21 cnf(1483,plain,
% 10.09/10.21 (E(f4(f5(x14831),x14831),f6(x14832,a3))),
% 10.09/10.21 inference(scs_inference,[],[309,643,1464,1427,953,45,101,1431,2,65,12,11,10,3])).
% 10.09/10.21 cnf(1500,plain,
% 10.09/10.21 (P2(x15001,x15002,f4(x15001,x15002))),
% 10.09/10.21 inference(rename_variables,[],[45])).
% 10.09/10.21 cnf(1507,plain,
% 10.09/10.21 (P1(f6(x15071,a3),x15072,f6(x15071,a3))),
% 10.09/10.21 inference(scs_inference,[],[555,127,309,643,1132,1127,1464,1427,1230,953,46,202,45,1478,1500,101,59,48,1101,1303,1431,2,65,12,11,10,3,14,13,9,70,69,68,67,73])).
% 10.09/10.21 cnf(1509,plain,
% 10.09/10.21 (P2(f6(a7,a1),f6(a7,a1),f6(a7,a1))+~P2(a7,a7,a7)),
% 10.09/10.21 inference(scs_inference,[],[555,127,309,643,1132,1127,1206,1464,1427,1230,953,46,202,45,1478,1500,101,59,48,1101,1303,1431,2,65,12,11,10,3,14,13,9,70,69,68,67,73,72])).
% 10.09/10.21 cnf(1511,plain,
% 10.09/10.21 (P2(f6(a7,a1),f6(a7,a1),f6(a7,a1))+~P2(a8,a8,a8)),
% 10.09/10.21 inference(scs_inference,[],[555,127,309,643,1132,1127,1206,1464,1427,1230,953,46,202,45,1478,1500,101,59,48,1101,1303,1431,2,65,12,11,10,3,14,13,9,70,69,68,67,73,72,71])).
% 10.09/10.21 cnf(1515,plain,
% 10.09/10.21 (P2(x15151,x15152,f4(x15152,x15151))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1522,plain,
% 10.09/10.21 (E(f6(x15221,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1528,plain,
% 10.09/10.21 (P1(f6(x15281,a3),x15282,f6(a3,x15283))),
% 10.09/10.21 inference(scs_inference,[],[840,679,385,1082,909,1230,1522,1427,953,302,44,1483,1477,2,65,3,13,14,12,10,11,9])).
% 10.09/10.21 cnf(1535,plain,
% 10.09/10.21 (P1(f4(a3,a3),x15351,f6(a3,x15352))),
% 10.09/10.21 inference(rename_variables,[],[840])).
% 10.09/10.21 cnf(1546,plain,
% 10.09/10.21 (P2(x15461,x15462,f4(x15462,x15461))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1550,plain,
% 10.09/10.21 (P1(f6(a3,x15501),x15502,f4(f6(a3,x15503),f6(a3,x15503)))),
% 10.09/10.21 inference(scs_inference,[],[20,840,1535,356,679,385,1082,1223,1464,909,1230,1522,1427,953,302,379,44,1515,1546,27,47,751,57,1483,1477,2,65,3,13,14,12,10,11,9,70,69,68,67,74,73])).
% 10.09/10.21 cnf(1559,plain,
% 10.09/10.21 (E(f4(x15591,f5(x15591)),a3)),
% 10.09/10.21 inference(scs_inference,[],[44,31,1435,2,65])).
% 10.09/10.21 cnf(1561,plain,
% 10.09/10.21 (P2(x15611,x15612,f4(x15612,x15611))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1564,plain,
% 10.09/10.21 (P1(a8,f6(a2,a2),f6(a2,a2))),
% 10.09/10.21 inference(scs_inference,[],[761,730,1427,44,31,1435,75,2,65,12,11])).
% 10.09/10.21 cnf(1566,plain,
% 10.09/10.21 (E(f4(f4(a3,a3),a3),f6(x15661,a3))),
% 10.09/10.21 inference(scs_inference,[],[761,730,1427,953,44,31,1435,539,75,2,65,12,11,3])).
% 10.09/10.21 cnf(1584,plain,
% 10.09/10.21 (P1(f6(a3,x15841),x15842,f4(f6(a3,x15843),f6(a3,x15843)))),
% 10.09/10.21 inference(rename_variables,[],[1550])).
% 10.09/10.21 cnf(1585,plain,
% 10.09/10.21 (P1(x15851,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1595,plain,
% 10.09/10.21 (P1(x15951,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1597,plain,
% 10.09/10.21 (P1(x15971,f6(x15972,a3),f4(a3,a3))),
% 10.09/10.21 inference(scs_inference,[],[20,127,1585,1595,94,761,1132,1218,1223,1550,1584,1321,730,1230,1427,953,256,294,101,379,44,1561,93,31,1190,1435,539,19,75,2,65,12,11,3,10,14,13,9,70,68,69,67,71,74])).
% 10.09/10.21 cnf(1609,plain,
% 10.09/10.21 (E(f4(x16091,f6(x16091,x16091)),a3)),
% 10.09/10.21 inference(scs_inference,[],[44,91,1566,2,65])).
% 10.09/10.21 cnf(1615,plain,
% 10.09/10.21 (P2(f4(a3,a3),f6(f4(a3,a3),x16151),f6(x16152,a3))),
% 10.09/10.21 inference(scs_inference,[],[926,1464,701,44,91,1566,19,2,65,10,13])).
% 10.09/10.21 cnf(1619,plain,
% 10.09/10.21 (E(f6(x16191,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1620,plain,
% 10.09/10.21 (E(f4(x16201,f5(x16201)),f6(x16202,a3))),
% 10.09/10.21 inference(scs_inference,[],[926,1464,1230,701,953,379,44,91,1566,1559,19,2,65,10,13,12,14,3])).
% 10.09/10.21 cnf(1631,plain,
% 10.09/10.21 (P1(f4(a3,a3),x16311,f6(a3,x16312))),
% 10.09/10.21 inference(rename_variables,[],[840])).
% 10.09/10.21 cnf(1635,plain,
% 10.09/10.21 (P2(f6(a3,x16351),f6(a3,x16351),f6(a3,x16352))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1639,plain,
% 10.09/10.21 (P2(f6(a3,x16391),f6(a3,x16391),f6(a3,x16392))),
% 10.09/10.21 inference(rename_variables,[],[1082])).
% 10.09/10.21 cnf(1642,plain,
% 10.09/10.21 (P2(f6(a3,x16421),f6(a3,x16421),f4(f6(a3,x16422),f6(a3,x16422)))),
% 10.09/10.21 inference(scs_inference,[],[20,840,356,938,640,1132,926,1082,1635,1639,1464,1597,1550,1230,1619,701,953,379,44,45,26,91,1481,1303,1566,1559,19,75,2,65,10,13,12,14,3,11,9,70,69,68,67,71])).
% 10.09/10.21 cnf(1645,plain,
% 10.09/10.21 (P1(f6(a3,x16451),x16452,f6(a3,x16451))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1648,plain,
% 10.09/10.21 (P2(x16481,x16481,f4(f6(x16482,x16482),f6(x16482,x16482)))),
% 10.09/10.21 inference(rename_variables,[],[93])).
% 10.09/10.21 cnf(1651,plain,
% 10.09/10.21 (P1(f6(a3,x16511),x16512,f4(f6(x16513,x16513),f6(x16513,x16513)))),
% 10.09/10.21 inference(scs_inference,[],[20,840,1631,356,1645,938,640,1132,926,1082,1635,1639,1464,1597,1550,1230,1619,701,953,379,44,45,93,1648,26,91,1481,1303,1566,1559,19,75,2,65,10,13,12,14,3,11,9,70,69,68,67,71,74,73])).
% 10.09/10.21 cnf(1659,plain,
% 10.09/10.21 (P2(f4(a3,a3),f6(f4(a3,a3),a7),f6(a3,x16591))),
% 10.09/10.21 inference(scs_inference,[],[1269,603,1620,2,14])).
% 10.09/10.21 cnf(1662,plain,
% 10.09/10.21 (P1(x16621,f6(a3,x16622),f6(a3,x16622))),
% 10.09/10.21 inference(rename_variables,[],[1132])).
% 10.09/10.21 cnf(1663,plain,
% 10.09/10.21 (E(f6(x16631,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1666,plain,
% 10.09/10.21 (E(f4(x16661,f6(x16661,x16661)),f6(x16662,a3))),
% 10.09/10.21 inference(scs_inference,[],[1132,1223,1269,1230,1663,953,603,1620,1609,2,14,11,10,3])).
% 10.09/10.21 cnf(1668,plain,
% 10.09/10.21 (P2(f6(a3,x16681),f6(a3,x16681),f4(f6(a3,x16682),f6(a3,x16682)))),
% 10.09/10.21 inference(rename_variables,[],[1642])).
% 10.09/10.21 cnf(1669,plain,
% 10.09/10.21 (E(f6(x16691,a3),f6(a2,a3))),
% 10.09/10.21 inference(rename_variables,[],[1230])).
% 10.09/10.21 cnf(1675,plain,
% 10.09/10.21 (P1(a2,f6(x16751,a1),a8)),
% 10.09/10.21 inference(scs_inference,[],[22,725,761,1132,1223,1642,1668,1269,1230,1663,1669,953,603,60,1620,1609,75,2,14,11,10,3,13,12,9,70])).
% 10.09/10.21 cnf(1684,plain,
% 10.09/10.21 (P1(x16841,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1691,plain,
% 10.09/10.21 (P2(a8,a8,a8)),
% 10.09/10.21 inference(scs_inference,[],[22,725,127,1684,761,1132,1662,1127,1082,1223,1464,1507,1642,1668,1269,1230,1663,1669,953,603,44,93,60,48,1620,1609,75,2,14,11,10,3,13,12,9,70,68,69,73,71])).
% 10.09/10.21 cnf(1694,plain,
% 10.09/10.21 (P2(a7,a7,a7)),
% 10.09/10.21 inference(scs_inference,[],[22,725,127,1684,761,1132,1662,1127,1082,1223,1464,1507,1642,1668,1269,1230,1663,1669,953,603,44,93,60,48,1620,1609,75,2,14,11,10,3,13,12,9,70,68,69,73,71,826])).
% 10.09/10.21 cnf(1695,plain,
% 10.09/10.21 (P2(a2,a2,a2)),
% 10.09/10.21 inference(scs_inference,[],[22,725,127,1684,761,1132,1662,1127,1082,1223,1464,1507,1642,1668,1269,1230,1663,1669,953,603,44,93,60,48,1620,1609,75,2,14,11,10,3,13,12,9,70,68,69,73,71,826,72])).
% 10.09/10.21 cnf(1698,plain,
% 10.09/10.21 (P2(f6(x16981,a7),f6(x16981,a7),f6(x16981,a7))),
% 10.09/10.21 inference(scs_inference,[],[1695,569])).
% 10.09/10.21 cnf(1699,plain,
% 10.09/10.21 (P2(f6(a8,x16991),f6(a8,x16991),f6(a8,x16991))),
% 10.09/10.21 inference(scs_inference,[],[1695,868])).
% 10.09/10.21 cnf(1700,plain,
% 10.09/10.21 (P2(f6(a7,a1),f6(a7,a1),f6(a7,a1))),
% 10.09/10.21 inference(scs_inference,[],[1694,1509])).
% 10.09/10.21 cnf(1701,plain,
% 10.09/10.21 (P2(f6(a7,a1),f6(a7,a1),f6(a7,a1))),
% 10.09/10.21 inference(scs_inference,[],[1691,1511])).
% 10.09/10.21 cnf(1703,plain,
% 10.09/10.21 (P2(a8,a8,f6(a8,a8))),
% 10.09/10.21 inference(scs_inference,[],[1691,1666,75,2,14])).
% 10.09/10.21 cnf(1704,plain,
% 10.09/10.21 (E(x17041,f6(x17041,x17041))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(1706,plain,
% 10.09/10.21 (E(x17061,f6(x17061,x17061))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(1708,plain,
% 10.09/10.21 (E(x17081,f6(x17081,x17081))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(1709,plain,
% 10.09/10.21 (E(f4(a3,f4(a3,a3)),f6(a3,x17091))),
% 10.09/10.21 inference(scs_inference,[],[1691,145,1666,1477,75,1704,1706,2,14,13,12,3])).
% 10.09/10.21 cnf(1712,plain,
% 10.09/10.21 (E(x17121,f6(x17121,x17121))),
% 10.09/10.21 inference(rename_variables,[],[75])).
% 10.09/10.21 cnf(1716,plain,
% 10.09/10.21 (P1(a1,a8,f6(a3,a1))),
% 10.09/10.21 inference(scs_inference,[],[20,640,1132,926,1063,1691,1675,145,1666,1477,131,75,1704,1706,1708,1712,2,14,13,12,3,11,10,9,70])).
% 10.09/10.21 cnf(1717,plain,
% 10.09/10.21 (P1(a2,f6(x17171,a1),a8)),
% 10.09/10.21 inference(rename_variables,[],[1675])).
% 10.09/10.21 cnf(1721,plain,
% 10.09/10.21 (P2(x17211,x17212,f4(x17212,x17211))),
% 10.09/10.21 inference(rename_variables,[],[44])).
% 10.09/10.21 cnf(1723,plain,
% 10.09/10.21 (P1(a8,x17231,a8)),
% 10.09/10.21 inference(scs_inference,[],[20,356,640,1132,926,1063,648,1691,1675,1717,145,44,661,1666,1477,131,75,1704,1706,1708,1712,2,14,13,12,3,11,10,9,70,68,69])).
% 10.09/10.21 cnf(1725,plain,
% 10.09/10.21 (P1(f6(a3,x17251),x17252,f6(a3,x17251))),
% 10.09/10.21 inference(rename_variables,[],[356])).
% 10.09/10.21 cnf(1729,plain,
% 10.09/10.21 (P2(f6(a1,a2),f6(a1,a2),f6(a1,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,356,640,1132,926,1063,648,1691,1694,1675,1717,145,44,661,1145,1666,1477,131,75,1704,1706,1708,1712,2,14,13,12,3,11,10,9,70,68,69,67,72])).
% 10.09/10.21 cnf(1737,plain,
% 10.09/10.21 (P2(a7,a7,f6(a1,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,356,1725,640,1132,926,1127,1063,648,1691,1694,1695,1159,1675,1717,145,46,44,1721,661,1145,1666,1477,131,75,1704,1706,1708,1712,2,14,13,12,3,11,10,9,70,68,69,67,72,74,73,71])).
% 10.09/10.21 cnf(1741,plain,
% 10.09/10.21 (E(a3,a8)),
% 10.09/10.21 inference(scs_inference,[],[127,1723,1709,2,66])).
% 10.09/10.21 cnf(1742,plain,
% 10.09/10.21 (P1(a8,x17421,a8)),
% 10.09/10.21 inference(rename_variables,[],[1723])).
% 10.09/10.21 cnf(1743,plain,
% 10.09/10.21 (P1(x17431,a3,a3)),
% 10.09/10.21 inference(rename_variables,[],[127])).
% 10.09/10.21 cnf(1755,plain,
% 10.09/10.21 (P1(a2,a7,a8)),
% 10.09/10.21 inference(scs_inference,[],[20,22,127,385,926,1112,1729,1723,1742,1230,145,1709,15,1609,131,75,2,66,14,11,13,10,3,9,12,70])).
% 10.09/10.21 cnf(1756,plain,
% 10.09/10.21 (P1(a8,x17561,a8)),
% 10.09/10.21 inference(rename_variables,[],[1723])).
% 10.09/10.21 cnf(1760,plain,
% 10.09/10.21 (P2(f6(x17601,a7),f6(x17601,a7),f6(x17601,a7))),
% 10.09/10.21 inference(rename_variables,[],[1698])).
% 10.09/10.21 cnf(1771,plain,
% 10.09/10.21 (P2(f6(a2,a2),f6(a2,a2),f6(a2,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,22,127,1743,1132,385,926,1112,1729,1698,1760,1723,1742,1756,1691,1230,145,1108,1099,1564,1709,15,1609,131,75,2,66,14,11,13,10,3,9,12,70,68,69,67,72])).
% 10.09/10.21 cnf(1777,plain,
% 10.09/10.21 (P2(f4(a7,a2),f4(a7,a2),f4(a7,a2))),
% 10.09/10.21 inference(scs_inference,[],[20,22,356,127,1743,1132,385,926,1082,1112,1729,1698,1760,1723,1742,1756,1691,1230,145,26,1108,1099,1564,1709,15,1609,131,75,2,66,14,11,13,10,3,9,12,70,68,69,67,72,73,71])).
% 10.09/10.21 cnf(1782,plain,
% 10.09/10.21 (P2(f6(a7,a1),f6(a7,a1),f6(a7,a1))),
% 10.09/10.21 inference(scs_inference,[],[1771,459])).
% 10.09/10.21 cnf(1784,plain,
% 10.09/10.21 (P2(f4(a2,a7),f4(a2,a7),f4(a2,a7))),
% 10.09/10.21 inference(scs_inference,[],[1771,1474])).
% 10.09/10.21 cnf(1785,plain,
% 10.09/10.21 (E(a8,a3)),
% 10.09/10.21 inference(scs_inference,[],[1741,2])).
% 10.09/10.21 cnf(1789,plain,
% 10.09/10.21 (P1(f6(a3,x17891),x17892,f6(a3,x17893))),
% 10.09/10.21 inference(scs_inference,[],[127,1242,1771,1741,1321,19,2,14,10,9])).
% 10.09/10.21 cnf(1791,plain,
% 10.09/10.21 (P1(x17911,a3,a8)),
% 10.09/10.21 inference(scs_inference,[],[127,1242,1771,1741,1321,19,2,14,10,9,11])).
% 10.09/10.21 cnf(1795,plain,
% 10.09/10.21 (P1(a2,f6(a3,a2),a8)),
% 10.09/10.21 inference(scs_inference,[],[22,127,1242,1218,1771,887,1741,1723,1321,1431,19,2,14,10,9,11,13,3,12,70])).
% 10.09/10.21 cnf(1796,plain,
% 10.09/10.21 (P1(a8,x17961,a8)),
% 10.09/10.21 inference(rename_variables,[],[1723])).
% 10.09/10.21 cnf(1800,plain,
% 10.09/10.21 (P2(f6(x18001,a7),f6(x18001,a7),f6(x18001,a7))),
% 10.09/10.21 inference(rename_variables,[],[1698])).
% 10.09/10.21 cnf(1802,plain,
% 10.09/10.21 (P1(f6(a7,a1),x18021,f6(a7,a1))),
% 10.09/10.21 inference(scs_inference,[],[22,127,1242,1218,1771,887,1741,1698,1723,1796,1206,1321,1148,1431,19,2,14,10,9,11,13,3,12,70,68,69])).
% 10.09/10.21 cnf(1810,plain,
% 10.09/10.21 (P1(f6(x18101,a3),x18102,f4(f6(x18103,x18103),f6(x18103,x18103)))),
% 10.09/10.21 inference(scs_inference,[],[22,356,127,1242,1127,1218,1771,887,1741,1695,1698,1800,1723,1796,1206,1321,93,1148,1141,52,1431,19,2,14,10,9,11,13,3,12,70,68,69,67,72,73])).
% 10.09/10.21 cnf(1812,plain,
% 10.09/10.21 (P2(f6(a3,x18121),f6(a3,x18121),f6(x18122,a3))),
% 10.09/10.21 inference(rename_variables,[],[1127])).
% 10.09/10.21 cnf(1814,plain,
% 10.09/10.21 (P2(f6(x18141,a2),f6(x18141,a2),f6(x18141,a2))),
% 10.09/10.21 inference(scs_inference,[],[22,356,127,94,1242,1127,1218,1771,887,1741,1695,1698,1800,1723,1796,1206,1321,93,1148,1141,52,1431,19,2,14,10,9,11,13,3,12,70,68,69,67,72,73,71])).
% 10.09/10.21 cnf(1823,plain,
% 10.09/10.21 (E(f4(a3,a3),a8)),
% 10.09/10.21 inference(scs_inference,[],[22,309,356,127,94,1132,1242,1127,1812,123,1218,1771,887,1741,1695,1698,1800,1723,1796,1206,1321,27,93,1148,1141,52,1431,19,2,14,10,9,11,13,3,12,70,68,69,67,72,73,71,74,66])).
% 10.09/10.21 cnf(1826,plain,
% 10.09/10.21 (E(a8,f4(a3,a3))),
% 10.09/10.21 inference(scs_inference,[],[1823,2])).
% 10.09/10.21 cnf(1827,plain,
% 10.09/10.21 (E(a3,f6(a7,a1))),
% 10.09/10.21 inference(scs_inference,[],[127,1802,1823,2,66])).
% 10.09/10.21 cnf(1828,plain,
% 10.09/10.21 (P1(f6(a7,a1),x18281,f6(a7,a1))),
% 10.09/10.21 inference(rename_variables,[],[1802])).
% 10.09/10.21 cnf(1829,plain,
% 10.09/10.21 (P1(x18291,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(1833,plain,
% 10.09/10.22 (P1(a2,a1,a3)),
% 10.09/10.22 inference(scs_inference,[],[22,127,1802,1700,1823,1785,75,2,66,14,11])).
% 10.09/10.22 cnf(1837,plain,
% 10.09/10.22 (P1(a8,x18371,f4(a3,a3))),
% 10.09/10.22 inference(scs_inference,[],[22,309,127,385,1464,1802,1700,1823,366,1785,75,2,66,14,11,3,13,10,9])).
% 10.09/10.22 cnf(1839,plain,
% 10.09/10.22 (P1(a1,a8,f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[20,22,309,127,385,1464,1802,1700,1755,1823,366,46,1785,75,2,66,14,11,3,13,10,9,12,70])).
% 10.09/10.22 cnf(1847,plain,
% 10.09/10.22 (P1(f6(a7,a1),x18471,f6(a7,a1))),
% 10.09/10.22 inference(rename_variables,[],[1802])).
% 10.09/10.22 cnf(1848,plain,
% 10.09/10.22 (P1(x18481,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(1853,plain,
% 10.09/10.22 (P2(f4(a3,a3),f4(a3,a3),a8)),
% 10.09/10.22 inference(scs_inference,[],[20,22,309,127,1829,1132,385,1464,1802,1828,1700,1755,1814,1823,1694,366,46,880,1108,1791,1785,75,2,66,14,11,3,13,10,9,12,70,68,69,67,72])).
% 10.09/10.22 cnf(1856,plain,
% 10.09/10.22 (P1(f4(a3,a3),x18561,f4(a3,a3))),
% 10.09/10.22 inference(rename_variables,[],[309])).
% 10.09/10.22 cnf(1863,plain,
% 10.09/10.22 (P2(a3,a3,f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[20,22,309,1856,127,1829,1848,1132,385,1082,1218,1464,1802,1828,1847,1700,1755,1814,1823,1694,366,46,44,880,1108,1791,1785,75,2,66,14,11,3,13,10,9,12,70,68,69,67,72,74,71])).
% 10.09/10.22 cnf(1873,plain,
% 10.09/10.22 (E(f6(a7,a1),a3)),
% 10.09/10.22 inference(scs_inference,[],[1827,2])).
% 10.09/10.22 cnf(1876,plain,
% 10.09/10.22 (E(f4(x18761,f5(x18761)),f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[1777,1827,1559,75,2,14,3])).
% 10.09/10.22 cnf(1880,plain,
% 10.09/10.22 (P1(a8,x18801,f6(a3,x18802))),
% 10.09/10.22 inference(scs_inference,[],[22,840,127,1218,1777,1827,1823,1826,1559,75,2,14,3,13,10,11,9])).
% 10.09/10.22 cnf(1882,plain,
% 10.09/10.22 (P1(a2,a7,f4(a3,a3))),
% 10.09/10.22 inference(scs_inference,[],[20,22,840,127,1218,1777,1837,1827,1823,1826,1559,75,2,14,3,13,10,11,9,12,70])).
% 10.09/10.22 cnf(1889,plain,
% 10.09/10.22 (P1(f6(a7,a7),x18891,f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[20,22,840,127,1218,1777,1837,1827,1839,1814,1723,1823,1148,1826,1559,75,2,14,3,13,10,11,9,12,70,68,69])).
% 10.09/10.22 cnf(1894,plain,
% 10.09/10.22 (P2(f6(a2,a8),f6(a2,a8),f6(a2,a8))),
% 10.09/10.22 inference(scs_inference,[],[20,22,840,127,1218,1777,1837,1853,1827,1839,1814,1695,1723,1823,603,1148,1826,35,1559,75,2,14,3,13,10,11,9,12,70,68,69,67,72])).
% 10.09/10.22 cnf(1896,plain,
% 10.09/10.22 (P2(a3,a3,a8)),
% 10.09/10.22 inference(scs_inference,[],[20,22,840,127,1218,1777,1837,1853,1827,1839,1814,1695,1723,1823,603,1148,1826,35,1559,75,2,14,3,13,10,11,9,12,70,68,69,67,72,71])).
% 10.09/10.22 cnf(1909,plain,
% 10.09/10.22 (E(f6(a7,a1),f4(x19091,f5(x19091)))),
% 10.09/10.22 inference(scs_inference,[],[1876,2])).
% 10.09/10.22 cnf(1910,plain,
% 10.09/10.22 (E(a3,f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[127,1889,1876,2,66])).
% 10.09/10.22 cnf(1912,plain,
% 10.09/10.22 (P1(x19121,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(1915,plain,
% 10.09/10.22 (E(x19151,f6(x19151,x19151))),
% 10.09/10.22 inference(rename_variables,[],[75])).
% 10.09/10.22 cnf(1916,plain,
% 10.09/10.22 (P1(x19161,a8,f4(a3,a3))),
% 10.09/10.22 inference(scs_inference,[],[127,973,1894,1889,1823,1876,75,2,66,14,10])).
% 10.09/10.22 cnf(1918,plain,
% 10.09/10.22 (P1(f4(a3,a3),f6(a2,a2),a2)),
% 10.09/10.22 inference(scs_inference,[],[132,127,761,973,1894,1889,1823,1876,1826,75,2,66,14,10,11,9])).
% 10.09/10.22 cnf(1919,plain,
% 10.09/10.22 (E(f6(a7,a1),f6(f6(a3,x19191),x19192))),
% 10.09/10.22 inference(scs_inference,[],[132,127,761,973,1894,1889,1180,1823,1876,1873,1826,75,2,66,14,10,11,9,3])).
% 10.09/10.22 cnf(1921,plain,
% 10.09/10.22 (E(x19211,f6(x19211,x19211))),
% 10.09/10.22 inference(rename_variables,[],[75])).
% 10.09/10.22 cnf(1924,plain,
% 10.09/10.22 (P1(a2,a7,f6(a3,x19241))),
% 10.09/10.22 inference(scs_inference,[],[20,22,132,127,761,973,1894,1889,1880,1180,1823,1876,1873,1826,75,1915,1921,2,66,14,10,11,9,3,13,12,70])).
% 10.09/10.22 cnf(1930,plain,
% 10.09/10.22 (P1(a7,a7,f4(a3,a3))),
% 10.09/10.22 inference(scs_inference,[],[20,22,132,127,761,973,1127,1413,1894,1882,1889,1880,1180,1823,1273,1876,1873,1826,75,1915,1921,2,66,14,10,11,9,3,13,12,70,68,69])).
% 10.09/10.22 cnf(1936,plain,
% 10.09/10.22 (P2(f4(a8,a2),f4(a8,a2),f4(a8,a2))),
% 10.09/10.22 inference(scs_inference,[],[20,22,132,127,761,973,1127,1413,1894,1882,1889,1863,1880,1695,1180,1823,101,1273,1876,1873,1826,51,75,1915,1921,2,66,14,10,11,9,3,13,12,70,68,69,67,72])).
% 10.09/10.22 cnf(1938,plain,
% 10.09/10.22 (P1(x19381,f6(a7,a1),f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[20,22,132,127,1912,761,973,1127,1413,1894,1882,1889,1863,1880,1695,1180,1823,101,1273,1876,1873,1826,51,75,1915,1921,2,66,14,10,11,9,3,13,12,70,68,69,67,72,74])).
% 10.09/10.22 cnf(1940,plain,
% 10.09/10.22 (P2(f6(x19401,a8),f6(x19401,a8),f6(x19401,a8))),
% 10.09/10.22 inference(scs_inference,[],[20,22,132,127,1912,94,761,973,1127,1413,1894,1882,1889,1863,1880,1695,1180,1823,101,1273,1876,1873,1826,51,75,1915,1921,2,66,14,10,11,9,3,13,12,70,68,69,67,72,74,71])).
% 10.09/10.22 cnf(1943,plain,
% 10.09/10.22 (P1(f6(a8,a8),x19431,f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[20,22,132,127,1912,94,761,973,1127,1413,1894,1882,1889,1863,1880,1695,1723,1180,1823,101,1273,1876,1873,1703,1826,51,75,1915,1921,2,66,14,10,11,9,3,13,12,70,68,69,67,72,74,71,73])).
% 10.09/10.22 cnf(1945,plain,
% 10.09/10.22 (E(f6(a7,a7),a3)),
% 10.09/10.22 inference(scs_inference,[],[1910,2])).
% 10.09/10.22 cnf(1946,plain,
% 10.09/10.22 (E(a3,f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[127,1943,1910,2,66])).
% 10.09/10.22 cnf(1947,plain,
% 10.09/10.22 (P1(f6(a8,a8),x19471,f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[1943])).
% 10.09/10.22 cnf(1948,plain,
% 10.09/10.22 (P1(x19481,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(1953,plain,
% 10.09/10.22 (E(f6(a7,a1),f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[132,127,1948,1943,1701,1910,1909,1873,1785,2,66,11,10,14,3])).
% 10.09/10.22 cnf(1957,plain,
% 10.09/10.22 (P1(a1,f6(a7,a1),f6(a7,f6(a7,a1)))),
% 10.09/10.22 inference(scs_inference,[],[20,132,127,1948,761,1218,1943,1701,1938,1910,46,1909,1873,1785,2,66,11,10,14,3,9,13,12,70])).
% 10.09/10.22 cnf(1958,plain,
% 10.09/10.22 (P1(x19581,f6(a7,a1),f6(a7,a1))),
% 10.09/10.22 inference(rename_variables,[],[1938])).
% 10.09/10.22 cnf(1966,plain,
% 10.09/10.22 (P1(f6(a8,a8),x19661,f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[1943])).
% 10.09/10.22 cnf(1967,plain,
% 10.09/10.22 (P1(x19671,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(1974,plain,
% 10.09/10.22 (P2(f4(a3,a3),f4(a3,a3),f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[20,132,309,127,1948,761,1132,1082,1218,1464,1943,1947,1701,1938,1958,1940,1910,46,1099,1141,1909,1873,1785,2,66,11,10,14,3,9,13,12,70,68,69,67,72])).
% 10.09/10.22 cnf(1979,plain,
% 10.09/10.22 (P2(a3,a3,f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[20,132,309,127,1948,1967,761,1132,1082,1218,1464,1943,1947,1966,1701,1938,1958,1940,1910,46,1099,1141,1909,1873,1785,2,66,11,10,14,3,9,13,12,70,68,69,67,72,71])).
% 10.09/10.22 cnf(1982,plain,
% 10.09/10.22 (P1(x19821,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(1984,plain,
% 10.09/10.22 (P1(x19841,a8,a8)),
% 10.09/10.22 inference(scs_inference,[],[20,132,309,127,1948,1967,1982,761,1132,1082,1218,1464,1943,1947,1966,1701,1938,1958,1940,1910,1896,46,1099,1141,1909,1873,1785,2,66,11,10,14,3,9,13,12,70,68,69,67,72,71,74])).
% 10.09/10.22 cnf(1989,plain,
% 10.09/10.22 (E(f6(a8,a8),a3)),
% 10.09/10.22 inference(scs_inference,[],[1946,2])).
% 10.09/10.22 cnf(1990,plain,
% 10.09/10.22 (E(f4(a3,a3),f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[309,1946,1938,2,66])).
% 10.09/10.22 cnf(1992,plain,
% 10.09/10.22 (P1(f4(a3,a3),x19921,f4(a3,a3))),
% 10.09/10.22 inference(rename_variables,[],[309])).
% 10.09/10.22 cnf(1994,plain,
% 10.09/10.22 (E(f4(f4(a3,a3),x19941),x19941)),
% 10.09/10.22 inference(scs_inference,[],[309,1946,1938,603,47,2,66,65])).
% 10.09/10.22 cnf(2008,plain,
% 10.09/10.22 (P2(a3,x20081,f4(f4(x20081,a3),f6(x20082,a3)))),
% 10.09/10.22 inference(scs_inference,[],[309,1992,127,216,1218,1782,1918,1946,1938,1823,603,101,44,47,1919,1945,2,66,65,14,9,3,11,10,13,12,70,68])).
% 10.09/10.22 cnf(2011,plain,
% 10.09/10.22 (P1(a7,a1,a8)),
% 10.09/10.22 inference(scs_inference,[],[20,22,309,1992,127,216,1218,1782,1918,1946,1984,1938,1823,603,101,44,47,1919,1945,2,66,65,14,9,3,11,10,13,12,70,68,69])).
% 10.09/10.22 cnf(2017,plain,
% 10.09/10.22 (P1(x20171,f6(a8,a8),f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[20,22,309,1992,127,216,1218,1782,1918,1946,1984,1979,1938,1823,603,101,44,47,1919,1945,2,66,65,14,9,3,11,10,13,12,70,68,69,67,74])).
% 10.09/10.22 cnf(2019,plain,
% 10.09/10.22 (P2(a3,a3,f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[20,22,309,1992,127,216,1218,1782,1918,1946,1984,1979,1938,1889,1823,603,101,44,47,1919,1945,2,66,65,14,9,3,11,10,13,12,70,68,69,67,74,71])).
% 10.09/10.22 cnf(2028,plain,
% 10.09/10.22 (E(f6(a3,x20281),f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[840,2017,1990,2,66])).
% 10.09/10.22 cnf(2029,plain,
% 10.09/10.22 (P1(x20291,f6(a8,a8),f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[2017])).
% 10.09/10.22 cnf(2030,plain,
% 10.09/10.22 (P1(f4(a3,a3),x20301,f6(a3,x20302))),
% 10.09/10.22 inference(rename_variables,[],[840])).
% 10.09/10.22 cnf(2032,plain,
% 10.09/10.22 (E(f4(a3,x20321),x20321)),
% 10.09/10.22 inference(scs_inference,[],[840,2017,1990,28,47,2,66,65])).
% 10.09/10.22 cnf(2036,plain,
% 10.09/10.22 (P1(f6(a7,a1),x20361,f6(a3,x20362))),
% 10.09/10.22 inference(scs_inference,[],[840,2030,2017,1990,28,47,2,66,65,9])).
% 10.09/10.22 cnf(2038,plain,
% 10.09/10.22 (P1(f4(a3,a3),x20381,f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[840,2030,309,2017,1990,366,28,47,2,66,65,9,3,11])).
% 10.09/10.22 cnf(2043,plain,
% 10.09/10.22 (P1(a1,f6(a8,a8),f6(a7,f6(a8,a8)))),
% 10.09/10.22 inference(scs_inference,[],[20,840,2030,309,385,1464,1974,2017,2029,1990,366,46,28,47,1953,2,66,65,9,3,11,14,10,13,12,70])).
% 10.09/10.22 cnf(2044,plain,
% 10.09/10.22 (P1(x20441,f6(a8,a8),f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[2017])).
% 10.09/10.22 cnf(2049,plain,
% 10.09/10.22 (P2(f6(x20491,a8),f6(x20491,a8),f6(x20491,a8))),
% 10.09/10.22 inference(rename_variables,[],[1940])).
% 10.09/10.22 cnf(2052,plain,
% 10.09/10.22 (P1(x20521,f6(a8,a8),f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[2017])).
% 10.09/10.22 cnf(2059,plain,
% 10.09/10.22 (P2(f6(a3,x20591),f6(a3,x20591),f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[20,840,2030,309,385,1464,1974,1940,2049,2017,2029,2044,2052,1990,366,46,28,47,1108,1141,57,1953,2,66,65,9,3,11,14,10,13,12,70,68,69,67,72])).
% 10.09/10.22 cnf(2067,plain,
% 10.09/10.22 (P1(x20671,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(2069,plain,
% 10.09/10.22 (P2(f6(x20691,a1),f6(x20691,a1),f6(x20691,a1))),
% 10.09/10.22 inference(scs_inference,[],[20,840,2030,309,127,385,1127,1464,1974,1940,2049,2017,2029,2044,2052,1990,1691,366,46,28,47,1108,1141,341,57,1953,2008,2,66,65,9,3,11,14,10,13,12,70,68,69,67,72,73,71])).
% 10.09/10.22 cnf(2071,plain,
% 10.09/10.22 (P1(x20711,f6(a7,a7),f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[20,840,2030,309,127,2067,385,1127,1464,1974,1940,2049,2017,2029,2044,2052,1990,2019,1691,366,46,28,47,1108,1141,341,57,1953,2008,2,66,65,9,3,11,14,10,13,12,70,68,69,67,72,73,71,74])).
% 10.09/10.22 cnf(2074,plain,
% 10.09/10.22 (E(f6(a3,x20741),f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[840,2071,2028,2,66])).
% 10.09/10.22 cnf(2075,plain,
% 10.09/10.22 (P1(x20751,f6(a7,a7),f6(a7,a7))),
% 10.09/10.22 inference(rename_variables,[],[2071])).
% 10.09/10.22 cnf(2076,plain,
% 10.09/10.22 (P1(f4(a3,a3),x20761,f6(a3,x20762))),
% 10.09/10.22 inference(rename_variables,[],[840])).
% 10.09/10.22 cnf(2078,plain,
% 10.09/10.22 (E(f4(x20781,f4(x20781,x20782)),x20782)),
% 10.09/10.22 inference(scs_inference,[],[840,2071,2028,45,47,2,66,65])).
% 10.09/10.22 cnf(2082,plain,
% 10.09/10.22 (E(f6(f4(a3,a3),a7),f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[840,2071,2028,1269,45,47,2,66,65,3])).
% 10.09/10.22 cnf(2083,plain,
% 10.09/10.22 (E(f6(a3,x20831),f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[2028])).
% 10.09/10.22 cnf(2085,plain,
% 10.09/10.22 (P1(f4(a3,a3),x20851,f6(a3,x20852))),
% 10.09/10.22 inference(rename_variables,[],[840])).
% 10.09/10.22 cnf(2087,plain,
% 10.09/10.22 (P2(f4(a3,a3),f4(a3,a3),f6(x20871,a3))),
% 10.09/10.22 inference(rename_variables,[],[1464])).
% 10.09/10.22 cnf(2088,plain,
% 10.09/10.22 (E(f6(a3,x20881),f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[2028])).
% 10.09/10.22 cnf(2091,plain,
% 10.09/10.22 (P1(x20911,f6(a3,x20912),f6(a3,x20912))),
% 10.09/10.22 inference(rename_variables,[],[1132])).
% 10.09/10.22 cnf(2093,plain,
% 10.09/10.22 (P2(f6(a3,x20931),f6(a3,x20931),f6(a3,x20932))),
% 10.09/10.22 inference(rename_variables,[],[1082])).
% 10.09/10.22 cnf(2095,plain,
% 10.09/10.22 (P2(f6(a3,x20951),f6(a3,x20951),f6(a3,x20952))),
% 10.09/10.22 inference(rename_variables,[],[1082])).
% 10.09/10.22 cnf(2097,plain,
% 10.09/10.22 (P1(x20971,f6(a7,a7),f6(a7,a7))),
% 10.09/10.22 inference(rename_variables,[],[2071])).
% 10.09/10.22 cnf(2102,plain,
% 10.09/10.22 (P1(x21021,a3,a3)),
% 10.09/10.22 inference(rename_variables,[],[127])).
% 10.09/10.22 cnf(2111,plain,
% 10.09/10.22 (P2(f6(a3,x21111),f6(a3,x21111),f6(a3,x21112))),
% 10.09/10.22 inference(rename_variables,[],[1082])).
% 10.09/10.22 cnf(2116,plain,
% 10.09/10.22 (P1(f4(a3,a3),x21161,f6(a3,x21162))),
% 10.09/10.22 inference(rename_variables,[],[840])).
% 10.09/10.22 cnf(2123,plain,
% 10.09/10.22 (P2(f6(a3,x21231),f6(a3,x21231),f6(a7,a1))),
% 10.09/10.22 inference(scs_inference,[],[20,840,2076,2085,2116,309,127,2102,1132,2091,1082,2093,2095,2111,1464,2087,2071,2075,2097,2059,2028,2083,2088,1889,1269,1990,46,27,45,47,48,2038,2008,2,66,65,3,11,14,9,10,13,12,70,69,68,67,72,73,71])).
% 10.09/10.22 cnf(2136,plain,
% 10.09/10.22 (P1(f4(a3,a3),x21361,f6(a3,x21362))),
% 10.09/10.22 inference(rename_variables,[],[840])).
% 10.09/10.22 cnf(2139,plain,
% 10.09/10.22 (E(f6(a3,x21391),f6(a7,a7))),
% 10.09/10.22 inference(rename_variables,[],[2074])).
% 10.09/10.22 cnf(2143,plain,
% 10.09/10.22 (E(f6(a3,x21431),f6(a7,a7))),
% 10.09/10.22 inference(rename_variables,[],[2074])).
% 10.09/10.22 cnf(2147,plain,
% 10.09/10.22 (P2(f6(a3,x21471),f6(a3,x21471),f6(x21472,a3))),
% 10.09/10.22 inference(rename_variables,[],[1127])).
% 10.09/10.22 cnf(2150,plain,
% 10.09/10.22 (P1(a7,f4(a3,a3),f6(a3,x21501))),
% 10.09/10.22 inference(scs_inference,[],[840,2136,520,1132,1127,2147,1218,1784,1930,2074,2139,2143,1321,2008,75,2,65,11,9,14,3,10,13,12,70])).
% 10.09/10.22 cnf(2172,plain,
% 10.09/10.22 (E(x21721,f4(f4(a3,a3),x21721))),
% 10.09/10.22 inference(scs_inference,[],[1994,2])).
% 10.09/10.22 cnf(2173,plain,
% 10.09/10.22 (E(f4(a3,a3),f6(a8,a8))),
% 10.09/10.22 inference(scs_inference,[],[309,2017,1994,2,66])).
% 10.09/10.22 cnf(2177,plain,
% 10.09/10.22 (P2(a2,a2,f6(a2,a2))),
% 10.09/10.22 inference(scs_inference,[],[309,1695,2017,1994,75,2,66,14])).
% 10.09/10.22 cnf(2179,plain,
% 10.09/10.22 (E(f6(f4(a3,a3),a7),f6(a7,a7))),
% 10.09/10.22 inference(scs_inference,[],[309,1695,2017,2074,1269,1994,75,2,66,14,3])).
% 10.09/10.22 cnf(2184,plain,
% 10.09/10.22 (E(f6(a3,x21841),f6(a8,a8))),
% 10.09/10.22 inference(rename_variables,[],[2028])).
% 10.09/10.22 cnf(2187,plain,
% 10.09/10.22 (P2(f6(a3,x21871),f6(a3,x21871),f6(x21872,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(2190,plain,
% 10.27/10.22 (P1(a1,f4(a3,a3),f6(a3,x21901))),
% 10.27/10.22 inference(scs_inference,[],[20,309,127,474,973,1127,2187,1695,2017,2150,2028,2184,2074,1269,1827,1990,1994,75,2,66,14,3,11,9,10,13,12,70])).
% 10.27/10.22 cnf(2214,plain,
% 10.27/10.22 (E(f4(f6(x22141,a3),f4(x22142,a3)),x22142)),
% 10.27/10.22 inference(scs_inference,[],[2173,45,1303,2,65])).
% 10.27/10.22 cnf(2215,plain,
% 10.27/10.22 (P2(x22151,x22152,f4(x22151,x22152))),
% 10.27/10.22 inference(rename_variables,[],[45])).
% 10.27/10.22 cnf(2218,plain,
% 10.27/10.22 (E(x22181,f4(f4(a3,a3),x22181))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2220,plain,
% 10.27/10.22 (E(x22201,f4(f4(a3,a3),x22201))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2222,plain,
% 10.27/10.22 (E(x22221,f4(f4(a3,a3),x22221))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2223,plain,
% 10.27/10.22 (E(f6(f4(a3,a3),a8),f6(a8,a8))),
% 10.27/10.22 inference(scs_inference,[],[20,22,1695,2173,2028,1321,45,1303,2172,2218,2220,2,65,11,14,9,3])).
% 10.27/10.22 cnf(2229,plain,
% 10.27/10.22 (P1(a1,a8,f6(a3,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,22,1132,1464,1695,1795,2173,2028,1321,45,1303,2172,2218,2220,2222,2,65,11,14,9,3,10,13,12,70])).
% 10.27/10.22 cnf(2232,plain,
% 10.27/10.22 (P2(a3,x22321,f4(f6(x22322,a3),f4(x22321,a3)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,1132,1218,1464,1695,1795,2173,2028,1321,45,2215,101,1303,2172,2218,2220,2222,2,65,11,14,9,3,10,13,12,70,68])).
% 10.27/10.22 cnf(2252,plain,
% 10.27/10.22 (E(x22521,f4(x22522,f4(x22522,x22521)))),
% 10.27/10.22 inference(scs_inference,[],[2078,2])).
% 10.27/10.22 cnf(2257,plain,
% 10.27/10.22 (E(x22571,f4(f4(a3,a3),x22571))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2261,plain,
% 10.27/10.22 (E(x22611,f4(f4(a3,a3),x22611))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2263,plain,
% 10.27/10.22 (E(x22631,f4(f4(a3,a3),x22631))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2265,plain,
% 10.27/10.22 (E(x22651,f4(f4(a3,a3),x22651))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2267,plain,
% 10.27/10.22 (E(x22671,f4(f4(a3,a3),x22671))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2270,plain,
% 10.27/10.22 (P1(a1,f6(a3,x22701),f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,1218,1695,1936,1924,1930,1910,2078,2232,2172,2257,2261,2263,2265,2267,2,65,9,3,11,10,14,13,12,70])).
% 10.27/10.22 cnf(2274,plain,
% 10.27/10.22 (P1(x22741,a3,a3)),
% 10.27/10.22 inference(rename_variables,[],[127])).
% 10.27/10.22 cnf(2280,plain,
% 10.27/10.22 (P2(x22801,a3,x22801)),
% 10.27/10.22 inference(rename_variables,[],[27])).
% 10.27/10.22 cnf(2287,plain,
% 10.27/10.22 (P1(x22871,a3,a3)),
% 10.27/10.22 inference(rename_variables,[],[127])).
% 10.27/10.22 cnf(2289,plain,
% 10.27/10.22 (P2(f5(a3),f5(a3),f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,127,2274,973,1082,1218,1507,1695,1936,1924,1930,2123,1910,27,2280,28,31,2078,2232,2172,2257,2261,2263,2265,2267,2,65,9,3,11,10,14,13,12,70,69,68,67,73,71])).
% 10.27/10.22 cnf(2292,plain,
% 10.27/10.22 (P1(x22921,f5(a3),f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,127,2274,2287,973,1082,1218,1507,1695,1936,1924,1930,2123,1910,27,2280,28,31,2078,2232,2172,2257,2261,2263,2265,2267,2,65,9,3,11,10,14,13,12,70,69,68,67,73,71,74])).
% 10.27/10.22 cnf(2299,plain,
% 10.27/10.22 (E(x22991,f4(x22992,f4(x22992,x22991)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2301,plain,
% 10.27/10.22 (E(x23011,f4(x23012,f4(x23012,x23011)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2303,plain,
% 10.27/10.22 (E(x23031,f4(x23032,f4(x23032,x23031)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2305,plain,
% 10.27/10.22 (E(x23051,f4(x23052,f4(x23052,x23051)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2309,plain,
% 10.27/10.22 (E(x23091,f4(x23092,f4(x23092,x23091)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2313,plain,
% 10.27/10.22 (P1(x23131,f4(a3,a3),f4(a3,a3))),
% 10.27/10.22 inference(rename_variables,[],[973])).
% 10.27/10.22 cnf(2329,plain,
% 10.27/10.22 (P2(f6(a3,x23291),f6(a3,x23291),f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,127,973,2313,1218,1464,1695,1651,1698,2190,2292,1741,93,1234,1615,2252,2299,2301,2303,2305,2309,2223,2214,2,11,10,14,9,3,13,12,70,67,69,68,72])).
% 10.27/10.22 cnf(2341,plain,
% 10.27/10.22 (E(f4(a3,a3),f6(a7,a7))),
% 10.27/10.22 inference(scs_inference,[],[309,2071,2082,2,66])).
% 10.27/10.22 cnf(2343,plain,
% 10.27/10.22 (P1(f4(a3,a3),x23431,f4(a3,a3))),
% 10.27/10.22 inference(rename_variables,[],[309])).
% 10.27/10.22 cnf(2346,plain,
% 10.27/10.22 (E(x23461,f4(x23462,f4(x23462,x23461)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2348,plain,
% 10.27/10.22 (P2(f6(a8,x23481),f6(a8,x23481),f6(a8,x23481))),
% 10.27/10.22 inference(rename_variables,[],[1699])).
% 10.27/10.22 cnf(2349,plain,
% 10.27/10.22 (E(f6(x23491,a3),f6(a2,a3))),
% 10.27/10.22 inference(rename_variables,[],[1230])).
% 10.27/10.22 cnf(2351,plain,
% 10.27/10.22 (E(x23511,f4(x23512,f4(x23512,x23511)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2352,plain,
% 10.27/10.22 (E(f6(a8,a8),f6(a7,a1))),
% 10.27/10.22 inference(scs_inference,[],[22,132,309,1699,2071,1827,1230,2082,1989,2252,2346,2,66,11,14,9,3])).
% 10.27/10.22 cnf(2363,plain,
% 10.27/10.22 (P2(f6(a3,x23631),f6(a3,x23631),f5(a3))),
% 10.27/10.22 inference(rename_variables,[],[2329])).
% 10.27/10.22 cnf(2366,plain,
% 10.27/10.22 (P1(f6(x23661,a1),x23662,f6(x23661,a1))),
% 10.27/10.22 inference(scs_inference,[],[22,132,309,1082,1880,1723,1699,2348,2019,2071,2043,2329,1827,1230,2349,341,2082,1989,2252,2346,2351,2,66,11,14,9,3,10,13,12,70,67,69])).
% 10.27/10.22 cnf(2377,plain,
% 10.27/10.22 (P2(a7,a7,f6(a1,a1))),
% 10.27/10.22 inference(scs_inference,[],[22,132,309,79,474,1082,1218,1695,1880,1723,1699,2348,2019,2071,2043,2329,2363,1827,1230,2349,26,1234,341,2082,1989,2252,2346,2351,2,66,11,14,9,3,10,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(2379,plain,
% 10.27/10.22 (P2(f4(a3,a3),f4(a3,a3),f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[22,132,309,2343,79,474,1082,1464,1218,1695,1880,1723,1699,2348,2019,2071,2043,2329,2363,2292,1827,1230,2349,26,1234,341,2082,1989,2252,2346,2351,2,66,11,14,9,3,10,13,12,70,67,69,68,73,71,72])).
% 10.27/10.22 cnf(2388,plain,
% 10.27/10.22 (E(a7,f6(a1,a1))),
% 10.27/10.22 inference(scs_inference,[],[79,2341,2366,2,66])).
% 10.27/10.22 cnf(2389,plain,
% 10.27/10.22 (P1(f6(x23891,a1),x23892,f6(x23891,a1))),
% 10.27/10.22 inference(rename_variables,[],[2366])).
% 10.27/10.22 cnf(2393,plain,
% 10.27/10.22 (E(x23931,f4(f4(a3,a3),x23931))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2395,plain,
% 10.27/10.22 (E(x23951,f4(f4(a3,a3),x23951))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2414,plain,
% 10.27/10.22 (P1(f5(a3),x24141,f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[22,132,309,79,127,1082,1464,1880,1737,1694,1957,2341,2366,2389,2379,2377,1946,379,1303,1094,2032,2172,2393,2395,2,66,11,14,10,9,3,13,12,70,67,69,68,73])).
% 10.27/10.22 cnf(2427,plain,
% 10.27/10.22 (E(f6(a1,a1),a7)),
% 10.27/10.22 inference(scs_inference,[],[2388,2])).
% 10.27/10.22 cnf(2428,plain,
% 10.27/10.22 (E(f4(a3,a3),f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[309,2388,2292,2,66])).
% 10.27/10.22 cnf(2430,plain,
% 10.27/10.22 (P1(f4(a3,a3),x24301,f4(a3,a3))),
% 10.27/10.22 inference(rename_variables,[],[309])).
% 10.27/10.22 cnf(2432,plain,
% 10.27/10.22 (E(f4(f4(x24321,a3),f6(x24322,a3)),x24321)),
% 10.27/10.22 inference(scs_inference,[],[309,2388,2292,44,1303,2,66,65])).
% 10.27/10.22 cnf(2436,plain,
% 10.27/10.22 (E(x24361,f4(x24362,f4(x24362,x24361)))),
% 10.27/10.22 inference(rename_variables,[],[2252])).
% 10.27/10.22 cnf(2442,plain,
% 10.27/10.22 (P1(f6(a8,a8),x24421,f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,132,309,2430,1896,2388,2292,2173,44,1303,1994,2252,2436,2,66,65,14,3,10,11,9])).
% 10.27/10.22 cnf(2481,plain,
% 10.27/10.22 (E(f5(a3),f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[2428,2])).
% 10.27/10.22 cnf(2483,plain,
% 10.27/10.22 (E(x24831,f4(f4(a3,a3),x24831))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2492,plain,
% 10.27/10.22 (P1(a1,f4(a3,a3),f6(x24921,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,555,309,1223,1464,1896,1597,2428,2388,2432,2172,2483,2,14,11,3,10,9,13,12,70])).
% 10.27/10.22 cnf(2494,plain,
% 10.27/10.22 (P1(x24941,f6(x24942,a3),f6(x24942,a3))),
% 10.27/10.22 inference(rename_variables,[],[1223])).
% 10.27/10.22 cnf(2509,plain,
% 10.27/10.22 (P2(x25091,x25091,a3)),
% 10.27/10.22 inference(rename_variables,[],[26])).
% 10.27/10.22 cnf(2511,plain,
% 10.27/10.22 (P1(f6(x25111,a8),a1,f6(x25111,a8))),
% 10.27/10.22 inference(rename_variables,[],[520])).
% 10.27/10.22 cnf(2513,plain,
% 10.27/10.22 (P2(f6(a8,a8),f6(a8,a8),f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,555,309,520,2511,127,1223,2494,1127,1464,1507,1896,1597,1940,1698,2442,2428,2388,26,2509,1148,1659,2432,2172,2483,2,14,11,3,10,9,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(2530,plain,
% 10.27/10.22 (E(f6(a8,a8),f6(f6(a3,x25301),x25302))),
% 10.27/10.22 inference(scs_inference,[],[1464,2289,1180,44,2352,2481,1989,2,65,14,3])).
% 10.27/10.22 cnf(2536,plain,
% 10.27/10.22 (P1(f6(a7,a7),x25361,f6(a3,x25362))),
% 10.27/10.22 inference(scs_inference,[],[79,840,520,1464,2289,2341,2028,1180,44,2352,2481,1989,2252,2,65,14,3,11,10,9])).
% 10.27/10.22 cnf(2569,plain,
% 10.27/10.22 (E(x25691,f4(f4(a3,a3),x25691))),
% 10.27/10.22 inference(rename_variables,[],[2172])).
% 10.27/10.22 cnf(2572,plain,
% 10.27/10.22 (P1(f6(x25721,a7),a2,f6(x25721,a7))),
% 10.27/10.22 inference(rename_variables,[],[474])).
% 10.27/10.22 cnf(2573,plain,
% 10.27/10.22 (E(f6(a3,x25731),f6(a7,a7))),
% 10.27/10.22 inference(rename_variables,[],[2074])).
% 10.27/10.22 cnf(2578,plain,
% 10.27/10.22 (P2(f6(a3,x25781),f6(a3,x25781),f6(a3,x25782))),
% 10.27/10.22 inference(rename_variables,[],[1082])).
% 10.27/10.22 cnf(2581,plain,
% 10.27/10.22 (P1(a2,f6(a3,a2),f6(a3,x25811))),
% 10.27/10.22 inference(scs_inference,[],[22,79,840,474,1082,2578,1880,1777,2229,2173,2074,2573,1741,2179,1945,2172,2569,2,14,3,11,10,9,13,12,70])).
% 10.27/10.22 cnf(2592,plain,
% 10.27/10.22 (P2(x25921,x25922,f4(x25921,x25922))),
% 10.27/10.22 inference(rename_variables,[],[45])).
% 10.27/10.22 cnf(2594,plain,
% 10.27/10.22 (P1(f6(x25941,a3),x25942,f4(f4(a3,a3),f4(a3,a3)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,309,79,840,474,1464,1082,2578,1880,1777,2229,2379,2173,2074,2573,1741,603,27,45,2592,1916,2179,1945,2172,2569,2,14,3,11,10,9,13,12,70,67,69,68,73])).
% 10.27/10.22 cnf(2597,plain,
% 10.27/10.22 (P2(f6(a7,a7),f6(a7,a7),f6(a3,x25971))),
% 10.27/10.22 inference(scs_inference,[],[20,22,309,79,840,474,2572,1464,1082,2578,1695,1880,1777,2229,2536,2379,2173,2074,2573,1741,603,27,45,2592,1916,2179,1945,2172,2569,2,14,3,11,10,9,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(2610,plain,
% 10.27/10.22 (E(f4(x26101,f4(x26102,x26101)),x26102)),
% 10.27/10.22 inference(scs_inference,[],[44,48,2530,2,65])).
% 10.27/10.22 cnf(2617,plain,
% 10.27/10.22 (P1(f6(a7,a7),x26171,f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[309,474,2513,2341,44,48,2530,2252,2,65,14,10,9])).
% 10.27/10.22 cnf(2618,plain,
% 10.27/10.22 (E(f4(f6(x26181,a3),f4(a3,a3)),f6(a8,a8))),
% 10.27/10.22 inference(scs_inference,[],[309,474,2513,2341,1946,44,48,2530,2214,2252,2,65,14,10,9,3])).
% 10.27/10.22 cnf(2620,plain,
% 10.27/10.22 (P1(f6(x26201,a3),x26202,f6(a8,a8))),
% 10.27/10.22 inference(scs_inference,[],[309,474,1528,2513,2341,2028,1946,44,48,2530,2214,2252,2,65,14,10,9,3,11])).
% 10.27/10.22 cnf(2650,plain,
% 10.27/10.22 (E(x26501,f4(x26502,f4(x26501,x26502)))),
% 10.27/10.22 inference(scs_inference,[],[2610,2])).
% 10.27/10.22 cnf(2651,plain,
% 10.27/10.22 (E(f6(a7,a1),f6(a3,x26511))),
% 10.27/10.22 inference(scs_inference,[],[94,2036,2610,2,66])).
% 10.27/10.22 cnf(2653,plain,
% 10.27/10.22 (P1(f6(x26531,x26532),f6(a2,x26532),f6(x26531,x26532))),
% 10.27/10.22 inference(rename_variables,[],[94])).
% 10.27/10.22 cnf(2658,plain,
% 10.27/10.22 (E(f4(x26581,f4(a7,x26581)),f6(a1,a1))),
% 10.27/10.22 inference(scs_inference,[],[309,840,94,2036,2513,2428,2388,2610,2,66,9,11,14,3])).
% 10.27/10.22 cnf(2675,plain,
% 10.27/10.22 (P2(a3,a3,f6(x26751,a3))),
% 10.27/10.22 inference(rename_variables,[],[1218])).
% 10.27/10.22 cnf(2683,plain,
% 10.27/10.22 (P2(f6(x26831,a3),f6(x26831,a3),f6(a3,x26832))),
% 10.27/10.22 inference(scs_inference,[],[20,132,309,840,474,761,94,2653,127,1528,2036,1132,1218,2675,1464,1082,1737,1880,2513,2581,1413,2428,2388,47,44,2232,2610,2172,2,66,9,11,14,3,10,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(2695,plain,
% 10.27/10.22 (E(f6(a1,a1),f4(x26951,f4(a7,x26951)))),
% 10.27/10.22 inference(scs_inference,[],[2658,2])).
% 10.27/10.22 cnf(2696,plain,
% 10.27/10.22 (E(a2,a8)),
% 10.27/10.22 inference(scs_inference,[],[761,1723,2658,2,66])).
% 10.27/10.22 cnf(2700,plain,
% 10.27/10.22 (P2(x27001,x27001,f4(f6(x27002,x27002),f6(x27002,x27002)))),
% 10.27/10.22 inference(rename_variables,[],[93])).
% 10.27/10.22 cnf(2703,plain,
% 10.27/10.22 (E(x27031,f4(x27032,f4(x27031,x27032)))),
% 10.27/10.22 inference(rename_variables,[],[2650])).
% 10.27/10.22 cnf(2707,plain,
% 10.27/10.22 (E(x27071,f4(x27072,f4(x27071,x27072)))),
% 10.27/10.22 inference(rename_variables,[],[2650])).
% 10.27/10.22 cnf(2709,plain,
% 10.27/10.22 (E(x27091,f4(x27092,f4(x27091,x27092)))),
% 10.27/10.22 inference(rename_variables,[],[2650])).
% 10.27/10.22 cnf(2711,plain,
% 10.27/10.22 (E(x27111,f4(x27112,f4(x27111,x27112)))),
% 10.27/10.22 inference(rename_variables,[],[2650])).
% 10.27/10.22 cnf(2713,plain,
% 10.27/10.22 (E(x27131,f4(x27132,f4(x27131,x27132)))),
% 10.27/10.22 inference(rename_variables,[],[2650])).
% 10.27/10.22 cnf(2716,plain,
% 10.27/10.22 (P1(a2,f4(a3,a3),f6(a3,x27161))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1132,1723,2270,1741,93,2650,2703,2707,2709,2711,2713,2658,2432,2,66,65,14,3,10,11,9,13,12,70])).
% 10.27/10.22 cnf(2730,plain,
% 10.27/10.22 (P1(a2,a1,f4(f6(x27301,x27301),f6(x27301,x27301)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1132,1723,2270,1741,93,2700,27,249,47,29,52,2650,2703,2707,2709,2711,2713,2658,2432,2,66,65,14,3,10,11,9,13,12,70,67,69,68,73])).
% 10.27/10.22 cnf(2731,plain,
% 10.27/10.22 (P2(x27311,x27311,f4(f6(x27312,x27312),f6(x27312,x27312)))),
% 10.27/10.22 inference(rename_variables,[],[93])).
% 10.27/10.22 cnf(2733,plain,
% 10.27/10.22 (P2(f6(a7,a1),f6(a7,a1),f6(a3,x27331))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,94,2036,1695,1132,1723,2069,2270,1741,93,2700,27,249,47,29,52,2650,2703,2707,2709,2711,2713,2658,2432,2,66,65,14,3,10,11,9,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(2739,plain,
% 10.27/10.22 (P1(a1,a2,f4(f6(x27391,x27391),f6(x27391,x27391)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,94,2036,1695,1132,1723,2069,2270,1741,93,2700,2731,27,249,47,29,52,2650,2703,2707,2709,2711,2713,2658,2432,2,66,65,14,3,10,11,9,13,12,70,67,69,68,73,71,74])).
% 10.27/10.22 cnf(2745,plain,
% 10.27/10.22 (E(a8,a2)),
% 10.27/10.22 inference(scs_inference,[],[2696,2])).
% 10.27/10.22 cnf(2746,plain,
% 10.27/10.22 (E(a2,f6(a3,x27461))),
% 10.27/10.22 inference(scs_inference,[],[761,1880,2696,2,66])).
% 10.27/10.22 cnf(2747,plain,
% 10.27/10.22 (P1(a8,x27471,f6(a3,x27472))),
% 10.27/10.22 inference(rename_variables,[],[1880])).
% 10.27/10.22 cnf(2749,plain,
% 10.27/10.22 (E(a2,f4(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[761,1695,1880,2696,45,2,66,65])).
% 10.27/10.22 cnf(2750,plain,
% 10.27/10.22 (P2(x27501,x27502,f4(x27501,x27502))),
% 10.27/10.22 inference(rename_variables,[],[45])).
% 10.27/10.22 cnf(2756,plain,
% 10.27/10.22 (E(x27561,f4(x27562,f4(x27561,x27562)))),
% 10.27/10.22 inference(rename_variables,[],[2650])).
% 10.27/10.22 cnf(2763,plain,
% 10.27/10.22 (P1(a8,x27631,f6(a3,x27632))),
% 10.27/10.22 inference(rename_variables,[],[1880])).
% 10.27/10.22 cnf(2772,plain,
% 10.27/10.22 (P2(a2,x27721,f4(a2,f4(a2,x27721)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,1528,761,1695,1880,2747,2069,1716,2733,2696,2594,45,2750,47,2650,2756,2032,2,66,65,3,10,11,14,9,13,12,70,67,69,68])).
% 10.27/10.22 cnf(2774,plain,
% 10.27/10.22 (P2(x27741,x27742,f4(x27741,x27742))),
% 10.27/10.22 inference(rename_variables,[],[45])).
% 10.27/10.22 cnf(2776,plain,
% 10.27/10.22 (P1(a2,a1,f4(a8,a8))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,1528,761,1695,1880,2747,2069,1716,2733,2696,2594,45,2750,2774,47,2650,2756,2032,2,66,65,3,10,11,14,9,13,12,70,67,69,68,73])).
% 10.27/10.22 cnf(2777,plain,
% 10.27/10.22 (P2(x27771,x27772,f4(x27771,x27772))),
% 10.27/10.22 inference(rename_variables,[],[45])).
% 10.27/10.22 cnf(2779,plain,
% 10.27/10.22 (P2(a2,a2,f6(a3,x27791))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,1528,761,1695,1880,2747,2763,1814,2069,1716,2733,2696,2594,45,2750,2774,47,2650,2756,2032,2,66,65,3,10,11,14,9,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(2783,plain,
% 10.27/10.22 (P1(a1,a2,f4(a7,a7))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,1528,761,1695,1880,2747,2763,1814,2069,1716,2733,2696,2594,45,2750,2774,2777,47,2650,2756,2032,2,66,65,3,10,11,14,9,13,12,70,67,69,68,73,71,74])).
% 10.27/10.22 cnf(2790,plain,
% 10.27/10.22 (E(a2,f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[761,2746,1837,2,66])).
% 10.27/10.22 cnf(2793,plain,
% 10.27/10.22 (E(a2,a3)),
% 10.27/10.22 inference(scs_inference,[],[761,1695,2746,1837,26,2,66,65])).
% 10.27/10.22 cnf(2794,plain,
% 10.27/10.22 (P2(x27941,x27941,a3)),
% 10.27/10.22 inference(rename_variables,[],[26])).
% 10.27/10.22 cnf(2797,plain,
% 10.27/10.22 (P2(a3,a3,a2)),
% 10.27/10.22 inference(scs_inference,[],[20,761,1695,1896,2746,1837,26,2745,2,66,65,10,14])).
% 10.27/10.22 cnf(2799,plain,
% 10.27/10.22 (E(a8,f6(a3,x27991))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1896,2746,1837,26,2745,2,66,65,10,14,11,3])).
% 10.27/10.22 cnf(2803,plain,
% 10.27/10.22 (P1(a2,f6(a3,x28031),a8)),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1896,1723,2190,2746,1837,26,2745,2,66,65,10,14,11,3,9,13,12,70])).
% 10.27/10.22 cnf(2806,plain,
% 10.27/10.22 (P2(f6(a3,x28061),a2,f6(a3,x28061))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1896,1723,2190,2746,2779,1837,26,2745,2,66,65,10,14,11,3,9,13,12,70,67])).
% 10.27/10.22 cnf(2808,plain,
% 10.27/10.22 (P1(f4(a7,a7),f6(a2,a2),f4(a7,a7))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1896,1723,2190,843,2746,2783,2779,1837,26,2745,2,66,65,10,14,11,3,9,13,12,70,67,69])).
% 10.27/10.22 cnf(2811,plain,
% 10.27/10.22 (P2(x28111,x28111,a3)),
% 10.27/10.22 inference(rename_variables,[],[26])).
% 10.27/10.22 cnf(2820,plain,
% 10.27/10.22 (P2(f4(a3,a3),a7,f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1896,1723,973,2190,843,1597,2716,2746,2783,2779,2776,1837,26,2794,1303,2745,2,66,65,10,14,11,3,9,13,12,70,67,69,68,72,73,71])).
% 10.27/10.22 cnf(2823,plain,
% 10.27/10.22 (P1(a1,a2,a3)),
% 10.27/10.22 inference(scs_inference,[],[20,22,761,1695,1896,1723,973,2190,843,1597,2716,2746,2783,2779,2776,1837,26,2794,2811,1303,2745,2,66,65,10,14,11,3,9,13,12,70,67,69,68,72,73,71,74])).
% 10.27/10.22 cnf(2827,plain,
% 10.27/10.22 (E(f6(a3,x28271),f4(f4(a3,a3),f4(a3,a3)))),
% 10.27/10.22 inference(scs_inference,[],[1789,2790,2594,2,66])).
% 10.27/10.22 cnf(2831,plain,
% 10.27/10.22 (E(f4(f6(x28311,x28311),x28311),a3)),
% 10.27/10.22 inference(scs_inference,[],[1789,2790,2594,45,91,2,66,65])).
% 10.27/10.22 cnf(2842,plain,
% 10.27/10.22 (P1(a2,f6(x28421,a3),a8)),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,1789,761,1695,1979,1723,2492,2790,2594,2173,1827,45,91,2799,2,66,65,14,3,11,10,9,13,12,70])).
% 10.27/10.22 cnf(2869,plain,
% 10.27/10.22 (E(f6(a7,a1),f4(f4(a3,a3),f4(a3,a3)))),
% 10.27/10.22 inference(scs_inference,[],[2651,2827,2618,2,3])).
% 10.27/10.22 cnf(2870,plain,
% 10.27/10.22 (E(f6(a3,x28701),f4(f4(a3,a3),f4(a3,a3)))),
% 10.27/10.22 inference(rename_variables,[],[2827])).
% 10.27/10.22 cnf(2876,plain,
% 10.27/10.22 (P2(f6(a3,x28761),f6(a3,x28761),f6(x28762,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(2877,plain,
% 10.27/10.22 (E(f6(a3,x28771),f4(f4(a3,a3),f4(a3,a3)))),
% 10.27/10.22 inference(rename_variables,[],[2827])).
% 10.27/10.22 cnf(2880,plain,
% 10.27/10.22 (E(f6(a3,x28801),f4(f4(a3,a3),f4(a3,a3)))),
% 10.27/10.22 inference(rename_variables,[],[2827])).
% 10.27/10.22 cnf(2882,plain,
% 10.27/10.22 (P2(f6(a3,x28821),f6(a3,x28821),f6(x28822,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(2884,plain,
% 10.27/10.22 (P2(f6(a3,x28841),f6(a3,x28841),f6(x28842,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(2887,plain,
% 10.27/10.22 (P1(a2,f6(a3,x28871),f6(a3,x28872))),
% 10.27/10.22 inference(scs_inference,[],[22,840,1528,1127,2876,2882,1880,2190,1974,2651,2827,2870,2877,2880,2820,2618,2650,2,3,11,10,14,9,13,12,67,70])).
% 10.27/10.22 cnf(2899,plain,
% 10.27/10.22 (P1(x28991,a3,a3)),
% 10.27/10.22 inference(rename_variables,[],[127])).
% 10.27/10.22 cnf(2904,plain,
% 10.27/10.22 (P1(x29041,a2,a2)),
% 10.27/10.22 inference(scs_inference,[],[22,840,1528,127,2899,1464,1127,2876,2882,2884,1880,2190,1974,1814,2808,2651,2827,2870,2877,2880,2776,2820,45,29,2618,2797,2650,2,3,11,10,14,9,13,12,67,70,69,68,73,71,74])).
% 10.27/10.22 cnf(2906,plain,
% 10.27/10.22 (E(a7,a2)),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,1528,127,2899,1464,1127,2876,2882,2884,1880,2190,1974,1814,2808,2651,2827,2870,2877,2880,2776,2820,45,29,2618,2797,2650,2,3,11,10,14,9,13,12,67,70,69,68,73,71,74,66])).
% 10.27/10.22 cnf(2912,plain,
% 10.27/10.22 (E(f6(a1,a1),a2)),
% 10.27/10.22 inference(scs_inference,[],[2906,2427,2,3])).
% 10.27/10.22 cnf(2920,plain,
% 10.27/10.22 (P2(f6(a3,x29201),f6(a3,x29201),f6(a3,x29202))),
% 10.27/10.22 inference(rename_variables,[],[1082])).
% 10.27/10.22 cnf(2923,plain,
% 10.27/10.22 (P1(a2,f4(a7,a7),a8)),
% 10.27/10.22 inference(scs_inference,[],[22,132,555,1723,1082,2920,2597,2783,2906,2827,2427,2650,2,3,14,10,11,9,13,12,70])).
% 10.27/10.22 cnf(2935,plain,
% 10.27/10.22 (P2(a7,a7,a2)),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,555,1789,1723,1082,2920,2597,1853,648,2783,2904,2906,2827,2820,93,978,1101,2427,2650,2,3,14,10,11,9,13,12,70,67,69,68,72])).
% 10.27/10.22 cnf(2936,plain,
% 10.27/10.22 (P1(x29361,a2,a2)),
% 10.27/10.22 inference(rename_variables,[],[2904])).
% 10.27/10.22 cnf(2939,plain,
% 10.27/10.22 (P2(f6(a7,a7),f6(a7,a7),f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,555,1789,474,1695,1723,1082,2920,2597,1853,648,2617,2783,2904,2906,2827,2820,93,978,1101,2427,2650,2,3,14,10,11,9,13,12,70,67,69,68,72,71])).
% 10.27/10.22 cnf(2944,plain,
% 10.27/10.22 (P1(x29441,f6(a2,a2),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,555,1789,474,1695,1723,1082,2920,2597,1853,648,2617,2783,2904,2936,2906,2827,2820,93,978,1101,2427,2177,2650,2,3,14,10,11,9,13,12,70,67,69,68,72,71,74])).
% 10.27/10.22 cnf(2946,plain,
% 10.27/10.22 (E(f4(a3,a3),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,309,555,1789,474,1695,1723,1082,2920,2597,1853,648,2617,2783,2904,2936,2906,2827,2820,93,978,1101,2427,2177,2650,2,3,14,10,11,9,13,12,70,67,69,68,72,71,74,66])).
% 10.27/10.22 cnf(2952,plain,
% 10.27/10.22 (E(f6(a2,a2),f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[2946,2])).
% 10.27/10.22 cnf(2957,plain,
% 10.27/10.22 (P1(f6(a2,a2),x29571,f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[309,79,2377,2946,2906,2790,2695,2,3,10,11,14,9])).
% 10.27/10.22 cnf(2968,plain,
% 10.27/10.22 (P1(x29681,f6(a2,a2),f6(a2,a2))),
% 10.27/10.22 inference(rename_variables,[],[2944])).
% 10.27/10.22 cnf(2974,plain,
% 10.27/10.22 (P2(f4(a3,a3),f4(a3,a3),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,309,79,1132,1464,2377,1698,2944,2968,2946,2939,2887,2906,2790,603,46,2695,2,3,10,11,14,9,13,12,70,67,69,68,72])).
% 10.27/10.22 cnf(2979,plain,
% 10.27/10.22 (P2(a2,a7,a2)),
% 10.27/10.22 inference(scs_inference,[],[20,309,79,1132,1464,1695,2377,1698,2944,2968,2946,2939,2887,2904,2906,2790,603,46,2695,2,3,10,11,14,9,13,12,70,67,69,68,72,71])).
% 10.27/10.22 cnf(3009,plain,
% 10.27/10.22 (P1(f6(a2,a2),x30091,f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,309,840,555,1789,127,1223,1737,2414,2513,2974,2923,2935,2979,2820,2827,2946,2906,2341,2790,46,2952,2869,2,11,3,14,10,9,13,12,70,67,69,68,73])).
% 10.27/10.22 cnf(3011,plain,
% 10.27/10.22 (P2(a8,a8,f4(a3,a3))),
% 10.27/10.22 inference(scs_inference,[],[20,132,309,840,555,1789,127,1223,1737,2414,2513,2957,2974,2923,2935,2979,2820,2827,2946,2906,2341,2790,93,46,2952,2869,2,11,3,14,10,9,13,12,70,67,69,68,73,71])).
% 10.27/10.22 cnf(3018,plain,
% 10.27/10.22 (E(a8,f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,132,309,840,555,1789,127,1695,1223,1737,2414,2513,2957,2974,2923,2935,2979,2823,2820,2827,2946,2906,2341,2790,93,46,2232,2952,2869,2,11,3,14,10,9,13,12,70,67,69,68,73,71,74,66])).
% 10.27/10.22 cnf(3020,plain,
% 10.27/10.22 (P2(f6(a3,x30201),f6(a3,x30201),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,132,309,840,555,1789,127,1695,1464,1223,1737,2414,2513,2957,2974,2923,2935,2979,2944,2823,2820,2827,2946,2906,2341,2790,93,46,2232,2952,2869,2,11,3,14,10,9,13,12,70,67,69,68,73,71,74,66,72])).
% 10.27/10.22 cnf(3025,plain,
% 10.27/10.22 (E(f6(a2,a2),a8)),
% 10.27/10.22 inference(scs_inference,[],[3018,2])).
% 10.27/10.22 cnf(3029,plain,
% 10.27/10.22 (P1(a2,a2,a7)),
% 10.27/10.22 inference(scs_inference,[],[22,79,1896,3018,2696,2912,2,14,11,10,9])).
% 10.27/10.22 cnf(3050,plain,
% 10.27/10.22 (P1(a1,a2,f4(a2,f4(a2,a7)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,132,79,1695,1218,1127,1863,1896,2011,2683,3009,3020,3018,2730,2904,2696,2906,1910,1234,2232,2772,2912,1833,2,14,11,10,9,3,13,12,70,67,69,68,73,74])).
% 10.27/10.22 cnf(3062,plain,
% 10.27/10.22 (E(f6(a3,x30621),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[840,2944,2749,2,66])).
% 10.27/10.22 cnf(3064,plain,
% 10.27/10.22 (P1(f4(a3,a3),x30641,f6(a3,x30642))),
% 10.27/10.22 inference(rename_variables,[],[840])).
% 10.27/10.22 cnf(3081,plain,
% 10.27/10.22 (P1(f4(a3,a3),x30811,f6(a3,x30812))),
% 10.27/10.22 inference(rename_variables,[],[840])).
% 10.27/10.22 cnf(3087,plain,
% 10.27/10.22 (P2(f6(a3,x30871),f6(a3,x30871),f6(f6(x30872,a3),x30873))),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,3064,3081,555,2036,883,1464,1723,2019,2289,1691,2944,3011,2739,2827,2173,2746,2906,1741,45,26,61,2038,2749,328,3025,2,66,3,10,9,14,11,13,12,70,67,69,68,72])).
% 10.27/10.22 cnf(3109,plain,
% 10.27/10.22 (E(f6(a7,a1),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[79,1723,2597,3062,2651,3018,2746,2,14,10,9,3])).
% 10.27/10.22 cnf(3110,plain,
% 10.27/10.22 (E(f6(a3,x31101),f6(a2,a2))),
% 10.27/10.22 inference(rename_variables,[],[3062])).
% 10.27/10.22 cnf(3111,plain,
% 10.27/10.22 (P1(f6(x31111,a3),x31112,f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[79,1528,1723,2597,3062,3110,2651,3018,2746,2,14,10,9,3,11])).
% 10.27/10.22 cnf(3145,plain,
% 10.27/10.22 (E(a3,f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[127,3009,3109,2,66])).
% 10.27/10.22 cnf(3185,plain,
% 10.27/10.22 (E(f6(a2,a2),a3)),
% 10.27/10.22 inference(scs_inference,[],[3145,2])).
% 10.27/10.22 cnf(3186,plain,
% 10.27/10.22 (E(f6(x31861,a3),f6(a8,a8))),
% 10.27/10.22 inference(scs_inference,[],[1507,3145,2620,2,66])).
% 10.27/10.22 cnf(3226,plain,
% 10.27/10.22 (E(f6(x32261,a3),f6(a8,a8))),
% 10.27/10.22 inference(rename_variables,[],[3186])).
% 10.27/10.22 cnf(3228,plain,
% 10.27/10.22 (P1(f6(a8,a8),x32281,f6(x32282,a3))),
% 10.27/10.22 inference(scs_inference,[],[555,1507,2597,3186,3226,1990,2790,3185,2,10,14,3,9])).
% 10.27/10.22 cnf(3237,plain,
% 10.27/10.22 (P1(x32371,f6(a3,x32372),f6(a3,x32372))),
% 10.27/10.22 inference(rename_variables,[],[1132])).
% 10.27/10.22 cnf(3241,plain,
% 10.27/10.22 (P2(x32411,x32412,f4(x32411,x32412))),
% 10.27/10.22 inference(rename_variables,[],[45])).
% 10.27/10.22 cnf(3253,plain,
% 10.27/10.22 (P2(a3,a7,a3)),
% 10.27/10.22 inference(scs_inference,[],[20,555,1695,1789,1507,1127,127,1132,3237,2377,1863,2597,2803,3009,3186,3226,3145,1990,2388,2790,45,3241,47,1303,1010,2806,3185,2,10,14,3,9,11,13,12,70,67,69,68,71])).
% 10.27/10.22 cnf(3268,plain,
% 10.27/10.22 (P2(a2,a2,f6(a3,x32681))),
% 10.27/10.22 inference(rename_variables,[],[2779])).
% 10.27/10.22 cnf(3269,plain,
% 10.27/10.22 (E(f6(x32691,a3),f6(a8,a8))),
% 10.27/10.22 inference(rename_variables,[],[3186])).
% 10.27/10.22 cnf(3280,plain,
% 10.27/10.22 (P1(x32801,f6(x32802,a3),f6(x32802,a3))),
% 10.27/10.22 inference(rename_variables,[],[1223])).
% 10.27/10.22 cnf(3295,plain,
% 10.27/10.22 (P1(f6(x32951,a8),a1,f6(x32951,a8))),
% 10.27/10.22 inference(rename_variables,[],[520])).
% 10.27/10.22 cnf(3298,plain,
% 10.27/10.22 (E(f6(a8,a8),f4(f6(x32981,x32981),f6(x32981,x32981)))),
% 10.27/10.22 inference(scs_inference,[],[20,2036,474,520,3295,127,1223,3280,2377,1810,1979,2779,3268,2842,2979,3009,3253,3228,3186,3269,2696,2906,1180,93,44,2772,2793,2,65,10,14,3,9,11,13,12,70,67,69,68,71,66])).
% 10.27/10.22 cnf(3318,plain,
% 10.27/10.22 (E(f4(f6(x33181,x33181),x33181),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[474,2733,3298,3186,3145,2746,2831,2,10,14,3])).
% 10.27/10.22 cnf(3342,plain,
% 10.27/10.22 (E(f6(a2,a2),f4(f6(x33421,x33421),x33421))),
% 10.27/10.22 inference(scs_inference,[],[3318,2])).
% 10.27/10.22 cnf(3343,plain,
% 10.27/10.22 (E(f6(x33431,a3),f5(a3))),
% 10.27/10.22 inference(scs_inference,[],[1223,2414,3318,2,66])).
% 10.27/10.22 cnf(3352,plain,
% 10.27/10.22 (E(f6(a2,a2),f6(a8,a8))),
% 10.27/10.22 inference(scs_inference,[],[1063,1223,2414,2683,3186,1946,3318,3185,2650,2,66,10,14,3])).
% 10.27/10.22 cnf(3386,plain,
% 10.27/10.22 (E(f6(x33861,a3),f6(a2,a2))),
% 10.27/10.22 inference(scs_inference,[],[1507,3111,3352,2,66])).
% 10.27/10.22 cnf(3391,plain,
% 10.27/10.22 (E(f6(x33911,a3),f5(a3))),
% 10.27/10.22 inference(rename_variables,[],[3343])).
% 10.27/10.22 cnf(3394,plain,
% 10.27/10.22 (P1(f6(x33941,a3),x33942,f6(x33941,a3))),
% 10.27/10.22 inference(rename_variables,[],[1507])).
% 10.27/10.22 cnf(3397,plain,
% 10.27/10.22 (E(f6(x33971,a3),f5(a3))),
% 10.27/10.22 inference(rename_variables,[],[3343])).
% 10.27/10.22 cnf(3399,plain,
% 10.27/10.22 (P1(f6(x33991,a3),x33992,f6(x33991,a3))),
% 10.27/10.22 inference(rename_variables,[],[1507])).
% 10.27/10.22 cnf(3401,plain,
% 10.27/10.22 (P2(f6(a3,x34011),f6(a3,x34011),f6(a3,x34012))),
% 10.27/10.22 inference(rename_variables,[],[1082])).
% 10.27/10.22 cnf(3402,plain,
% 10.27/10.22 (E(f6(x34021,a3),f5(a3))),
% 10.27/10.22 inference(rename_variables,[],[3343])).
% 10.27/10.22 cnf(3404,plain,
% 10.27/10.22 (P2(f6(a3,x34041),f6(a3,x34041),f6(a3,x34042))),
% 10.27/10.22 inference(rename_variables,[],[1082])).
% 10.27/10.22 cnf(3422,plain,
% 10.27/10.22 (P1(a2,x34221,a2)),
% 10.27/10.22 inference(scs_inference,[],[1218,555,1082,3401,3404,1507,3394,3399,1132,123,2597,2904,3029,3228,3020,3343,3391,3397,3402,2651,93,27,3111,2797,3352,2,66,10,3,9,14,11,13,12,67,69,70,68,73])).
% 10.27/10.22 cnf(3431,plain,
% 10.27/10.22 (E(f6(a2,a2),f6(x34311,a3))),
% 10.27/10.22 inference(scs_inference,[],[3386,2])).
% 10.27/10.22 cnf(3436,plain,
% 10.27/10.22 (E(f4(f6(x34361,x34361),x34361),f6(a7,a1))),
% 10.27/10.22 inference(scs_inference,[],[555,1507,2289,3386,1827,3342,1143,2831,2,10,9,14,3])).
% 10.27/10.22 cnf(3448,plain,
% 10.27/10.22 (P2(x34481,x34481,f4(f6(x34482,x34482),f6(x34482,x34482)))),
% 10.27/10.22 inference(rename_variables,[],[93])).
% 10.27/10.22 cnf(3454,plain,
% 10.27/10.22 (P1(f6(x34541,a3),x34542,f4(f4(a3,a3),f6(x34543,a3)))),
% 10.27/10.22 inference(scs_inference,[],[20,1218,555,1507,2036,123,2779,2783,2289,2011,2904,2776,3386,3253,2696,1827,93,249,44,2008,3342,1143,2831,2,10,9,14,3,11,13,12,69,70,67,68,73])).
% 10.27/10.22 cnf(3461,plain,
% 10.27/10.22 (E(f6(a3,x34611),f4(f4(a3,a3),f6(x34612,a3)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,1218,555,1528,1507,2036,123,2779,2783,2289,2011,2904,2776,3386,3422,3253,2696,1827,93,3448,249,44,2008,3342,1143,2831,2,10,9,14,3,11,13,12,69,70,67,68,73,71,66])).
% 10.27/10.22 cnf(3468,plain,
% 10.27/10.22 (P1(f6(x34681,a3),x34682,f6(a3,x34683))),
% 10.27/10.22 inference(rename_variables,[],[1528])).
% 10.27/10.22 cnf(3469,plain,
% 10.27/10.22 (E(f6(a3,x34691),f4(f4(a3,a3),f6(x34692,a3)))),
% 10.27/10.22 inference(rename_variables,[],[3461])).
% 10.27/10.22 cnf(3471,plain,
% 10.27/10.22 (P2(f4(a3,a3),f4(a3,a3),f6(x34711,a3))),
% 10.27/10.22 inference(rename_variables,[],[1464])).
% 10.27/10.22 cnf(3472,plain,
% 10.27/10.22 (E(f6(a3,x34721),f4(f4(a3,a3),f6(x34722,a3)))),
% 10.27/10.22 inference(rename_variables,[],[3461])).
% 10.27/10.22 cnf(3474,plain,
% 10.27/10.22 (E(f6(a3,x34741),f4(f4(a3,a3),f6(x34742,a3)))),
% 10.27/10.22 inference(rename_variables,[],[3461])).
% 10.27/10.22 cnf(3476,plain,
% 10.27/10.22 (P1(f4(a3,a3),x34761,f6(a3,x34762))),
% 10.27/10.22 inference(rename_variables,[],[840])).
% 10.27/10.22 cnf(3478,plain,
% 10.27/10.22 (P2(f6(a3,x34781),f6(a3,x34781),f6(x34782,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(3481,plain,
% 10.27/10.22 (P1(a7,x34811,a2)),
% 10.27/10.22 inference(scs_inference,[],[20,840,1464,555,1127,3478,1528,2904,3461,3469,3472,3474,3422,2651,3431,2,10,9,14,3,11,13,12,69])).
% 10.27/10.22 cnf(3482,plain,
% 10.27/10.22 (P1(x34821,a2,a2)),
% 10.27/10.22 inference(rename_variables,[],[2904])).
% 10.27/10.22 cnf(3495,plain,
% 10.27/10.22 (P1(f6(x34951,a3),x34952,f4(f6(x34953,a3),f4(a3,a3)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,1218,1464,555,1127,3478,1528,1723,123,2779,2904,2979,3050,3461,3469,3472,3474,3422,2651,28,249,978,2232,3431,2,10,9,14,3,11,13,12,69,70,67,68,73])).
% 10.27/10.22 cnf(3498,plain,
% 10.27/10.22 (P1(x34981,a7,a7)),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,1218,1464,555,1127,3478,1528,1723,123,2779,2904,3482,2979,3050,3461,3469,3472,3474,3422,2651,28,249,978,2232,3431,2,10,9,14,3,11,13,12,69,70,67,68,73,74])).
% 10.27/10.22 cnf(3500,plain,
% 10.27/10.22 (P2(f6(a3,x35001),f6(a3,x35001),a7)),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,3476,1218,1464,3471,555,1127,3478,1528,1723,123,2779,2904,3482,2979,3050,3461,3469,3472,3474,3422,2651,28,249,978,2232,3431,2,10,9,14,3,11,13,12,69,70,67,68,73,74,72])).
% 10.27/10.22 cnf(3507,plain,
% 10.27/10.22 (P1(f6(x35071,a3),x35072,f6(a3,x35073))),
% 10.27/10.22 inference(rename_variables,[],[1528])).
% 10.27/10.22 cnf(3509,plain,
% 10.27/10.22 (E(f6(a3,x35091),f4(f6(x35092,a3),f4(a3,a3)))),
% 10.27/10.22 inference(scs_inference,[],[20,22,840,3476,1218,1464,3471,555,1127,3478,1528,3468,3507,1723,123,2779,2904,3482,2979,3050,3454,3461,3469,3472,3474,3422,2651,28,249,978,2232,3431,2,10,9,14,3,11,13,12,69,70,67,68,73,74,72,71,66])).
% 10.27/10.22 cnf(3516,plain,
% 10.27/10.22 (E(f6(a3,x35161),a7)),
% 10.27/10.22 inference(scs_inference,[],[840,3509,3498,2,66])).
% 10.27/10.22 cnf(3517,plain,
% 10.27/10.22 (P1(x35171,a7,a7)),
% 10.27/10.22 inference(rename_variables,[],[3498])).
% 10.27/10.22 cnf(3518,plain,
% 10.27/10.22 (P1(f4(a3,a3),x35181,f6(a3,x35182))),
% 10.27/10.22 inference(rename_variables,[],[840])).
% 10.27/10.22 cnf(3524,plain,
% 10.27/10.22 (E(f6(a3,x35241),f4(f6(x35242,a3),f4(a3,a3)))),
% 10.27/10.22 inference(rename_variables,[],[3509])).
% 10.27/10.22 cnf(3526,plain,
% 10.27/10.22 (P1(f6(x35261,a3),x35262,f6(a3,x35263))),
% 10.27/10.22 inference(rename_variables,[],[1528])).
% 10.27/10.22 cnf(3527,plain,
% 10.27/10.22 (E(f6(a3,x35271),f4(f6(x35272,a3),f4(a3,a3)))),
% 10.27/10.22 inference(rename_variables,[],[3509])).
% 10.27/10.22 cnf(3529,plain,
% 10.27/10.22 (E(f6(a3,x35291),f4(f6(x35292,a3),f4(a3,a3)))),
% 10.27/10.22 inference(rename_variables,[],[3509])).
% 10.27/10.22 cnf(3533,plain,
% 10.27/10.22 (P2(f6(a3,x35331),f6(a3,x35331),f6(x35332,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(3535,plain,
% 10.27/10.22 (P2(f6(a3,x35351),f6(a3,x35351),f6(x35352,a3))),
% 10.27/10.22 inference(rename_variables,[],[1127])).
% 10.27/10.22 cnf(3553,plain,
% 10.27/10.22 (P1(x35531,a7,a7)),
% 10.27/10.22 inference(rename_variables,[],[3498])).
% 10.27/10.22 cnf(3555,plain,
% 10.27/10.22 (P1(x35551,f6(a1,a2),f6(a1,a2))),
% 10.27/10.22 inference(scs_inference,[],[20,840,3518,1464,1737,1127,3533,3535,1528,3526,1063,127,3495,3087,3509,3524,3527,3529,3500,3481,3498,3517,3553,2651,978,2252,2,66,10,14,9,3,11,13,12,69,70,67,68,73,74])).
% 10.27/10.22 cnf(3575,plain,
% 10.27/10.22 (E(f6(a3,x35751),a7)),
% 10.27/10.22 inference(rename_variables,[],[3516])).
% 10.27/10.22 cnf(3578,plain,
% 10.27/10.22 (E(f6(a3,x35781),a7)),
% 10.27/10.22 inference(rename_variables,[],[3516])).
% 10.27/10.22 cnf(3579,plain,
% 10.27/10.22 ($false),
% 10.27/10.22 inference(scs_inference,[],[63,840,1218,1528,1112,3555,3516,3575,3578,3436,2799,2650,2,66,10,14,9,3]),
% 10.27/10.22 ['proof']).
% 10.27/10.22 % SZS output end Proof
% 10.27/10.22 % Total time :9.570000s
%------------------------------------------------------------------------------