%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN003-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 : n001.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:46 EDT 2024
% Result : Unsatisfiable 202.05s 202.03s
% Output : CNFRefutation 202.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HEN003-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.12/0.33 % Computer : n001.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sat Jun 22 05:35:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 202.05/202.01 %-------------------------------------------
% 202.05/202.01 % File :CSE---1.7
% 202.05/202.01 % Problem :theBenchmark
% 202.05/202.01 % Transform :cnf
% 202.05/202.01 % Format :tptp:raw
% 202.05/202.01 % Command :java -jar mcs_scs.jar %d %s
% 202.05/202.01
% 202.05/202.01 % Result :Theorem 201.440000s
% 202.05/202.01 % Output :CNFRefutation 201.440000s
% 202.05/202.01 %-------------------------------------------
% 202.05/202.02 %--------------------------------------------------------------------------
% 202.05/202.02 % File : HEN003-5 : TPTP v8.2.0. Released v1.0.0.
% 202.05/202.02 % Domain : Henkin Models
% 202.05/202.02 % Problem : X/X = zero
% 202.05/202.02 % Version : [MOW76] (equality) axioms : Reduced > Complete.
% 202.05/202.02 % English :
% 202.05/202.02
% 202.05/202.02 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 202.05/202.02 % Source : [ANL]
% 202.05/202.02 % Names : hp3.ver3.in [ANL]
% 202.05/202.02
% 202.05/202.02 % Status : Unsatisfiable
% 202.05/202.02 % Rating : 0.00 v6.3.0, 0.10 v6.2.0, 0.30 v6.1.0, 0.18 v6.0.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.12 v5.1.0, 0.22 v5.0.0, 0.10 v4.1.0, 0.11 v4.0.1, 0.25 v4.0.0, 0.14 v3.7.0, 0.00 v2.0.0
% 202.05/202.02 % Syntax : Number of clauses : 6 ( 5 unt; 0 nHn; 2 RR)
% 202.05/202.02 % Number of literals : 8 ( 8 equ; 3 neg)
% 202.05/202.02 % Maximal clause size : 3 ( 1 avg)
% 202.05/202.02 % Maximal term depth : 4 ( 1 avg)
% 202.05/202.02 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 202.05/202.02 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 202.05/202.02 % Number of variables : 9 ( 3 sgn)
% 202.05/202.02 % SPC : CNF_UNS_RFO_PEQ_NUE
% 202.05/202.02
% 202.05/202.02 % Comments : less_equal replaced by divides
% 202.05/202.02 %--------------------------------------------------------------------------
% 202.05/202.02 %----Include Henkin model axioms, for the equality formulation with
% 202.05/202.03 %----less_equals removed.
% 202.05/202.03 include('Axioms/HEN003-0.ax').
% 202.05/202.03 %--------------------------------------------------------------------------
% 202.05/202.03 cnf(prove_x_divide_x_is_zero,negated_conjecture,
% 202.05/202.03 divide(a,a) != zero ).
% 202.05/202.03
% 202.05/202.03 %--------------------------------------------------------------------------
% 202.05/202.03 %-------------------------------------------
% 202.05/202.03 % Proof found
% 202.05/202.03 % SZS status Theorem for theBenchmark
% 202.05/202.03 % SZS output start Proof
% 202.05/202.03 %ClaNum:11(EqnAxiom:5)
% 202.05/202.03 %VarNum:18(SingletonVarNum:9)
% 202.05/202.03 %MaxLitNum:3
% 202.05/202.03 %MaxfuncDepth:3
% 202.05/202.03 %SharedTerms:5
% 202.05/202.03 %goalClause: 10
% 202.05/202.03 %singleGoalClaCount:1
% 202.05/202.03 [10]~E(f2(a3,a3),a4)
% 202.05/202.03 [6]E(f2(x61,a1),a4)
% 202.05/202.03 [7]E(f2(a4,x71),a4)
% 202.05/202.03 [8]E(f2(f2(x81,x82),x81),a4)
% 202.05/202.03 [9]E(f2(f2(f2(x91,x92),f2(x93,x92)),f2(f2(x91,x93),x92)),a4)
% 202.05/202.03 [11]E(x111,x112)+~E(f2(x112,x111),a4)+~E(f2(x111,x112),a4)
% 202.05/202.03 %EqnAxiom
% 202.05/202.03 [1]E(x11,x11)
% 202.05/202.03 [2]E(x22,x21)+~E(x21,x22)
% 202.05/202.03 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 202.05/202.03 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 202.05/202.03 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 202.05/202.03
% 202.05/202.03 %-------------------------------------------
% 202.05/202.04 cnf(12,plain,
% 202.05/202.04 (E(a4,f2(x121,a1))),
% 202.05/202.04 inference(scs_inference,[],[6,2])).
% 202.05/202.05 cnf(13,plain,
% 202.05/202.05 (E(a4,f2(a4,x131))),
% 202.05/202.05 inference(scs_inference,[],[6,7,8,2,11])).
% 202.05/202.05 cnf(17,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(x171,a1))),
% 202.05/202.05 inference(scs_inference,[],[10,6,7,8,2,11,3])).
% 202.05/202.05 cnf(18,plain,
% 202.05/202.05 (~E(a3,a1)),
% 202.05/202.05 inference(scs_inference,[],[10,6,7,8,2,11,3,5])).
% 202.05/202.05 cnf(19,plain,
% 202.05/202.05 (E(a4,f2(f2(f2(x191,x192),f2(x193,x192)),f2(f2(x191,x193),x192)))),
% 202.05/202.05 inference(scs_inference,[],[9,2])).
% 202.05/202.05 cnf(20,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(f2(x201,x202),f2(x203,x202)),f2(f2(x201,x203),x202)))),
% 202.05/202.05 inference(scs_inference,[],[10,9,2,3])).
% 202.05/202.05 cnf(21,plain,
% 202.05/202.05 (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)),
% 202.05/202.05 inference(scs_inference,[],[10,9,2,3,11])).
% 202.05/202.05 cnf(23,plain,
% 202.05/202.05 (E(a4,f2(f2(x231,x232),x231))),
% 202.05/202.05 inference(scs_inference,[],[8,2])).
% 202.05/202.05 cnf(24,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(a4,x241))),
% 202.05/202.05 inference(scs_inference,[],[10,7,8,2,3])).
% 202.05/202.05 cnf(26,plain,
% 202.05/202.05 (~E(f2(a3,a4),a4)),
% 202.05/202.05 inference(scs_inference,[],[10,7,8,2,3,4,11])).
% 202.05/202.05 cnf(29,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(x291,x292),x291))),
% 202.05/202.05 inference(scs_inference,[],[10,8,3])).
% 202.05/202.05 cnf(31,plain,
% 202.05/202.05 (~E(f2(a3,f2(a3,x311)),a4)),
% 202.05/202.05 inference(scs_inference,[],[10,8,3,4,11])).
% 202.05/202.05 cnf(37,plain,
% 202.05/202.05 (E(f2(x371,f2(x372,a1)),f2(x371,a4))),
% 202.05/202.05 inference(scs_inference,[],[12,2,5])).
% 202.05/202.05 cnf(38,plain,
% 202.05/202.05 (E(f2(x381,a4),f2(x381,f2(x382,a1)))),
% 202.05/202.05 inference(scs_inference,[],[37,2])).
% 202.05/202.05 cnf(44,plain,
% 202.05/202.05 (E(f2(f2(x441,a1),x442),f2(a4,x442))),
% 202.05/202.05 inference(scs_inference,[],[12,2,4])).
% 202.05/202.05 cnf(45,plain,
% 202.05/202.05 (E(f2(a4,x451),f2(f2(x452,a1),x451))),
% 202.05/202.05 inference(scs_inference,[],[44,2])).
% 202.05/202.05 cnf(47,plain,
% 202.05/202.05 (E(f2(x471,f2(a4,x472)),f2(x471,a4))),
% 202.05/202.05 inference(scs_inference,[],[13,2,5])).
% 202.05/202.05 cnf(48,plain,
% 202.05/202.05 (E(f2(x481,a4),f2(x481,f2(a4,x482)))),
% 202.05/202.05 inference(scs_inference,[],[47,2])).
% 202.05/202.05 cnf(49,plain,
% 202.05/202.05 (~E(f2(a4,x491),f2(a3,a3))),
% 202.05/202.05 inference(scs_inference,[],[10,13,2,3])).
% 202.05/202.05 cnf(50,plain,
% 202.05/202.05 (E(f2(f2(a4,x501),x502),f2(a4,x502))),
% 202.05/202.05 inference(scs_inference,[],[13,2,4])).
% 202.05/202.05 cnf(51,plain,
% 202.05/202.05 (E(f2(a4,x511),f2(f2(a4,x512),x511))),
% 202.05/202.05 inference(scs_inference,[],[50,2])).
% 202.05/202.05 cnf(52,plain,
% 202.05/202.05 (~E(f2(f2(a3,a3),f2(f2(a3,a3),a1)),a4)),
% 202.05/202.05 inference(scs_inference,[],[17,8,2,11])).
% 202.05/202.05 cnf(53,plain,
% 202.05/202.05 (~E(f2(a1,a3),a4)),
% 202.05/202.05 inference(scs_inference,[],[18,6,2,11])).
% 202.05/202.05 cnf(55,plain,
% 202.05/202.05 (~E(a4,f2(a3,a3))),
% 202.05/202.05 inference(scs_inference,[],[20,9,2,3])).
% 202.05/202.05 cnf(56,plain,
% 202.05/202.05 (E(f2(f2(f2(x561,x562),x561),x563),f2(a4,x563))),
% 202.05/202.05 inference(scs_inference,[],[23,2,4])).
% 202.05/202.05 cnf(57,plain,
% 202.05/202.05 (E(f2(a4,x571),f2(f2(f2(x572,x573),x572),x571))),
% 202.05/202.05 inference(scs_inference,[],[56,2])).
% 202.05/202.05 cnf(58,plain,
% 202.05/202.05 (E(f2(x581,f2(f2(x582,x583),x582)),f2(x581,a4))),
% 202.05/202.05 inference(scs_inference,[],[23,2,5])).
% 202.05/202.05 cnf(59,plain,
% 202.05/202.05 (E(f2(x591,a4),f2(x591,f2(f2(x592,x593),x592)))),
% 202.05/202.05 inference(scs_inference,[],[58,2])).
% 202.05/202.05 cnf(60,plain,
% 202.05/202.05 (~E(f2(f2(x601,x602),x601),f2(a3,a3))),
% 202.05/202.05 inference(scs_inference,[],[10,23,2,3])).
% 202.05/202.05 cnf(61,plain,
% 202.05/202.05 (~E(f2(f2(f2(x611,x612),x611),x613),f2(a3,a3))),
% 202.05/202.05 inference(scs_inference,[],[24,57,2,3])).
% 202.05/202.05 cnf(64,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(f2(x641,x642),x641),x643))),
% 202.05/202.05 inference(scs_inference,[],[24,61,56,4,3])).
% 202.05/202.05 cnf(66,plain,
% 202.05/202.05 (~E(a3,f2(f2(x661,x662),x661))),
% 202.05/202.05 inference(scs_inference,[],[64,4])).
% 202.05/202.05 cnf(68,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(x681,a1),x682))),
% 202.05/202.05 inference(scs_inference,[],[24,64,44,4,3])).
% 202.05/202.05 cnf(70,plain,
% 202.05/202.05 (E(f2(f2(x701,a4),x702),f2(f2(x701,f2(a4,x703)),x702))),
% 202.05/202.05 inference(scs_inference,[],[13,4,5])).
% 202.05/202.05 cnf(73,plain,
% 202.05/202.05 (E(f2(f2(x731,f2(a4,x732)),x733),f2(f2(x731,a4),x733))),
% 202.05/202.05 inference(scs_inference,[],[70,68,4,2])).
% 202.05/202.05 cnf(74,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(a4,x741),x742))),
% 202.05/202.05 inference(scs_inference,[],[24,70,68,50,4,2,3])).
% 202.05/202.05 cnf(76,plain,
% 202.05/202.05 (E(f2(x761,f2(a4,x762)),f2(x761,f2(f2(a4,x763),x762)))),
% 202.05/202.05 inference(scs_inference,[],[13,4,5])).
% 202.05/202.05 cnf(77,plain,
% 202.05/202.05 (~E(a3,f2(a4,x771))),
% 202.05/202.05 inference(scs_inference,[],[74,4])).
% 202.05/202.05 cnf(79,plain,
% 202.05/202.05 (E(f2(x791,f2(f2(a4,x792),x793)),f2(x791,f2(a4,x793)))),
% 202.05/202.05 inference(scs_inference,[],[76,74,4,2])).
% 202.05/202.05 cnf(80,plain,
% 202.05/202.05 (~E(a3,f2(f2(f2(x801,x802),f2(x803,x802)),f2(f2(x801,x803),x802)))),
% 202.05/202.05 inference(scs_inference,[],[24,9,4,3])).
% 202.05/202.05 cnf(84,plain,
% 202.05/202.05 (E(f2(f2(x841,f2(a4,x842)),a4),f2(f2(x841,a4),f2(a4,x843)))),
% 202.05/202.05 inference(scs_inference,[],[13,73,5,3])).
% 202.05/202.05 cnf(85,plain,
% 202.05/202.05 (E(f2(f2(x851,a4),f2(a4,x852)),f2(f2(x851,f2(a4,x853)),a4))),
% 202.05/202.05 inference(scs_inference,[],[84,2])).
% 202.05/202.05 cnf(93,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(f2(f2(a4,x931),x932),a4),f2(a4,x933)))),
% 202.05/202.05 inference(scs_inference,[],[85,64,3])).
% 202.05/202.05 cnf(97,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(f2(f2(a4,x971),x972),f2(a4,x973)),a4))),
% 202.05/202.05 inference(scs_inference,[],[84,93,3])).
% 202.05/202.05 cnf(108,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x1081,x1082),f2(x1083,x1082)),f2(f2(x1081,x1083),x1082)))),
% 202.05/202.05 inference(scs_inference,[],[26,9,3])).
% 202.05/202.05 cnf(110,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x1101,x1101),f2(x1102,x1101)),a4))),
% 202.05/202.05 inference(scs_inference,[],[59,108,3])).
% 202.05/202.05 cnf(115,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x1151,x1151),a4),f2(a4,x1152)))),
% 202.05/202.05 inference(scs_inference,[],[85,110,3])).
% 202.05/202.05 cnf(119,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x1191,x1191),a4),f2(f2(a4,x1192),x1193)))),
% 202.05/202.05 inference(scs_inference,[],[79,115,3])).
% 202.05/202.05 cnf(122,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x1221,x1221),a4),a4))),
% 202.05/202.05 inference(scs_inference,[],[38,119,3])).
% 202.05/202.05 cnf(125,plain,
% 202.05/202.05 (~E(a3,f2(f2(x1251,x1251),a4))),
% 202.05/202.05 inference(scs_inference,[],[38,119,3,4])).
% 202.05/202.05 cnf(129,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x1291,x1291),a4),f2(x1292,a1)))),
% 202.05/202.05 inference(scs_inference,[],[122,37,3])).
% 202.05/202.05 cnf(134,plain,
% 202.05/202.05 (~E(a3,f2(f2(x1341,x1341),f2(a4,x1342)))),
% 202.05/202.05 inference(scs_inference,[],[84,129,3,4])).
% 202.05/202.05 cnf(142,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(x1421,a1))),
% 202.05/202.05 inference(scs_inference,[],[26,6,3])).
% 202.05/202.05 cnf(143,plain,
% 202.05/202.05 (~E(a4,a1)),
% 202.05/202.05 inference(scs_inference,[],[26,6,3,5])).
% 202.05/202.05 cnf(145,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(a4,x1451))),
% 202.05/202.05 inference(scs_inference,[],[26,7,3])).
% 202.05/202.05 cnf(147,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(x1471,x1472),x1471))),
% 202.05/202.05 inference(scs_inference,[],[26,8,3])).
% 202.05/202.05 cnf(149,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(a4,x1491),x1492),a4))),
% 202.05/202.05 inference(scs_inference,[],[48,147,3])).
% 202.05/202.05 cnf(165,plain,
% 202.05/202.05 (~E(f2(a3,a3),f2(f2(f2(x1651,a1),x1652),a4))),
% 202.05/202.05 inference(scs_inference,[],[29,38,3])).
% 202.05/202.05 cnf(180,plain,
% 202.05/202.05 (~E(f2(a3,f2(a3,x1801)),f2(x1802,a1))),
% 202.05/202.05 inference(scs_inference,[],[31,6,3])).
% 202.05/202.05 cnf(181,plain,
% 202.05/202.05 (~E(f2(a3,x1811),a1)),
% 202.05/202.05 inference(scs_inference,[],[31,6,3,5])).
% 202.05/202.05 cnf(183,plain,
% 202.05/202.05 (~E(f2(a3,f2(a3,x1831)),f2(a4,x1832))),
% 202.05/202.05 inference(scs_inference,[],[31,7,3])).
% 202.05/202.05 cnf(186,plain,
% 202.05/202.05 (~E(a3,f2(f2(a3,x1861),x1862))),
% 202.05/202.05 inference(scs_inference,[],[31,8,3,4])).
% 202.05/202.05 cnf(210,plain,
% 202.05/202.05 (E(f2(a4,a4),f2(f2(x2101,a1),f2(a4,x2102)))),
% 202.05/202.05 inference(scs_inference,[],[13,45,5,3])).
% 202.05/202.05 cnf(211,plain,
% 202.05/202.05 (E(f2(f2(x2111,a1),f2(a4,x2112)),f2(a4,a4))),
% 202.05/202.05 inference(scs_inference,[],[210,2])).
% 202.05/202.05 cnf(229,plain,
% 202.05/202.05 (~E(f2(f2(a3,a3),f2(f2(a3,a3),a1)),f2(a4,x2291))),
% 202.05/202.05 inference(scs_inference,[],[52,7,3])).
% 202.05/202.05 cnf(235,plain,
% 202.05/202.05 (~E(f2(f2(a3,a3),a1),a1)),
% 202.05/202.05 inference(scs_inference,[],[52,6,3,5])).
% 202.05/202.05 cnf(236,plain,
% 202.05/202.05 (E(a1,f2(a3,a3))+~E(f2(a1,f2(a3,a3)),a4)),
% 202.05/202.05 inference(scs_inference,[],[52,6,3,5,11])).
% 202.05/202.05 cnf(247,plain,
% 202.05/202.05 (~E(f2(a1,f2(a3,a3)),a4)),
% 202.05/202.05 inference(scs_inference,[],[181,236,2])).
% 202.05/202.05 cnf(248,plain,
% 202.05/202.05 (~E(f2(f2(a3,a3),f2(f2(a3,a3),a1)),f2(f2(x2481,a1),x2482))),
% 202.05/202.05 inference(scs_inference,[],[229,44,3])).
% 202.05/202.05 cnf(251,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(x2511,x2512),x2511),x2513))),
% 202.05/202.05 inference(scs_inference,[],[145,56,3])).
% 202.05/202.05 cnf(254,plain,
% 202.05/202.05 (~E(f2(a3,f2(a3,x2541)),f2(f2(f2(x2542,x2543),x2542),x2544))),
% 202.05/202.05 inference(scs_inference,[],[183,56,3])).
% 202.05/202.05 cnf(256,plain,
% 202.05/202.05 (~E(f2(f2(a3,a3),f2(f2(a3,a3),a1)),f2(f2(a4,x2561),x2562))),
% 202.05/202.05 inference(scs_inference,[],[229,50,3])).
% 202.05/202.05 cnf(259,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(x2591,a1),x2592))),
% 202.05/202.05 inference(scs_inference,[],[145,44,3])).
% 202.05/202.05 cnf(265,plain,
% 202.05/202.05 (~E(f2(a3,a4),f2(f2(f2(a4,x2651),x2652),f2(a4,x2653)))),
% 202.05/202.05 inference(scs_inference,[],[149,47,3])).
% 202.05/202.05 cnf(274,plain,
% 202.05/202.05 (~E(f2(a1,a3),f2(f2(f2(x2741,x2742),f2(x2743,x2742)),f2(f2(x2741,x2743),x2742)))),
% 202.05/202.05 inference(scs_inference,[],[53,9,3])).
% 202.05/202.05 cnf(276,plain,
% 202.05/202.05 (~E(f2(a1,a3),f2(f2(x2761,x2762),x2761))),
% 202.05/202.05 inference(scs_inference,[],[53,8,3])).
% 202.05/202.05 cnf(277,plain,
% 202.05/202.05 (~E(a1,f2(a3,x2771))),
% 202.05/202.05 inference(scs_inference,[],[53,8,3,4])).
% 202.05/202.05 cnf(279,plain,
% 202.05/202.05 (~E(f2(a1,a3),f2(a4,x2791))),
% 202.05/202.05 inference(scs_inference,[],[53,7,3])).
% 202.05/202.05 cnf(280,plain,
% 202.05/202.05 (~E(a1,a4)),
% 202.05/202.05 inference(scs_inference,[],[53,7,3,4])).
% 202.05/202.05 cnf(281,plain,
% 202.05/202.05 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a3)),a4)),
% 202.05/202.05 inference(scs_inference,[],[53,147,8,7,3,4,11])).
% 202.05/202.05 cnf(286,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(x2861,a1))),
% 202.05/202.06 inference(scs_inference,[],[53,6,3])).
% 202.05/202.06 cnf(296,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(a4,x2961),f2(a4,x2962)),x2963))),
% 202.05/202.06 inference(scs_inference,[],[64,73,3])).
% 202.05/202.06 cnf(300,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(a4,x3001),x3002),a4))),
% 202.05/202.06 inference(scs_inference,[],[66,48,3])).
% 202.05/202.06 cnf(312,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(f2(a4,x3121),x3122),x3123),f2(a4,x3122)))),
% 202.05/202.06 inference(scs_inference,[],[66,76,3])).
% 202.05/202.06 cnf(322,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x3221,x3222),x3221),x3223))),
% 202.05/202.06 inference(scs_inference,[],[77,56,3])).
% 202.05/202.06 cnf(325,plain,
% 202.05/202.06 (~E(a3,f2(f2(x3251,a1),x3252))),
% 202.05/202.06 inference(scs_inference,[],[77,44,3])).
% 202.05/202.06 cnf(330,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x3301,x3301),f2(x3302,x3301)),a4))),
% 202.05/202.06 inference(scs_inference,[],[80,59,3])).
% 202.05/202.06 cnf(345,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(f2(a4,x3451),x3452),f2(a4,x3453)),f2(x3454,a1)))),
% 202.05/202.06 inference(scs_inference,[],[97,37,3])).
% 202.05/202.06 cnf(354,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(x3541,x3542),a4),f2(f2(x3541,a4),x3542)))),
% 202.05/202.06 inference(scs_inference,[],[108,70,3])).
% 202.05/202.06 cnf(371,plain,
% 202.05/202.06 (~E(a3,f2(f2(x3711,x3711),f2(x3712,a1)))),
% 202.05/202.06 inference(scs_inference,[],[125,37,3])).
% 202.05/202.06 cnf(374,plain,
% 202.05/202.06 (~E(a3,f2(f2(x3741,x3741),f2(f2(x3742,x3743),x3742)))),
% 202.05/202.06 inference(scs_inference,[],[125,58,3])).
% 202.05/202.06 cnf(382,plain,
% 202.05/202.06 (~E(a3,f2(f2(x3821,x3821),f2(f2(a4,x3822),x3823)))),
% 202.05/202.06 inference(scs_inference,[],[134,79,3])).
% 202.05/202.06 cnf(390,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(a4,x3901),x3902))),
% 202.05/202.06 inference(scs_inference,[],[145,50,3])).
% 202.05/202.06 cnf(394,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(x3941,a1),x3942),a4))),
% 202.05/202.06 inference(scs_inference,[],[147,38,3])).
% 202.05/202.06 cnf(398,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(f2(a4,x3981),x3982),x3983),f2(a4,x3982)))),
% 202.05/202.06 inference(scs_inference,[],[147,76,3])).
% 202.05/202.06 cnf(435,plain,
% 202.05/202.06 (~E(f2(a3,f2(a3,x4351)),f2(f2(a4,x4352),x4353))),
% 202.05/202.06 inference(scs_inference,[],[183,50,3])).
% 202.05/202.06 cnf(478,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(x4781,x4782),f2(x4783,x4782)),f2(f2(x4781,x4783),x4782)))),
% 202.05/202.06 inference(scs_inference,[],[247,9,3])).
% 202.05/202.06 cnf(480,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(x4801,x4802),x4801))),
% 202.05/202.06 inference(scs_inference,[],[247,8,3])).
% 202.05/202.06 cnf(481,plain,
% 202.05/202.06 (~E(a1,f2(f2(a3,a3),x4811))),
% 202.05/202.06 inference(scs_inference,[],[247,8,3,4])).
% 202.05/202.06 cnf(483,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(a4,x4831))),
% 202.05/202.06 inference(scs_inference,[],[247,7,3])).
% 202.05/202.06 cnf(485,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(x4851,a1))),
% 202.05/202.06 inference(scs_inference,[],[247,6,3])).
% 202.05/202.06 cnf(489,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(a4,x4891),f2(a4,x4892)),x4893))),
% 202.05/202.06 inference(scs_inference,[],[251,73,3])).
% 202.05/202.06 cnf(498,plain,
% 202.05/202.06 (~E(f2(a3,f2(a3,x4981)),f2(f2(f2(a4,x4982),f2(a4,x4983)),x4984))),
% 202.05/202.06 inference(scs_inference,[],[254,73,3])).
% 202.05/202.06 cnf(501,plain,
% 202.05/202.06 (~E(f2(a3,f2(a3,x5011)),f2(f2(f2(f2(a4,x5012),x5013),a4),f2(a4,x5014)))),
% 202.05/202.06 inference(scs_inference,[],[254,85,3])).
% 202.05/202.06 cnf(509,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(a4,x5091),x5092),f2(f2(a4,x5093),x5094)))),
% 202.05/202.06 inference(scs_inference,[],[265,79,3])).
% 202.05/202.06 cnf(513,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x5131,x5131),f2(x5132,x5131)),a4))),
% 202.05/202.06 inference(scs_inference,[],[274,59,3])).
% 202.05/202.06 cnf(521,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x5211,x5212),a4),f2(f2(x5211,a4),x5212)))),
% 202.05/202.06 inference(scs_inference,[],[274,70,3])).
% 202.05/202.06 cnf(530,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(a4,x5301),x5302),a4))),
% 202.05/202.06 inference(scs_inference,[],[276,48,3])).
% 202.05/202.06 cnf(565,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x5651,x5652),x5651),x5653))),
% 202.05/202.06 inference(scs_inference,[],[279,56,3])).
% 202.05/202.06 cnf(567,plain,
% 202.05/202.06 (~E(a1,f2(f2(x5671,x5672),x5671))),
% 202.05/202.06 inference(scs_inference,[],[279,56,3,4])).
% 202.05/202.06 cnf(569,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(x5691,a1),x5692))),
% 202.05/202.06 inference(scs_inference,[],[279,44,3])).
% 202.05/202.06 cnf(571,plain,
% 202.05/202.06 (~E(a1,f2(x5711,a1))),
% 202.05/202.06 inference(scs_inference,[],[279,44,3,4])).
% 202.05/202.06 cnf(575,plain,
% 202.05/202.06 (~E(a1,f2(a4,x5751))),
% 202.05/202.06 inference(scs_inference,[],[279,50,3,4])).
% 202.05/202.06 cnf(577,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x5771,x5772),f2(x5773,x5772)),f2(f2(x5771,x5773),x5772)))),
% 202.05/202.06 inference(scs_inference,[],[280,9,3])).
% 202.05/202.06 cnf(582,plain,
% 202.05/202.06 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a3)),f2(a4,x5821))),
% 202.05/202.06 inference(scs_inference,[],[281,7,3])).
% 202.05/202.06 cnf(584,plain,
% 202.05/202.06 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a3)),f2(x5841,a1))),
% 202.05/202.06 inference(scs_inference,[],[281,6,3])).
% 202.05/202.06 cnf(586,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),a4)),
% 202.05/202.06 inference(scs_inference,[],[281,277,6,3,5,11])).
% 202.05/202.06 cnf(599,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(a4,x5991),x5992),f2(x5993,a1)))),
% 202.05/202.06 inference(scs_inference,[],[300,37,3])).
% 202.05/202.06 cnf(616,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(f2(a4,x6161),x6162),f2(a4,x6163)),a4))),
% 202.05/202.06 inference(scs_inference,[],[312,84,3])).
% 202.05/202.06 cnf(621,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(f2(a4,x6211),x6212),a4),f2(a4,x6213)))),
% 202.05/202.06 inference(scs_inference,[],[322,85,3])).
% 202.05/202.06 cnf(625,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(a4,x6251),f2(a4,x6252)),x6253))),
% 202.05/202.06 inference(scs_inference,[],[322,73,3])).
% 202.05/202.06 cnf(635,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x6351,x6351),a4),a4))),
% 202.05/202.06 inference(scs_inference,[],[330,70,3])).
% 202.05/202.06 cnf(639,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x6391,x6391),f2(x6392,x6391)),f2(a4,x6393)))),
% 202.05/202.06 inference(scs_inference,[],[330,47,3])).
% 202.05/202.06 cnf(642,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x6421,x6421),f2(x6422,x6421)),f2(f2(x6423,x6424),x6423)))),
% 202.05/202.06 inference(scs_inference,[],[330,58,3])).
% 202.05/202.06 cnf(656,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(f2(a4,x6561),x6562),a4),f2(x6563,a1)))),
% 202.05/202.06 inference(scs_inference,[],[345,70,3])).
% 202.05/202.06 cnf(660,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(x6601,x6602),f2(a4,x6603)),f2(f2(x6601,a4),x6602)))),
% 202.05/202.06 inference(scs_inference,[],[354,73,3])).
% 202.05/202.06 cnf(677,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(x6771,a1),x6772),f2(a4,x6773)))),
% 202.05/202.06 inference(scs_inference,[],[394,47,3])).
% 202.05/202.06 cnf(680,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(x6801,a1),x6802),f2(f2(x6803,x6804),x6803)))),
% 202.05/202.06 inference(scs_inference,[],[394,58,3])).
% 202.05/202.06 cnf(687,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(f2(a4,x6871),x6872),f2(a4,x6873)),a4))),
% 202.05/202.06 inference(scs_inference,[],[398,84,3])).
% 202.05/202.06 cnf(747,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(x7471,x7471),f2(x7472,x7471)),a4))),
% 202.05/202.06 inference(scs_inference,[],[478,59,3])).
% 202.05/202.06 cnf(779,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(f2(a4,x7791),x7792),x7793),f2(a4,x7792)))),
% 202.05/202.06 inference(scs_inference,[],[480,76,3])).
% 202.05/202.06 cnf(798,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(x7981,x7982),x7981),x7983))),
% 202.05/202.06 inference(scs_inference,[],[483,56,3])).
% 202.05/202.06 cnf(801,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(x8011,a1),x8012))),
% 202.05/202.06 inference(scs_inference,[],[483,44,3])).
% 202.05/202.06 cnf(804,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(a4,x8041),x8042))),
% 202.05/202.06 inference(scs_inference,[],[483,50,3])).
% 202.05/202.06 cnf(813,plain,
% 202.05/202.06 (~E(f2(a3,f2(a3,x8131)),f2(f2(f2(f2(a4,x8132),x8133),f2(a4,x8134)),f2(a4,x8135)))),
% 202.05/202.06 inference(scs_inference,[],[501,73,3])).
% 202.05/202.06 cnf(817,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x8171,x8171),a4),f2(a4,x8172)))),
% 202.05/202.06 inference(scs_inference,[],[513,85,3])).
% 202.05/202.06 cnf(827,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x8271,x8271),f2(x8272,x8271)),f2(f2(x8273,x8274),x8273)))),
% 202.05/202.06 inference(scs_inference,[],[513,58,3])).
% 202.05/202.06 cnf(834,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x8341,x8342),f2(a4,x8343)),f2(f2(x8341,a4),x8342)))),
% 202.05/202.06 inference(scs_inference,[],[521,73,3])).
% 202.05/202.06 cnf(838,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(a4,x8381),x8382),f2(a4,x8383)))),
% 202.05/202.06 inference(scs_inference,[],[530,47,3])).
% 202.05/202.06 cnf(843,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(a4,x8431),x8432),f2(x8433,a1)))),
% 202.05/202.06 inference(scs_inference,[],[530,37,3])).
% 202.05/202.06 cnf(865,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(f2(a4,x8651),x8652),a4),f2(a4,x8653)))),
% 202.05/202.06 inference(scs_inference,[],[565,85,3])).
% 202.05/202.06 cnf(869,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(a4,x8691),f2(a4,x8692)),x8693))),
% 202.05/202.06 inference(scs_inference,[],[565,73,3])).
% 202.05/202.06 cnf(875,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(a4,x8751),x8752),a4))),
% 202.05/202.06 inference(scs_inference,[],[567,48,3])).
% 202.05/202.06 cnf(878,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x8781,a1),x8782),a4))),
% 202.05/202.06 inference(scs_inference,[],[567,38,3])).
% 202.05/202.06 cnf(886,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(f2(a4,x8861),x8862),x8863),f2(a4,x8862)))),
% 202.05/202.06 inference(scs_inference,[],[567,76,3])).
% 202.05/202.06 cnf(903,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x9031,x9032),x9031),x9033))),
% 202.05/202.06 inference(scs_inference,[],[575,56,3])).
% 202.05/202.06 cnf(906,plain,
% 202.05/202.06 (~E(a1,f2(f2(x9061,a1),x9062))),
% 202.05/202.06 inference(scs_inference,[],[575,44,3])).
% 202.05/202.06 cnf(909,plain,
% 202.05/202.06 (~E(a1,f2(f2(a4,x9091),x9092))),
% 202.05/202.06 inference(scs_inference,[],[575,50,3])).
% 202.05/202.06 cnf(912,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x9121,x9121),f2(x9122,x9121)),a4))),
% 202.05/202.06 inference(scs_inference,[],[577,59,3])).
% 202.05/202.06 cnf(940,plain,
% 202.05/202.06 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a3)),f2(f2(a4,x9401),x9402))),
% 202.05/202.06 inference(scs_inference,[],[582,50,3])).
% 202.05/202.06 cnf(944,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x9441,x9442),f2(x9443,x9442)),f2(f2(x9441,x9443),x9442)))),
% 202.05/202.06 inference(scs_inference,[],[586,9,3])).
% 202.05/202.06 cnf(945,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(x9451,x9452),x9451))),
% 202.05/202.06 inference(scs_inference,[],[586,8,3])).
% 202.05/202.06 cnf(946,plain,
% 202.05/202.06 (~E(a1,f2(f2(a3,a4),x9461))),
% 202.05/202.06 inference(scs_inference,[],[586,8,3,4])).
% 202.05/202.06 cnf(948,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(a4,x9481))),
% 202.05/202.06 inference(scs_inference,[],[586,7,3])).
% 202.05/202.06 cnf(950,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(x9501,a1))),
% 202.05/202.06 inference(scs_inference,[],[586,6,3])).
% 202.05/202.06 cnf(969,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(f2(a4,x9691),x9692),f2(a4,x9693)),f2(x9694,a1)))),
% 202.05/202.06 inference(scs_inference,[],[616,37,3])).
% 202.05/202.06 cnf(987,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x9871,x9871),a4),f2(x9872,a1)))),
% 202.05/202.06 inference(scs_inference,[],[635,37,3])).
% 202.05/202.06 cnf(991,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(x9911,x9911),f2(x9912,x9911)),f2(f2(a4,x9913),x9914)))),
% 202.05/202.06 inference(scs_inference,[],[639,79,3])).
% 202.05/202.06 cnf(1001,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(x10011,a1),x10012),f2(f2(a4,x10013),x10014)))),
% 202.05/202.06 inference(scs_inference,[],[677,79,3])).
% 202.05/202.06 cnf(1008,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(f2(a4,x10081),x10082),f2(a4,x10083)),f2(x10084,a1)))),
% 202.05/202.06 inference(scs_inference,[],[687,37,3])).
% 202.05/202.06 cnf(1049,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(x10491,x10491),a4),a4))),
% 202.05/202.06 inference(scs_inference,[],[747,70,3])).
% 202.05/202.06 cnf(1089,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(f2(a4,x10891),x10892),f2(a4,x10893)),a4))),
% 202.05/202.06 inference(scs_inference,[],[779,84,3])).
% 202.05/202.06 cnf(1093,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(f2(a4,x10931),x10932),a4),f2(a4,x10933)))),
% 202.05/202.06 inference(scs_inference,[],[798,85,3])).
% 202.05/202.06 cnf(1111,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x11111,x11111),a4),f2(f2(a4,x11112),x11113)))),
% 202.05/202.06 inference(scs_inference,[],[817,79,3])).
% 202.05/202.06 cnf(1128,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(a4,x11281),x11282),f2(f2(a4,x11283),x11284)))),
% 202.05/202.06 inference(scs_inference,[],[838,79,3])).
% 202.05/202.06 cnf(1152,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(a4,x11521),x11522),f2(f2(x11523,x11524),x11523)))),
% 202.05/202.06 inference(scs_inference,[],[875,58,3])).
% 202.05/202.06 cnf(1155,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(a4,x11551),x11552),f2(x11553,a1)))),
% 202.05/202.06 inference(scs_inference,[],[875,37,3])).
% 202.05/202.06 cnf(1166,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x11661,a1),x11662),f2(f2(x11663,x11664),x11663)))),
% 202.05/202.06 inference(scs_inference,[],[878,58,3])).
% 202.05/202.06 cnf(1169,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x11691,a1),x11692),f2(x11693,a1)))),
% 202.05/202.06 inference(scs_inference,[],[878,37,3])).
% 202.05/202.06 cnf(1173,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(f2(a4,x11731),x11732),f2(a4,x11733)),a4))),
% 202.05/202.06 inference(scs_inference,[],[886,84,3])).
% 202.05/202.06 cnf(1178,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(f2(a4,x11781),x11782),a4),f2(a4,x11783)))),
% 202.05/202.06 inference(scs_inference,[],[903,85,3])).
% 202.05/202.06 cnf(1182,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(a4,x11821),f2(a4,x11822)),x11823))),
% 202.05/202.06 inference(scs_inference,[],[903,73,3])).
% 202.05/202.06 cnf(1187,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x11871,x11871),a4),f2(a4,x11872)))),
% 202.05/202.06 inference(scs_inference,[],[912,85,3])).
% 202.05/202.06 cnf(1195,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x11951,x11951),f2(x11952,x11951)),f2(a4,x11953)))),
% 202.05/202.06 inference(scs_inference,[],[912,47,3])).
% 202.05/202.06 cnf(1198,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x11981,x11981),f2(x11982,x11981)),f2(f2(x11983,x11984),x11983)))),
% 202.05/202.06 inference(scs_inference,[],[912,58,3])).
% 202.05/202.06 cnf(1209,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x12091,x12091),f2(x12092,x12091)),a4))),
% 202.05/202.06 inference(scs_inference,[],[944,59,3])).
% 202.05/202.06 cnf(1235,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x12351),x12352),x12353),f2(a4,x12352)))),
% 202.05/202.06 inference(scs_inference,[],[945,76,3])).
% 202.05/202.06 cnf(1255,plain,
% 202.05/202.06 (~E(a1,f2(f2(a3,f2(a4,x12551)),x12552))),
% 202.05/202.06 inference(scs_inference,[],[946,73,3])).
% 202.05/202.06 cnf(1262,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x12621,x12622),x12621),x12623))),
% 202.05/202.06 inference(scs_inference,[],[948,56,3])).
% 202.05/202.06 cnf(1268,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(a4,x12681),x12682))),
% 202.05/202.06 inference(scs_inference,[],[948,50,3])).
% 202.05/202.06 cnf(1278,plain,
% 202.05/202.06 (~E(a3,f2(f2(f2(f2(a4,x12781),x12782),a4),f2(x12783,a1)))),
% 202.05/202.06 inference(scs_inference,[],[969,70,3])).
% 202.05/202.06 cnf(1297,plain,
% 202.05/202.06 (~E(f2(a3,a4),f2(f2(f2(f2(a4,x12971),x12972),a4),f2(x12973,a1)))),
% 202.05/202.06 inference(scs_inference,[],[1008,70,3])).
% 202.05/202.06 cnf(1326,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(x13261,x13261),a4),f2(x13262,a1)))),
% 202.05/202.06 inference(scs_inference,[],[1049,37,3])).
% 202.05/202.06 cnf(1346,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a3)),f2(f2(f2(f2(a4,x13461),x13462),f2(a4,x13463)),f2(a4,x13464)))),
% 202.05/202.06 inference(scs_inference,[],[1089,47,3])).
% 202.05/202.06 cnf(1361,plain,
% 202.05/202.06 (~E(f2(a1,a3),f2(f2(f2(x13611,x13611),f2(a4,x13612)),f2(f2(a4,x13613),x13614)))),
% 202.05/202.06 inference(scs_inference,[],[1111,73,3])).
% 202.05/202.06 cnf(1387,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(f2(a4,x13871),x13872),f2(a4,x13873)),f2(a4,x13874)))),
% 202.05/202.06 inference(scs_inference,[],[1173,47,3])).
% 202.05/202.06 cnf(1399,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x13991,x13991),f2(a4,x13992)),a4))),
% 202.05/202.06 inference(scs_inference,[],[1187,84,3])).
% 202.05/202.06 cnf(1404,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x14041,x14041),f2(a4,x14042)),f2(a4,x14043)))),
% 202.05/202.06 inference(scs_inference,[],[1187,73,3])).
% 202.05/202.06 cnf(1414,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x14141,x14141),f2(x14142,x14141)),f2(f2(a4,x14143),x14144)))),
% 202.05/202.06 inference(scs_inference,[],[1195,79,3])).
% 202.05/202.06 cnf(1420,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x14201,x14201),a4),f2(a4,x14202)))),
% 202.05/202.06 inference(scs_inference,[],[1209,85,3])).
% 202.05/202.06 cnf(1465,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x14651),x14652),f2(a4,x14653)),a4))),
% 202.05/202.06 inference(scs_inference,[],[1235,84,3])).
% 202.05/202.06 cnf(1469,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x14691),x14692),a4),f2(a4,x14693)))),
% 202.05/202.06 inference(scs_inference,[],[1262,85,3])).
% 202.05/202.06 cnf(1520,plain,
% 202.05/202.06 (~E(a1,f2(f2(f2(x15201,x15201),f2(a4,x15202)),f2(x15203,a1)))),
% 202.05/202.06 inference(scs_inference,[],[1399,37,3])).
% 202.05/202.06 cnf(1531,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x15311,x15311),f2(a4,x15312)),a4))),
% 202.05/202.06 inference(scs_inference,[],[1420,84,3])).
% 202.05/202.06 cnf(1566,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x15661),x15662),f2(a4,x15663)),f2(x15664,a1)))),
% 202.05/202.06 inference(scs_inference,[],[1465,37,3])).
% 202.05/202.06 cnf(1580,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(x15801,x15801),f2(a4,x15802)),f2(x15803,a1)))),
% 202.05/202.06 inference(scs_inference,[],[1531,37,3])).
% 202.05/202.06 cnf(1593,plain,
% 202.05/202.06 (~E(f2(a1,f2(a3,a4)),f2(f2(f2(f2(a4,x15931),x15932),a4),f2(x15933,a1)))),
% 202.05/202.06 inference(scs_inference,[],[1566,70,3])).
% 202.05/202.06 cnf(1608,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x16081,x16081),f2(x16082,x16081)),a4))),
% 202.05/202.06 inference(scs_inference,[],[20,59,3])).
% 202.05/202.06 cnf(1670,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x16701,a1),x16702),f2(a4,x16703)))),
% 202.05/202.06 inference(scs_inference,[],[165,47,3])).
% 202.05/202.06 cnf(1673,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x16731,a1),x16732),f2(f2(x16733,x16734),x16733)))),
% 202.05/202.06 inference(scs_inference,[],[165,58,3])).
% 202.05/202.06 cnf(1881,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x18811,x18811),a4),f2(a4,x18812)))),
% 202.05/202.06 inference(scs_inference,[],[1608,85,3])).
% 202.05/202.06 cnf(1892,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x18921,x18921),f2(x18922,x18921)),f2(f2(x18923,x18924),x18923)))),
% 202.05/202.06 inference(scs_inference,[],[1608,58,3])).
% 202.05/202.06 cnf(1899,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x18991,a1),x18992),f2(f2(a4,x18993),x18994)))),
% 202.05/202.06 inference(scs_inference,[],[1670,79,3])).
% 202.05/202.06 cnf(1905,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x19051,x19051),a4),f2(f2(a4,x19052),x19053)))),
% 202.05/202.06 inference(scs_inference,[],[1881,79,3])).
% 202.05/202.06 cnf(1930,plain,
% 202.05/202.06 (~E(f2(a3,a3),f2(f2(f2(x19301,x19301),f2(a4,x19302)),f2(f2(a4,x19303),x19304)))),
% 202.05/202.06 inference(scs_inference,[],[1905,73,3])).
% 202.05/202.06 cnf(2225,plain,
% 202.05/202.06 (~E(f2(x22251,a1),f2(a1,a3))),
% 202.05/202.06 inference(scs_inference,[],[286,56,5,2])).
% 202.05/202.06 cnf(2227,plain,
% 202.05/202.06 (~E(f2(a1,a4),a4)),
% 202.05/202.06 inference(scs_inference,[],[143,286,56,6,5,2,4,11])).
% 202.05/202.06 cnf(2232,plain,
% 202.05/202.06 (E(f2(x22321,f2(f2(x22322,a1),x22323)),f2(x22321,f2(a4,x22323)))),
% 202.05/202.06 inference(scs_inference,[],[44,5])).
% 202.05/202.06 cnf(2233,plain,
% 202.05/202.06 (~E(a4,f2(a1,a4))),
% 202.05/202.06 inference(scs_inference,[],[2227,44,5,2])).
% 202.05/202.06 cnf(2235,plain,
% 202.05/202.06 (~E(f2(f2(a1,a3),f2(f2(a1,a3),a1)),a4)),
% 202.05/202.06 inference(scs_inference,[],[2227,2225,44,8,5,2,4,11])).
% 202.05/202.06 cnf(2241,plain,
% 202.05/202.06 (E(f2(x22411,f2(f2(x22412,a1),f2(a4,x22413))),f2(x22411,f2(a4,a4)))),
% 202.05/202.06 inference(scs_inference,[],[211,5])).
% 202.05/202.06 cnf(2242,plain,
% 202.05/202.06 (~E(f2(x22421,a1),f2(a3,a4))),
% 202.05/202.06 inference(scs_inference,[],[142,211,5,2])).
% 202.05/202.06 cnf(2247,plain,
% 202.05/202.06 (~E(f2(f2(x22471,x22472),x22471),f2(a1,a4))),
% 202.05/202.06 inference(scs_inference,[],[2233,142,235,23,50,211,6,5,2,4,11,3])).
% 202.05/202.07 cnf(2249,plain,
% 202.05/202.07 (E(f2(x22491,f2(a4,a4)),f2(x22491,f2(f2(x22492,a1),f2(a4,x22493))))),
% 202.05/202.07 inference(scs_inference,[],[210,5])).
% 202.05/202.07 cnf(2250,plain,
% 202.05/202.07 (~E(f2(x22501,a1),a1)),
% 202.05/202.07 inference(scs_inference,[],[571,210,5,2])).
% 202.05/202.07 cnf(2252,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a1)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2242,571,210,8,5,2,4,11])).
% 202.05/202.07 cnf(2258,plain,
% 202.05/202.07 (E(f2(x22581,f2(a4,x22582)),f2(x22581,f2(f2(x22583,a1),x22582)))),
% 202.05/202.07 inference(scs_inference,[],[45,5])).
% 202.05/202.07 cnf(2259,plain,
% 202.05/202.07 (~E(f2(a1,a4),f2(f2(x22591,x22592),x22591))),
% 202.05/202.07 inference(scs_inference,[],[2247,45,5,2])).
% 202.05/202.07 cnf(2260,plain,
% 202.05/202.07 (E(f2(f2(f2(x22601,a1),f2(a4,x22602)),x22603),f2(f2(a4,a4),x22603))),
% 202.05/202.07 inference(scs_inference,[],[2247,211,45,5,2,4])).
% 202.05/202.07 cnf(2261,plain,
% 202.05/202.07 (~E(f2(a1,f2(x22611,a1)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2250,2247,211,45,6,5,2,4,11])).
% 202.05/202.07 cnf(2264,plain,
% 202.05/202.07 (~E(f2(f2(x22641,x22642),x22641),a1)),
% 202.05/202.07 inference(scs_inference,[],[2250,2247,143,23,211,45,6,5,2,4,11,3])).
% 202.05/202.07 cnf(2265,plain,
% 202.05/202.07 (E(f2(x22651,f2(x22652,a4)),f2(x22651,f2(x22652,f2(a4,x22653))))),
% 202.05/202.07 inference(scs_inference,[],[48,5])).
% 202.05/202.07 cnf(2266,plain,
% 202.05/202.07 (E(f2(f2(a4,x22661),x22662),f2(f2(f2(a4,x22663),x22661),x22662))),
% 202.05/202.07 inference(scs_inference,[],[51,48,5,4])).
% 202.05/202.07 cnf(2267,plain,
% 202.05/202.07 (~E(f2(x22671,a1),f2(a1,f2(a3,a4)))),
% 202.05/202.07 inference(scs_inference,[],[950,51,48,5,4,2])).
% 202.05/202.07 cnf(2268,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(x22681,x22682),x22681)),a4)),
% 202.05/202.07 inference(scs_inference,[],[950,2264,51,48,6,5,4,2,11])).
% 202.05/202.07 cnf(2271,plain,
% 202.05/202.07 (~E(f2(x22711,a1),f2(a1,a4))),
% 202.05/202.07 inference(scs_inference,[],[950,2264,2233,12,51,48,6,5,4,2,11,3])).
% 202.05/202.07 cnf(2273,plain,
% 202.05/202.07 (E(f2(x22731,f2(x22732,a4)),f2(x22731,f2(x22732,f2(x22733,a1))))),
% 202.05/202.07 inference(scs_inference,[],[38,5])).
% 202.05/202.07 cnf(2275,plain,
% 202.05/202.07 (E(f2(f2(a4,x22751),x22752),f2(f2(f2(x22753,a1),x22751),x22752))),
% 202.05/202.07 inference(scs_inference,[],[2271,45,38,5,2,4])).
% 202.05/202.07 cnf(2276,plain,
% 202.05/202.07 (~E(f2(f2(a1,a4),f2(f2(a1,a4),a1)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2271,45,8,38,5,2,4,11])).
% 202.05/202.07 cnf(2282,plain,
% 202.05/202.07 (E(f2(x22821,f2(x22822,f2(a4,x22823))),f2(x22821,f2(x22822,a4)))),
% 202.05/202.07 inference(scs_inference,[],[47,5])).
% 202.05/202.07 cnf(2283,plain,
% 202.05/202.07 (E(f2(f2(x22831,a4),x22832),f2(f2(x22831,f2(x22833,a1)),x22832))),
% 202.05/202.07 inference(scs_inference,[],[38,47,5,4])).
% 202.05/202.07 cnf(2284,plain,
% 202.05/202.07 (~E(f2(x22841,a1),f2(a1,f2(a3,a3)))),
% 202.05/202.07 inference(scs_inference,[],[485,38,47,5,4,2])).
% 202.05/202.07 cnf(2290,plain,
% 202.05/202.07 (~E(f2(x22901,a1),f2(a3,f2(a3,x22902)))),
% 202.05/202.07 inference(scs_inference,[],[180,37,5,2])).
% 202.05/202.07 cnf(2291,plain,
% 202.05/202.07 (E(f2(f2(x22911,f2(x22912,a1)),x22913),f2(f2(x22911,a4),x22913))),
% 202.05/202.07 inference(scs_inference,[],[180,37,5,2,4])).
% 202.05/202.07 cnf(2293,plain,
% 202.05/202.07 (~E(f2(f2(x22931,a1),x22932),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[569,2])).
% 202.05/202.07 cnf(2294,plain,
% 202.05/202.07 (~E(f2(f2(x22941,a1),f2(a4,x22942)),f2(a3,a3))),
% 202.05/202.07 inference(scs_inference,[],[569,49,210,2,3])).
% 202.05/202.07 cnf(2301,plain,
% 202.05/202.07 (~E(f2(f2(a4,x23011),x23012),f2(a3,a4))),
% 202.05/202.07 inference(scs_inference,[],[390,2])).
% 202.05/202.07 cnf(2305,plain,
% 202.05/202.07 (~E(f2(f2(x23051,a1),x23052),f2(a3,a4))),
% 202.05/202.07 inference(scs_inference,[],[259,2])).
% 202.05/202.07 cnf(2313,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),x23131),a1)),
% 202.05/202.07 inference(scs_inference,[],[481,2])).
% 202.05/202.07 cnf(2318,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(a3,a3),x23181)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2313,371,6,2,11])).
% 202.05/202.07 cnf(2327,plain,
% 202.05/202.07 (~E(f2(f2(a1,a4),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[186,2233,7,2,11])).
% 202.05/202.07 cnf(2330,plain,
% 202.05/202.07 (~E(f2(f2(f2(x23301,x23302),f2(x23303,x23302)),f2(f2(x23301,x23303),x23302)),f2(a1,a4))),
% 202.05/202.07 inference(scs_inference,[],[186,2233,19,7,2,11,3])).
% 202.05/202.07 cnf(2331,plain,
% 202.05/202.07 (~E(a4,f2(f2(a1,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2327,2])).
% 202.05/202.07 cnf(2332,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2327,55,7,2,11])).
% 202.05/202.07 cnf(2335,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,a3),a4))),
% 202.05/202.07 inference(scs_inference,[],[2332,2])).
% 202.05/202.07 cnf(2336,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),a4),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2331,2332,7,2,11])).
% 202.05/202.07 cnf(2339,plain,
% 202.05/202.07 (~E(f2(x23391,a1),f2(f2(a1,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2331,2332,12,7,2,11,3])).
% 202.05/202.07 cnf(2340,plain,
% 202.05/202.07 (~E(f2(f2(a1,a4),a4),f2(x23401,a1))),
% 202.05/202.07 inference(scs_inference,[],[2339,2])).
% 202.05/202.07 cnf(2341,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a3),a4),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2339,2335,7,2,11])).
% 202.05/202.07 cnf(2344,plain,
% 202.05/202.07 (~E(f2(f2(x23441,x23442),x23441),f2(f2(a3,a3),a4))),
% 202.05/202.07 inference(scs_inference,[],[2339,2335,23,7,2,11,3])).
% 202.05/202.07 cnf(2347,plain,
% 202.05/202.07 (~E(f2(f2(x23471,x23472),x23471),f2(f2(a1,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[325,2331,23,2,3])).
% 202.05/202.07 cnf(2349,plain,
% 202.05/202.07 (~E(f2(f2(x23491,a1),x23492),a1)),
% 202.05/202.07 inference(scs_inference,[],[906,2])).
% 202.05/202.07 cnf(2350,plain,
% 202.05/202.07 (~E(f2(x23501,a1),f2(f2(a3,a3),a4))),
% 202.05/202.07 inference(scs_inference,[],[906,2335,12,2,3])).
% 202.05/202.07 cnf(2352,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),a4),f2(x23521,a1))),
% 202.05/202.07 inference(scs_inference,[],[2350,2])).
% 202.05/202.07 cnf(2353,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(x23531,a1),x23532)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2350,2349,6,2,11])).
% 202.05/202.07 cnf(2357,plain,
% 202.05/202.07 (~E(f2(f2(a4,x23571),x23572),a1)),
% 202.05/202.07 inference(scs_inference,[],[909,2])).
% 202.05/202.07 cnf(2359,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(x23591,a1)))),
% 202.05/202.07 inference(scs_inference,[],[2261,2])).
% 202.05/202.07 cnf(2360,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(a4,x23601),x23602)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2357,2261,6,2,11])).
% 202.05/202.07 cnf(2365,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(x23651,a1)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2359,2347,7,2,11])).
% 202.05/202.07 cnf(2383,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x23831),x23832),f2(x23833,a1)),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[843,2])).
% 202.05/202.07 cnf(2402,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),a4),f2(f2(x24021,x24022),x24021))),
% 202.05/202.07 inference(scs_inference,[],[2344,2])).
% 202.05/202.07 cnf(2407,plain,
% 202.05/202.07 (~E(f2(f2(a4,x24071),x24072),f2(a1,f2(a3,a4)))),
% 202.05/202.07 inference(scs_inference,[],[1268,2])).
% 202.05/202.07 cnf(2409,plain,
% 202.05/202.07 (~E(f2(f2(x24091,a1),x24092),f2(a1,f2(a3,a3)))),
% 202.05/202.07 inference(scs_inference,[],[801,2])).
% 202.05/202.07 cnf(2411,plain,
% 202.05/202.07 (~E(f2(f2(a4,x24111),x24112),f2(a1,f2(a3,a3)))),
% 202.05/202.07 inference(scs_inference,[],[804,2])).
% 202.05/202.07 cnf(2417,plain,
% 202.05/202.07 (~E(f2(f2(a4,x24171),x24172),f2(a3,f2(a3,x24173)))),
% 202.05/202.07 inference(scs_inference,[],[435,2])).
% 202.05/202.07 cnf(2428,plain,
% 202.05/202.07 (~E(f2(f2(f2(x24281,x24281),f2(a4,x24282)),f2(a4,x24283)),a1)),
% 202.05/202.07 inference(scs_inference,[],[1404,2])).
% 202.05/202.07 cnf(2430,plain,
% 202.05/202.07 (~E(f2(f2(f2(x24301,x24301),f2(a4,x24302)),f2(x24303,a1)),a1)),
% 202.05/202.07 inference(scs_inference,[],[1520,2])).
% 202.05/202.07 cnf(2431,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(f2(x24311,x24311),f2(a4,x24312)),f2(a4,x24313))),a4)),
% 202.05/202.07 inference(scs_inference,[],[1520,2428,6,2,11])).
% 202.05/202.07 cnf(2436,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(f2(x24361,x24361),f2(a4,x24362)),f2(x24363,a1))),a4)),
% 202.05/202.07 inference(scs_inference,[],[2430,599,6,2,11])).
% 202.05/202.07 cnf(2442,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x24421),x24422),f2(x24423,a1)),a1)),
% 202.05/202.07 inference(scs_inference,[],[1155,2])).
% 202.05/202.07 cnf(2444,plain,
% 202.05/202.07 (~E(f2(f2(f2(x24441,a1),x24442),f2(x24443,a1)),a1)),
% 202.05/202.07 inference(scs_inference,[],[1169,2])).
% 202.05/202.07 cnf(2445,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(f2(a4,x24451),x24452),f2(x24453,a1))),a4)),
% 202.05/202.07 inference(scs_inference,[],[1169,2442,6,2,11])).
% 202.05/202.07 cnf(2449,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(f2(x24491,a1),x24492),f2(x24493,a1))),a4)),
% 202.05/202.07 inference(scs_inference,[],[2444,987,6,2,11])).
% 202.05/202.07 cnf(2455,plain,
% 202.05/202.07 (~E(f2(x24551,a1),f2(f2(a3,a4),f2(f2(a3,a4),a3)))),
% 202.05/202.07 inference(scs_inference,[],[584,2])).
% 202.05/202.07 cnf(2475,plain,
% 202.05/202.07 (~E(f2(f2(f2(x24751,a1),x24752),f2(a3,a4)),a4)+~E(f2(f2(a3,a4),f2(f2(x24751,a1),x24752)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2305,1580,2,11])).
% 202.05/202.07 cnf(2489,plain,
% 202.05/202.07 (~E(f2(f2(f2(x24891,a1),f2(a4,x24892)),f2(a3,a3)),a4)+~E(f2(f2(a3,a3),f2(f2(x24891,a1),f2(a4,x24892))),a4)),
% 202.05/202.07 inference(scs_inference,[],[2294,1326,2,11])).
% 202.05/202.07 cnf(2502,plain,
% 202.05/202.07 (~E(a4,f2(f2(f2(a1,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2336,2])).
% 202.05/202.07 cnf(2503,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x25031),f2(a4,x25032)),x25033),f2(a3,a4))),
% 202.05/202.07 inference(scs_inference,[],[489,2])).
% 202.05/202.07 cnf(2504,plain,
% 202.05/202.07 (~E(f2(x25041,a1),f2(f2(f2(a1,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2502,489,12,2,3])).
% 202.05/202.07 cnf(2509,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(x25091,a1)),a4),f2(x25092,a1))),
% 202.05/202.07 inference(scs_inference,[],[2340,869,2283,2,3])).
% 202.05/202.07 cnf(2512,plain,
% 202.05/202.07 (~E(f2(f2(x25121,x25122),x25121),f2(f2(f2(a1,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2509,2502,23,2,3])).
% 202.05/202.07 cnf(2513,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x25131),f2(a4,x25132)),x25133),f2(a3,a3))),
% 202.05/202.07 inference(scs_inference,[],[296,2])).
% 202.05/202.07 cnf(2514,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(x25141,x25142),x25141)),f2(x25143,a1))),
% 202.05/202.07 inference(scs_inference,[],[2352,296,59,2,3])).
% 202.05/202.07 cnf(2516,plain,
% 202.05/202.07 (~E(f2(x25161,a1),f2(f2(a3,a3),f2(f2(x25162,x25163),x25162)))),
% 202.05/202.07 inference(scs_inference,[],[2514,2])).
% 202.05/202.07 cnf(2517,plain,
% 202.05/202.07 (~E(f2(a4,x25171),f2(f2(f2(a1,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2514,2502,13,2,3])).
% 202.05/202.07 cnf(2521,plain,
% 202.05/202.07 (~E(a4,f2(f2(a1,a4),f2(f2(a1,a4),a1)))),
% 202.05/202.07 inference(scs_inference,[],[2276,2])).
% 202.05/202.07 cnf(2522,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(x25221,x25222),x25221)),f2(f2(x25223,x25224),x25223))),
% 202.05/202.07 inference(scs_inference,[],[2259,2276,59,2,3])).
% 202.05/202.07 cnf(2524,plain,
% 202.05/202.07 (~E(a4,f2(f2(f2(a3,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2341,2])).
% 202.05/202.07 cnf(2526,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),a4),a4),f2(x25261,a1))),
% 202.05/202.07 inference(scs_inference,[],[2504,2])).
% 202.05/202.07 cnf(2530,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),a4),a4),f2(a4,x25301))),
% 202.05/202.07 inference(scs_inference,[],[2517,2])).
% 202.05/202.07 cnf(2531,plain,
% 202.05/202.07 (~E(f2(f2(x25311,x25312),x25311),f2(f2(f2(a3,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2517,2524,23,2,3])).
% 202.05/202.07 cnf(2540,plain,
% 202.05/202.07 (~E(f2(f2(x25401,x25402),x25401),f2(f2(a1,a4),f2(f2(a1,a4),a1)))),
% 202.05/202.07 inference(scs_inference,[],[374,2521,23,2,3])).
% 202.05/202.07 cnf(2543,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(x25431,x25432),x25431)),f2(f2(x25433,x25434),x25433))),
% 202.05/202.07 inference(scs_inference,[],[2402,382,59,2,3])).
% 202.05/202.07 cnf(2546,plain,
% 202.05/202.07 (~E(f2(x25461,a1),f2(f2(f2(a3,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[625,2524,12,2,3])).
% 202.05/202.07 cnf(2551,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),f2(x25511,a1)),a4),f2(x25512,a1))),
% 202.05/202.07 inference(scs_inference,[],[2526,2546,2283,2,3])).
% 202.05/202.07 cnf(2553,plain,
% 202.05/202.07 (~E(f2(x25531,a1),f2(f2(f2(a1,a4),f2(x25532,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2551,2])).
% 202.05/202.07 cnf(2554,plain,
% 202.05/202.07 (~E(f2(a4,x25541),f2(f2(a1,a4),f2(f2(a1,a4),a1)))),
% 202.05/202.07 inference(scs_inference,[],[2551,2521,13,2,3])).
% 202.05/202.07 cnf(2556,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),f2(x25561,a1)),a4),f2(a4,x25562))),
% 202.05/202.07 inference(scs_inference,[],[2530,2554,2283,2,3])).
% 202.05/202.07 cnf(2558,plain,
% 202.05/202.07 (~E(f2(a4,x25581),f2(f2(f2(a1,a4),f2(x25582,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2556,2])).
% 202.05/202.07 cnf(2559,plain,
% 202.05/202.07 (~E(f2(a4,x25591),f2(f2(f2(a3,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2556,2524,13,2,3])).
% 202.05/202.07 cnf(2563,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a3),a4),a4),f2(a4,x25631))),
% 202.05/202.07 inference(scs_inference,[],[2559,2])).
% 202.05/202.07 cnf(2567,plain,
% 202.05/202.07 (~E(f2(f2(x25671,a1),f2(a4,x25672)),f2(f2(f2(a1,a4),f2(x25673,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2558,1182,210,2,3])).
% 202.05/202.07 cnf(2569,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,a4),f2(f2(a3,a4),a1)))),
% 202.05/202.07 inference(scs_inference,[],[2252,2])).
% 202.05/202.07 cnf(2573,plain,
% 202.05/202.07 (~E(f2(x25731,a1),f2(f2(a3,a4),f2(f2(a3,a4),a1)))),
% 202.05/202.07 inference(scs_inference,[],[2569,2235,12,2,3])).
% 202.05/202.07 cnf(2577,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a1)),f2(x25771,a1))),
% 202.05/202.07 inference(scs_inference,[],[2573,2])).
% 202.05/202.07 cnf(2582,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x25821)),x25822),a1)),
% 202.05/202.07 inference(scs_inference,[],[1255,2])).
% 202.05/202.07 cnf(2583,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a3),f2(x25831,a1)),a4),f2(a4,x25832))),
% 202.05/202.07 inference(scs_inference,[],[2563,1255,2283,2,3])).
% 202.05/202.07 cnf(2586,plain,
% 202.05/202.07 (~E(f2(f2(x25861,x25862),x25861),f2(f2(a3,a4),f2(f2(a3,a4),a1)))),
% 202.05/202.07 inference(scs_inference,[],[2583,2569,23,2,3])).
% 202.05/202.07 cnf(2590,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(x25901,x25902),x25901)))),
% 202.05/202.07 inference(scs_inference,[],[2268,2])).
% 202.05/202.07 cnf(2591,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(x25911,a1)),f2(f2(a3,a4),a1)),f2(x25912,a1))),
% 202.05/202.07 inference(scs_inference,[],[2577,2268,2283,2,3])).
% 202.05/202.07 cnf(2594,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(a3,a3),x25941)))),
% 202.05/202.07 inference(scs_inference,[],[2318,2])).
% 202.05/202.07 cnf(2596,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(x25961,a1),x25962)))),
% 202.05/202.07 inference(scs_inference,[],[2353,2])).
% 202.05/202.07 cnf(2597,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(a3,a4)))),
% 202.05/202.07 inference(scs_inference,[],[6,2267,2353,2,3])).
% 202.05/202.07 cnf(2599,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(a4,x25991),x25992)))),
% 202.05/202.07 inference(scs_inference,[],[2360,2])).
% 202.05/202.07 cnf(2601,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(a3,a4)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2597,2360,19,7,2,3,11])).
% 202.05/202.07 cnf(2605,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(a3,a3)))),
% 202.05/202.07 inference(scs_inference,[],[6,2284,2601,2,3])).
% 202.05/202.07 cnf(2607,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(a3,a3),a3)),a4)),
% 202.05/202.07 inference(scs_inference,[],[6,2284,2601,60,8,2,3,11])).
% 202.05/202.07 cnf(2613,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(a3,a3)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2605,2607,19,7,2,3,11])).
% 202.05/202.07 cnf(2617,plain,
% 202.05/202.07 (~E(a4,f2(a3,f2(a3,x26171)))),
% 202.05/202.07 inference(scs_inference,[],[6,2290,2613,2,3])).
% 202.05/202.07 cnf(2619,plain,
% 202.05/202.07 (~E(f2(a1,f2(a3,x26191)),a4)),
% 202.05/202.07 inference(scs_inference,[],[6,2290,2613,181,2,3,11])).
% 202.05/202.07 cnf(2622,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(a3,x26221)))),
% 202.05/202.07 inference(scs_inference,[],[2619,2])).
% 202.05/202.07 cnf(2624,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a3,x26241)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2617,2619,23,7,2,3,11])).
% 202.05/202.07 cnf(2627,plain,
% 202.05/202.07 (~E(a4,f2(f2(a1,f2(x26271,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2365,2])).
% 202.05/202.07 cnf(2629,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(a3,x26291)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2622,2365,12,7,2,3,11])).
% 202.05/202.07 cnf(2637,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,f2(a3,x26371)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2624,2])).
% 202.05/202.07 cnf(2638,plain,
% 202.05/202.07 (~E(a4,f2(a3,a4))),
% 202.05/202.07 inference(scs_inference,[],[6,2503,2624,2,3])).
% 202.05/202.07 cnf(2641,plain,
% 202.05/202.07 (~E(a4,f2(f2(a1,f2(a3,x26411)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2629,2])).
% 202.05/202.07 cnf(2642,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2638,2629,7,2,11])).
% 202.05/202.07 cnf(2646,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2642,2])).
% 202.05/202.07 cnf(2647,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a4),a4),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[7,2642,2,11])).
% 202.05/202.07 cnf(2650,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(x26501,a1)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[7,2642,2283,2,11,3])).
% 202.05/202.07 cnf(2652,plain,
% 202.05/202.07 (~E(a4,f2(f2(f2(a3,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2647,2])).
% 202.05/202.07 cnf(2658,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,f2(x26581,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2650,2])).
% 202.05/202.07 cnf(2674,plain,
% 202.05/202.07 (~E(f2(x26741,a1),f2(a1,f2(f2(x26742,a1),x26743)))),
% 202.05/202.07 inference(scs_inference,[],[2596,2330,12,2,3])).
% 202.05/202.07 cnf(2678,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(x26781,a1),x26782)),f2(x26783,a1))),
% 202.05/202.07 inference(scs_inference,[],[2674,2])).
% 202.05/202.07 cnf(2694,plain,
% 202.05/202.07 (~E(a4,f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[8,2383,2591,2,3])).
% 202.05/202.07 cnf(2697,plain,
% 202.05/202.07 (~E(f2(f2(x26971,x26972),x26971),f2(f2(a3,a3),f2(f2(x26973,x26974),x26973)))),
% 202.05/202.07 inference(scs_inference,[],[2543,2])).
% 202.05/202.07 cnf(2698,plain,
% 202.05/202.07 (~E(f2(f2(f2(x26981,x26982),f2(x26983,x26982)),f2(f2(x26981,x26983),x26982)),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[2694,2543,19,2,3])).
% 202.05/202.07 cnf(2699,plain,
% 202.05/202.07 (~E(f2(f2(a1,a3),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2694,2543,19,7,2,3,11])).
% 202.05/202.07 cnf(2702,plain,
% 202.05/202.07 (~E(a4,f2(f2(a1,a3),a4))),
% 202.05/202.07 inference(scs_inference,[],[2699,2])).
% 202.05/202.07 cnf(2703,plain,
% 202.05/202.07 (~E(f2(f2(a1,a3),f2(f2(x27031,x27032),x27031)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2699,59,2,3])).
% 202.05/202.07 cnf(2705,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a3),a4),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2699,59,7,2,3,11])).
% 202.05/202.07 cnf(2708,plain,
% 202.05/202.07 (~E(a4,f2(f2(f2(a1,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2705,2])).
% 202.05/202.07 cnf(2709,plain,
% 202.05/202.07 (~E(f2(f2(f2(x27091,x27092),f2(x27093,x27092)),f2(f2(x27091,x27093),x27092)),f2(f2(a1,a3),a4))),
% 202.05/202.07 inference(scs_inference,[],[2702,2705,19,2,3])).
% 202.05/202.07 cnf(2710,plain,
% 202.05/202.07 (~E(a4,f2(f2(a1,a3),f2(f2(x27101,x27102),x27101)))),
% 202.05/202.07 inference(scs_inference,[],[2703,2])).
% 202.05/202.07 cnf(2711,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,a3),f2(f2(x27111,x27112),x27111)))),
% 202.05/202.07 inference(scs_inference,[],[8,2516,2703,2,3])).
% 202.05/202.07 cnf(2714,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(x27141,x27142),x27141)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2711,2])).
% 202.05/202.07 cnf(2715,plain,
% 202.05/202.07 (~E(f2(x27151,a1),f2(f2(a1,a3),f2(f2(x27152,x27153),x27152)))),
% 202.05/202.07 inference(scs_inference,[],[2710,2711,12,2,3])).
% 202.05/202.07 cnf(2720,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,a4),f2(f2(a3,a4),a3)))),
% 202.05/202.07 inference(scs_inference,[],[8,2715,2455,2,3])).
% 202.05/202.07 cnf(2728,plain,
% 202.05/202.07 (~E(a4,f2(f2(f2(a1,a4),f2(x27281,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[8,2553,940,2,3])).
% 202.05/202.07 cnf(2731,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),f2(x27311,a1)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[2728,2])).
% 202.05/202.07 cnf(2737,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),a4),f2(f2(x27371,a1),x27372))),
% 202.05/202.07 inference(scs_inference,[],[248,37,2,3])).
% 202.05/202.07 cnf(2740,plain,
% 202.05/202.07 (~E(f2(x27401,a1),f2(f2(f2(a1,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2737,2708,12,2,3])).
% 202.05/202.07 cnf(2741,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a3),a4),a4),f2(x27411,a1))),
% 202.05/202.07 inference(scs_inference,[],[2740,2])).
% 202.05/202.07 cnf(2742,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),a4),f2(f2(a4,x27421),x27422))),
% 202.05/202.07 inference(scs_inference,[],[2740,256,37,2,3])).
% 202.05/202.07 cnf(2745,plain,
% 202.05/202.07 (~E(f2(x27451,a1),f2(a1,f2(f2(a4,x27452),x27453)))),
% 202.05/202.07 inference(scs_inference,[],[2742,2599,12,2,3])).
% 202.05/202.07 cnf(2749,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(a4,x27491),x27492)),f2(x27493,a1))),
% 202.05/202.07 inference(scs_inference,[],[2745,2])).
% 202.05/202.07 cnf(2750,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a3),f2(x27501,a1)),a4),f2(x27502,a1))),
% 202.05/202.07 inference(scs_inference,[],[2741,2745,2283,2,3])).
% 202.05/202.07 cnf(2753,plain,
% 202.05/202.07 (~E(f2(f2(x27531,x27532),x27531),f2(f2(a1,f2(x27533,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2750,2627,23,2,3])).
% 202.05/202.07 cnf(2755,plain,
% 202.05/202.07 (~E(f2(a1,a3),f2(f2(f2(x27551,a4),f2(a4,x27552)),f2(f2(x27551,a4),f2(a4,x27553))))),
% 202.05/202.07 inference(scs_inference,[],[1297,834,2282,2,3])).
% 202.05/202.07 cnf(2759,plain,
% 202.05/202.07 (~E(f2(x27591,a1),f2(f2(a3,f2(a3,x27592)),a4))),
% 202.05/202.07 inference(scs_inference,[],[2637,865,12,2,3])).
% 202.05/202.07 cnf(2763,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a3,x27631)),a4),f2(x27632,a1))),
% 202.05/202.07 inference(scs_inference,[],[2759,2])).
% 202.05/202.07 cnf(2776,plain,
% 202.05/202.07 (~E(f2(x27761,a1),f2(f2(a1,f2(a3,x27762)),a4))),
% 202.05/202.07 inference(scs_inference,[],[12,2641,656,2,3])).
% 202.05/202.07 cnf(2781,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(a3,x27811)),a4),f2(x27812,a1))),
% 202.05/202.07 inference(scs_inference,[],[2776,2])).
% 202.05/202.07 cnf(2798,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x27981),x27982),x27983),f2(a1,f2(a3,a4)))),
% 202.05/202.07 inference(scs_inference,[],[2407,1346,2266,2,3])).
% 202.05/202.07 cnf(2801,plain,
% 202.05/202.07 (~E(f2(f2(f2(x28011,x28012),f2(x28013,x28012)),f2(f2(x28011,x28013),x28012)),f2(f2(a3,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2798,2646,19,2,3])).
% 202.05/202.07 cnf(2803,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(a4,x28031),f2(x28032,a1))),a4)),
% 202.05/202.07 inference(scs_inference,[],[2714,813,2273,2,3])).
% 202.05/202.07 cnf(2806,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,a3),f2(f2(a4,x28061),f2(x28062,a1))))),
% 202.05/202.07 inference(scs_inference,[],[2803,2])).
% 202.05/202.07 cnf(2807,plain,
% 202.05/202.07 (~E(f2(x28071,a1),f2(f2(a1,a3),a4))),
% 202.05/202.07 inference(scs_inference,[],[12,2803,2702,2,3])).
% 202.05/202.07 cnf(2812,plain,
% 202.05/202.07 (~E(f2(f2(f2(x28121,a1),x28122),x28123),f2(a1,f2(a3,a3)))),
% 202.05/202.07 inference(scs_inference,[],[2807,2411,2275,2,3])).
% 202.05/202.07 cnf(2815,plain,
% 202.05/202.07 (~E(f2(x28151,a1),f2(f2(a3,a3),f2(f2(a4,x28152),f2(x28153,a1))))),
% 202.05/202.07 inference(scs_inference,[],[12,2806,2812,2,3])).
% 202.05/202.07 cnf(2816,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(a4,x28161),f2(x28162,a1))),f2(x28163,a1))),
% 202.05/202.07 inference(scs_inference,[],[2815,2])).
% 202.05/202.07 cnf(2817,plain,
% 202.05/202.07 (~E(f2(a1,f2(a4,a4)),f2(x28171,a1))),
% 202.05/202.07 inference(scs_inference,[],[2678,2815,2241,2,3])).
% 202.05/202.07 cnf(2821,plain,
% 202.05/202.07 (~E(f2(a4,x28211),f2(f2(f2(a3,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[13,2817,2652,2,3])).
% 202.05/202.07 cnf(2825,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a4),a4),a4),f2(a4,x28251))),
% 202.05/202.07 inference(scs_inference,[],[2821,2])).
% 202.05/202.07 cnf(2826,plain,
% 202.05/202.07 (~E(f2(f2(a4,a4),x28261),f2(a3,a3))),
% 202.05/202.07 inference(scs_inference,[],[2513,2821,2260,2,3])).
% 202.05/202.07 cnf(2832,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a4),f2(x28321,a1)),a4),f2(a4,x28322))),
% 202.05/202.07 inference(scs_inference,[],[2825,621,2283,2,3])).
% 202.05/202.07 cnf(2837,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(a4,a4),x28371)),a4)+~E(f2(f2(f2(a4,a4),x28371),f2(a3,a3)),a4)),
% 202.05/202.07 inference(scs_inference,[],[13,2826,2832,2720,2,3,11])).
% 202.05/202.07 cnf(2841,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(a4,f2(x28411,a1))),f2(x28412,a1))),
% 202.05/202.07 inference(scs_inference,[],[2816,1178,2232,2,3])).
% 202.05/202.07 cnf(2845,plain,
% 202.05/202.07 (~E(f2(a4,x28451),f2(f2(a1,a3),f2(f2(x28452,x28453),x28452)))),
% 202.05/202.07 inference(scs_inference,[],[13,2841,2710,2,3])).
% 202.05/202.07 cnf(2846,plain,
% 202.05/202.07 (~E(f2(f2(a1,a3),f2(f2(x28461,x28462),x28461)),f2(a4,x28463))),
% 202.05/202.07 inference(scs_inference,[],[2845,2])).
% 202.05/202.07 cnf(2851,plain,
% 202.05/202.07 (~E(f2(a4,x28511),f2(f2(a3,a3),f2(f2(x28512,x28513),x28512)))),
% 202.05/202.07 inference(scs_inference,[],[13,1278,2711,2,3])).
% 202.05/202.07 cnf(2852,plain,
% 202.05/202.07 (~E(f2(f2(f2(x28521,a1),x28522),f2(a1,f2(a3,a3))),a4)+~E(f2(f2(a1,f2(a3,a3)),f2(f2(x28521,a1),x28522)),a4)),
% 202.05/202.07 inference(scs_inference,[],[13,2409,1278,2711,2,3,11])).
% 202.05/202.07 cnf(2855,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(x28551,x28552),x28551)),f2(a4,x28553))),
% 202.05/202.07 inference(scs_inference,[],[2851,2])).
% 202.05/202.07 cnf(2868,plain,
% 202.05/202.07 (~E(f2(f2(x28681,x28682),x28681),f2(f2(a3,a3),f2(f2(a4,x28683),f2(x28684,a1))))),
% 202.05/202.07 inference(scs_inference,[],[2512,2806,23,2,3])).
% 202.05/202.07 cnf(2873,plain,
% 202.05/202.07 (~E(f2(f2(a1,a3),f2(f2(a4,x28731),f2(a4,x28732))),f2(a4,x28733))),
% 202.05/202.07 inference(scs_inference,[],[2846,827,2265,2,3])).
% 202.05/202.07 cnf(2877,plain,
% 202.05/202.07 (~E(f2(f2(x28771,x28772),x28771),f2(f2(f2(a1,a3),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2873,2708,23,2,3])).
% 202.05/202.07 cnf(2878,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a3),a4),a4),f2(f2(x28781,x28782),x28781))),
% 202.05/202.07 inference(scs_inference,[],[2877,2])).
% 202.05/202.07 cnf(2879,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(a4,x28791),f2(x28792,a1))),f2(a4,x28793))),
% 202.05/202.07 inference(scs_inference,[],[2855,2877,2273,2,3])).
% 202.05/202.07 cnf(2883,plain,
% 202.05/202.07 (~E(f2(a4,x28831),f2(a1,f2(f2(x28832,x28833),x28832)))),
% 202.05/202.07 inference(scs_inference,[],[2879,2590,13,2,3])).
% 202.05/202.07 cnf(2884,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x28841),x28842),f2(a3,f2(a3,x28843))),a4)+~E(f2(f2(a3,f2(a3,x28843)),f2(f2(a4,x28841),x28842)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2417,2879,2590,13,2,3,11])).
% 202.05/202.07 cnf(2887,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(x28871,x28872),x28871)),f2(a4,x28873))),
% 202.05/202.07 inference(scs_inference,[],[2883,2])).
% 202.05/202.07 cnf(2888,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),x28881),a1)),
% 202.05/202.07 inference(scs_inference,[],[2883,2582,2291,2,3])).
% 202.05/202.07 cnf(2892,plain,
% 202.05/202.07 (~E(f2(a1,f2(f2(a3,a4),x28921)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2888,2540,6,2,11])).
% 202.05/202.07 cnf(2904,plain,
% 202.05/202.07 (~E(f2(a1,f2(a4,a4)),f2(a4,x29041))),
% 202.05/202.07 inference(scs_inference,[],[2887,2892,2344,2241,8,2,11,3])).
% 202.05/202.07 cnf(2907,plain,
% 202.05/202.07 (~E(f2(a4,x29071),f2(a1,f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[2904,2])).
% 202.05/202.07 cnf(2912,plain,
% 202.05/202.07 (~E(f2(a1,f2(a4,x29121)),f2(x29122,a1))),
% 202.05/202.07 inference(scs_inference,[],[2749,1892,2232,2,3])).
% 202.05/202.07 cnf(2916,plain,
% 202.05/202.07 (~E(f2(f2(x29161,a1),f2(a4,x29162)),f2(a1,f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[2912,2907,210,2,3])).
% 202.05/202.07 cnf(2921,plain,
% 202.05/202.07 (~E(f2(a1,f2(a4,a4)),f2(f2(x29211,a1),f2(a4,x29212)))),
% 202.05/202.07 inference(scs_inference,[],[2916,2])).
% 202.05/202.07 cnf(2933,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(a4,a4)),f2(f2(x29331,a1),f2(a4,x29332))),a4)+~E(f2(f2(f2(x29331,a1),f2(a4,x29332)),f2(a1,f2(a4,a4))),a4)),
% 202.05/202.07 inference(scs_inference,[],[2921,680,2594,23,2,3,11])).
% 202.05/202.07 cnf(2970,plain,
% 202.05/202.07 (~E(f2(a4,x29701),f2(f2(a1,f2(x29702,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[1673,2627,13,2,3])).
% 202.05/202.07 cnf(2971,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(x29711,a1)),a4),f2(a4,x29712))),
% 202.05/202.07 inference(scs_inference,[],[2970,2])).
% 202.05/202.07 cnf(2974,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(a4,x29741),f2(x29742,a1))),f2(f2(x29743,x29744),x29743))),
% 202.05/202.07 inference(scs_inference,[],[2868,2])).
% 202.05/202.07 cnf(2980,plain,
% 202.05/202.07 (~E(f2(f2(a1,a4),a4),f2(a4,x29801))),
% 202.05/202.07 inference(scs_inference,[],[2971,1001,2291,2,3])).
% 202.05/202.07 cnf(2983,plain,
% 202.05/202.07 (~E(f2(a4,x29831),f2(f2(a1,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2980,2])).
% 202.05/202.07 cnf(2986,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a3),f2(x29861,a1)),a4),f2(f2(x29862,x29863),x29862))),
% 202.05/202.07 inference(scs_inference,[],[2878,660,2283,2,3])).
% 202.05/202.07 cnf(2989,plain,
% 202.05/202.07 (~E(f2(f2(x29891,a1),f2(a4,x29892)),f2(f2(a1,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[2983,2986,210,2,3])).
% 202.05/202.07 cnf(2994,plain,
% 202.05/202.07 (~E(f2(f2(a1,a4),a4),f2(f2(x29941,a1),f2(a4,x29942)))),
% 202.05/202.07 inference(scs_inference,[],[2989,2])).
% 202.05/202.07 cnf(2995,plain,
% 202.05/202.07 (~E(f2(a3,a3),f2(f2(f2(x29951,a4),f2(x29952,a4)),f2(f2(x29951,x29952),f2(a4,x29953))))),
% 202.05/202.07 inference(scs_inference,[],[20,2989,2282,2,3])).
% 202.05/202.07 cnf(2999,plain,
% 202.05/202.07 (~E(f2(a4,x29991),f2(f2(a3,f2(x29992,a1)),a4))),
% 202.05/202.07 inference(scs_inference,[],[509,2658,13,2,3])).
% 202.05/202.07 cnf(3000,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(x30001,a1)),a4),f2(a4,x30002))),
% 202.05/202.07 inference(scs_inference,[],[2999,2])).
% 202.05/202.07 cnf(3006,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),a4),f2(f2(x30061,a1),f2(a4,x30062))),a4)+~E(f2(f2(f2(x30061,a1),f2(a4,x30062)),f2(f2(a1,a4),a4)),a4)),
% 202.05/202.07 inference(scs_inference,[],[2994,1361,2638,23,2,3,11])).
% 202.05/202.07 cnf(3010,plain,
% 202.05/202.07 (~E(f2(a3,a3),f2(f2(f2(x30101,f2(a4,x30102)),f2(a1,f2(a4,x30102))),f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[20,1128,2249,2,3])).
% 202.05/202.07 cnf(3016,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a3),a4),a4),f2(f2(x30161,x30162),x30161))),
% 202.05/202.07 inference(scs_inference,[],[2531,2])).
% 202.05/202.07 cnf(3017,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),a4),f2(a4,x30171))),
% 202.05/202.07 inference(scs_inference,[],[3000,2531,2291,2,3])).
% 202.05/202.07 cnf(3020,plain,
% 202.05/202.07 (~E(f2(a4,x30201),f2(f2(a3,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[3017,2])).
% 202.05/202.07 cnf(3027,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a3),f2(x30271,a1)),a4),f2(f2(x30272,x30273),x30272))),
% 202.05/202.07 inference(scs_inference,[],[3016,1930,2283,2,3])).
% 202.05/202.07 cnf(3030,plain,
% 202.05/202.07 (~E(f2(f2(x30301,a1),f2(a4,x30302)),f2(f2(a3,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[3020,3027,210,2,3])).
% 202.05/202.07 cnf(3032,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),a4),f2(f2(x30321,a1),f2(a4,x30322)))),
% 202.05/202.07 inference(scs_inference,[],[3030,2])).
% 202.05/202.07 cnf(3033,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(a4,a4)),f2(f2(x30331,x30332),x30331))),
% 202.05/202.07 inference(scs_inference,[],[3030,2974,2241,2,3])).
% 202.05/202.07 cnf(3036,plain,
% 202.05/202.07 (~E(f2(f2(x30361,x30362),x30361),f2(f2(a3,a3),f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[3033,2])).
% 202.05/202.07 cnf(3037,plain,
% 202.05/202.07 (~E(f2(f2(x30371,x30372),x30371),f2(f2(a3,a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[23,3033,2646,2,3])).
% 202.05/202.07 cnf(3043,plain,
% 202.05/202.07 (~E(f2(f2(a4,a4),f2(x30431,a1)),f2(f2(a3,a3),f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[3036,3037,2260,2,3])).
% 202.05/202.07 cnf(3046,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(a4,a4)),f2(f2(a4,a4),f2(x30461,a1)))),
% 202.05/202.07 inference(scs_inference,[],[3043,2])).
% 202.05/202.07 cnf(3058,plain,
% 202.05/202.07 (~E(f2(f2(a3,a3),f2(f2(x30581,a1),a4)),f2(f2(a4,a4),f2(x30582,a1)))),
% 202.05/202.07 inference(scs_inference,[],[3046,1899,2258,2,3])).
% 202.05/202.07 cnf(3061,plain,
% 202.05/202.07 (~E(f2(f2(x30611,x30612),x30611),f2(a1,f2(a3,x30613)))),
% 202.05/202.07 inference(scs_inference,[],[23,3058,2622,2,3])).
% 202.05/202.07 cnf(3063,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(x30631,a1)),a4),f2(f2(x30632,a1),f2(a4,x30633)))),
% 202.05/202.07 inference(scs_inference,[],[3032,3061,2283,2,3])).
% 202.05/202.07 cnf(3066,plain,
% 202.05/202.07 (~E(f2(f2(x30661,x30662),x30661),f2(f2(f2(a3,a4),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[23,3063,2652,2,3])).
% 202.05/202.07 cnf(3070,plain,
% 202.05/202.07 (~E(f2(f2(f2(a3,a4),a4),a4),f2(f2(x30701,x30702),x30701))),
% 202.05/202.07 inference(scs_inference,[],[3066,2])).
% 202.05/202.07 cnf(3075,plain,
% 202.05/202.07 (~E(f2(f2(f2(x30751,a4),f2(x30752,a4)),f2(f2(x30751,x30752),f2(a4,x30753))),f2(a3,a3))),
% 202.05/202.07 inference(scs_inference,[],[2995,2])).
% 202.05/202.07 cnf(3082,plain,
% 202.05/202.07 (~E(f2(f2(f2(x30821,a4),f2(a4,x30822)),f2(f2(x30821,a4),f2(a4,x30823))),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[2755,2])).
% 202.05/202.07 cnf(3084,plain,
% 202.05/202.07 (~E(f2(f2(a3,a4),f2(f2(a3,a4),a1)),f2(f2(x30841,x30842),x30841))),
% 202.05/202.07 inference(scs_inference,[],[2586,2])).
% 202.05/202.07 cnf(3116,plain,
% 202.05/202.07 (~E(f2(f2(f2(x31161,a4),f2(x31162,a4)),f2(f2(x31161,x31162),f2(x31163,a1))),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[2698,2753,2273,2,3])).
% 202.05/202.07 cnf(3119,plain,
% 202.05/202.07 (~E(f2(a1,a3),f2(f2(f2(x31191,a4),f2(x31192,a4)),f2(f2(x31191,x31192),f2(x31193,a1))))),
% 202.05/202.07 inference(scs_inference,[],[3116,2])).
% 202.05/202.07 cnf(3126,plain,
% 202.05/202.07 (~E(f2(f2(f2(x31261,a4),f2(a1,a4)),f2(a4,f2(a4,x31262))),f2(a3,a3))),
% 202.05/202.07 inference(scs_inference,[],[3075,498,2232,2,3])).
% 202.05/202.07 cnf(3129,plain,
% 202.05/202.07 (~E(f2(a3,a3),f2(f2(f2(x31291,a4),f2(a1,a4)),f2(a4,f2(a4,x31292))))),
% 202.05/202.07 inference(scs_inference,[],[3126,2])).
% 202.05/202.07 cnf(3134,plain,
% 202.05/202.07 (~E(f2(a3,f2(f2(x31341,x31342),x31341)),a4)),
% 202.05/202.07 inference(scs_inference,[],[26,2567,59,2,3])).
% 202.05/202.07 cnf(3136,plain,
% 202.05/202.07 (~E(a4,f2(a3,f2(f2(x31361,x31362),x31361)))),
% 202.05/202.07 inference(scs_inference,[],[3134,2])).
% 202.05/202.07 cnf(3137,plain,
% 202.05/202.07 (~E(f2(a3,f2(a4,x31371)),a4)),
% 202.05/202.07 inference(scs_inference,[],[26,3134,48,2,3])).
% 202.05/202.07 cnf(3139,plain,
% 202.05/202.07 (~E(a4,f2(a3,f2(a4,x31391)))),
% 202.05/202.07 inference(scs_inference,[],[3137,2])).
% 202.05/202.07 cnf(3140,plain,
% 202.05/202.07 (~E(f2(a3,f2(x31401,a1)),a4)),
% 202.05/202.07 inference(scs_inference,[],[26,3137,38,2,3])).
% 202.05/202.07 cnf(3142,plain,
% 202.05/202.07 (~E(a4,f2(a3,f2(x31421,a1)))),
% 202.05/202.07 inference(scs_inference,[],[3140,2])).
% 202.05/202.07 cnf(3144,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x31441)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[3139,3140,19,7,2,3,11])).
% 202.05/202.07 cnf(3147,plain,
% 202.05/202.07 (~E(a4,f2(f2(a3,f2(a4,x31471)),a4))),
% 202.05/202.07 inference(scs_inference,[],[3144,2])).
% 202.05/202.07 cnf(3161,plain,
% 202.05/202.07 (~E(f2(x31611,a1),f2(a3,f2(f2(x31612,x31613),x31612)))),
% 202.05/202.07 inference(scs_inference,[],[3136,642,12,2,3])).
% 202.05/202.07 cnf(3162,plain,
% 202.05/202.07 (~E(f2(a3,f2(f2(x31621,x31622),x31621)),f2(x31623,a1))),
% 202.05/202.07 inference(scs_inference,[],[3161,2])).
% 202.05/202.07 cnf(3163,plain,
% 202.05/202.07 (~E(f2(f2(f2(x31631,a4),f2(a4,x31632)),f2(f2(x31631,a4),a4)),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[3161,3082,2282,2,3])).
% 202.05/202.07 cnf(3167,plain,
% 202.05/202.07 (~E(f2(x31671,a1),f2(f2(a3,f2(a4,x31672)),a4))),
% 202.05/202.07 inference(scs_inference,[],[3147,1198,12,2,3])).
% 202.05/202.07 cnf(3168,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x31681)),a4),f2(x31682,a1))),
% 202.05/202.07 inference(scs_inference,[],[3167,2])).
% 202.05/202.07 cnf(3176,plain,
% 202.05/202.07 (~E(f2(x31761,a1),f2(a3,f2(x31762,a1)))),
% 202.05/202.07 inference(scs_inference,[],[991,3142,12,2,3])).
% 202.05/202.07 cnf(3178,plain,
% 202.05/202.07 (~E(f2(a3,f2(f2(a4,x31781),f2(a4,x31782))),f2(x31783,a1))),
% 202.05/202.07 inference(scs_inference,[],[3176,3162,2265,2,3])).
% 202.05/202.07 cnf(3182,plain,
% 202.05/202.07 (~E(f2(a4,x31821),f2(a3,f2(f2(x31822,x31823),x31822)))),
% 202.05/202.07 inference(scs_inference,[],[3178,3136,13,2,3])).
% 202.05/202.07 cnf(3183,plain,
% 202.05/202.07 (~E(f2(a3,f2(f2(x31831,x31832),x31831)),f2(a4,x31833))),
% 202.05/202.07 inference(scs_inference,[],[3182,2])).
% 202.05/202.07 cnf(3184,plain,
% 202.05/202.07 (~E(f2(f2(f2(x31841,a4),f2(a4,x31842)),f2(f2(x31841,a4),f2(x31843,a1))),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[3182,3163,2273,2,3])).
% 202.05/202.07 cnf(3190,plain,
% 202.05/202.07 (~E(f2(a4,x31901),f2(f2(a3,f2(a4,x31902)),a4))),
% 202.05/202.07 inference(scs_inference,[],[3184,3147,13,2,3])).
% 202.05/202.07 cnf(3191,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x31911)),a4),f2(a4,x31912))),
% 202.05/202.07 inference(scs_inference,[],[3190,2])).
% 202.05/202.07 cnf(3192,plain,
% 202.05/202.07 (~E(f2(a3,f2(a4,a4)),f2(a4,x31921))),
% 202.05/202.07 inference(scs_inference,[],[3183,3190,2241,2,3])).
% 202.05/202.07 cnf(3195,plain,
% 202.05/202.07 (~E(f2(a4,x31951),f2(a3,f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[3192,2])).
% 202.05/202.07 cnf(3196,plain,
% 202.05/202.07 (~E(f2(x31961,a1),f2(a3,f2(a4,x31962)))),
% 202.05/202.07 inference(scs_inference,[],[3192,3139,12,2,3])).
% 202.05/202.07 cnf(3200,plain,
% 202.05/202.07 (~E(f2(f2(a4,x32001),f2(a3,f2(a4,a4))),a4)+~E(f2(f2(a3,f2(a4,a4)),f2(a4,x32001)),a4)),
% 202.05/202.07 inference(scs_inference,[],[3195,3196,3070,2283,2,3,11])).
% 202.05/202.07 cnf(3216,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(x32161,a1)),f2(f2(a3,a4),a1)),f2(f2(x32162,x32163),x32162))),
% 202.05/202.07 inference(scs_inference,[],[3084,1414,2283,2,3])).
% 202.05/202.07 cnf(3225,plain,
% 202.05/202.07 (~E(f2(a1,f2(a4,x32251)),f2(f2(x32252,x32253),x32252))),
% 202.05/202.07 inference(scs_inference,[],[2522,1152,2232,2,3])).
% 202.05/202.07 cnf(3228,plain,
% 202.05/202.07 (~E(f2(f2(x32281,x32282),x32281),f2(a1,f2(a4,x32283)))),
% 202.05/202.07 inference(scs_inference,[],[3225,2])).
% 202.05/202.07 cnf(3230,plain,
% 202.05/202.07 (~E(f2(f2(a4,a4),f2(a4,x32301)),f2(a1,f2(a4,x32302)))),
% 202.05/202.07 inference(scs_inference,[],[3228,1166,84,2,3])).
% 202.05/202.07 cnf(3234,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x32341),a4),f2(a4,x32342)),f2(a1,f2(a4,x32343)))),
% 202.05/202.07 inference(scs_inference,[],[3230,2266,2,3])).
% 202.05/202.07 cnf(3239,plain,
% 202.05/202.07 (~E(f2(a1,f2(a4,x32391)),f2(f2(f2(a4,x32392),a4),f2(a4,x32393)))),
% 202.05/202.07 inference(scs_inference,[],[3234,2])).
% 202.05/202.07 cnf(3279,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(f2(x32791,x32791),f2(a4,x32792)),f2(a4,x32793))))),
% 202.05/202.07 inference(scs_inference,[],[2431,2])).
% 202.05/202.07 cnf(3285,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(f2(x32851,x32851),f2(a4,x32852)),f2(x32853,a1))))),
% 202.05/202.07 inference(scs_inference,[],[2436,2])).
% 202.05/202.07 cnf(3294,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(f2(a4,x32941),x32942),f2(x32943,a1))))),
% 202.05/202.07 inference(scs_inference,[],[2445,2])).
% 202.05/202.07 cnf(3299,plain,
% 202.05/202.07 (~E(a4,f2(a1,f2(f2(f2(x32991,a1),x32992),f2(x32993,a1))))),
% 202.05/202.07 inference(scs_inference,[],[2449,2])).
% 202.05/202.07 cnf(3315,plain,
% 202.05/202.07 (~E(f2(x33151,a1),f2(a1,f2(f2(f2(x33152,a1),x33153),f2(x33154,a1))))),
% 202.05/202.07 inference(scs_inference,[],[3299,2801,12,2,3])).
% 202.05/202.07 cnf(3320,plain,
% 202.05/202.07 (~E(f2(a1,a4),f2(f2(f2(a4,x33201),a4),f2(a4,x33202)))),
% 202.05/202.07 inference(scs_inference,[],[37,3239,3315,2,3])).
% 202.05/202.07 cnf(3323,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x33231),a4),f2(a4,x33232)),f2(a1,a4))),
% 202.05/202.07 inference(scs_inference,[],[3320,2])).
% 202.05/202.07 cnf(3327,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x33271),a4),a4),f2(a1,a4))),
% 202.05/202.07 inference(scs_inference,[],[37,3323,3010,2,3])).
% 202.05/202.07 cnf(3330,plain,
% 202.05/202.07 (~E(f2(a1,a4),f2(f2(f2(a4,x33301),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[3327,2])).
% 202.05/202.07 cnf(3347,plain,
% 202.05/202.07 (~E(f2(f2(f2(a4,x33471),x33472),f2(a3,a4)),a4)+~E(f2(f2(a3,a4),f2(f2(a4,x33471),x33472)),a4)),
% 202.05/202.07 inference(scs_inference,[],[3216,2301,3279,23,2,3,11])).
% 202.05/202.07 cnf(3351,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a3,x33511)),f2(x33512,a1)),f2(x33513,a1))),
% 202.05/202.07 inference(scs_inference,[],[38,2763,2709,2,3])).
% 202.05/202.07 cnf(3354,plain,
% 202.05/202.07 (~E(f2(a4,x33541),f2(a1,f2(f2(f2(x33542,x33542),f2(a4,x33543)),f2(x33544,a1))))),
% 202.05/202.07 inference(scs_inference,[],[3351,3285,13,2,3])).
% 202.05/202.07 cnf(3356,plain,
% 202.05/202.07 (~E(f2(f2(a1,f2(a3,x33561)),f2(x33562,a1)),f2(x33563,a1))),
% 202.05/202.07 inference(scs_inference,[],[38,2781,3354,2,3])).
% 202.05/202.07 cnf(3360,plain,
% 202.05/202.07 (~E(f2(f2(a1,a3),f2(f2(x33601,a1),x33602)),a4)+~E(f2(f2(f2(x33601,a1),x33602),f2(a1,a3)),a4)),
% 202.05/202.07 inference(scs_inference,[],[3356,2293,3294,23,2,3,11])).
% 202.05/202.07 cnf(3364,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x33641)),f2(x33642,a1)),f2(x33643,a1))),
% 202.05/202.07 inference(scs_inference,[],[38,3168,1469,2,3])).
% 202.05/202.07 cnf(3367,plain,
% 202.05/202.07 (~E(f2(a4,x33671),f2(a1,f2(f2(f2(x33672,a1),x33673),f2(x33674,a1))))),
% 202.05/202.07 inference(scs_inference,[],[3364,3299,13,2,3])).
% 202.05/202.07 cnf(3369,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x33691)),f2(x33692,a1)),f2(a4,x33693))),
% 202.05/202.07 inference(scs_inference,[],[38,3191,3367,2,3])).
% 202.05/202.07 cnf(3371,plain,
% 202.05/202.07 (~E(f2(a4,x33711),f2(f2(a3,f2(a4,x33712)),f2(x33713,a1)))),
% 202.05/202.07 inference(scs_inference,[],[3369,2])).
% 202.05/202.07 cnf(3377,plain,
% 202.05/202.07 (~E(f2(a1,f2(x33771,a1)),f2(f2(f2(a4,x33772),a4),a4))),
% 202.05/202.07 inference(scs_inference,[],[38,3330,1593,2,3])).
% 202.05/202.07 cnf(3380,plain,
% 202.05/202.07 (~E(f2(f2(x33801,a1),f2(a4,x33802)),f2(f2(a3,f2(a4,x33803)),f2(x33804,a1)))),
% 202.05/202.07 inference(scs_inference,[],[3371,3377,210,2,3])).
% 202.05/202.07 cnf(3382,plain,
% 202.05/202.07 (~E(f2(f2(a3,f2(a4,x33821)),f2(x33822,a1)),f2(f2(x33823,a1),f2(a4,x33824)))),
% 202.05/202.07 inference(scs_inference,[],[3380,2])).
% 202.05/202.07 cnf(3383,plain,
% 202.05/202.07 (~E(f2(f2(f2(a1,a4),f2(x33831,a1)),f2(x33832,a1)),a4)),
% 202.05/202.07 inference(scs_inference,[],[38,3380,2731,2,3])).
% 202.05/202.07 cnf(3386,plain,
% 202.05/202.07 (~E(f2(f2(f2(f2(a1,a4),f2(x33861,a1)),f2(x33862,a1)),a4),a4)),
% 202.05/202.07 inference(scs_inference,[],[3383,7,2,11])).
% 202.05/202.07 cnf(3390,plain,
% 202.05/202.07 (~E(f2(a1,a3),f2(f2(f2(x33901,a4),f2(a1,a4)),f2(a4,a4)))),
% 202.05/202.07 inference(scs_inference,[],[3119,3386,2249,2,3])).
% 202.05/202.07 cnf(3393,plain,
% 202.05/202.07 (~E(f2(f2(f2(x33931,a4),f2(a1,a4)),f2(a4,a4)),f2(a1,a3))),
% 202.05/202.07 inference(scs_inference,[],[3390,2])).
% 202.05/202.07 cnf(3395,plain,
% 202.05/202.07 (~E(f2(f2(f2(x33951,a4),f2(a1,a4)),f2(f2(x33952,a1),f2(a4,x33953))),f2(a1,a3))),
% 202.05/202.08 inference(scs_inference,[],[3393,1093,2249,2,3])).
% 202.05/202.08 cnf(3401,plain,
% 202.05/202.08 (~E(f2(f2(f2(a3,f2(a4,x34011)),f2(x34012,a1)),f2(f2(x34013,a1),f2(a4,x34014))),a4)+~E(f2(f2(f2(x34013,a1),f2(a4,x34014)),f2(f2(a3,f2(a4,x34011)),f2(x34012,a1))),a4)),
% 202.05/202.08 inference(scs_inference,[],[3382,3395,3129,2265,2,3,11])).
% 202.05/202.08 cnf(3840,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,a4),f2(f2(x38401,a1),x38402)))+~E(f2(f2(f2(x38401,a1),x38402),f2(a3,a4)),a4)),
% 202.05/202.08 inference(scs_inference,[],[2475,2])).
% 202.05/202.08 cnf(3864,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,a3),f2(f2(a4,a4),x38641)))+~E(f2(f2(f2(a4,a4),x38641),f2(a3,a3)),a4)),
% 202.05/202.08 inference(scs_inference,[],[2837,2])).
% 202.05/202.08 cnf(3871,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,f2(a4,a4)),f2(a4,x38711)))+~E(f2(f2(a4,x38711),f2(a3,f2(a4,a4))),a4)),
% 202.05/202.08 inference(scs_inference,[],[3200,2])).
% 202.05/202.08 cnf(3873,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,a4),f2(f2(a4,x38731),x38732)))+~E(f2(f2(f2(a4,x38731),x38732),f2(a3,a4)),a4)),
% 202.05/202.08 inference(scs_inference,[],[3347,2])).
% 202.05/202.08 cnf(3874,plain,
% 202.05/202.08 (~E(a4,f2(f2(a1,a3),f2(f2(x38741,a1),x38742)))+~E(f2(f2(f2(x38741,a1),x38742),f2(a1,a3)),a4)),
% 202.05/202.08 inference(scs_inference,[],[3360,2])).
% 202.05/202.08 cnf(3892,plain,
% 202.05/202.08 (~E(f2(f2(f2(x38921,a1),x38922),f2(a3,a4)),a4)+~E(f2(f2(f2(a3,a4),f2(f2(x38921,a1),x38922)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[7,3840,11])).
% 202.05/202.08 cnf(3918,plain,
% 202.05/202.08 (~E(f2(f2(f2(a4,a4),x39181),f2(a3,a3)),a4)+~E(f2(f2(f2(a3,a3),f2(f2(a4,a4),x39181)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[7,3864,11])).
% 202.05/202.08 cnf(3930,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,f2(a4,a4)),f2(a4,a1)))),
% 202.05/202.08 inference(scs_inference,[],[7,44,3871,3])).
% 202.05/202.08 cnf(3934,plain,
% 202.05/202.08 (~E(f2(f2(f2(a4,x39341),x39342),f2(a3,a4)),a4)+~E(f2(f2(f2(a3,a4),f2(f2(a4,x39341),x39342)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[7,3873,11])).
% 202.05/202.08 cnf(3938,plain,
% 202.05/202.08 (~E(f2(f2(f2(x39381,a1),x39382),f2(a1,a3)),a4)+~E(f2(f2(f2(a1,a3),f2(f2(x39381,a1),x39382)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[7,3874,11])).
% 202.05/202.08 cnf(4034,plain,
% 202.05/202.08 (~E(a4,f2(f2(f2(x40341,a1),x40342),f2(a3,a4)))+~E(f2(f2(f2(a3,a4),f2(f2(x40341,a1),x40342)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[3892,2])).
% 202.05/202.08 cnf(4058,plain,
% 202.05/202.08 (~E(a4,f2(f2(f2(a4,a4),x40581),f2(a3,a3)))+~E(f2(f2(f2(a3,a3),f2(f2(a4,a4),x40581)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[3918,2])).
% 202.05/202.08 cnf(4066,plain,
% 202.05/202.08 (~E(a4,f2(f2(f2(a4,x40661),x40662),f2(a3,a4)))+~E(f2(f2(f2(a3,a4),f2(f2(a4,x40661),x40662)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[3934,2])).
% 202.05/202.08 cnf(4074,plain,
% 202.05/202.08 (~E(a4,f2(f2(f2(x40741,a1),x40742),f2(a1,a3)))+~E(f2(f2(f2(a1,a3),f2(f2(x40741,a1),x40742)),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[3938,2])).
% 202.05/202.08 cnf(4254,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,a3),f2(f2(x42541,a1),f2(a4,x42542))))+~E(f2(f2(f2(x42541,a1),f2(a4,x42542)),f2(a3,a3)),a4)),
% 202.05/202.08 inference(scs_inference,[],[2489,2])).
% 202.05/202.08 cnf(4261,plain,
% 202.05/202.08 (~E(a4,f2(f2(a1,f2(a3,a3)),f2(f2(x42611,a1),x42612)))+~E(f2(f2(f2(x42611,a1),x42612),f2(a1,f2(a3,a3))),a4)),
% 202.05/202.08 inference(scs_inference,[],[2852,2])).
% 202.05/202.08 cnf(4267,plain,
% 202.05/202.08 (~E(a4,f2(f2(a3,f2(a3,x42671)),f2(f2(a4,x42672),x42673)))+~E(f2(f2(f2(a4,x42672),x42673),f2(a3,f2(a3,x42671))),a4)),
% 202.05/202.08 inference(scs_inference,[],[2884,2])).
% 202.05/202.08 cnf(4321,plain,
% 202.05/202.08 (~E(a4,f2(f2(f2(x43211,a1),f2(a4,x43212)),f2(a3,a3)))+~E(a4,f2(f2(a3,a3),f2(f2(x43211,a1),f2(a4,x43212))))),
% 202.05/202.08 inference(scs_inference,[],[4254,2])).
% 202.05/202.08 cnf(4393,plain,
% 202.05/202.08 (~E(f2(f2(a3,a3),f2(f2(x43931,a1),f2(a4,x43932))),a4)+~E(a4,f2(f2(f2(x43931,a1),f2(a4,x43932)),f2(a3,a3)))),
% 202.05/202.08 inference(scs_inference,[],[4321,2])).
% 202.05/202.08 cnf(4447,plain,
% 202.05/202.08 (~E(a4,f2(f2(f2(x44471,a1),f2(a4,x44472)),f2(a3,a3)))+~E(f2(f2(f2(a3,a3),f2(f2(x44471,a1),f2(a4,x44472))),a4),a4)),
% 202.05/202.08 inference(scs_inference,[],[7,4393,11])).
% 202.05/202.08 cnf(4452,plain,
% 202.05/202.08 (E(f2(a4,x44521),f2(x44522,a1))),
% 202.05/202.08 inference(scs_inference,[],[13,3930,6,7,11,3,2])).
% 202.05/202.08 cnf(4453,plain,
% 202.05/202.08 (E(f2(x44531,f2(x44532,a1)),f2(x44531,f2(a4,x44533)))),
% 202.05/202.08 inference(scs_inference,[],[13,3930,6,7,11,3,2,5])).
% 202.05/202.08 cnf(4459,plain,
% 202.05/202.08 (E(f2(x44591,a1),a4)),
% 202.05/202.08 inference(rename_variables,[],[6])).
% 202.05/202.08 cnf(4461,plain,
% 202.05/202.08 (E(f2(x44611,a1),f2(f2(f2(x44612,x44613),f2(x44614,x44613)),f2(f2(x44612,x44614),x44613)))),
% 202.05/202.08 inference(scs_inference,[],[4452,19,4453,1195,6,4459,2,4,11,3])).
% 202.05/202.08 cnf(4467,plain,
% 202.05/202.08 (E(a4,f2(f2(f2(x44671,x44672),x44671),x44673))),
% 202.05/202.08 inference(scs_inference,[],[13,4461,57,1387,6,2,11,3])).
% 202.05/202.08 cnf(4471,plain,
% 202.05/202.08 (E(a4,f2(f2(f2(x44711,x44712),x44711),x44713))),
% 202.05/202.08 inference(rename_variables,[],[4467])).
% 202.05/202.08 cnf(4474,plain,
% 202.05/202.08 (E(a4,f2(f2(f2(x44741,x44742),x44741),x44743))),
% 202.05/202.08 inference(rename_variables,[],[4467])).
% 202.05/202.08 cnf(4477,plain,
% 202.05/202.08 (E(a4,f2(f2(f2(x44771,x44772),x44771),x44773))),
% 202.05/202.08 inference(rename_variables,[],[4467])).
% 202.05/202.08 cnf(4480,plain,
% 202.05/202.08 (E(a4,f2(f2(f2(x44801,x44802),x44801),x44803))),
% 202.05/202.08 inference(rename_variables,[],[4467])).
% 202.05/202.08 cnf(4483,plain,
% 202.05/202.08 (E(a4,f2(f2(f2(x44831,x44832),x44831),x44833))),
% 202.05/202.08 inference(rename_variables,[],[4467])).
% 202.05/202.08 cnf(4485,plain,
% 202.05/202.08 (E(f2(f2(f2(x44851,x44852),x44851),x44853),a4)),
% 202.05/202.08 inference(scs_inference,[],[4467,4471,4474,4477,4480,4483,4034,4058,4066,4074,4447,2])).
% 202.05/202.08 cnf(4496,plain,
% 202.05/202.08 (E(f2(f2(f2(x44961,x44962),x44961),x44963),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4499,plain,
% 202.05/202.08 (E(f2(f2(f2(x44991,x44992),x44991),x44993),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4502,plain,
% 202.05/202.08 (E(f2(f2(f2(x45021,x45022),x45021),x45023),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4505,plain,
% 202.05/202.08 (E(f2(f2(f2(x45051,x45052),x45051),x45053),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4508,plain,
% 202.05/202.08 (E(f2(f2(f2(x45081,x45082),x45081),x45083),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4511,plain,
% 202.05/202.08 (E(f2(f2(f2(x45111,x45112),x45111),x45113),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4514,plain,
% 202.05/202.08 (E(f2(f2(f2(x45141,x45142),x45141),x45143),a4)),
% 202.05/202.08 inference(rename_variables,[],[4485])).
% 202.05/202.08 cnf(4516,plain,
% 202.05/202.08 ($false),
% 202.05/202.08 inference(scs_inference,[],[4485,4496,4499,4502,4505,4508,4511,4514,2697,2933,3006,3401,3840,3873,4261,4267,21]),
% 202.05/202.08 ['proof']).
% 202.05/202.08 % SZS output end Proof
% 202.05/202.08 % Total time :201.440000s
%------------------------------------------------------------------------------