%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT009-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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 04:40:12 EDT 2024
% Result : Unsatisfiable 147.26s 147.39s
% Output : CNFRefutation 147.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : CAT009-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n020.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 : Tue Jun 18 12:23:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.46/0.60 start to proof:theBenchmark
% 147.26/147.37 %-------------------------------------------
% 147.26/147.37 % File :CSE---1.7
% 147.26/147.37 % Problem :theBenchmark
% 147.26/147.37 % Transform :cnf
% 147.26/147.37 % Format :tptp:raw
% 147.26/147.37 % Command :java -jar mcs_scs.jar %d %s
% 147.26/147.37
% 147.26/147.37 % Result :Theorem 146.640000s
% 147.26/147.37 % Output :CNFRefutation 146.640000s
% 147.26/147.37 %-------------------------------------------
% 147.26/147.39 %--------------------------------------------------------------------------
% 147.26/147.39 % File : CAT009-1 : TPTP v8.2.0. Released v1.0.0.
% 147.26/147.39 % Domain : Category Theory
% 147.26/147.39 % Problem : If xy is defined, then domain(xy) = domain(y)
% 147.26/147.39 % Version : [Mit67] axioms.
% 147.26/147.39 % English :
% 147.26/147.39
% 147.26/147.39 % Refs : [Mit67] Mitchell (1967), Theory of Categories
% 147.26/147.39 % Source : [ANL]
% 147.26/147.39 % Names : p9.ver1.in [ANL]
% 147.26/147.39
% 147.26/147.39 % Status : Unsatisfiable
% 147.26/147.39 % Rating : 0.00 v6.0.0, 0.22 v5.5.0, 0.38 v5.4.0, 0.33 v5.3.0, 0.42 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.00 v4.0.0, 0.17 v3.5.0, 0.00 v3.1.0, 0.22 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.33 v2.2.0, 0.43 v2.1.0, 0.60 v2.0.0
% 147.26/147.39 % Syntax : Number of clauses : 20 ( 8 unt; 0 nHn; 14 RR)
% 147.26/147.39 % Number of literals : 47 ( 2 equ; 28 neg)
% 147.26/147.39 % Maximal clause size : 4 ( 2 avg)
% 147.26/147.39 % Maximal term depth : 3 ( 1 avg)
% 147.26/147.39 % Number of predicates : 4 ( 3 usr; 0 prp; 1-3 aty)
% 147.26/147.39 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 147.26/147.39 % Number of variables : 52 ( 5 sgn)
% 147.26/147.39 % SPC : CNF_UNS_RFO_SEQ_HRN
% 147.26/147.39
% 147.26/147.39 % Comments :
% 147.26/147.39 %--------------------------------------------------------------------------
% 147.26/147.39 %----Include Mitchell's axioms for category theory
% 147.26/147.39 include('Axioms/CAT001-0.ax').
% 147.26/147.39 %--------------------------------------------------------------------------
% 147.26/147.39 cnf(ba_defined,hypothesis,
% 147.26/147.39 defined(b,a) ).
% 147.26/147.39
% 147.26/147.39 cnf(prove_domain_of_ba_equals_domain_of_a,negated_conjecture,
% 147.26/147.39 domain(compose(b,a)) != domain(a) ).
% 147.26/147.39
% 147.26/147.39 %--------------------------------------------------------------------------
% 147.26/147.39 %-------------------------------------------
% 147.26/147.39 % Proof found
% 147.26/147.39 % SZS status Theorem for theBenchmark
% 147.26/147.39 % SZS output start Proof
% 147.26/147.40 %ClaNum:33(EqnAxiom:13)
% 147.26/147.40 %VarNum:108(SingletonVarNum:52)
% 147.26/147.40 %MaxLitNum:4
% 147.26/147.40 %MaxfuncDepth:2
% 147.26/147.40 %SharedTerms:7
% 147.26/147.40 %goalClause: 21
% 147.26/147.40 %singleGoalClaCount:1
% 147.26/147.40 [16]P2(a3,a4)
% 147.26/147.40 [21]~E(f1(f5(a3,a4)),f1(a4))
% 147.26/147.40 [14]P1(f1(x141))
% 147.26/147.40 [15]P1(f2(x151))
% 147.26/147.40 [17]P2(x171,f1(x171))
% 147.26/147.40 [18]P2(f2(x181),x181)
% 147.26/147.40 [19]P3(x191,f1(x191),x191)
% 147.26/147.40 [20]P3(f2(x201),x201,x201)
% 147.26/147.40 [26]~P2(x261,x262)+P3(x261,x262,f5(x261,x262))
% 147.26/147.40 [25]P2(x251,x252)+~P3(x251,x252,x253)
% 147.26/147.40 [23]~P1(x231)+~P2(x231,x232)+P3(x231,x232,x232)
% 147.26/147.40 [24]~P1(x242)+~P2(x241,x242)+P3(x241,x242,x241)
% 147.26/147.40 [27]P2(x271,x272)+~P3(x272,x274,x273)+~P2(x271,x273)
% 147.26/147.40 [28]P2(x281,x282)+~P3(x284,x281,x283)+~P2(x283,x282)
% 147.26/147.40 [29]~P3(x293,x294,x291)+E(x291,x292)+~P3(x293,x294,x292)
% 147.26/147.40 [22]~P2(x223,x222)+~P2(x221,x223)+P2(x221,x222)+~P1(x223)
% 147.26/147.40 [30]~P3(x305,x302,x304)+P2(x301,x302)+~P3(x303,x305,x301)+~P2(x303,x304)
% 147.26/147.40 [31]~P3(x311,x315,x313)+P2(x311,x312)+~P3(x315,x314,x312)+~P2(x313,x314)
% 147.26/147.40 [32]~P3(x326,x322,x325)+P3(x321,x322,x323)+~P3(x324,x325,x323)+~P3(x324,x326,x321)
% 147.26/147.40 [33]~P3(x331,x336,x334)+P3(x331,x332,x333)+~P3(x334,x335,x333)+~P3(x336,x335,x332)
% 147.26/147.40 %EqnAxiom
% 147.26/147.40 [1]E(x11,x11)
% 147.26/147.40 [2]E(x22,x21)+~E(x21,x22)
% 147.26/147.40 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 147.26/147.40 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 147.26/147.40 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 147.26/147.40 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 147.26/147.40 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 147.26/147.40 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 147.26/147.40 [9]P3(x92,x93,x94)+~E(x91,x92)+~P3(x91,x93,x94)
% 147.26/147.40 [10]P3(x103,x102,x104)+~E(x101,x102)+~P3(x103,x101,x104)
% 147.26/147.40 [11]P3(x113,x114,x112)+~E(x111,x112)+~P3(x113,x114,x111)
% 147.26/147.40 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 147.26/147.40 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 147.26/147.40
% 147.26/147.40 %-------------------------------------------
% 147.26/147.43 cnf(34,plain,
% 147.26/147.43 (~E(f5(a3,a4),a4)),
% 147.26/147.43 inference(scs_inference,[],[21,4])).
% 147.26/147.43 cnf(35,plain,
% 147.26/147.43 (P2(f1(x351),f1(x351))),
% 147.26/147.43 inference(scs_inference,[],[21,19,17,4,28])).
% 147.26/147.43 cnf(38,plain,
% 147.26/147.43 (P2(f1(x381),f2(f1(x381)))),
% 147.26/147.43 inference(scs_inference,[],[21,19,20,17,4,28,27])).
% 147.26/147.43 cnf(41,plain,
% 147.26/147.43 (P3(x411,f1(x412),x412)+~E(x412,x411)),
% 147.26/147.43 inference(scs_inference,[],[21,19,20,17,4,28,27,9])).
% 147.26/147.43 cnf(50,plain,
% 147.26/147.43 (P2(f1(f2(x501)),x501)),
% 147.26/147.43 inference(scs_inference,[],[19,18,28])).
% 147.26/147.43 cnf(51,plain,
% 147.26/147.43 (P3(x511,f1(x511),x511)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(53,plain,
% 147.26/147.43 (P3(x531,x532,x532)+~E(f2(x532),x531)),
% 147.26/147.43 inference(scs_inference,[],[19,20,18,28,9])).
% 147.26/147.43 cnf(54,plain,
% 147.26/147.43 (E(x541,f1(x541))+~E(f2(f1(x541)),x541)),
% 147.26/147.43 inference(scs_inference,[],[19,51,20,18,28,9,29])).
% 147.26/147.43 cnf(65,plain,
% 147.26/147.43 (P2(f1(f1(x651)),f1(x651))),
% 147.26/147.43 inference(scs_inference,[],[19,35,28])).
% 147.26/147.43 cnf(66,plain,
% 147.26/147.43 (P3(x661,f1(x661),x661)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(68,plain,
% 147.26/147.43 (P2(f2(x681),x682)+~E(x681,x682)),
% 147.26/147.43 inference(scs_inference,[],[19,18,35,28,13])).
% 147.26/147.43 cnf(69,plain,
% 147.26/147.43 (P3(x691,x692,x691)+~E(f1(x691),x692)),
% 147.26/147.43 inference(scs_inference,[],[19,66,18,35,28,13,10])).
% 147.26/147.43 cnf(70,plain,
% 147.26/147.43 (P3(x701,f1(x701),x702)+~E(x701,x702)),
% 147.26/147.43 inference(scs_inference,[],[19,66,18,35,28,13,10,11])).
% 147.26/147.43 cnf(71,plain,
% 147.26/147.43 (P2(x711,x712)+~E(f2(x712),x711)),
% 147.26/147.43 inference(scs_inference,[],[19,66,18,35,28,13,10,11,12])).
% 147.26/147.43 cnf(72,plain,
% 147.26/147.43 (P3(f2(x721),x722,x721)+~E(x721,x722)),
% 147.26/147.43 inference(scs_inference,[],[19,66,20,18,35,28,13,10,11,12,33])).
% 147.26/147.43 cnf(85,plain,
% 147.26/147.43 (P2(f1(a3),a4)),
% 147.26/147.43 inference(scs_inference,[],[19,16,28])).
% 147.26/147.43 cnf(88,plain,
% 147.26/147.43 (P2(f1(x881),x882)+~E(f1(x881),x882)),
% 147.26/147.43 inference(scs_inference,[],[19,35,16,28,13])).
% 147.26/147.43 cnf(89,plain,
% 147.26/147.43 (P3(f2(x891),x891,x892)+~E(x891,x892)),
% 147.26/147.43 inference(scs_inference,[],[19,20,35,16,28,13,11])).
% 147.26/147.43 cnf(98,plain,
% 147.26/147.43 (P2(f1(f1(x981)),f2(f1(x981)))),
% 147.26/147.43 inference(scs_inference,[],[19,38,28])).
% 147.26/147.43 cnf(99,plain,
% 147.26/147.43 (P3(x991,f1(x991),x991)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(101,plain,
% 147.26/147.43 (P2(x1011,x1012)+~E(f1(x1011),x1012)),
% 147.26/147.43 inference(scs_inference,[],[19,17,38,28,13])).
% 147.26/147.43 cnf(103,plain,
% 147.26/147.43 (~P3(x1031,f2(f1(x1032)),x1032)+P3(x1031,f1(x1032),x1032)),
% 147.26/147.43 inference(scs_inference,[],[19,99,20,35,17,38,28,13,12,33])).
% 147.26/147.43 cnf(106,plain,
% 147.26/147.43 (~P3(f1(x1061),f1(x1061),x1062)+P2(x1062,f1(f1(x1061)))),
% 147.26/147.43 inference(scs_inference,[],[19,99,20,35,17,38,28,13,12,33,30])).
% 147.26/147.43 cnf(114,plain,
% 147.26/147.43 (P2(f1(f1(a3)),a4)),
% 147.26/147.43 inference(scs_inference,[],[19,85,28])).
% 147.26/147.43 cnf(115,plain,
% 147.26/147.43 (P3(x1151,f1(x1151),x1151)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(117,plain,
% 147.26/147.43 (P2(f1(f2(x1171)),x1172)+~E(x1171,x1172)),
% 147.26/147.43 inference(scs_inference,[],[19,50,85,28,13])).
% 147.26/147.43 cnf(118,plain,
% 147.26/147.43 (P2(x1181,f1(x1182))+~E(x1182,x1181)),
% 147.26/147.43 inference(scs_inference,[],[19,17,50,85,28,13,12])).
% 147.26/147.43 cnf(119,plain,
% 147.26/147.43 (~P3(f1(x1191),x1192,f1(x1191))+P3(x1191,x1192,x1191)),
% 147.26/147.43 inference(scs_inference,[],[19,115,17,50,85,28,13,12,32])).
% 147.26/147.43 cnf(121,plain,
% 147.26/147.43 (~P3(f1(f2(x1211)),x1211,x1212)+P2(f2(x1211),x1212)),
% 147.26/147.43 inference(scs_inference,[],[19,115,18,17,50,85,28,13,12,32,31])).
% 147.26/147.43 cnf(122,plain,
% 147.26/147.43 (P3(x1221,f1(x1221),x1221)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(124,plain,
% 147.26/147.43 (~P3(f1(f2(x1241)),x1241,x1242)+P2(x1242,f1(x1241))),
% 147.26/147.43 inference(scs_inference,[],[19,115,122,18,17,50,85,28,13,12,32,31,30])).
% 147.26/147.43 cnf(129,plain,
% 147.26/147.43 (P2(a3,x1291)+~E(a4,x1291)),
% 147.26/147.43 inference(scs_inference,[],[16,13])).
% 147.26/147.43 cnf(130,plain,
% 147.26/147.43 (P2(f1(a3),x1301)+~E(a4,x1301)),
% 147.26/147.43 inference(scs_inference,[],[19,16,13,28])).
% 147.26/147.43 cnf(151,plain,
% 147.26/147.43 (P2(x1511,a4)+~E(a3,x1511)),
% 147.26/147.43 inference(scs_inference,[],[16,65,13,12])).
% 147.26/147.43 cnf(152,plain,
% 147.26/147.43 (~P3(x1521,f1(x1521),x1522)+P2(x1522,f1(f1(x1521)))),
% 147.26/147.43 inference(scs_inference,[],[19,17,16,65,13,12,30])).
% 147.26/147.43 cnf(153,plain,
% 147.26/147.43 (P3(x1531,f1(x1531),x1531)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(155,plain,
% 147.26/147.43 (~P3(f1(x1551),f1(x1551),x1552)+P2(x1551,x1552)),
% 147.26/147.43 inference(scs_inference,[],[19,153,17,16,65,13,12,30,31])).
% 147.26/147.43 cnf(160,plain,
% 147.26/147.43 (P2(f1(f1(a3)),x1601)+~E(a4,x1601)),
% 147.26/147.43 inference(scs_inference,[],[114,13])).
% 147.26/147.43 cnf(161,plain,
% 147.26/147.43 (P2(x1611,f2(f1(x1612)))+~E(f1(x1612),x1611)),
% 147.26/147.43 inference(scs_inference,[],[38,114,13,12])).
% 147.26/147.43 cnf(171,plain,
% 147.26/147.43 (P2(f1(x1711),a4)+~E(f1(a3),x1711)),
% 147.26/147.43 inference(scs_inference,[],[19,85,12,28])).
% 147.26/147.43 cnf(190,plain,
% 147.26/147.43 (P2(x1901,f1(x1902))+~E(f1(f1(x1902)),x1901)),
% 147.26/147.43 inference(scs_inference,[],[65,12])).
% 147.26/147.43 cnf(191,plain,
% 147.26/147.43 (P2(f1(x1911),f1(x1912))+~E(f1(f1(x1912)),x1911)),
% 147.26/147.43 inference(scs_inference,[],[19,65,12,28])).
% 147.26/147.43 cnf(200,plain,
% 147.26/147.43 (P2(x2001,f2(f1(x2002)))+~E(f1(f1(x2002)),x2001)),
% 147.26/147.43 inference(scs_inference,[],[98,12])).
% 147.26/147.43 cnf(201,plain,
% 147.26/147.43 (P2(f1(x2011),f2(f1(x2012)))+~E(f1(f1(x2012)),x2011)),
% 147.26/147.43 inference(scs_inference,[],[19,98,12,28])).
% 147.26/147.43 cnf(210,plain,
% 147.26/147.43 (P2(x2101,a4)+~E(f1(f1(a3)),x2101)),
% 147.26/147.43 inference(scs_inference,[],[114,12])).
% 147.26/147.43 cnf(211,plain,
% 147.26/147.43 (P2(f1(x2111),a4)+~E(f1(f1(a3)),x2111)),
% 147.26/147.43 inference(scs_inference,[],[19,114,12,28])).
% 147.26/147.43 cnf(227,plain,
% 147.26/147.43 (~E(a4,f5(a3,a4))),
% 147.26/147.43 inference(scs_inference,[],[21,2,4])).
% 147.26/147.43 cnf(244,plain,
% 147.26/147.43 (~P3(f1(a3),a4,x2441)+P2(a3,x2441)),
% 147.26/147.43 inference(scs_inference,[],[19,16,31])).
% 147.26/147.43 cnf(264,plain,
% 147.26/147.43 (P3(x2641,f1(x2641),f5(x2641,f1(x2641)))),
% 147.26/147.43 inference(scs_inference,[],[19,25,26])).
% 147.26/147.43 cnf(265,plain,
% 147.26/147.43 (E(x2651,f5(x2651,f1(x2651)))),
% 147.26/147.43 inference(scs_inference,[],[19,264,29])).
% 147.26/147.43 cnf(268,plain,
% 147.26/147.43 (P3(f5(x2681,f1(x2681)),f1(x2681),x2681)),
% 147.26/147.43 inference(scs_inference,[],[19,264,29,9])).
% 147.26/147.43 cnf(269,plain,
% 147.26/147.43 (P3(f2(x2691),x2691,f5(x2691,f1(x2691)))),
% 147.26/147.43 inference(scs_inference,[],[19,20,264,29,9,11])).
% 147.26/147.43 cnf(270,plain,
% 147.26/147.43 (P3(f2(x2701),x2701,x2701)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(271,plain,
% 147.26/147.43 (P3(f2(x2711),f5(x2711,f1(x2711)),x2711)),
% 147.26/147.43 inference(scs_inference,[],[19,20,270,264,29,9,11,10])).
% 147.26/147.43 cnf(272,plain,
% 147.26/147.43 (P3(f2(x2721),x2721,x2721)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(273,plain,
% 147.26/147.43 (P2(f5(x2731,f1(x2731)),f1(x2731))),
% 147.26/147.43 inference(scs_inference,[],[19,20,270,264,17,29,9,11,10,12])).
% 147.26/147.43 cnf(275,plain,
% 147.26/147.43 (P2(f2(x2751),f5(x2751,f1(x2751)))),
% 147.26/147.43 inference(scs_inference,[],[19,20,270,264,18,17,29,9,11,10,12,13])).
% 147.26/147.43 cnf(277,plain,
% 147.26/147.43 (P3(f2(f2(x2771)),x2771,x2771)),
% 147.26/147.43 inference(scs_inference,[],[19,20,270,272,264,18,17,29,9,11,10,12,13,33])).
% 147.26/147.43 cnf(285,plain,
% 147.26/147.43 (E(f5(x2851,f1(x2851)),x2851)),
% 147.26/147.43 inference(scs_inference,[],[265,2])).
% 147.26/147.43 cnf(288,plain,
% 147.26/147.43 (E(x2881,f5(x2881,f1(x2881)))),
% 147.26/147.43 inference(rename_variables,[],[265])).
% 147.26/147.43 cnf(290,plain,
% 147.26/147.43 (E(x2901,f5(x2901,f1(x2901)))),
% 147.26/147.43 inference(rename_variables,[],[265])).
% 147.26/147.43 cnf(293,plain,
% 147.26/147.43 (E(x2931,f5(x2931,f1(x2931)))),
% 147.26/147.43 inference(rename_variables,[],[265])).
% 147.26/147.43 cnf(295,plain,
% 147.26/147.43 (E(x2951,f5(x2951,f1(x2951)))),
% 147.26/147.43 inference(rename_variables,[],[265])).
% 147.26/147.43 cnf(296,plain,
% 147.26/147.43 (~E(f5(a3,a4),f5(a4,f1(a4)))),
% 147.26/147.43 inference(scs_inference,[],[265,288,290,293,34,2,117,129,130,151,160,3])).
% 147.26/147.43 cnf(297,plain,
% 147.26/147.43 (P3(f5(x2971,f1(x2971)),f1(x2971),f5(x2971,f1(x2971)))),
% 147.26/147.43 inference(scs_inference,[],[265,288,290,293,295,34,264,2,117,129,130,151,160,3,9])).
% 147.26/147.43 cnf(299,plain,
% 147.26/147.43 (P3(f2(x2991),f5(x2991,f1(x2991)),f5(x2991,f1(x2991)))),
% 147.26/147.43 inference(scs_inference,[],[265,288,290,293,295,34,264,269,2,117,129,130,151,160,3,9,10])).
% 147.26/147.43 cnf(305,plain,
% 147.26/147.43 (P3(x3051,f1(f1(x3051)),x3051)),
% 147.26/147.43 inference(scs_inference,[],[19,265,288,290,293,295,34,264,268,269,277,2,117,129,130,151,160,3,9,10,11,13,32])).
% 147.26/147.43 cnf(306,plain,
% 147.26/147.43 (P3(x3061,f1(x3061),x3061)),
% 147.26/147.43 inference(rename_variables,[],[19])).
% 147.26/147.43 cnf(308,plain,
% 147.26/147.43 (P2(x3081,f1(f1(x3081)))),
% 147.26/147.43 inference(scs_inference,[],[19,306,265,288,290,293,295,34,264,268,273,269,277,2,117,129,130,151,160,3,9,10,11,13,32,30])).
% 147.26/147.43 cnf(317,plain,
% 147.26/147.43 (P3(x3171,f1(f1(x3171)),f5(x3171,f1(x3171)))),
% 147.26/147.43 inference(scs_inference,[],[19,297,268,32])).
% 147.26/147.43 cnf(321,plain,
% 147.26/147.43 (~P1(f5(x3211,f1(x3211)))+P1(x3211)),
% 147.26/147.43 inference(scs_inference,[],[19,285,297,268,32,8])).
% 147.26/147.43 cnf(328,plain,
% 147.26/147.43 (P3(f2(x3281),x3281,f2(x3281))+~P1(f5(x3281,f1(x3281)))),
% 147.26/147.43 inference(scs_inference,[],[18,321,24])).
% 147.26/147.43 cnf(329,plain,
% 147.26/147.43 (P3(f5(x3291,f1(x3291)),f1(f1(x3291)),x3291)),
% 147.26/147.43 inference(scs_inference,[],[265,305,9])).
% 147.26/147.43 cnf(331,plain,
% 147.26/147.43 (P3(f2(f2(x3311)),f5(x3311,f1(x3311)),x3311)),
% 147.26/147.43 inference(scs_inference,[],[265,277,305,9,10])).
% 147.26/147.43 cnf(352,plain,
% 147.26/147.43 (~P3(f1(x3521),f1(x3521),x3522)+P3(x3521,x3522,f5(x3521,x3522))),
% 147.26/147.43 inference(scs_inference,[],[155,26])).
% 147.26/147.43 cnf(354,plain,
% 147.26/147.43 (P2(f2(x3541),f2(x3541))),
% 147.26/147.43 inference(scs_inference,[],[20,18,27])).
% 147.26/147.43 cnf(355,plain,
% 147.26/147.43 (P2(f2(x3551),x3551)),
% 147.26/147.43 inference(rename_variables,[],[18])).
% 147.26/147.43 cnf(357,plain,
% 147.26/147.43 (P2(f1(f2(x3571)),f2(x3571))),
% 147.26/147.43 inference(scs_inference,[],[20,19,18,27,28])).
% 147.26/147.43 cnf(362,plain,
% 147.26/147.43 (P3(f2(x3621),x3621,x3621)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(364,plain,
% 147.26/147.43 (~P3(f1(x3641),f2(f1(x3641)),x3642)+P2(x3642,f1(x3641))),
% 147.26/147.43 inference(scs_inference,[],[20,362,19,35,18,355,269,27,28,31,30])).
% 147.26/147.43 cnf(367,plain,
% 147.26/147.43 (P2(f5(x3671,f1(x3671)),f1(x3672))+~P3(f1(x3672),f2(f1(x3672)),x3671)),
% 147.26/147.43 inference(scs_inference,[],[20,362,19,265,35,18,355,269,27,28,31,30,12])).
% 147.26/147.43 cnf(373,plain,
% 147.26/147.43 (P2(a3,f2(a4))),
% 147.26/147.43 inference(scs_inference,[],[20,16,27])).
% 147.26/147.43 cnf(374,plain,
% 147.26/147.43 (P3(f2(x3741),x3741,x3741)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(376,plain,
% 147.26/147.43 (P2(f5(a3,f1(a3)),f2(a4))),
% 147.26/147.43 inference(scs_inference,[],[20,265,16,27,12])).
% 147.26/147.43 cnf(378,plain,
% 147.26/147.43 (P2(f2(f2(x3781)),x3781)),
% 147.26/147.43 inference(scs_inference,[],[20,374,265,16,275,271,27,12,31])).
% 147.26/147.43 cnf(380,plain,
% 147.26/147.43 (P3(f2(x3801),x3801,x3801)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(382,plain,
% 147.26/147.43 (~P3(f2(x3821),f2(x3821),x3822)+P2(x3822,x3821)),
% 147.26/147.43 inference(scs_inference,[],[20,374,380,265,18,16,275,271,27,12,31,30])).
% 147.26/147.43 cnf(391,plain,
% 147.26/147.43 (~P3(f2(x3911),f2(x3911),x3912)+P3(x3912,x3911,f5(x3912,x3911))),
% 147.26/147.43 inference(scs_inference,[],[382,26])).
% 147.26/147.43 cnf(392,plain,
% 147.26/147.43 (P2(f1(a3),f2(a4))),
% 147.26/147.43 inference(scs_inference,[],[20,85,27])).
% 147.26/147.43 cnf(393,plain,
% 147.26/147.43 (P3(f2(x3931),x3931,x3931)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(395,plain,
% 147.26/147.43 (~P3(a3,f2(a4),x3951)+P2(x3951,a4)),
% 147.26/147.43 inference(scs_inference,[],[20,393,16,85,27,30])).
% 147.26/147.43 cnf(406,plain,
% 147.26/147.43 (P2(x4061,f2(f1(x4061)))),
% 147.26/147.43 inference(scs_inference,[],[20,17,27])).
% 147.26/147.43 cnf(407,plain,
% 147.26/147.43 (P3(f2(x4071),x4071,x4071)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(411,plain,
% 147.26/147.43 (~P3(f1(a3),f2(a4),x4111)+P2(x4111,a4)),
% 147.26/147.43 inference(scs_inference,[],[20,407,265,85,17,27,12,13,30])).
% 147.26/147.43 cnf(412,plain,
% 147.26/147.43 (P3(f2(x4121),x4121,x4121)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(414,plain,
% 147.26/147.43 (~P3(f1(x4141),f1(x4141),x4142)+P2(f2(f1(x4141)),x4142)),
% 147.26/147.43 inference(scs_inference,[],[20,407,412,265,35,85,17,27,12,13,30,31])).
% 147.26/147.43 cnf(418,plain,
% 147.26/147.43 (P2(f1(f1(a3)),f2(a4))),
% 147.26/147.43 inference(scs_inference,[],[20,114,27])).
% 147.26/147.43 cnf(419,plain,
% 147.26/147.43 (P3(f2(x4191),x4191,x4191)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(421,plain,
% 147.26/147.43 (~P3(x4211,f2(f1(x4211)),x4212)+P2(x4212,f1(x4211))),
% 147.26/147.43 inference(scs_inference,[],[20,419,17,114,27,30])).
% 147.26/147.43 cnf(424,plain,
% 147.26/147.43 (P2(f5(x4241,f1(x4241)),f1(x4242))+~P3(x4242,f2(f1(x4242)),x4241)),
% 147.26/147.43 inference(scs_inference,[],[20,419,265,17,114,27,30,12])).
% 147.26/147.43 cnf(430,plain,
% 147.26/147.43 (P2(a3,f2(f2(a4)))),
% 147.26/147.43 inference(scs_inference,[],[20,373,27])).
% 147.26/147.43 cnf(445,plain,
% 147.26/147.43 (P2(f2(x4451),f2(f2(x4451)))),
% 147.26/147.43 inference(scs_inference,[],[20,354,27])).
% 147.26/147.43 cnf(471,plain,
% 147.26/147.43 (P2(f1(a3),f2(f2(a4)))),
% 147.26/147.43 inference(scs_inference,[],[20,392,27])).
% 147.26/147.43 cnf(485,plain,
% 147.26/147.43 (P2(f1(f1(a3)),f2(f2(a4)))),
% 147.26/147.43 inference(scs_inference,[],[20,418,27])).
% 147.26/147.43 cnf(486,plain,
% 147.26/147.43 (P3(f2(x4861),x4861,x4861)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(488,plain,
% 147.26/147.43 (~P3(f5(x4881,f1(x4881)),f2(f1(x4881)),x4882)+P2(x4882,f1(x4881))),
% 147.26/147.43 inference(scs_inference,[],[20,486,273,418,27,30])).
% 147.26/147.43 cnf(510,plain,
% 147.26/147.43 (P3(f2(x5101),x5101,x5101)),
% 147.26/147.43 inference(rename_variables,[],[20])).
% 147.26/147.43 cnf(515,plain,
% 147.26/147.43 (P2(f5(x5151,f1(x5151)),f2(x5152))+~P3(f2(x5152),f2(f2(x5152)),x5151)),
% 147.26/147.43 inference(scs_inference,[],[20,510,265,354,30,27,12])).
% 147.26/147.43 cnf(594,plain,
% 147.26/147.43 (~P3(f1(x5941),f2(f1(x5941)),x5942)+P2(f2(f1(x5941)),x5942)),
% 147.26/147.44 inference(scs_inference,[],[20,38,31])).
% 147.26/147.44 cnf(642,plain,
% 147.26/147.44 (~P3(f2(x6421),f2(x6421),x6422)+P2(f2(f2(x6421)),x6422)),
% 147.26/147.44 inference(scs_inference,[],[20,354,31])).
% 147.26/147.44 cnf(666,plain,
% 147.26/147.44 (~P3(x6661,f2(f1(x6661)),x6662)+P2(f2(x6661),x6662)),
% 147.26/147.44 inference(scs_inference,[],[20,406,31])).
% 147.26/147.44 cnf(727,plain,
% 147.26/147.44 (P2(f5(f1(a3),f2(a4)),a4)),
% 147.26/147.44 inference(scs_inference,[],[392,411,26])).
% 147.26/147.44 cnf(728,plain,
% 147.26/147.44 (P2(f5(f1(a3),f2(a4)),f5(a4,f1(a4)))),
% 147.26/147.44 inference(scs_inference,[],[265,727,13])).
% 147.26/147.44 cnf(729,plain,
% 147.26/147.44 (E(x7291,f5(x7291,f1(x7291)))),
% 147.26/147.44 inference(rename_variables,[],[265])).
% 147.26/147.44 cnf(730,plain,
% 147.26/147.44 (~P3(f2(x7301),f2(x7301),x7302)+P2(x7302,f1(f2(x7301)))),
% 147.26/147.44 inference(scs_inference,[],[265,19,354,727,13,30])).
% 147.26/147.44 cnf(731,plain,
% 147.26/147.44 (P3(x7311,f1(x7311),x7311)),
% 147.26/147.44 inference(rename_variables,[],[19])).
% 147.26/147.44 cnf(735,plain,
% 147.26/147.44 (P2(f5(x7351,f1(x7351)),f1(f2(x7352)))+~P3(f2(x7352),f2(x7352),x7351)),
% 147.26/147.44 inference(scs_inference,[],[265,729,19,731,354,727,13,30,28,12])).
% 147.26/147.44 cnf(802,plain,
% 147.26/147.44 (~P3(f1(a3),f2(a4),x8021)+P2(a3,x8021)),
% 147.26/147.44 inference(scs_inference,[],[19,373,31])).
% 147.26/147.44 cnf(840,plain,
% 147.26/147.44 (~P3(f1(x8401),f2(f1(x8401)),x8402)+P2(x8401,x8402)),
% 147.26/147.44 inference(scs_inference,[],[19,406,31])).
% 147.26/147.44 cnf(893,plain,
% 147.26/147.44 (P2(a3,f5(f1(a3),f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[392,802,26])).
% 147.26/147.44 cnf(894,plain,
% 147.26/147.44 (P2(f1(a3),f5(f1(a3),f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[19,893,28])).
% 147.26/147.44 cnf(908,plain,
% 147.26/147.44 (E(f5(x9081,f5(x9082,f1(x9082))),f5(x9081,x9082))),
% 147.26/147.44 inference(scs_inference,[],[265,7,2])).
% 147.26/147.44 cnf(923,plain,
% 147.26/147.44 (~P3(f1(f2(x9231)),x9231,x9232)+P3(f2(x9231),x9232,f5(f2(x9231),x9232))),
% 147.26/147.44 inference(scs_inference,[],[121,26])).
% 147.26/147.44 cnf(924,plain,
% 147.26/147.44 (~P3(f1(f2(x9241)),x9241,x9242)+P3(x9242,f1(x9241),f5(x9242,f1(x9241)))),
% 147.26/147.44 inference(scs_inference,[],[124,26])).
% 147.26/147.44 cnf(940,plain,
% 147.26/147.44 (~P3(x9401,f2(f1(x9401)),x9402)+P3(x9402,f1(x9401),f5(x9402,f1(x9401)))),
% 147.26/147.44 inference(scs_inference,[],[421,26])).
% 147.26/147.44 cnf(996,plain,
% 147.26/147.44 (P3(f5(x9961,f1(x9961)),f1(x9961),x9961)),
% 147.26/147.44 inference(rename_variables,[],[268])).
% 147.26/147.44 cnf(998,plain,
% 147.26/147.44 (P2(f5(a3,f1(a3)),f5(x9981,f1(x9981)))+~P3(f1(a3),a4,x9981)),
% 147.26/147.44 inference(scs_inference,[],[268,996,16,31,27])).
% 147.26/147.44 cnf(1004,plain,
% 147.26/147.44 (~P3(f1(x10041),f1(x10041),x10042)+P2(f5(x10041,f1(x10041)),x10042)),
% 147.26/147.44 inference(scs_inference,[],[268,17,31])).
% 147.26/147.44 cnf(1031,plain,
% 147.26/147.44 (~P3(f1(x10311),f2(f1(x10311)),x10312)+P2(f5(x10311,f1(x10311)),x10312)),
% 147.26/147.44 inference(scs_inference,[],[268,406,31])).
% 147.26/147.44 cnf(1050,plain,
% 147.26/147.44 (P2(f5(f1(a3),f2(a4)),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[269,728,27])).
% 147.26/147.44 cnf(1179,plain,
% 147.26/147.44 (~P3(f5(x11791,f1(x11791)),f2(f1(x11791)),x11792)+P2(f2(x11791),x11792)),
% 147.26/147.44 inference(scs_inference,[],[271,406,31])).
% 147.26/147.44 cnf(1203,plain,
% 147.26/147.44 (~P3(x12031,f2(f1(x12031)),x12032)+P3(f2(x12031),x12032,f5(f2(x12031),x12032))),
% 147.26/147.44 inference(scs_inference,[],[666,26])).
% 147.26/147.44 cnf(1291,plain,
% 147.26/147.44 (~P3(f2(f2(x12911)),f2(f2(x12911)),x12912)+P2(x12912,x12911)),
% 147.26/147.44 inference(scs_inference,[],[277,378,30])).
% 147.26/147.44 cnf(1334,plain,
% 147.26/147.44 (P3(f2(f2(x13341)),x13341,x13341)),
% 147.26/147.44 inference(rename_variables,[],[277])).
% 147.26/147.44 cnf(1338,plain,
% 147.26/147.44 (P2(f2(f2(a3)),f5(x13381,f1(x13381)))+~P3(a3,f2(f2(a4)),x13381)),
% 147.26/147.44 inference(scs_inference,[],[277,1334,265,430,31,27,13])).
% 147.26/147.44 cnf(1343,plain,
% 147.26/147.44 (~P3(x13431,f2(f1(x13431)),x13432)+P2(f2(f2(x13431)),x13432)),
% 147.26/147.44 inference(scs_inference,[],[277,406,31])).
% 147.26/147.44 cnf(1361,plain,
% 147.26/147.44 (~P3(f1(x13611),f2(f1(x13611)),x13612)+P3(x13611,x13612,f5(x13611,x13612))),
% 147.26/147.44 inference(scs_inference,[],[840,26])).
% 147.26/147.44 cnf(1369,plain,
% 147.26/147.44 (~P3(f1(x13691),f1(x13691),x13692)+P3(x13692,f1(f1(x13691)),f5(x13692,f1(f1(x13691))))),
% 147.26/147.44 inference(scs_inference,[],[106,26])).
% 147.26/147.44 cnf(1408,plain,
% 147.26/147.44 (~P3(f1(f2(x14081)),x14081,x14082)+P2(x14082,f1(f1(x14081)))),
% 147.26/147.44 inference(scs_inference,[],[305,50,30])).
% 147.26/147.44 cnf(1516,plain,
% 147.26/147.44 (~P3(f1(f1(x15161)),f1(f1(x15161)),x15162)+P2(x15161,x15162)),
% 147.26/147.44 inference(scs_inference,[],[305,308,31])).
% 147.26/147.44 cnf(1544,plain,
% 147.26/147.44 (P3(x15441,f1(x15441),x15441)),
% 147.26/147.44 inference(rename_variables,[],[19])).
% 147.26/147.44 cnf(1550,plain,
% 147.26/147.44 (P3(x15501,f1(x15501),f1(f1(x15501)))+~E(f5(x15501,f1(x15501)),f1(f1(x15501)))),
% 147.26/147.44 inference(scs_inference,[],[285,19,1544,20,264,305,33,32,8,11])).
% 147.26/147.44 cnf(1567,plain,
% 147.26/147.44 (~P3(x15671,f5(x15672,f1(x15672)),f1(x15672))+P3(x15671,x15672,f1(x15672))),
% 147.26/147.44 inference(scs_inference,[],[19,329,33])).
% 147.26/147.44 cnf(1711,plain,
% 147.26/147.44 (~P3(f1(f1(x17111)),f1(f1(x17111)),x17112)+P2(f5(x17111,f1(x17111)),x17112)),
% 147.26/147.44 inference(scs_inference,[],[329,308,31])).
% 147.26/147.44 cnf(1777,plain,
% 147.26/147.44 (P3(f2(f1(x17771)),f1(x17771),f2(f1(x17771)))),
% 147.26/147.44 inference(scs_inference,[],[265,14,328,8])).
% 147.26/147.44 cnf(1870,plain,
% 147.26/147.44 (~P3(f1(x18701),f2(f1(x18701)),x18702)+P3(x18702,f1(x18701),f5(x18702,f1(x18701)))),
% 147.26/147.44 inference(scs_inference,[],[364,26])).
% 147.26/147.44 cnf(1873,plain,
% 147.26/147.44 (~P3(f1(x18731),f1(x18731),x18732)+P3(f2(f1(x18731)),x18732,f5(f2(f1(x18731)),x18732))),
% 147.26/147.44 inference(scs_inference,[],[414,26])).
% 147.26/147.44 cnf(1894,plain,
% 147.26/147.44 (~P3(f2(x18941),f2(x18941),x18942)+P3(f2(f2(x18941)),x18942,f5(f2(f2(x18941)),x18942))),
% 147.26/147.44 inference(scs_inference,[],[642,26])).
% 147.26/147.44 cnf(1899,plain,
% 147.26/147.44 (~P3(f2(x18991),f2(x18991),x18992)+P3(x18992,f1(f2(x18991)),f5(x18992,f1(f2(x18991))))),
% 147.26/147.44 inference(scs_inference,[],[730,26])).
% 147.26/147.44 cnf(1909,plain,
% 147.26/147.44 (~P3(f2(f2(x19091)),f2(f2(x19091)),x19092)+P3(x19092,x19091,f5(x19092,x19091))),
% 147.26/147.44 inference(scs_inference,[],[1291,26])).
% 147.26/147.44 cnf(1910,plain,
% 147.26/147.44 (E(f2(f1(x19101)),f1(x19101))),
% 147.26/147.44 inference(scs_inference,[],[1777,20,29])).
% 147.26/147.44 cnf(1913,plain,
% 147.26/147.44 (~E(f1(f5(a3,a4)),f2(f1(a4)))),
% 147.26/147.44 inference(scs_inference,[],[1777,21,20,29,3])).
% 147.26/147.44 cnf(1915,plain,
% 147.26/147.44 (E(f1(a4),f2(f1(a4)))),
% 147.26/147.44 inference(scs_inference,[],[1777,21,20,29,3,53,2])).
% 147.26/147.44 cnf(1943,plain,
% 147.26/147.44 (P3(f1(x19431),f1(x19431),f1(x19431))),
% 147.26/147.44 inference(scs_inference,[],[1910,1915,72,70,53])).
% 147.26/147.44 cnf(1947,plain,
% 147.26/147.44 (E(f1(x19471),f2(f1(x19471)))),
% 147.26/147.44 inference(scs_inference,[],[1910,1915,72,70,53,118,41,69,2])).
% 147.26/147.44 cnf(1963,plain,
% 147.26/147.44 (P3(f2(f1(x19631)),f2(f1(x19631)),f1(x19631))),
% 147.26/147.44 inference(scs_inference,[],[1947,72])).
% 147.26/147.44 cnf(1965,plain,
% 147.26/147.44 (P3(f1(x19651),f1(f1(x19651)),f2(f1(x19651)))),
% 147.26/147.44 inference(scs_inference,[],[1947,72,70])).
% 147.26/147.44 cnf(1968,plain,
% 147.26/147.44 (P3(x19681,f2(f1(x19681)),x19681)),
% 147.26/147.44 inference(scs_inference,[],[1947,72,70,118,41,69])).
% 147.26/147.44 cnf(1969,plain,
% 147.26/147.44 (P3(f5(x19691,f1(x19691)),f2(f1(x19691)),x19691)),
% 147.26/147.44 inference(scs_inference,[],[265,1947,72,70,118,41,69,9])).
% 147.26/147.44 cnf(1971,plain,
% 147.26/147.44 (P3(f1(x19711),f2(f1(x19711)),f2(f1(x19711)))),
% 147.26/147.44 inference(scs_inference,[],[1777,265,1947,72,70,118,41,69,9,11,32])).
% 147.26/147.44 cnf(2005,plain,
% 147.26/147.44 (P3(f1(x20051),f2(f1(x20051)),f1(x20051))),
% 147.26/147.44 inference(scs_inference,[],[20,1963,32])).
% 147.26/147.44 cnf(2011,plain,
% 147.26/147.44 (P3(f1(x20111),f1(x20111),f2(f1(x20111)))),
% 147.26/147.44 inference(scs_inference,[],[1910,1777,9])).
% 147.26/147.44 cnf(2015,plain,
% 147.26/147.44 (~P3(a4,f1(a4),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[296,264,29])).
% 147.26/147.44 cnf(2016,plain,
% 147.26/147.44 (P3(x20161,f1(x20161),f5(x20161,f1(x20161)))),
% 147.26/147.44 inference(rename_variables,[],[264])).
% 147.26/147.44 cnf(2020,plain,
% 147.26/147.44 (~P3(f2(a4),a4,f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[19,296,20,264,2016,29,11,32])).
% 147.26/147.44 cnf(2029,plain,
% 147.26/147.44 (P3(x20291,f1(x20291),x20291)),
% 147.26/147.44 inference(rename_variables,[],[19])).
% 147.26/147.44 cnf(2032,plain,
% 147.26/147.44 (~P3(f2(f2(a4)),a4,f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[2015,19,2029,296,264,277,317,29,33,32])).
% 147.26/147.44 cnf(2051,plain,
% 147.26/147.44 (~P3(f2(a4),f5(a4,f1(a4)),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[296,299,29])).
% 147.26/147.44 cnf(2064,plain,
% 147.26/147.44 (~P3(f1(a4),f1(f1(a4)),f1(f5(a3,a4)))),
% 147.26/147.44 inference(scs_inference,[],[1913,1965,29])).
% 147.26/147.44 cnf(2067,plain,
% 147.26/147.44 (~P3(f2(a4),f2(a4),x20671)+~P3(x20671,a4,f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[1913,2051,269,1965,29,33])).
% 147.26/147.44 cnf(2072,plain,
% 147.26/147.44 (~P3(f2(a4),f2(a4),a3)),
% 147.26/147.44 inference(scs_inference,[],[1913,2051,16,269,1965,29,33,26,352,391])).
% 147.26/147.44 cnf(2116,plain,
% 147.26/147.44 (~P3(f1(f2(x21161)),x21161,x21162)+P2(f1(f2(x21161)),x21162)),
% 147.26/147.44 inference(scs_inference,[],[1943,50,31])).
% 147.26/147.44 cnf(2149,plain,
% 147.26/147.44 (~P3(f1(f2(x21491)),x21491,x21492)+P3(f1(f2(x21491)),x21492,f5(f1(f2(x21491)),x21492))),
% 147.26/147.44 inference(scs_inference,[],[2116,26])).
% 147.26/147.44 cnf(2150,plain,
% 147.26/147.44 (P2(f2(f1(a3)),a4)),
% 147.26/147.44 inference(scs_inference,[],[1947,85,12])).
% 147.26/147.44 cnf(2163,plain,
% 147.26/147.44 (P2(f2(f1(a3)),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[1947,392,12])).
% 147.26/147.44 cnf(2328,plain,
% 147.26/147.44 (P3(x23281,f2(f1(x23281)),x23281)),
% 147.26/147.44 inference(rename_variables,[],[1968])).
% 147.26/147.44 cnf(2332,plain,
% 147.26/147.44 (P2(f5(x23321,f1(x23321)),f2(f1(a4)))+~P3(f1(a3),a4,x23321)),
% 147.26/147.44 inference(scs_inference,[],[1968,2328,265,85,30,28,12])).
% 147.26/147.44 cnf(2357,plain,
% 147.26/147.44 (~P3(f1(f2(x23571)),x23571,x23572)+P2(x23572,f2(f1(x23571)))),
% 147.26/147.44 inference(scs_inference,[],[1968,50,30])).
% 147.26/147.44 cnf(2416,plain,
% 147.26/147.44 (~P3(f2(f1(a3)),f2(a4),x24161)+P2(a3,x24161)),
% 147.26/147.44 inference(scs_inference,[],[1968,373,31])).
% 147.26/147.44 cnf(2469,plain,
% 147.26/147.44 (P2(a3,f5(f2(f1(a3)),f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[2163,2416,26])).
% 147.26/147.44 cnf(2609,plain,
% 147.26/147.44 (~P3(f1(f2(x26091)),x26091,x26092)+P3(x26092,f2(f1(x26091)),f5(x26092,f2(f1(x26091))))),
% 147.26/147.44 inference(scs_inference,[],[2357,26])).
% 147.26/147.44 cnf(2611,plain,
% 147.26/147.44 (~P3(f1(f1(x26111)),f1(x26111),x26112)+P2(x26112,f2(f1(x26111)))),
% 147.26/147.44 inference(scs_inference,[],[1971,98,30])).
% 147.26/147.44 cnf(2614,plain,
% 147.26/147.44 (P2(f5(x26141,f1(x26141)),f2(f1(x26142)))+~P3(f1(f1(x26142)),f1(x26142),x26141)),
% 147.26/147.44 inference(scs_inference,[],[1971,265,98,30,12])).
% 147.26/147.44 cnf(2713,plain,
% 147.26/147.44 (~P3(f2(f2(a4)),f2(f2(a4)),x27131)+~P3(x27131,a4,f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[2032,277,33])).
% 147.26/147.44 cnf(2773,plain,
% 147.26/147.44 (~P3(f2(a4),f2(a4),x27731)+~P3(x27731,f1(f2(a4)),a3)),
% 147.26/147.44 inference(scs_inference,[],[2072,19,33])).
% 147.26/147.44 cnf(2891,plain,
% 147.26/147.44 (P3(f2(x28911),x28911,x28911)),
% 147.26/147.44 inference(rename_variables,[],[20])).
% 147.26/147.44 cnf(2896,plain,
% 147.26/147.44 (P2(x28961,f5(a4,f1(a4)))+~P3(f2(f1(a3)),f2(a4),x28961)),
% 147.26/147.44 inference(scs_inference,[],[20,2891,265,2150,30,27,13])).
% 147.26/147.44 cnf(3075,plain,
% 147.26/147.44 (~P3(f2(f5(a3,a4)),f5(a3,a4),a4)),
% 147.26/147.44 inference(scs_inference,[],[227,20,29])).
% 147.26/147.44 cnf(3081,plain,
% 147.26/147.44 (~P3(f1(f1(x30811)),f1(x30811),x30812)+P3(x30812,f2(f1(x30811)),f5(x30812,f2(f1(x30811))))),
% 147.26/147.44 inference(scs_inference,[],[2611,26])).
% 147.26/147.44 cnf(3095,plain,
% 147.26/147.44 (~P3(f2(f5(a3,a4)),f2(f5(a3,a4)),x30951)+~P3(x30951,f5(a3,a4),a4)),
% 147.26/147.44 inference(scs_inference,[],[3075,20,33])).
% 147.26/147.44 cnf(3178,plain,
% 147.26/147.44 (P3(f1(x31781),f1(f1(x31781)),f1(f1(x31781)))),
% 147.26/147.44 inference(scs_inference,[],[1969,14,488,23])).
% 147.26/147.44 cnf(3179,plain,
% 147.26/147.44 (~E(f1(f1(a4)),f1(f5(a3,a4)))),
% 147.26/147.44 inference(scs_inference,[],[2064,3178,11])).
% 147.26/147.44 cnf(3181,plain,
% 147.26/147.44 (~E(f1(a4),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[2064,3178,11,4])).
% 147.26/147.44 cnf(3263,plain,
% 147.26/147.44 (P3(f2(x32631),x32631,f5(f2(x32631),x32631))),
% 147.26/147.44 inference(scs_inference,[],[1969,1179,26])).
% 147.26/147.44 cnf(3264,plain,
% 147.26/147.44 (E(x32641,f5(f2(x32641),x32641))),
% 147.26/147.44 inference(scs_inference,[],[20,3263,29])).
% 147.26/147.44 cnf(3265,plain,
% 147.26/147.44 (P3(f2(x32651),x32651,f5(f2(x32651),x32651))),
% 147.26/147.44 inference(rename_variables,[],[3263])).
% 147.26/147.44 cnf(3269,plain,
% 147.26/147.44 (P3(f2(x32691),x32691,f5(f2(x32691),x32691))),
% 147.26/147.44 inference(rename_variables,[],[3263])).
% 147.26/147.44 cnf(3270,plain,
% 147.26/147.44 (P3(f2(x32701),f5(x32701,f1(x32701)),f5(f2(x32701),x32701))),
% 147.26/147.44 inference(scs_inference,[],[3075,265,20,3263,3265,3269,14,29,8,11,10])).
% 147.26/147.44 cnf(3271,plain,
% 147.26/147.44 (P3(f2(x32711),x32711,f5(f2(x32711),x32711))),
% 147.26/147.44 inference(rename_variables,[],[3263])).
% 147.26/147.44 cnf(3272,plain,
% 147.26/147.44 (~P3(f5(f2(a4),a4),f1(a4),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[3075,2051,265,20,264,3263,3265,3269,3271,14,29,8,11,10,33])).
% 147.26/147.44 cnf(3279,plain,
% 147.26/147.44 (P3(x32791,f5(f2(f1(x32791)),f1(x32791)),x32791)),
% 147.26/147.44 inference(scs_inference,[],[3075,2051,265,20,264,3263,3265,3269,3271,14,29,8,11,10,33,88,101,2,69])).
% 147.26/147.44 cnf(3292,plain,
% 147.26/147.44 (E(x32921,f5(f2(x32921),x32921))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3294,plain,
% 147.26/147.44 (P2(f1(a3),f5(f2(a4),a4))),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,71,68,130])).
% 147.26/147.44 cnf(3295,plain,
% 147.26/147.44 (E(x32951,f5(f2(x32951),x32951))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3298,plain,
% 147.26/147.44 (E(x32981,f5(f2(x32981),x32981))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3300,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),a4)),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,71,68,130,160,117,151])).
% 147.26/147.44 cnf(3301,plain,
% 147.26/147.44 (E(x33011,f5(f2(x33011),x33011))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3302,plain,
% 147.26/147.44 (P2(a3,f5(f2(a4),a4))),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,71,68,130,160,117,151,129])).
% 147.26/147.44 cnf(3303,plain,
% 147.26/147.44 (E(x33031,f5(f2(x33031),x33031))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3304,plain,
% 147.26/147.44 (P3(f2(x33041),f5(f2(x33041),x33041),x33041)),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,3303,71,68,130,160,117,151,129,72])).
% 147.26/147.44 cnf(3306,plain,
% 147.26/147.44 (P3(f5(f2(f2(x33061)),f2(x33061)),x33061,x33061)),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,3303,71,68,130,160,117,151,129,72,53])).
% 147.26/147.44 cnf(3307,plain,
% 147.26/147.44 (E(x33071,f5(f2(x33071),x33071))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3308,plain,
% 147.26/147.44 (P3(x33081,f1(x33081),f5(f2(x33081),x33081))),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,3303,3307,71,68,130,160,117,151,129,72,53,70])).
% 147.26/147.44 cnf(3309,plain,
% 147.26/147.44 (P3(f5(f2(x33091),x33091),f1(x33091),x33091)),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,3303,3307,71,68,130,160,117,151,129,72,53,70,41])).
% 147.26/147.44 cnf(3310,plain,
% 147.26/147.44 (P2(f5(f2(x33101),x33101),f1(x33101))),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,3303,3307,71,68,130,160,117,151,129,72,53,70,41,118])).
% 147.26/147.44 cnf(3311,plain,
% 147.26/147.44 (E(f5(f2(x33111),x33111),x33111)),
% 147.26/147.44 inference(scs_inference,[],[3264,3292,3295,3298,3301,3303,3307,71,68,130,160,117,151,129,72,53,70,41,118,2])).
% 147.26/147.44 cnf(3312,plain,
% 147.26/147.44 (P3(f5(x33121,f1(x33121)),f1(x33121),f5(f2(x33121),x33121))),
% 147.26/147.44 inference(scs_inference,[],[265,3264,3292,3295,3298,3301,3303,3307,71,68,130,160,117,151,129,72,53,70,41,118,2,9])).
% 147.26/147.44 cnf(3313,plain,
% 147.26/147.44 (P3(x33131,f2(f1(x33131)),f5(f2(x33131),x33131))),
% 147.26/147.44 inference(scs_inference,[],[265,1947,3264,3292,3295,3298,3301,3303,3307,71,68,130,160,117,151,129,72,53,70,41,118,2,9,10])).
% 147.26/147.44 cnf(3317,plain,
% 147.26/147.44 (E(x33171,f5(x33171,f1(x33171)))),
% 147.26/147.44 inference(rename_variables,[],[265])).
% 147.26/147.44 cnf(3320,plain,
% 147.26/147.44 (P3(f2(a4),f5(f2(a4),a4),f5(f2(a4),a4))),
% 147.26/147.44 inference(scs_inference,[],[2051,265,3317,1947,3264,3292,3295,3298,3301,3303,3307,20,3270,71,68,130,160,117,151,129,72,53,70,41,118,2,9,10,11,13,12,33])).
% 147.26/147.44 cnf(3323,plain,
% 147.26/147.44 (~E(f2(a4),a3)),
% 147.26/147.44 inference(scs_inference,[],[2051,265,3317,1947,3264,3292,3295,3298,3301,3303,3307,20,3270,71,68,130,160,117,151,129,72,53,70,41,118,2,9,10,11,13,12,33,6])).
% 147.26/147.44 cnf(3324,plain,
% 147.26/147.44 (E(f5(a4,f1(a4)),f5(f2(a4),a4))),
% 147.26/147.44 inference(scs_inference,[],[2051,265,3317,1947,285,3264,3292,3295,3298,3301,3303,3307,20,3270,71,68,130,160,117,151,129,72,53,70,41,118,2,9,10,11,13,12,33,6,3])).
% 147.26/147.44 cnf(3343,plain,
% 147.26/147.44 (E(f5(f2(a4),a4),f5(a4,f1(a4)))),
% 147.26/147.44 inference(scs_inference,[],[3324,2])).
% 147.26/147.44 cnf(3344,plain,
% 147.26/147.44 (~E(f5(a3,a4),f5(f2(a4),a4))),
% 147.26/147.44 inference(scs_inference,[],[3324,296,2,3])).
% 147.26/147.44 cnf(3345,plain,
% 147.26/147.44 (~P3(f2(a4),f5(f2(a4),a4),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[3324,296,3320,2,3,29])).
% 147.26/147.44 cnf(3347,plain,
% 147.26/147.44 (~E(a3,f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[3324,296,3320,2,3,29,6])).
% 147.26/147.44 cnf(3421,plain,
% 147.26/147.44 (P3(f1(x34211),f1(x34211),f5(f2(f1(x34211)),f1(x34211)))),
% 147.26/147.44 inference(scs_inference,[],[1910,3263,9])).
% 147.26/147.44 cnf(3434,plain,
% 147.26/147.44 (P3(f5(f2(f1(x34341)),f1(x34341)),f1(x34341),f1(x34341))),
% 147.26/147.44 inference(scs_inference,[],[1910,3304,3421,9,32])).
% 147.26/147.44 cnf(3457,plain,
% 147.26/147.44 (P3(f5(f2(x34571),x34571),f2(f1(x34571)),x34571)),
% 147.26/147.44 inference(scs_inference,[],[1947,3309,10])).
% 147.26/147.44 cnf(3463,plain,
% 147.26/147.44 (~P3(f5(f2(a3),a3),f2(f1(a3)),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[1947,3294,3309,3310,3323,10,13,12,29])).
% 147.26/147.44 cnf(3471,plain,
% 147.26/147.44 (~P3(a3,f1(a3),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[3463,2011,3309,33])).
% 147.26/147.44 cnf(3476,plain,
% 147.26/147.44 (~P3(a3,f1(f1(a3)),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[3463,1965,3309,33])).
% 147.26/147.44 cnf(3493,plain,
% 147.26/147.44 (P3(f5(f2(x34931),x34931),f1(f1(x34931)),x34931)),
% 147.26/147.44 inference(scs_inference,[],[1965,1969,3312,32])).
% 147.26/147.44 cnf(3752,plain,
% 147.26/147.44 (~P3(f2(f5(a3,a4)),f2(f5(a3,a4)),x37521)+~P3(x37521,f5(f2(f5(a3,a4)),f5(a3,a4)),a4)),
% 147.26/147.44 inference(scs_inference,[],[3075,3304,33])).
% 147.26/147.44 cnf(3798,plain,
% 147.26/147.44 (P2(f5(x37981,f1(x37981)),f5(f2(f1(a4)),f1(f2(f1(a4)))))+~P3(f1(a3),a4,x37981)),
% 147.26/147.44 inference(scs_inference,[],[265,2332,13])).
% 147.26/147.44 cnf(3811,plain,
% 147.26/147.44 (~P3(f2(f1(a3)),f2(a4),x38111)+P3(x38111,f5(a4,f1(a4)),f5(x38111,f5(a4,f1(a4))))),
% 147.26/147.44 inference(scs_inference,[],[2896,26])).
% 147.26/147.44 cnf(3846,plain,
% 147.26/147.44 (~P3(f5(a3,a4),f1(f5(a3,a4)),f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[3181,19,3311,3,29])).
% 147.26/147.44 cnf(3850,plain,
% 147.26/147.44 (~P3(f2(f5(a3,a4)),f5(a3,a4),f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[3181,20,29])).
% 147.26/147.44 cnf(3853,plain,
% 147.26/147.44 (~E(f5(a3,a4),f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[3181,3846,19,20,29,11])).
% 147.26/147.44 cnf(3858,plain,
% 147.26/147.44 (~P3(f2(f5(a3,a4)),f2(f5(a3,a4)),x38581)+~P3(x38581,f5(a3,a4),f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[3850,20,3263,11,33])).
% 147.26/147.44 cnf(3879,plain,
% 147.26/147.44 (P3(f5(f2(x38791),x38791),f1(x38791),f5(x38791,f1(x38791)))),
% 147.26/147.44 inference(scs_inference,[],[3264,264,9])).
% 147.26/147.44 cnf(3899,plain,
% 147.26/147.44 (P3(f5(f2(x38991),x38991),f1(x38991),f5(f2(x38991),x38991))),
% 147.26/147.44 inference(scs_inference,[],[3264,3308,9])).
% 147.26/147.44 cnf(3904,plain,
% 147.26/147.44 (E(x39041,f5(f2(x39041),x39041))),
% 147.26/147.44 inference(rename_variables,[],[3264])).
% 147.26/147.44 cnf(3905,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[3264,3904,373,727,269,3308,9,10,13,12])).
% 147.26/147.44 cnf(3907,plain,
% 147.26/147.44 (~P3(f5(f2(a3),a3),f2(a4),x39071)+P2(x39071,f1(f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[3264,3904,19,373,727,269,3308,9,10,13,12,30])).
% 147.26/147.44 cnf(3962,plain,
% 147.26/147.44 (P2(f5(f2(x39621),x39621),f1(f1(x39621)))),
% 147.26/147.44 inference(scs_inference,[],[3264,308,12])).
% 147.26/147.44 cnf(3964,plain,
% 147.26/147.44 (~P3(f5(f2(a3),a3),f2(a4),x39641)+P3(x39641,f1(f2(a4)),f5(x39641,f1(f2(a4))))),
% 147.26/147.44 inference(scs_inference,[],[3907,26])).
% 147.26/147.44 cnf(4010,plain,
% 147.26/147.44 (~P3(f2(x40101),f2(f2(x40101)),x40102)+P3(f5(x40102,f1(x40102)),f2(x40101),f5(f5(x40102,f1(x40102)),f2(x40101)))),
% 147.26/147.44 inference(scs_inference,[],[515,26])).
% 147.26/147.44 cnf(4021,plain,
% 147.26/147.44 (~P3(f1(a3),a4,x40211)+P2(x40211,f5(f2(f1(a4)),f1(a4)))),
% 147.26/147.44 inference(scs_inference,[],[3279,85,30])).
% 147.26/147.44 cnf(4096,plain,
% 147.26/147.44 (P3(f2(x40961),f5(f2(x40961),x40961),x40961)),
% 147.26/147.44 inference(rename_variables,[],[3304])).
% 147.26/147.44 cnf(4098,plain,
% 147.26/147.44 (P2(f5(f2(x40981),x40981),f5(f2(a4),a4))+~P3(f1(a3),f2(a4),x40981)),
% 147.26/147.44 inference(scs_inference,[],[3304,4096,85,30,28])).
% 147.26/147.44 cnf(4100,plain,
% 147.26/147.44 (P2(f5(x41001,f1(x41001)),f5(f2(a4),a4))+~P3(f1(a3),f2(a4),x41001)),
% 147.26/147.44 inference(scs_inference,[],[3304,4096,265,85,30,28,12])).
% 147.26/147.44 cnf(4119,plain,
% 147.26/147.44 (~P3(f1(f1(a3)),f2(a4),x41191)+P2(x41191,f5(f2(a4),a4))),
% 147.26/147.44 inference(scs_inference,[],[3304,114,30])).
% 147.26/147.44 cnf(4145,plain,
% 147.26/147.44 (P3(f2(x41451),f5(f2(x41451),x41451),x41451)),
% 147.26/147.44 inference(rename_variables,[],[3304])).
% 147.26/147.44 cnf(4147,plain,
% 147.26/147.44 (P2(f2(a3),f2(x41471))+~P3(f5(f2(a3),a3),f2(a4),x41471)),
% 147.26/147.44 inference(scs_inference,[],[3304,4145,373,31,27])).
% 147.26/147.44 cnf(4149,plain,
% 147.26/147.44 (P2(f2(a3),f5(x41491,f1(x41491)))+~P3(f5(f2(a3),a3),f2(a4),x41491)),
% 147.26/147.44 inference(scs_inference,[],[3304,4145,265,373,31,27,13])).
% 147.26/147.44 cnf(4303,plain,
% 147.26/147.44 (P3(f2(x43031),f5(f2(x43031),x43031),x43031)),
% 147.26/147.44 inference(rename_variables,[],[3304])).
% 147.26/147.44 cnf(4305,plain,
% 147.26/147.44 (P2(f5(f2(x43051),x43051),f5(f2(a4),a4))+~P3(f5(f2(a3),a3),f2(a4),x43051)),
% 147.26/147.44 inference(scs_inference,[],[3304,4303,3300,30,28])).
% 147.26/147.44 cnf(4307,plain,
% 147.26/147.44 (P2(f5(x43071,f1(x43071)),f5(f2(a4),a4))+~P3(f5(f2(a3),a3),f2(a4),x43071)),
% 147.26/147.44 inference(scs_inference,[],[3304,4303,265,3300,30,28,12])).
% 147.26/147.44 cnf(4342,plain,
% 147.26/147.44 (~P3(a3,a4,x43421)+P2(f5(f2(f2(a3)),f2(a3)),x43421)),
% 147.26/147.44 inference(scs_inference,[],[3306,16,31])).
% 147.26/147.44 cnf(4348,plain,
% 147.26/147.44 (P2(f5(f2(f2(a3)),f2(a3)),f5(f2(f2(x43481)),f2(x43481)))+~P3(a3,a4,x43481)),
% 147.26/147.44 inference(scs_inference,[],[3306,4342,27])).
% 147.26/147.44 cnf(4349,plain,
% 147.26/147.44 (~P3(a3,f2(a4),x43491)+P2(f5(f2(f2(a3)),f2(a3)),x43491)),
% 147.26/147.44 inference(scs_inference,[],[3306,373,31])).
% 147.26/147.44 cnf(4362,plain,
% 147.26/147.44 (~P3(f1(f1(a3)),f2(a4),x43621)+P3(x43621,f5(f2(a4),a4),f5(x43621,f5(f2(a4),a4)))),
% 147.26/147.44 inference(scs_inference,[],[4119,26])).
% 147.26/147.44 cnf(4390,plain,
% 147.26/147.44 (~P3(f1(a3),a4,x43901)+P2(f5(f2(a3),a3),x43901)),
% 147.26/147.44 inference(scs_inference,[],[3309,16,31])).
% 147.26/147.44 cnf(4391,plain,
% 147.26/147.44 (P3(f5(f2(x43911),x43911),f1(x43911),x43911)),
% 147.26/147.44 inference(rename_variables,[],[3309])).
% 147.26/147.44 cnf(4393,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f5(f2(x43931),x43931))+~P3(f1(a3),a4,x43931)),
% 147.26/147.44 inference(scs_inference,[],[3309,4391,16,31,27])).
% 147.26/147.44 cnf(4395,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f5(x43951,f1(x43951)))+~P3(f1(a3),a4,x43951)),
% 147.26/147.44 inference(scs_inference,[],[3309,4391,265,16,31,27,13])).
% 147.26/147.44 cnf(4402,plain,
% 147.26/147.44 (P3(f5(f2(a3),a3),x44021,f5(f5(f2(a3),a3),x44021))+~P3(f1(a3),a4,x44021)),
% 147.26/147.44 inference(scs_inference,[],[4390,26])).
% 147.26/147.44 cnf(4410,plain,
% 147.26/147.44 (P3(f5(f2(x44101),x44101),f1(x44101),x44101)),
% 147.26/147.44 inference(rename_variables,[],[3309])).
% 147.26/147.44 cnf(4412,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f5(f2(x44121),x44121))+~P3(f1(a3),f2(a4),x44121)),
% 147.26/147.44 inference(scs_inference,[],[3309,4410,373,31,27])).
% 147.26/147.44 cnf(4414,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f5(x44141,f1(x44141)))+~P3(f1(a3),f2(a4),x44141)),
% 147.26/147.44 inference(scs_inference,[],[3309,4410,265,373,31,27,13])).
% 147.26/147.44 cnf(4446,plain,
% 147.26/147.44 (~P3(f1(a3),f2(f2(a4)),x44461)+P2(f5(f2(a3),a3),x44461)),
% 147.26/147.44 inference(scs_inference,[],[3309,430,31])).
% 147.26/147.44 cnf(4447,plain,
% 147.26/147.44 (P3(f5(f2(x44471),x44471),f1(x44471),x44471)),
% 147.26/147.44 inference(rename_variables,[],[3309])).
% 147.26/147.44 cnf(4449,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f5(f2(x44491),x44491))+~P3(f1(a3),f2(f2(a4)),x44491)),
% 147.26/147.44 inference(scs_inference,[],[3309,4447,430,31,27])).
% 147.26/147.44 cnf(4451,plain,
% 147.26/147.44 (P2(f5(f2(a3),a3),f5(x44511,f1(x44511)))+~P3(f1(a3),f2(f2(a4)),x44511)),
% 147.26/147.44 inference(scs_inference,[],[3309,4447,265,430,31,27,13])).
% 147.26/147.44 cnf(4579,plain,
% 147.26/147.44 (P2(f1(f2(a3)),x45791)+~P3(a3,f2(a4),x45791)),
% 147.26/147.44 inference(scs_inference,[],[3312,4349,28])).
% 147.26/147.44 cnf(4589,plain,
% 147.26/147.44 (P3(f1(f2(a3)),x45891,f5(f1(f2(a3)),x45891))+~P3(a3,f2(a4),x45891)),
% 147.26/147.44 inference(scs_inference,[],[4579,26])).
% 147.26/147.44 cnf(4600,plain,
% 147.26/147.44 (~P3(f2(a3),f5(f2(a3),a3),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[3313,3463,3263,32])).
% 147.26/147.44 cnf(4605,plain,
% 147.26/147.44 (~P3(f1(a3),f2(f2(a4)),x46051)+P3(f5(f2(a3),a3),x46051,f5(f5(f2(a3),a3),x46051))),
% 147.26/147.44 inference(scs_inference,[],[4446,26])).
% 147.26/147.44 cnf(4617,plain,
% 147.26/147.44 (~E(f2(a4),f5(a3,f1(a3)))),
% 147.26/147.44 inference(scs_inference,[],[3323,285,3])).
% 147.26/147.44 cnf(4623,plain,
% 147.26/147.44 (~E(f2(a4),f5(f2(a3),a3))),
% 147.26/147.44 inference(scs_inference,[],[3323,3311,3])).
% 147.26/147.44 cnf(4629,plain,
% 147.26/147.44 (~P3(f5(f2(a3),a3),f1(a3),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[4617,3879,29])).
% 147.26/147.44 cnf(4636,plain,
% 147.26/147.44 (~E(f5(f2(a3),a3),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[3323,4629,3899,331,29,11])).
% 147.26/147.44 cnf(4673,plain,
% 147.26/147.44 (P2(f5(f5(a3,f1(a3)),f1(f5(a3,f1(a3)))),f5(x46731,f1(x46731)))+~P3(f1(a3),a4,x46731)),
% 147.26/147.44 inference(scs_inference,[],[265,998,12])).
% 147.26/147.44 cnf(4675,plain,
% 147.26/147.44 (~E(a3,f5(f2(f2(a4)),f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[3347,3311,3])).
% 147.26/147.44 cnf(4718,plain,
% 147.26/147.44 (~P3(f1(a3),a4,x47181)+P2(f5(f2(f1(a3)),f1(a3)),x47181)),
% 147.26/147.44 inference(scs_inference,[],[3434,85,31])).
% 147.26/147.44 cnf(4721,plain,
% 147.26/147.44 (~P3(f1(a3),f2(a4),x47211)+P2(f5(f2(f1(a3)),f1(a3)),x47211)),
% 147.26/147.44 inference(scs_inference,[],[3434,392,31])).
% 147.26/147.44 cnf(4724,plain,
% 147.26/147.44 (P2(f5(f5(f2(f1(a3)),f1(a3)),f1(f5(f2(f1(a3)),f1(a3)))),x47241)+~P3(f1(a3),a4,x47241)),
% 147.26/147.44 inference(scs_inference,[],[265,4718,12])).
% 147.26/147.44 cnf(4844,plain,
% 147.26/147.44 (P3(f5(f2(x48441),x48441),f2(f1(x48441)),x48441)),
% 147.26/147.44 inference(rename_variables,[],[3457])).
% 147.26/147.44 cnf(4846,plain,
% 147.26/147.44 (P2(f2(f1(x48461)),f2(f1(a4)))+~P3(a3,f5(f2(a4),a4),x48461)),
% 147.26/147.44 inference(scs_inference,[],[3457,4844,16,30,28])).
% 147.26/147.44 cnf(4848,plain,
% 147.26/147.44 (P2(f5(x48481,f1(x48481)),f2(f1(a4)))+~P3(a3,f5(f2(a4),a4),x48481)),
% 147.26/147.44 inference(scs_inference,[],[3457,4844,265,16,30,28,12])).
% 147.26/147.44 cnf(4940,plain,
% 147.26/147.44 (P2(f1(f2(f2(a3))),f5(x49401,f1(x49401)))+~P3(a3,f2(f2(a4)),x49401)),
% 147.26/147.44 inference(scs_inference,[],[19,1338,28])).
% 147.26/147.44 cnf(4955,plain,
% 147.26/147.44 (~P3(f1(f1(a3)),f2(a4),x49551)+P2(f5(f2(a3),a3),x49551)),
% 147.26/147.44 inference(scs_inference,[],[3493,373,31])).
% 147.26/147.44 cnf(5003,plain,
% 147.26/147.44 (~P3(f1(f1(a3)),f2(a4),x50031)+P3(f5(f2(a3),a3),x50031,f5(f5(f2(a3),a3),x50031))),
% 147.26/147.44 inference(scs_inference,[],[4955,26])).
% 147.26/147.44 cnf(5037,plain,
% 147.26/147.44 (P3(f5(f2(x50371),x50371),f1(f1(x50371)),x50371)),
% 147.26/147.44 inference(rename_variables,[],[3493])).
% 147.26/147.44 cnf(5039,plain,
% 147.26/147.44 (P2(f1(f1(x50391)),f1(f1(a4)))+~P3(a3,f5(f2(a4),a4),x50391)),
% 147.26/147.44 inference(scs_inference,[],[3493,5037,16,30,28])).
% 147.26/147.44 cnf(5041,plain,
% 147.26/147.44 (P2(f5(x50411,f1(x50411)),f1(f1(a4)))+~P3(a3,f5(f2(a4),a4),x50411)),
% 147.26/147.44 inference(scs_inference,[],[3493,5037,265,16,30,28,12])).
% 147.26/147.44 cnf(5144,plain,
% 147.26/147.44 (P3(f1(x51441),f1(x51441),f5(f1(x51441),f1(x51441)))),
% 147.26/147.44 inference(scs_inference,[],[2005,1870])).
% 147.26/147.44 cnf(5146,plain,
% 147.26/147.44 (P3(f2(x51461),f2(x51461),f5(f2(x51461),f2(x51461)))),
% 147.26/147.44 inference(scs_inference,[],[2005,354,1870,26])).
% 147.26/147.44 cnf(5149,plain,
% 147.26/147.44 (P3(f5(f2(a3),a3),f2(a4),f5(f2(a3),a3))),
% 147.26/147.44 inference(scs_inference,[],[4675,3905,2005,15,354,1870,26,2,24])).
% 147.26/147.44 cnf(5152,plain,
% 147.26/147.44 (~P3(f5(f2(a3),a3),f2(a4),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[4636,4675,3905,2005,15,354,1870,26,2,24,29])).
% 147.26/147.44 cnf(5156,plain,
% 147.26/147.44 (P2(x51561,f5(f1(x51561),f1(x51561)))),
% 147.26/147.44 inference(scs_inference,[],[3471,4636,4675,3905,3311,2005,15,354,1870,26,2,24,29,11,155])).
% 147.26/147.44 cnf(5158,plain,
% 147.26/147.44 (P2(f5(f2(x51581),f2(x51581)),x51581)),
% 147.26/147.44 inference(scs_inference,[],[3471,4636,4675,3905,3311,2005,15,354,1870,26,2,24,29,11,155,382])).
% 147.26/147.44 cnf(5170,plain,
% 147.26/147.44 (~P3(f5(f2(a4),f2(a4)),a4,f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[3471,4636,4675,3905,3311,2005,15,354,1870,26,2,24,29,11,155,382,106,414,642,730,1004,2067])).
% 147.26/147.44 cnf(5173,plain,
% 147.26/147.44 (P2(f2(a4),f1(f1(a3)))),
% 147.26/147.44 inference(scs_inference,[],[3471,4636,4675,3962,3905,3311,2005,15,354,1870,26,2,24,29,11,155,382,106,414,642,730,1004,2067,53,28])).
% 147.26/147.44 cnf(5185,plain,
% 147.26/147.44 (P3(f1(a3),f2(a4),f5(f1(a3),f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[392,26])).
% 147.26/147.44 cnf(5187,plain,
% 147.26/147.44 (~P3(f1(a4),f2(f1(a4)),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[3181,2005,392,26,29])).
% 147.26/147.44 cnf(5201,plain,
% 147.26/147.44 (P3(a3,f2(a4),f5(a3,f2(a4)))),
% 147.26/147.44 inference(scs_inference,[],[373,26])).
% 147.26/147.44 cnf(5203,plain,
% 147.26/147.44 (P2(f5(f2(x52031),f2(x52031)),f2(x52031))),
% 147.26/147.44 inference(scs_inference,[],[5158,271,373,26,27])).
% 147.26/147.44 cnf(5206,plain,
% 147.26/147.44 (~P3(a4,f5(f1(a4),f1(a4)),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[3272,5158,5144,3308,271,373,26,27,32])).
% 147.26/147.44 cnf(5207,plain,
% 147.26/147.44 (P3(f1(x52071),f1(x52071),f5(f1(x52071),f1(x52071)))),
% 147.26/147.44 inference(rename_variables,[],[5144])).
% 147.26/147.44 cnf(5216,plain,
% 147.26/147.44 (P2(f5(a3,f2(a4)),a4)),
% 147.26/147.44 inference(scs_inference,[],[3272,5158,5185,5144,5207,5146,3308,894,271,373,26,27,32,30,31,395])).
% 147.26/147.44 cnf(5221,plain,
% 147.26/147.44 (P3(f1(a3),a4,f5(f1(a3),a4))),
% 147.26/147.44 inference(scs_inference,[],[85,26])).
% 147.26/147.44 cnf(5223,plain,
% 147.26/147.44 (P3(f2(a4),f1(f1(a3)),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[5173,14,85,26,24])).
% 147.26/147.44 cnf(5226,plain,
% 147.26/147.44 (~P3(f5(f1(a4),f1(a4)),f1(a4),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[5187,5173,5144,2011,14,85,26,24,33])).
% 147.26/147.44 cnf(5227,plain,
% 147.26/147.44 (P3(f1(x52271),f1(x52271),f5(f1(x52271),f1(x52271)))),
% 147.26/147.44 inference(rename_variables,[],[5144])).
% 147.26/147.44 cnf(5228,plain,
% 147.26/147.44 (P3(f1(x52281),f1(x52281),f2(f1(x52281)))),
% 147.26/147.44 inference(rename_variables,[],[2011])).
% 147.26/147.44 cnf(5230,plain,
% 147.26/147.44 (P2(f5(f1(a3),a4),f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[5187,5173,5144,3308,2011,3294,14,85,26,24,33,30])).
% 147.26/147.44 cnf(5233,plain,
% 147.26/147.44 (P2(a3,f5(f1(a3),a4))),
% 147.26/147.44 inference(scs_inference,[],[5187,5173,5144,3308,2011,3294,14,85,26,24,33,30,244])).
% 147.26/147.44 cnf(5237,plain,
% 147.26/147.44 (P3(f5(f1(x52371),f1(x52371)),f1(x52371),f1(x52371))),
% 147.26/147.44 inference(scs_inference,[],[5187,5152,5173,5144,5227,3308,2011,5228,2005,3294,14,3264,85,26,24,33,30,244,9,32])).
% 147.26/147.44 cnf(5241,plain,
% 147.26/147.44 (P2(f5(f1(x52411),f1(x52411)),f1(x52411))),
% 147.26/147.44 inference(scs_inference,[],[5187,5152,5173,5144,5227,3308,2011,5228,2005,3294,14,3264,85,26,24,33,30,244,9,32,25])).
% 147.26/147.44 cnf(5247,plain,
% 147.26/147.44 (P3(a3,a4,f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[16,26])).
% 147.26/147.44 cnf(5249,plain,
% 147.26/147.44 (P3(f2(x52491),f2(f2(x52491)),f2(x52491))),
% 147.26/147.44 inference(scs_inference,[],[15,445,16,26,24])).
% 147.26/147.44 cnf(5252,plain,
% 147.26/147.44 (~P3(a3,a4,f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[3853,15,445,16,26,24,29])).
% 147.26/147.44 cnf(5259,plain,
% 147.26/147.44 (~P3(f5(f2(a3),a3),a4,f1(a4))),
% 147.26/147.44 inference(scs_inference,[],[3476,5203,5223,3853,3311,15,445,1943,16,26,24,29,32,23,9])).
% 147.26/147.44 cnf(5272,plain,
% 147.26/147.44 (E(f5(x52721,f1(x52721)),x52721)),
% 147.26/147.44 inference(rename_variables,[],[285])).
% 147.26/147.44 cnf(5283,plain,
% 147.26/147.44 (~P3(a3,f2(f2(a4)),f2(a4))),
% 147.26/147.44 inference(scs_inference,[],[5252,5247,5241,3344,2020,1910,14,85,277,285,5272,9,29,11,10,22,32])).
% 147.26/147.44 cnf(5286,plain,
% 147.26/147.44 (P3(f1(x52861),f5(f1(x52861),f1(x52861)),f1(x52861))),
% 147.26/147.44 inference(scs_inference,[],[5252,5247,5241,3344,5237,5144,2020,1910,14,85,277,285,5272,9,29,11,10,22,32,33])).
% 147.26/147.44 cnf(5289,plain,
% 147.26/147.44 (P2(f1(x52891),f5(f1(x52891),f1(x52891)))),
% 147.26/147.44 inference(scs_inference,[],[5252,5247,5241,3344,5237,5144,2020,1910,14,85,277,285,5272,9,29,11,10,22,32,33,25])).
% 147.26/147.44 cnf(5291,plain,
% 147.26/147.44 (P3(x52911,f5(f1(x52911),f1(x52911)),x52911)),
% 147.26/147.44 inference(scs_inference,[],[5252,5247,5241,3344,5237,5144,2020,1910,14,85,277,285,5272,9,29,11,10,22,32,33,25,119])).
% 147.26/147.44 cnf(5293,plain,
% 147.26/147.44 (P3(f1(a3),f2(f2(a4)),f1(a3))),
% 147.26/147.44 inference(scs_inference,[],[15,471,24])).
% 147.26/147.44 cnf(5299,plain,
% 147.26/147.44 (E(f5(f2(x52991),x52991),x52991)),
% 147.26/147.44 inference(rename_variables,[],[3311])).
% 147.26/147.44 cnf(5302,plain,
% 147.26/147.44 (~P3(f1(a4),f5(f1(a4),f1(a4)),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[5286,5226,34,5247,5237,3311,5299,15,471,24,29,9,10,33])).
% 147.26/147.44 cnf(5306,plain,
% 147.26/147.44 (P3(a3,f2(f2(a4)),a3)),
% 147.26/147.44 inference(scs_inference,[],[5286,5226,34,5247,5237,3311,5299,15,471,24,29,9,10,33,119])).
% 147.26/147.44 cnf(5310,plain,
% 147.26/147.44 (~P3(f1(a4),f1(a4),f5(a3,a4))),
% 147.26/147.44 inference(scs_inference,[],[5286,5230,5226,5233,34,5247,5237,5144,3311,5299,15,471,1943,24,29,9,10,33,119,22,32])).
% 147.26/147.44 cnf(5318,plain,
% 147.26/147.45 (~P3(f2(f1(a4)),f1(a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5310,1910,9])).
% 147.26/147.45 cnf(5345,plain,
% 147.26/147.45 (P2(f5(a3,f2(a4)),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5216,271,27])).
% 147.26/147.45 cnf(5389,plain,
% 147.26/147.45 (P2(f2(f2(a3)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5247,277,16,31])).
% 147.26/147.45 cnf(5401,plain,
% 147.26/147.45 (P3(f2(f2(a3)),f5(a3,a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5389,15,23])).
% 147.26/147.45 cnf(5402,plain,
% 147.26/147.45 (P1(f2(x54021))),
% 147.26/147.45 inference(rename_variables,[],[15])).
% 147.26/147.45 cnf(5404,plain,
% 147.26/147.45 (P2(f2(a3),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5389,445,15,5402,23,22])).
% 147.26/147.45 cnf(5408,plain,
% 147.26/147.45 (P3(f2(a3),f5(a3,a4),f5(f2(a3),f5(a3,a4)))),
% 147.26/147.45 inference(scs_inference,[],[5389,445,15,5402,23,22,26])).
% 147.26/147.45 cnf(5410,plain,
% 147.26/147.45 (~P3(f2(f2(a3)),f5(a3,a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5389,3853,445,15,5402,23,22,26,29])).
% 147.26/147.45 cnf(5417,plain,
% 147.26/147.45 (P3(f2(a3),f5(a3,a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5404,15,23])).
% 147.26/147.45 cnf(5418,plain,
% 147.26/147.45 (P1(f2(x54181))),
% 147.26/147.45 inference(rename_variables,[],[15])).
% 147.26/147.45 cnf(5420,plain,
% 147.26/147.45 (~P3(f2(f2(a3)),f5(a3,a4),a4)),
% 147.26/147.45 inference(scs_inference,[],[5404,5401,34,15,23,29])).
% 147.26/147.45 cnf(5422,plain,
% 147.26/147.45 (P2(f1(f2(a3)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5404,5401,34,15,3309,23,29,28])).
% 147.26/147.45 cnf(5429,plain,
% 147.26/147.45 (P3(f5(f2(a3),f2(a3)),f5(a3,a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5404,5401,5203,34,5146,15,5418,3309,23,29,28,22,32])).
% 147.26/147.45 cnf(5432,plain,
% 147.26/147.45 (P2(f2(a3),f2(f5(a3,a4)))),
% 147.26/147.45 inference(scs_inference,[],[5404,5401,5203,34,5146,15,5418,271,3309,23,29,28,22,32,27])).
% 147.26/147.45 cnf(5437,plain,
% 147.26/147.45 (P2(f5(a3,a4),f5(f1(a4),f1(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5404,5206,5401,5203,34,5291,5146,5247,15,5418,271,3309,16,23,29,28,22,32,27,33,30])).
% 147.26/147.45 cnf(5443,plain,
% 147.26/147.45 (P3(f1(f2(a3)),f5(a3,a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5422,14,23])).
% 147.26/147.45 cnf(5446,plain,
% 147.26/147.45 (P3(f2(a3),f2(f5(a3,a4)),f2(a3))),
% 147.26/147.45 inference(scs_inference,[],[5422,5432,14,15,23,24])).
% 147.26/147.45 cnf(5456,plain,
% 147.26/147.45 (~E(a3,f5(f2(a4),f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5417,5422,5437,5432,5241,5170,3344,5247,14,15,23,24,29,22,32,89])).
% 147.26/147.45 cnf(5462,plain,
% 147.26/147.45 (P3(f2(x54621),f2(x54621),f2(x54621))),
% 147.26/147.45 inference(scs_inference,[],[15,354,24])).
% 147.26/147.45 cnf(5467,plain,
% 147.26/147.45 (P2(f2(a4),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5443,5173,3853,65,14,15,354,24,29,22])).
% 147.26/147.45 cnf(5473,plain,
% 147.26/147.45 (P3(f2(a4),f1(a3),f5(f2(a4),f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[4600,5443,5408,5173,3853,65,14,15,354,24,29,22,33,26])).
% 147.26/147.45 cnf(5475,plain,
% 147.26/147.45 (P3(f2(a4),f1(a3),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5467,15,23])).
% 147.26/147.45 cnf(5478,plain,
% 147.26/147.45 (P3(f2(a4),f1(a3),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5467,14,15,23,24])).
% 147.26/147.45 cnf(5479,plain,
% 147.26/147.45 (P1(f1(x54791))),
% 147.26/147.45 inference(rename_variables,[],[14])).
% 147.26/147.45 cnf(5483,plain,
% 147.26/147.45 (P2(f2(a4),f2(f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5467,4623,1947,14,15,23,24,29,13])).
% 147.26/147.45 cnf(5489,plain,
% 147.26/147.45 (~P3(f2(a4),f1(a3),a3)),
% 147.26/147.45 inference(scs_inference,[],[5467,5289,4623,5283,5293,1947,14,5479,15,23,24,29,13,22,32])).
% 147.26/147.45 cnf(5491,plain,
% 147.26/147.45 (~P3(f2(a4),f2(f1(a3)),a3)),
% 147.26/147.45 inference(scs_inference,[],[5467,5289,4623,5283,5293,1947,14,5479,15,23,24,29,13,22,32,103])).
% 147.26/147.45 cnf(5495,plain,
% 147.26/147.45 (P2(f2(a4),f5(f2(a4),f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5462,5467,5302,5473,5289,4623,5283,5443,5293,1947,14,5479,15,23,24,29,13,22,32,103,33,31])).
% 147.26/147.45 cnf(5498,plain,
% 147.26/147.45 (~P1(f5(f2(a3),a3))),
% 147.26/147.45 inference(scs_inference,[],[5152,3905,23])).
% 147.26/147.45 cnf(5500,plain,
% 147.26/147.45 (P3(f2(a4),f2(f1(a3)),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5483,5152,3905,15,23,24])).
% 147.26/147.45 cnf(5501,plain,
% 147.26/147.45 (P1(f2(x55011))),
% 147.26/147.45 inference(rename_variables,[],[15])).
% 147.26/147.45 cnf(5506,plain,
% 147.26/147.45 (P2(f1(a3),f5(f2(a4),f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5478,5495,5483,5152,4617,3905,14,15,5501,392,23,24,29,8,22])).
% 147.26/147.45 cnf(5509,plain,
% 147.26/147.45 (~P3(f5(a3,f1(a3)),f2(a4),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5475,5489,5478,5495,5483,5152,4617,3905,14,15,5501,392,268,23,24,29,8,22,32])).
% 147.26/147.45 cnf(5512,plain,
% 147.26/147.45 (P3(f2(a4),f5(f1(a3),f1(a3)),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5475,5489,5478,5495,5483,5152,4617,3905,5144,14,15,5501,392,268,23,24,29,8,22,32,33])).
% 147.26/147.45 cnf(5515,plain,
% 147.26/147.45 (~E(f5(f2(a3),a3),f1(x55151))),
% 147.26/147.45 inference(scs_inference,[],[5475,5489,5478,5495,5483,5152,4617,3905,5144,14,15,5501,392,268,23,24,29,8,22,32,33,2])).
% 147.26/147.45 cnf(5516,plain,
% 147.26/147.45 (P2(f2(f2(a4)),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5475,5489,5478,5495,5483,5152,4617,3905,5467,5144,14,15,5501,392,268,20,23,24,29,8,22,32,33,2,31])).
% 147.26/147.45 cnf(5519,plain,
% 147.26/147.45 (~E(a3,f1(x55191))),
% 147.26/147.45 inference(scs_inference,[],[5475,5489,5478,5495,5483,5152,4617,3905,5467,5144,3311,14,15,5501,392,268,20,23,24,29,8,22,32,33,2,31,3])).
% 147.26/147.45 cnf(5521,plain,
% 147.26/147.45 (~E(f2(f1(a3)),a3)),
% 147.26/147.45 inference(scs_inference,[],[5519,54])).
% 147.26/147.45 cnf(5522,plain,
% 147.26/147.45 (~E(a3,f1(x55221))),
% 147.26/147.45 inference(rename_variables,[],[5519])).
% 147.26/147.45 cnf(5524,plain,
% 147.26/147.45 (~E(f1(x55241),a3)),
% 147.26/147.45 inference(scs_inference,[],[5519,5522,54,2])).
% 147.26/147.45 cnf(5525,plain,
% 147.26/147.45 (P3(f2(f2(a4)),f1(a3),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5519,5522,5516,15,54,2,23])).
% 147.26/147.45 cnf(5526,plain,
% 147.26/147.45 (P1(f2(x55261))),
% 147.26/147.45 inference(rename_variables,[],[15])).
% 147.26/147.45 cnf(5528,plain,
% 147.26/147.45 (~P3(a3,f2(f2(a4)),f1(x55281))),
% 147.26/147.45 inference(scs_inference,[],[5519,5522,5516,5306,15,54,2,23,29])).
% 147.26/147.45 cnf(5533,plain,
% 147.26/147.45 (~P3(f2(a3),f5(a3,a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5519,5522,5516,5410,5345,5306,5417,5467,15,5526,20,54,2,23,29,22,33])).
% 147.26/147.45 cnf(5542,plain,
% 147.26/147.45 (~P1(f5(a3,f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5521,5509,376,2,23])).
% 147.26/147.45 cnf(5547,plain,
% 147.26/147.45 (~E(f2(x55471),f5(f2(a3),a3))),
% 147.26/147.45 inference(scs_inference,[],[5524,5525,5521,5498,5509,376,15,2,23,29,8])).
% 147.26/147.45 cnf(5548,plain,
% 147.26/147.45 (~P3(f1(a3),f2(f2(a4)),a3)),
% 147.26/147.45 inference(scs_inference,[],[5524,5525,5528,5521,5498,5509,5462,5293,376,15,2,23,29,8,32])).
% 147.26/147.45 cnf(5554,plain,
% 147.26/147.45 (P2(f5(a3,a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5533,5524,5525,5528,5521,5498,5509,5437,5462,5293,5144,376,1910,15,2,23,29,8,32,11,27])).
% 147.26/147.45 cnf(5560,plain,
% 147.26/147.45 (P3(f5(a3,a4),f1(a4),f5(f5(a3,a4),f1(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5533,5524,5525,5528,5521,5498,5509,5437,5462,5286,5293,5144,376,1910,15,2,23,29,8,32,11,27,33,26])).
% 147.26/147.45 cnf(5562,plain,
% 147.26/147.45 (~E(f5(f2(a3),a3),f2(x55621))),
% 147.26/147.45 inference(scs_inference,[],[5547,2])).
% 147.26/147.45 cnf(5563,plain,
% 147.26/147.45 (P3(f5(a3,a4),f1(a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5554,5547,14,2,24])).
% 147.26/147.45 cnf(5564,plain,
% 147.26/147.45 (P1(f1(x55641))),
% 147.26/147.45 inference(rename_variables,[],[14])).
% 147.26/147.45 cnf(5566,plain,
% 147.26/147.45 (~P3(f2(x55661),f2(x55661),f5(f2(a3),a3))),
% 147.26/147.45 inference(scs_inference,[],[5554,5547,5462,14,2,24,29])).
% 147.26/147.45 cnf(5569,plain,
% 147.26/147.45 (~E(f1(x55691),f5(a3,f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5554,5542,5547,5462,14,5564,2,24,29,8])).
% 147.26/147.45 cnf(5570,plain,
% 147.26/147.45 (P2(f1(f5(a3,a4)),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5554,5542,5547,5462,14,5564,3309,2,24,29,8,28])).
% 147.26/147.45 cnf(5576,plain,
% 147.26/147.45 (P3(f2(a4),f1(a3),f2(f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5554,5542,5547,5548,5512,5462,5306,5237,2011,14,5564,3309,277,2,24,29,8,28,32,33])).
% 147.26/147.45 cnf(5580,plain,
% 147.26/147.45 (P2(f5(a3,a4),f2(f1(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5554,5542,5547,5548,5512,5462,5306,5237,2011,1947,14,5564,3309,277,2,24,29,8,28,32,33,13])).
% 147.26/147.45 cnf(5585,plain,
% 147.26/147.45 (P3(f1(f5(a3,a4)),f1(a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5570,5569,14,2,23])).
% 147.26/147.45 cnf(5588,plain,
% 147.26/147.45 (P3(f5(a3,a4),f2(f1(a4)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5570,5569,5580,14,15,2,23,24])).
% 147.26/147.45 cnf(5589,plain,
% 147.26/147.45 (P1(f2(x55891))),
% 147.26/147.45 inference(rename_variables,[],[15])).
% 147.26/147.45 cnf(5593,plain,
% 147.26/147.45 (~E(f2(x55931),f5(a3,f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5563,5570,5569,5580,5542,3344,14,15,5589,2,23,24,29,8])).
% 147.26/147.45 cnf(5597,plain,
% 147.26/147.45 (~P3(f2(f5(a3,a4)),a3,f2(a3))),
% 147.26/147.45 inference(scs_inference,[],[5563,5570,5566,5569,5580,5446,5206,5542,3344,5286,14,15,5589,3263,2,23,24,29,8,32,33])).
% 147.26/147.45 cnf(5601,plain,
% 147.26/147.45 (~P3(f5(a3,a4),f2(f1(a4)),a4)),
% 147.26/147.45 inference(scs_inference,[],[5563,5570,5566,5569,5580,5446,5206,5542,3344,5286,14,15,5589,3263,2,23,24,29,8,32,33,103])).
% 147.26/147.45 cnf(5603,plain,
% 147.26/147.45 (~E(a3,f2(x56031))),
% 147.26/147.45 inference(scs_inference,[],[5563,5562,5570,5566,5569,5580,5446,5206,5542,3344,5286,3311,14,15,5589,3263,2,23,24,29,8,32,33,103,3])).
% 147.26/147.45 cnf(5608,plain,
% 147.26/147.45 (P2(f5(a3,a4),f1(f1(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5563,5562,5570,5566,5569,5580,5446,5206,5542,5408,3344,5554,5462,5286,5404,3311,14,15,5589,3263,19,2,23,24,29,8,32,33,103,3,31,30])).
% 147.26/147.45 cnf(5611,plain,
% 147.26/147.45 (~E(f2(x56111),a3)),
% 147.26/147.45 inference(scs_inference,[],[5603,2])).
% 147.26/147.45 cnf(5612,plain,
% 147.26/147.45 (P3(f2(f1(a3)),f2(a4),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5603,2163,15,2,23])).
% 147.26/147.45 cnf(5630,plain,
% 147.26/147.45 (~P3(f2(f1(a3)),f2(a4),a3)),
% 147.26/147.45 inference(scs_inference,[],[5611,5612,5593,2,29])).
% 147.26/147.45 cnf(5635,plain,
% 147.26/147.45 (P3(f2(f1(a3)),a4,a4)),
% 147.26/147.45 inference(scs_inference,[],[5611,5588,5612,5593,5601,5443,271,2,29,32,33])).
% 147.26/147.45 cnf(5647,plain,
% 147.26/147.45 (P3(f1(x56471),f1(x56471),f2(f1(x56471)))),
% 147.26/147.45 inference(rename_variables,[],[2011])).
% 147.26/147.45 cnf(5652,plain,
% 147.26/147.45 (P3(f5(a3,a4),f1(f1(a4)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5491,5608,5635,5318,5588,5576,227,2011,5647,14,29,32,33,24])).
% 147.26/147.45 cnf(5657,plain,
% 147.26/147.45 (~P3(f1(a3),f2(a4),f5(f2(a3),a3))),
% 147.26/147.45 inference(scs_inference,[],[5630,5491,5608,5635,5318,5588,5576,227,2011,5647,3311,1947,14,29,32,33,24,9,11])).
% 147.26/147.45 cnf(5661,plain,
% 147.26/147.45 (~P3(f1(f5(a3,a4)),f1(a4),a3)),
% 147.26/147.45 inference(scs_inference,[],[5524,5585,29])).
% 147.26/147.45 cnf(5673,plain,
% 147.26/147.45 (~P3(f5(a3,a4),f1(f1(a4)),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5652,3853,29])).
% 147.26/147.45 cnf(5685,plain,
% 147.26/147.45 (~P3(a3,f2(f2(a4)),f2(x56851))),
% 147.26/147.45 inference(scs_inference,[],[5603,5306,29])).
% 147.26/147.45 cnf(5697,plain,
% 147.26/147.45 (~P3(f2(a3),f2(f5(a3,a4)),a3)),
% 147.26/147.45 inference(scs_inference,[],[5611,5446,29])).
% 147.26/147.45 cnf(5708,plain,
% 147.26/147.45 (P3(f1(a3),f2(a4),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5673,5216,5611,5446,5533,5585,5563,5291,5144,392,15,29,32,33,23,24])).
% 147.26/147.45 cnf(5711,plain,
% 147.26/147.45 (P2(f5(f2(a3),f5(a3,a4)),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5673,5216,5611,5446,5533,5585,5408,5563,5404,5291,5144,392,15,29,32,33,23,24,30])).
% 147.26/147.45 cnf(5713,plain,
% 147.26/147.45 (P3(a3,f2(a4),a3)),
% 147.26/147.45 inference(scs_inference,[],[5673,5216,5611,5446,5533,5585,5408,5563,5404,5291,5144,392,15,29,32,33,23,24,30,119])).
% 147.26/147.45 cnf(5721,plain,
% 147.26/147.45 (~P3(a3,f1(a3),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5708,5713,5657,5456,3308,29,32])).
% 147.26/147.45 cnf(5724,plain,
% 147.26/147.45 (P3(f2(a3),f5(f2(a3),f5(a3,a4)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5708,5713,5657,5456,5429,5408,5146,3308,29,32,33])).
% 147.26/147.45 cnf(5727,plain,
% 147.26/147.45 (P2(f5(f2(a4),f1(a3)),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5708,5713,5657,5456,5473,5429,5408,5146,3308,5467,29,32,33,30])).
% 147.26/147.45 cnf(5733,plain,
% 147.26/147.45 (~P3(f2(x57331),f2(x57331),f5(a3,f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5721,5593,5462,285,9,29])).
% 147.26/147.45 cnf(5742,plain,
% 147.26/147.45 (~P3(a3,f2(a4),f1(x57421))),
% 147.26/147.45 inference(scs_inference,[],[5519,5713,29])).
% 147.26/147.45 cnf(5744,plain,
% 147.26/147.45 (~P3(f2(x57441),f2(x57441),a3)),
% 147.26/147.45 inference(scs_inference,[],[5733,5519,5713,265,29,11])).
% 147.26/147.45 cnf(5756,plain,
% 147.26/147.45 (~P3(f2(x57561),f2(x57561),a3)),
% 147.26/147.45 inference(rename_variables,[],[5744])).
% 147.26/147.45 cnf(5762,plain,
% 147.26/147.45 (~P3(f2(f1(x57621)),f1(x57621),a3)),
% 147.26/147.45 inference(scs_inference,[],[5744,5756,5742,5249,5611,1910,1947,9,29,11,10])).
% 147.26/147.45 cnf(5763,plain,
% 147.26/147.45 (~P3(f2(x57631),f2(x57631),a3)),
% 147.26/147.45 inference(rename_variables,[],[5744])).
% 147.26/147.45 cnf(5770,plain,
% 147.26/147.45 (P3(a3,f5(f2(a4),a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5744,5756,5763,5742,5727,5249,5611,5478,5185,5713,5247,5467,1910,1947,15,3263,9,29,11,10,22,32,33])).
% 147.26/147.45 cnf(5773,plain,
% 147.26/147.45 (P3(f5(f2(a3),f5(a3,a4)),f1(a4),f1(a4))+~P1(f5(f2(a3),f5(a3,a4)))),
% 147.26/147.45 inference(scs_inference,[],[5744,5756,5763,5742,5711,5727,5249,5611,5478,5185,5713,5247,5467,1910,1947,15,3263,9,29,11,10,22,32,33,23])).
% 147.26/147.45 cnf(5775,plain,
% 147.26/147.45 (~E(f1(x57751),f5(f2(a3),f5(a3,a4)))+P3(f5(f2(a3),f5(a3,a4)),f1(a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5744,5756,5763,5742,5711,5727,5249,5611,5478,5185,5713,5247,5467,1910,1947,14,15,3263,9,29,11,10,22,32,33,23,8])).
% 147.26/147.45 cnf(5776,plain,
% 147.26/147.45 (~E(f5(f2(a3),f5(a3,a4)),f1(x57761))+P3(f5(f2(a3),f5(a3,a4)),f1(a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5744,5756,5763,5742,5711,5727,5249,5611,5478,5185,5713,5247,5467,1910,1947,14,15,3263,9,29,11,10,22,32,33,23,8,2])).
% 147.26/147.45 cnf(5788,plain,
% 147.26/147.45 (~P3(f1(x57881),f1(x57881),f5(f2(a3),a3))),
% 147.26/147.45 inference(scs_inference,[],[5762,5770,5420,5226,5401,5652,5585,3181,3308,3311,1947,29,32,33,9,11])).
% 147.26/147.45 cnf(5823,plain,
% 147.26/147.45 (~P3(f2(a3),a3,f1(x58231))),
% 147.26/147.45 inference(scs_inference,[],[5515,3263,29])).
% 147.26/147.45 cnf(5836,plain,
% 147.26/147.45 (~P3(f2(a3),f5(f2(a3),a3),f1(x58361))),
% 147.26/147.45 inference(scs_inference,[],[5823,3311,10])).
% 147.26/147.45 cnf(5853,plain,
% 147.26/147.45 (P3(a3,a4,f5(f5(a3,a4),f1(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5685,5770,5560,5306,3309,277,32,33])).
% 147.26/147.45 cnf(5859,plain,
% 147.26/147.45 (~P3(a3,f2(a4),f2(x58591))),
% 147.26/147.45 inference(scs_inference,[],[5603,5713,29])).
% 147.26/147.45 cnf(5866,plain,
% 147.26/147.45 (P2(f5(f5(a3,a4),f1(a4)),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5597,5661,5853,5603,5446,5585,5713,5286,3302,3308,29,33,32,30])).
% 147.26/147.45 cnf(5873,plain,
% 147.26/147.45 (~P3(a3,f1(a3),f2(x58731))),
% 147.26/147.45 inference(scs_inference,[],[5859,5562,3308,285,9,29])).
% 147.26/147.45 cnf(5874,plain,
% 147.26/147.45 (P3(x58741,f1(x58741),f5(f2(x58741),x58741))),
% 147.26/147.45 inference(rename_variables,[],[3308])).
% 147.26/147.45 cnf(5882,plain,
% 147.26/147.45 (~P3(a3,f2(f1(a3)),f2(x58821))),
% 147.26/147.45 inference(scs_inference,[],[5859,5836,5866,5562,5525,3308,5874,1910,285,9,29,33,23,10])).
% 147.26/147.45 cnf(5894,plain,
% 147.26/147.45 (P3(f2(a4),f5(f1(a3),f1(a3)),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5873,5524,5512,5478,5462,3311,9,29,32])).
% 147.26/147.45 cnf(5897,plain,
% 147.26/147.45 (P3(f2(a4),f1(a3),f5(f1(a3),f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[5873,5524,5512,5478,5462,5237,5144,3311,9,29,32,33])).
% 147.26/147.45 cnf(5937,plain,
% 147.26/147.45 (P3(f1(a3),f5(f2(a4),f2(a4)),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5708,5146,33])).
% 147.26/147.45 cnf(5940,plain,
% 147.26/147.45 (P3(a3,f5(f2(a4),f2(a4)),a3)),
% 147.26/147.45 inference(scs_inference,[],[5708,5146,33,119])).
% 147.26/147.45 cnf(5951,plain,
% 147.26/147.45 (P3(f2(a4),f5(f2(a4),f2(a4)),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5937,5940,5519,5478,29,32])).
% 147.26/147.45 cnf(5953,plain,
% 147.26/147.45 (P3(f5(a3,f2(a4)),f2(a4),f2(a4))+~P1(f5(a3,f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5937,5940,5345,5519,5478,29,32,23])).
% 147.26/147.45 cnf(5955,plain,
% 147.26/147.45 (~E(f2(x59551),f5(a3,f2(a4)))+P3(f5(a3,f2(a4)),f2(a4),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[5937,5940,5345,5519,5478,15,29,32,23,8])).
% 147.26/147.45 cnf(5976,plain,
% 147.26/147.45 (~P3(f2(a3),f5(f5(a3,a4),f1(a4)),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5259,5853,3263,32])).
% 147.26/147.45 cnf(5981,plain,
% 147.26/147.45 (P3(f2(a4),f2(f1(a3)),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[5897,5237,2011,33])).
% 147.26/147.45 cnf(5995,plain,
% 147.26/147.45 (~P3(f5(a3,f2(a4)),f1(a3),f2(x59951))),
% 147.26/147.45 inference(scs_inference,[],[5882,5201,5576,33])).
% 147.26/147.45 cnf(6004,plain,
% 147.26/147.45 (~P3(f5(a3,f2(a4)),f1(a3),f2(x60041))),
% 147.26/147.45 inference(rename_variables,[],[5995])).
% 147.26/147.45 cnf(6007,plain,
% 147.26/147.45 (~P3(f5(a3,f2(a4)),f1(a3),f2(x60071))),
% 147.26/147.45 inference(rename_variables,[],[5995])).
% 147.26/147.45 cnf(6009,plain,
% 147.26/147.45 (~P3(f5(a3,f2(a4)),f1(a3),f1(x60091))),
% 147.26/147.45 inference(scs_inference,[],[5995,6004,6007,5894,5897,5512,1947,32,33,11])).
% 147.26/147.45 cnf(6014,plain,
% 147.26/147.45 (~P1(f5(a3,f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5995,6004,6007,5894,5156,5897,5512,1947,16,32,33,11,22,5953])).
% 147.26/147.45 cnf(6015,plain,
% 147.26/147.45 (~E(f2(x60151),f5(a3,f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5995,6004,6007,5894,5156,5897,5512,1947,16,32,33,11,22,5953,5955])).
% 147.26/147.45 cnf(6018,plain,
% 147.26/147.45 (~E(f2(x60181),f5(a3,f2(a4)))),
% 147.26/147.45 inference(rename_variables,[],[6015])).
% 147.26/147.45 cnf(6026,plain,
% 147.26/147.45 (P3(f2(a4),a4,f5(f1(a3),a4))),
% 147.26/147.45 inference(scs_inference,[],[6009,6015,6018,5981,5635,5897,5221,5576,5286,1910,3,29,32,33])).
% 147.26/147.45 cnf(6056,plain,
% 147.26/147.45 (~P3(a3,f5(f2(a4),f2(a4)),f2(x60561))),
% 147.26/147.45 inference(scs_inference,[],[5940,5603,29])).
% 147.26/147.45 cnf(6060,plain,
% 147.26/147.45 (P3(f2(a4),f2(a4),f5(f1(a3),f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[5995,5981,5940,5603,5473,5612,5201,5185,29,32,33])).
% 147.26/147.45 cnf(6062,plain,
% 147.26/147.45 (~P3(f5(f1(a3),f2(a4)),a4,f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[5995,5981,5940,5603,5473,5612,5201,5185,29,32,33,2067])).
% 147.26/147.45 cnf(6072,plain,
% 147.26/147.45 (~P3(f5(f2(a3),f5(a3,a4)),f1(a4),f1(a4))),
% 147.26/147.45 inference(scs_inference,[],[5976,6015,5443,5770,5408,5560,2011,3345,29,32,33])).
% 147.26/147.45 cnf(6076,plain,
% 147.26/147.45 (~P1(f5(f2(a3),f5(a3,a4)))),
% 147.26/147.45 inference(scs_inference,[],[5976,6060,5495,6015,5443,5770,5473,5408,5560,2011,3345,29,32,33,30,5773])).
% 147.26/147.45 cnf(6078,plain,
% 147.26/147.45 (~E(f5(f2(a3),f5(a3,a4)),f1(x60781))),
% 147.26/147.45 inference(scs_inference,[],[5976,6060,5495,6015,5443,5770,5473,5408,5560,2011,3345,29,32,33,30,5773,5775,5776])).
% 147.26/147.45 cnf(6085,plain,
% 147.26/147.45 (~E(f2(x60851),f5(f2(a3),f5(a3,a4)))),
% 147.26/147.45 inference(scs_inference,[],[6078,6076,5408,15,29,8])).
% 147.26/147.45 cnf(6088,plain,
% 147.26/147.45 (~E(a3,f5(f1(a3),f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[6078,6062,6076,5417,5408,5247,15,29,8,32,89])).
% 147.26/147.45 cnf(6089,plain,
% 147.26/147.45 (~E(f5(f2(a3),f5(a3,a4)),f2(x60891))),
% 147.26/147.45 inference(scs_inference,[],[6078,6062,6076,5417,5408,5247,15,29,8,32,89,2])).
% 147.26/147.45 cnf(6108,plain,
% 147.26/147.45 (~P3(f2(a3),f5(a3,a4),f2(x61081))),
% 147.26/147.45 inference(scs_inference,[],[6089,5408,29])).
% 147.26/147.45 cnf(6113,plain,
% 147.26/147.45 (P3(f1(a3),f5(f1(a3),f2(a4)),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[6089,6072,6060,5708,5408,1943,29,32,33])).
% 147.26/147.45 cnf(6116,plain,
% 147.26/147.45 (P3(a3,f5(f1(a3),f2(a4)),a3)),
% 147.26/147.45 inference(scs_inference,[],[6089,6072,6060,5708,5408,1943,29,32,33,69,119])).
% 147.26/147.45 cnf(6135,plain,
% 147.26/147.45 (~P1(f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6108,6062,6113,6026,6060,5524,1050,5404,29,32,23,24])).
% 147.26/147.45 cnf(6142,plain,
% 147.26/147.45 (~P3(a3,f2(a4),f5(f1(a3),f2(a4)))),
% 147.26/147.45 inference(scs_inference,[],[6088,5713,29])).
% 147.26/147.45 cnf(6144,plain,
% 147.26/147.45 (~E(f1(x61441),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6135,6088,5713,14,29,8])).
% 147.26/147.45 cnf(6145,plain,
% 147.26/147.45 (~E(f5(a3,a4),f1(x61451))),
% 147.26/147.45 inference(scs_inference,[],[6135,6088,5713,14,29,8,2])).
% 147.26/147.45 cnf(6151,plain,
% 147.26/147.45 (~P3(f1(a3),f5(f1(a3),f2(a4)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6144,6113,29])).
% 147.26/147.45 cnf(6154,plain,
% 147.26/147.45 (~E(f2(x61541),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6144,6135,6113,15,29,8])).
% 147.26/147.45 cnf(6155,plain,
% 147.26/147.45 (~E(f5(a3,a4),f2(x61551))),
% 147.26/147.45 inference(scs_inference,[],[6144,6135,6113,15,29,8,2])).
% 147.26/147.45 cnf(6171,plain,
% 147.26/147.45 (P3(f1(f1(a3)),f2(a4),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[6145,5506,5652,418,14,29,24,23])).
% 147.26/147.45 cnf(6208,plain,
% 147.26/147.45 (~P3(f2(a4),f2(f1(a3)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6154,5500,29])).
% 147.26/147.45 cnf(6211,plain,
% 147.26/147.45 (~P3(f1(a3),f2(a4),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6151,6154,5500,6060,5708,29,33])).
% 147.26/147.45 cnf(6213,plain,
% 147.26/147.45 (P3(f1(f2(x62131)),f2(x62131),f2(x62131))),
% 147.26/147.45 inference(scs_inference,[],[6151,6154,5500,6060,5708,357,14,29,33,23])).
% 147.26/147.45 cnf(6228,plain,
% 147.26/147.45 (P3(f1(f2(x62281)),f2(x62281),f2(x62281))),
% 147.26/147.45 inference(rename_variables,[],[6213])).
% 147.26/147.45 cnf(6231,plain,
% 147.26/147.45 (P3(f1(f2(x62311)),f2(x62311),f2(x62311))),
% 147.26/147.45 inference(rename_variables,[],[6213])).
% 147.26/147.45 cnf(6233,plain,
% 147.26/147.45 (P2(f1(f2(a4)),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[6211,6213,6228,6231,6056,6142,6155,5483,5951,5981,5724,6060,1910,9,29,32,33,31])).
% 147.26/147.45 cnf(6236,plain,
% 147.26/147.45 (P3(f1(f2(a4)),f1(a3),f1(a3))),
% 147.26/147.45 inference(scs_inference,[],[6233,14,23])).
% 147.26/147.45 cnf(6239,plain,
% 147.26/147.45 (~P3(f1(f2(x62391)),f2(x62391),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6233,6213,6154,14,23,29])).
% 147.26/147.45 cnf(6255,plain,
% 147.26/147.45 (P3(f1(f1(x62551)),f1(x62551),f1(x62551))),
% 147.26/147.45 inference(scs_inference,[],[65,14,23])).
% 147.26/147.45 cnf(6258,plain,
% 147.26/147.45 (~P3(f1(f2(a3)),f5(a3,a4),f1(x62581))),
% 147.26/147.45 inference(scs_inference,[],[6145,5443,65,14,23,29])).
% 147.26/147.45 cnf(6280,plain,
% 147.26/147.45 (~P3(a3,f5(f2(a4),a4),f2(x62801))),
% 147.26/147.45 inference(scs_inference,[],[6155,5770,29])).
% 147.26/147.45 cnf(6301,plain,
% 147.26/147.45 (~P3(f1(a3),f1(a3),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6208,5788,6236,6154,5894,5475,2011,3308,1947,10,29,32,33])).
% 147.26/147.45 cnf(6308,plain,
% 147.26/147.45 (~P3(f5(f2(a3),f2(a3)),f5(a3,a4),f1(x63081))),
% 147.26/147.45 inference(scs_inference,[],[6301,6145,5429,1910,9,29])).
% 147.26/147.45 cnf(6319,plain,
% 147.26/147.45 (~P3(f5(a3,a4),f1(a4),f5(f1(a4),f1(a4)))),
% 147.26/147.45 inference(scs_inference,[],[6236,5226,6144,5588,2011,29,32])).
% 147.26/147.45 cnf(6379,plain,
% 147.26/147.45 (P3(f1(f2(x63791)),x63791,x63791)),
% 147.26/147.45 inference(scs_inference,[],[5223,6154,50,14,29,23])).
% 147.26/147.45 cnf(6406,plain,
% 147.26/147.45 (P3(f2(a4),f5(f1(a3),a4),a4)),
% 147.26/147.45 inference(scs_inference,[],[6379,5853,5635,5576,5221,32,33])).
% 147.26/147.45 cnf(6419,plain,
% 147.26/147.45 (P3(f1(a3),f2(a4),f2(a4))),
% 147.26/147.45 inference(scs_inference,[],[6308,6379,5603,5146,5408,392,14,29,32,23])).
% 147.26/147.45 cnf(6433,plain,
% 147.26/147.45 (~P3(a3,a4,f1(x64331))),
% 147.26/147.45 inference(scs_inference,[],[6419,6258,6085,6379,5770,3264,29,33,10])).
% 147.26/147.45 cnf(6441,plain,
% 147.26/147.45 (E(f5(x64411,f1(x64411)),x64411)),
% 147.26/147.45 inference(rename_variables,[],[285])).
% 147.26/147.45 cnf(6442,plain,
% 147.26/147.45 (~P3(a3,f5(a4,f1(a4)),f1(x64421))),
% 147.26/147.45 inference(scs_inference,[],[6433,285,6441,9,10])).
% 147.26/147.45 cnf(6447,plain,
% 147.26/147.45 (P3(f1(a3),a4,a4)),
% 147.26/147.45 inference(scs_inference,[],[6433,6406,6419,6255,5524,285,6441,9,10,29,33])).
% 147.26/147.45 cnf(6511,plain,
% 147.26/147.45 (~P3(f1(a3),f2(f1(a3)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6301,1910,10])).
% 147.26/147.45 cnf(6597,plain,
% 147.26/147.45 (~P3(f5(a3,f2(a4)),a4,f1(x65971))),
% 147.26/147.45 inference(scs_inference,[],[6442,5201,269,33])).
% 147.26/147.45 cnf(6702,plain,
% 147.26/147.45 (~P3(f1(a4),f1(f5(a3,a4)),f5(a3,a4))),
% 147.26/147.45 inference(scs_inference,[],[6511,6319,5585,5576,5185,5144,85,33,24,32])).
% 147.26/147.45 cnf(6811,plain,
% 147.26/147.45 (~P3(f1(f2(a3)),f2(a3),a3)),
% 147.26/147.45 inference(scs_inference,[],[5697,5446,6213,32])).
% 147.26/147.45 cnf(6821,plain,
% 147.26/147.45 (~P3(a3,f5(f1(a3),f2(a4)),f2(a3))),
% 147.26/147.45 inference(scs_inference,[],[6811,6116,6379,33])).
% 147.26/147.45 cnf(6849,plain,
% 147.26/147.45 (P2(f1(a4),f1(f5(a3,a4)))),
% 147.26/147.45 inference(scs_inference,[],[17,6821,6113,5563,268,32,28])).
% 147.26/147.45 cnf(6869,plain,
% 147.26/147.45 (P2(f2(f5(a3,a4)),f2(a3))),
% 147.26/147.45 inference(scs_inference,[],[18,5724,27])).
% 147.26/147.45 cnf(6885,plain,
% 147.26/147.45 (P2(f2(f5(a3,a4)),a3)),
% 147.26/147.45 inference(scs_inference,[],[18,6869,6849,5446,15,14,23,24,28])).
% 147.26/147.45 cnf(6913,plain,
% 147.26/147.45 (P3(f2(f5(a3,a4)),a3,a3)),
% 147.26/147.45 inference(scs_inference,[],[6885,15,23])).
% 147.26/147.45 cnf(6952,plain,
% 147.26/147.45 (~P3(f2(f5(a3,a4)),f5(a3,a4),f2(x69521))),
% 147.26/147.45 inference(scs_inference,[],[6913,6280,5770,32])).
% 147.26/147.45 cnf(7002,plain,
% 147.26/147.45 (P3(x70021,f1(x70021),x70021)),
% 147.26/147.45 inference(rename_variables,[],[19])).
% 147.26/147.45 cnf(7005,plain,
% 147.26/147.45 (~P3(f5(a3,a4),f1(f5(a3,a4)),f1(x70051))),
% 147.26/147.45 inference(scs_inference,[],[19,7002,6239,6145,5443,33,29])).
% 147.26/147.45 cnf(7040,plain,
% 147.26/147.45 (P3(f1(a3),f1(a3),f5(f2(a4),f1(a3)))),
% 147.26/147.45 inference(scs_inference,[],[20,5981,5473,32])).
% 147.26/147.45 cnf(7412,plain,
% 147.26/147.45 (E(f1(x74121),f2(f1(x74121)))),
% 147.26/147.45 inference(rename_variables,[],[1947])).
% 147.26/147.45 cnf(7415,plain,
% 147.26/147.45 (E(f1(x74151),f2(f1(x74151)))),
% 147.26/147.45 inference(rename_variables,[],[1947])).
% 147.26/147.45 cnf(7417,plain,
% 147.26/147.45 (E(f1(x74171),f2(f1(x74171)))),
% 147.26/147.45 inference(rename_variables,[],[1947])).
% 147.26/147.45 cnf(7420,plain,
% 147.26/147.45 (E(f1(x74201),f2(f1(x74201)))),
% 147.26/147.45 inference(rename_variables,[],[1947])).
% 147.26/147.45 cnf(7423,plain,
% 147.26/147.45 (E(f1(x74231),f2(f1(x74231)))),
% 147.26/147.45 inference(rename_variables,[],[1947])).
% 147.26/147.45 cnf(7425,plain,
% 147.26/147.45 (E(f1(x74251),f2(f1(x74251)))),
% 147.26/147.45 inference(rename_variables,[],[1947])).
% 147.26/147.45 cnf(7428,plain,
% 147.26/147.45 (P3(f2(x74281),f2(x74281),f5(f2(x74281),f2(x74281)))),
% 147.26/147.45 inference(rename_variables,[],[5146])).
% 147.26/147.45 cnf(7469,plain,
% 147.26/147.45 (P3(f2(x74691),f2(x74691),f5(f2(x74691),f2(x74691)))),
% 147.26/147.45 inference(rename_variables,[],[5146])).
% 147.26/147.45 cnf(7502,plain,
% 147.26/147.45 (P3(f2(x75021),f2(x75021),f5(f2(x75021),f2(x75021)))),
% 147.26/147.45 inference(rename_variables,[],[5146])).
% 147.26/147.45 cnf(7510,plain,
% 147.26/147.45 (P3(f5(f2(a3),a3),a4,f5(f5(f2(a3),a3),a4))),
% 147.26/147.45 inference(scs_inference,[],[5149,908,7005,3421,5293,6447,6419,5306,5221,6255,2005,5770,5247,5249,5201,6060,5185,6379,5146,7428,7469,1947,7412,7415,7417,7420,7423,7425,5,171,190,210,7,191,200,211,1291,201,367,515,735,4342,1550,2614,3907,4021,4147,1369,1873,1894,1899,2149,2609,4393,4395,2713,4721,4846,5039,3081,4098,4100,4149,4412,4414,4589,4848,4940,5041,4449,4451,3095,4305,4307,4348,4402])).
% 147.26/147.45 cnf(7513,plain,
% 147.26/147.45 (P3(f2(x75131),f2(x75131),f5(f2(x75131),f2(x75131)))),
% 147.26/147.45 inference(rename_variables,[],[5146])).
% 147.26/147.45 cnf(7539,plain,
% 147.26/147.45 (P3(f1(x75391),f1(x75391),f5(f2(f1(x75391)),f1(x75391)))),
% 147.26/147.45 inference(rename_variables,[],[3421])).
% 147.26/147.45 cnf(7542,plain,
% 147.26/147.45 (P3(f1(x75421),f1(x75421),f5(f2(f1(x75421)),f1(x75421)))),
% 147.26/147.45 inference(rename_variables,[],[3421])).
% 147.26/147.45 cnf(7592,plain,
% 147.26/147.45 (P3(f5(f1(a3),f2(a4)),a4,f5(f5(f1(a3),f2(a4)),a4))),
% 147.26/147.45 inference(scs_inference,[],[5149,908,7005,3421,7539,7542,3313,1965,5293,6447,6419,6171,5306,5221,5612,6255,2005,5770,5247,7040,5249,5201,6060,5185,5462,6379,5146,7428,7469,7502,1947,7412,7415,7417,7420,7423,7425,3264,5,171,190,210,7,191,200,211,1291,201,367,515,735,4342,1550,2614,3907,4021,4147,1369,1873,1894,1899,2149,2609,4393,4395,2713,4721,4846,5039,3081,4098,4100,4149,4412,4414,4589,4848,4940,5041,4449,4451,3095,4305,4307,4348,4402,3858,3798,3964,4010,3811,4362,4605,5003,4673,3752,4724,161,1516,1711,424,940,840,364,594,1031,421,666,1343,4390,121,124,1408,2116,2357,924,152,923,1004,730,642,414,2773,1203,391])).
% 147.26/147.45 cnf(7611,plain,
% 147.26/147.45 (E(f5(f5(x76111,f5(x76112,f1(x76112))),x76113),f5(f5(x76111,x76112),x76113))),
% 147.26/147.45 inference(scs_inference,[],[5149,908,6702,3179,7005,6952,3421,7539,7542,3313,1965,5293,6447,6419,6171,5306,5221,5612,6255,2005,5770,5247,7040,5249,5201,6060,5185,5462,6379,5146,7428,7469,7502,7513,1947,7412,7415,7417,7420,7423,7425,3264,5,171,190,210,7,191,200,211,1291,201,367,515,735,4342,1550,2614,3907,4021,4147,1369,1873,1894,1899,2149,2609,4393,4395,2713,4721,4846,5039,3081,4098,4100,4149,4412,4414,4589,4848,4940,5041,4449,4451,3095,4305,4307,4348,4402,3858,3798,3964,4010,3811,4362,4605,5003,4673,3752,4724,161,1516,1711,424,940,840,364,594,1031,421,666,1343,4390,121,124,1408,2116,2357,924,152,923,1004,730,642,414,2773,1203,391,1909,1870,106,328,103,2,1361,352,6])).
% 147.26/147.45 cnf(8834,plain,
% 147.26/147.45 (E(f5(f5(x88341,x88342),x88343),f5(f5(x88341,f5(x88342,f1(x88342))),x88343))),
% 147.26/147.45 inference(scs_inference,[],[3324,3343,7611,6014,89,321,117,2])).
% 147.26/147.45 cnf(9556,plain,
% 147.26/147.45 (E(x95561,f5(x95561,f1(x95561)))),
% 147.26/147.45 inference(rename_variables,[],[265])).
% 147.26/147.45 cnf(9558,plain,
% 147.26/147.45 (E(x95581,f5(x95581,f1(x95581)))),
% 147.26/147.45 inference(rename_variables,[],[265])).
% 147.26/147.45 cnf(9560,plain,
% 147.26/147.45 (E(x95601,f5(x95601,f1(x95601)))),
% 147.26/147.45 inference(rename_variables,[],[265])).
% 147.26/147.45 cnf(9569,plain,
% 147.26/147.45 ($false),
% 147.26/147.45 inference(scs_inference,[],[14,265,9556,9558,9560,19,21,5146,5585,7592,485,2469,7510,3905,6062,6597,8834,5570,89,70,68,41,118,1567,72,13,9,10,11,12,28,29,24]),
% 147.26/147.45 ['proof']).
% 147.26/147.45 % SZS output end Proof
% 147.26/147.45 % Total time :146.640000s
%------------------------------------------------------------------------------