%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN004-5 : 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 : n022.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 07:26:47 EDT 2024
% Result : Unsatisfiable 281.74s 281.71s
% Output : CNFRefutation 281.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HEN004-5 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n022.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Sat Jun 22 05:29:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.20/0.54 start to proof:theBenchmark
% 281.73/281.70 %-------------------------------------------
% 281.73/281.70 % File :CSE---1.7
% 281.73/281.70 % Problem :theBenchmark
% 281.73/281.70 % Transform :cnf
% 281.73/281.70 % Format :tptp:raw
% 281.73/281.70 % Command :java -jar mcs_scs.jar %d %s
% 281.73/281.70
% 281.73/281.70 % Result :Theorem 281.090000s
% 281.73/281.70 % Output :CNFRefutation 281.090000s
% 281.73/281.70 %-------------------------------------------
% 281.74/281.71 %--------------------------------------------------------------------------
% 281.74/281.71 % File : HEN004-5 : TPTP v8.2.0. Released v1.0.0.
% 281.74/281.71 % Domain : Henkin Models
% 281.74/281.71 % Problem : X/zero = X
% 281.74/281.71 % Version : [MOW76] (equality) axioms : Reduced & Augmented > Complete.
% 281.74/281.71 % English :
% 281.74/281.71
% 281.74/281.71 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 281.74/281.71 % Source : [ANL]
% 281.74/281.71 % Names : hp4.ver3.in [ANL]
% 281.74/281.71
% 281.74/281.71 % Status : Unsatisfiable
% 281.74/281.71 % Rating : 0.00 v6.3.0, 0.10 v6.2.0, 0.20 v6.1.0, 0.09 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.00 v5.3.0, 0.20 v5.2.0, 0.00 v5.1.0, 0.11 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.25 v4.0.0, 0.14 v3.7.0, 0.00 v2.0.0
% 281.74/281.71 % Syntax : Number of clauses : 7 ( 6 unt; 0 nHn; 2 RR)
% 281.74/281.71 % Number of literals : 9 ( 9 equ; 3 neg)
% 281.74/281.71 % Maximal clause size : 3 ( 1 avg)
% 281.74/281.71 % Maximal term depth : 4 ( 1 avg)
% 281.74/281.71 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 281.74/281.71 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 281.74/281.71 % Number of variables : 10 ( 3 sgn)
% 281.74/281.71 % SPC : CNF_UNS_RFO_PEQ_NUE
% 281.74/281.71
% 281.74/281.71 % Comments : less_equal replaced by divides
% 281.74/281.71 %--------------------------------------------------------------------------
% 281.74/281.71 %----Include Henkin model axioms, for the equality formulation with
% 281.74/281.71 %----less_equals removed.
% 281.74/281.71 include('Axioms/HEN003-0.ax').
% 281.74/281.71 %--------------------------------------------------------------------------
% 281.74/281.71 cnf(x_divide_x_is_zero,axiom,
% 281.74/281.71 divide(X,X) = zero ).
% 281.74/281.71
% 281.74/281.71 cnf(prove_x_divide_zero_is_x,negated_conjecture,
% 281.74/281.71 divide(a,zero) != a ).
% 281.74/281.71
% 281.74/281.71 %--------------------------------------------------------------------------
% 281.74/281.71 %-------------------------------------------
% 281.74/281.71 % Proof found
% 281.74/281.71 % SZS status Theorem for theBenchmark
% 281.74/281.71 % SZS output start Proof
% 281.74/281.71 %ClaNum:12(EqnAxiom:5)
% 281.74/281.71 %VarNum:20(SingletonVarNum:10)
% 281.74/281.71 %MaxLitNum:3
% 281.74/281.71 %MaxfuncDepth:3
% 281.74/281.71 %SharedTerms:5
% 281.74/281.71 %goalClause: 11
% 281.74/281.71 %singleGoalClaCount:1
% 281.74/281.71 [11]~E(f2(a3,a4),a3)
% 281.74/281.71 [6]E(f2(x61,a1),a4)
% 281.74/281.71 [7]E(f2(a4,x71),a4)
% 281.74/281.71 [8]E(f2(x81,x81),a4)
% 281.74/281.71 [9]E(f2(f2(x91,x92),x91),a4)
% 281.74/281.71 [10]E(f2(f2(f2(x101,x102),f2(x103,x102)),f2(f2(x101,x103),x102)),a4)
% 281.74/281.71 [12]E(x121,x122)+~E(f2(x122,x121),a4)+~E(f2(x121,x122),a4)
% 281.74/281.71 %EqnAxiom
% 281.74/281.71 [1]E(x11,x11)
% 281.74/281.71 [2]E(x22,x21)+~E(x21,x22)
% 281.74/281.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 281.74/281.71 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 281.74/281.71 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 281.74/281.72
% 281.74/281.72 %-------------------------------------------
% 281.77/281.73 cnf(13,plain,
% 281.77/281.73 (E(a4,f2(x131,x131))),
% 281.77/281.73 inference(scs_inference,[],[8,2])).
% 281.77/281.73 cnf(14,plain,
% 281.77/281.73 (E(a4,f2(a4,x141))),
% 281.77/281.73 inference(scs_inference,[],[8,7,9,2,12])).
% 281.77/281.73 cnf(18,plain,
% 281.77/281.73 (E(f2(x181,x181),f2(a4,x182))),
% 281.77/281.73 inference(scs_inference,[],[8,7,9,2,12,3])).
% 281.77/281.73 cnf(19,plain,
% 281.77/281.73 (E(f2(a4,x191),f2(x192,x192))),
% 281.77/281.73 inference(scs_inference,[],[18,2])).
% 281.77/281.73 cnf(20,plain,
% 281.77/281.73 (E(f2(x201,a1),f2(a4,x202))),
% 281.77/281.73 inference(scs_inference,[],[14,18,6,2,3])).
% 281.77/281.73 cnf(21,plain,
% 281.77/281.73 (E(f2(f2(x211,x212),x213),f2(f2(x211,x213),f2(x212,x213)))+~E(f2(f2(f2(x211,x212),x213),f2(f2(x211,x213),f2(x212,x213))),a4)),
% 281.77/281.73 inference(scs_inference,[],[14,18,6,10,2,3,12])).
% 281.77/281.73 cnf(23,plain,
% 281.77/281.73 (E(f2(a4,x231),f2(x232,a1))),
% 281.77/281.73 inference(scs_inference,[],[20,2])).
% 281.77/281.73 cnf(24,plain,
% 281.77/281.73 (E(f2(x241,a1),f2(x242,x242))),
% 281.77/281.73 inference(scs_inference,[],[20,13,6,2,3])).
% 281.77/281.73 cnf(25,plain,
% 281.77/281.73 (E(f2(x251,x251),f2(x252,a1))),
% 281.77/281.73 inference(scs_inference,[],[24,2])).
% 281.77/281.73 cnf(26,plain,
% 281.77/281.73 (E(f2(f2(f2(x261,x262),f2(x263,x262)),f2(f2(x261,x263),x262)),f2(a4,x264))),
% 281.77/281.73 inference(scs_inference,[],[14,24,10,2,3])).
% 281.77/281.73 cnf(27,plain,
% 281.77/281.73 (E(f2(a4,x271),f2(f2(f2(x272,x273),f2(x274,x273)),f2(f2(x272,x274),x273)))),
% 281.77/281.73 inference(scs_inference,[],[26,2])).
% 281.77/281.73 cnf(28,plain,
% 281.77/281.73 (E(f2(f2(f2(x281,x282),f2(x283,x282)),f2(f2(x281,x283),x282)),f2(x284,x284))),
% 281.77/281.73 inference(scs_inference,[],[26,13,10,2,3])).
% 281.77/281.73 cnf(29,plain,
% 281.77/281.73 (E(f2(x291,x291),f2(f2(f2(x292,x293),f2(x294,x293)),f2(f2(x292,x294),x293)))),
% 281.77/281.73 inference(scs_inference,[],[28,2])).
% 281.77/281.73 cnf(30,plain,
% 281.77/281.73 (E(a4,f2(f2(f2(x301,x302),f2(x303,x302)),f2(f2(x301,x303),x302)))),
% 281.77/281.73 inference(scs_inference,[],[14,28,27,2,3])).
% 281.77/281.73 cnf(32,plain,
% 281.77/281.73 (E(a4,f2(f2(x321,x322),x321))),
% 281.77/281.73 inference(scs_inference,[],[9,2])).
% 281.77/281.73 cnf(33,plain,
% 281.77/281.73 (E(f2(x331,x331),f2(x332,x332))),
% 281.77/281.73 inference(scs_inference,[],[29,28,9,2,3])).
% 281.77/281.73 cnf(35,plain,
% 281.77/281.73 (E(a4,f2(x351,a1))),
% 281.77/281.73 inference(scs_inference,[],[6,2])).
% 281.77/281.73 cnf(36,plain,
% 281.77/281.73 (E(f2(f2(f2(x361,x362),f2(x363,x362)),f2(f2(x361,x363),x362)),f2(f2(x364,x365),x364))),
% 281.77/281.73 inference(scs_inference,[],[32,10,6,2,3])).
% 281.77/281.73 cnf(37,plain,
% 281.77/281.73 (E(f2(f2(x371,x372),x371),f2(f2(f2(x373,x374),f2(x375,x374)),f2(f2(x373,x375),x374)))),
% 281.77/281.73 inference(scs_inference,[],[36,2])).
% 281.77/281.73 cnf(38,plain,
% 281.77/281.73 (E(f2(f2(f2(x381,x382),f2(x383,x382)),f2(f2(x381,x383),x382)),f2(x384,a1))),
% 281.77/281.73 inference(scs_inference,[],[36,35,10,2,3])).
% 281.77/281.73 cnf(39,plain,
% 281.77/281.73 (E(f2(x391,a1),f2(f2(f2(x392,x393),f2(x394,x393)),f2(f2(x392,x394),x393)))),
% 281.77/281.73 inference(scs_inference,[],[38,2])).
% 281.77/281.73 cnf(40,plain,
% 281.77/281.73 (E(f2(f2(x401,x402),x401),f2(x403,a1))),
% 281.77/281.73 inference(scs_inference,[],[37,38,2,3])).
% 281.77/281.73 cnf(42,plain,
% 281.77/281.73 (E(f2(x421,a1),f2(f2(x422,x423),x422))),
% 281.77/281.73 inference(scs_inference,[],[40,2])).
% 281.77/281.73 cnf(43,plain,
% 281.77/281.73 (E(f2(x431,a1),f2(x432,a1))),
% 281.77/281.73 inference(scs_inference,[],[40,39,38,2,3])).
% 281.77/281.73 cnf(45,plain,
% 281.77/281.73 (E(f2(a4,x451),f2(f2(x452,a1),x451))),
% 281.77/281.73 inference(scs_inference,[],[6,4,2])).
% 281.77/281.73 cnf(46,plain,
% 281.77/281.73 (E(f2(f2(x461,a1),x462),f2(a4,x462))),
% 281.77/281.73 inference(scs_inference,[],[45,2])).
% 281.77/281.73 cnf(47,plain,
% 281.77/281.73 (E(a4,f2(f2(x471,a1),x472))),
% 281.77/281.73 inference(scs_inference,[],[14,45,2,3])).
% 281.77/281.73 cnf(49,plain,
% 281.77/281.73 (E(f2(x491,a4),f2(x491,f2(x492,a1)))),
% 281.77/281.73 inference(scs_inference,[],[6,5,2])).
% 281.77/281.73 cnf(50,plain,
% 281.77/281.73 (E(f2(f2(x501,a1),x502),a4)),
% 281.77/281.73 inference(scs_inference,[],[47,2])).
% 281.77/281.73 cnf(51,plain,
% 281.77/281.73 (E(f2(f2(x511,x512),a1),f2(f2(x511,a1),f2(x512,a1)))),
% 281.77/281.73 inference(scs_inference,[],[47,10,2,12])).
% 281.77/281.73 cnf(54,plain,
% 281.77/281.73 (E(f2(x541,a1),f2(f2(f2(x542,x543),a1),f2(f2(x542,a1),f2(x543,a1))))),
% 281.77/281.73 inference(scs_inference,[],[6,47,10,2,12,3])).
% 281.77/281.73 cnf(56,plain,
% 281.77/281.73 (E(f2(f2(f2(x561,x562),a1),x563),f2(f2(f2(x561,a1),f2(x562,a1)),x563))),
% 281.77/281.73 inference(scs_inference,[],[50,21,4])).
% 281.77/281.73 cnf(57,plain,
% 281.77/281.73 (E(f2(f2(x571,a1),f2(x572,a1)),f2(f2(x571,x572),a1))),
% 281.77/281.73 inference(scs_inference,[],[51,2])).
% 281.77/281.73 cnf(58,plain,
% 281.77/281.73 (E(f2(x581,a1),f2(f2(x581,a1),x582))),
% 281.77/281.73 inference(scs_inference,[],[51,50,9,2,12])).
% 281.77/281.73 cnf(62,plain,
% 281.77/281.73 (E(f2(x621,x621),f2(f2(x622,a1),f2(x623,a1)))),
% 281.77/281.73 inference(scs_inference,[],[51,25,50,9,2,12,3])).
% 281.77/281.73 cnf(64,plain,
% 281.77/281.73 (~E(f2(a3,f2(a3,a4)),a4)),
% 281.77/281.73 inference(scs_inference,[],[11,9,2,12])).
% 281.77/281.73 cnf(65,plain,
% 281.77/281.73 (E(f2(f2(x651,a1),x652),f2(x651,a1))),
% 281.77/281.73 inference(scs_inference,[],[58,2])).
% 281.77/281.73 cnf(66,plain,
% 281.77/281.73 (~E(f2(a3,f2(a3,a4)),f2(x661,a1))),
% 281.77/281.73 inference(scs_inference,[],[6,58,64,2,3])).
% 281.77/281.73 cnf(67,plain,
% 281.77/281.73 (~E(f2(a3,a4),a1)),
% 281.77/281.73 inference(scs_inference,[],[6,58,64,2,3,5])).
% 281.77/281.73 cnf(68,plain,
% 281.77/281.73 (E(a1,a3)+~E(f2(a1,a3),a4)),
% 281.77/281.73 inference(scs_inference,[],[6,58,64,2,3,5,12])).
% 281.77/281.73 cnf(72,plain,
% 281.77/281.73 (E(f2(f2(x721,a1),f2(x722,a1)),f2(x723,x723))),
% 281.77/281.73 inference(scs_inference,[],[62,2])).
% 281.77/281.73 cnf(73,plain,
% 281.77/281.73 (~E(f2(a3,f2(a3,a4)),f2(f2(x731,a1),x732))),
% 281.77/281.73 inference(scs_inference,[],[50,62,64,2,3])).
% 281.77/281.73 cnf(74,plain,
% 281.77/281.73 (~E(a3,f2(x741,a1))),
% 281.77/281.73 inference(scs_inference,[],[50,62,64,2,3,4])).
% 281.77/281.73 cnf(79,plain,
% 281.77/281.73 (E(f2(f2(f2(x791,x792),a1),f2(f2(x791,a1),f2(x792,a1))),f2(x793,a1))),
% 281.77/281.73 inference(scs_inference,[],[54,2])).
% 281.77/281.73 cnf(80,plain,
% 281.77/281.73 (~E(f2(a3,f2(a3,a4)),f2(x801,x801))),
% 281.77/281.73 inference(scs_inference,[],[33,54,66,2,3])).
% 281.77/281.73 cnf(83,plain,
% 281.77/281.73 (~E(a3,f2(a3,a4))),
% 281.77/281.73 inference(scs_inference,[],[33,54,66,2,3,4])).
% 281.77/281.73 cnf(85,plain,
% 281.77/281.73 (E(f2(x851,f2(x852,a1)),f2(x851,a4))),
% 281.77/281.73 inference(scs_inference,[],[49,2])).
% 281.77/281.73 cnf(86,plain,
% 281.77/281.73 (~E(f2(a3,f2(a3,a4)),f2(a4,x861))),
% 281.77/281.73 inference(scs_inference,[],[19,66,49,2,3])).
% 281.77/281.73 cnf(91,plain,
% 281.77/281.73 (~E(a3,f2(a3,f2(x911,a1)))),
% 281.77/281.74 inference(scs_inference,[],[85,83,3])).
% 281.77/281.74 cnf(94,plain,
% 281.77/281.74 (~E(f2(a3,f2(a3,a4)),f2(f2(f2(x941,x942),f2(x943,x942)),f2(f2(x941,x943),x942)))),
% 281.77/281.74 inference(scs_inference,[],[36,66,3])).
% 281.77/281.74 cnf(98,plain,
% 281.77/281.74 (~E(f2(a3,f2(a3,a4)),f2(f2(x981,x982),x981))),
% 281.77/281.74 inference(scs_inference,[],[37,94,3])).
% 281.77/281.74 cnf(101,plain,
% 281.77/281.74 (E(f2(a4,x1011),f2(f2(x1012,x1012),x1011))),
% 281.77/281.74 inference(scs_inference,[],[8,2,4])).
% 281.77/281.74 cnf(102,plain,
% 281.77/281.74 (E(f2(f2(x1021,x1021),x1022),f2(a4,x1022))),
% 281.77/281.74 inference(scs_inference,[],[101,2])).
% 281.77/281.74 cnf(103,plain,
% 281.77/281.74 (~E(a1,f2(a3,a4))),
% 281.77/281.74 inference(scs_inference,[],[66,2,5])).
% 281.77/281.74 cnf(104,plain,
% 281.77/281.74 (E(f2(a4,x1041),f2(f2(f2(x1042,x1043),x1042),x1041))),
% 281.77/281.74 inference(scs_inference,[],[9,2,4])).
% 281.77/281.74 cnf(105,plain,
% 281.77/281.74 (E(f2(f2(f2(x1051,x1052),x1051),x1053),f2(a4,x1053))),
% 281.77/281.74 inference(scs_inference,[],[104,2])).
% 281.77/281.74 cnf(106,plain,
% 281.77/281.74 (E(f2(x1061,a4),f2(x1061,f2(f2(x1062,x1063),x1062)))),
% 281.77/281.74 inference(scs_inference,[],[9,2,5])).
% 281.77/281.74 cnf(107,plain,
% 281.77/281.74 (E(f2(x1071,f2(f2(x1072,x1073),x1072)),f2(x1071,a4))),
% 281.77/281.74 inference(scs_inference,[],[106,2])).
% 281.77/281.74 cnf(113,plain,
% 281.77/281.74 (~E(a1,f2(a3,f2(f2(x1131,x1132),x1131)))),
% 281.77/281.74 inference(scs_inference,[],[107,103,3])).
% 281.77/281.74 cnf(118,plain,
% 281.77/281.74 (~E(a4,a3)),
% 281.77/281.74 inference(scs_inference,[],[86,2,4])).
% 281.77/281.74 cnf(119,plain,
% 281.77/281.74 (E(f2(x1191,f2(x1192,x1192)),f2(x1191,a4))),
% 281.77/281.74 inference(scs_inference,[],[13,2,5])).
% 281.77/281.74 cnf(120,plain,
% 281.77/281.74 (E(f2(x1201,a4),f2(x1201,f2(x1202,x1202)))),
% 281.77/281.74 inference(scs_inference,[],[119,2])).
% 281.77/281.74 cnf(121,plain,
% 281.77/281.74 (E(a3,a1)+~E(f2(a1,a3),a4)),
% 281.77/281.74 inference(scs_inference,[],[68,2])).
% 281.77/281.74 cnf(122,plain,
% 281.77/281.74 (~E(a4,f2(a1,a3))+E(a3,a1)),
% 281.77/281.74 inference(scs_inference,[],[121,2])).
% 281.77/281.74 cnf(123,plain,
% 281.77/281.74 (~E(f2(a4,x1231),f2(a1,a3))+E(a3,a1)),
% 281.77/281.74 inference(scs_inference,[],[14,122,3])).
% 281.77/281.74 cnf(124,plain,
% 281.77/281.74 (~E(a4,a1)+E(a3,a1)),
% 281.77/281.74 inference(scs_inference,[],[123,4])).
% 281.77/281.74 cnf(125,plain,
% 281.77/281.74 (~E(a1,a4)+E(a3,a1)),
% 281.77/281.74 inference(scs_inference,[],[124,2])).
% 281.77/281.74 cnf(160,plain,
% 281.77/281.74 (~E(a3,f2(f2(x1601,a1),x1602))),
% 281.77/281.74 inference(scs_inference,[],[74,65,3])).
% 281.77/281.74 cnf(165,plain,
% 281.77/281.74 (~E(a3,f2(x1651,x1651))),
% 281.77/281.74 inference(scs_inference,[],[74,33,3])).
% 281.77/281.74 cnf(177,plain,
% 281.77/281.74 (~E(a3,f2(f2(x1771,x1772),x1771))),
% 281.77/281.74 inference(scs_inference,[],[74,40,3])).
% 281.77/281.74 cnf(180,plain,
% 281.77/281.74 (~E(a3,f2(f2(f2(x1801,x1801),x1802),a4))),
% 281.77/281.74 inference(scs_inference,[],[120,177,3])).
% 281.77/281.74 cnf(194,plain,
% 281.77/281.74 (~E(a3,f2(a3,f2(x1941,x1941)))),
% 281.77/281.74 inference(scs_inference,[],[83,119,3])).
% 281.77/281.74 cnf(202,plain,
% 281.77/281.74 (~E(f2(a3,f2(a3,a4)),f2(f2(f2(x2021,x2022),x2021),x2023))),
% 281.77/281.74 inference(scs_inference,[],[86,105,3])).
% 281.77/281.74 cnf(219,plain,
% 281.77/281.74 (~E(f2(a3,f2(a3,a4)),f2(f2(f2(x2191,x2191),x2192),a4))),
% 281.77/281.74 inference(scs_inference,[],[98,120,3])).
% 281.77/281.74 cnf(242,plain,
% 281.77/281.74 (~E(a1,f2(a3,f2(x2421,a1)))),
% 281.77/281.74 inference(scs_inference,[],[103,85,3])).
% 281.77/281.74 cnf(303,plain,
% 281.77/281.74 (~E(f2(a3,f2(a3,a4)),f2(f2(f2(x3031,x3031),x3032),f2(x3033,a1)))),
% 281.77/281.74 inference(scs_inference,[],[219,85,3])).
% 281.77/281.74 cnf(391,plain,
% 281.77/281.74 (~E(a1,f2(x3911,a1))+~E(a1,a4)),
% 281.77/281.74 inference(scs_inference,[],[74,125,3])).
% 281.77/281.74 cnf(678,plain,
% 281.77/281.74 (~E(a1,a4)+~E(f2(a1,f2(x6781,a1)),a4)),
% 281.77/281.74 inference(scs_inference,[],[50,391,12])).
% 281.77/281.74 cnf(679,plain,
% 281.77/281.74 (~E(a4,f2(a1,f2(x6791,a1)))+~E(a1,a4)),
% 281.77/281.74 inference(scs_inference,[],[678,2])).
% 281.77/281.74 cnf(680,plain,
% 281.77/281.74 (~E(a4,f2(a1,a4))+~E(a1,a4)),
% 281.77/281.74 inference(scs_inference,[],[120,679,3])).
% 281.77/281.74 cnf(681,plain,
% 281.77/281.74 (~E(f2(a1,a4),a4)+~E(a1,a4)),
% 281.77/281.74 inference(scs_inference,[],[680,2])).
% 281.77/281.74 cnf(785,plain,
% 281.77/281.74 (~E(a4,f2(a1,a4))+~E(f2(a1,a4),a4)),
% 281.77/281.74 inference(scs_inference,[],[6,680,12])).
% 281.77/281.74 cnf(786,plain,
% 281.77/281.74 (~E(a4,f2(a1,a4))),
% 281.77/281.74 inference(scs_inference,[],[785,2])).
% 281.77/281.74 cnf(787,plain,
% 281.77/281.74 (~E(a4,f2(a1,f2(x7871,a1)))),
% 281.77/281.74 inference(scs_inference,[],[786,85,3])).
% 281.77/281.74 cnf(789,plain,
% 281.77/281.74 (~E(f2(a1,a4),a4)),
% 281.77/281.74 inference(scs_inference,[],[6,681,12])).
% 281.77/281.74 cnf(790,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(x7901,a1),x7902))),
% 281.77/281.74 inference(scs_inference,[],[50,789,3])).
% 281.77/281.74 cnf(791,plain,
% 281.77/281.74 (~E(a1,f2(x7911,a1))),
% 281.77/281.74 inference(scs_inference,[],[50,789,3,4])).
% 281.77/281.74 cnf(797,plain,
% 281.77/281.74 (~E(a4,f2(a1,f2(f2(x7971,x7972),x7971)))),
% 281.77/281.74 inference(scs_inference,[],[786,107,3])).
% 281.77/281.74 cnf(800,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(x8001,x8002),f2(x8003,x8002)),f2(f2(x8001,x8003),x8002)))),
% 281.77/281.74 inference(scs_inference,[],[789,10,3])).
% 281.77/281.74 cnf(802,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(x8021,x8021))),
% 281.77/281.74 inference(scs_inference,[],[29,800,3])).
% 281.77/281.74 cnf(809,plain,
% 281.77/281.74 (~E(a1,f2(f2(x8091,x8092),x8091))),
% 281.77/281.74 inference(scs_inference,[],[802,106,3,4])).
% 281.77/281.74 cnf(810,plain,
% 281.77/281.74 (~E(a4,f2(a1,f2(x8101,x8101)))),
% 281.77/281.74 inference(scs_inference,[],[786,119,3])).
% 281.77/281.74 cnf(812,plain,
% 281.77/281.74 (E(f2(f2(a4,x8121),x8122),f2(a4,x8122))),
% 281.77/281.74 inference(scs_inference,[],[14,4,2])).
% 281.77/281.74 cnf(813,plain,
% 281.77/281.74 (E(f2(a4,x8131),f2(f2(a4,x8132),x8131))),
% 281.77/281.74 inference(scs_inference,[],[812,2])).
% 281.77/281.74 cnf(815,plain,
% 281.77/281.74 (E(f2(f2(f2(x8151,a1),f2(x8152,a1)),x8153),f2(f2(f2(x8151,x8152),a1),x8153))),
% 281.77/281.74 inference(scs_inference,[],[51,4,2])).
% 281.77/281.74 cnf(816,plain,
% 281.77/281.74 (E(f2(f2(x8161,a4),x8162),f2(f2(x8161,f2(a4,x8163)),x8162))),
% 281.77/281.74 inference(scs_inference,[],[14,4,5])).
% 281.77/281.74 cnf(817,plain,
% 281.77/281.74 (E(f2(f2(x8171,f2(a4,x8172)),x8173),f2(f2(x8171,a4),x8173))),
% 281.77/281.74 inference(scs_inference,[],[816,2])).
% 281.77/281.74 cnf(820,plain,
% 281.77/281.74 (E(f2(f2(f2(x8201,a1),x8202),x8203),f2(f2(x8201,a1),x8203))),
% 281.77/281.74 inference(scs_inference,[],[58,4,2])).
% 281.77/281.74 cnf(826,plain,
% 281.77/281.74 (E(f2(x8261,f2(a4,x8262)),f2(x8261,f2(f2(a4,x8263),x8262)))),
% 281.77/281.74 inference(scs_inference,[],[14,4,5])).
% 281.77/281.74 cnf(827,plain,
% 281.77/281.74 (E(f2(x8271,f2(f2(a4,x8272),x8273)),f2(x8271,f2(a4,x8273)))),
% 281.77/281.74 inference(scs_inference,[],[826,2])).
% 281.77/281.74 cnf(831,plain,
% 281.77/281.74 (~E(f2(f2(x8311,x8312),x8311),a3)),
% 281.77/281.74 inference(scs_inference,[],[202,4,2])).
% 281.77/281.74 cnf(839,plain,
% 281.77/281.74 (E(f2(a4,a1),f2(f2(f2(a4,x8391),a1),x8392))),
% 281.77/281.74 inference(scs_inference,[],[14,58,4,3])).
% 281.77/281.74 cnf(840,plain,
% 281.77/281.74 (E(f2(f2(f2(a4,x8401),a1),x8402),f2(a4,a1))),
% 281.77/281.74 inference(scs_inference,[],[839,2])).
% 281.77/281.74 cnf(843,plain,
% 281.77/281.74 (~E(a1,f2(f2(x8431,a1),x8432))),
% 281.77/281.74 inference(scs_inference,[],[802,50,4,3])).
% 281.77/281.74 cnf(844,plain,
% 281.77/281.74 (~E(f2(x8441,a1),a1)),
% 281.77/281.74 inference(scs_inference,[],[790,4,2])).
% 281.77/281.74 cnf(848,plain,
% 281.77/281.74 (~E(f2(a3,f2(f2(a1,x8481),a1)),a4)),
% 281.77/281.74 inference(scs_inference,[],[202,50,4,12])).
% 281.77/281.74 cnf(849,plain,
% 281.77/281.74 (~E(f2(a3,f2(f2(a1,x8491),a1)),f2(f2(x8492,a1),x8493))),
% 281.77/281.74 inference(scs_inference,[],[50,848,3])).
% 281.77/281.74 cnf(850,plain,
% 281.77/281.74 (~E(f2(a3,f2(x8501,a1)),a4)),
% 281.77/281.74 inference(scs_inference,[],[849,50,4,12])).
% 281.77/281.74 cnf(851,plain,
% 281.77/281.74 (~E(f2(a3,f2(x8511,a1)),f2(f2(x8512,a1),x8513))),
% 281.77/281.74 inference(scs_inference,[],[50,850,3])).
% 281.77/281.74 cnf(852,plain,
% 281.77/281.74 (~E(f2(a3,f2(x8521,a1)),f2(f2(f2(x8522,x8523),f2(x8524,x8523)),f2(f2(x8522,x8524),x8523)))),
% 281.77/281.74 inference(scs_inference,[],[850,10,3])).
% 281.77/281.74 cnf(853,plain,
% 281.77/281.74 (E(f2(x8531,f2(a4,x8532)),f2(x8531,a4))),
% 281.77/281.74 inference(scs_inference,[],[14,5,2])).
% 281.77/281.74 cnf(854,plain,
% 281.77/281.74 (E(f2(x8541,a4),f2(x8541,f2(a4,x8542)))),
% 281.77/281.74 inference(scs_inference,[],[853,2])).
% 281.77/281.74 cnf(855,plain,
% 281.77/281.74 (~E(a4,f2(a1,f2(a4,x8551)))),
% 281.77/281.74 inference(scs_inference,[],[853,786,2,3])).
% 281.77/281.74 cnf(858,plain,
% 281.77/281.74 (E(f2(x8581,f2(f2(x8582,a1),f2(x8583,a1))),f2(x8581,f2(f2(x8582,x8583),a1)))),
% 281.77/281.74 inference(scs_inference,[],[51,5,2])).
% 281.77/281.74 cnf(862,plain,
% 281.77/281.74 (~E(f2(a3,f2(a4,x8621)),a1)),
% 281.77/281.74 inference(scs_inference,[],[66,854,5,3])).
% 281.77/281.74 cnf(863,plain,
% 281.77/281.74 (~E(f2(a1,f2(a3,a4)),a4)),
% 281.77/281.74 inference(scs_inference,[],[66,6,5,12])).
% 281.77/281.74 cnf(907,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(x9071,x9072),x9071))),
% 281.77/281.74 inference(scs_inference,[],[789,9,3])).
% 281.77/281.74 cnf(910,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(a4,x9101),x9102),a4))),
% 281.77/281.74 inference(scs_inference,[],[854,907,3])).
% 281.77/281.74 cnf(913,plain,
% 281.77/281.74 (~E(a1,f2(f2(a4,x9131),x9132))),
% 281.77/281.74 inference(scs_inference,[],[854,907,3,4])).
% 281.77/281.74 cnf(916,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(a4,x9161))),
% 281.77/281.74 inference(scs_inference,[],[789,7,3])).
% 281.77/281.74 cnf(923,plain,
% 281.77/281.74 (~E(a1,f2(x9231,x9231))),
% 281.77/281.74 inference(scs_inference,[],[791,18,3])).
% 281.77/281.74 cnf(927,plain,
% 281.77/281.74 (~E(a1,f2(f2(f2(x9271,x9272),f2(x9273,x9272)),f2(f2(x9271,x9273),x9272)))),
% 281.77/281.74 inference(scs_inference,[],[791,36,3])).
% 281.77/281.74 cnf(933,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(x9331,x9332),a4),f2(f2(x9331,a4),x9332)))),
% 281.77/281.74 inference(scs_inference,[],[800,816,3])).
% 281.77/281.74 cnf(954,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(x9541,a4),f2(x9541,f2(a4,x9542))))),
% 281.77/281.74 inference(scs_inference,[],[802,816,3])).
% 281.77/281.74 cnf(987,plain,
% 281.77/281.74 (~E(a1,f2(f2(f2(x9871,x9871),x9872),a4))),
% 281.77/281.74 inference(scs_inference,[],[809,120,3])).
% 281.77/281.74 cnf(1024,plain,
% 281.77/281.74 (~E(a1,f2(f2(f2(x10241,a1),x10242),x10243))),
% 281.77/281.74 inference(scs_inference,[],[843,820,3])).
% 281.77/281.74 cnf(1033,plain,
% 281.77/281.74 (~E(f2(a3,f2(x10331,a1)),f2(x10332,x10332))),
% 281.77/281.74 inference(scs_inference,[],[850,8,3])).
% 281.77/281.74 cnf(1035,plain,
% 281.77/281.74 (~E(f2(a3,f2(x10351,a1)),f2(f2(x10352,x10353),x10352))),
% 281.77/281.74 inference(scs_inference,[],[850,9,3])).
% 281.77/281.74 cnf(1038,plain,
% 281.77/281.74 (~E(f2(a3,f2(x10381,a1)),f2(a4,x10382))),
% 281.77/281.74 inference(scs_inference,[],[850,7,3])).
% 281.77/281.74 cnf(1040,plain,
% 281.77/281.74 (~E(f2(a3,f2(x10401,a1)),f2(f2(f2(x10402,a1),x10403),x10404))),
% 281.77/281.74 inference(scs_inference,[],[851,820,3])).
% 281.77/281.74 cnf(1044,plain,
% 281.77/281.74 (~E(f2(a3,f2(x10441,a1)),f2(f2(f2(x10442,x10443),a4),f2(f2(x10442,a4),x10443)))),
% 281.77/281.74 inference(scs_inference,[],[852,816,3])).
% 281.77/281.74 cnf(1055,plain,
% 281.77/281.74 (~E(a4,f2(a1,f2(f2(a4,x10551),x10552)))),
% 281.77/281.74 inference(scs_inference,[],[855,827,3])).
% 281.77/281.74 cnf(1060,plain,
% 281.77/281.74 (~E(f2(a1,f2(a3,a4)),f2(x10601,x10601))),
% 281.77/281.74 inference(scs_inference,[],[863,8,3])).
% 281.77/281.74 cnf(1062,plain,
% 281.77/281.74 (~E(f2(a1,f2(a3,a4)),f2(f2(x10621,x10622),x10621))),
% 281.77/281.74 inference(scs_inference,[],[863,9,3])).
% 281.77/281.74 cnf(1063,plain,
% 281.77/281.74 (~E(a1,f2(f2(a3,a4),x10631))),
% 281.77/281.74 inference(scs_inference,[],[863,9,3,4])).
% 281.77/281.74 cnf(1103,plain,
% 281.77/281.74 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x11031,x11032),x11031),a4))),
% 281.77/281.74 inference(scs_inference,[],[1060,106,3])).
% 281.77/281.74 cnf(1107,plain,
% 281.77/281.74 (~E(f2(a1,f2(a3,a4)),f2(x11071,a1))),
% 281.77/281.74 inference(scs_inference,[],[863,6,3])).
% 281.77/281.74 cnf(1109,plain,
% 281.77/281.74 (~E(f2(a1,f2(a3,a4)),f2(a4,x11091))),
% 281.77/281.74 inference(scs_inference,[],[863,7,3])).
% 281.77/281.74 cnf(1144,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(x11441,x11441),x11442),a4))),
% 281.77/281.74 inference(scs_inference,[],[907,120,3])).
% 281.77/281.74 cnf(1147,plain,
% 281.77/281.74 (~E(a1,f2(f2(x11471,x11471),x11472))),
% 281.77/281.74 inference(scs_inference,[],[907,120,3,4])).
% 281.77/281.74 cnf(1178,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(a4,x11781),x11782),f2(f2(x11783,x11784),x11783)))),
% 281.77/281.74 inference(scs_inference,[],[910,107,3])).
% 281.77/281.74 cnf(1181,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(a4,x11811),x11812),f2(x11813,x11813)))),
% 281.77/281.74 inference(scs_inference,[],[910,119,3])).
% 281.77/281.74 cnf(1187,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(a4,x11871),x11872))),
% 281.77/281.74 inference(scs_inference,[],[916,812,3])).
% 281.77/281.74 cnf(1190,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(x11901,x11902),x11901),x11903))),
% 281.77/281.74 inference(scs_inference,[],[916,105,3])).
% 281.77/281.74 cnf(1193,plain,
% 281.77/281.74 (~E(a1,f2(f2(x11931,f2(a4,x11932)),f2(x11931,a4)))),
% 281.77/281.74 inference(scs_inference,[],[923,817,3])).
% 281.77/281.74 cnf(1197,plain,
% 281.77/281.74 (~E(a1,f2(f2(x11971,a4),f2(x11971,f2(a4,x11972))))),
% 281.77/281.74 inference(scs_inference,[],[923,816,3])).
% 281.77/281.74 cnf(1206,plain,
% 281.77/281.74 (~E(a1,f2(f2(f2(x12061,x12062),a4),f2(f2(x12061,a4),x12062)))),
% 281.77/281.74 inference(scs_inference,[],[927,816,3])).
% 281.77/281.74 cnf(1211,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(f2(x12111,x12112),f2(a4,x12113)),f2(f2(x12111,a4),x12112)))),
% 281.77/281.74 inference(scs_inference,[],[933,817,3])).
% 281.77/281.74 cnf(1227,plain,
% 281.77/281.74 (~E(f2(a1,a4),f2(f2(x12271,f2(a4,x12272)),f2(x12271,f2(a4,x12273))))),
% 281.77/281.74 inference(scs_inference,[],[954,817,3])).
% 281.77/281.74 cnf(1250,plain,
% 281.77/281.74 (~E(a1,f2(f2(f2(x12501,x12501),x12502),f2(f2(x12503,x12504),x12503)))),
% 281.77/281.74 inference(scs_inference,[],[987,107,3])).
% 281.77/281.74 cnf(1261,plain,
% 281.77/281.74 (~E(f2(a3,f2(x12611,a1)),f2(f2(x12612,f2(a4,x12613)),f2(x12612,a4)))),
% 281.77/281.74 inference(scs_inference,[],[1033,817,3])).
% 281.77/281.74 cnf(1270,plain,
% 281.77/281.74 (~E(f2(a3,f2(x12701,a1)),f2(f2(f2(a4,x12702),x12703),a4))),
% 281.77/281.75 inference(scs_inference,[],[1035,854,3])).
% 281.77/281.75 cnf(1273,plain,
% 281.77/281.75 (~E(f2(a3,f2(x12731,a1)),f2(f2(f2(x12732,x12732),x12733),a4))),
% 281.77/281.75 inference(scs_inference,[],[1035,120,3])).
% 281.77/281.75 cnf(1303,plain,
% 281.77/281.75 (~E(f2(a3,f2(x13031,a1)),f2(f2(a4,x13032),x13033))),
% 281.77/281.75 inference(scs_inference,[],[1038,812,3])).
% 281.77/281.75 cnf(1306,plain,
% 281.77/281.75 (~E(f2(a3,f2(x13061,a1)),f2(f2(x13062,x13062),x13063))),
% 281.77/281.75 inference(scs_inference,[],[1038,102,3])).
% 281.77/281.75 cnf(1309,plain,
% 281.77/281.75 (~E(f2(a3,f2(x13091,a1)),f2(f2(f2(x13092,x13093),x13092),x13094))),
% 281.77/281.75 inference(scs_inference,[],[1038,105,3])).
% 281.77/281.75 cnf(1314,plain,
% 281.77/281.75 (~E(f2(a3,f2(x13141,a1)),f2(f2(f2(x13142,x13143),f2(a4,x13144)),f2(f2(x13142,a4),x13143)))),
% 281.77/281.75 inference(scs_inference,[],[1044,817,3])).
% 281.77/281.75 cnf(1319,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(x13191,f2(a4,x13192)),f2(x13191,a4)))),
% 281.77/281.75 inference(scs_inference,[],[1060,817,3])).
% 281.77/281.75 cnf(1322,plain,
% 281.77/281.75 (~E(a1,f2(a3,f2(a4,x13221)))),
% 281.77/281.75 inference(scs_inference,[],[1060,817,3,4])).
% 281.77/281.75 cnf(1328,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x13281,x13281),x13282),a4))),
% 281.77/281.75 inference(scs_inference,[],[1062,120,3])).
% 281.77/281.75 cnf(1408,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x14081,x14082),x14081),f2(x14083,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1103,85,3])).
% 281.77/281.75 cnf(1417,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(a4,x14171),x14172))),
% 281.77/281.75 inference(scs_inference,[],[1109,812,3])).
% 281.77/281.75 cnf(1429,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(x14291,x14291),x14292),f2(x14293,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1144,85,3])).
% 281.77/281.75 cnf(1432,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(x14321,x14321),x14322),f2(f2(x14323,x14324),x14323)))),
% 281.77/281.75 inference(scs_inference,[],[1144,107,3])).
% 281.77/281.75 cnf(1434,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(x14341,x14341),x14342),f2(x14343,x14343)))),
% 281.77/281.75 inference(scs_inference,[],[1144,119,3])).
% 281.77/281.75 cnf(1451,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(a4,x14511),f2(a4,x14512)),x14513))),
% 281.77/281.75 inference(scs_inference,[],[1190,817,3])).
% 281.77/281.75 cnf(1457,plain,
% 281.77/281.75 (~E(a1,f2(f2(x14571,f2(a4,x14572)),f2(x14571,f2(a4,x14573))))),
% 281.77/281.75 inference(scs_inference,[],[1197,817,3])).
% 281.77/281.75 cnf(1460,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(x14601,x14602),f2(a4,x14603)),f2(f2(x14601,a4),x14602)))),
% 281.77/281.75 inference(scs_inference,[],[1206,817,3])).
% 281.77/281.75 cnf(1464,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(x14641,f2(x14641,a4)),f2(a4,x14642)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1211,120,3])).
% 281.77/281.75 cnf(1467,plain,
% 281.77/281.75 (~E(a1,f2(f2(x14671,f2(x14671,a4)),f2(a4,x14672)))),
% 281.77/281.75 inference(scs_inference,[],[1211,120,3,4])).
% 281.77/281.75 cnf(1477,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(f2(a4,x14771),x14772),f2(a4,x14773)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1227,106,3])).
% 281.77/281.75 cnf(1500,plain,
% 281.77/281.75 (~E(a3,f2(f2(a4,x15001),x15002))),
% 281.77/281.75 inference(scs_inference,[],[1270,853,3,4])).
% 281.77/281.75 cnf(1502,plain,
% 281.77/281.75 (~E(f2(a3,f2(x15021,a1)),f2(f2(f2(x15022,f2(x15022,a4)),f2(a4,x15023)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1314,120,3])).
% 281.77/281.75 cnf(1508,plain,
% 281.77/281.75 (~E(a1,f2(a3,f2(f2(a4,x15081),x15082)))),
% 281.77/281.75 inference(scs_inference,[],[1322,827,3])).
% 281.77/281.75 cnf(1517,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x15171,x15171),x15172),f2(x15173,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1328,85,3])).
% 281.77/281.75 cnf(1563,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(a4,x15631),f2(a4,x15632)),f2(x15633,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1408,817,3])).
% 281.77/281.75 cnf(1567,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x15671),x15672),a4),f2(x15673,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1408,816,3])).
% 281.77/281.75 cnf(1599,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x15991),x15992),f2(a4,x15993)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1457,106,3])).
% 281.77/281.75 cnf(1603,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(x16031,f2(x16031,a4)),f2(a4,x16032)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1460,120,3])).
% 281.77/281.75 cnf(1607,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(x16071,f2(x16071,a4)),f2(a4,x16072)),f2(a4,x16073)))),
% 281.77/281.75 inference(scs_inference,[],[1464,853,3])).
% 281.77/281.75 cnf(1619,plain,
% 281.77/281.75 (~E(a1,f2(f2(x16191,f2(x16191,a4)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1467,854,3])).
% 281.77/281.75 cnf(1627,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(f2(a4,x16271),x16272),f2(a4,x16273)),f2(a4,x16274)))),
% 281.77/281.75 inference(scs_inference,[],[1477,853,3])).
% 281.77/281.75 cnf(1648,plain,
% 281.77/281.75 (~E(f2(a3,f2(x16481,a1)),f2(f2(f2(x16482,f2(x16482,a4)),f2(a4,x16483)),f2(a4,x16484)))),
% 281.77/281.75 inference(scs_inference,[],[1502,853,3])).
% 281.77/281.75 cnf(1676,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x16761),x16762),f2(a4,x16763)),f2(x16764,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1567,817,3])).
% 281.77/281.75 cnf(1695,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x16951),x16952),f2(a4,x16953)),f2(a4,x16954)))),
% 281.77/281.75 inference(scs_inference,[],[1599,853,3])).
% 281.77/281.75 cnf(1701,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x17011),x17012),f2(a4,x17013)),f2(x17014,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1599,85,3])).
% 281.77/281.75 cnf(1704,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x17041),x17042),f2(a4,x17043)),f2(x17044,x17044)))),
% 281.77/281.75 inference(scs_inference,[],[1599,119,3])).
% 281.77/281.75 cnf(1707,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(x17071,f2(x17071,a4)),f2(a4,x17072)),f2(a4,x17073)))),
% 281.77/281.75 inference(scs_inference,[],[1603,853,3])).
% 281.77/281.75 cnf(1713,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(x17131,f2(x17131,a4)),f2(a4,x17132)),f2(x17133,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1603,85,3])).
% 281.77/281.75 cnf(1722,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(x17221,f2(x17221,a4)),a4),f2(a4,x17222)))),
% 281.77/281.75 inference(scs_inference,[],[1607,816,3])).
% 281.77/281.75 cnf(1732,plain,
% 281.77/281.75 (~E(a1,f2(f2(x17321,f2(x17321,a4)),f2(f2(x17322,x17323),x17322)))),
% 281.77/281.75 inference(scs_inference,[],[1619,107,3])).
% 281.77/281.75 cnf(1735,plain,
% 281.77/281.75 (~E(a1,f2(f2(x17351,f2(x17351,a4)),f2(x17352,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1619,85,3])).
% 281.77/281.75 cnf(1746,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(f2(f2(a4,x17461),x17462),a4),f2(a4,x17463)))),
% 281.77/281.75 inference(scs_inference,[],[1627,816,3])).
% 281.77/281.75 cnf(1769,plain,
% 281.77/281.75 (~E(f2(a3,f2(x17691,a1)),f2(f2(f2(x17692,f2(x17692,a4)),a4),f2(a4,x17693)))),
% 281.77/281.75 inference(scs_inference,[],[1648,816,3])).
% 281.77/281.75 cnf(1772,plain,
% 281.77/281.75 (~E(a3,f2(f2(x17721,f2(x17721,a4)),a4))),
% 281.77/281.75 inference(scs_inference,[],[1769,4])).
% 281.77/281.75 cnf(1806,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x18061),x18062),a4),f2(a4,x18063)))),
% 281.77/281.75 inference(scs_inference,[],[1695,816,3])).
% 281.77/281.75 cnf(1810,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x18101),x18102),a4),f2(x18103,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1701,816,3])).
% 281.77/281.75 cnf(1814,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(f2(a4,x18141),x18142),a4),f2(x18143,x18143)))),
% 281.77/281.75 inference(scs_inference,[],[1704,816,3])).
% 281.77/281.75 cnf(1819,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(x18191,f2(x18191,a4)),a4),f2(a4,x18192)))),
% 281.77/281.75 inference(scs_inference,[],[1707,816,3])).
% 281.77/281.75 cnf(1824,plain,
% 281.77/281.75 (~E(a1,f2(f2(f2(x18241,f2(x18241,a4)),a4),f2(x18242,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1713,816,3])).
% 281.77/281.75 cnf(1861,plain,
% 281.77/281.75 (~E(a3,f2(f2(x18611,f2(x18611,a4)),f2(f2(x18612,x18613),x18612)))),
% 281.77/281.75 inference(scs_inference,[],[1772,107,3])).
% 281.77/281.75 cnf(1864,plain,
% 281.77/281.75 (~E(a3,f2(f2(x18641,f2(x18641,a4)),f2(x18642,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1772,85,3])).
% 281.77/281.75 cnf(1946,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,a4)),f2(f2(f2(x19461,a1),x19462),x19463))),
% 281.77/281.75 inference(scs_inference,[],[73,820,3])).
% 281.77/281.75 cnf(1952,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,a4)),f2(f2(x19521,f2(a4,x19522)),f2(x19521,a4)))),
% 281.77/281.75 inference(scs_inference,[],[80,817,3])).
% 281.77/281.75 cnf(1955,plain,
% 281.77/281.75 (~E(a3,f2(a3,f2(a4,x19551)))),
% 281.77/281.75 inference(scs_inference,[],[80,817,3,4])).
% 281.77/281.75 cnf(1957,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,a4)),f2(f2(x19571,a4),f2(x19571,f2(a4,x19572))))),
% 281.77/281.75 inference(scs_inference,[],[80,816,3])).
% 281.77/281.75 cnf(1963,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,a4)),f2(f2(a4,x19631),x19632))),
% 281.77/281.75 inference(scs_inference,[],[86,812,3])).
% 281.77/281.75 cnf(1993,plain,
% 281.77/281.75 (~E(a3,f2(f2(f2(x19931,a1),x19932),x19933))),
% 281.77/281.75 inference(scs_inference,[],[160,820,3])).
% 281.77/281.75 cnf(2002,plain,
% 281.77/281.75 (~E(a3,f2(f2(x20021,a4),f2(x20021,f2(a4,x20022))))),
% 281.77/281.75 inference(scs_inference,[],[165,816,3])).
% 281.77/281.75 cnf(2012,plain,
% 281.77/281.75 (~E(a3,f2(f2(f2(f2(a4,x20121),x20122),x20123),f2(a4,x20122)))),
% 281.77/281.75 inference(scs_inference,[],[177,826,3])).
% 281.77/281.75 cnf(2017,plain,
% 281.77/281.75 (~E(a3,f2(f2(f2(x20171,x20171),x20172),f2(a4,x20173)))),
% 281.77/281.75 inference(scs_inference,[],[180,853,3])).
% 281.77/281.75 cnf(2029,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,a4)),f2(f2(f2(x20291,x20291),x20292),f2(a4,x20293)))),
% 281.77/281.75 inference(scs_inference,[],[219,853,3])).
% 281.77/281.75 cnf(2081,plain,
% 281.77/281.75 (~E(f2(a1,a4),f2(f2(x20811,x20811),x20812))),
% 281.77/281.75 inference(scs_inference,[],[916,102,3])).
% 281.77/281.75 cnf(2101,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,a4)),f2(f2(x21011,a4),f2(x21011,f2(a4,x21012))))),
% 281.77/281.75 inference(scs_inference,[],[1060,816,3])).
% 281.77/281.75 cnf(2145,plain,
% 281.77/281.75 (~E(f2(a3,f2(x21451,a1)),f2(f2(f2(a4,x21452),x21453),f2(x21454,x21454)))),
% 281.77/281.75 inference(scs_inference,[],[1270,119,3])).
% 281.77/281.75 cnf(2152,plain,
% 281.77/281.75 (~E(f2(a3,f2(x21521,a1)),f2(f2(f2(x21522,x21522),x21523),f2(x21524,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1273,85,3])).
% 281.77/281.75 cnf(2155,plain,
% 281.77/281.75 (E(f2(x21551,f2(x21552,a1)),f2(x21551,f2(x21553,a1)))),
% 281.77/281.75 inference(scs_inference,[],[43,5])).
% 281.77/281.75 cnf(2156,plain,
% 281.77/281.75 (E(f2(f2(x21561,a1),x21562),f2(f2(x21563,a1),x21562))),
% 281.77/281.75 inference(scs_inference,[],[43,5,4])).
% 281.77/281.75 cnf(2157,plain,
% 281.77/281.75 (~E(f2(x21571,a1),f2(a1,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[1107,43,5,4,2])).
% 281.77/281.75 cnf(2160,plain,
% 281.77/281.75 (E(f2(x21601,f2(a4,x21602)),f2(x21601,f2(x21603,x21603)))),
% 281.77/281.75 inference(scs_inference,[],[19,5])).
% 281.77/281.75 cnf(2161,plain,
% 281.77/281.75 (E(f2(f2(a4,x21611),x21612),f2(f2(f2(a4,x21613),x21611),x21612))),
% 281.77/281.75 inference(scs_inference,[],[813,19,5,4])).
% 281.77/281.75 cnf(2163,plain,
% 281.77/281.75 (~E(f2(a3,a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[118,2081,813,19,7,5,4,2,12])).
% 281.77/281.75 cnf(2166,plain,
% 281.77/281.75 (~E(f2(f2(f2(x21661,a1),x21662),f2(x21663,a1)),a3)),
% 281.77/281.75 inference(scs_inference,[],[118,2081,831,2155,813,19,7,5,4,2,12,3])).
% 281.77/281.75 cnf(2170,plain,
% 281.77/281.75 (E(f2(x21701,f2(x21702,x21702)),f2(x21701,f2(x21703,a1)))),
% 281.77/281.75 inference(scs_inference,[],[25,5])).
% 281.77/281.75 cnf(2171,plain,
% 281.77/281.75 (E(f2(f2(x21711,x21711),x21712),f2(f2(x21713,a1),x21712))),
% 281.77/281.75 inference(scs_inference,[],[25,5,4])).
% 281.77/281.75 cnf(2172,plain,
% 281.77/281.75 (~E(a4,f2(a3,a4))),
% 281.77/281.75 inference(scs_inference,[],[2163,25,5,4,2])).
% 281.77/281.75 cnf(2173,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(x21731,x21731)),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2163,810,25,7,5,4,2,12])).
% 281.77/281.75 cnf(2180,plain,
% 281.77/281.75 (E(f2(x21801,f2(a4,x21802)),f2(x21801,f2(x21803,a1)))),
% 281.77/281.75 inference(scs_inference,[],[23,5])).
% 281.77/281.75 cnf(2181,plain,
% 281.77/281.75 (E(f2(f2(a4,x21811),x21812),f2(f2(x21813,a1),x21812))),
% 281.77/281.75 inference(scs_inference,[],[23,5,4])).
% 281.77/281.75 cnf(2182,plain,
% 281.77/281.75 (~E(f2(f2(a4,x21821),x21822),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[1187,23,5,4,2])).
% 281.77/281.75 cnf(2183,plain,
% 281.77/281.75 (~E(f2(f2(a3,a4),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2172,1187,23,7,5,4,2,12])).
% 281.77/281.75 cnf(2190,plain,
% 281.77/281.75 (E(f2(x21901,f2(f2(x21902,a1),f2(x21903,a1))),f2(x21901,f2(x21904,x21904)))),
% 281.77/281.75 inference(scs_inference,[],[72,5])).
% 281.77/281.75 cnf(2192,plain,
% 281.77/281.75 (~E(a4,f2(f2(a3,a4),a4))),
% 281.77/281.75 inference(scs_inference,[],[2183,72,5,4,2])).
% 281.77/281.75 cnf(2193,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(x21931,a1)),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2183,787,72,7,5,4,2,12])).
% 281.77/281.75 cnf(2196,plain,
% 281.77/281.75 (~E(f2(x21961,x21961),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[2182,2183,787,72,7,5,4,2,12,3])).
% 281.77/281.75 cnf(2199,plain,
% 281.77/281.75 (E(f2(x21991,f2(f2(x21992,a1),x21993)),f2(x21991,f2(x21992,a1)))),
% 281.77/281.75 inference(scs_inference,[],[65,5])).
% 281.77/281.75 cnf(2200,plain,
% 281.77/281.75 (E(f2(f2(f2(x22001,a1),x22002),x22003),f2(f2(a4,x22002),x22003))),
% 281.77/281.75 inference(scs_inference,[],[65,46,5,4])).
% 281.77/281.75 cnf(2201,plain,
% 281.77/281.75 (~E(f2(f2(x22011,x22011),x22012),a1)),
% 281.77/281.75 inference(scs_inference,[],[1147,65,46,5,4,2])).
% 281.77/281.75 cnf(2202,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(a1,a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2196,1147,65,46,50,5,4,2,12])).
% 281.77/281.75 cnf(2204,plain,
% 281.77/281.75 (~E(f2(x22041,x22041),f2(a1,a4))),
% 281.77/281.75 inference(rename_variables,[],[2196])).
% 281.77/281.75 cnf(2206,plain,
% 281.77/281.75 (~E(f2(f2(x22061,a1),f2(x22062,x22062)),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[2196,2204,1147,2171,65,46,50,5,4,2,12,3])).
% 281.77/281.75 cnf(2210,plain,
% 281.77/281.75 (E(f2(x22101,f2(x22102,x22102)),f2(x22101,f2(f2(x22103,a1),f2(x22104,a1))))),
% 281.77/281.75 inference(scs_inference,[],[62,5])).
% 281.77/281.75 cnf(2211,plain,
% 281.77/281.75 (E(f2(f2(x22111,x22111),x22112),f2(f2(f2(x22113,a1),f2(x22114,a1)),x22112))),
% 281.77/281.75 inference(scs_inference,[],[62,5,4])).
% 281.77/281.75 cnf(2212,plain,
% 281.77/281.75 (~E(a4,f2(f2(a1,a4),f2(a1,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2202,62,5,4,2])).
% 281.77/281.75 cnf(2213,plain,
% 281.77/281.75 (~E(f2(f2(f2(a3,a4),a4),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2192,2202,62,7,5,4,2,12])).
% 281.77/281.75 cnf(2216,plain,
% 281.77/281.75 (~E(f2(f2(x22161,a1),f2(x22162,a1)),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[2206,2192,2202,2170,62,7,5,4,2,12,3])).
% 281.77/281.75 cnf(2219,plain,
% 281.77/281.75 (E(f2(x22191,f2(a4,x22192)),f2(x22191,f2(f2(x22193,x22193),x22192)))),
% 281.77/281.75 inference(scs_inference,[],[101,5])).
% 281.77/281.75 cnf(2220,plain,
% 281.77/281.75 (E(f2(f2(a4,x22201),x22202),f2(f2(f2(x22203,x22203),x22201),x22202))),
% 281.77/281.75 inference(scs_inference,[],[101,5,4])).
% 281.77/281.75 cnf(2225,plain,
% 281.77/281.75 (~E(f2(f2(x22251,a1),f2(f2(x22252,a1),f2(x22253,a1))),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[2216,2212,913,2210,101,7,5,4,2,12,3])).
% 281.77/281.75 cnf(2231,plain,
% 281.77/281.75 (~E(f2(f2(a4,x22311),x22312),a3)),
% 281.77/281.75 inference(scs_inference,[],[1500,42,5,4,2])).
% 281.77/281.75 cnf(2232,plain,
% 281.77/281.75 (~E(f2(f2(x22321,x22322),x22321),f2(a1,f2(f2(x22323,x22324),x22323)))),
% 281.77/281.75 inference(scs_inference,[],[1500,797,42,32,5,4,2,3])).
% 281.77/281.75 cnf(2234,plain,
% 281.77/281.75 (E(f2(x22341,f2(x22342,x22342)),f2(x22341,f2(a4,x22343)))),
% 281.77/281.75 inference(scs_inference,[],[18,5])).
% 281.77/281.75 cnf(2235,plain,
% 281.77/281.75 (E(f2(f2(x22351,x22351),x22352),f2(f2(a4,x22353),x22352))),
% 281.77/281.75 inference(scs_inference,[],[18,5,4])).
% 281.77/281.75 cnf(2236,plain,
% 281.77/281.75 (~E(f2(a3,f2(x22361,x22361)),a3)),
% 281.77/281.75 inference(scs_inference,[],[194,18,5,4,2])).
% 281.77/281.75 cnf(2240,plain,
% 281.77/281.75 (E(f2(x22401,f2(x22402,a1)),f2(x22401,f2(x22403,x22403)))),
% 281.77/281.75 inference(scs_inference,[],[24,5])).
% 281.77/281.75 cnf(2241,plain,
% 281.77/281.75 (E(f2(f2(a4,x22411),x22412),f2(f2(x22413,x22413),x22412))),
% 281.77/281.75 inference(scs_inference,[],[19,24,5,4])).
% 281.77/281.75 cnf(2242,plain,
% 281.77/281.75 (~E(f2(a3,f2(x22421,a1)),a3)),
% 281.77/281.75 inference(scs_inference,[],[91,19,24,5,4,2])).
% 281.77/281.75 cnf(2243,plain,
% 281.77/281.75 (~E(f2(a1,f2(x22431,a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[844,91,19,24,50,5,4,2,12])).
% 281.77/281.75 cnf(2250,plain,
% 281.77/281.75 (E(f2(x22501,f2(x22502,a1)),f2(x22501,f2(a4,x22503)))),
% 281.77/281.75 inference(scs_inference,[],[20,5])).
% 281.77/281.75 cnf(2251,plain,
% 281.77/281.75 (E(f2(f2(x22511,a1),x22512),f2(f2(a4,x22513),x22512))),
% 281.77/281.75 inference(scs_inference,[],[20,5,4])).
% 281.77/281.75 cnf(2252,plain,
% 281.77/281.75 (~E(f2(a3,f2(x22521,a1)),a1)),
% 281.77/281.75 inference(scs_inference,[],[242,20,5,4,2])).
% 281.77/281.75 cnf(2257,plain,
% 281.77/281.75 (E(f2(x22571,f2(f2(x22572,x22573),x22572)),f2(x22571,f2(x22574,a1)))),
% 281.77/281.75 inference(scs_inference,[],[40,5])).
% 281.77/281.75 cnf(2258,plain,
% 281.77/281.75 (E(f2(f2(f2(x22581,x22582),x22581),x22583),f2(f2(x22584,a1),x22583))),
% 281.77/281.75 inference(scs_inference,[],[40,5,4])).
% 281.77/281.75 cnf(2259,plain,
% 281.77/281.75 (~E(f2(a3,f2(a4,x22591)),a3)),
% 281.77/281.75 inference(scs_inference,[],[1955,40,5,4,2])).
% 281.77/281.75 cnf(2267,plain,
% 281.77/281.75 (E(f2(x22671,f2(f2(x22672,a1),x22673)),f2(x22671,f2(a4,x22673)))),
% 281.77/281.75 inference(scs_inference,[],[46,5])).
% 281.77/281.75 cnf(2268,plain,
% 281.77/281.75 (E(f2(a4,x22681),f2(f2(f2(x22682,a1),x22683),x22681))),
% 281.77/281.75 inference(scs_inference,[],[46,47,5,4])).
% 281.77/281.75 cnf(2270,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(a3,a4)),f2(x22701,a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2157,1434,46,47,50,5,4,2,12])).
% 281.77/281.75 cnf(2276,plain,
% 281.77/281.75 (E(f2(x22761,f2(a4,x22762)),f2(x22761,f2(f2(x22763,a1),x22762)))),
% 281.77/281.75 inference(scs_inference,[],[45,5])).
% 281.77/281.75 cnf(2277,plain,
% 281.77/281.75 (E(f2(f2(x22771,a1),x22772),f2(f2(x22773,x22773),x22772))),
% 281.77/281.75 inference(scs_inference,[],[24,45,5,4])).
% 281.77/281.75 cnf(2279,plain,
% 281.77/281.75 (~E(f2(f2(x22791,a1),x22792),a1)),
% 281.77/281.75 inference(scs_inference,[],[2201,1181,2181,24,45,5,4,2,3])).
% 281.77/281.75 cnf(2283,plain,
% 281.77/281.75 (E(f2(x22831,a4),f2(x22831,f2(f2(x22832,a1),x22833)))),
% 281.77/281.75 inference(scs_inference,[],[47,5])).
% 281.77/281.75 cnf(2284,plain,
% 281.77/281.75 (E(f2(f2(x22841,x22841),x22842),f2(f2(x22843,x22843),x22842))),
% 281.77/281.75 inference(scs_inference,[],[47,33,5,4])).
% 281.77/281.75 cnf(2285,plain,
% 281.77/281.75 (~E(f2(f2(f2(x22851,x22851),x22852),f2(x22853,a1)),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[1429,47,33,5,4,2])).
% 281.77/281.75 cnf(2289,plain,
% 281.77/281.75 (E(f2(x22891,f2(x22892,x22892)),f2(x22891,f2(x22893,x22893)))),
% 281.77/281.75 inference(scs_inference,[],[33,5])).
% 281.77/281.75 cnf(2296,plain,
% 281.77/281.75 (E(f2(f2(f2(a4,x22961),x22962),x22963),f2(f2(a4,x22962),x22963))),
% 281.77/281.75 inference(scs_inference,[],[812,102,5,4])).
% 281.77/281.75 cnf(2309,plain,
% 281.77/281.75 (E(f2(f2(x23091,a4),x23092),f2(f2(x23091,f2(x23093,a1)),x23092))),
% 281.77/281.75 inference(scs_inference,[],[49,854,5,4])).
% 281.77/281.75 cnf(2310,plain,
% 281.77/281.75 (~E(f2(f2(a4,x23101),x23102),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[1963,49,854,5,4,2])).
% 281.77/281.75 cnf(2311,plain,
% 281.77/281.75 (~E(f2(a3,f2(f2(x23111,a1),x23112)),a1)),
% 281.77/281.75 inference(scs_inference,[],[67,1963,2283,49,854,5,4,2,3])).
% 281.77/281.75 cnf(2315,plain,
% 281.77/281.75 (E(f2(f2(x23151,a4),x23152),f2(f2(x23151,f2(x23153,x23153)),x23152))),
% 281.77/281.75 inference(scs_inference,[],[120,5,4])).
% 281.77/281.75 cnf(2324,plain,
% 281.77/281.75 (E(f2(x23241,f2(x23242,a1)),f2(x23241,f2(f2(x23242,a1),x23243)))),
% 281.77/281.75 inference(scs_inference,[],[58,5])).
% 281.77/281.75 cnf(2325,plain,
% 281.77/281.75 (E(f2(f2(x23251,f2(x23252,x23252)),x23253),f2(f2(x23251,a4),x23253))),
% 281.77/281.75 inference(scs_inference,[],[58,119,5,4])).
% 281.77/281.75 cnf(2327,plain,
% 281.77/281.75 (~E(f2(a1,f2(f2(x23271,a1),x23272)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2279,1417,58,119,6,5,4,2,12])).
% 281.77/281.75 cnf(2333,plain,
% 281.77/281.75 (E(f2(x23331,f2(x23332,f2(x23333,x23333))),f2(x23331,f2(x23332,a4)))),
% 281.77/281.75 inference(scs_inference,[],[119,5])).
% 281.77/281.75 cnf(2334,plain,
% 281.77/281.75 (E(f2(f2(x23341,f2(x23342,a1)),x23343),f2(f2(x23341,a4),x23343))),
% 281.77/281.75 inference(scs_inference,[],[119,85,5,4])).
% 281.77/281.75 cnf(2336,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,f2(a4,x23361))),a4)),
% 281.77/281.75 inference(scs_inference,[],[862,1306,119,6,85,5,4,2,12])).
% 281.77/281.75 cnf(2339,plain,
% 281.77/281.75 (~E(f2(f2(f2(a4,x23391),x23392),x23393),a3)),
% 281.77/281.75 inference(scs_inference,[],[2231,862,1306,2161,119,6,85,5,4,2,12,3])).
% 281.77/281.75 cnf(2344,plain,
% 281.77/281.75 (~E(f2(f2(a4,x23441),x23442),f2(a3,f2(x23443,a1)))),
% 281.77/281.75 inference(scs_inference,[],[1303,853,50,5,4,2])).
% 281.77/281.75 cnf(2345,plain,
% 281.77/281.75 (~E(f2(a1,f2(a3,f2(x23451,a1))),a4)),
% 281.77/281.75 inference(scs_inference,[],[2252,1303,6,853,50,5,4,2,12])).
% 281.77/281.75 cnf(2352,plain,
% 281.77/281.75 (E(f2(x23521,f2(x23522,f2(x23523,a1))),f2(x23521,f2(x23522,a4)))),
% 281.77/281.75 inference(scs_inference,[],[85,5])).
% 281.77/281.75 cnf(2383,plain,
% 281.77/281.75 (~E(f2(f2(f2(x23831,x23831),x23832),f2(a4,x23833)),a3)),
% 281.77/281.75 inference(scs_inference,[],[2017,2])).
% 281.77/281.75 cnf(2390,plain,
% 281.77/281.75 (~E(a4,f2(f2(a1,f2(a3,a4)),f2(x23901,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2270,2])).
% 281.77/281.75 cnf(2391,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,f2(x23911,x23911))),a4)),
% 281.77/281.75 inference(scs_inference,[],[2236,2270,9,2,12])).
% 281.77/281.75 cnf(2399,plain,
% 281.77/281.75 (~E(f2(f2(a3,f2(a3,a4)),f2(f2(a4,x23991),a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2310,1193,50,2,12])).
% 281.77/281.75 cnf(2407,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,f2(x24071,a1))),a4)),
% 281.77/281.75 inference(scs_inference,[],[2242,1735,9,2,12])).
% 281.77/281.75 cnf(2410,plain,
% 281.77/281.75 (~E(f2(x24101,a1),f2(f2(a1,f2(a3,a4)),f2(x24102,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2242,2390,1735,35,9,2,12,3])).
% 281.77/281.75 cnf(2412,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(a3,a4)),f2(x24121,a1)),f2(x24122,a1))),
% 281.77/281.75 inference(scs_inference,[],[2410,2])).
% 281.77/281.75 cnf(2421,plain,
% 281.77/281.75 (~E(f2(a3,f2(a3,f2(a4,x24211))),a4)),
% 281.77/281.75 inference(scs_inference,[],[2259,1864,9,2,12])).
% 281.77/281.75 cnf(2435,plain,
% 281.77/281.75 (~E(f2(f2(f2(x24351,x24351),x24352),f2(x24353,a1)),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[303,2])).
% 281.77/281.75 cnf(2449,plain,
% 281.77/281.75 (~E(f2(f2(x24491,a1),f2(a4,x24492)),a3)),
% 281.77/281.75 inference(scs_inference,[],[2383,2029,2258,2,3])).
% 281.77/281.75 cnf(2453,plain,
% 281.77/281.75 (~E(f2(f2(x24531,f2(a4,x24532)),f2(x24531,a4)),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[1952,2])).
% 281.77/281.75 cnf(2454,plain,
% 281.77/281.75 (~E(f2(f2(x24541,a1),f2(f2(x24542,x24542),x24543)),a3)),
% 281.77/281.75 inference(scs_inference,[],[2449,1952,2219,2,3])).
% 281.77/281.75 cnf(2465,plain,
% 281.77/281.75 (~E(f2(a4,a1),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[2285,1517,840,2,3])).
% 281.77/281.75 cnf(2469,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(a4,a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2465,1319,50,2,12])).
% 281.77/281.75 cnf(2474,plain,
% 281.77/281.75 (~E(a4,f2(f2(a1,a4),f2(a4,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2469,2])).
% 281.77/281.75 cnf(2478,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(f2(a4,a1),x24781)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2469,2324,7,2,12,3])).
% 281.77/281.75 cnf(2480,plain,
% 281.77/281.75 (~E(f2(f2(f2(a4,x24801),f2(a4,x24802)),f2(x24803,a1)),f2(a1,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[1563,2])).
% 281.77/281.75 cnf(2481,plain,
% 281.77/281.75 (~E(f2(f2(x24811,x24812),x24811),f2(f2(a1,a4),f2(a4,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2474,1563,32,2,3])).
% 281.77/281.75 cnf(2482,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(a4,a1)),f2(f2(x24821,x24822),x24821))),
% 281.77/281.75 inference(scs_inference,[],[2481,2])).
% 281.77/281.75 cnf(2492,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(a4,a1)),f2(f2(x24921,x24922),x24921))),
% 281.77/281.75 inference(rename_variables,[],[2482])).
% 281.77/281.75 cnf(2495,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(f2(x24951,a1),a1)),f2(f2(x24952,x24953),x24952))),
% 281.77/281.75 inference(scs_inference,[],[2482,2492,2145,2276,9,2,12,3])).
% 281.77/281.75 cnf(2498,plain,
% 281.77/281.75 (~E(f2(x24981,a1),f2(a1,a4))),
% 281.77/281.75 inference(scs_inference,[],[2225,2152,79,2,3])).
% 281.77/281.75 cnf(2506,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(x25061,a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2498,1261,50,2,12])).
% 281.77/281.75 cnf(2509,plain,
% 281.77/281.75 (~E(f2(a1,f2(x25091,x25091)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2498,2243,1261,2289,50,2,12,3])).
% 281.77/281.75 cnf(2513,plain,
% 281.77/281.75 (~E(f2(f2(f2(a1,a4),f2(x25131,a1)),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2506,7,2,12])).
% 281.77/281.75 cnf(2530,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(a3,a4)),f2(x25301,x25301)),f2(x25302,a1))),
% 281.77/281.75 inference(scs_inference,[],[2412,2344,1451,2160,50,2,12,3])).
% 281.77/281.75 cnf(2533,plain,
% 281.77/281.75 (~E(f2(x25331,a1),f2(f2(a1,f2(a3,a4)),f2(x25332,x25332)))),
% 281.77/281.75 inference(scs_inference,[],[2530,2])).
% 281.77/281.75 cnf(2541,plain,
% 281.77/281.75 (~E(a4,f2(f2(a1,a4),f2(f2(a4,a1),x25411)))),
% 281.77/281.75 inference(scs_inference,[],[2478,2])).
% 281.77/281.75 cnf(2542,plain,
% 281.77/281.75 (~E(f2(f2(f2(a1,f2(a3,a4)),f2(x25421,x25421)),f2(x25422,a1)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2533,2478,50,2,12])).
% 281.77/281.75 cnf(2548,plain,
% 281.77/281.75 (~E(a4,f2(f2(f2(a1,f2(a3,a4)),f2(x25481,x25481)),f2(x25482,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2542,2])).
% 281.77/281.75 cnf(2552,plain,
% 281.77/281.75 (~E(f2(a1,f2(a4,x25521)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2509,2542,2234,7,2,12,3])).
% 281.77/281.75 cnf(2555,plain,
% 281.77/281.75 (~E(f2(f2(f2(a3,a4),f2(x25551,a1)),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[1024,2213,2309,2,3])).
% 281.77/281.75 cnf(2557,plain,
% 281.77/281.75 (~E(f2(f2(f2(x25571,a1),x25572),x25573),a3)),
% 281.77/281.75 inference(scs_inference,[],[1993,2])).
% 281.77/281.75 cnf(2561,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(a4,x25611)),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2552,2166,1993,2156,7,2,3,12])).
% 281.77/281.75 cnf(2565,plain,
% 281.77/281.75 (~E(f2(f2(f2(a1,a4),a4),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[2339,2513,2325,2,3])).
% 281.77/281.75 cnf(2568,plain,
% 281.77/281.75 (~E(a4,f2(f2(f2(a1,a4),a4),a4))),
% 281.77/281.75 inference(scs_inference,[],[2565,2])).
% 281.77/281.75 cnf(2587,plain,
% 281.77/281.75 (~E(f2(f2(x25871,a4),f2(x25871,f2(a4,x25872))),a3)),
% 281.77/281.75 inference(scs_inference,[],[2002,2])).
% 281.77/281.75 cnf(2600,plain,
% 281.77/281.75 (~E(f2(a3,f2(f2(x26001,x26002),x26001)),a1)),
% 281.77/281.75 inference(scs_inference,[],[113,2])).
% 281.77/281.75 cnf(2601,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),a4),a4)),
% 281.77/281.75 inference(scs_inference,[],[113,2173,2334,2,3])).
% 281.77/281.75 cnf(2604,plain,
% 281.77/281.75 (~E(a4,f2(f2(a1,a4),a4))),
% 281.77/281.75 inference(scs_inference,[],[2601,2])).
% 281.77/281.75 cnf(2609,plain,
% 281.77/281.75 (~E(f2(f2(f2(x26091,x26092),f2(x26093,x26092)),f2(f2(x26091,x26093),x26092)),f2(f2(a1,a4),a4))),
% 281.77/281.75 inference(scs_inference,[],[2604,1508,30,2,3])).
% 281.77/281.75 cnf(2617,plain,
% 281.77/281.75 (~E(f2(x26171,a1),f2(f2(f2(a1,f2(a3,a4)),f2(x26172,x26172)),f2(x26173,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2548,2311,35,2,3])).
% 281.77/281.75 cnf(2618,plain,
% 281.77/281.75 (~E(f2(f2(f2(a1,f2(a3,a4)),f2(x26181,x26181)),f2(x26182,a1)),f2(x26183,a1))),
% 281.77/281.75 inference(scs_inference,[],[2617,2])).
% 281.77/281.75 cnf(2619,plain,
% 281.77/281.75 (~E(f2(f2(x26191,x26191),f2(a4,a4)),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[2453,2617,2241,2,3])).
% 281.77/281.75 cnf(2622,plain,
% 281.77/281.75 (~E(a4,f2(a1,f2(f2(x26221,a1),x26222)))),
% 281.77/281.75 inference(scs_inference,[],[2327,2])).
% 281.77/281.75 cnf(2623,plain,
% 281.77/281.75 (~E(f2(f2(x26231,x26232),x26231),f2(f2(f2(a1,a4),a4),a4))),
% 281.77/281.75 inference(scs_inference,[],[2568,2327,32,2,3])).
% 281.77/281.75 cnf(2624,plain,
% 281.77/281.75 (~E(a4,f2(f2(f2(a3,a4),f2(x26241,a1)),a4))),
% 281.77/281.75 inference(scs_inference,[],[2555,2])).
% 281.77/281.75 cnf(2625,plain,
% 281.77/281.75 (~E(f2(f2(x26251,x26251),f2(x26252,a1)),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[2619,2555,2180,2,3])).
% 281.77/281.75 cnf(2630,plain,
% 281.77/281.75 (~E(a4,f2(a3,f2(a3,f2(x26301,x26301))))),
% 281.77/281.75 inference(scs_inference,[],[2391,2])).
% 281.77/281.75 cnf(2631,plain,
% 281.77/281.75 (~E(f2(f2(a1,f2(x26311,a1)),f2(f2(x26312,a1),x26313)),a4)),
% 281.77/281.75 inference(scs_inference,[],[2391,2193,2283,2,3])).
% 281.77/281.75 cnf(2633,plain,
% 281.77/281.75 (~E(a4,f2(a1,f2(a3,f2(a4,x26331))))),
% 281.77/281.75 inference(scs_inference,[],[2336,2])).
% 281.77/281.75 cnf(2634,plain,
% 281.77/281.75 (~E(f2(f2(x26341,a1),f2(x26342,a1)),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[2625,2336,2181,2,3])).
% 281.77/281.75 cnf(2637,plain,
% 281.77/281.75 (~E(a4,f2(a1,f2(a3,f2(x26371,a1))))),
% 281.77/281.75 inference(scs_inference,[],[2345,2])).
% 281.77/281.75 cnf(2638,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(x26381,a1)),f2(f2(x26382,x26383),x26382))),
% 281.77/281.75 inference(scs_inference,[],[2345,2495,2155,2,3])).
% 281.77/281.75 cnf(2640,plain,
% 281.77/281.75 (~E(f2(f2(x26401,x26402),x26401),f2(f2(a1,a4),f2(x26403,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2638,2])).
% 281.77/281.75 cnf(2641,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(f2(x26411,a1),f2(x26412,a1))),f2(f2(x26413,x26414),x26413))),
% 281.77/281.75 inference(scs_inference,[],[2638,2210,2,3])).
% 281.77/281.75 cnf(2649,plain,
% 281.77/281.75 (~E(a4,f2(a3,f2(a3,f2(x26491,a1))))),
% 281.77/281.75 inference(scs_inference,[],[2407,2])).
% 281.77/281.75 cnf(2652,plain,
% 281.77/281.75 (~E(f2(f2(x26521,x26522),x26521),f2(f2(a1,a4),f2(x26523,a1)))),
% 281.77/281.75 inference(rename_variables,[],[2640])).
% 281.77/281.75 cnf(2654,plain,
% 281.77/281.75 (~E(f2(f2(a4,x26541),f2(x26542,a1)),f2(f2(a1,a4),f2(x26543,a1)))),
% 281.77/281.75 inference(scs_inference,[],[2640,2652,2407,2200,50,2,12,3])).
% 281.77/281.75 cnf(2658,plain,
% 281.77/281.75 (~E(f2(f2(a1,a4),f2(f2(a1,a4),f2(a1,a4))),a4)),
% 281.77/281.75 inference(scs_inference,[],[2654,2196,9,2,12])).
% 281.77/281.75 cnf(2662,plain,
% 281.77/281.75 (~E(f2(f2(f2(x26621,a1),f2(x26622,a1)),f2(x26623,a1)),f2(a3,f2(a3,a4)))),
% 281.77/281.75 inference(scs_inference,[],[2634,2654,2196,2211,9,2,12,3])).
% 281.77/281.75 cnf(2666,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x26661,x26661)),f2(f2(a1,a4),f2(a1,a4))),a4)),
% 281.77/281.76 inference(scs_inference,[],[2658,2315,2,3])).
% 281.77/281.76 cnf(2668,plain,
% 281.77/281.76 (~E(a4,f2(a3,f2(a3,f2(a4,x26681))))),
% 281.77/281.76 inference(scs_inference,[],[2421,2])).
% 281.77/281.76 cnf(2671,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(a4,x26711)),a4))),
% 281.77/281.76 inference(scs_inference,[],[2561,2])).
% 281.77/281.76 cnf(2672,plain,
% 281.77/281.76 (~E(f2(f2(a4,x26721),f2(a4,x26722)),f2(f2(f2(a1,a4),a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[2561,2296,2623,2,3])).
% 281.77/281.76 cnf(2675,plain,
% 281.77/281.76 (~E(f2(f2(x26751,x26752),x26751),f2(f2(a1,a4),f2(f2(x26753,a1),f2(x26754,a1))))),
% 281.77/281.76 inference(scs_inference,[],[2641,2])).
% 281.77/281.76 cnf(2709,plain,
% 281.77/281.76 (~E(f2(f2(a4,x27091),x27092),f2(f2(a1,a4),f2(f2(x27093,a1),f2(x27094,a1))))),
% 281.77/281.76 inference(scs_inference,[],[1722,2675,2235,2,3])).
% 281.77/281.76 cnf(2713,plain,
% 281.77/281.76 (~E(f2(f2(f2(x27131,x27131),x27132),a1),f2(a3,f2(a3,a4)))),
% 281.77/281.76 inference(scs_inference,[],[2435,1746,57,2,3])).
% 281.77/281.76 cnf(2729,plain,
% 281.77/281.76 (~E(f2(f2(a4,x27291),x27292),f2(a1,f2(f2(x27293,x27294),x27293)))),
% 281.77/281.76 inference(scs_inference,[],[1676,2232,2251,2,3])).
% 281.77/281.76 cnf(2765,plain,
% 281.77/281.76 (~E(f2(a4,x27651),f2(a1,f2(a3,a4)))),
% 281.77/281.76 inference(scs_inference,[],[2480,1814,26,2,3])).
% 281.77/281.76 cnf(2772,plain,
% 281.77/281.76 (~E(f2(f2(x27721,a4),f2(x27721,a4)),a3)),
% 281.77/281.76 inference(scs_inference,[],[2587,2012,2333,2,3])).
% 281.77/281.76 cnf(2776,plain,
% 281.77/281.76 (~E(f2(f2(x27761,f2(x27762,x27762)),f2(x27761,a4)),a3)),
% 281.77/281.76 inference(scs_inference,[],[2772,1819,2315,2,3])).
% 281.77/281.76 cnf(2779,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x27791,x27791)),f2(x27792,x27792)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2776,2666,2289,2,3])).
% 281.77/281.76 cnf(2781,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(x27811,x27811)),f2(x27812,x27812)))),
% 281.77/281.76 inference(scs_inference,[],[2779,2])).
% 281.77/281.76 cnf(2782,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(x27821,x27821)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2779,2325,2,3])).
% 281.77/281.76 cnf(2787,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,a4),f2(x27871,x27871)))),
% 281.77/281.76 inference(scs_inference,[],[2782,2])).
% 281.77/281.76 cnf(2791,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(a4,f2(x27911,a1))),a4)),
% 281.77/281.76 inference(scs_inference,[],[2782,2781,2267,7,2,12,3])).
% 281.77/281.76 cnf(2794,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,a4),f2(a4,f2(x27941,a1))))),
% 281.77/281.76 inference(scs_inference,[],[2791,2])).
% 281.77/281.76 cnf(2795,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),f2(x27951,x27951)),a4),a4)),
% 281.77/281.76 inference(scs_inference,[],[2787,2791,7,2,12])).
% 281.77/281.76 cnf(2802,plain,
% 281.77/281.76 (~E(a4,f2(f2(f2(a1,a4),f2(x28021,x28021)),a4))),
% 281.77/281.76 inference(scs_inference,[],[2795,2])).
% 281.77/281.76 cnf(2803,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),f2(x28031,x28031)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2795,2399,2240,2,3])).
% 281.77/281.76 cnf(2806,plain,
% 281.77/281.76 (~E(f2(f2(f2(x28061,a1),x28062),x28063),f2(a1,f2(a3,a4)))),
% 281.77/281.76 inference(scs_inference,[],[2765,2803,2268,2,3])).
% 281.77/281.76 cnf(2809,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x28091,a1)),f2(x28092,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[1824,2631,2257,2,3])).
% 281.77/281.76 cnf(2815,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(x28151,a1)),f2(x28152,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2809,2])).
% 281.77/281.76 cnf(2827,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,f2(a3,a4)),f2(x28271,x28271)),f2(a4,x28272)),f2(x28273,a1))),
% 281.77/281.76 inference(scs_inference,[],[2618,1806,2234,2,3])).
% 281.77/281.76 cnf(2833,plain,
% 281.77/281.76 (~E(f2(x28331,a1),f2(f2(f2(a1,f2(a3,a4)),f2(x28332,x28332)),f2(a4,x28333)))),
% 281.77/281.76 inference(scs_inference,[],[2827,2])).
% 281.77/281.76 cnf(2834,plain,
% 281.77/281.76 (~E(a4,f2(a1,f2(a3,a4)))),
% 281.77/281.76 inference(scs_inference,[],[6,2827,2806,2,3])).
% 281.77/281.76 cnf(2841,plain,
% 281.77/281.76 (~E(a4,f2(f2(f2(a1,f2(a3,a4)),f2(x28411,x28411)),f2(a4,x28412)))),
% 281.77/281.76 inference(scs_inference,[],[6,2833,1810,2,3])).
% 281.77/281.76 cnf(2843,plain,
% 281.77/281.76 (~E(f2(f2(f2(f2(a1,f2(a3,a4)),f2(x28431,x28431)),f2(a4,x28432)),f2(x28433,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[6,2833,1810,50,2,3,12])).
% 281.77/281.76 cnf(2847,plain,
% 281.77/281.76 (~E(a4,f2(a3,f2(a3,a4)))),
% 281.77/281.76 inference(scs_inference,[],[6,2841,2713,2,3])).
% 281.77/281.76 cnf(2849,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(a3,a4)),a4),a4)),
% 281.77/281.76 inference(scs_inference,[],[6,2834,2841,2713,7,2,3,12])).
% 281.77/281.76 cnf(2852,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(a3,a4)),a4))),
% 281.77/281.76 inference(scs_inference,[],[2849,2])).
% 281.77/281.76 cnf(2855,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),a4),a4)),
% 281.77/281.76 inference(scs_inference,[],[2847,2662,2849,2250,7,2,3,12])).
% 281.77/281.76 cnf(2858,plain,
% 281.77/281.76 (~E(a4,f2(f2(a3,f2(a3,a4)),a4))),
% 281.77/281.76 inference(scs_inference,[],[2855,2])).
% 281.77/281.76 cnf(2859,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),f2(f2(x28591,a1),x28592)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2855,2283,2,3])).
% 281.77/281.76 cnf(2864,plain,
% 281.77/281.76 (~E(a4,f2(f2(f2(f2(a1,f2(a3,a4)),f2(x28641,x28641)),f2(a4,x28642)),f2(x28643,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2843,2])).
% 281.77/281.76 cnf(2871,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,a4),f2(f2(x28711,a1),f2(x28712,a1))))),
% 281.77/281.76 inference(scs_inference,[],[6,1432,2709,2,3])).
% 281.77/281.76 cnf(2874,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x28741,a1),f2(x28742,a1))),a4)),
% 281.77/281.76 inference(scs_inference,[],[2871,2])).
% 281.77/281.76 cnf(2879,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x28791,a1),a4)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2874,1178,2352,2,3])).
% 281.77/281.76 cnf(2883,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,a4),f2(f2(x28831,a1),a4)))),
% 281.77/281.76 inference(scs_inference,[],[2879,2])).
% 281.77/281.76 cnf(2898,plain,
% 281.77/281.76 (~E(f2(f2(f2(x28981,a1),x28982),x28983),f2(a3,f2(a3,a4)))),
% 281.77/281.76 inference(scs_inference,[],[1946,2])).
% 281.77/281.76 cnf(2920,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),a4),a4),f2(f2(a4,x29201),f2(a4,x29202)))),
% 281.77/281.76 inference(scs_inference,[],[2672,2])).
% 281.77/281.76 cnf(2928,plain,
% 281.77/281.76 (~E(f2(a3,f2(x29281,x29281)),a1)),
% 281.77/281.76 inference(scs_inference,[],[2600,1957,2190,2,3])).
% 281.77/281.76 cnf(2932,plain,
% 281.77/281.76 (~E(f2(x29321,x29321),f2(f2(a1,f2(x29322,a1)),f2(x29323,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2815,2101,13,2,3])).
% 281.77/281.76 cnf(2933,plain,
% 281.77/281.76 (~E(f2(a1,f2(a3,f2(x29331,x29331))),a4)),
% 281.77/281.76 inference(scs_inference,[],[2928,2815,2101,13,6,2,3,12])).
% 281.77/281.76 cnf(2936,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x29361,a1)),f2(x29362,a1)),f2(x29363,x29363))),
% 281.77/281.76 inference(scs_inference,[],[2932,2])).
% 281.77/281.76 cnf(2937,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),f2(x29371,a1)),a4),f2(f2(a4,x29372),f2(a4,x29373)))),
% 281.77/281.76 inference(scs_inference,[],[2932,2920,2309,2,3])).
% 281.77/281.76 cnf(2939,plain,
% 281.77/281.76 (~E(a4,f2(a1,f2(a3,f2(x29391,x29391))))),
% 281.77/281.76 inference(scs_inference,[],[2933,2])).
% 281.77/281.76 cnf(2940,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(x29401,a1)),f2(x29402,x29402))),
% 281.77/281.76 inference(scs_inference,[],[2936,2933,2325,2,3])).
% 281.77/281.76 cnf(2943,plain,
% 281.77/281.76 (~E(f2(x29431,x29431),f2(f2(a1,a4),f2(x29432,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2940,2])).
% 281.77/281.76 cnf(2944,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),f2(x29441,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2940,2859,2199,2,3])).
% 281.77/281.76 cnf(2947,plain,
% 281.77/281.76 (~E(a4,f2(f2(a3,f2(a3,a4)),f2(x29471,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2944,2])).
% 281.77/281.76 cnf(2948,plain,
% 281.77/281.76 (~E(f2(f2(a4,x29481),f2(f2(x29482,a1),x29481)),f2(f2(a1,a4),f2(x29483,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2943,2944,2200,2,3])).
% 281.77/281.76 cnf(2956,plain,
% 281.77/281.76 (~E(f2(f2(x29561,x29561),f2(f2(x29562,a1),a4)),f2(f2(a1,a4),f2(x29563,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2948,2284,2,3])).
% 281.77/281.76 cnf(2960,plain,
% 281.77/281.76 (~E(f2(x29601,a1),f2(f2(a3,f2(a3,a4)),f2(x29602,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2947,2956,35,2,3])).
% 281.77/281.76 cnf(2961,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),f2(x29611,a1)),f2(x29612,a1))),
% 281.77/281.76 inference(scs_inference,[],[2960,2])).
% 281.77/281.76 cnf(2966,plain,
% 281.77/281.76 (~E(f2(f2(x29661,x29662),x29661),f2(f2(a1,a4),f2(f2(a4,a1),x29663)))),
% 281.77/281.76 inference(scs_inference,[],[2541,2937,32,2,3])).
% 281.77/281.76 cnf(2971,plain,
% 281.77/281.76 (~E(f2(f2(a4,x29711),f2(a4,x29712)),f2(f2(a1,a4),f2(f2(a4,a1),x29713)))),
% 281.77/281.76 inference(scs_inference,[],[2966,2296,2,3])).
% 281.77/281.76 cnf(2975,plain,
% 281.77/281.76 (~E(f2(f2(x29751,a1),x29752),f2(f2(a1,a4),f2(a4,f2(x29753,a1))))),
% 281.77/281.76 inference(scs_inference,[],[2794,2971,47,2,3])).
% 281.77/281.76 cnf(2976,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(a4,f2(x29761,a1))),f2(f2(x29762,a1),x29763))),
% 281.77/281.76 inference(scs_inference,[],[2975,2])).
% 281.77/281.76 cnf(2980,plain,
% 281.77/281.76 (~E(f2(f2(f2(x29801,x29802),x29801),x29803),f2(a3,f2(x29804,a1)))),
% 281.77/281.76 inference(scs_inference,[],[1309,2])).
% 281.77/281.76 cnf(2981,plain,
% 281.77/281.76 (~E(f2(x29811,x29811),f2(f2(a1,a4),f2(f2(x29812,a1),a4)))),
% 281.77/281.76 inference(scs_inference,[],[2883,1309,13,2,3])).
% 281.77/281.76 cnf(2982,plain,
% 281.77/281.76 (~E(f2(a1,f2(f2(x29821,x29821),x29822)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2883,1309,1147,13,6,2,3,12])).
% 281.77/281.76 cnf(2985,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x29851,a1),a4)),f2(x29852,x29852))),
% 281.77/281.76 inference(scs_inference,[],[2981,2])).
% 281.77/281.76 cnf(2986,plain,
% 281.77/281.76 (~E(f2(a4,a1),f2(f2(a1,a4),f2(f2(x29861,a1),a4)))),
% 281.77/281.76 inference(scs_inference,[],[2981,840,2,3])).
% 281.77/281.76 cnf(2989,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x29891,a1),a4)),f2(a4,a1))),
% 281.77/281.76 inference(scs_inference,[],[2986,2])).
% 281.77/281.76 cnf(2990,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x29901,x29901)),f2(f2(x29902,a1),a4)),f2(x29903,x29903))),
% 281.77/281.76 inference(scs_inference,[],[2985,2986,2315,2,3])).
% 281.77/281.76 cnf(2992,plain,
% 281.77/281.76 (~E(a4,f2(a1,f2(f2(x29921,x29921),x29922)))),
% 281.77/281.76 inference(scs_inference,[],[2982,2])).
% 281.77/281.76 cnf(2993,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(x29931,a1)),f2(a4,a1))),
% 281.77/281.76 inference(scs_inference,[],[2989,2982,2257,2,3])).
% 281.77/281.76 cnf(2996,plain,
% 281.77/281.76 (~E(f2(a4,a1),f2(f2(a1,a4),f2(x29961,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2993,2])).
% 281.77/281.76 cnf(2997,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x29971,a1)),f2(x29972,a1)),f2(a4,a1))),
% 281.77/281.76 inference(scs_inference,[],[2993,2309,2,3])).
% 281.77/281.76 cnf(2999,plain,
% 281.77/281.76 (~E(f2(a1,f2(f2(a3,a4),x29991)),a4)),
% 281.77/281.76 inference(scs_inference,[],[2993,1063,2309,6,2,3,12])).
% 281.77/281.76 cnf(3003,plain,
% 281.77/281.76 (~E(f2(f2(a4,x30031),a1),f2(f2(a1,a4),f2(x30032,a1)))),
% 281.77/281.76 inference(scs_inference,[],[2996,2997,813,2,3])).
% 281.77/281.76 cnf(3005,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(x30051,a1)),f2(f2(a4,x30052),a1))),
% 281.77/281.76 inference(scs_inference,[],[3003,2])).
% 281.77/281.76 cnf(3006,plain,
% 281.77/281.76 (~E(f2(f2(x30061,x30061),a1),f2(f2(a1,a4),f2(x30062,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3003,2241,2,3])).
% 281.77/281.76 cnf(3008,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(x30081,a1)),f2(f2(x30082,x30082),a1))),
% 281.77/281.76 inference(scs_inference,[],[3006,2])).
% 281.77/281.76 cnf(3011,plain,
% 281.77/281.76 (~E(a4,f2(a1,f2(f2(a3,a4),x30111)))),
% 281.77/281.76 inference(scs_inference,[],[2999,2])).
% 281.77/281.76 cnf(3012,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30121,x30121)),f2(x30122,a1)),f2(f2(x30123,x30123),a1))),
% 281.77/281.76 inference(scs_inference,[],[3008,2999,2315,2,3])).
% 281.77/281.76 cnf(3017,plain,
% 281.77/281.76 (~E(f2(f2(x30171,x30171),a1),f2(f2(a1,f2(x30172,x30172)),f2(x30173,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3012,2])).
% 281.77/281.76 cnf(3018,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30181,x30181)),f2(a4,a4)),f2(x30182,x30182))),
% 281.77/281.76 inference(scs_inference,[],[3012,2990,2267,2,3])).
% 281.77/281.76 cnf(3021,plain,
% 281.77/281.76 (~E(f2(x30211,x30211),f2(f2(a1,f2(x30212,x30212)),f2(a4,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3018,2])).
% 281.77/281.76 cnf(3022,plain,
% 281.77/281.76 (~E(f2(f2(x30221,a1),a1),f2(f2(a1,f2(x30222,x30222)),f2(x30223,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3018,3017,2181,2,3])).
% 281.77/281.76 cnf(3025,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30251,x30251)),f2(x30252,a1)),f2(f2(x30253,a1),a1))),
% 281.77/281.76 inference(scs_inference,[],[3022,2])).
% 281.77/281.76 cnf(3026,plain,
% 281.77/281.76 (~E(f2(f2(a4,x30261),f2(x30262,x30262)),f2(f2(a1,f2(x30263,x30263)),f2(a4,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3021,3022,2235,2,3])).
% 281.77/281.76 cnf(3029,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30291,x30291)),f2(a4,a4)),f2(f2(a4,x30292),f2(x30293,x30293)))),
% 281.77/281.76 inference(scs_inference,[],[3026,2])).
% 281.77/281.76 cnf(3030,plain,
% 281.77/281.76 (~E(f2(f2(f2(x30301,x30301),x30302),f2(x30303,x30303)),f2(f2(a1,f2(x30304,x30304)),f2(a4,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3026,2220,2,3])).
% 281.77/281.76 cnf(3035,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30351,x30351)),f2(a4,a4)),f2(f2(f2(x30352,x30352),x30353),f2(x30354,x30354)))),
% 281.77/281.76 inference(scs_inference,[],[3030,2])).
% 281.77/281.76 cnf(3036,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30361,x30361)),f2(x30362,a1)),f2(f2(a4,x30363),f2(x30364,x30364)))),
% 281.77/281.76 inference(scs_inference,[],[3029,3030,2180,2,3])).
% 281.77/281.76 cnf(3038,plain,
% 281.77/281.76 (~E(f2(f2(a4,x30381),f2(x30382,x30382)),f2(f2(a1,f2(x30383,x30383)),f2(x30384,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3036,2])).
% 281.77/281.76 cnf(3039,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30391,a1)),f2(x30392,a1)),f2(f2(a4,x30393),a1))),
% 281.77/281.76 inference(scs_inference,[],[3005,3036,2309,2,3])).
% 281.77/281.76 cnf(3041,plain,
% 281.77/281.76 (~E(f2(f2(a4,x30411),a1),f2(f2(a1,f2(x30412,a1)),f2(x30413,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3039,2])).
% 281.77/281.76 cnf(3042,plain,
% 281.77/281.76 (~E(f2(f2(x30421,x30421),f2(x30422,x30422)),f2(f2(a1,f2(x30423,x30423)),f2(x30424,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3038,3039,2277,2,3])).
% 281.77/281.76 cnf(3045,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30451,x30451)),f2(x30452,a1)),f2(f2(x30453,x30453),f2(x30454,x30454)))),
% 281.77/281.76 inference(scs_inference,[],[3042,2])).
% 281.77/281.76 cnf(3046,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(x30461,x30461)),f2(x30462,a1)))),
% 281.77/281.76 inference(scs_inference,[],[10,3042,2,3])).
% 281.77/281.76 cnf(3056,plain,
% 281.77/281.76 (~E(f2(f2(x30561,a1),a1),f2(f2(a1,f2(x30562,a1)),f2(x30563,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3046,3041,2156,7,2,12,3])).
% 281.77/281.76 cnf(3063,plain,
% 281.77/281.76 (~E(f2(f2(x30631,x30631),a1),f2(f2(a1,f2(x30632,a1)),f2(x30633,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3025,3056,2241,50,2,12,3])).
% 281.77/281.76 cnf(3067,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(a4,a4)),f2(f2(x30671,a1),x30672))),
% 281.77/281.76 inference(scs_inference,[],[3063,2976,2333,2,3])).
% 281.77/281.76 cnf(3070,plain,
% 281.77/281.76 (~E(f2(f2(x30701,a1),x30702),f2(f2(a1,a4),f2(a4,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3067,2])).
% 281.77/281.76 cnf(3071,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(x30711,x30711)),f2(a4,a4)),f2(f2(x30712,a1),x30713))),
% 281.77/281.76 inference(scs_inference,[],[3067,2315,2,3])).
% 281.77/281.76 cnf(3073,plain,
% 281.77/281.76 (~E(f2(f2(x30731,a1),x30732),f2(f2(a1,f2(x30733,x30733)),f2(a4,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3071,2])).
% 281.77/281.76 cnf(3074,plain,
% 281.77/281.76 (~E(f2(f2(a4,x30741),x30742),f2(f2(a1,a4),f2(a4,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3070,3071,2251,2,3])).
% 281.77/281.76 cnf(3076,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(a4,a4)),f2(f2(a4,x30761),x30762))),
% 281.77/281.76 inference(scs_inference,[],[3074,2])).
% 281.77/281.76 cnf(3077,plain,
% 281.77/281.76 (~E(f2(x30771,x30771),f2(f2(a1,f2(a3,a4)),a4))),
% 281.77/281.76 inference(scs_inference,[],[13,3074,2852,2,3])).
% 281.77/281.76 cnf(3083,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(a3,a4)),a4),f2(x30831,x30831))),
% 281.77/281.76 inference(scs_inference,[],[3077,2])).
% 281.77/281.76 cnf(3084,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x30841,x30841),a4)),f2(f2(a4,x30842),x30843))),
% 281.77/281.76 inference(scs_inference,[],[3076,3077,2219,2,3])).
% 281.77/281.76 cnf(3087,plain,
% 281.77/281.76 (~E(f2(x30871,x30871),f2(f2(a3,f2(a3,a4)),a4))),
% 281.77/281.76 inference(scs_inference,[],[13,2858,3084,2,3])).
% 281.77/281.76 cnf(3088,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),a4),f2(x30881,x30881))),
% 281.77/281.76 inference(scs_inference,[],[3087,2])).
% 281.77/281.76 cnf(3089,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),f2(f2(x30891,a1),x30892)),f2(x30893,a1))),
% 281.77/281.76 inference(scs_inference,[],[2961,3087,2324,2,3])).
% 281.77/281.76 cnf(3093,plain,
% 281.77/281.76 (~E(f2(x30931,x30931),f2(f2(f2(a1,a4),f2(x30932,x30932)),a4))),
% 281.77/281.76 inference(scs_inference,[],[13,2802,3089,2,3])).
% 281.77/281.76 cnf(3098,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),f2(x30981,x30981)),a4),f2(x30982,x30982))),
% 281.77/281.76 inference(scs_inference,[],[3093,2])).
% 281.77/281.76 cnf(3099,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(a3,a4)),f2(f2(x30991,a1),x30992)),f2(x30993,x30993))),
% 281.77/281.76 inference(scs_inference,[],[3083,3093,2283,2,3])).
% 281.77/281.76 cnf(3101,plain,
% 281.77/281.76 (~E(f2(x31011,x31011),f2(f2(a1,f2(a3,a4)),f2(f2(x31012,a1),x31013)))),
% 281.77/281.76 inference(scs_inference,[],[3099,2])).
% 281.77/281.76 cnf(3102,plain,
% 281.77/281.76 (~E(f2(x31021,x31021),f2(a1,f2(f2(x31022,x31022),x31023)))),
% 281.77/281.76 inference(scs_inference,[],[13,2992,3099,2,3])).
% 281.77/281.76 cnf(3104,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a4)),f2(f2(x31041,a1),x31042)),f2(x31043,x31043))),
% 281.77/281.76 inference(scs_inference,[],[3088,3102,2283,2,3])).
% 281.77/281.76 cnf(3106,plain,
% 281.77/281.76 (~E(f2(x31061,x31061),f2(f2(a3,f2(a3,a4)),f2(f2(x31062,a1),x31063)))),
% 281.77/281.76 inference(scs_inference,[],[3104,2])).
% 281.77/281.76 cnf(3107,plain,
% 281.77/281.76 (~E(f2(x31071,x31071),f2(a1,f2(f2(a3,a4),x31072)))),
% 281.77/281.76 inference(scs_inference,[],[13,3011,3104,2,3])).
% 281.77/281.76 cnf(3111,plain,
% 281.77/281.76 (~E(f2(a1,f2(f2(a3,a4),x31111)),f2(x31112,x31112))),
% 281.77/281.76 inference(scs_inference,[],[3107,2])).
% 281.77/281.76 cnf(3112,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),a4),a4),f2(x31121,x31121))),
% 281.77/281.76 inference(scs_inference,[],[3098,3107,2334,2,3])).
% 281.77/281.76 cnf(3115,plain,
% 281.77/281.76 (~E(f2(x31151,x31151),f2(f2(f2(a1,a4),a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[3112,2])).
% 281.77/281.76 cnf(3116,plain,
% 281.77/281.76 (~E(f2(a4,x31161),f2(a1,f2(f2(a4,x31162),x31163)))),
% 281.77/281.76 inference(scs_inference,[],[14,3112,1055,2,3])).
% 281.77/281.76 cnf(3117,plain,
% 281.77/281.76 (~E(f2(a1,f2(f2(a4,x31171),x31172)),f2(a4,x31173))),
% 281.77/281.76 inference(scs_inference,[],[3116,2])).
% 281.77/281.76 cnf(3118,plain,
% 281.77/281.76 (~E(f2(a4,x31181),f2(a1,f2(f2(x31182,a1),x31183)))),
% 281.77/281.76 inference(scs_inference,[],[14,3116,2622,2,3])).
% 281.77/281.76 cnf(3119,plain,
% 281.77/281.76 (~E(f2(a1,f2(f2(x31191,a1),x31192)),f2(a4,x31193))),
% 281.77/281.76 inference(scs_inference,[],[3118,2])).
% 281.77/281.76 cnf(3120,plain,
% 281.77/281.76 (~E(f2(a4,x31201),f2(f2(f2(a3,a4),f2(x31202,a1)),a4))),
% 281.77/281.76 inference(scs_inference,[],[14,3118,2624,2,3])).
% 281.77/281.76 cnf(3121,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(f2(a4,x31211),x31212)),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[14,3117,3118,2624,50,2,3,12])).
% 281.77/281.76 cnf(3125,plain,
% 281.77/281.76 (~E(f2(f2(f2(a3,a4),f2(x31251,a1)),a4),f2(a4,x31252))),
% 281.77/281.76 inference(scs_inference,[],[3120,2])).
% 281.77/281.76 cnf(3126,plain,
% 281.77/281.76 (~E(f2(a4,x31261),f2(a3,f2(a3,f2(x31262,x31262))))),
% 281.77/281.76 inference(scs_inference,[],[14,3120,2630,2,3])).
% 281.77/281.76 cnf(3127,plain,
% 281.77/281.76 (~E(f2(a3,f2(a3,f2(x31271,x31271))),f2(a4,x31272))),
% 281.77/281.76 inference(scs_inference,[],[3126,2])).
% 281.77/281.76 cnf(3128,plain,
% 281.77/281.76 (~E(f2(a4,x31281),f2(a1,f2(a3,f2(x31282,x31282))))),
% 281.77/281.76 inference(scs_inference,[],[14,3126,2939,2,3])).
% 281.77/281.76 cnf(3129,plain,
% 281.77/281.76 (~E(f2(a1,f2(a3,f2(x31291,x31291))),f2(a4,x31292))),
% 281.77/281.76 inference(scs_inference,[],[3128,2])).
% 281.77/281.76 cnf(3130,plain,
% 281.77/281.76 (~E(f2(f2(f2(a3,a4),a4),a4),f2(a4,x31301))),
% 281.77/281.76 inference(scs_inference,[],[3125,3128,2325,2,3])).
% 281.77/281.76 cnf(3135,plain,
% 281.77/281.76 (~E(f2(a4,x31351),f2(a1,f2(a3,f2(a4,x31352))))),
% 281.77/281.76 inference(scs_inference,[],[14,3130,2633,2,3])).
% 281.77/281.76 cnf(3136,plain,
% 281.77/281.76 (~E(f2(f2(f2(f2(a3,a4),a4),a4),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[14,3130,2633,50,2,3,12])).
% 281.77/281.76 cnf(3141,plain,
% 281.77/281.76 (~E(f2(a4,x31411),f2(a1,f2(a3,f2(x31412,a1))))),
% 281.77/281.76 inference(scs_inference,[],[14,3135,2637,2,3])).
% 281.77/281.76 cnf(3142,plain,
% 281.77/281.76 (~E(f2(a1,f2(a3,f2(x31421,a1))),f2(a4,x31422))),
% 281.77/281.76 inference(scs_inference,[],[3141,2])).
% 281.77/281.76 cnf(3143,plain,
% 281.77/281.76 (~E(f2(a4,x31431),f2(a3,f2(a3,f2(x31432,a1))))),
% 281.77/281.76 inference(scs_inference,[],[14,3141,2649,2,3])).
% 281.77/281.76 cnf(3145,plain,
% 281.77/281.76 (~E(f2(a4,x31451),f2(a3,f2(a3,f2(a4,x31452))))),
% 281.77/281.76 inference(scs_inference,[],[14,3143,2668,2,3])).
% 281.77/281.76 cnf(3147,plain,
% 281.77/281.76 (~E(f2(a4,x31471),f2(f2(a1,f2(a4,x31472)),a4))),
% 281.77/281.76 inference(scs_inference,[],[14,3145,2671,2,3])).
% 281.77/281.76 cnf(3148,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(f2(x31481,a1),x31482)),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[14,3119,3145,2671,50,2,3,12])).
% 281.77/281.76 cnf(3152,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(a4,x31521)),a4),f2(a4,x31522))),
% 281.77/281.76 inference(scs_inference,[],[3147,2])).
% 281.77/281.76 cnf(3153,plain,
% 281.77/281.76 (~E(f2(a4,x31531),f2(f2(f2(a1,a4),a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[18,3115,3147,2,3])).
% 281.77/281.76 cnf(3155,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),a4),a4),f2(a4,x31551))),
% 281.77/281.76 inference(scs_inference,[],[3153,2])).
% 281.77/281.76 cnf(3156,plain,
% 281.77/281.76 (~E(f2(x31561,a1),f2(f2(f2(f2(a1,f2(a3,a4)),f2(x31562,x31562)),f2(a4,x31563)),f2(x31564,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3153,2864,35,2,3])).
% 281.77/281.76 cnf(3158,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),f2(x31581,a1)),a4),f2(a4,x31582))),
% 281.77/281.76 inference(scs_inference,[],[3155,3156,2309,2,3])).
% 281.77/281.76 cnf(3164,plain,
% 281.77/281.76 (~E(f2(f2(f2(f2(a1,a4),f2(x31641,a1)),a4),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[3158,2454,812,50,2,3,12])).
% 281.77/281.76 cnf(3168,plain,
% 281.77/281.76 (~E(a4,f2(f2(f2(f2(a3,a4),a4),a4),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3136,2])).
% 281.77/281.76 cnf(3169,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),a4),f2(a4,x31691))),
% 281.77/281.76 inference(scs_inference,[],[3152,3136,2334,2,3])).
% 281.77/281.76 cnf(3172,plain,
% 281.77/281.76 (~E(f2(a4,x31721),f2(f2(a1,a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[3169,2])).
% 281.77/281.76 cnf(3173,plain,
% 281.77/281.76 (~E(f2(f2(x31731,x31732),x31731),f2(f2(f2(f2(a3,a4),a4),a4),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3169,3168,32,2,3])).
% 281.77/281.76 cnf(3174,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(f2(a4,x31741),x31742)),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3121,2])).
% 281.77/281.76 cnf(3175,plain,
% 281.77/281.76 (~E(f2(a4,x31751),a3)),
% 281.77/281.76 inference(scs_inference,[],[18,2557,3121,2,3])).
% 281.77/281.76 cnf(3178,plain,
% 281.77/281.76 (~E(a4,f2(f2(a1,f2(f2(x31781,a1),x31782)),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3148,2])).
% 281.77/281.76 cnf(3179,plain,
% 281.77/281.76 (~E(f2(f2(x31791,a1),x31792),f2(f2(a1,f2(f2(a4,x31793),x31794)),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3148,3174,47,2,3])).
% 281.77/281.76 cnf(3180,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,f2(x31801,x31801))),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[3127,3148,3174,47,50,2,3,12])).
% 281.77/281.76 cnf(3184,plain,
% 281.77/281.76 (~E(a4,f2(f2(f2(f2(a1,a4),f2(x31841,a1)),a4),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3164,2])).
% 281.77/281.76 cnf(3189,plain,
% 281.77/281.76 (~E(f2(x31891,a1),f2(f2(a1,f2(f2(x31892,a1),x31893)),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3178,3180,35,2,3])).
% 281.77/281.76 cnf(3192,plain,
% 281.77/281.76 (~E(f2(a4,x31921),f2(a3,f2(x31922,a1)))),
% 281.77/281.76 inference(scs_inference,[],[18,2980,3189,2,3])).
% 281.77/281.76 cnf(3196,plain,
% 281.77/281.76 (~E(f2(f2(x31961,x31962),x31961),f2(f2(f2(f2(a1,a4),f2(x31963,a1)),a4),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3184,2729,32,2,3])).
% 281.77/281.76 cnf(3197,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(a3,f2(x31971,x31971))),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[3129,3184,2729,32,50,2,3,12])).
% 281.77/281.76 cnf(3202,plain,
% 281.77/281.76 (~E(f2(x32021,x32021),a3)),
% 281.77/281.76 inference(scs_inference,[],[19,3175,3197,2,3])).
% 281.77/281.76 cnf(3205,plain,
% 281.77/281.76 (~E(f2(a3,f2(a3,a3)),a4)),
% 281.77/281.76 inference(scs_inference,[],[3202,1040,9,2,12])).
% 281.77/281.76 cnf(3213,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a3)),a4),a4)),
% 281.77/281.76 inference(scs_inference,[],[3205,7,2,12])).
% 281.77/281.76 cnf(3216,plain,
% 281.77/281.76 (~E(f2(x32161,x32161),f2(f2(a1,a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[19,3172,3205,7,2,12,3])).
% 281.77/281.76 cnf(3218,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),a4),f2(x32181,x32181))),
% 281.77/281.76 inference(scs_inference,[],[3216,2])).
% 281.77/281.76 cnf(3222,plain,
% 281.77/281.76 (~E(a4,f2(f2(a3,f2(a3,a3)),a4))),
% 281.77/281.76 inference(scs_inference,[],[3213,2])).
% 281.77/281.76 cnf(3223,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x32231,a1),x32232)),f2(x32233,x32233))),
% 281.77/281.76 inference(scs_inference,[],[3218,3213,2283,2,3])).
% 281.77/281.76 cnf(3225,plain,
% 281.77/281.76 (~E(f2(x32251,x32251),f2(f2(a1,a4),f2(f2(x32252,a1),x32253)))),
% 281.77/281.76 inference(scs_inference,[],[3223,2])).
% 281.77/281.76 cnf(3239,plain,
% 281.77/281.76 (~E(f2(x32391,x32391),f2(a3,f2(x32392,a1)))),
% 281.77/281.76 inference(scs_inference,[],[19,3192,1250,2,3])).
% 281.77/281.76 cnf(3242,plain,
% 281.77/281.76 (~E(f2(f2(f2(a4,x32421),x32422),f2(a4,x32422)),f2(a3,f2(x32423,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3239,1732,2161,2,3])).
% 281.77/281.76 cnf(3245,plain,
% 281.77/281.76 (~E(f2(f2(a1,f2(a3,f2(x32451,a1))),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[3239,3142,1732,2161,50,2,3,12])).
% 281.77/281.76 cnf(3250,plain,
% 281.77/281.76 (~E(f2(a4,x32501),f2(f2(a1,a4),f2(f2(x32502,a1),x32503)))),
% 281.77/281.76 inference(scs_inference,[],[20,3225,3245,2,3])).
% 281.77/281.76 cnf(3253,plain,
% 281.77/281.76 (~E(f2(f2(a1,a4),f2(f2(x32531,a1),x32532)),f2(a4,x32533))),
% 281.77/281.76 inference(scs_inference,[],[3250,2])).
% 281.77/281.76 cnf(3258,plain,
% 281.77/281.76 (~E(f2(a4,x32581),f2(f2(a1,f2(a3,a4)),f2(f2(x32582,a1),x32583)))),
% 281.77/281.76 inference(scs_inference,[],[20,3101,1861,2,3])).
% 281.77/281.76 cnf(3266,plain,
% 281.77/281.76 (~E(f2(f2(f2(a1,a4),f2(f2(x32661,a1),x32662)),f2(a4,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[3253,3242,3258,37,50,2,3,12])).
% 281.77/281.76 cnf(3271,plain,
% 281.77/281.76 (~E(f2(a4,x32711),f2(f2(a3,f2(a3,a4)),f2(f2(x32712,a1),x32713)))),
% 281.77/281.76 inference(scs_inference,[],[20,3266,3106,2,3])).
% 281.77/281.76 cnf(3275,plain,
% 281.77/281.76 (~E(f2(f2(x32751,a1),x32752),f2(f2(a3,f2(a3,a3)),a4))),
% 281.77/281.76 inference(scs_inference,[],[3222,3271,47,2,3])).
% 281.77/281.76 cnf(3277,plain,
% 281.77/281.76 (E(f2(f2(f2(f2(x32771,x32772),a1),x32773),x32774),f2(f2(f2(f2(x32771,a1),f2(x32772,a1)),x32773),x32774))),
% 281.77/281.76 inference(scs_inference,[],[56,815,5,4])).
% 281.77/281.76 cnf(3278,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a3,a3)),a4),f2(f2(x32781,a1),x32782))),
% 281.77/281.76 inference(scs_inference,[],[3275,56,815,5,4,2])).
% 281.77/281.76 cnf(3285,plain,
% 281.77/281.76 (E(f2(x32851,f2(x32852,f2(f2(x32853,a1),f2(x32854,a1)))),f2(x32851,f2(x32852,f2(f2(x32853,x32854),a1))))),
% 281.77/281.76 inference(scs_inference,[],[858,5])).
% 281.77/281.76 cnf(3308,plain,
% 281.77/281.76 (E(f2(f2(x33081,f2(a4,x33082)),f2(f2(x33083,x33084),x33083)),f2(f2(x33081,a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[107,817,2936,3277,3099,2,4,5,3])).
% 281.77/281.76 cnf(3316,plain,
% 281.77/281.76 (E(f2(f2(x33161,f2(a4,x33162)),f2(a4,x33163)),f2(f2(x33161,a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[853,817,3042,3104,3308,4,5,2,3])).
% 281.77/281.76 cnf(3324,plain,
% 281.77/281.76 (E(f2(f2(x33241,f2(a4,x33242)),f2(f2(a4,x33243),x33244)),f2(f2(x33241,a4),f2(a4,x33244)))),
% 281.77/281.76 inference(scs_inference,[],[817,827,3018,2990,3316,4,5,2,3])).
% 281.77/281.76 cnf(3332,plain,
% 281.77/281.76 (E(f2(f2(x33321,a4),f2(x33322,a1)),f2(f2(x33321,f2(a4,x33323)),a4))),
% 281.77/281.76 inference(scs_inference,[],[85,816,2990,3324,3111,4,5,2,3])).
% 281.77/281.76 cnf(3337,plain,
% 281.77/281.76 (~E(f2(f2(a3,a4),a4),f2(a4,a1))),
% 281.77/281.76 inference(scs_inference,[],[3125,3173,4,5])).
% 281.77/281.76 cnf(3340,plain,
% 281.77/281.76 (E(f2(f2(x33401,f2(a4,x33402)),f2(x33403,x33403)),f2(f2(x33401,a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[817,119,3125,3332,3173,4,5,2,3])).
% 281.77/281.76 cnf(3343,plain,
% 281.77/281.76 (~E(f2(f2(a4,a1),x33431),f2(f2(f2(a3,a4),a4),a4))),
% 281.77/281.76 inference(scs_inference,[],[3173,4])).
% 281.77/281.76 cnf(3345,plain,
% 281.77/281.76 (E(f2(f2(x33451,a4),a4),f2(f2(x33451,f2(a4,x33452)),f2(x33453,x33453)))),
% 281.77/281.76 inference(scs_inference,[],[3173,3340,4,2])).
% 281.77/281.76 cnf(3346,plain,
% 281.77/281.76 (E(f2(f2(x33461,f2(a4,x33462)),a1),f2(f2(f2(x33461,a4),a1),x33463))),
% 281.77/281.76 inference(scs_inference,[],[817,58,3173,3340,4,2,3])).
% 281.77/281.76 cnf(3352,plain,
% 281.77/281.76 (E(f2(f2(x33521,f2(a4,x33522)),a1),f2(f2(x33521,a1),f2(a4,a1)))),
% 281.77/281.76 inference(scs_inference,[],[817,51,3030,3346,4,2,3])).
% 281.77/281.76 cnf(3358,plain,
% 281.77/281.76 (E(f2(f2(a4,x33581),f2(x33582,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[85,9,3029,3352,4,2,3])).
% 281.77/281.76 cnf(3364,plain,
% 281.77/281.76 (E(f2(f2(x33641,f2(a4,x33642)),f2(a4,x33643)),f2(f2(x33641,a4),f2(f2(a4,x33644),x33643)))),
% 281.77/281.76 inference(scs_inference,[],[817,826,3071,3358,4,2,3])).
% 281.77/281.76 cnf(3371,plain,
% 281.77/281.76 (E(f2(f2(f2(x33711,a1),x33712),f2(x33713,a1)),f2(f2(x33711,a1),a4))),
% 281.77/281.76 inference(scs_inference,[],[85,820,3073,3364,4,2,3])).
% 281.77/281.76 cnf(3377,plain,
% 281.77/281.76 (E(f2(f2(f2(x33771,x33772),a4),f2(f2(x33771,a4),x33772)),a4)),
% 281.77/281.76 inference(scs_inference,[],[816,10,3275,3371,4,2,3])).
% 281.77/281.76 cnf(3380,plain,
% 281.77/281.76 (~E(f2(f2(f2(a3,a4),f2(a3,a4)),f2(f2(a3,f2(a3,a4)),a4)),a4)),
% 281.77/281.76 inference(scs_inference,[],[816,10,3087,3275,3371,4,2,3,12])).
% 281.77/281.76 cnf(3386,plain,
% 281.77/281.76 (E(f2(f2(x33861,x33861),f2(x33862,a1)),f2(a4,a4))),
% 281.77/281.76 inference(scs_inference,[],[85,102,3120,3377,4,2,3])).
% 281.77/281.76 cnf(3392,plain,
% 281.77/281.76 (E(f2(x33921,f2(x33922,a1)),f2(x33921,f2(f2(x33923,a1),x33924)))),
% 281.77/281.76 inference(scs_inference,[],[85,2283,3386,2898,4,2,3])).
% 281.77/281.76 cnf(3397,plain,
% 281.77/281.76 (E(f2(f2(a4,x33971),f2(x33972,a1)),f2(a4,a4))),
% 281.77/281.76 inference(scs_inference,[],[85,812,3392,3035,4,2,3])).
% 281.77/281.76 cnf(3403,plain,
% 281.77/281.76 (E(f2(x34031,a1),f2(f2(x34032,a1),x34033))),
% 281.77/281.76 inference(scs_inference,[],[6,47,3397,3278,4,2,3])).
% 281.77/281.76 cnf(3406,plain,
% 281.77/281.76 (E(f2(f2(x34061,a1),x34062),f2(x34063,a1))),
% 281.77/281.76 inference(scs_inference,[],[3403,3196,4,2])).
% 281.77/281.76 cnf(3407,plain,
% 281.77/281.76 (E(f2(f2(x34071,a4),f2(x34072,a1)),f2(f2(x34071,f2(x34073,x34073)),a4))),
% 281.77/281.76 inference(scs_inference,[],[85,2315,3403,3196,4,2,3])).
% 281.77/281.76 cnf(3413,plain,
% 281.77/281.76 (E(f2(f2(x34131,a4),f2(x34132,a1)),f2(f2(x34131,f2(x34133,a1)),a4))),
% 281.77/281.76 inference(scs_inference,[],[85,2309,3407,3179,4,2,3])).
% 281.77/281.76 cnf(3419,plain,
% 281.77/281.76 (E(f2(f2(f2(x34191,x34192),x34191),f2(x34193,a1)),f2(a4,a4))),
% 281.77/281.76 inference(scs_inference,[],[85,105,3413,3343,4,2,3])).
% 281.77/281.76 cnf(3424,plain,
% 281.77/281.76 (E(f2(a4,a4),f2(f2(f2(x34241,x34242),x34241),f2(x34243,a1)))),
% 281.77/281.76 inference(scs_inference,[],[3419,3045,4,2])).
% 281.77/281.76 cnf(3635,plain,
% 281.77/281.76 (E(f2(a4,f2(x36351,a1)),f2(f2(f2(x36352,x36353),x36352),f2(x36354,a1)))),
% 281.77/281.76 inference(scs_inference,[],[85,3424,3285,2,3])).
% 281.77/281.76 cnf(3638,plain,
% 281.77/281.76 (E(f2(f2(x36381,f2(a4,x36382)),f2(x36383,f2(f2(x36384,a1),f2(x36385,a1)))),f2(f2(x36381,a4),f2(x36383,f2(f2(x36384,x36385),a1))))),
% 281.77/281.76 inference(scs_inference,[],[817,3285,3635,2,3])).
% 281.77/281.76 cnf(3708,plain,
% 281.77/281.76 (E(f2(f2(x37081,f2(a4,x37082)),a4),f2(f2(x37081,a4),f2(x37083,x37083)))),
% 281.77/281.76 inference(scs_inference,[],[817,120,3638,2,3])).
% 281.77/281.76 cnf(3712,plain,
% 281.77/281.76 (E(f2(f2(x37121,f2(a4,x37122)),a4),f2(f2(x37121,a4),f2(a4,x37123)))),
% 281.77/281.76 inference(scs_inference,[],[817,854,3708,2,3])).
% 281.77/281.76 cnf(3716,plain,
% 281.77/281.76 (E(f2(f2(x37161,f2(a4,x37162)),a4),f2(f2(x37161,a4),f2(f2(x37163,x37164),x37163)))),
% 281.77/281.76 inference(scs_inference,[],[817,106,3712,2,3])).
% 281.77/281.76 cnf(3720,plain,
% 281.77/281.76 (E(f2(f2(x37201,f2(a4,x37202)),a4),f2(f2(x37201,a4),f2(f2(x37203,a1),x37204)))),
% 281.77/281.76 inference(scs_inference,[],[817,2283,3716,2,3])).
% 281.77/281.76 cnf(3724,plain,
% 281.77/281.76 (E(f2(f2(x37241,f2(a4,x37242)),x37243),f2(f2(x37241,f2(x37244,x37244)),x37243))),
% 281.77/281.76 inference(scs_inference,[],[817,2315,3720,2,3])).
% 281.77/281.76 cnf(3727,plain,
% 281.77/281.76 (E(f2(f2(x37271,f2(a4,x37272)),x37273),f2(f2(x37271,f2(x37274,a1)),x37273))),
% 281.77/281.76 inference(scs_inference,[],[817,2309,3724,2,3])).
% 281.77/281.76 cnf(3730,plain,
% 281.77/281.76 (E(f2(f2(f2(a4,x37301),f2(a4,x37302)),x37303),f2(a4,x37303))),
% 281.77/281.76 inference(scs_inference,[],[817,105,3727,2,3])).
% 281.77/281.76 cnf(3735,plain,
% 281.77/281.76 (E(f2(f2(x37351,f2(a4,x37352)),f2(x37351,a4)),a4)),
% 281.77/281.76 inference(scs_inference,[],[817,8,3730,2,3])).
% 281.77/281.76 cnf(3738,plain,
% 281.77/281.76 (E(a4,f2(f2(x37381,f2(a4,x37382)),f2(x37381,a4)))),
% 281.77/281.76 inference(scs_inference,[],[3735,2])).
% 281.77/281.76 cnf(3822,plain,
% 281.77/281.76 (E(f2(x38221,a4),f2(x38221,f2(f2(x38222,f2(a4,x38223)),f2(x38222,a4))))),
% 281.77/281.76 inference(scs_inference,[],[3337,3738,50,12,5])).
% 281.77/281.76 cnf(3825,plain,
% 281.77/281.76 (~E(f2(f2(a3,f2(a4,x38251)),f2(x38252,x38252)),f2(a4,a1))),
% 281.77/281.76 inference(scs_inference,[],[3337,2609,3406,3345,3738,50,12,5,4,2,3])).
% 281.77/281.76 cnf(3832,plain,
% 281.77/281.76 (~E(a4,f2(f2(f2(a3,a4),f2(a3,a4)),f2(f2(a3,f2(a3,a4)),a4)))),
% 281.77/281.76 inference(scs_inference,[],[10,3380,3825,50,12,5,4,2])).
% 281.77/281.76 cnf(4481,plain,
% 281.77/281.76 (E(f2(x44811,f2(f2(x44812,f2(a4,x44813)),f2(x44812,a4))),f2(x44811,a4))),
% 281.77/281.76 inference(scs_inference,[],[106,3822,5,4,2])).
% 281.77/281.76 cnf(4900,plain,
% 281.77/281.76 (E(f2(x49001,f2(x49002,f2(a4,x49003))),f2(x49001,f2(x49002,f2(x49004,a1))))),
% 281.77/281.76 inference(scs_inference,[],[2180,5])).
% 281.77/281.76 cnf(4979,plain,
% 281.77/281.76 (~E(f2(f2(f2(f2(a1,a4),a4),a4),f2(a1,a1)),a4)),
% 281.77/281.76 inference(scs_inference,[],[50,2200,2296,3112,4900,5,4,2,12])).
% 281.77/281.76 cnf(5070,plain,
% 281.77/281.76 ($false),
% 281.77/281.76 inference(scs_inference,[],[14,4979,3832,4481,101,5,2,4,3]),
% 281.77/281.76 ['proof']).
% 281.77/281.76 % SZS output end Proof
% 281.77/281.76 % Total time :281.090000s
%------------------------------------------------------------------------------