%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET702+4 : TPTP v8.2.0. Released v2.2.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:22:16 EDT 2024
% Result : Theorem 118.13s 118.88s
% Output : CNFRefutation 118.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET702+4 : TPTP v8.2.0. Released v2.2.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jun 23 11:11:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.54/0.59 start to proof:theBenchmark
% 118.13/118.87 %-------------------------------------------
% 118.13/118.87 % File :CSE---1.7
% 118.13/118.87 % Problem :theBenchmark
% 118.13/118.87 % Transform :cnf
% 118.13/118.87 % Format :tptp:raw
% 118.13/118.87 % Command :java -jar mcs_scs.jar %d %s
% 118.13/118.87
% 118.13/118.87 % Result :Theorem 117.530000s
% 118.13/118.87 % Output :CNFRefutation 117.530000s
% 118.13/118.87 %-------------------------------------------
% 118.13/118.88 %--------------------------------------------------------------------------
% 118.13/118.88 % File : SET702+4 : TPTP v8.2.0. Released v2.2.0.
% 118.13/118.88 % Domain : Set Theory (Naive)
% 118.13/118.88 % Problem : Property of product and intersection
% 118.13/118.88 % Version : [Pas99] axioms.
% 118.13/118.88 % English : The intersection of product(A) and product(B) is a subset of
% 118.13/118.88 % the product of the intersection of A and B.
% 118.13/118.88
% 118.13/118.88 % Refs : [Pas99] Pastre (1999), Email to G. Sutcliffe
% 118.13/118.88 % Source : [Pas99]
% 118.13/118.88 % Names :
% 118.13/118.88
% 118.13/118.88 % Status : Theorem
% 118.13/118.88 % Rating : 0.39 v8.2.0, 0.44 v8.1.0, 0.42 v7.5.0, 0.41 v7.4.0, 0.40 v7.3.0, 0.38 v7.2.0, 0.34 v7.1.0, 0.30 v7.0.0, 0.37 v6.4.0, 0.42 v6.2.0, 0.40 v6.1.0, 0.47 v6.0.0, 0.48 v5.5.0, 0.59 v5.4.0, 0.68 v5.3.0, 0.67 v5.2.0, 0.50 v5.1.0, 0.57 v5.0.0, 0.62 v4.1.0, 0.61 v4.0.1, 0.65 v4.0.0, 0.67 v3.7.0, 0.70 v3.5.0, 0.68 v3.4.0, 0.79 v3.3.0, 0.71 v3.2.0, 0.73 v3.1.0, 0.78 v2.7.0, 0.67 v2.6.0, 0.71 v2.5.0, 0.75 v2.4.0, 0.25 v2.3.0, 0.00 v2.2.1
% 118.13/118.88 % Syntax : Number of formulae : 12 ( 2 unt; 0 def)
% 118.13/118.88 % Number of atoms : 30 ( 3 equ)
% 118.13/118.88 % Maximal formula atoms : 3 ( 2 avg)
% 118.13/118.88 % Number of connectives : 20 ( 2 ~; 2 |; 4 &)
% 118.13/118.88 % ( 10 <=>; 2 =>; 0 <=; 0 <~>)
% 118.13/118.88 % Maximal formula depth : 7 ( 5 avg)
% 118.13/118.88 % Maximal term depth : 3 ( 1 avg)
% 118.13/118.88 % Number of predicates : 4 ( 3 usr; 0 prp; 2-2 aty)
% 118.13/118.88 % Number of functors : 9 ( 9 usr; 1 con; 0-2 aty)
% 118.13/118.88 % Number of variables : 30 ( 29 !; 1 ?)
% 118.13/118.88 % SPC : FOF_THM_RFO_SEQ
% 118.13/118.88
% 118.13/118.88 % Comments :
% 118.13/118.88 %--------------------------------------------------------------------------
% 118.13/118.88 %----Include set theory definitions
% 118.13/118.88 include('Axioms/SET006+0.ax').
% 118.13/118.88 %--------------------------------------------------------------------------
% 118.13/118.88 fof(thI36,conjecture,
% 118.13/118.88 ! [A,B] : subset(intersection(product(A),product(B)),product(intersection(A,B))) ).
% 118.13/118.88
% 118.13/118.88 %--------------------------------------------------------------------------
% 118.13/118.88 %-------------------------------------------
% 118.13/118.88 % Proof found
% 118.13/118.88 % SZS status Theorem for theBenchmark
% 118.13/118.88 % SZS output start Proof
% 118.13/118.89 %ClaNum:57(EqnAxiom:27)
% 118.13/118.89 %VarNum:147(SingletonVarNum:72)
% 118.13/118.89 %MaxLitNum:3
% 118.13/118.89 %MaxfuncDepth:2
% 118.13/118.89 %SharedTerms:9
% 118.13/118.89 %goalClause: 29
% 118.13/118.89 %singleGoalClaCount:1
% 118.13/118.89 [29]~P3(f9(f7(a3),f7(a8)),f7(f9(a3,a8)))
% 118.13/118.89 [28]~P1(x281,a1)
% 118.13/118.89 [32]~P2(x322,x321)+P3(x321,x322)
% 118.13/118.89 [33]~P2(x331,x332)+P3(x331,x332)
% 118.13/118.89 [30]~E(x301,x302)+P1(x301,f11(x302))
% 118.13/118.89 [31]E(x311,x312)+~P1(x311,f11(x312))
% 118.13/118.89 [34]~P3(x341,x342)+P1(x341,f10(x342))
% 118.13/118.89 [37]P3(x371,x372)+~P1(x371,f10(x372))
% 118.13/118.89 [38]P3(x381,x382)+P1(f4(x381,x382),x381)
% 118.13/118.89 [41]P1(f5(x411,x412),x412)+P1(x411,f7(x412))
% 118.13/118.89 [47]~P1(x471,f14(x472))+P1(x471,f6(x471,x472))
% 118.13/118.89 [48]~P1(x481,f14(x482))+P1(f6(x481,x482),x482)
% 118.13/118.89 [53]P3(x531,x532)+~P1(f4(x531,x532),x532)
% 118.13/118.89 [54]~P1(x541,f5(x541,x542))+P1(x541,f7(x542))
% 118.13/118.89 [35]~E(x351,x353)+P1(x351,f12(x352,x353))
% 118.13/118.89 [36]~E(x361,x362)+P1(x361,f12(x362,x363))
% 118.13/118.89 [42]~P1(x421,x423)+P1(x421,f13(x422,x423))
% 118.13/118.89 [43]~P1(x431,x432)+P1(x431,f13(x432,x433))
% 118.13/118.89 [50]P1(x501,x502)+~P1(x501,f9(x503,x502))
% 118.13/118.89 [51]P1(x511,x512)+~P1(x511,f9(x512,x513))
% 118.13/118.89 [52]P1(x521,x522)+~P1(x521,f2(x522,x523))
% 118.13/118.89 [56]~P1(x561,x562)+~P1(x561,f2(x563,x562))
% 118.13/118.89 [40]~P3(x402,x401)+~P3(x401,x402)+P2(x401,x402)
% 118.13/118.89 [39]~P1(x391,x393)+P1(x391,x392)+~P3(x393,x392)
% 118.13/118.89 [44]~P1(x443,x442)+~P1(x441,x443)+P1(x441,f14(x442))
% 118.13/118.89 [45]E(x451,x452)+E(x451,x453)+~P1(x451,f12(x453,x452))
% 118.13/118.89 [46]P1(x461,x462)+~P1(x462,x463)+~P1(x461,f7(x463))
% 118.13/118.89 [49]~P1(x491,x493)+P1(x491,x492)+P1(x491,f2(x493,x492))
% 118.13/118.89 [55]~P1(x551,x553)+~P1(x551,x552)+P1(x551,f9(x552,x553))
% 118.13/118.89 [57]P1(x571,x572)+P1(x571,x573)+~P1(x571,f13(x573,x572))
% 118.13/118.89 %EqnAxiom
% 118.13/118.89 [1]E(x11,x11)
% 118.13/118.89 [2]E(x22,x21)+~E(x21,x22)
% 118.13/118.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 118.13/118.89 [4]~E(x41,x42)+E(f7(x41),f7(x42))
% 118.13/118.89 [5]~E(x51,x52)+E(f13(x51,x53),f13(x52,x53))
% 118.13/118.89 [6]~E(x61,x62)+E(f13(x63,x61),f13(x63,x62))
% 118.13/118.89 [7]~E(x71,x72)+E(f9(x71,x73),f9(x72,x73))
% 118.13/118.89 [8]~E(x81,x82)+E(f9(x83,x81),f9(x83,x82))
% 118.13/118.89 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 118.13/118.89 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 118.13/118.89 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113))
% 118.13/118.89 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122))
% 118.13/118.89 [13]~E(x131,x132)+E(f11(x131),f11(x132))
% 118.13/118.89 [14]~E(x141,x142)+E(f5(x141,x143),f5(x142,x143))
% 118.13/118.89 [15]~E(x151,x152)+E(f5(x153,x151),f5(x153,x152))
% 118.13/118.89 [16]~E(x161,x162)+E(f10(x161),f10(x162))
% 118.13/118.89 [17]~E(x171,x172)+E(f12(x171,x173),f12(x172,x173))
% 118.13/118.89 [18]~E(x181,x182)+E(f12(x183,x181),f12(x183,x182))
% 118.13/118.89 [19]~E(x191,x192)+E(f14(x191),f14(x192))
% 118.13/118.89 [20]~E(x201,x202)+E(f4(x201,x203),f4(x202,x203))
% 118.13/118.89 [21]~E(x211,x212)+E(f4(x213,x211),f4(x213,x212))
% 118.13/118.89 [22]P1(x222,x223)+~E(x221,x222)+~P1(x221,x223)
% 118.13/118.89 [23]P1(x233,x232)+~E(x231,x232)+~P1(x233,x231)
% 118.13/118.89 [24]P3(x242,x243)+~E(x241,x242)+~P3(x241,x243)
% 118.13/118.89 [25]P3(x253,x252)+~E(x251,x252)+~P3(x253,x251)
% 118.13/118.89 [26]P2(x262,x263)+~E(x261,x262)+~P2(x261,x263)
% 118.13/118.89 [27]P2(x273,x272)+~E(x271,x272)+~P2(x273,x271)
% 118.13/118.89
% 118.13/118.89 %-------------------------------------------
% 118.13/118.90 cnf(58,plain,
% 118.13/118.90 (P1(x581,f11(x581))),
% 118.13/118.90 inference(equality_inference,[],[30])).
% 118.13/118.90 cnf(59,plain,
% 118.13/118.90 (P1(x591,f12(x592,x591))),
% 118.13/118.90 inference(equality_inference,[],[35])).
% 118.13/118.90 cnf(60,plain,
% 118.13/118.90 (P1(x601,f12(x601,x602))),
% 118.13/118.90 inference(equality_inference,[],[36])).
% 118.13/118.90 cnf(65,plain,
% 118.13/118.90 (P3(a1,x651)),
% 118.13/118.90 inference(scs_inference,[],[29,28,32,33,38])).
% 118.13/118.90 cnf(66,plain,
% 118.13/118.90 (~P1(x661,a1)),
% 118.13/118.90 inference(rename_variables,[],[28])).
% 118.13/118.90 cnf(68,plain,
% 118.13/118.90 (~P1(x681,f14(a1))),
% 118.13/118.90 inference(scs_inference,[],[29,28,66,32,33,38,48])).
% 118.13/118.90 cnf(69,plain,
% 118.13/118.90 (~P1(x691,a1)),
% 118.13/118.90 inference(rename_variables,[],[28])).
% 118.13/118.90 cnf(71,plain,
% 118.13/118.90 (~E(a1,f9(f7(a3),f7(a8)))),
% 118.13/118.90 inference(scs_inference,[],[29,28,66,32,33,38,48,24])).
% 118.13/118.90 cnf(72,plain,
% 118.13/118.90 (~E(f11(x721),a1)),
% 118.13/118.90 inference(scs_inference,[],[29,58,28,66,69,32,33,38,48,24,23])).
% 118.13/118.90 cnf(73,plain,
% 118.13/118.90 (P1(x731,f11(x731))),
% 118.13/118.90 inference(rename_variables,[],[58])).
% 118.13/118.90 cnf(76,plain,
% 118.13/118.90 (P1(x761,f11(x762))+~E(x762,x761)),
% 118.13/118.90 inference(scs_inference,[],[29,58,73,28,66,69,32,33,38,48,24,23,40,22])).
% 118.13/118.90 cnf(80,plain,
% 118.13/118.90 (~P1(x801,f14(f14(a1)))),
% 118.13/118.90 inference(scs_inference,[],[68,48])).
% 118.13/118.90 cnf(81,plain,
% 118.13/118.90 (~P1(x811,f14(a1))),
% 118.13/118.90 inference(rename_variables,[],[68])).
% 118.13/118.90 cnf(83,plain,
% 118.13/118.90 (P3(f14(a1),x831)),
% 118.13/118.90 inference(scs_inference,[],[68,81,48,38])).
% 118.13/118.90 cnf(84,plain,
% 118.13/118.90 (~P1(x841,f14(a1))),
% 118.13/118.90 inference(rename_variables,[],[68])).
% 118.13/118.90 cnf(86,plain,
% 118.13/118.90 (P2(a1,a1)),
% 118.13/118.90 inference(scs_inference,[],[65,68,81,48,38,40])).
% 118.13/118.90 cnf(90,plain,
% 118.13/118.90 (~E(f12(x901,x902),f14(a1))),
% 118.13/118.90 inference(scs_inference,[],[65,59,68,81,84,48,38,40,23])).
% 118.13/118.90 cnf(91,plain,
% 118.13/118.90 (P1(x911,f12(x912,x911))),
% 118.13/118.90 inference(rename_variables,[],[59])).
% 118.13/118.90 cnf(92,plain,
% 118.13/118.90 (~E(f14(a1),f9(f7(a3),f7(a8)))),
% 118.13/118.90 inference(scs_inference,[],[29,65,59,68,81,84,48,38,40,23,24])).
% 118.13/118.90 cnf(95,plain,
% 118.13/118.90 (P1(x951,f12(x952,x953))+~E(x953,x951)),
% 118.13/118.90 inference(scs_inference,[],[29,65,59,91,68,81,84,48,38,40,23,24,26,27,22])).
% 118.13/118.90 cnf(100,plain,
% 118.13/118.90 (~P1(x1001,f14(f14(a1)))),
% 118.13/118.90 inference(rename_variables,[],[80])).
% 118.13/118.90 cnf(102,plain,
% 118.13/118.90 (P3(f14(f14(a1)),x1021)),
% 118.13/118.90 inference(scs_inference,[],[80,100,48,38])).
% 118.13/118.90 cnf(103,plain,
% 118.13/118.90 (~P1(x1031,f14(f14(a1)))),
% 118.13/118.90 inference(rename_variables,[],[80])).
% 118.13/118.90 cnf(110,plain,
% 118.13/118.90 (P1(x1101,f12(x1101,x1102))),
% 118.13/118.90 inference(rename_variables,[],[60])).
% 118.13/118.90 cnf(114,plain,
% 118.13/118.90 (P1(x1141,f12(x1142,x1143))+~E(x1142,x1141)),
% 118.13/118.90 inference(scs_inference,[],[29,83,60,110,80,100,103,48,38,40,23,24,26,27,22])).
% 118.13/118.90 cnf(118,plain,
% 118.13/118.90 (~E(f11(x1181),f14(a1))),
% 118.13/118.90 inference(scs_inference,[],[68,58,23])).
% 118.13/118.90 cnf(133,plain,
% 118.13/118.90 (P2(a1,x1331)+~E(f14(a1),x1331)),
% 118.13/118.90 inference(scs_inference,[],[83,65,40,26,27])).
% 118.13/118.90 cnf(157,plain,
% 118.13/118.90 (P2(f14(a1),x1571)+~E(a1,x1571)),
% 118.13/118.90 inference(scs_inference,[],[65,83,40,26,27])).
% 118.13/118.90 cnf(160,plain,
% 118.13/118.90 (~P1(f9(f7(a3),f7(a8)),f11(a1))),
% 118.13/118.90 inference(scs_inference,[],[71,2,31])).
% 118.13/118.90 cnf(161,plain,
% 118.13/118.90 (~E(f9(f7(a3),f7(a8)),a1)),
% 118.13/118.91 inference(scs_inference,[],[160,30])).
% 118.13/118.91 cnf(163,plain,
% 118.13/118.91 (~E(f12(x1631,x1632),a1)),
% 118.13/118.91 inference(scs_inference,[],[28,59,160,30,23])).
% 118.13/118.91 cnf(165,plain,
% 118.13/118.91 (P1(a1,f10(a1))),
% 118.13/118.91 inference(scs_inference,[],[86,34,32])).
% 118.13/118.91 cnf(166,plain,
% 118.13/118.91 (~E(f10(a1),a1)),
% 118.13/118.91 inference(scs_inference,[],[28,165,23])).
% 118.13/118.91 cnf(191,plain,
% 118.13/118.91 (P1(x1911,f13(f7(f14(a1)),x1912))),
% 118.13/118.91 inference(scs_inference,[],[68,43,41])).
% 118.13/118.91 cnf(192,plain,
% 118.13/118.91 (P1(x1921,f7(f14(a1)))),
% 118.13/118.91 inference(scs_inference,[],[68,191,57])).
% 118.13/118.91 cnf(193,plain,
% 118.13/118.91 (P1(x1931,f13(f7(f14(a1)),x1932))),
% 118.13/118.91 inference(rename_variables,[],[191])).
% 118.13/118.91 cnf(197,plain,
% 118.13/118.91 (P3(x1971,f7(f14(a1)))),
% 118.13/118.91 inference(scs_inference,[],[68,191,193,57,23,53])).
% 118.13/118.91 cnf(199,plain,
% 118.13/118.91 (~E(f7(f14(a1)),f7(f9(a3,a8)))),
% 118.13/118.91 inference(scs_inference,[],[29,68,191,193,57,23,53,25])).
% 118.13/118.91 cnf(202,plain,
% 118.13/118.91 (~E(f14(a1),f9(a3,a8))),
% 118.13/118.91 inference(scs_inference,[],[29,68,191,193,57,23,53,25,40,4])).
% 118.13/118.91 cnf(209,plain,
% 118.13/118.91 (~E(f11(x2091),f14(f14(a1)))),
% 118.13/118.91 inference(scs_inference,[],[197,80,58,40,23])).
% 118.13/118.91 cnf(221,plain,
% 118.13/118.91 (~P1(a1,f2(x2211,f10(x2212)))),
% 118.13/118.91 inference(scs_inference,[],[65,56,34])).
% 118.13/118.91 cnf(222,plain,
% 118.13/118.91 (P1(a1,f10(x2221))),
% 118.13/118.91 inference(scs_inference,[],[60,221,49])).
% 118.13/118.91 cnf(226,plain,
% 118.13/118.91 (~E(f7(f14(a1)),f14(a1))),
% 118.13/118.91 inference(scs_inference,[],[68,60,192,221,49,23])).
% 118.13/118.91 cnf(228,plain,
% 118.13/118.91 (P1(x2281,f10(x2282))+~E(a1,x2281)),
% 118.13/118.91 inference(scs_inference,[],[68,60,192,221,49,23,22])).
% 118.13/118.91 cnf(233,plain,
% 118.13/118.91 (~P1(x2331,f14(x2332))+P1(x2331,f13(x2333,f6(x2331,x2332)))),
% 118.13/118.91 inference(scs_inference,[],[47,42])).
% 118.13/118.91 cnf(234,plain,
% 118.13/118.91 (~E(f10(x2341),f14(a1))),
% 118.13/118.91 inference(scs_inference,[],[68,222,23])).
% 118.13/118.91 cnf(236,plain,
% 118.13/118.91 (~P1(f4(f9(f7(a3),f7(a8)),f7(f9(a3,a8))),f5(f4(f9(f7(a3),f7(a8)),f7(f9(a3,a8))),f9(a3,a8)))),
% 118.13/118.91 inference(scs_inference,[],[29,54,53])).
% 118.13/118.91 cnf(250,plain,
% 118.13/118.91 (~P1(x2501,f14(x2502))+P1(x2501,f13(f13(x2503,f6(x2501,x2502)),x2504))),
% 118.13/118.91 inference(scs_inference,[],[233,43])).
% 118.13/118.91 cnf(268,plain,
% 118.13/118.91 (P2(a1,x2681)+~E(f14(f14(a1)),x2681)),
% 118.13/118.91 inference(scs_inference,[],[102,65,40,26,27])).
% 118.13/118.91 cnf(282,plain,
% 118.13/118.91 (~P1(x2821,f14(x2822))+~P1(x2821,f2(x2823,f13(f13(x2824,f6(x2821,x2822)),x2825)))),
% 118.13/118.91 inference(scs_inference,[],[250,56])).
% 118.13/118.91 cnf(286,plain,
% 118.13/118.91 (~E(x2861,f14(a1))+~E(f9(f7(a3),f7(a8)),x2861)),
% 118.13/118.91 inference(scs_inference,[],[92,3,2])).
% 118.13/118.91 cnf(289,plain,
% 118.13/118.91 (~E(f9(f7(a3),f7(a8)),f14(a1))),
% 118.13/118.91 inference(scs_inference,[],[58,286,31])).
% 118.13/118.91 cnf(293,plain,
% 118.13/118.91 (~E(f7(f14(a1)),f11(a1))),
% 118.13/118.91 inference(scs_inference,[],[160,192,23])).
% 118.13/118.91 cnf(302,plain,
% 118.13/118.91 (~P1(a1,f11(f12(x3021,x3022)))),
% 118.13/118.91 inference(scs_inference,[],[163,2,31])).
% 118.13/118.91 cnf(305,plain,
% 118.13/118.91 (~E(f14(f14(a1)),f12(x3051,x3052))),
% 118.13/118.91 inference(scs_inference,[],[59,80,2,23])).
% 118.13/118.91 cnf(306,plain,
% 118.13/118.91 (~P1(a1,f11(f10(a1)))),
% 118.13/118.91 inference(scs_inference,[],[166,2,31])).
% 118.13/118.91 cnf(314,plain,
% 118.13/118.91 (~P1(f9(a3,a8),f11(f14(a1)))),
% 118.13/118.91 inference(scs_inference,[],[202,2,31])).
% 118.13/118.91 cnf(316,plain,
% 118.13/118.91 (~E(x3161,a1)+P2(x3161,a1)),
% 118.13/118.91 inference(scs_inference,[],[86,2,26])).
% 118.13/118.91 cnf(318,plain,
% 118.13/118.91 (~E(f2(x3181,f10(x3182)),f12(x3183,a1))),
% 118.13/118.91 inference(scs_inference,[],[59,221,2,23])).
% 118.13/118.91 cnf(321,plain,
% 118.13/118.91 (~E(f2(x3211,f10(x3212)),f12(a1,x3213))),
% 118.13/118.91 inference(scs_inference,[],[60,221,2,23])).
% 118.13/118.91 cnf(327,plain,
% 118.13/118.91 (~E(f10(x3271),f2(x3272,f10(x3273)))),
% 118.13/118.91 inference(scs_inference,[],[221,222,23])).
% 118.13/118.91 cnf(329,plain,
% 118.13/118.91 (~E(f11(a1),f2(x3291,f10(x3292)))),
% 118.13/118.91 inference(scs_inference,[],[221,58,23])).
% 118.13/118.91 cnf(335,plain,
% 118.13/118.91 (P3(x3351,a1)+~E(f14(a1),x3351)),
% 118.13/118.91 inference(scs_inference,[],[32,133])).
% 118.13/118.91 cnf(341,plain,
% 118.13/118.91 (P3(x3411,f14(a1))+~E(a1,x3411)),
% 118.13/118.91 inference(scs_inference,[],[32,157])).
% 118.13/118.91 cnf(356,plain,
% 118.13/118.91 (P3(x3561,a1)+~E(f14(f14(a1)),x3561)),
% 118.13/118.91 inference(scs_inference,[],[32,268])).
% 118.13/118.91 cnf(362,plain,
% 118.13/118.91 (P3(x3621,a1)+~E(x3621,a1)),
% 118.13/118.91 inference(scs_inference,[],[33,316])).
% 118.13/118.91 cnf(368,plain,
% 118.13/118.91 (~E(f12(x3681,a1),f11(f12(x3682,x3683)))),
% 118.13/118.91 inference(scs_inference,[],[302,59,23])).
% 118.13/118.91 cnf(371,plain,
% 118.13/118.91 (~E(f12(a1,x3711),f11(f12(x3712,x3713)))),
% 118.13/118.91 inference(scs_inference,[],[302,60,23])).
% 118.13/118.91 cnf(377,plain,
% 118.13/118.91 (~E(f10(x3771),f11(f12(x3772,x3773)))),
% 118.25/118.91 inference(scs_inference,[],[302,222,23])).
% 118.25/118.91 cnf(384,plain,
% 118.25/118.91 (~E(f12(x3841,a1),f11(f10(a1)))),
% 118.25/118.91 inference(scs_inference,[],[306,59,23])).
% 118.25/118.91 cnf(386,plain,
% 118.25/118.91 (~E(f12(a1,x3861),f11(f10(a1)))),
% 118.25/118.91 inference(scs_inference,[],[306,60,23])).
% 118.25/118.91 cnf(390,plain,
% 118.25/118.91 (~E(f10(x3901),f11(f10(a1)))),
% 118.25/118.91 inference(scs_inference,[],[306,222,23])).
% 118.25/118.91 cnf(393,plain,
% 118.25/118.91 (P2(a1,x3931)+~E(x3931,a1)),
% 118.25/118.91 inference(scs_inference,[],[65,362,40])).
% 118.25/118.91 cnf(395,plain,
% 118.25/118.91 (P2(a1,x3951)+~E(x3952,x3951)+~E(x3952,a1)),
% 118.25/118.91 inference(scs_inference,[],[393,27])).
% 118.25/118.91 cnf(402,plain,
% 118.25/118.91 (~E(x4021,x4022)+P1(x4021,f13(x4023,f11(x4022)))),
% 118.25/118.91 inference(scs_inference,[],[30,42])).
% 118.25/118.91 cnf(403,plain,
% 118.25/118.91 (P1(x4031,f13(x4032,f11(x4031)))),
% 118.25/118.91 inference(equality_inference,[],[402])).
% 118.25/118.91 cnf(406,plain,
% 118.25/118.91 (P1(x4061,f13(x4062,f11(x4063)))+~E(x4063,x4061)),
% 118.25/118.91 inference(scs_inference,[],[314,192,403,23,22])).
% 118.25/118.91 cnf(407,plain,
% 118.25/118.91 (P3(x4071,f13(x4072,f11(x4073)))+~E(x4073,f4(x4071,f13(x4072,f11(x4073))))),
% 118.25/118.91 inference(scs_inference,[],[314,192,403,23,22,53])).
% 118.25/118.91 cnf(409,plain,
% 118.25/118.91 (P1(x4091,f13(x4092,f11(x4093)))+~E(x4093,f4(f12(x4094,x4091),f13(x4092,f11(x4093))))),
% 118.25/118.91 inference(scs_inference,[],[314,59,192,403,23,22,53,39])).
% 118.25/118.91 cnf(413,plain,
% 118.25/118.91 (~E(f4(x4131,f13(x4132,f11(x4133))),x4133)+P3(x4131,f13(x4132,f11(x4133)))),
% 118.25/118.91 inference(scs_inference,[],[407,2])).
% 118.25/118.91 cnf(419,plain,
% 118.25/118.91 (P1(x4191,f13(x4192,f11(x4193)))+~P1(x4193,f11(f4(f12(x4194,x4191),f13(x4192,f11(x4193)))))),
% 118.25/118.91 inference(scs_inference,[],[409,31])).
% 118.25/118.91 cnf(423,plain,
% 118.25/118.91 (~E(x4231,x4232)+P1(x4231,f13(f11(x4232),x4233))),
% 118.25/118.91 inference(scs_inference,[],[30,43])).
% 118.25/118.91 cnf(424,plain,
% 118.25/118.91 (P1(x4241,f13(f11(x4241),x4242))),
% 118.25/118.91 inference(equality_inference,[],[423])).
% 118.25/118.91 cnf(426,plain,
% 118.25/118.91 (P1(x4261,f13(f11(x4261),x4262))),
% 118.25/118.91 inference(rename_variables,[],[424])).
% 118.25/118.91 cnf(427,plain,
% 118.25/118.91 (P1(x4271,f13(f11(x4272),x4273))+~E(x4272,x4271)),
% 118.25/118.91 inference(scs_inference,[],[80,424,426,23,22])).
% 118.25/118.91 cnf(428,plain,
% 118.25/118.91 (P3(x4281,f13(f11(x4282),x4283))+~E(x4282,f4(x4281,f13(f11(x4282),x4283)))),
% 118.25/118.91 inference(scs_inference,[],[80,424,426,23,22,53])).
% 118.25/118.91 cnf(430,plain,
% 118.25/118.91 (P1(x4301,f13(f11(x4302),x4303))+~E(x4302,f4(f12(x4304,x4301),f13(f11(x4302),x4303)))),
% 118.25/118.91 inference(scs_inference,[],[59,80,424,426,23,22,53,39])).
% 118.25/118.91 cnf(434,plain,
% 118.25/118.91 (~E(f4(x4341,f13(f11(x4342),x4343)),x4342)+P3(x4341,f13(f11(x4342),x4343))),
% 118.25/118.91 inference(scs_inference,[],[428,2])).
% 118.25/118.91 cnf(436,plain,
% 118.25/118.91 (P1(x4361,f13(f11(x4362),x4363))+~P1(x4362,f11(f4(f12(x4364,x4361),f13(f11(x4362),x4363))))),
% 118.25/118.91 inference(scs_inference,[],[430,31])).
% 118.25/118.91 cnf(440,plain,
% 118.25/118.91 (~E(f4(x4401,f11(x4402)),x4402)+P3(x4401,f11(x4402))),
% 118.25/118.91 inference(scs_inference,[],[30,53])).
% 118.25/118.91 cnf(441,plain,
% 118.25/118.91 (~E(x4411,f4(x4412,f11(x4411)))+P3(x4412,f11(x4411))),
% 118.25/118.91 inference(scs_inference,[],[440,2])).
% 118.25/118.91 cnf(443,plain,
% 118.25/118.91 (~E(x4431,x4432)+~P1(x4431,f2(x4433,f11(x4432)))),
% 118.25/118.91 inference(scs_inference,[],[30,56])).
% 118.25/118.91 cnf(444,plain,
% 118.25/118.91 (~P1(x4441,f2(x4442,f11(x4441)))),
% 118.25/118.91 inference(equality_inference,[],[443])).
% 118.25/118.91 cnf(460,plain,
% 118.25/118.91 (~E(x4601,x4602)+~E(f11(x4602),f2(x4603,f11(x4601)))),
% 118.25/118.91 inference(scs_inference,[],[444,30,23])).
% 118.25/118.91 cnf(461,plain,
% 118.25/118.91 (~E(f12(x4611,x4612),f2(x4613,f11(x4612)))),
% 118.25/118.91 inference(scs_inference,[],[444,59,23])).
% 118.25/118.91 cnf(463,plain,
% 118.25/118.91 (~E(f11(x4631),f2(x4632,f11(x4631)))),
% 118.25/118.91 inference(scs_inference,[],[58,460,31])).
% 118.25/118.91 cnf(464,plain,
% 118.25/118.91 (~E(f12(x4641,x4642),f2(x4643,f11(x4641)))),
% 118.25/118.91 inference(scs_inference,[],[444,60,23])).
% 118.25/118.91 cnf(466,plain,
% 118.25/118.91 (~E(f2(x4661,f11(x4662)),x4663)+~P1(x4662,f7(f11(x4663)))),
% 118.25/118.91 inference(scs_inference,[],[444,30,46])).
% 118.25/118.91 cnf(467,plain,
% 118.25/118.91 (~P1(x4671,f7(f11(f2(x4672,f11(x4671)))))),
% 118.25/118.91 inference(equality_inference,[],[466])).
% 118.25/118.91 cnf(470,plain,
% 118.25/118.91 (~E(x4701,x4702)+P1(x4701,f9(f12(x4703,x4701),f11(x4702)))),
% 118.25/118.91 inference(scs_inference,[],[59,30,55])).
% 118.25/118.91 cnf(471,plain,
% 118.25/118.91 (P1(x4711,f9(f12(x4712,x4711),f11(x4711)))),
% 118.25/118.91 inference(equality_inference,[],[470])).
% 118.25/118.91 cnf(472,plain,
% 118.25/118.91 (~E(f10(x4721),f2(x4722,f11(a1)))),
% 118.25/118.91 inference(scs_inference,[],[444,222,23])).
% 118.25/118.91 cnf(474,plain,
% 118.25/118.91 (P1(x4741,f9(f12(x4742,x4743),f11(x4743)))+~E(x4743,x4741)),
% 118.25/118.91 inference(scs_inference,[],[444,222,471,23,22])).
% 118.25/118.91 cnf(479,plain,
% 118.25/118.91 (~E(f12(x4791,x4792),x4793)+P1(x4792,f14(f11(x4793)))),
% 118.25/118.91 inference(scs_inference,[],[59,30,44])).
% 118.25/118.91 cnf(480,plain,
% 118.25/118.91 (P1(x4801,f14(f11(f12(x4802,x4801))))),
% 118.25/118.91 inference(equality_inference,[],[479])).
% 118.25/118.91 cnf(481,plain,
% 118.25/118.91 (~E(f13(x4811,f11(x4812)),f2(x4813,f11(x4812)))),
% 118.25/118.91 inference(scs_inference,[],[444,403,23])).
% 118.25/118.91 cnf(493,plain,
% 118.25/118.91 (~E(x4931,x4932)+P1(x4931,f9(f11(x4932),f12(x4933,x4931)))),
% 118.25/118.91 inference(scs_inference,[],[59,30,55])).
% 118.25/118.91 cnf(494,plain,
% 118.25/118.91 (P1(x4941,f9(f11(x4941),f12(x4942,x4941)))),
% 118.25/118.91 inference(equality_inference,[],[493])).
% 118.25/118.91 cnf(496,plain,
% 118.25/118.91 (P1(x4961,f9(f11(x4961),f12(x4962,x4961)))),
% 118.25/118.91 inference(rename_variables,[],[494])).
% 118.25/118.91 cnf(497,plain,
% 118.25/118.91 (P1(x4971,f9(f11(x4972),f12(x4973,x4972)))+~E(x4972,x4971)),
% 118.25/118.91 inference(scs_inference,[],[80,494,496,23,22])).
% 118.25/118.91 cnf(502,plain,
% 118.25/118.91 (E(f6(x5021,f11(f12(x5022,x5021))),f12(x5022,x5021))),
% 118.25/118.91 inference(scs_inference,[],[480,31,48])).
% 118.25/118.91 cnf(503,plain,
% 118.25/118.91 (E(f12(x5031,x5032),f6(x5032,f11(f12(x5031,x5032))))),
% 118.25/118.91 inference(scs_inference,[],[502,2])).
% 118.25/118.91 cnf(508,plain,
% 118.25/118.91 (~P1(f11(f6(x5081,f11(f12(x5082,x5081)))),f11(f2(x5083,f11(f12(x5082,x5081)))))),
% 118.25/118.91 inference(scs_inference,[],[503,31,460])).
% 118.25/118.91 cnf(509,plain,
% 118.25/118.91 (P1(x5091,f6(x5092,f11(f12(x5091,x5092))))),
% 118.25/118.91 inference(scs_inference,[],[60,503,23])).
% 118.25/118.91 cnf(512,plain,
% 118.25/118.91 (~P1(f12(x5121,x5122),f9(x5123,f11(f2(x5124,f11(x5121)))))),
% 118.25/118.91 inference(scs_inference,[],[464,31,50])).
% 118.25/118.91 cnf(515,plain,
% 118.25/118.91 (~E(f2(x5151,f11(a1)),f10(x5152))),
% 118.25/118.91 inference(scs_inference,[],[472,31,76])).
% 118.25/118.91 cnf(517,plain,
% 118.25/118.91 (~P1(f13(x5171,f11(x5172)),f9(f11(f2(x5173,f11(x5172))),x5174))),
% 118.25/118.91 inference(scs_inference,[],[481,31,51])).
% 118.25/118.91 cnf(532,plain,
% 118.25/118.91 (~E(f10(x5321),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,222,23])).
% 118.25/118.91 cnf(537,plain,
% 118.25/118.91 (P1(f14(a1),f2(f12(x5371,f14(a1)),f11(f9(f7(a3),f7(a8)))))),
% 118.25/118.91 inference(scs_inference,[],[92,59,31,49])).
% 118.25/118.91 cnf(538,plain,
% 118.25/118.91 (~E(f7(f14(a1)),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,192,23])).
% 118.25/118.91 cnf(541,plain,
% 118.25/118.91 (~E(f13(x5411,f11(x5412)),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,403,23])).
% 118.25/118.91 cnf(544,plain,
% 118.25/118.91 (~E(f13(f11(x5441),x5442),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,424,23])).
% 118.25/118.91 cnf(547,plain,
% 118.25/118.91 (~E(f9(f12(x5471,x5472),f11(x5472)),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,471,23])).
% 118.25/118.91 cnf(552,plain,
% 118.25/118.91 (~E(f9(f11(x5521),f12(x5522,x5521)),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,494,23])).
% 118.25/118.91 cnf(554,plain,
% 118.25/118.91 (P1(a1,f13(x5541,f10(x5542)))),
% 118.25/118.91 inference(scs_inference,[],[65,34,42])).
% 118.25/118.91 cnf(555,plain,
% 118.25/118.91 (~E(f13(x5551,f10(x5552)),a1)),
% 118.25/118.91 inference(scs_inference,[],[28,554,23])).
% 118.25/118.91 cnf(566,plain,
% 118.25/118.91 (P1(f14(f14(a1)),f10(x5661))),
% 118.25/118.91 inference(scs_inference,[],[80,34,38])).
% 118.25/118.91 cnf(567,plain,
% 118.25/118.91 (P1(x5671,f10(x5672))+~E(f14(f14(a1)),x5671)),
% 118.25/118.91 inference(scs_inference,[],[566,22])).
% 118.25/118.91 cnf(571,plain,
% 118.25/118.91 (P1(a1,f13(f10(x5711),x5712))),
% 118.25/118.91 inference(scs_inference,[],[65,34,43])).
% 118.25/118.91 cnf(585,plain,
% 118.25/118.91 (~E(f9(f12(x5851,x5852),f11(x5852)),f14(a1))),
% 118.25/118.91 inference(scs_inference,[],[68,471,23])).
% 118.25/118.91 cnf(587,plain,
% 118.25/118.91 (~E(f13(x5871,f10(x5872)),f14(a1))),
% 118.25/118.91 inference(scs_inference,[],[68,554,23])).
% 118.25/118.91 cnf(589,plain,
% 118.25/118.91 (~E(f14(f11(f12(x5891,x5892))),f14(a1))),
% 118.25/118.91 inference(scs_inference,[],[68,480,23])).
% 118.25/118.91 cnf(591,plain,
% 118.25/118.91 (~E(f9(f11(x5911),f12(x5912,x5911)),f14(a1))),
% 118.25/118.91 inference(scs_inference,[],[68,494,23])).
% 118.25/118.91 cnf(593,plain,
% 118.25/118.91 (~E(f13(f10(x5931),x5932),f14(a1))),
% 118.25/118.91 inference(scs_inference,[],[68,571,23])).
% 118.25/118.91 cnf(599,plain,
% 118.25/118.91 (P1(f14(a1),f10(x5991))),
% 118.25/118.91 inference(scs_inference,[],[68,34,38])).
% 118.25/118.91 cnf(600,plain,
% 118.25/118.91 (P1(x6001,f10(x6002))+~E(f14(a1),x6001)),
% 118.25/118.91 inference(scs_inference,[],[599,22])).
% 118.25/118.91 cnf(618,plain,
% 118.25/118.91 (~P1(x6181,f7(f10(x6182)))),
% 118.25/118.91 inference(scs_inference,[],[65,28,34,46])).
% 118.25/118.91 cnf(619,plain,
% 118.25/118.91 (P1(f5(x6191,f10(x6192)),f10(x6192))),
% 118.25/118.91 inference(scs_inference,[],[618,41])).
% 118.25/118.91 cnf(621,plain,
% 118.25/118.91 (~P1(x6211,f5(x6211,f10(x6212)))),
% 118.25/118.91 inference(scs_inference,[],[618,41,54])).
% 118.25/118.91 cnf(624,plain,
% 118.25/118.91 (~P1(x6241,f7(f10(x6242)))),
% 118.25/118.91 inference(rename_variables,[],[618])).
% 118.25/118.91 cnf(626,plain,
% 118.25/118.91 (P3(f7(f10(x6261)),x6262)),
% 118.25/118.91 inference(scs_inference,[],[618,624,41,54,48,38])).
% 118.25/118.91 cnf(638,plain,
% 118.25/118.91 (P3(f5(x6381,f10(x6382)),x6382)),
% 118.25/118.91 inference(scs_inference,[],[619,37])).
% 118.25/118.91 cnf(651,plain,
% 118.25/118.91 (P2(x6511,a1)+~E(f7(f10(x6512)),x6511)),
% 118.25/118.91 inference(scs_inference,[],[65,626,68,619,37,39,40,38,24,22,26])).
% 118.25/118.91 cnf(661,plain,
% 118.25/118.91 (P1(x6611,f10(x6612))+~E(f5(x6613,f10(x6612)),x6611)),
% 118.25/118.91 inference(scs_inference,[],[65,638,619,40,22])).
% 118.25/118.91 cnf(718,plain,
% 118.25/118.91 (~E(f13(f10(x7181),x7182),f2(x7183,f10(x7184)))),
% 118.25/118.91 inference(scs_inference,[],[221,571,23])).
% 118.25/118.91 cnf(732,plain,
% 118.25/118.91 (P1(f9(f7(a3),f7(a8)),f2(f7(f14(a1)),f10(f7(f9(a3,a8)))))),
% 118.25/118.91 inference(scs_inference,[],[29,192,37,49])).
% 118.25/118.91 cnf(742,plain,
% 118.25/118.91 (P1(x7421,f14(f11(f12(x7421,x7422))))),
% 118.25/118.91 inference(scs_inference,[],[503,509,76,44])).
% 118.25/118.91 cnf(752,plain,
% 118.25/118.91 (~E(f13(x7521,f10(x7522)),f11(f12(x7523,x7524)))),
% 118.25/118.91 inference(scs_inference,[],[302,554,23])).
% 118.25/118.91 cnf(777,plain,
% 118.25/118.91 (~P1(f10(a1),f11(a1))),
% 118.25/118.91 inference(scs_inference,[],[306,76,31])).
% 118.25/118.91 cnf(836,plain,
% 118.25/118.91 (~E(f9(f11(x8361),f12(x8362,x8361)),f2(x8363,f11(x8361)))),
% 118.25/118.91 inference(scs_inference,[],[444,494,23])).
% 118.25/118.91 cnf(855,plain,
% 118.25/118.91 (P1(a1,f9(f10(x8551),f10(x8552)))),
% 118.25/118.91 inference(scs_inference,[],[222,228,55])).
% 118.25/118.91 cnf(856,plain,
% 118.25/118.91 (~E(f9(f10(x8561),f10(x8562)),f14(a1))),
% 118.25/118.91 inference(scs_inference,[],[68,855,23])).
% 118.25/118.91 cnf(867,plain,
% 118.25/118.91 (~E(f14(a1),f10(x8671))),
% 118.25/118.91 inference(scs_inference,[],[222,28,335,39])).
% 118.25/118.91 cnf(869,plain,
% 118.25/118.91 (~E(a1,f10(x8691))),
% 118.25/118.91 inference(scs_inference,[],[222,68,341,39])).
% 118.25/118.91 cnf(870,plain,
% 118.25/118.91 (E(f7(f6(x8701,f11(f12(x8702,x8701)))),f7(f12(x8702,x8701)))),
% 118.25/118.91 inference(scs_inference,[],[503,4,2])).
% 118.25/118.91 cnf(887,plain,
% 118.25/118.91 (~E(f13(x8871,f10(x8872)),f7(f10(x8873)))),
% 118.25/118.91 inference(scs_inference,[],[618,554,23])).
% 118.25/118.91 cnf(896,plain,
% 118.25/118.91 (~E(f12(x8961,x8962),f7(f10(x8963)))),
% 118.25/118.91 inference(scs_inference,[],[618,59,23])).
% 118.25/118.91 cnf(901,plain,
% 118.25/118.91 (~P1(f14(a1),f11(f9(a3,a8)))),
% 118.25/118.91 inference(scs_inference,[],[199,4,31])).
% 118.25/118.91 cnf(902,plain,
% 118.25/118.91 (~E(f13(f11(x9021),x9022),f7(f10(x9023)))),
% 118.25/118.91 inference(scs_inference,[],[618,424,23])).
% 118.25/118.91 cnf(911,plain,
% 118.25/118.91 (~E(f9(f11(x9111),f12(x9112,x9111)),f7(f10(x9113)))),
% 118.25/118.91 inference(scs_inference,[],[618,494,23])).
% 118.25/118.91 cnf(914,plain,
% 118.25/118.91 (~E(f11(x9141),f7(f10(x9142)))),
% 118.25/118.91 inference(scs_inference,[],[618,58,23])).
% 118.25/118.91 cnf(919,plain,
% 118.25/118.91 (~E(f10(x9191),f5(a1,f10(x9192)))),
% 118.25/118.91 inference(scs_inference,[],[621,222,23])).
% 118.25/118.91 cnf(931,plain,
% 118.25/118.91 (~E(f10(x9311),f5(f14(a1),f10(x9312)))),
% 118.25/118.91 inference(scs_inference,[],[621,599,23])).
% 118.25/118.91 cnf(943,plain,
% 118.25/118.91 (~E(f12(x9431,x9432),f5(x9432,f10(x9433)))),
% 118.25/118.91 inference(scs_inference,[],[621,59,23])).
% 118.25/118.91 cnf(946,plain,
% 118.25/118.91 (~E(f12(x9461,x9462),f5(x9461,f10(x9463)))),
% 118.25/118.91 inference(scs_inference,[],[621,60,23])).
% 118.25/118.91 cnf(958,plain,
% 118.25/118.91 (~E(f9(f12(x9581,x9582),f11(x9582)),f5(x9582,f10(x9583)))),
% 118.25/118.91 inference(scs_inference,[],[621,471,23])).
% 118.25/118.91 cnf(964,plain,
% 118.25/118.91 (~E(f11(x9641),f5(x9641,f10(x9642)))),
% 118.25/118.91 inference(scs_inference,[],[621,58,23])).
% 118.25/118.91 cnf(1088,plain,
% 118.25/118.91 (~E(f12(f10(a1),x10881),f11(a1))),
% 118.25/118.92 inference(scs_inference,[],[777,60,23])).
% 118.25/118.92 cnf(1097,plain,
% 118.25/118.92 (~E(f11(f10(a1)),f11(a1))),
% 118.25/118.92 inference(scs_inference,[],[777,58,23])).
% 118.25/118.92 cnf(1117,plain,
% 118.25/118.92 (E(f11(f6(x11171,f11(f12(x11172,x11171)))),f11(f12(x11172,x11171)))),
% 118.25/118.92 inference(scs_inference,[],[503,13,2])).
% 118.25/118.92 cnf(1134,plain,
% 118.25/118.92 (~E(f10(x11341),f11(f9(a3,a8)))),
% 118.25/118.92 inference(scs_inference,[],[901,599,23])).
% 118.25/118.92 cnf(1200,plain,
% 118.25/118.92 (~P1(x12001,f5(x12002,f10(a1)))),
% 118.25/118.92 inference(scs_inference,[],[28,638,39])).
% 118.25/118.92 cnf(1203,plain,
% 118.25/118.92 (~E(f13(f10(x12031),x12032),a1)),
% 118.25/118.92 inference(scs_inference,[],[28,638,571,39,23])).
% 118.25/118.92 cnf(1207,plain,
% 118.25/118.92 (~P1(x12071,f5(x12072,f10(a1)))),
% 118.25/118.92 inference(rename_variables,[],[1200])).
% 118.25/118.92 cnf(1209,plain,
% 118.25/118.92 (P3(f5(x12091,f10(a1)),x12092)),
% 118.25/118.92 inference(scs_inference,[],[1200,1207,48,38])).
% 118.25/118.92 cnf(1213,plain,
% 118.25/118.92 (~E(f9(f10(x12131),f10(x12132)),a1)),
% 118.25/118.92 inference(scs_inference,[],[28,29,855,1200,1207,48,38,24,23])).
% 118.25/118.92 cnf(1326,plain,
% 118.25/118.92 (~P1(f11(f12(x13261,x13262)),f11(a1))),
% 118.25/118.92 inference(scs_inference,[],[589,19,31])).
% 118.25/118.92 cnf(1386,plain,
% 118.25/118.92 (P1(f13(x13861,f12(x13862,x13863)),f12(x13864,f13(x13861,f6(x13863,f11(f12(x13862,x13863))))))),
% 118.25/118.92 inference(scs_inference,[],[503,35,6])).
% 118.25/118.92 cnf(1462,plain,
% 118.25/118.92 (P1(f4(f9(f7(a3),f7(a8)),f7(f9(a3,a8))),f7(a3))),
% 118.25/118.92 inference(scs_inference,[],[29,38,51])).
% 118.25/118.92 cnf(1515,plain,
% 118.25/118.92 (P3(f13(f14(f14(a1)),f14(f14(a1))),x15151)),
% 118.25/118.92 inference(scs_inference,[],[80,38,57])).
% 118.25/118.92 cnf(1531,plain,
% 118.25/118.92 (~P1(x15311,f7(f13(x15312,f10(x15313))))),
% 118.25/118.92 inference(scs_inference,[],[222,28,42,46])).
% 118.25/118.92 cnf(1532,plain,
% 118.25/118.92 (~P1(x15321,f5(x15321,f13(x15322,f10(x15323))))),
% 118.25/118.92 inference(scs_inference,[],[1531,54])).
% 118.25/118.92 cnf(1547,plain,
% 118.25/118.92 (P1(x15471,f13(x15472,f7(f14(f14(a1)))))),
% 118.25/118.92 inference(scs_inference,[],[80,42,41])).
% 118.25/118.92 cnf(1606,plain,
% 118.25/118.92 (P3(f9(x16061,f5(x16062,f10(a1))),x16063)),
% 118.25/118.92 inference(scs_inference,[],[1200,50,38])).
% 118.25/118.92 cnf(1653,plain,
% 118.25/118.92 (P2(f5(x16531,f10(a1)),f5(x16531,f10(a1)))),
% 118.25/118.92 inference(scs_inference,[],[1209,40])).
% 118.25/118.92 cnf(1657,plain,
% 118.25/118.92 (P2(x16571,f5(x16572,f10(a1)))+~E(f5(x16572,f10(a1)),x16571)),
% 118.25/118.92 inference(scs_inference,[],[1209,40,26])).
% 118.25/118.92 cnf(1688,plain,
% 118.25/118.92 (P2(f5(x16881,f10(a1)),x16882)+~E(f5(x16881,f10(a1)),x16882)),
% 118.25/118.92 inference(scs_inference,[],[1653,27])).
% 118.25/118.92 cnf(1715,plain,
% 118.25/118.92 (~P1(f11(f12(x17151,x17152)),f9(f9(x17153,f11(a1)),x17154))),
% 118.25/118.92 inference(scs_inference,[],[1326,51,50])).
% 118.25/118.92 cnf(1817,plain,
% 118.25/118.92 (~P1(x18171,f2(a1,x18172))),
% 118.25/118.92 inference(scs_inference,[],[65,80,52,39])).
% 118.25/118.92 cnf(1818,plain,
% 118.25/118.92 (~P1(x18181,f14(f2(a1,x18182)))),
% 118.25/118.92 inference(scs_inference,[],[1817,48])).
% 118.25/118.92 cnf(1819,plain,
% 118.25/118.92 (~P1(x18191,f2(a1,x18192))),
% 118.25/118.92 inference(rename_variables,[],[1817])).
% 118.25/118.92 cnf(1821,plain,
% 118.25/118.92 (P3(f2(a1,x18211),x18212)),
% 118.25/118.92 inference(scs_inference,[],[1817,1819,48,38])).
% 118.25/118.92 cnf(1834,plain,
% 118.25/118.92 (~P1(x18341,f14(f2(a1,x18342)))),
% 118.25/118.92 inference(rename_variables,[],[1818])).
% 118.25/118.92 cnf(1836,plain,
% 118.25/118.92 (P3(f14(f2(a1,x18361)),x18362)),
% 118.25/118.92 inference(scs_inference,[],[1818,1834,48,38])).
% 118.25/118.92 cnf(1840,plain,
% 118.25/118.92 (P2(f2(a1,x18401),a1)),
% 118.25/118.92 inference(scs_inference,[],[29,65,1821,1818,1834,48,38,24,40])).
% 118.25/118.92 cnf(1844,plain,
% 118.25/118.92 (P2(x18441,a1)+~E(f2(a1,x18442),x18441)),
% 118.25/118.92 inference(scs_inference,[],[29,65,1821,1818,1834,48,38,24,40,26])).
% 118.25/118.92 cnf(1862,plain,
% 118.25/118.92 (P2(f2(a1,x18621),x18622)+~E(a1,x18622)),
% 118.25/118.92 inference(scs_inference,[],[83,1606,1840,40,26,27])).
% 118.25/118.92 cnf(1889,plain,
% 118.25/118.92 (P3(f2(f7(f13(x18891,f10(x18892))),x18893),x18894)),
% 118.25/118.92 inference(scs_inference,[],[1531,52,38])).
% 118.25/118.92 cnf(1909,plain,
% 118.25/118.92 (~E(f11(x19091),f5(x19091,f13(x19092,f10(x19093))))),
% 118.25/118.92 inference(scs_inference,[],[1532,58,23])).
% 118.25/118.92 cnf(1974,plain,
% 118.25/118.92 (P3(f2(f7(f10(x19741)),x19742),x19743)),
% 118.25/118.92 inference(scs_inference,[],[618,52,38])).
% 118.25/118.92 cnf(2025,plain,
% 118.25/118.92 (~P1(x20251,f14(f2(f7(f10(x20252)),x20253)))),
% 118.25/118.92 inference(scs_inference,[],[618,52,48])).
% 118.25/118.92 cnf(2121,plain,
% 118.25/118.92 (~E(x21211,f7(f10(x21212)))+~P1(x21213,f2(x21211,x21214))),
% 118.25/118.92 inference(scs_inference,[],[618,52,23])).
% 118.25/118.92 cnf(2140,plain,
% 118.25/118.92 (P1(f5(f4(f9(f7(a3),f7(a8)),f7(f9(a3,a8))),f9(a3,a8)),f9(a3,a8))),
% 118.25/118.92 inference(scs_inference,[],[29,53,41])).
% 118.25/118.92 cnf(2157,plain,
% 118.25/118.92 (P3(x21571,f9(f7(f14(a1)),f7(f14(a1))))),
% 118.25/118.92 inference(scs_inference,[],[192,53,55])).
% 118.25/118.92 cnf(2246,plain,
% 118.25/118.92 (~E(f10(x22461),f2(a1,x22462))),
% 118.25/118.92 inference(scs_inference,[],[1817,638,222,39,23])).
% 118.25/118.92 cnf(2249,plain,
% 118.25/118.92 (~E(f13(x22491,f10(x22492)),f2(a1,x22493))),
% 118.25/118.92 inference(scs_inference,[],[1817,554,23])).
% 118.25/118.92 cnf(2252,plain,
% 118.25/118.92 (~E(f13(f10(x22521),x22522),f2(a1,x22523))),
% 118.25/118.92 inference(scs_inference,[],[1817,571,23])).
% 118.25/118.92 cnf(2255,plain,
% 118.25/118.92 (~E(f9(f10(x22551),f10(x22552)),f2(a1,x22553))),
% 118.25/118.92 inference(scs_inference,[],[1817,855,23])).
% 118.25/118.92 cnf(2258,plain,
% 118.25/118.92 (~E(f7(f14(a1)),f2(a1,x22581))),
% 118.25/118.92 inference(scs_inference,[],[1817,192,23])).
% 118.25/118.92 cnf(2275,plain,
% 118.25/118.92 (~E(f12(x22751,x22752),f2(a1,x22753))),
% 118.25/118.92 inference(scs_inference,[],[1817,59,23])).
% 118.25/118.92 cnf(2279,plain,
% 118.25/118.92 (~E(f9(f12(x22791,x22792),f11(x22792)),f2(a1,x22793))),
% 118.25/118.92 inference(scs_inference,[],[1817,471,23])).
% 118.25/118.92 cnf(2282,plain,
% 118.25/118.92 (~E(f9(f11(x22821),f12(x22822,x22821)),f2(a1,x22823))),
% 118.25/118.92 inference(scs_inference,[],[1817,494,23])).
% 118.25/118.92 cnf(2285,plain,
% 118.25/118.92 (~E(f13(x22851,f11(x22852)),f2(a1,x22853))),
% 118.25/118.92 inference(scs_inference,[],[1817,403,23])).
% 118.25/118.92 cnf(2288,plain,
% 118.25/118.92 (~E(f13(f11(x22881),x22882),f2(a1,x22883))),
% 118.25/118.92 inference(scs_inference,[],[1817,424,23])).
% 118.25/118.92 cnf(2290,plain,
% 118.25/118.92 (P1(x22901,f14(f12(f12(x22901,x22902),x22903)))),
% 118.25/118.92 inference(scs_inference,[],[503,509,114,44])).
% 118.25/118.92 cnf(2307,plain,
% 118.25/118.92 (~E(f10(x23071),f14(f2(a1,x23072)))),
% 118.25/118.92 inference(scs_inference,[],[1818,222,23])).
% 118.25/118.92 cnf(2322,plain,
% 118.25/118.92 (~E(f12(x23221,x23222),f14(f2(a1,x23223)))),
% 118.25/118.92 inference(scs_inference,[],[1818,59,23])).
% 118.25/118.92 cnf(2337,plain,
% 118.25/118.92 (~E(f11(x23371),f14(f2(a1,x23372)))),
% 118.25/118.92 inference(scs_inference,[],[1818,58,23])).
% 118.25/118.92 cnf(2341,plain,
% 118.25/118.92 (P2(f2(a1,x23411),f2(a1,x23411))),
% 118.25/118.92 inference(scs_inference,[],[1821,40])).
% 118.25/118.92 cnf(2345,plain,
% 118.25/118.92 (P2(x23451,f2(a1,x23452))+~E(f2(a1,x23452),x23451)),
% 118.25/118.92 inference(scs_inference,[],[1821,40,26])).
% 118.25/118.92 cnf(2354,plain,
% 118.25/118.92 (P2(f2(a1,x23541),x23542)+~E(f2(a1,x23541),x23542)),
% 118.25/118.92 inference(scs_inference,[],[1821,65,2341,40,26,27])).
% 118.25/118.92 cnf(2590,plain,
% 118.25/118.92 (~E(f14(f14(a1)),f10(x25901))),
% 118.25/118.92 inference(scs_inference,[],[222,28,356,39])).
% 118.25/118.92 cnf(2591,plain,
% 118.25/118.92 (~E(f14(a1),x25911)+P1(x25911,f13(f10(x25912),x25913))),
% 118.25/118.92 inference(scs_inference,[],[600,43])).
% 118.25/118.92 cnf(2592,plain,
% 118.25/118.92 (P1(f14(a1),f13(f10(x25921),x25922))),
% 118.25/118.92 inference(equality_inference,[],[2591])).
% 118.25/118.92 cnf(2615,plain,
% 118.25/118.92 (P3(x26151,a1)+~E(f7(f10(x26152)),x26151)),
% 118.25/118.92 inference(scs_inference,[],[651,33])).
% 118.25/118.92 cnf(2678,plain,
% 118.25/118.92 (P3(x26781,a1)+~E(f2(a1,x26782),x26781)),
% 118.25/118.92 inference(scs_inference,[],[1844,33])).
% 118.25/118.92 cnf(2681,plain,
% 118.25/118.92 (P3(x26811,f2(a1,x26812))+~E(a1,x26811)),
% 118.25/118.92 inference(scs_inference,[],[1862,32])).
% 118.25/118.92 cnf(2691,plain,
% 118.25/118.92 (~E(f7(f10(x26911)),f10(x26912))),
% 118.25/118.92 inference(scs_inference,[],[222,28,2615,39])).
% 118.25/118.92 cnf(2692,plain,
% 118.25/118.92 (~E(f2(a1,x26921),f10(x26922))),
% 118.25/118.92 inference(scs_inference,[],[222,28,2678,39])).
% 118.25/118.92 cnf(2717,plain,
% 118.25/118.92 (P1(f5(x27171,f13(f7(f10(x27172)),f10(x27173))),f10(x27173))),
% 118.25/118.92 inference(scs_inference,[],[1531,618,41,57])).
% 118.25/118.92 cnf(2766,plain,
% 118.25/118.92 (~P1(x27661,f2(f14(a1),x27662))),
% 118.25/118.92 inference(scs_inference,[],[28,48,52])).
% 118.25/118.92 cnf(2767,plain,
% 118.25/118.92 (P3(f2(f14(a1),x27671),x27672)),
% 118.25/118.92 inference(scs_inference,[],[2766,38])).
% 118.25/118.92 cnf(2771,plain,
% 118.25/118.92 (P3(f5(x27711,f10(x27712)),x27713)+~E(x27712,x27713)),
% 118.25/118.92 inference(scs_inference,[],[29,638,2766,38,24,25])).
% 118.25/118.92 cnf(2773,plain,
% 118.25/118.92 (~P1(x27731,f14(f9(x27732,a1)))),
% 118.25/118.92 inference(scs_inference,[],[28,48,50])).
% 118.25/118.92 cnf(2774,plain,
% 118.25/118.92 (P3(f14(f9(x27741,a1)),x27742)),
% 118.25/118.92 inference(scs_inference,[],[2773,38])).
% 118.25/118.92 cnf(2775,plain,
% 118.25/118.92 (~P1(x27751,f14(f9(x27752,a1)))),
% 118.25/118.92 inference(rename_variables,[],[2773])).
% 118.25/118.92 cnf(2777,plain,
% 118.25/118.92 (~P1(f10(x27771),f9(x27772,a1))),
% 118.25/118.92 inference(scs_inference,[],[222,2773,2775,38,44])).
% 118.25/118.92 cnf(2792,plain,
% 118.25/118.92 (~P1(x27921,f9(f14(a1),x27922))),
% 118.25/118.92 inference(scs_inference,[],[28,48,51])).
% 118.25/118.92 cnf(2793,plain,
% 118.25/118.92 (P3(f9(f14(a1),x27931),x27932)),
% 118.25/118.92 inference(scs_inference,[],[2792,38])).
% 118.25/118.92 cnf(2801,plain,
% 118.25/118.92 (~E(f14(a1),f7(a3))),
% 118.25/118.92 inference(scs_inference,[],[29,65,2774,2792,38,24,40,7])).
% 118.25/118.92 cnf(2846,plain,
% 118.25/118.92 (~E(f7(a3),f14(a1))),
% 118.25/118.92 inference(scs_inference,[],[2801,1515,31,34,76])).
% 118.25/118.92 cnf(2855,plain,
% 118.25/118.92 (P1(x28551,f6(x28551,f11(f12(x28551,x28552))))),
% 118.25/118.92 inference(scs_inference,[],[2801,742,1515,2777,2592,31,34,76,42,43,52,56,47])).
% 118.25/118.92 cnf(2857,plain,
% 118.25/118.92 (P1(x28571,f7(f9(f14(a1),x28572)))),
% 118.25/118.92 inference(scs_inference,[],[2801,742,1515,2777,2592,2792,31,34,76,42,43,52,56,47,41])).
% 118.25/118.92 cnf(2860,plain,
% 118.25/118.92 (~E(f2(a1,x28601),f12(x28602,x28603))),
% 118.25/118.92 inference(scs_inference,[],[2801,2275,742,1515,2777,2592,2792,31,34,76,42,43,52,56,47,41,2])).
% 118.25/118.92 cnf(2861,plain,
% 118.25/118.92 (~P1(f10(x28611),f9(x28612,f9(x28613,a1)))),
% 118.25/118.92 inference(scs_inference,[],[2801,2275,742,1515,2777,2592,2792,31,34,76,42,43,52,56,47,41,2,50])).
% 118.25/118.92 cnf(2863,plain,
% 118.25/118.92 (~P1(f10(x28631),f9(f9(x28632,a1),x28633))),
% 118.25/118.92 inference(scs_inference,[],[2801,2275,742,1515,2777,2592,2792,31,34,76,42,43,52,56,47,41,2,50,51])).
% 118.25/118.92 cnf(2867,plain,
% 118.25/118.92 (P1(f6(x28671,f11(f12(x28671,x28672))),f11(f12(x28671,x28672)))),
% 118.25/118.92 inference(scs_inference,[],[2801,2275,742,1515,2777,2592,2792,502,31,34,76,42,43,52,56,47,41,2,50,51,30,48])).
% 118.25/118.92 cnf(2896,plain,
% 118.25/118.92 (P1(x28961,f7(f2(a1,x28962)))),
% 118.25/118.92 inference(scs_inference,[],[1326,1817,52,41])).
% 118.25/118.92 cnf(2901,plain,
% 118.25/118.92 (P1(f9(f14(a1),x29011),f10(x29012))),
% 118.25/118.92 inference(scs_inference,[],[2246,2793,1326,1817,52,41,31,34])).
% 118.25/118.92 cnf(2905,plain,
% 118.25/118.92 (P1(f14(f14(a1)),f13(f10(x29051),x29052))),
% 118.25/118.92 inference(scs_inference,[],[2246,2793,566,1326,1817,52,41,31,34,42,43])).
% 118.25/118.92 cnf(2927,plain,
% 118.25/118.92 (P1(f9(f14(a1),x29271),f13(f10(x29272),x29273))),
% 118.25/118.92 inference(scs_inference,[],[2901,777,52,43])).
% 118.25/118.92 cnf(2929,plain,
% 118.25/118.92 (P1(x29291,f7(a1))),
% 118.25/118.92 inference(scs_inference,[],[2901,777,28,52,43,41])).
% 118.25/118.92 cnf(2932,plain,
% 118.25/118.92 (P1(f14(f9(x29321,a1)),f10(x29322))),
% 118.25/118.92 inference(scs_inference,[],[2901,2774,777,28,52,43,41,34])).
% 118.25/118.92 cnf(2934,plain,
% 118.25/118.92 (P1(f9(f14(a1),x29341),f13(x29342,f10(x29343)))),
% 118.25/118.92 inference(scs_inference,[],[2901,2774,777,28,52,43,41,34,42])).
% 118.25/118.92 cnf(2944,plain,
% 118.25/118.92 (~E(f14(a1),f12(x29441,x29442))),
% 118.25/118.92 inference(scs_inference,[],[2846,90,2901,2774,777,28,52,43,41,34,42,50,31,56,51,2])).
% 118.25/118.92 cnf(2950,plain,
% 118.25/118.92 (P1(f9(f14(a1),x29501),f9(f10(x29502),f10(x29502)))),
% 118.25/118.92 inference(scs_inference,[],[2846,90,2901,2896,2774,2777,777,28,52,43,41,34,42,50,31,56,51,2,45,49,55])).
% 118.25/118.92 cnf(2964,plain,
% 118.25/118.92 (P1(x29641,f13(f7(a1),x29642))),
% 118.25/118.92 inference(scs_inference,[],[2929,160,52,43])).
% 118.25/118.92 cnf(2968,plain,
% 118.25/118.92 (P1(f2(f14(a1),x29681),f10(x29682))),
% 118.25/118.92 inference(scs_inference,[],[2929,2767,160,52,43,50,34])).
% 118.25/118.92 cnf(2970,plain,
% 118.25/118.92 (P1(x29701,f13(x29702,f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2929,2767,160,52,43,50,34,42])).
% 118.25/118.92 cnf(2972,plain,
% 118.25/118.92 (~P1(x29721,f2(x29722,f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2929,2767,160,52,43,50,34,42,56])).
% 118.25/118.92 cnf(2978,plain,
% 118.25/118.92 (~E(f14(a1),f11(x29781))),
% 118.25/118.92 inference(scs_inference,[],[2692,118,2929,2767,160,52,43,50,34,42,56,31,51,2])).
% 118.25/118.92 cnf(2980,plain,
% 118.25/118.92 (P1(x29801,f7(a1))),
% 118.25/118.92 inference(rename_variables,[],[2929])).
% 118.25/118.92 cnf(2984,plain,
% 118.25/118.92 (P1(x29841,f7(a1))),
% 118.25/118.92 inference(rename_variables,[],[2929])).
% 118.25/118.92 cnf(2990,plain,
% 118.25/118.92 (P1(x29901,f9(f7(a1),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2692,118,2929,2980,2984,2861,2767,160,52,43,50,34,42,56,31,51,2,46,44,45,57,55])).
% 118.25/118.92 cnf(2992,plain,
% 118.25/118.92 (~P3(f7(a1),f9(x29921,f9(x29922,a1)))),
% 118.25/118.92 inference(scs_inference,[],[2692,118,2929,2980,2984,2861,2767,160,52,43,50,34,42,56,31,51,2,46,44,45,57,55,39])).
% 118.25/118.92 cnf(2993,plain,
% 118.25/118.92 (P1(x29931,f7(a1))),
% 118.25/118.92 inference(rename_variables,[],[2929])).
% 118.25/118.92 cnf(2995,plain,
% 118.25/118.92 (P1(f7(a1),f6(f7(a1),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2692,118,2929,2980,2984,2861,2767,160,52,43,50,34,42,56,31,51,2,46,44,45,57,55,39,47])).
% 118.25/118.92 cnf(2997,plain,
% 118.25/118.92 (~E(f7(a1),f9(x29971,f9(x29972,a1)))),
% 118.25/118.92 inference(scs_inference,[],[2692,118,2929,2980,2984,2993,2861,2767,160,52,43,50,34,42,56,31,51,2,46,44,45,57,55,39,47,23])).
% 118.25/118.92 cnf(2999,plain,
% 118.25/118.92 (~P1(x29991,f2(f2(a1,x29992),x29993))),
% 118.25/118.92 inference(scs_inference,[],[1817,52])).
% 118.25/118.92 cnf(3001,plain,
% 118.25/118.92 (P1(f14(f9(x30011,a1)),f13(f10(x30012),x30013))),
% 118.25/118.92 inference(scs_inference,[],[2932,1817,52,43])).
% 118.25/118.92 cnf(3003,plain,
% 118.25/118.92 (~P1(x30031,f9(x30032,f14(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2932,68,1817,52,43,50])).
% 118.25/118.92 cnf(3005,plain,
% 118.25/118.92 (~P1(f14(f9(x30051,a1)),f2(x30052,f10(x30053)))),
% 118.25/118.92 inference(scs_inference,[],[2932,68,1817,52,43,50,56])).
% 118.25/118.92 cnf(3007,plain,
% 118.25/118.92 (P1(f5(x30071,f10(a1)),f10(x30072))),
% 118.25/118.92 inference(scs_inference,[],[2932,1209,68,1817,52,43,50,56,34])).
% 118.25/118.92 cnf(3011,plain,
% 118.25/118.92 (~P1(x30111,f9(f2(a1,x30112),x30113))),
% 118.25/118.92 inference(scs_inference,[],[2932,1209,68,1817,52,43,50,56,34,42,51])).
% 118.25/118.92 cnf(3015,plain,
% 118.25/118.92 (~E(a1,f11(x30151))),
% 118.25/118.92 inference(scs_inference,[],[2860,72,2932,1209,68,1817,52,43,50,56,34,42,51,31,2])).
% 118.25/118.92 cnf(3021,plain,
% 118.25/118.92 (P1(f14(f9(x30211,a1)),f9(f10(x30212),f10(x30212)))),
% 118.25/118.92 inference(scs_inference,[],[2860,72,2932,2929,1209,68,1817,52,43,50,56,34,42,51,31,2,44,45,55])).
% 118.25/118.92 cnf(3023,plain,
% 118.25/118.92 (~P1(f10(x30231),f13(f9(f9(x30232,a1),x30233),f14(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2860,72,2932,2863,2929,1209,68,1817,52,43,50,56,34,42,51,31,2,44,45,55,57])).
% 118.25/118.92 cnf(3036,plain,
% 118.25/118.92 (P1(f5(x30361,f10(a1)),f13(f10(x30362),x30363))),
% 118.25/118.92 inference(scs_inference,[],[3007,43])).
% 118.25/118.92 cnf(3038,plain,
% 118.25/118.92 (P1(f5(x30381,f10(a1)),f13(x30382,f10(x30383)))),
% 118.25/118.92 inference(scs_inference,[],[3007,43,42])).
% 118.25/118.92 cnf(3042,plain,
% 118.25/118.92 (~P1(x30421,f9(x30422,f2(a1,x30423)))),
% 118.25/118.92 inference(scs_inference,[],[3007,1817,43,42,56,50])).
% 118.25/118.92 cnf(3044,plain,
% 118.25/118.92 (P1(f14(f2(a1,x30441)),f10(x30442))),
% 118.25/118.92 inference(scs_inference,[],[3007,1836,1817,43,42,56,50,34])).
% 118.25/118.92 cnf(3048,plain,
% 118.25/118.92 (~P1(x30481,f9(a1,x30482))),
% 118.25/118.92 inference(scs_inference,[],[234,3007,1836,1817,28,43,42,56,50,34,31,51])).
% 118.25/118.92 cnf(3051,plain,
% 118.25/118.92 (~P1(x30511,f7(f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[234,226,3007,2999,2929,1836,1817,28,43,42,56,50,34,31,51,2,46])).
% 118.25/118.92 cnf(3056,plain,
% 118.25/118.92 (P1(f5(x30561,f10(a1)),f9(f10(x30562),f10(x30562)))),
% 118.25/118.92 inference(scs_inference,[],[234,226,3007,2999,2929,1836,1817,28,43,42,56,50,34,31,51,2,46,45,55])).
% 118.25/118.92 cnf(3061,plain,
% 118.25/118.92 (P1(x30611,f7(f9(a1,x30612)))),
% 118.25/118.92 inference(scs_inference,[],[234,226,3007,2999,2929,1836,1817,28,43,42,56,50,34,31,51,2,46,45,55,39,41])).
% 118.25/118.92 cnf(3065,plain,
% 118.25/118.92 (~P1(f5(x30651,f9(a1,x30652)),f13(a1,a1))),
% 118.25/118.92 inference(scs_inference,[],[234,226,3007,2999,2929,1836,1817,28,43,42,56,50,34,31,51,2,46,45,55,39,41,52,57])).
% 118.25/118.92 cnf(3068,plain,
% 118.25/118.92 (~E(f9(f14(a1),x30681),f7(a1))),
% 118.25/118.92 inference(scs_inference,[],[234,226,3007,2999,2992,2793,2929,1836,1817,28,43,42,56,50,34,31,51,2,46,45,55,39,41,52,57,24])).
% 118.25/118.92 cnf(3070,plain,
% 118.25/118.92 (~P1(x30701,f2(f9(a1,x30702),x30703))),
% 118.25/118.92 inference(scs_inference,[],[3048,52])).
% 118.25/118.92 cnf(3072,plain,
% 118.25/118.92 (P1(f14(f2(a1,x30721)),f13(f10(x30722),x30723))),
% 118.25/118.92 inference(scs_inference,[],[3048,3044,52,43])).
% 118.25/118.92 cnf(3076,plain,
% 118.25/118.92 (~P1(x30761,f9(x30762,f9(a1,x30763)))),
% 118.25/118.92 inference(scs_inference,[],[3048,3044,52,43,42,50])).
% 118.25/118.92 cnf(3080,plain,
% 118.25/118.92 (~P1(f14(f2(a1,x30801)),f2(x30802,f10(x30803)))),
% 118.25/118.92 inference(scs_inference,[],[3048,867,3044,52,43,42,50,31,56])).
% 118.25/118.92 cnf(3082,plain,
% 118.25/118.92 (P1(f7(f10(x30821)),f10(x30822))),
% 118.25/118.92 inference(scs_inference,[],[3048,867,3044,626,52,43,42,50,31,56,34])).
% 118.25/118.92 cnf(3084,plain,
% 118.25/118.92 (~P1(x30841,f9(f9(a1,x30842),x30843))),
% 118.25/118.92 inference(scs_inference,[],[3048,867,3044,626,52,43,42,50,31,56,34,51])).
% 118.25/118.92 cnf(3089,plain,
% 118.25/118.92 (P1(f14(f2(a1,x30891)),f2(f10(x30892),f9(a1,x30893)))),
% 118.25/118.92 inference(scs_inference,[],[3048,867,293,3044,626,52,43,42,50,31,56,34,51,2,45,49])).
% 118.25/118.92 cnf(3090,plain,
% 118.25/118.92 (~P1(x30901,f9(a1,x30902))),
% 118.25/118.92 inference(rename_variables,[],[3048])).
% 118.25/118.92 cnf(3092,plain,
% 118.25/118.92 (P1(f14(f2(a1,x30921)),f9(f10(x30922),f10(x30922)))),
% 118.25/118.92 inference(scs_inference,[],[3048,867,293,3044,626,52,43,42,50,31,56,34,51,2,45,49,55])).
% 118.25/118.92 cnf(3094,plain,
% 118.25/118.92 (~P1(x30941,f13(f9(a1,x30942),f9(a1,x30942)))),
% 118.25/118.92 inference(scs_inference,[],[3048,3090,867,293,3044,626,52,43,42,50,31,56,34,51,2,45,49,55,57])).
% 118.25/118.92 cnf(3099,plain,
% 118.25/118.92 (~P1(f10(x30991),f10(f9(a1,x30992)))),
% 118.25/118.92 inference(scs_inference,[],[3048,3090,867,293,3044,626,52,43,42,50,31,56,34,51,2,45,49,55,57,39,37])).
% 118.25/118.92 cnf(3101,plain,
% 118.25/118.92 (P1(f4(f10(x31011),f9(a1,x31012)),f10(x31011))),
% 118.25/118.92 inference(scs_inference,[],[3048,3090,867,293,3044,626,52,43,42,50,31,56,34,51,2,45,49,55,57,39,37,38])).
% 118.25/118.92 cnf(3108,plain,
% 118.25/118.92 (P1(f7(f10(x31081)),f13(f10(x31082),x31083))),
% 118.25/118.92 inference(scs_inference,[],[3082,3065,52,43])).
% 118.25/118.92 cnf(3110,plain,
% 118.25/118.92 (~P1(f7(f10(x31101)),f2(x31102,f10(x31103)))),
% 118.25/118.92 inference(scs_inference,[],[3082,3065,52,43,56])).
% 118.25/118.92 cnf(3112,plain,
% 118.25/118.92 (P1(f7(f10(x31121)),f13(x31122,f10(x31123)))),
% 118.25/118.92 inference(scs_inference,[],[3082,3065,52,43,56,42])).
% 118.25/118.92 cnf(3118,plain,
% 118.25/118.92 (P1(f2(a1,x31181),f10(x31182))),
% 118.25/118.92 inference(scs_inference,[],[2944,3082,3065,1821,52,43,56,42,50,31,34])).
% 118.25/118.92 cnf(3122,plain,
% 118.25/118.92 (~E(f2(a1,x31221),f9(f12(x31222,x31223),f11(x31223)))),
% 118.25/118.92 inference(scs_inference,[],[2944,3082,2279,3065,1821,52,43,56,42,50,31,34,51,2])).
% 118.25/118.92 cnf(3128,plain,
% 118.25/118.92 (P1(f7(f10(x31281)),f9(f10(x31282),f10(x31282)))),
% 118.25/118.92 inference(scs_inference,[],[2944,3082,2279,3065,3048,1821,52,43,56,42,50,31,34,51,2,49,45,55])).
% 118.25/118.92 cnf(3132,plain,
% 118.25/118.92 (~P3(f10(x31321),f9(f2(a1,x31322),x31323))),
% 118.25/118.92 inference(scs_inference,[],[2944,3082,2279,3065,3011,3048,1821,52,43,56,42,50,31,34,51,2,49,45,55,57,39])).
% 118.25/118.92 cnf(3137,plain,
% 118.25/118.92 (~E(f13(x31371,f7(a1)),f13(a1,a1))),
% 118.25/118.92 inference(scs_inference,[],[2944,3082,3101,2279,3065,3011,2970,3048,1821,52,43,56,42,50,31,34,51,2,49,45,55,57,39,44,23])).
% 118.25/118.92 cnf(3145,plain,
% 118.25/118.92 (P1(f2(a1,x31451),f13(x31452,f10(x31453)))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,43,31,56,42])).
% 118.25/118.92 cnf(3147,plain,
% 118.25/118.92 (~P1(x31471,f9(x31472,a1))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,28,43,31,56,42,50])).
% 118.25/118.92 cnf(3149,plain,
% 118.25/118.92 (~P1(x31491,f9(f9(x31492,a1),x31493))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,28,43,31,56,42,50,51])).
% 118.25/118.92 cnf(3154,plain,
% 118.25/118.92 (P1(f2(a1,x31541),f9(f10(x31542),f10(x31542)))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,2282,28,43,31,56,42,50,51,2,45,55])).
% 118.25/118.92 cnf(3156,plain,
% 118.25/118.92 (~P1(x31561,f13(f9(x31562,f2(a1,x31563)),f9(a1,x31564)))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,2282,3042,3048,28,43,31,56,42,50,51,2,45,55,57])).
% 118.25/118.92 cnf(3157,plain,
% 118.25/118.92 (~P1(x31571,f9(a1,x31572))),
% 118.25/118.92 inference(rename_variables,[],[3048])).
% 118.25/118.92 cnf(3159,plain,
% 118.25/118.92 (~P3(f10(x31591),f9(x31592,f2(a1,x31593)))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,2282,3042,3048,28,43,31,56,42,50,51,2,45,55,57,39])).
% 118.25/118.92 cnf(3162,plain,
% 118.25/118.92 (P1(x31621,f7(f9(x31622,a1)))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,2282,3042,3048,28,43,31,56,42,50,51,2,45,55,57,39,41])).
% 118.25/118.92 cnf(3166,plain,
% 118.25/118.92 (P1(f2(a1,x31661),f2(f10(x31662),f9(a1,x31663)))),
% 118.25/118.92 inference(scs_inference,[],[3118,2978,2282,3042,3048,3157,28,43,31,56,42,50,51,2,45,55,57,39,41,52,49])).
% 118.25/118.92 cnf(3175,plain,
% 118.25/118.92 (~P1(x31751,f2(f9(x31752,a1),x31753))),
% 118.25/118.92 inference(scs_inference,[],[3147,52])).
% 118.25/118.92 cnf(3177,plain,
% 118.25/118.92 (P1(f2(f14(a1),x31771),f13(f10(x31772),x31773))),
% 118.25/118.92 inference(scs_inference,[],[3147,2968,52,43])).
% 118.25/118.92 cnf(3179,plain,
% 118.25/118.92 (~P1(f10(x31791),f11(a1))),
% 118.25/118.92 inference(scs_inference,[],[3147,532,2968,52,43,31])).
% 118.25/118.92 cnf(3187,plain,
% 118.25/118.92 (~P1(x31871,f9(x31872,f9(x31873,a1)))),
% 118.25/118.92 inference(scs_inference,[],[3147,532,2968,52,43,31,51,42,56,50])).
% 118.25/118.92 cnf(3191,plain,
% 118.25/118.92 (~P1(x31911,f9(x31912,a1))),
% 118.25/118.92 inference(rename_variables,[],[3147])).
% 118.25/118.92 cnf(3193,plain,
% 118.25/118.92 (~P1(f10(x31931),f12(a1,a1))),
% 118.25/118.92 inference(scs_inference,[],[3147,532,2249,2995,2968,52,43,31,51,42,56,50,2,49,45])).
% 118.25/118.92 cnf(3195,plain,
% 118.25/118.92 (P1(f2(f14(a1),x31951),f9(f10(x31952),f10(x31952)))),
% 118.25/118.92 inference(scs_inference,[],[3147,532,2249,2995,2968,52,43,31,51,42,56,50,2,49,45,55])).
% 118.25/118.92 cnf(3197,plain,
% 118.25/118.92 (~P1(x31971,f13(f9(x31972,a1),f9(x31972,a1)))),
% 118.25/118.92 inference(scs_inference,[],[3147,3191,532,2249,2995,2968,52,43,31,51,42,56,50,2,49,45,55,57])).
% 118.25/118.92 cnf(3199,plain,
% 118.25/118.92 (~P3(f6(f7(a1),f7(a1)),f9(x31991,a1))),
% 118.25/118.92 inference(scs_inference,[],[3147,3191,532,2249,2995,2968,52,43,31,51,42,56,50,2,49,45,55,57,39])).
% 118.25/118.92 cnf(3206,plain,
% 118.25/118.92 (~E(f9(f14(a1),x32061),f10(x32062))),
% 118.25/118.92 inference(scs_inference,[],[3147,3191,532,2249,2995,3132,2968,2793,52,43,31,51,42,56,50,2,49,45,55,57,39,2121,37,24])).
% 118.25/118.92 cnf(3208,plain,
% 118.25/118.92 (~E(a1,f6(f7(a1),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3147,3191,532,2249,2995,3132,2968,2793,52,43,31,51,42,56,50,2,49,45,55,57,39,2121,37,24,228])).
% 118.25/118.92 cnf(3209,plain,
% 118.25/118.92 (~E(f14(a1),f6(f7(a1),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3147,3191,532,2249,2995,3132,2968,2793,52,43,31,51,42,56,50,2,49,45,55,57,39,2121,37,24,228,600])).
% 118.25/118.92 cnf(3210,plain,
% 118.25/118.92 (~E(f14(f14(a1)),f6(f7(a1),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3147,3191,532,2249,2995,3132,2968,2793,52,43,31,51,42,56,50,2,49,45,55,57,39,2121,37,24,228,600,567])).
% 118.25/118.92 cnf(3213,plain,
% 118.25/118.92 (P1(f4(f10(x32131),f9(a1,x32132)),f13(f10(x32131),x32133))),
% 118.25/118.92 inference(scs_inference,[],[3179,3101,52,43])).
% 118.25/118.92 cnf(3215,plain,
% 118.25/118.92 (~P1(f4(f10(x32151),f9(a1,x32152)),f2(x32153,f10(x32151)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3101,52,43,56])).
% 118.25/118.92 cnf(3221,plain,
% 118.25/118.92 (P1(f4(f10(x32211),f9(a1,x32212)),f13(x32213,f10(x32211)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3101,52,43,56,51,31,42])).
% 118.25/118.92 cnf(3226,plain,
% 118.25/118.92 (P1(f10(x32261),f2(f7(f9(a1,x32262)),f11(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3206,3061,3101,52,43,56,51,31,42,50,2,49])).
% 118.25/118.92 cnf(3227,plain,
% 118.25/118.92 (P1(x32271,f7(f9(a1,x32272)))),
% 118.25/118.92 inference(rename_variables,[],[3061])).
% 118.25/118.92 cnf(3233,plain,
% 118.25/118.92 (~P1(f10(x32331),f13(f11(a1),f11(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3206,3061,3101,52,43,56,51,31,42,50,2,49,45,55,57])).
% 118.25/118.92 cnf(3240,plain,
% 118.25/118.92 (~E(f7(f9(a1,x32401)),f7(f10(x32402)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3206,3061,3227,3101,52,43,56,51,31,42,50,2,49,45,55,57,39,440,2121])).
% 118.25/118.92 cnf(3247,plain,
% 118.25/118.92 (~E(f7(f14(a1)),f9(x32471,a1))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3206,3199,3061,3227,3101,197,52,43,56,51,31,42,50,2,49,45,55,57,39,440,2121,53,37,3,25])).
% 118.25/118.92 cnf(3250,plain,
% 118.25/118.92 (~E(a1,f7(f9(a1,x32501)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3206,3199,3061,3227,3101,197,52,43,56,51,31,42,50,2,49,45,55,57,39,440,2121,53,37,3,25,567,228])).
% 118.25/118.92 cnf(3252,plain,
% 118.25/118.92 (~E(f14(a1),f7(f9(a1,x32521)))),
% 118.25/118.92 inference(scs_inference,[],[3179,3193,869,3206,3199,3061,3227,3101,197,52,43,56,51,31,42,50,2,49,45,55,57,39,440,2121,53,37,3,25,567,228,76,600])).
% 118.25/118.92 cnf(3255,plain,
% 118.25/118.92 (P1(x32551,f13(f12(x32551,x32552),x32553))),
% 118.25/118.92 inference(scs_inference,[],[3193,60,52,43])).
% 118.25/118.92 cnf(3257,plain,
% 118.25/118.92 (P1(x32571,f13(x32572,f12(x32571,x32573)))),
% 118.25/118.92 inference(scs_inference,[],[3193,60,52,43,42])).
% 118.25/118.92 cnf(3259,plain,
% 118.25/118.92 (~P1(x32591,f2(x32592,f12(x32591,x32593)))),
% 118.25/118.92 inference(scs_inference,[],[3193,60,52,43,42,56])).
% 118.25/118.92 cnf(3268,plain,
% 118.25/118.92 (P1(f5(x32681,f10(x32682)),f9(f10(x32682),f10(x32682)))),
% 118.25/118.92 inference(scs_inference,[],[3015,2252,3193,619,60,52,43,42,56,31,50,2,45,55])).
% 118.25/118.92 cnf(3270,plain,
% 118.25/118.92 (~P1(f10(x32701),f13(f12(a1,a1),f12(a1,a1)))),
% 118.25/118.92 inference(scs_inference,[],[3015,2252,3193,619,60,52,43,42,56,31,50,2,45,55,57])).
% 118.25/118.92 cnf(3272,plain,
% 118.25/118.92 (~P3(f7(f9(x32721,a1)),f13(f11(a1),f11(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3015,2252,3233,3162,3193,619,60,52,43,42,56,31,50,2,45,55,57,39])).
% 118.25/118.92 cnf(3279,plain,
% 118.25/118.92 (P1(x32791,f13(f12(x32792,x32791),x32793))),
% 118.25/118.92 inference(scs_inference,[],[59,43])).
% 118.25/118.92 cnf(3281,plain,
% 118.25/118.92 (P1(x32811,f13(x32812,f12(x32813,x32811)))),
% 118.25/118.92 inference(scs_inference,[],[59,43,42])).
% 118.25/118.92 cnf(3285,plain,
% 118.25/118.92 (~P1(x32851,f2(x32852,f12(x32853,x32851)))),
% 118.25/118.92 inference(scs_inference,[],[2691,59,43,42,31,56])).
% 118.25/118.92 cnf(3290,plain,
% 118.25/118.92 (P1(f14(a1),f9(f10(x32901),f10(x32901)))),
% 118.25/118.92 inference(scs_inference,[],[289,2691,2255,599,59,43,42,31,56,2,45,55])).
% 118.25/118.92 cnf(3295,plain,
% 118.25/118.92 (~P3(f13(f12(x32951,x32952),x32953),f2(x32954,f12(x32951,x32955)))),
% 118.25/118.92 inference(scs_inference,[],[289,2691,2255,3255,3259,3147,599,59,43,42,31,56,2,45,55,57,39])).
% 118.25/118.92 cnf(3296,plain,
% 118.25/118.92 (~P1(x32961,f2(x32962,f12(x32961,x32963)))),
% 118.25/118.92 inference(rename_variables,[],[3259])).
% 118.25/118.92 cnf(3298,plain,
% 118.25/118.92 (~E(a1,f13(f12(x32981,x32982),x32983))),
% 118.25/118.92 inference(scs_inference,[],[289,2691,2255,3255,3259,3147,599,59,43,42,31,56,2,45,55,57,39,2681])).
% 118.25/118.92 cnf(3304,plain,
% 118.25/118.92 (~P1(x33041,f2(x33042,f12(x33043,x33044)))+~E(x33041,x33043)),
% 118.25/118.92 inference(scs_inference,[],[289,2691,2255,3255,3259,3296,3147,2774,2793,599,59,43,42,31,56,2,45,55,57,39,2681,40,22])).
% 118.25/118.92 cnf(3309,plain,
% 118.25/118.92 (~P1(f14(f14(a1)),f12(f12(x33091,x33092),f12(x33091,x33092)))),
% 118.25/118.92 inference(scs_inference,[],[305,2285,31,2,45])).
% 118.25/118.92 cnf(3311,plain,
% 118.25/118.92 (P1(x33111,f9(f13(x33112,f12(x33111,x33113)),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[305,2285,3257,2929,31,2,45,55])).
% 118.25/118.92 cnf(3317,plain,
% 118.25/118.92 (~E(a1,f13(x33171,f12(x33172,x33173)))),
% 118.25/118.92 inference(scs_inference,[],[305,2285,3257,3285,2929,31,2,45,55,39,2681])).
% 118.25/118.92 cnf(3319,plain,
% 118.25/118.92 (~E(f2(f14(a1),x33191),f10(x33192))),
% 118.25/118.92 inference(scs_inference,[],[305,2285,3257,3285,3159,2767,2929,31,2,45,55,39,2681,24])).
% 118.25/118.92 cnf(3321,plain,
% 118.25/118.92 (~P1(f2(f14(a1),x33211),f11(f10(x33212)))),
% 118.25/118.92 inference(scs_inference,[],[3319,31])).
% 118.25/118.92 cnf(3329,plain,
% 118.25/118.92 (P1(x33291,f2(f13(f12(x33292,x33291),x33293),f9(x33294,a1)))),
% 118.25/118.92 inference(scs_inference,[],[3319,3279,3149,3147,31,2,45,39,49])).
% 118.25/118.92 cnf(3335,plain,
% 118.25/118.92 (~E(f13(f12(x33351,x33352),x33353),f7(f10(x33354)))),
% 118.25/118.92 inference(scs_inference,[],[3319,3279,3149,3295,3147,197,31,2,45,39,49,3,25,2121])).
% 118.25/118.92 cnf(3343,plain,
% 118.25/118.92 (P1(x33431,f13(x33432,f12(x33433,x33431)))),
% 118.25/118.92 inference(rename_variables,[],[3281])).
% 118.25/118.92 cnf(3345,plain,
% 118.25/118.92 (P1(x33451,f14(f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[318,2288,3281,3343,3175,2929,31,2,45,39,44])).
% 118.25/118.92 cnf(3350,plain,
% 118.25/118.92 (P1(x33501,f6(x33501,f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[318,2288,3281,3343,3175,2929,31,2,45,39,44,23,47])).
% 118.25/118.92 cnf(3357,plain,
% 118.25/118.92 (~P1(x33571,f13(f9(x33572,f9(x33573,a1)),f9(x33574,a1)))),
% 118.25/118.92 inference(scs_inference,[],[321,585,3187,3147,31,2,45,57])).
% 118.25/118.92 cnf(3377,plain,
% 118.25/118.92 (P1(f2(a1,x33771),f9(f9(f10(x33772),f10(x33772)),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[2590,591,3154,3051,2929,31,2,45,39,55])).
% 118.25/118.92 cnf(3413,plain,
% 118.25/118.92 (~P1(f13(x34131,f10(x34132)),f12(f14(a1),f14(a1)))),
% 118.25/118.92 inference(scs_inference,[],[587,31,2,45])).
% 118.25/118.92 cnf(3416,plain,
% 118.25/118.92 (~P1(f7(f10(x34161)),f2(x34162,f10(x34163)))),
% 118.25/118.92 inference(rename_variables,[],[3110])).
% 118.25/118.92 cnf(3427,plain,
% 118.25/118.92 (~P1(x34271,f2(x34272,f10(x34273)))+~E(x34271,f7(f10(x34274)))),
% 118.25/118.92 inference(scs_inference,[],[587,3270,3128,3110,3416,3147,2774,1209,31,2,45,39,2681,57,40,22])).
% 118.25/118.92 cnf(3437,plain,
% 118.25/118.92 (P1(f2(a1,x34371),f9(f13(x34372,f10(x34373)),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[593,3145,3413,3345,2929,31,2,45,39,55])).
% 118.25/118.92 cnf(3445,plain,
% 118.25/118.92 (~P1(f9(f10(x34451),f10(x34452)),f12(f14(a1),f14(a1)))),
% 118.25/118.92 inference(scs_inference,[],[856,31,2,45])).
% 118.25/118.92 cnf(3450,plain,
% 118.25/118.92 (P1(f14(a1),f2(f9(f10(x34501),f10(x34501)),f9(a1,x34502)))),
% 118.25/118.92 inference(scs_inference,[],[856,3290,3076,3048,31,2,45,39,49])).
% 118.25/118.92 cnf(3464,plain,
% 118.25/118.92 (~E(f9(f10(x34641),f10(x34641)),f9(f9(a1,x34642),x34643))),
% 118.25/118.92 inference(scs_inference,[],[2258,3268,3445,3084,2896,31,2,45,39,23])).
% 118.25/118.92 cnf(3478,plain,
% 118.25/118.92 (~P1(x34781,f2(x34782,f10(x34783)))+~E(x34781,f4(f10(x34783),f9(a1,x34784)))),
% 118.25/118.92 inference(scs_inference,[],[3247,3108,3215,3094,2767,2774,31,2,45,39,40,22])).
% 118.25/118.92 cnf(3498,plain,
% 118.25/118.92 (~E(x34981,f11(a1))+~E(f12(f10(a1),x34982),x34981)),
% 118.25/118.92 inference(scs_inference,[],[1088,3112,3197,31,2,45,39,3])).
% 118.25/118.92 cnf(3501,plain,
% 118.25/118.92 (~P1(f9(f14(a1),x35011),f11(f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3068,31])).
% 118.25/118.92 cnf(3504,plain,
% 118.25/118.92 (~P1(f9(f14(a1),x35041),f12(f7(a1),f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3068,31,2,45])).
% 118.25/118.92 cnf(3506,plain,
% 118.25/118.92 (~P3(f10(x35061),f13(f9(x35062,f2(a1,x35063)),f9(a1,x35064)))),
% 118.25/118.92 inference(scs_inference,[],[3068,3156,2901,31,2,45,39])).
% 118.25/118.92 cnf(3513,plain,
% 118.25/118.92 (~E(f13(a1,a1),f13(x35131,f7(a1)))),
% 118.25/118.92 inference(scs_inference,[],[3137,31,2])).
% 118.25/118.92 cnf(3519,plain,
% 118.25/118.92 (P2(f9(f14(a1),x35191),f9(f14(a1),x35191))),
% 118.25/118.92 inference(scs_inference,[],[3137,2950,3501,2793,31,2,45,39,40])).
% 118.25/118.92 cnf(3527,plain,
% 118.25/118.92 (~E(f2(x35271,f11(x35272)),f11(x35272))),
% 118.25/118.92 inference(scs_inference,[],[463,538,31,2])).
% 118.25/118.92 cnf(3530,plain,
% 118.25/118.92 (~P1(f9(f7(a3),f7(a8)),f12(a1,a1))),
% 118.25/118.92 inference(scs_inference,[],[161,463,538,31,2,57,45])).
% 118.25/118.92 cnf(3542,plain,
% 118.25/118.92 (~E(f14(f9(x35421,a1)),f10(x35422))),
% 118.25/118.92 inference(scs_inference,[],[161,463,538,3357,3506,2968,2774,31,2,57,45,39,406,52,51,50,24])).
% 118.25/118.92 cnf(3550,plain,
% 118.25/118.92 (~P1(f2(x35501,f11(x35502)),f11(f11(x35502)))),
% 118.25/118.92 inference(scs_inference,[],[3527,3530,52,51,50,31])).
% 118.25/118.92 cnf(3558,plain,
% 118.25/118.92 (~P1(f2(x35581,f11(x35582)),f12(f11(x35582),f11(x35582)))),
% 118.25/118.92 inference(scs_inference,[],[3527,3542,3530,2929,52,51,50,31,2,49,57,45])).
% 118.25/118.92 cnf(3563,plain,
% 118.25/118.92 (~E(f7(a1),f7(f10(x35631)))),
% 118.25/118.92 inference(scs_inference,[],[3527,3542,3530,3213,3003,2929,52,51,50,31,2,49,57,45,39,2121])).
% 118.25/118.92 cnf(3565,plain,
% 118.25/118.92 (~E(x35651,f11(x35652))+~E(f2(x35653,f11(x35652)),x35651)),
% 118.25/118.92 inference(scs_inference,[],[3527,3542,3530,3213,3003,2929,52,51,50,31,2,49,57,45,39,2121,3])).
% 118.25/118.92 cnf(3570,plain,
% 118.25/118.92 (~E(f5(x35701,f10(x35702)),f11(x35701))),
% 118.25/118.92 inference(scs_inference,[],[964,547,31,2])).
% 118.25/118.92 cnf(3571,plain,
% 118.25/118.92 (~P1(f9(f12(x35711,x35712),f11(x35712)),f12(a1,a1))),
% 118.25/118.92 inference(scs_inference,[],[964,547,31,2,45])).
% 118.25/118.92 cnf(3576,plain,
% 118.25/118.92 (P1(f2(f14(a1),x35761),f9(f10(x35762),f10(x35762)))),
% 118.25/118.92 inference(rename_variables,[],[3195])).
% 118.25/118.92 cnf(3577,plain,
% 118.25/118.92 (~P1(f2(x35771,f11(x35772)),f12(f11(x35772),f11(x35772)))),
% 118.25/118.92 inference(rename_variables,[],[3558])).
% 118.25/118.92 cnf(3580,plain,
% 118.25/118.92 (~P1(f9(f12(x35801,x35802),f11(x35802)),f2(f11(a1),x35803))),
% 118.25/118.92 inference(scs_inference,[],[964,547,3558,3195,31,2,45,57,39,427,52])).
% 118.25/118.92 cnf(3586,plain,
% 118.25/118.92 (~E(f9(f10(x35861),f10(x35861)),f12(f11(x35862),f11(x35862)))),
% 118.25/118.92 inference(scs_inference,[],[964,547,3558,3577,3195,3576,31,2,45,57,39,427,52,51,50,23])).
% 118.25/118.92 cnf(3589,plain,
% 118.25/118.92 (~P1(f9(f12(x35891,x35892),f11(x35892)),f2(f12(a1,a1),x35893))),
% 118.25/118.92 inference(scs_inference,[],[3571,52])).
% 118.25/118.92 cnf(3595,plain,
% 118.25/118.92 (~P1(f5(x35951,f10(x35952)),f11(f11(x35951)))),
% 118.25/118.92 inference(scs_inference,[],[3570,3571,52,51,50,31])).
% 118.25/118.92 cnf(3597,plain,
% 118.25/118.92 (~E(f2(x35971,f11(x35972)),f12(x35973,x35972))),
% 118.25/118.92 inference(scs_inference,[],[3570,3571,461,52,51,50,31,2])).
% 118.25/118.92 cnf(3613,plain,
% 118.25/118.92 (~E(f5(x36131,f10(x36132)),f12(x36133,x36131))),
% 118.25/118.92 inference(scs_inference,[],[3597,943,31,2])).
% 118.25/118.92 cnf(3619,plain,
% 118.25/118.92 (~P1(f5(x36191,f10(x36192)),f11(f12(x36193,x36191)))),
% 118.25/118.92 inference(scs_inference,[],[3613,31])).
% 118.25/118.92 cnf(3621,plain,
% 118.25/118.92 (~E(f5(x36211,f10(x36212)),f12(x36211,x36213))),
% 118.25/118.92 inference(scs_inference,[],[3613,946,31,2])).
% 118.25/118.92 cnf(3622,plain,
% 118.25/118.92 (~P1(f5(x36221,f10(x36222)),f12(f12(x36223,x36221),f12(x36223,x36221)))),
% 118.25/118.92 inference(scs_inference,[],[3613,946,31,2,45])).
% 118.25/118.92 cnf(3624,plain,
% 118.25/118.92 (~P3(f9(f10(x36241),f10(x36241)),f11(f11(x36242)))),
% 118.25/118.92 inference(scs_inference,[],[3613,946,3595,3056,31,2,45,39])).
% 118.25/118.92 cnf(3627,plain,
% 118.25/118.92 (~E(x36271,f12(x36272,x36273))+~E(f5(x36273,f10(x36274)),x36271)),
% 118.25/118.92 inference(scs_inference,[],[3613,946,3595,3056,31,2,45,39,3])).
% 118.25/118.92 cnf(3633,plain,
% 118.25/118.92 (~E(f2(x36331,f10(x36332)),f10(x36333))),
% 118.25/118.92 inference(scs_inference,[],[327,552,31,2])).
% 118.25/118.92 cnf(3636,plain,
% 118.25/118.92 (~P1(f9(f11(x36361),f12(x36362,x36361)),f12(a1,a1))),
% 118.25/118.92 inference(scs_inference,[],[327,552,31,2,57,45])).
% 118.25/118.92 cnf(3642,plain,
% 118.25/118.92 (~P1(f9(f11(x36421),f12(x36422,x36421)),f2(f11(a1),x36423))),
% 118.25/118.92 inference(scs_inference,[],[327,552,2927,3504,31,2,57,45,39,95,52])).
% 118.25/118.92 cnf(3648,plain,
% 118.25/118.92 (~E(f9(f10(x36481),f10(x36481)),f9(f9(x36482,a1),x36483))),
% 118.25/118.92 inference(scs_inference,[],[327,552,3021,2927,3504,3149,31,2,57,45,39,95,52,50,51,23])).
% 118.25/118.92 cnf(3650,plain,
% 118.25/118.92 (~P1(f9(f11(x36501),f12(x36502,x36501)),f2(f12(a1,a1),x36503))),
% 118.25/118.92 inference(scs_inference,[],[3636,52])).
% 118.25/118.92 cnf(3658,plain,
% 118.25/118.92 (~E(f11(f12(x36581,x36582)),f10(x36583))),
% 118.25/118.92 inference(scs_inference,[],[3633,3636,377,52,51,50,31,2])).
% 118.25/118.92 cnf(3659,plain,
% 118.25/118.92 (~P1(f2(x36591,f10(x36592)),f12(f10(x36593),f10(x36593)))),
% 118.25/118.92 inference(scs_inference,[],[3633,3636,377,52,51,50,31,2,45])).
% 118.25/118.92 cnf(3666,plain,
% 118.25/118.92 (P1(f9(f11(x36661),f12(x36662,x36661)),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.92 inference(scs_inference,[],[3633,3636,377,3092,3070,2929,52,51,50,31,2,45,57,39,49])).
% 118.25/118.92 cnf(3669,plain,
% 118.25/118.92 (~P1(x36691,f2(f12(a1,a1),x36692))+~E(x36691,f9(f12(x36693,x36694),f11(x36694)))),
% 118.25/118.92 inference(scs_inference,[],[3633,3636,377,3589,3092,3070,2929,52,51,50,31,2,45,57,39,49,22])).
% 118.25/118.92 cnf(3673,plain,
% 118.25/118.92 (~E(f7(f10(x36731)),f12(x36732,x36733))),
% 118.25/118.92 inference(scs_inference,[],[3658,896,31,2])).
% 118.25/118.92 cnf(3681,plain,
% 118.25/118.92 (~E(f7(f10(x36811)),f11(x36812))),
% 118.25/118.92 inference(scs_inference,[],[3673,914,31,2])).
% 118.25/118.92 cnf(3687,plain,
% 118.25/118.92 (~E(x36871,f12(x36872,x36873))+~E(f7(f10(x36874)),x36871)),
% 118.25/118.92 inference(scs_inference,[],[3673,914,3311,3147,31,2,45,39,3])).
% 118.25/118.92 cnf(3692,plain,
% 118.25/118.92 (~E(f6(f7(a1),f7(a1)),f14(a1))),
% 118.25/118.92 inference(scs_inference,[],[3681,3209,31,2])).
% 118.25/118.92 cnf(3702,plain,
% 118.25/118.92 (~E(f6(f7(a1),f7(a1)),a1)),
% 118.25/118.92 inference(scs_inference,[],[3692,3208,31,2])).
% 118.25/118.92 cnf(3708,plain,
% 118.25/118.92 (~P1(x37081,f2(f12(a1,a1),x37082))+~E(x37081,f9(f11(x37083),f12(x37084,x37083)))),
% 118.25/118.92 inference(scs_inference,[],[3692,3208,3650,3036,3619,31,2,45,39,22])).
% 118.25/118.92 cnf(3712,plain,
% 118.25/118.92 (~E(f5(f14(a1),f10(x37121)),f10(x37122))),
% 118.25/118.92 inference(scs_inference,[],[931,541,31,2])).
% 118.25/118.92 cnf(3715,plain,
% 118.25/118.92 (~P1(f13(x37151,f11(x37152)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[931,541,31,2,57,45])).
% 118.25/118.93 cnf(3727,plain,
% 118.25/118.93 (~P1(f13(x37271,f11(x37272)),f2(f12(a1,a1),x37273))),
% 118.25/118.93 inference(scs_inference,[],[3715,52])).
% 118.25/118.93 cnf(3735,plain,
% 118.25/118.93 (~E(f14(f2(a1,x37351)),f10(x37352))),
% 118.25/118.93 inference(scs_inference,[],[3715,3712,2307,52,51,50,31,2])).
% 118.25/118.93 cnf(3738,plain,
% 118.25/118.93 (~P1(f5(f14(a1),f10(x37381)),f12(f10(x37382),f10(x37382)))),
% 118.25/118.93 inference(scs_inference,[],[3715,3712,2307,52,51,50,31,2,57,45])).
% 118.25/118.93 cnf(3744,plain,
% 118.25/118.93 (P1(f13(x37441,f11(x37442)),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3715,3712,2307,3177,3659,2929,52,51,50,31,2,57,45,39,49])).
% 118.25/118.93 cnf(3750,plain,
% 118.25/118.93 (~P1(f14(f2(a1,x37501)),f11(f10(x37502)))),
% 118.25/118.93 inference(scs_inference,[],[3735,31])).
% 118.25/118.93 cnf(3752,plain,
% 118.25/118.93 (~E(f14(f2(a1,x37521)),f12(x37522,x37523))),
% 118.25/118.93 inference(scs_inference,[],[3735,2322,31,2])).
% 118.25/118.93 cnf(3759,plain,
% 118.25/118.93 (~E(f2(f7(a1),f12(a1,a1)),f2(f12(a1,a1),x37591))),
% 118.25/118.93 inference(scs_inference,[],[3735,2322,3744,3727,3738,3038,31,2,45,39,23])).
% 118.25/118.93 cnf(3761,plain,
% 118.25/118.93 (~P1(f14(f2(a1,x37611)),f11(f12(x37612,x37613)))),
% 118.25/118.93 inference(scs_inference,[],[3752,31])).
% 118.25/118.93 cnf(3763,plain,
% 118.25/118.93 (~E(f14(f2(a1,x37631)),f11(x37632))),
% 118.25/118.93 inference(scs_inference,[],[3752,2337,31,2])).
% 118.25/118.93 cnf(3769,plain,
% 118.25/118.93 (~P1(x37691,f2(f11(a1),x37692))+~E(x37691,f9(f12(x37693,x37694),f11(x37694)))),
% 118.25/118.93 inference(scs_inference,[],[3752,2337,3580,3072,3750,31,2,45,39,22])).
% 118.25/118.93 cnf(3773,plain,
% 118.25/118.93 (~E(f14(f14(a1)),f11(x37731))),
% 118.25/118.93 inference(scs_inference,[],[3763,209,31,2])).
% 118.25/118.93 cnf(3781,plain,
% 118.25/118.93 (~E(f11(f12(x37811,x37812)),f12(x37813,a1))),
% 118.25/118.93 inference(scs_inference,[],[3773,368,31,2])).
% 118.25/118.93 cnf(3793,plain,
% 118.25/118.93 (~E(f11(f12(x37931,x37932)),f12(a1,x37933))),
% 118.25/118.93 inference(scs_inference,[],[3781,371,31,2])).
% 118.25/118.93 cnf(3801,plain,
% 118.25/118.93 (~E(f11(f10(a1)),f10(x38011))),
% 118.25/118.93 inference(scs_inference,[],[3793,390,31,2])).
% 118.25/118.93 cnf(3806,plain,
% 118.25/118.93 (~P1(x38061,f2(f11(a1),x38062))+~E(x38061,f9(f11(x38063),f12(x38064,x38063)))),
% 118.25/118.93 inference(scs_inference,[],[3793,390,3642,2905,3309,31,2,45,39,22])).
% 118.25/118.93 cnf(3810,plain,
% 118.25/118.93 (~E(f5(a1,f10(x38101)),f10(x38102))),
% 118.25/118.93 inference(scs_inference,[],[3801,919,31,2])).
% 118.25/118.93 cnf(3816,plain,
% 118.25/118.93 (~E(a1,f2(f10(x38161),f9(a1,x38162)))),
% 118.25/118.93 inference(scs_inference,[],[3801,919,3080,3089,31,2,45,39,2681])).
% 118.25/118.93 cnf(3819,plain,
% 118.25/118.93 (~P1(f13(f11(x38191),x38192),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[544,31])).
% 118.25/118.93 cnf(3821,plain,
% 118.25/118.93 (~E(f11(f9(a3,a8)),f10(x38211))),
% 118.25/118.93 inference(scs_inference,[],[1134,544,31,2])).
% 118.25/118.93 cnf(3824,plain,
% 118.25/118.93 (~P1(f13(f11(x38241),x38242),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[1134,544,31,2,57,45])).
% 118.25/118.93 cnf(3839,plain,
% 118.25/118.93 (~P1(f13(f11(x38391),x38392),f2(f12(a1,a1),x38393))),
% 118.25/118.93 inference(scs_inference,[],[3824,52])).
% 118.25/118.93 cnf(3847,plain,
% 118.25/118.93 (~E(f2(x38471,f10(x38472)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3824,3821,329,52,50,51,31,2])).
% 118.25/118.93 cnf(3848,plain,
% 118.25/118.93 (P1(f13(f11(x38481),x38482),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3824,3821,329,2929,52,50,51,31,2,49])).
% 118.25/118.93 cnf(3855,plain,
% 118.25/118.93 (~P3(f6(f13(f11(x38551),x38552),f7(a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[3824,3821,329,3350,2929,52,50,51,31,2,49,57,45,39])).
% 118.25/118.93 cnf(3862,plain,
% 118.25/118.93 (~E(f11(f10(a1)),f12(x38621,a1))),
% 118.25/118.93 inference(scs_inference,[],[3847,384,31,2])).
% 118.25/118.93 cnf(3873,plain,
% 118.25/118.93 (~P1(f4(f2(f7(a1),f12(a1,a1)),f11(a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3819,3847,384,3848,3048,31,2,57,45,39,440,53])).
% 118.25/118.93 cnf(3875,plain,
% 118.25/118.93 (~P1(f2(f7(a1),f12(a1,a1)),f10(f11(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3819,3847,384,3848,3048,31,2,57,45,39,440,53,37])).
% 118.25/118.93 cnf(3879,plain,
% 118.25/118.93 (~E(a1,f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3819,3847,384,3848,3839,3048,31,2,57,45,39,440,53,37,22,76,228])).
% 118.25/118.93 cnf(3880,plain,
% 118.25/118.93 (~E(f14(a1),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3819,3847,384,3848,3839,3048,31,2,57,45,39,440,53,37,22,76,228,600])).
% 118.25/118.93 cnf(3881,plain,
% 118.25/118.93 (~E(f14(f14(a1)),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3819,3847,384,3848,3839,3048,31,2,57,45,39,440,53,37,22,76,228,600,567])).
% 118.25/118.93 cnf(3885,plain,
% 118.25/118.93 (~E(f11(f10(a1)),f12(a1,x38851))),
% 118.25/118.93 inference(scs_inference,[],[3862,386,31,2])).
% 118.25/118.93 cnf(3888,plain,
% 118.25/118.93 (~P3(f13(f7(a1),x38881),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3862,386,3873,2964,31,2,45,39])).
% 118.25/118.93 cnf(3893,plain,
% 118.25/118.93 (~P1(f4(f13(f7(a1),x38931),f11(a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3888,440,53])).
% 118.25/118.93 cnf(3899,plain,
% 118.25/118.93 (~E(f2(f7(a1),f12(a1,a1)),f14(a1))),
% 118.25/118.93 inference(scs_inference,[],[3885,3888,3880,440,53,37,31,2])).
% 118.25/118.93 cnf(3905,plain,
% 118.25/118.93 (~E(f14(a1),f13(f7(a1),x39051))),
% 118.25/118.93 inference(scs_inference,[],[3885,3888,3880,3377,3147,440,53,37,31,2,45,39,600])).
% 118.25/118.93 cnf(3906,plain,
% 118.25/118.93 (~E(a1,f13(f7(a1),x39061))),
% 118.25/118.93 inference(scs_inference,[],[3885,3888,3880,3377,3147,440,53,37,31,2,45,39,600,228])).
% 118.25/118.93 cnf(3909,plain,
% 118.25/118.93 (~E(x39091,f12(a1,x39092))+~E(f11(f10(a1)),x39091)),
% 118.25/118.93 inference(scs_inference,[],[3885,3888,3880,3377,3147,440,53,37,31,2,45,39,600,228,76,567,3])).
% 118.25/118.93 cnf(3910,plain,
% 118.25/118.93 (~E(f7(f14(a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[3885,3888,3880,3855,3377,3147,197,440,53,37,31,2,45,39,600,228,76,567,3,25])).
% 118.25/118.93 cnf(3914,plain,
% 118.25/118.93 (~E(f12(a1,a1),f7(f14(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3910,31,2])).
% 118.25/118.93 cnf(3917,plain,
% 118.25/118.93 (~P3(f13(x39171,f7(a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3910,3893,2970,31,2,45,39])).
% 118.25/118.93 cnf(3920,plain,
% 118.25/118.93 (~E(f9(f13(x39201,f10(x39202)),f7(a1)),f9(a1,x39203))),
% 118.25/118.93 inference(scs_inference,[],[3910,3893,3437,2970,3048,31,2,45,39,23])).
% 118.25/118.93 cnf(3922,plain,
% 118.25/118.93 (~E(f4(f13(x39221,f7(a1)),f11(a1)),a1)),
% 118.25/118.93 inference(scs_inference,[],[3917,440])).
% 118.25/118.93 cnf(3924,plain,
% 118.25/118.93 (~P1(f4(f13(x39241,f7(a1)),f11(a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3917,440,53])).
% 118.25/118.93 cnf(3930,plain,
% 118.25/118.93 (~E(f2(f7(a1),f12(a1,a1)),a1)),
% 118.25/118.93 inference(scs_inference,[],[3899,3917,3879,440,53,37,31,2])).
% 118.25/118.93 cnf(3938,plain,
% 118.25/118.93 (~E(f14(a1),f13(x39381,f7(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3899,3917,3879,3450,3147,440,53,37,31,2,45,39,76,567,600])).
% 118.25/118.93 cnf(3939,plain,
% 118.25/118.93 (~E(a1,f13(x39391,f7(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3899,3917,3879,3450,3147,440,53,37,31,2,45,39,76,567,600,228])).
% 118.25/118.93 cnf(3942,plain,
% 118.25/118.93 (~P1(f13(x39421,f10(x39422)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[555,31])).
% 118.25/118.93 cnf(3944,plain,
% 118.25/118.93 (~E(f7(f10(x39441)),f7(a1))),
% 118.25/118.93 inference(scs_inference,[],[3563,555,31,2])).
% 118.25/118.93 cnf(3947,plain,
% 118.25/118.93 (~P1(f13(x39471,f10(x39472)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[3563,555,31,2,57,45])).
% 118.25/118.93 cnf(3949,plain,
% 118.25/118.93 (~P3(f7(f9(x39491,a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[3563,555,3924,3162,31,2,57,45,39])).
% 118.25/118.93 cnf(3972,plain,
% 118.25/118.93 (~E(f9(x39721,f9(x39722,a1)),f7(a1))),
% 118.25/118.93 inference(scs_inference,[],[3947,3944,3949,2997,440,53,37,52,51,50,31,2])).
% 118.25/118.93 cnf(3973,plain,
% 118.25/118.93 (P1(f13(x39731,f10(x39732)),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3947,3944,3949,2997,2929,440,53,37,52,51,50,31,2,49])).
% 118.25/118.93 cnf(3976,plain,
% 118.25/118.93 (~P1(f13(x39761,f10(x39762)),f13(f12(a1,a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3947,3944,3949,2997,2929,440,53,37,52,51,50,31,2,49,57])).
% 118.25/118.93 cnf(3984,plain,
% 118.25/118.93 (~E(a1,f7(f9(x39841,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3947,3944,3949,2997,3329,3048,2929,440,53,37,52,51,50,31,2,49,57,45,39,76,228])).
% 118.25/118.93 cnf(3985,plain,
% 118.25/118.93 (~E(f14(a1),f7(f9(x39851,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3947,3944,3949,2997,3329,3048,2929,440,53,37,52,51,50,31,2,49,57,45,39,76,228,600])).
% 118.25/118.93 cnf(3992,plain,
% 118.25/118.93 (~E(f7(f9(a1,x39921)),f14(a1))),
% 118.25/118.93 inference(scs_inference,[],[3972,3252,31,2])).
% 118.25/118.93 cnf(3996,plain,
% 118.25/118.93 (~P1(f9(x39961,f9(x39962,a1)),f12(f7(a1),f7(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3942,3972,3252,3147,31,2,57,45])).
% 118.25/118.93 cnf(4010,plain,
% 118.25/118.93 (~E(a1,f9(f7(a1),f7(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3942,3972,3252,3973,2990,3147,31,2,57,45,39,440,53,37,23,76,228])).
% 118.25/118.93 cnf(4011,plain,
% 118.25/118.93 (~E(f14(a1),f9(f7(a1),f7(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3942,3972,3252,3973,2990,3147,31,2,57,45,39,440,53,37,23,76,228,600])).
% 118.25/118.93 cnf(4025,plain,
% 118.25/118.93 (~E(f9(f7(a1),f7(a1)),f14(a1))),
% 118.25/118.93 inference(scs_inference,[],[3992,4011,31,2])).
% 118.25/118.93 cnf(4033,plain,
% 118.25/118.93 (~E(f9(f7(a1),f7(a1)),a1)),
% 118.25/118.93 inference(scs_inference,[],[4025,4010,31,2])).
% 118.25/118.93 cnf(4057,plain,
% 118.25/118.93 (~P1(f13(f10(x40571),x40572),f13(f11(a1),f11(a1)))),
% 118.25/118.93 inference(scs_inference,[],[3905,1203,31,2,57])).
% 118.25/118.93 cnf(4059,plain,
% 118.25/118.93 (~P1(f13(f10(x40591),x40592),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[3905,1203,31,2,57,45])).
% 118.25/118.93 cnf(4079,plain,
% 118.25/118.93 (~P1(f9(f10(x40791),f10(x40792)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4059,1213,52,50,51,31])).
% 118.25/118.93 cnf(4081,plain,
% 118.25/118.93 (~E(f13(x40811,f7(a1)),f14(a1))),
% 118.25/118.93 inference(scs_inference,[],[4059,3938,1213,52,50,51,31,2])).
% 118.25/118.93 cnf(4082,plain,
% 118.25/118.93 (P1(f13(f10(x40821),x40822),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[4059,3938,1213,2929,52,50,51,31,2,49])).
% 118.25/118.93 cnf(4087,plain,
% 118.25/118.93 (~P1(f9(f10(x40871),f10(x40872)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4059,3938,1213,2929,52,50,51,31,2,49,57,45])).
% 118.25/118.93 cnf(4101,plain,
% 118.25/118.93 (~E(f7(f9(x41011,a1)),f14(a1))),
% 118.25/118.93 inference(scs_inference,[],[4087,4081,3985,52,51,50,31,2])).
% 118.25/118.93 cnf(4102,plain,
% 118.25/118.93 (~P1(f9(f10(x41021),f10(x41022)),f13(f12(a1,a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[4087,4081,3985,52,51,50,31,2,57])).
% 118.25/118.93 cnf(4106,plain,
% 118.25/118.93 (~P3(f2(f7(a1),f12(a1,a1)),f13(f11(a1),f11(a1)))),
% 118.25/118.93 inference(scs_inference,[],[4087,4081,3985,4057,4082,52,51,50,31,2,57,45,39])).
% 118.25/118.93 cnf(4120,plain,
% 118.25/118.93 (~E(f13(f12(x41201,x41202),x41203),a1)),
% 118.25/118.93 inference(scs_inference,[],[4101,3298,4079,52,51,50,31,2])).
% 118.25/118.93 cnf(4133,plain,
% 118.25/118.93 (~E(f13(x41331,f12(x41332,x41333)),a1)),
% 118.25/118.93 inference(scs_inference,[],[3317,3702,31,2])).
% 118.25/118.93 cnf(4136,plain,
% 118.25/118.93 (~P1(f6(f7(a1),f7(a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[3317,3702,31,2,57,45])).
% 118.25/118.93 cnf(4138,plain,
% 118.25/118.93 (~P3(f9(f10(x41381),f10(x41381)),f11(f12(x41382,x41383)))),
% 118.25/118.93 inference(scs_inference,[],[3317,3702,3761,3092,31,2,57,45,39])).
% 118.25/118.93 cnf(4141,plain,
% 118.25/118.93 (~P1(f6(f7(a1),f7(a1)),f2(f11(a1),x41411))),
% 118.25/118.93 inference(scs_inference,[],[3317,3702,3761,3092,31,2,57,45,39,52])).
% 118.25/118.93 cnf(4155,plain,
% 118.25/118.93 (~P1(f2(f7(a1),f12(a1,a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4136,3930,52,51,50,31])).
% 118.25/118.93 cnf(4157,plain,
% 118.25/118.93 (~E(f2(f10(x41571),f9(a1,x41572)),a1)),
% 118.25/118.93 inference(scs_inference,[],[4136,3930,3816,52,51,50,31,2])).
% 118.25/118.93 cnf(4158,plain,
% 118.25/118.93 (~P1(f6(f7(a1),f7(a1)),f13(f12(a1,a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[4136,3930,3816,52,51,50,31,2,57])).
% 118.25/118.93 cnf(4160,plain,
% 118.25/118.93 (~P1(f2(f7(a1),f12(a1,a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4136,3930,3816,52,51,50,31,2,57,45])).
% 118.25/118.93 cnf(4166,plain,
% 118.25/118.93 (P1(f6(f7(a1),f7(a1)),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[4136,3930,3816,3996,2934,2929,52,51,50,31,2,57,45,39,49])).
% 118.25/118.93 cnf(4177,plain,
% 118.25/118.93 (~E(f7(f9(a1,x41771)),a1)),
% 118.25/118.93 inference(scs_inference,[],[4160,4120,3250,52,50,51,31,2])).
% 118.25/118.93 cnf(4180,plain,
% 118.25/118.93 (~P1(f13(f12(x41801,x41802),x41803),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4160,4120,3250,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4187,plain,
% 118.25/118.93 (~P1(f13(f12(x41871,x41872),x41873),f2(f12(a1,a1),x41874))),
% 118.25/118.93 inference(scs_inference,[],[4180,52])).
% 118.25/118.93 cnf(4193,plain,
% 118.25/118.93 (~P1(f13(x41931,f12(x41932,x41933)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4180,4133,52,51,50,31])).
% 118.25/118.93 cnf(4195,plain,
% 118.25/118.93 (~E(f13(f7(a1),x41951),a1)),
% 118.25/118.93 inference(scs_inference,[],[4180,4133,3906,52,51,50,31,2])).
% 118.25/118.93 cnf(4198,plain,
% 118.25/118.93 (~P1(f13(x41981,f12(x41982,x41983)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4180,4133,3906,52,51,50,31,2,57,45])).
% 118.25/118.93 cnf(4206,plain,
% 118.25/118.93 (~P1(f13(x42061,f12(x42062,x42063)),f2(f12(a1,a1),x42064))),
% 118.25/118.93 inference(scs_inference,[],[4198,52])).
% 118.25/118.93 cnf(4212,plain,
% 118.25/118.93 (~P1(f9(f7(a1),f7(a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4198,4033,52,50,51,31])).
% 118.25/118.93 cnf(4214,plain,
% 118.25/118.93 (~E(f13(x42141,f7(a1)),a1)),
% 118.25/118.93 inference(scs_inference,[],[4198,4033,3939,52,50,51,31,2])).
% 118.25/118.93 cnf(4217,plain,
% 118.25/118.93 (~P1(f9(f7(a1),f7(a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4198,4033,3939,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4222,plain,
% 118.25/118.93 (~P1(x42221,f2(f12(a1,a1),x42222))+~E(x42221,f13(f12(x42223,x42224),x42225))),
% 118.25/118.93 inference(scs_inference,[],[4198,4033,3939,4187,3321,3195,52,50,51,31,2,57,45,39,22])).
% 118.25/118.93 cnf(4226,plain,
% 118.25/118.93 (~P1(f9(f7(a1),f7(a1)),f9(x42261,f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[4217,52,50])).
% 118.25/118.93 cnf(4230,plain,
% 118.25/118.93 (~P1(f2(f10(x42301),f9(a1,x42302)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4217,4157,52,50,51,31])).
% 118.25/118.93 cnf(4232,plain,
% 118.25/118.93 (~E(f7(f9(x42321,a1)),a1)),
% 118.25/118.93 inference(scs_inference,[],[4217,4157,3984,52,50,51,31,2])).
% 118.25/118.93 cnf(4235,plain,
% 118.25/118.93 (~P1(f2(f10(x42351),f9(a1,x42352)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4217,4157,3984,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4241,plain,
% 118.25/118.93 (P1(f9(f7(a1),f7(a1)),f2(f7(a1),f12(a1,a1)))),
% 118.25/118.93 inference(scs_inference,[],[4217,4157,3984,3550,3166,2929,52,50,51,31,2,57,45,39,49])).
% 118.25/118.93 cnf(4255,plain,
% 118.25/118.93 (~P1(f7(f9(a1,x42551)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4235,4177,3920,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4259,plain,
% 118.25/118.93 (~E(x42591,f7(f14(a1)))+~E(f12(a1,a1),x42591)),
% 118.25/118.93 inference(scs_inference,[],[4235,3914,4177,3920,4241,4226,52,50,51,31,2,57,45,39,3])).
% 118.25/118.93 cnf(4268,plain,
% 118.25/118.93 (~P1(f13(f7(a1),x42681),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4255,4195,52,50,51,31])).
% 118.25/118.93 cnf(4273,plain,
% 118.25/118.93 (~P1(f13(f7(a1),x42731),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4255,4195,3586,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4292,plain,
% 118.25/118.93 (~P1(f13(x42921,f7(a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4273,4214,836,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4297,plain,
% 118.25/118.93 (~P1(x42971,f2(f12(a1,a1),x42972))+~E(x42971,f13(x42973,f12(x42974,x42975)))),
% 118.25/118.93 inference(scs_inference,[],[4273,4214,836,4206,3622,3056,52,50,51,31,2,57,45,39,22])).
% 118.25/118.93 cnf(4316,plain,
% 118.25/118.93 (~P1(f4(f2(f7(a1),f12(a1,a1)),f12(a1,a1)),f12(a1,a1))),
% 118.25/118.93 inference(scs_inference,[],[4292,4232,958,4082,52,50,51,31,2,57,45,39,53])).
% 118.25/118.93 cnf(4409,plain,
% 118.25/118.93 (~P3(f2(f7(f9(a1,x44091)),f11(a1)),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[911,3922,4268,3226,118,3179,52,50,51,31,2,57,45,39])).
% 118.25/118.93 cnf(4421,plain,
% 118.25/118.93 (~P1(f11(x44211),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4212,72,52,50,51,31])).
% 118.25/118.93 cnf(4439,plain,
% 118.25/118.93 (~P1(f12(x44391,x44392),f11(a1))),
% 118.25/118.93 inference(scs_inference,[],[4421,163,52,50,51,31])).
% 118.25/118.93 cnf(4454,plain,
% 118.25/118.93 (~P1(f12(x44541,x44542),f2(f11(a1),x44543))),
% 118.25/118.93 inference(scs_inference,[],[4439,52])).
% 118.25/118.93 cnf(4475,plain,
% 118.25/118.93 (~P1(f5(x44751,f10(x44752)),f11(f12(x44751,x44753)))),
% 118.25/118.93 inference(scs_inference,[],[4230,3621,52,50,51,31])).
% 118.25/118.93 cnf(4515,plain,
% 118.25/118.93 (~P1(f13(x45151,f12(x45152,x45153)),f13(f11(a1),f11(a1)))),
% 118.25/118.93 inference(scs_inference,[],[718,4193,1097,52,50,51,31,2,57])).
% 118.25/118.93 cnf(4522,plain,
% 118.25/118.93 (~P1(x45221,f2(f11(a1),x45222))+~E(x45221,f12(x45223,x45224))),
% 118.25/118.93 inference(scs_inference,[],[4454,718,4193,1097,3221,2972,52,50,51,31,2,57,45,39,22])).
% 118.25/118.93 cnf(4533,plain,
% 118.25/118.93 (~P1(f2(f7(a1),f12(a1,a1)),f13(f11(a1),f11(a1)))),
% 118.25/118.93 inference(scs_inference,[],[752,4155,515,52,50,51,31,2,57])).
% 118.25/118.93 cnf(4535,plain,
% 118.25/118.93 (~P1(f2(x45351,f11(a1)),f12(f10(x45352),f10(x45352)))),
% 118.25/118.93 inference(scs_inference,[],[752,4155,515,52,50,51,31,2,57,45])).
% 118.25/118.93 cnf(4540,plain,
% 118.25/118.93 (~P1(f9(f14(a1),x45401),f11(f10(x45402)))),
% 118.25/118.93 inference(scs_inference,[],[3206,31])).
% 118.25/118.93 cnf(4559,plain,
% 118.25/118.93 (~E(f9(f13(x45591,f12(x45592,x45593)),f7(a1)),f9(x45594,a1))),
% 118.25/118.93 inference(scs_inference,[],[887,3976,3542,3311,2970,3147,31,2,45,39,23])).
% 118.25/118.93 cnf(4572,plain,
% 118.25/118.93 (~P1(f9(f11(x45721),f12(x45722,x45721)),f11(f2(a1,x45723)))),
% 118.25/118.93 inference(scs_inference,[],[2282,31])).
% 118.25/118.93 cnf(4600,plain,
% 118.25/118.93 (~E(f2(f7(a1),f12(a1,a1)),f2(f11(a1),x46001))),
% 118.25/118.93 inference(scs_inference,[],[902,4102,4141,2252,4166,2990,31,2,45,39,23])).
% 118.25/118.93 cnf(4635,plain,
% 118.25/118.93 (~P3(f9(f10(x46351),f10(x46351)),f12(f10(x46352),f10(x46352)))),
% 118.25/118.93 inference(scs_inference,[],[3210,4535,3810,3154,31,2,45,39])).
% 118.25/118.93 cnf(4639,plain,
% 118.25/118.93 (~E(f13(f10(x46391),x46392),f11(f10(x46393)))),
% 118.25/118.93 inference(scs_inference,[],[3210,4540,4535,3810,2927,3154,31,2,45,39,23])).
% 118.25/118.93 cnf(4649,plain,
% 118.25/118.93 (~P1(x46491,f2(x46492,f10(x46493)))+~E(x46491,f14(f9(x46494,a1)))),
% 118.25/118.93 inference(scs_inference,[],[3335,3005,585,3001,2773,31,2,45,39,22])).
% 118.25/118.93 cnf(4656,plain,
% 118.25/118.93 (~P3(f2(f7(a1),f12(a1,a1)),f11(f2(a1,x46561)))),
% 118.25/118.93 inference(scs_inference,[],[3881,4572,591,3666,31,2,45,39])).
% 118.25/118.93 cnf(4659,plain,
% 118.25/118.93 (E(f13(f6(x46591,f11(f12(x46592,x46591))),x46593),f13(f12(x46592,x46591),x46593))),
% 118.25/118.93 inference(scs_inference,[],[502,5])).
% 118.25/118.93 cnf(4660,plain,
% 118.25/118.93 (E(f13(x46601,f6(x46602,f11(f12(x46603,x46602)))),f13(x46601,f12(x46603,x46602)))),
% 118.25/118.93 inference(scs_inference,[],[502,5,6])).
% 118.25/118.93 cnf(4661,plain,
% 118.25/118.93 (E(f9(x46611,f6(x46612,f11(f12(x46613,x46612)))),f9(x46611,f12(x46613,x46612)))),
% 118.25/118.93 inference(scs_inference,[],[502,5,6,8])).
% 118.25/118.93 cnf(4665,plain,
% 118.25/118.93 (E(f12(x46651,f6(x46652,f11(f12(x46653,x46652)))),f12(x46651,f12(x46653,x46652)))),
% 118.25/118.93 inference(scs_inference,[],[502,5,6,8,11,12,17,18])).
% 118.25/118.93 cnf(4677,plain,
% 118.25/118.93 (E(f12(x46771,x46772),f6(x46772,f11(f12(x46771,x46772))))),
% 118.25/118.93 inference(rename_variables,[],[503])).
% 118.25/118.93 cnf(4679,plain,
% 118.25/118.93 (E(f6(x46791,f11(f12(x46792,x46791))),f12(x46792,x46791))),
% 118.25/118.93 inference(rename_variables,[],[502])).
% 118.25/118.93 cnf(4682,plain,
% 118.25/118.93 (E(f12(x46821,x46822),f6(x46822,f11(f12(x46821,x46822))))),
% 118.25/118.93 inference(rename_variables,[],[503])).
% 118.25/118.93 cnf(4756,plain,
% 118.25/118.93 (P1(x47561,f7(f9(f14(a1),x47562)))),
% 118.25/118.93 inference(rename_variables,[],[2857])).
% 118.25/118.93 cnf(4764,plain,
% 118.25/118.93 (P1(x47641,f6(x47641,f11(f12(x47641,x47642))))),
% 118.25/118.93 inference(rename_variables,[],[2855])).
% 118.25/118.93 cnf(4773,plain,
% 118.25/118.93 (E(f11(f6(x47731,f11(f12(x47732,x47731)))),f11(f12(x47732,x47731)))),
% 118.25/118.93 inference(rename_variables,[],[1117])).
% 118.25/118.93 cnf(4780,plain,
% 118.25/118.93 (E(f11(f6(x47801,f11(f12(x47802,x47801)))),f11(f12(x47802,x47801)))),
% 118.25/118.93 inference(rename_variables,[],[1117])).
% 118.25/118.93 cnf(4781,plain,
% 118.25/118.93 (~P1(f5(x47811,f10(x47812)),f11(f6(x47813,f11(f12(x47811,x47813)))))),
% 118.25/118.93 inference(scs_inference,[],[29,3122,4158,4635,4639,4656,3023,2855,4764,1909,2290,2857,4756,1715,2157,512,1889,2025,1117,4773,4780,517,732,508,4138,4106,4475,4515,4533,3272,3345,502,4679,503,4677,4682,5,6,8,11,12,17,18,20,21,479,233,470,493,3498,3909,4522,4259,250,4649,407,413,428,434,282,3478,3806,4222,4297,409,430,3708,419,436,497,474,13,47,15,16,7,14,440,41,48,4,34,43,42,76,56,10,38,53,9,37,52,19,50,51,31,2,46,44,55,49,3,24,57,25,45,39,22,23])).
% 118.25/118.93 cnf(4803,plain,
% 118.25/118.93 (~P1(f9(f6(x48031,f11(f12(x48032,x48031))),f11(x48031)),f2(f12(a1,a1),x48033))),
% 118.25/118.93 inference(scs_inference,[],[29,3122,4158,4635,4639,4656,3023,2855,4764,1909,2290,2857,4756,1715,2157,512,1889,2025,870,1117,4773,4780,517,732,508,4138,4106,4475,4515,4533,3272,3345,502,4679,503,4677,4682,5,6,8,11,12,17,18,20,21,479,233,470,493,3498,3909,4522,4259,250,4649,407,413,428,434,282,3478,3806,4222,4297,409,430,3708,419,436,497,474,13,47,15,16,7,14,440,41,48,4,34,43,42,76,56,10,38,53,9,37,52,19,50,51,31,2,46,44,55,49,3,24,57,25,45,39,22,23,2771,3687,2345,2354,3627,3427,1657,1688,3304,2121,567,395,40,3565,3769,3669])).
% 118.25/118.93 cnf(4845,plain,
% 118.25/118.93 (~E(f7(a1),f7(f9(a3,a8)))),
% 118.25/118.93 inference(scs_inference,[],[29,618,65,2929,3147,3048,3044,3101,3350,3272,3051,4559,3875,3759,3464,3240,3513,4409,4316,3099,37,9,53,38,4,48,33,7,32,54,8,6,441,661,35,23,22,40,25])).
% 118.25/118.93 cnf(4846,plain,
% 118.25/118.93 (~E(f9(x48461,a1),f9(f7(a3),f7(a8)))),
% 118.25/118.93 inference(scs_inference,[],[29,618,65,2929,3147,3048,3044,3101,3350,3272,3051,4559,3875,3759,3464,3240,3513,4409,4316,3099,37,9,53,38,4,48,33,7,32,54,8,6,441,661,35,23,22,40,25,24])).
% 118.25/118.93 cnf(4877,plain,
% 118.25/118.93 (~P1(x48771,f7(f13(x48772,f10(x48773))))),
% 118.25/118.93 inference(rename_variables,[],[1531])).
% 118.25/118.93 cnf(4898,plain,
% 118.25/118.93 (E(f9(x48981,f6(x48982,f11(f12(x48983,x48982)))),f9(x48981,f12(x48983,x48982)))),
% 118.25/118.93 inference(rename_variables,[],[4661])).
% 118.25/118.93 cnf(4901,plain,
% 118.25/118.93 (E(f9(x49011,f6(x49012,f11(f12(x49013,x49012)))),f9(x49011,f12(x49013,x49012)))),
% 118.25/118.93 inference(rename_variables,[],[4661])).
% 118.25/118.93 cnf(4923,plain,
% 118.25/118.93 (P2(f9(f14(a1),x49231),f9(f14(a1),x49231))),
% 118.25/118.93 inference(rename_variables,[],[3519])).
% 118.25/118.93 cnf(4924,plain,
% 118.25/118.93 (E(f9(x49241,f6(x49242,f11(f12(x49243,x49242)))),f9(x49241,f12(x49243,x49242)))),
% 118.25/118.93 inference(rename_variables,[],[4661])).
% 118.25/118.93 cnf(4934,plain,
% 118.25/118.93 (P3(x49341,f9(f7(f14(a1)),f7(f14(a1))))),
% 118.25/118.93 inference(rename_variables,[],[2157])).
% 118.25/118.93 cnf(4959,plain,
% 118.25/118.93 ($false),
% 118.25/118.93 inference(scs_inference,[],[29,503,618,59,197,480,3048,638,1531,4877,2855,1974,2252,2157,4934,2896,3917,1117,3875,512,3624,4659,4660,4661,4898,4901,4924,4665,2717,1462,2140,2867,1547,1386,4803,236,4781,467,3648,4600,4846,4845,537,3519,4923,2,31,51,50,9,37,53,38,56,76,4,7,48,33,32,41,54,8,30,114,95,4222,661,2771,3627,3708,474,3806,406,427,3687,3909,497,3304,441,4297,4522,460,443,423,402,23,27,26,22,39,40,45,25,57,24,3,55,49,46]),
% 118.25/118.93 ['proof']).
% 118.25/118.93 % SZS output end Proof
% 118.25/118.93 % Total time :117.530000s
%------------------------------------------------------------------------------