%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN004-6 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 72.72s 72.76s
% Output : CNFRefutation 72.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HEN004-6 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n021.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Sat Jun 22 05:26:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.54 start to proof:theBenchmark
% 72.72/72.74 %-------------------------------------------
% 72.72/72.75 % File :CSE---1.7
% 72.72/72.75 % Problem :theBenchmark
% 72.72/72.75 % Transform :cnf
% 72.72/72.75 % Format :tptp:raw
% 72.72/72.75 % Command :java -jar mcs_scs.jar %d %s
% 72.72/72.75
% 72.72/72.75 % Result :Theorem 72.170000s
% 72.72/72.75 % Output :CNFRefutation 72.170000s
% 72.72/72.75 %-------------------------------------------
% 72.72/72.75 %--------------------------------------------------------------------------
% 72.72/72.75 % File : HEN004-6 : TPTP v8.2.0. Released v1.0.0.
% 72.72/72.75 % Domain : Henkin Models
% 72.72/72.75 % Problem : X/zero = X
% 72.72/72.76 % Version : [MOW76] axioms : Augmented.
% 72.72/72.76 % English :
% 72.72/72.76
% 72.72/72.76 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 72.72/72.76 % Source : [ANL]
% 72.72/72.76 % Names : hp4.ver2.in [ANL]
% 72.72/72.76
% 72.72/72.76 % Status : Unsatisfiable
% 72.72/72.76 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.40 v2.0.0
% 72.72/72.76 % Syntax : Number of clauses : 10 ( 7 unt; 0 nHn; 4 RR)
% 72.72/72.76 % Number of literals : 14 ( 6 equ; 5 neg)
% 72.72/72.76 % Maximal clause size : 3 ( 1 avg)
% 72.72/72.76 % Maximal term depth : 3 ( 1 avg)
% 72.72/72.76 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 72.72/72.76 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 72.72/72.76 % Number of variables : 15 ( 5 sgn)
% 72.72/72.76 % SPC : CNF_UNS_RFO_SEQ_HRN
% 72.72/72.76
% 72.72/72.76 % Comments :
% 72.72/72.76 %--------------------------------------------------------------------------
% 72.72/72.76 %----Include Henkin model axioms for equality formulation
% 72.72/72.76 include('Axioms/HEN002-0.ax').
% 72.72/72.76 %--------------------------------------------------------------------------
% 72.72/72.76 cnf(everything_divide_id_is_zero,axiom,
% 72.72/72.76 divide(X,identity) = zero ).
% 72.72/72.76
% 72.72/72.76 cnf(zero_divide_anything_is_zero,axiom,
% 72.72/72.76 divide(zero,X) = zero ).
% 72.72/72.76
% 72.72/72.76 cnf(prove_x_divide_zero_is_x,negated_conjecture,
% 72.72/72.76 divide(a,zero) != a ).
% 72.72/72.76
% 72.72/72.76 %--------------------------------------------------------------------------
% 72.72/72.76 %-------------------------------------------
% 72.72/72.76 % Proof found
% 72.72/72.76 % SZS status Theorem for theBenchmark
% 72.72/72.76 % SZS output start Proof
% 72.72/72.76 %ClaNum:17(EqnAxiom:7)
% 72.72/72.76 %VarNum:28(SingletonVarNum:15)
% 72.72/72.76 %MaxLitNum:3
% 72.72/72.76 %MaxfuncDepth:2
% 72.72/72.76 %SharedTerms:5
% 72.72/72.76 %goalClause: 14
% 72.72/72.76 %singleGoalClaCount:1
% 72.72/72.76 [14]~E(f2(a3,a4),a3)
% 72.72/72.76 [10]P1(x101,a1)
% 72.72/72.76 [11]P1(a4,x111)
% 72.72/72.76 [8]E(f2(x81,a1),a4)
% 72.72/72.76 [9]E(f2(a4,x91),a4)
% 72.72/72.76 [12]P1(f2(x121,x122),x121)
% 72.72/72.76 [13]P1(f2(f2(x131,x132),f2(x133,x132)),f2(f2(x131,x133),x132))
% 72.72/72.76 [15]~P1(x151,x152)+E(f2(x151,x152),a4)
% 72.72/72.76 [16]P1(x161,x162)+~E(f2(x161,x162),a4)
% 72.72/72.76 [17]~P1(x172,x171)+~P1(x171,x172)+E(x171,x172)
% 72.72/72.76 %EqnAxiom
% 72.72/72.76 [1]E(x11,x11)
% 72.72/72.76 [2]E(x22,x21)+~E(x21,x22)
% 72.72/72.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 72.72/72.76 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 72.72/72.76 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 72.72/72.76 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 72.72/72.76 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 72.72/72.76
% 72.72/72.76 %-------------------------------------------
% 72.72/72.78 cnf(18,plain,
% 72.72/72.78 (E(a4,f2(x181,a1))),
% 72.72/72.78 inference(scs_inference,[],[8,2])).
% 72.72/72.78 cnf(19,plain,
% 72.72/72.78 (~P1(a3,f2(a3,a4))),
% 72.72/72.78 inference(scs_inference,[],[14,12,8,2,17])).
% 72.72/72.78 cnf(22,plain,
% 72.72/72.78 (~E(a4,a3)),
% 72.72/72.78 inference(scs_inference,[],[14,11,12,8,2,17,6])).
% 72.72/72.78 cnf(24,plain,
% 72.72/72.78 (~E(a1,f2(a3,a4))),
% 72.72/72.78 inference(scs_inference,[],[14,10,11,12,8,2,17,6,7])).
% 72.72/72.78 cnf(26,plain,
% 72.72/72.78 (E(a4,f2(a4,x261))),
% 72.72/72.78 inference(scs_inference,[],[9,2])).
% 72.72/72.78 cnf(27,plain,
% 72.72/72.78 (E(f2(a4,x271),f2(x272,a1))),
% 72.72/72.78 inference(scs_inference,[],[18,9,2,3])).
% 72.72/72.78 cnf(28,plain,
% 72.72/72.78 (~P1(a3,a4)),
% 72.72/72.78 inference(scs_inference,[],[18,22,9,11,2,3,17])).
% 72.72/72.78 cnf(31,plain,
% 72.72/72.78 (P1(f2(f2(x311,a1),f2(x312,a1)),a4)),
% 72.72/72.78 inference(scs_inference,[],[18,22,13,9,11,8,2,3,17,7])).
% 72.72/72.78 cnf(36,plain,
% 72.72/72.78 (E(f2(x361,a1),f2(a4,x362))),
% 72.72/72.78 inference(scs_inference,[],[27,2])).
% 72.72/72.78 cnf(37,plain,
% 72.72/72.78 (E(f2(f2(x371,a1),f2(x372,a1)),a4)),
% 72.72/72.78 inference(scs_inference,[],[27,31,11,2,17])).
% 72.72/72.78 cnf(40,plain,
% 72.72/72.78 (E(f2(x401,a1),f2(x402,a1))),
% 72.72/72.78 inference(scs_inference,[],[27,18,31,11,8,2,17,3])).
% 72.72/72.78 cnf(41,plain,
% 72.72/72.78 (~E(f2(f2(x411,a1),f2(x412,a1)),a3)),
% 72.72/72.78 inference(scs_inference,[],[28,27,18,31,11,8,2,17,3,6])).
% 72.72/72.78 cnf(42,plain,
% 72.72/72.78 (P1(f2(f2(x421,a1),f2(x422,a1)),f2(a4,x423))),
% 72.72/72.78 inference(scs_inference,[],[28,27,26,18,31,11,8,2,17,3,6,7])).
% 72.72/72.78 cnf(43,plain,
% 72.72/72.78 (P1(f2(x431,a1),f2(x432,a1))),
% 72.72/72.78 inference(scs_inference,[],[28,27,26,18,31,11,8,2,17,3,6,7,16])).
% 72.72/72.78 cnf(45,plain,
% 72.72/72.78 (E(a4,f2(f2(x451,a1),f2(x452,a1)))),
% 72.72/72.78 inference(scs_inference,[],[37,2])).
% 72.72/72.78 cnf(46,plain,
% 72.72/72.78 (E(f2(f2(x461,a1),f2(x462,a1)),f2(a4,x463))),
% 72.72/72.78 inference(scs_inference,[],[37,26,2,3])).
% 72.72/72.78 cnf(47,plain,
% 72.72/72.78 (P1(f2(x471,a1),f2(a4,x472))),
% 72.72/72.78 inference(scs_inference,[],[36,37,26,43,2,3,7])).
% 72.72/72.78 cnf(48,plain,
% 72.72/72.78 (P1(f2(x481,a1),f2(x482,a1))),
% 72.72/72.78 inference(rename_variables,[],[43])).
% 72.72/72.78 cnf(49,plain,
% 72.72/72.78 (P1(f2(a4,x491),f2(x492,a1))),
% 72.72/72.78 inference(scs_inference,[],[36,37,26,43,48,2,3,7,6])).
% 72.72/72.78 cnf(51,plain,
% 72.72/72.78 (E(f2(f2(x511,x512),f2(x513,x512)),f2(f2(x511,x513),x512))+~P1(f2(f2(x511,x513),x512),f2(f2(x511,x512),f2(x513,x512)))),
% 72.72/72.78 inference(scs_inference,[],[36,37,26,43,48,13,2,3,7,6,17])).
% 72.72/72.78 cnf(53,plain,
% 72.72/72.78 (E(f2(a4,x531),f2(f2(x532,a1),f2(x533,a1)))),
% 72.72/72.78 inference(scs_inference,[],[46,2])).
% 72.72/72.78 cnf(57,plain,
% 72.72/72.78 (E(f2(f2(x571,a1),f2(x572,a1)),f2(f2(x573,a1),f2(x574,a1)))),
% 72.72/72.78 inference(scs_inference,[],[37,46,40,45,42,2,7,3])).
% 72.72/72.78 cnf(58,plain,
% 72.72/72.78 (E(f2(f2(x581,a1),f2(x582,a1)),f2(x583,a1))),
% 72.72/72.78 inference(scs_inference,[],[37,18,3])).
% 72.72/72.78 cnf(61,plain,
% 72.72/72.78 (E(f2(x611,a1),f2(f2(x612,a1),f2(x613,a1)))),
% 72.72/72.78 inference(scs_inference,[],[37,53,18,42,3,7,2])).
% 72.72/72.78 cnf(62,plain,
% 72.72/72.78 (P1(f2(x621,a1),f2(f2(x622,a1),f2(x623,a1)))),
% 72.72/72.78 inference(scs_inference,[],[61,47,7])).
% 72.72/72.78 cnf(67,plain,
% 72.72/72.78 (~E(f2(x671,a1),a3)),
% 72.72/72.78 inference(scs_inference,[],[28,37,62,7,6])).
% 72.72/72.78 cnf(68,plain,
% 72.72/72.78 (P1(f2(a4,x681),f2(f2(x682,a1),f2(x683,a1)))),
% 72.72/72.78 inference(scs_inference,[],[53,49,7])).
% 72.72/72.78 cnf(71,plain,
% 72.72/72.78 (P1(f2(f2(f2(x711,a1),f2(x712,a1)),x713),a4)),
% 72.72/72.78 inference(scs_inference,[],[37,12,7])).
% 72.72/72.78 cnf(77,plain,
% 72.72/72.78 (P1(f2(f2(x771,a1),f2(x772,a1)),x773)),
% 72.72/72.78 inference(scs_inference,[],[28,37,12,11,7,17,6,16])).
% 72.72/72.78 cnf(79,plain,
% 72.72/72.78 (E(a4,f2(f2(f2(x791,a1),f2(x792,a1)),x793))),
% 72.72/72.78 inference(scs_inference,[],[28,37,12,11,7,17,6,16,2])).
% 72.72/72.78 cnf(80,plain,
% 72.72/72.78 (~P1(a3,f2(f2(x801,a1),f2(x802,a1)))),
% 72.72/72.78 inference(scs_inference,[],[77,41,17])).
% 72.72/72.78 cnf(83,plain,
% 72.72/72.78 (~E(f2(a4,x831),a3)),
% 72.72/72.78 inference(scs_inference,[],[77,68,41,17,6])).
% 72.72/72.78 cnf(88,plain,
% 72.72/72.78 (~E(a1,f2(x881,a1))),
% 72.72/72.78 inference(scs_inference,[],[80,61,10,7,3])).
% 72.72/72.78 cnf(92,plain,
% 72.72/72.78 (~E(a1,a4)),
% 72.72/72.78 inference(scs_inference,[],[79,88,3])).
% 72.72/72.78 cnf(97,plain,
% 72.72/72.78 (P1(f2(f2(x971,a1),x972),a4)),
% 72.72/72.78 inference(scs_inference,[],[8,12,7])).
% 72.72/72.78 cnf(99,plain,
% 72.72/72.78 (E(f2(f2(x991,a1),x992),a4)),
% 72.72/72.78 inference(scs_inference,[],[8,12,11,7,17])).
% 72.72/72.78 cnf(102,plain,
% 72.72/72.78 (~E(f2(f2(x1021,a1),x1022),a3)),
% 72.72/72.78 inference(scs_inference,[],[8,28,12,11,7,17,6])).
% 72.72/72.78 cnf(103,plain,
% 72.72/72.78 (~E(a1,f2(f2(x1031,a1),x1032))),
% 72.72/72.78 inference(scs_inference,[],[8,28,92,12,11,7,17,6,3])).
% 72.72/72.78 cnf(104,plain,
% 72.72/72.78 (P1(f2(x1041,a1),x1042)),
% 72.72/72.78 inference(scs_inference,[],[8,28,92,12,11,7,17,6,3,16])).
% 72.72/72.78 cnf(106,plain,
% 72.72/72.78 (E(a4,f2(f2(x1061,a1),x1062))),
% 72.72/72.78 inference(scs_inference,[],[8,28,92,12,11,7,17,6,3,16,2])).
% 72.72/72.78 cnf(118,plain,
% 72.72/72.78 (E(f2(x1181,a4),f2(x1181,f2(x1182,a1)))),
% 72.72/72.78 inference(scs_inference,[],[8,2,5])).
% 72.72/72.78 cnf(119,plain,
% 72.72/72.78 (E(f2(x1191,f2(x1192,a1)),f2(x1191,a4))),
% 72.72/72.78 inference(scs_inference,[],[118,2])).
% 72.72/72.78 cnf(124,plain,
% 72.72/72.78 (~E(a1,f2(a3,f2(x1241,a1)))),
% 72.72/72.78 inference(scs_inference,[],[118,24,102,104,2,17,3])).
% 72.72/72.78 cnf(125,plain,
% 72.72/72.78 (E(f2(a4,x1251),f2(f2(x1252,a1),x1251))),
% 72.72/72.78 inference(scs_inference,[],[8,2,4])).
% 72.72/72.78 cnf(126,plain,
% 72.72/72.78 (E(f2(f2(x1261,a1),x1262),f2(a4,x1262))),
% 72.72/72.78 inference(scs_inference,[],[125,2])).
% 72.72/72.78 cnf(127,plain,
% 72.72/72.78 (~P1(a3,f2(x1271,a1))),
% 72.72/72.78 inference(scs_inference,[],[125,67,104,2,17])).
% 72.72/72.78 cnf(131,plain,
% 72.72/72.78 (E(f2(x1311,a4),f2(x1311,f2(a4,x1312)))),
% 72.72/72.78 inference(scs_inference,[],[9,2,5])).
% 72.72/72.78 cnf(132,plain,
% 72.72/72.78 (E(f2(x1321,f2(a4,x1322)),f2(x1321,a4))),
% 72.72/72.78 inference(scs_inference,[],[131,2])).
% 72.72/72.78 cnf(133,plain,
% 72.72/72.78 (P1(f2(f2(a4,x1331),x1332),a4)),
% 72.72/72.78 inference(scs_inference,[],[9,131,12,2,7])).
% 72.72/72.78 cnf(135,plain,
% 72.72/72.78 (~E(f2(f2(a4,x1351),x1352),a3)),
% 72.72/72.78 inference(scs_inference,[],[9,28,131,12,2,7,6])).
% 72.72/72.78 cnf(136,plain,
% 72.72/72.78 (E(f2(f2(a4,x1361),x1362),a4)),
% 72.72/72.78 inference(scs_inference,[],[9,28,131,12,11,2,7,6,17])).
% 72.72/72.78 cnf(139,plain,
% 72.72/72.78 (~E(a1,f2(f2(a4,x1391),x1392))),
% 72.72/72.78 inference(scs_inference,[],[9,28,131,92,12,11,2,7,6,17,3])).
% 72.72/72.78 cnf(140,plain,
% 72.72/72.78 (P1(f2(a4,x1401),x1402)),
% 72.72/72.78 inference(scs_inference,[],[9,28,131,92,12,11,2,7,6,17,3,16])).
% 72.72/72.78 cnf(142,plain,
% 72.72/72.78 (E(f2(a4,x1421),f2(f2(a4,x1422),x1421))),
% 72.72/72.78 inference(scs_inference,[],[9,2,4])).
% 72.72/72.78 cnf(143,plain,
% 72.72/72.78 (E(f2(f2(a4,x1431),x1432),f2(a4,x1432))),
% 72.72/72.78 inference(scs_inference,[],[142,2])).
% 72.72/72.78 cnf(144,plain,
% 72.72/72.78 (~P1(a3,f2(a4,x1441))),
% 72.72/72.78 inference(scs_inference,[],[142,140,83,2,17])).
% 72.72/72.78 cnf(148,plain,
% 72.72/72.78 (P1(f2(f2(f2(x1481,a1),f2(x1482,a1)),x1483),f2(a4,x1484))),
% 72.72/72.78 inference(scs_inference,[],[9,71,2,7])).
% 72.72/72.78 cnf(149,plain,
% 72.72/72.78 (E(a4,f2(f2(a4,x1491),x1492))),
% 72.72/72.78 inference(scs_inference,[],[136,2])).
% 72.72/72.78 cnf(150,plain,
% 72.72/72.78 (E(f2(f2(f2(x1501,a1),f2(x1502,a1)),x1503),f2(a4,x1504))),
% 72.72/72.78 inference(scs_inference,[],[136,148,140,2,17])).
% 72.72/72.78 cnf(154,plain,
% 72.72/72.78 (~E(a3,f2(a3,f2(x1541,a1)))),
% 72.72/72.78 inference(scs_inference,[],[14,119,2,3])).
% 72.72/72.78 cnf(157,plain,
% 72.72/72.78 (~E(a3,f2(a3,f2(a4,x1571)))),
% 72.72/72.78 inference(scs_inference,[],[14,132,2,3])).
% 72.72/72.78 cnf(159,plain,
% 72.72/72.78 (~E(a1,x1591)+E(f2(x1592,x1591),a4)),
% 72.72/72.78 inference(scs_inference,[],[10,15,7])).
% 72.72/72.78 cnf(162,plain,
% 72.72/72.78 (E(a4,f2(f2(x1621,x1622),x1621))),
% 72.72/72.78 inference(scs_inference,[],[12,15,2])).
% 72.72/72.78 cnf(163,plain,
% 72.72/72.78 (E(f2(f2(x1631,x1632),x1631),a4)),
% 72.72/72.78 inference(scs_inference,[],[162,2])).
% 72.72/72.78 cnf(164,plain,
% 72.72/72.78 (~E(a1,f2(f2(x1641,x1642),x1641))),
% 72.72/72.78 inference(scs_inference,[],[162,92,2,3])).
% 72.72/72.78 cnf(166,plain,
% 72.72/72.78 (E(f2(f2(f2(x1661,x1662),x1661),x1663),f2(a4,x1663))),
% 72.72/72.78 inference(scs_inference,[],[12,15,4])).
% 72.72/72.78 cnf(167,plain,
% 72.72/72.78 (E(f2(a4,x1671),f2(f2(f2(x1672,x1673),x1672),x1671))),
% 72.72/72.78 inference(scs_inference,[],[166,2])).
% 72.72/72.78 cnf(171,plain,
% 72.72/72.78 (P1(f2(f2(a4,x1711),x1712),f2(f2(x1713,x1714),x1713))),
% 72.72/72.78 inference(scs_inference,[],[118,162,166,164,133,2,3,7])).
% 72.72/72.78 cnf(172,plain,
% 72.72/72.78 (E(f2(x1721,f2(f2(x1722,x1723),x1722)),f2(x1721,a4))),
% 72.72/72.78 inference(scs_inference,[],[12,15,5])).
% 72.72/72.78 cnf(173,plain,
% 72.72/72.78 (E(f2(x1731,a4),f2(x1731,f2(f2(x1732,x1733),x1732)))),
% 72.72/72.78 inference(scs_inference,[],[172,2])).
% 72.72/72.78 cnf(176,plain,
% 72.72/72.78 (E(f2(f2(x1761,x1762),x1761),f2(f2(x1763,a1),x1764))),
% 72.72/72.78 inference(scs_inference,[],[12,106,15,3])).
% 72.72/72.78 cnf(177,plain,
% 72.72/72.78 (E(f2(f2(x1771,a1),x1772),f2(f2(x1773,x1774),x1773))),
% 72.72/72.78 inference(scs_inference,[],[176,2])).
% 72.72/72.78 cnf(180,plain,
% 72.72/72.78 (~E(f2(f2(x1801,x1801),f2(x1802,x1801)),a3)),
% 72.72/72.78 inference(scs_inference,[],[127,176,13,2,7,6])).
% 72.72/72.78 cnf(182,plain,
% 72.72/72.78 (E(f2(f2(f2(x1821,x1822),x1821),f2(x1823,a1)),a4)),
% 72.72/72.78 inference(scs_inference,[],[12,177,15,6])).
% 72.72/72.78 cnf(185,plain,
% 72.72/72.78 (E(a4,f2(f2(f2(x1851,x1852),x1851),f2(x1853,a1)))),
% 72.72/72.78 inference(scs_inference,[],[182,16,2])).
% 72.72/72.78 cnf(186,plain,
% 72.72/72.78 (~E(f2(f2(x1861,x1862),x1861),a3)),
% 72.72/72.78 inference(scs_inference,[],[144,182,16,2,6])).
% 72.72/72.78 cnf(188,plain,
% 72.72/72.79 (E(f2(f2(x1881,x1882),x1881),f2(a4,a1))),
% 72.72/72.79 inference(scs_inference,[],[144,182,140,16,2,6,17])).
% 72.72/72.79 cnf(192,plain,
% 72.72/72.79 (E(f2(a4,a1),f2(f2(x1921,x1922),x1921))),
% 72.72/72.79 inference(scs_inference,[],[188,2])).
% 72.72/72.79 cnf(193,plain,
% 72.72/72.79 (P1(f2(f2(x1931,a1),x1932),f2(f2(f2(x1933,x1934),x1933),f2(x1935,a1)))),
% 72.72/72.79 inference(scs_inference,[],[185,188,97,2,7])).
% 72.72/72.79 cnf(194,plain,
% 72.72/72.79 (E(f2(f2(f2(x1941,x1942),x1941),a4),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,192,15,6])).
% 72.72/72.79 cnf(199,plain,
% 72.72/72.79 (E(f2(f2(a4,x1991),a4),f2(f2(f2(a4,x1991),a4),f2(x1992,a1)))),
% 72.72/72.79 inference(scs_inference,[],[12,185,194,133,16,2,7,17])).
% 72.72/72.79 cnf(203,plain,
% 72.72/72.79 (E(f2(f2(f2(a4,x2031),a4),f2(x2032,a1)),f2(f2(a4,x2031),a4))),
% 72.72/72.79 inference(scs_inference,[],[199,2])).
% 72.72/72.79 cnf(204,plain,
% 72.72/72.79 (P1(f2(f2(x2041,x2041),f2(x2042,x2041)),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,13,15,7])).
% 72.72/72.79 cnf(205,plain,
% 72.72/72.79 (E(f2(f2(x2051,x2051),f2(x2052,x2051)),a4)),
% 72.72/72.79 inference(scs_inference,[],[204,11,17])).
% 72.72/72.79 cnf(208,plain,
% 72.72/72.79 (~E(a1,f2(f2(x2081,x2081),f2(x2082,x2081)))),
% 72.72/72.79 inference(scs_inference,[],[204,92,11,17,3])).
% 72.72/72.79 cnf(209,plain,
% 72.72/72.79 (P1(f2(x2091,x2091),f2(x2092,x2091))),
% 72.72/72.79 inference(scs_inference,[],[204,92,11,17,3,16])).
% 72.72/72.79 cnf(211,plain,
% 72.72/72.79 (E(a4,f2(f2(x2111,x2111),f2(x2112,x2111)))),
% 72.72/72.79 inference(scs_inference,[],[204,92,11,17,3,16,2])).
% 72.72/72.79 cnf(212,plain,
% 72.72/72.79 (E(f2(f2(x2121,x2122),x2121),f2(f2(x2123,x2123),f2(x2124,x2123)))),
% 72.72/72.79 inference(scs_inference,[],[12,211,15,3])).
% 72.72/72.79 cnf(213,plain,
% 72.72/72.79 (E(f2(f2(x2131,x2131),f2(x2132,x2131)),f2(f2(x2133,x2134),x2133))),
% 72.72/72.79 inference(scs_inference,[],[212,2])).
% 72.72/72.79 cnf(214,plain,
% 72.72/72.79 (E(f2(f2(x2141,a1),f2(x2142,a1)),f2(f2(x2143,x2143),f2(x2144,x2143)))),
% 72.72/72.79 inference(scs_inference,[],[212,57,2,3])).
% 72.72/72.79 cnf(215,plain,
% 72.72/72.79 (E(f2(f2(x2151,x2152),x2151),f2(f2(x2153,x2153),f2(x2154,x2153)))),
% 72.72/72.79 inference(rename_variables,[],[212])).
% 72.72/72.79 cnf(217,plain,
% 72.72/72.79 (P1(f2(f2(x2171,x2171),f2(x2172,x2171)),f2(f2(x2173,x2173),f2(x2174,x2173)))),
% 72.72/72.79 inference(scs_inference,[],[212,215,57,13,2,3,7])).
% 72.72/72.79 cnf(219,plain,
% 72.72/72.79 (E(f2(f2(f2(x2191,x2192),x2191),f2(x2193,x2193)),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,213,15,6])).
% 72.72/72.79 cnf(220,plain,
% 72.72/72.79 (P1(f2(f2(x2201,x2202),x2201),f2(x2203,x2203))),
% 72.72/72.79 inference(scs_inference,[],[219,16])).
% 72.72/72.79 cnf(223,plain,
% 72.72/72.79 (E(f2(a4,f2(x2231,a1)),f2(f2(a4,x2232),a4))),
% 72.72/72.79 inference(scs_inference,[],[214,167,203,219,16,2,3])).
% 72.72/72.79 cnf(230,plain,
% 72.72/72.79 (E(f2(f2(a4,x2301),a4),f2(a4,f2(x2302,a1)))),
% 72.72/72.79 inference(scs_inference,[],[223,2])).
% 72.72/72.79 cnf(231,plain,
% 72.72/72.79 (E(f2(f2(x2311,a1),a4),f2(x2312,a1))),
% 72.72/72.79 inference(scs_inference,[],[173,58,223,2,3])).
% 72.72/72.79 cnf(237,plain,
% 72.72/72.79 (E(f2(f2(x2371,x2371),f2(x2372,x2371)),f2(a4,f2(x2373,a1)))),
% 72.72/72.79 inference(scs_inference,[],[173,126,58,223,217,140,2,3,7,17])).
% 72.72/72.79 cnf(241,plain,
% 72.72/72.79 (E(f2(a4,f2(x2411,a1)),f2(f2(x2412,x2412),f2(x2413,x2412)))),
% 72.72/72.79 inference(scs_inference,[],[237,2])).
% 72.72/72.79 cnf(242,plain,
% 72.72/72.79 (E(f2(f2(x2421,x2421),f2(x2422,x2421)),f2(x2423,a1))),
% 72.72/72.79 inference(scs_inference,[],[237,231,213,2,3])).
% 72.72/72.79 cnf(248,plain,
% 72.72/72.79 (E(f2(x2481,a1),f2(f2(x2482,x2482),f2(x2483,x2482)))),
% 72.72/72.79 inference(scs_inference,[],[242,2])).
% 72.72/72.79 cnf(249,plain,
% 72.72/72.79 (E(f2(f2(a4,x2491),a4),f2(f2(f2(x2492,x2493),x2492),f2(x2494,a1)))),
% 72.72/72.79 inference(scs_inference,[],[230,242,167,2,3])).
% 72.72/72.79 cnf(253,plain,
% 72.72/72.79 (E(f2(f2(a4,x2531),x2532),f2(a4,f2(x2533,a1)))),
% 72.72/72.79 inference(scs_inference,[],[230,242,167,171,140,2,3,7,17])).
% 72.72/72.79 cnf(256,plain,
% 72.72/72.79 (E(f2(f2(f2(x2561,x2561),f2(x2562,x2561)),x2563),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,248,15,6])).
% 72.72/72.79 cnf(257,plain,
% 72.72/72.79 (P1(f2(f2(x2571,x2571),f2(x2572,x2571)),x2573)),
% 72.72/72.79 inference(scs_inference,[],[256,16])).
% 72.72/72.79 cnf(259,plain,
% 72.72/72.79 (E(f2(f2(f2(x2591,x2592),x2591),f2(x2593,a1)),f2(f2(a4,x2594),a4))),
% 72.72/72.79 inference(scs_inference,[],[249,256,16,2])).
% 72.72/72.79 cnf(260,plain,
% 72.72/72.79 (~P1(a3,f2(f2(x2601,x2601),f2(x2602,x2601)))),
% 72.72/72.79 inference(scs_inference,[],[249,180,256,16,2,17])).
% 72.72/72.79 cnf(262,plain,
% 72.72/72.79 (E(f2(f2(a4,x2621),x2622),f2(f2(x2623,x2623),f2(x2624,x2623)))),
% 72.72/72.79 inference(scs_inference,[],[241,249,253,180,256,16,2,17,3])).
% 72.72/72.79 cnf(264,plain,
% 72.72/72.79 (P1(f2(f2(x2641,x2642),x2641),f2(a4,f2(x2643,a1)))),
% 72.72/72.79 inference(scs_inference,[],[241,249,253,220,180,256,16,2,17,3,7])).
% 72.72/72.79 cnf(268,plain,
% 72.72/72.79 (E(f2(f2(x2681,x2681),f2(x2682,x2681)),f2(f2(a4,x2683),x2684))),
% 72.72/72.79 inference(scs_inference,[],[262,2])).
% 72.72/72.79 cnf(269,plain,
% 72.72/72.79 (~E(f2(f2(f2(x2691,x2691),f2(x2692,x2691)),x2693),a3)),
% 72.72/72.79 inference(scs_inference,[],[12,260,262,2,6])).
% 72.72/72.79 cnf(271,plain,
% 72.72/72.79 (E(f2(f2(x2711,x2712),x2711),f2(a4,f2(x2713,a1)))),
% 72.72/72.79 inference(scs_inference,[],[12,260,262,264,140,2,6,17])).
% 72.72/72.79 cnf(274,plain,
% 72.72/72.79 (E(f2(a4,a1),f2(f2(f2(x2741,a1),x2742),a4))),
% 72.72/72.79 inference(scs_inference,[],[12,260,192,262,119,264,140,2,6,17,3])).
% 72.72/72.79 cnf(278,plain,
% 72.72/72.79 (E(f2(f2(f2(a4,x2781),x2782),f2(x2783,x2783)),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,268,15,6])).
% 72.72/72.79 cnf(281,plain,
% 72.72/72.79 (E(f2(f2(f2(x2811,a1),x2812),a4),f2(a4,a1))),
% 72.72/72.79 inference(scs_inference,[],[274,278,16,2])).
% 72.72/72.79 cnf(282,plain,
% 72.72/72.79 (E(f2(f2(f2(x2821,x2822),x2821),f2(x2823,a1)),f2(a4,f2(x2824,a1)))),
% 72.72/72.79 inference(scs_inference,[],[274,271,259,278,16,2,3])).
% 72.72/72.79 cnf(283,plain,
% 72.72/72.79 (E(f2(f2(x2831,x2832),x2831),f2(a4,f2(x2833,a1)))),
% 72.72/72.79 inference(rename_variables,[],[271])).
% 72.72/72.79 cnf(287,plain,
% 72.72/72.79 (E(f2(f2(x2871,a1),x2872),f2(a4,f2(x2873,a1)))),
% 72.72/72.79 inference(scs_inference,[],[274,271,283,259,193,278,140,16,2,3,7,17])).
% 72.72/72.79 cnf(291,plain,
% 72.72/72.79 (E(f2(a4,f2(x2911,a1)),f2(f2(f2(x2912,x2913),x2912),f2(x2914,a1)))),
% 72.72/72.79 inference(scs_inference,[],[282,2])).
% 72.72/72.79 cnf(292,plain,
% 72.72/72.79 (E(f2(f2(x2921,x2921),f2(x2922,x2921)),f2(f2(x2923,x2923),f2(x2924,x2923)))),
% 72.72/72.79 inference(scs_inference,[],[282,268,248,2,3])).
% 72.72/72.79 cnf(296,plain,
% 72.72/72.79 (E(f2(a4,f2(x2961,a1)),f2(f2(x2962,a1),x2963))),
% 72.72/72.79 inference(scs_inference,[],[287,2])).
% 72.72/72.79 cnf(297,plain,
% 72.72/72.79 (E(f2(f2(x2971,a1),x2972),f2(f2(f2(x2973,x2974),x2973),f2(x2975,a1)))),
% 72.72/72.79 inference(scs_inference,[],[291,287,2,3])).
% 72.72/72.79 cnf(299,plain,
% 72.72/72.79 (P1(f2(f2(x2991,x2992),f2(a1,x2992)),f2(a4,f2(x2993,a1)))),
% 72.72/72.79 inference(scs_inference,[],[291,287,13,2,3,7])).
% 72.72/72.79 cnf(301,plain,
% 72.72/72.79 (~E(f2(f2(x3011,x3012),f2(a1,x3012)),a3)),
% 72.72/72.79 inference(scs_inference,[],[144,291,287,13,2,3,7,6])).
% 72.72/72.79 cnf(303,plain,
% 72.72/72.79 (E(f2(f2(x3031,x3032),f2(a1,x3032)),f2(a4,f2(x3033,a1)))),
% 72.72/72.79 inference(scs_inference,[],[144,291,287,13,140,2,3,7,6,17])).
% 72.72/72.79 cnf(306,plain,
% 72.72/72.79 (E(f2(f2(f2(f2(x3061,x3062),x3061),f2(x3063,a1)),f2(x3064,a1)),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,297,15,6])).
% 72.72/72.79 cnf(309,plain,
% 72.72/72.79 (E(f2(a4,f2(x3091,a1)),f2(f2(x3092,x3093),f2(a1,x3093)))),
% 72.72/72.79 inference(scs_inference,[],[303,306,16,2])).
% 72.72/72.79 cnf(311,plain,
% 72.72/72.79 (E(f2(a4,f2(x3111,a1)),f2(a4,f2(x3112,a1)))),
% 72.72/72.79 inference(scs_inference,[],[127,303,296,306,16,2,6,3])).
% 72.72/72.79 cnf(316,plain,
% 72.72/72.79 (E(f2(f2(f2(x3161,x3162),f2(a1,x3162)),a4),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,309,15,6])).
% 72.72/72.79 cnf(319,plain,
% 72.72/72.79 (E(f2(f2(f2(x3191,x3192),x3191),f2(x3193,a1)),f2(f2(x3194,a1),x3195))),
% 72.72/72.79 inference(scs_inference,[],[297,316,16,2])).
% 72.72/72.79 cnf(320,plain,
% 72.72/72.79 (E(f2(f2(x3201,x3202),f2(a1,x3202)),a4)),
% 72.72/72.79 inference(scs_inference,[],[297,316,11,16,2,17])).
% 72.72/72.79 cnf(323,plain,
% 72.72/72.79 (E(f2(f2(x3231,x3231),f2(x3232,x3231)),f2(a4,x3233))),
% 72.72/72.79 inference(scs_inference,[],[292,297,150,316,11,16,2,17,3])).
% 72.72/72.79 cnf(330,plain,
% 72.72/72.79 (P1(f2(x3301,x3302),f2(a1,x3302))),
% 72.72/72.79 inference(scs_inference,[],[320,16])).
% 72.72/72.79 cnf(332,plain,
% 72.72/72.79 (E(f2(a4,x3321),f2(f2(x3322,x3322),f2(x3323,x3322)))),
% 72.72/72.79 inference(scs_inference,[],[323,320,16,2])).
% 72.72/72.79 cnf(333,plain,
% 72.72/72.79 (E(f2(f2(f2(x3331,x3332),x3331),f2(x3333,a1)),f2(a4,a1))),
% 72.72/72.79 inference(scs_inference,[],[323,320,319,281,16,2,3])).
% 72.72/72.79 cnf(336,plain,
% 72.72/72.79 (P1(f2(f2(f2(x3361,x3361),f2(x3362,x3361)),x3363),f2(a4,x3364))),
% 72.72/72.79 inference(scs_inference,[],[12,323,320,319,281,16,2,3,7])).
% 72.72/72.79 cnf(338,plain,
% 72.72/72.79 (E(f2(f2(f2(x3381,x3381),f2(x3382,x3381)),a4),f2(a4,a4))),
% 72.72/72.79 inference(scs_inference,[],[12,323,320,319,281,209,16,2,3,7,17])).
% 72.72/72.79 cnf(343,plain,
% 72.72/72.79 (E(f2(f2(x3431,a1),x3432),f2(a4,a1))),
% 72.72/72.79 inference(scs_inference,[],[338,333,177,2,3])).
% 72.72/72.79 cnf(350,plain,
% 72.72/72.79 (E(f2(a4,a1),f2(f2(x3501,a1),x3502))),
% 72.72/72.79 inference(scs_inference,[],[343,2])).
% 72.72/72.79 cnf(351,plain,
% 72.72/72.79 (E(f2(a4,f2(x3511,a1)),f2(f2(a4,x3512),f2(x3513,a1)))),
% 72.72/72.79 inference(scs_inference,[],[311,343,142,2,3])).
% 72.72/72.79 cnf(353,plain,
% 72.72/72.79 (P1(f2(x3531,a4),f2(a1,f2(f2(x3532,x3533),x3532)))),
% 72.72/72.79 inference(scs_inference,[],[311,343,173,142,330,2,3,7])).
% 72.72/72.79 cnf(359,plain,
% 72.72/72.79 (E(a4,f2(f2(x3591,x3592),f2(a1,x3592)))),
% 72.72/72.79 inference(scs_inference,[],[320,2])).
% 72.72/72.79 cnf(360,plain,
% 72.72/72.79 (E(f2(f2(f2(x3601,x3601),f2(x3602,x3601)),x3603),f2(a4,a1))),
% 72.72/72.79 inference(scs_inference,[],[320,336,104,2,17])).
% 72.72/72.79 cnf(368,plain,
% 72.72/72.79 (E(f2(a4,a1),f2(f2(f2(x3681,x3681),f2(x3682,x3681)),x3683))),
% 72.72/72.79 inference(scs_inference,[],[360,2])).
% 72.72/72.79 cnf(369,plain,
% 72.72/72.79 (E(f2(f2(a4,x3691),f2(x3692,a1)),f2(f2(a4,x3693),f2(x3694,a1)))),
% 72.72/72.79 inference(scs_inference,[],[360,351,143,2,3])).
% 72.72/72.79 cnf(371,plain,
% 72.72/72.79 (P1(f2(f2(f2(x3711,a1),x3712),x3713),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,99,360,351,143,2,3,7])).
% 72.72/72.79 cnf(373,plain,
% 72.72/72.79 (~E(f2(f2(f2(x3731,a1),x3732),x3733),a3)),
% 72.72/72.79 inference(scs_inference,[],[12,28,99,360,351,143,2,3,7,6])).
% 72.72/72.79 cnf(374,plain,
% 72.72/72.79 (E(f2(f2(f2(x3741,a1),x3742),x3743),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,28,99,360,351,143,11,2,3,7,6,17])).
% 72.72/72.79 cnf(377,plain,
% 72.72/72.79 (P1(f2(f2(x3771,a1),x3772),x3773)),
% 72.72/72.79 inference(scs_inference,[],[12,28,99,360,351,143,11,2,3,7,6,17,16])).
% 72.72/72.79 cnf(379,plain,
% 72.72/72.79 (E(f2(f2(x3791,x3792),x3791),f2(f2(x3793,x3794),f2(a1,x3794)))),
% 72.72/72.79 inference(scs_inference,[],[12,359,15,3])).
% 72.72/72.79 cnf(380,plain,
% 72.72/72.79 (E(f2(f2(x3801,x3802),f2(a1,x3802)),f2(f2(x3803,x3804),x3803))),
% 72.72/72.79 inference(scs_inference,[],[379,2])).
% 72.72/72.79 cnf(381,plain,
% 72.72/72.79 (~P1(a3,f2(f2(x3811,a1),x3811))),
% 72.72/72.79 inference(scs_inference,[],[379,377,186,2,17])).
% 72.72/72.79 cnf(385,plain,
% 72.72/72.79 (E(f2(f2(x3851,x3852),x3851),f2(a4,x3853))),
% 72.72/72.79 inference(scs_inference,[],[379,46,377,186,2,17,3])).
% 72.72/72.79 cnf(390,plain,
% 72.72/72.79 (E(f2(a4,x3901),f2(f2(x3902,x3903),x3902))),
% 72.72/72.79 inference(scs_inference,[],[385,2])).
% 72.72/72.79 cnf(391,plain,
% 72.72/72.79 (~E(f2(x3911,x3911),a3)),
% 72.72/72.79 inference(scs_inference,[],[381,385,209,2,6])).
% 72.72/72.79 cnf(397,plain,
% 72.72/72.79 (E(f2(f2(x3971,x3972),f2(a1,x3972)),f2(x3973,a1))),
% 72.72/72.79 inference(scs_inference,[],[381,380,385,58,373,209,377,2,6,17,3])).
% 72.72/72.79 cnf(400,plain,
% 72.72/72.79 (P1(f2(f2(f2(x4001,x4002),x4001),x4003),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,381,163,380,385,58,373,209,377,2,6,17,3,7])).
% 72.72/72.79 cnf(403,plain,
% 72.72/72.79 (E(f2(x4031,a1),f2(f2(x4032,x4033),f2(a1,x4033)))),
% 72.72/72.79 inference(scs_inference,[],[397,2])).
% 72.72/72.79 cnf(404,plain,
% 72.72/72.79 (E(f2(f2(f2(x4041,x4042),x4041),x4043),a4)),
% 72.72/72.79 inference(scs_inference,[],[397,11,400,2,17])).
% 72.72/72.79 cnf(408,plain,
% 72.72/72.79 (E(f2(f2(x4081,x4082),f2(a1,x4082)),f2(f2(x4083,a1),x4084))),
% 72.72/72.79 inference(scs_inference,[],[28,397,350,11,400,2,17,6,3])).
% 72.72/72.79 cnf(410,plain,
% 72.72/72.79 (P1(f2(f2(f2(a4,x4101),x4102),x4103),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,28,136,397,350,11,400,2,17,6,3,7])).
% 72.72/72.79 cnf(412,plain,
% 72.72/72.79 (P1(f2(f2(x4121,x4122),x4121),x4123)),
% 72.72/72.79 inference(scs_inference,[],[12,28,136,397,350,11,400,2,17,6,3,7,16])).
% 72.72/72.79 cnf(414,plain,
% 72.72/72.79 (E(f2(f2(x4141,a1),x4142),f2(f2(x4143,x4144),f2(a1,x4144)))),
% 72.72/72.79 inference(scs_inference,[],[408,2])).
% 72.72/72.79 cnf(415,plain,
% 72.72/72.79 (~P1(a3,f2(f2(f2(x4151,x4151),f2(x4152,x4151)),f2(x4151,x4151)))),
% 72.72/72.79 inference(scs_inference,[],[408,412,269,2,17])).
% 72.72/72.79 cnf(419,plain,
% 72.72/72.79 (~E(f2(f2(f2(a4,x4191),x4192),x4193),a3)),
% 72.72/72.79 inference(scs_inference,[],[28,408,412,269,410,2,17,6])).
% 72.72/72.79 cnf(420,plain,
% 72.72/72.79 (E(f2(f2(x4201,x4202),f2(a1,x4202)),f2(f2(f2(x4203,x4204),x4203),f2(x4205,a1)))),
% 72.72/72.79 inference(scs_inference,[],[28,408,249,412,269,410,2,17,6,3])).
% 72.72/72.79 cnf(425,plain,
% 72.72/72.79 (P1(f2(x4251,x4251),a4)),
% 72.72/72.79 inference(scs_inference,[],[205,163,16,7])).
% 72.72/72.79 cnf(426,plain,
% 72.72/72.79 (E(f2(f2(f2(x4261,x4262),x4261),f2(x4263,a1)),f2(f2(x4264,x4265),f2(a1,x4265)))),
% 72.72/72.79 inference(scs_inference,[],[420,2])).
% 72.72/72.79 cnf(427,plain,
% 72.72/72.79 (E(f2(x4271,x4271),a4)),
% 72.72/72.79 inference(scs_inference,[],[420,11,425,2,17])).
% 72.72/72.79 cnf(430,plain,
% 72.72/72.79 (E(f2(f2(x4301,x4302),x4301),f2(f2(f2(x4303,x4304),x4303),f2(x4305,a1)))),
% 72.72/72.79 inference(scs_inference,[],[420,385,291,11,425,2,17,3])).
% 72.72/72.79 cnf(432,plain,
% 72.72/72.79 (P1(f2(f2(f2(x4321,x4322),f2(a1,x4322)),x4323),a4)),
% 72.72/72.79 inference(scs_inference,[],[12,320,420,385,291,11,425,2,17,3,7])).
% 72.72/72.79 cnf(434,plain,
% 72.72/72.79 (P1(x4341,x4341)),
% 72.72/72.79 inference(scs_inference,[],[12,320,420,385,291,11,425,2,17,3,7,16])).
% 72.72/72.79 cnf(436,plain,
% 72.72/72.79 (~E(f2(f2(f2(x4361,x4362),f2(a1,x4362)),x4363),a3)),
% 72.72/72.79 inference(scs_inference,[],[12,28,320,420,385,291,11,425,2,17,3,7,16,6])).
% 72.72/72.79 cnf(438,plain,
% 72.72/72.79 (E(f2(f2(f2(x4381,x4382),x4381),f2(x4383,a1)),f2(f2(x4384,x4385),x4384))),
% 72.72/72.79 inference(scs_inference,[],[430,2])).
% 72.72/72.79 cnf(439,plain,
% 72.72/72.79 (E(f2(f2(f2(x4391,x4392),f2(a1,x4392)),x4393),a4)),
% 72.72/72.79 inference(scs_inference,[],[430,11,432,2,17])).
% 72.72/72.79 cnf(442,plain,
% 72.72/72.79 (E(f2(f2(x4421,x4422),x4421),f2(f2(a4,x4423),a4))),
% 72.72/72.79 inference(scs_inference,[],[430,259,11,432,2,17,3])).
% 72.72/72.79 cnf(446,plain,
% 72.72/72.79 (P1(f2(f2(x4461,x4462),f2(a1,x4462)),x4463)),
% 72.72/72.79 inference(scs_inference,[],[430,332,259,299,11,432,2,17,3,7,16])).
% 72.72/72.79 cnf(448,plain,
% 72.72/72.79 (E(f2(f2(x4481,a1),x4482),f2(x4481,a1))),
% 72.72/72.79 inference(scs_inference,[],[99,12,16,17])).
% 72.72/72.79 cnf(449,plain,
% 72.72/72.79 (E(f2(x4491,a1),f2(f2(x4491,a1),x4492))),
% 72.72/72.79 inference(scs_inference,[],[448,2])).
% 72.72/72.79 cnf(450,plain,
% 72.72/72.79 (E(f2(a4,x4501),f2(f2(a4,x4501),x4502))),
% 72.72/72.79 inference(scs_inference,[],[12,448,140,2,17])).
% 72.72/72.79 cnf(454,plain,
% 72.72/72.79 (E(f2(f2(f2(x4541,x4542),x4541),f2(x4543,a1)),f2(x4544,a1))),
% 72.72/72.79 inference(scs_inference,[],[12,438,448,140,2,17,3])).
% 72.72/72.79 cnf(459,plain,
% 72.72/72.79 (~E(a4,f2(a3,f2(a3,a4)))),
% 72.72/72.79 inference(scs_inference,[],[19,16,2])).
% 72.72/72.79 cnf(460,plain,
% 72.72/72.79 (E(f2(f2(a4,x4601),x4602),f2(a4,x4601))),
% 72.72/72.79 inference(scs_inference,[],[450,2])).
% 72.72/72.79 cnf(461,plain,
% 72.72/72.79 (E(f2(f2(f2(a4,x4611),x4612),x4613),a4)),
% 72.72/72.79 inference(scs_inference,[],[450,11,410,2,17])).
% 72.72/72.79 cnf(464,plain,
% 72.72/72.79 (E(f2(f2(f2(x4641,x4642),x4641),f2(x4643,a1)),f2(f2(a4,x4644),f2(x4645,a1)))),
% 72.72/72.79 inference(scs_inference,[],[450,282,351,11,410,2,17,3])).
% 72.72/72.79 cnf(466,plain,
% 72.72/72.79 (~E(a3,f2(f2(f2(x4661,x4661),f2(x4662,x4661)),f2(x4661,x4661)))),
% 72.72/72.79 inference(scs_inference,[],[415,450,282,351,11,434,410,2,17,3,7])).
% 72.72/72.79 cnf(468,plain,
% 72.72/72.79 (P1(f2(f2(a4,x4681),x4682),x4683)),
% 72.72/72.79 inference(scs_inference,[],[415,450,282,351,11,434,410,2,17,3,7,16])).
% 72.72/72.79 cnf(471,plain,
% 72.72/72.79 (E(f2(f2(a4,x4711),f2(x4712,a1)),f2(f2(f2(x4713,x4714),x4713),f2(x4715,a1)))),
% 72.72/72.79 inference(scs_inference,[],[464,2])).
% 72.72/72.79 cnf(472,plain,
% 72.72/72.79 (E(f2(f2(f2(x4721,x4722),x4721),f2(x4723,a1)),f2(a4,x4724))),
% 72.72/72.79 inference(scs_inference,[],[426,460,464,2,3])).
% 72.72/72.79 cnf(477,plain,
% 72.72/72.79 (E(f2(x4771,a1),f2(f2(f2(x4772,x4773),x4772),f2(x4774,a1)))),
% 72.72/72.79 inference(scs_inference,[],[454,2])).
% 72.72/72.79 cnf(478,plain,
% 72.72/72.79 (E(f2(f2(x4781,a1),x4782),f2(x4783,a1))),
% 72.72/72.79 inference(scs_inference,[],[414,454,2,3])).
% 72.72/72.79 cnf(481,plain,
% 72.72/72.79 (P1(f2(x4811,x4811),f2(f2(x4812,x4812),f2(x4813,x4812)))),
% 72.72/72.79 inference(scs_inference,[],[414,454,211,425,2,3,7])).
% 72.72/72.79 cnf(483,plain,
% 72.72/72.79 (E(f2(a4,x4831),f2(f2(f2(x4832,x4833),x4832),f2(x4834,a1)))),
% 72.72/72.79 inference(scs_inference,[],[472,2])).
% 72.72/72.79 cnf(484,plain,
% 72.72/72.79 (E(f2(f2(a4,x4841),f2(x4842,a1)),f2(a4,x4843))),
% 72.72/72.79 inference(scs_inference,[],[471,472,2,3])).
% 72.72/72.79 cnf(488,plain,
% 72.72/72.79 (~E(f2(a3,f2(a3,a4)),f2(f2(a4,x4881),x4882))),
% 72.72/72.79 inference(scs_inference,[],[19,136,16,3])).
% 72.72/72.79 cnf(491,plain,
% 72.72/72.79 (E(f2(x4911,a1),f2(f2(x4912,a1),x4913))),
% 72.72/72.79 inference(scs_inference,[],[478,488,4,2])).
% 72.72/72.79 cnf(493,plain,
% 72.72/72.79 (E(f2(f2(a1,x4931),a1),f2(f2(a4,x4932),f2(x4933,a1)))),
% 72.72/72.79 inference(scs_inference,[],[449,478,464,359,488,425,4,2,7,3])).
% 72.72/72.79 cnf(497,plain,
% 72.72/72.79 (E(f2(f2(a4,x4971),a4),f2(f2(x4972,x4973),x4972))),
% 72.72/72.79 inference(scs_inference,[],[442,2])).
% 72.72/72.79 cnf(498,plain,
% 72.72/72.79 (~E(a3,f2(f2(x4981,x4981),f2(x4982,x4981)))),
% 72.72/72.79 inference(scs_inference,[],[260,442,434,2,7])).
% 72.72/72.79 cnf(500,plain,
% 72.72/72.79 (~E(a1,f2(f2(x5001,x5002),f2(a1,x5002)))),
% 72.72/72.79 inference(scs_inference,[],[260,320,442,434,92,2,7,3])).
% 72.72/72.79 cnf(502,plain,
% 72.72/72.79 (E(f2(a4,x5021),f2(f2(a4,x5022),f2(x5023,a1)))),
% 72.72/72.79 inference(scs_inference,[],[484,2])).
% 72.72/72.79 cnf(505,plain,
% 72.72/72.79 (~E(a3,f2(f2(x5051,a1),x5051))),
% 72.72/72.79 inference(scs_inference,[],[381,497,484,466,434,2,3,7])).
% 72.72/72.79 cnf(508,plain,
% 72.72/72.79 (E(f2(f2(a4,x5081),f2(x5082,a1)),f2(f2(a1,x5083),a1))),
% 72.72/72.79 inference(scs_inference,[],[493,2])).
% 72.72/72.79 cnf(516,plain,
% 72.72/72.79 (~E(a3,f2(x5161,a1))),
% 72.72/72.79 inference(scs_inference,[],[127,508,404,505,434,2,3,7])).
% 72.72/72.79 cnf(518,plain,
% 72.72/72.79 (~E(a4,f2(a3,f2(a4,x5181)))),
% 72.72/72.79 inference(scs_inference,[],[144,16,2])).
% 72.72/72.79 cnf(519,plain,
% 72.72/72.79 (E(a4,f2(f2(f2(x5191,x5192),f2(a1,x5192)),x5193))),
% 72.72/72.79 inference(scs_inference,[],[439,2])).
% 72.72/72.79 cnf(522,plain,
% 72.72/72.79 (~P1(f2(a3,f2(a3,a4)),a4)),
% 72.72/72.79 inference(scs_inference,[],[19,11,16,17])).
% 72.72/72.79 cnf(525,plain,
% 72.72/72.79 (~E(a3,a4)),
% 72.72/72.79 inference(scs_inference,[],[12,522,374,92,2,3,7])).
% 72.72/72.79 cnf(528,plain,
% 72.72/72.79 (E(a4,f2(f2(f2(a4,x5281),x5282),x5283))),
% 72.72/72.79 inference(scs_inference,[],[461,2])).
% 72.72/72.79 cnf(529,plain,
% 72.72/72.79 (~E(f2(a1,f2(a3,a4)),a4)),
% 72.72/72.79 inference(scs_inference,[],[461,522,330,2,7])).
% 72.72/72.79 cnf(532,plain,
% 72.72/72.79 (~P1(a1,f2(a3,a4))),
% 72.72/72.79 inference(scs_inference,[],[163,461,522,525,330,2,7,3,15])).
% 72.72/72.79 cnf(534,plain,
% 72.72/72.80 (~P1(f2(a3,f2(f2(x5341,x5341),f2(x5342,x5341))),a4)),
% 72.72/72.80 inference(scs_inference,[],[260,11,16,17])).
% 72.72/72.80 cnf(535,plain,
% 72.72/72.80 (E(a4,f2(x5351,x5351))),
% 72.72/72.80 inference(scs_inference,[],[427,2])).
% 72.72/72.80 cnf(536,plain,
% 72.72/72.80 (~P1(a3,f2(f2(a1,x5361),f2(a1,x5361)))),
% 72.72/72.80 inference(scs_inference,[],[427,446,391,2,17])).
% 72.72/72.80 cnf(540,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(x5401,x5401),f2(x5402,x5401)))),
% 72.72/72.80 inference(scs_inference,[],[205,427,446,391,529,2,17,3])).
% 72.72/72.80 cnf(541,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x5411,x5411),f2(x5412,x5411))),a4)),
% 72.72/72.80 inference(scs_inference,[],[205,534,427,446,391,529,330,2,17,3,7])).
% 72.72/72.80 cnf(543,plain,
% 72.72/72.80 (~P1(a1,f2(f2(x5431,x5431),f2(x5432,x5431)))),
% 72.72/72.80 inference(scs_inference,[],[205,534,427,446,391,529,330,2,17,3,7,15])).
% 72.72/72.80 cnf(546,plain,
% 72.72/72.80 (E(f2(a4,f2(x5461,a1)),f2(f2(a4,x5462),x5463))),
% 72.72/72.80 inference(scs_inference,[],[253,2])).
% 72.72/72.80 cnf(551,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(a4,a1))),
% 72.72/72.80 inference(scs_inference,[],[368,253,468,540,301,2,17,3])).
% 72.72/72.80 cnf(565,plain,
% 72.72/72.80 (E(a4,f2(f2(f2(f2(x5651,x5652),x5651),f2(x5653,a1)),f2(x5654,a1)))),
% 72.72/72.80 inference(scs_inference,[],[306,2])).
% 72.72/72.80 cnf(566,plain,
% 72.72/72.80 (~P1(a3,f2(f2(a4,x5661),x5662))),
% 72.72/72.80 inference(scs_inference,[],[306,135,468,2,17])).
% 72.72/72.80 cnf(569,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(a4,a1),x5691))),
% 72.72/72.80 inference(scs_inference,[],[460,306,551,135,468,2,17,3])).
% 72.72/72.80 cnf(577,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(a4,x5771),f2(x5772,a1)))),
% 72.72/72.80 inference(scs_inference,[],[369,569,436,412,17,3])).
% 72.72/72.80 cnf(587,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(x5871,a1))),
% 72.72/72.80 inference(scs_inference,[],[403,528,577,419,446,425,17,7,3])).
% 72.72/72.80 cnf(590,plain,
% 72.72/72.80 (~E(f2(a3,a4),a1)),
% 72.72/72.80 inference(scs_inference,[],[403,528,577,419,446,425,17,7,3,5])).
% 72.72/72.80 cnf(592,plain,
% 72.72/72.80 (~P1(a3,f2(f2(x5921,x5922),x5921))),
% 72.72/72.80 inference(scs_inference,[],[186,412,17])).
% 72.72/72.80 cnf(596,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(a4,f2(x5961,a1)))),
% 72.72/72.80 inference(scs_inference,[],[546,565,587,186,412,425,17,7,3])).
% 72.72/72.80 cnf(599,plain,
% 72.72/72.80 (~E(a4,f2(a3,f2(f2(x5991,x5992),x5991)))),
% 72.72/72.80 inference(scs_inference,[],[592,16,2])).
% 72.72/72.80 cnf(613,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(x6131,x6132),x6131))),
% 72.72/72.80 inference(scs_inference,[],[385,596,3])).
% 72.72/72.80 cnf(616,plain,
% 72.72/72.80 (~P1(f2(a3,f2(f2(x6161,x6162),x6161)),a4)),
% 72.72/72.80 inference(scs_inference,[],[592,11,16,17])).
% 72.72/72.80 cnf(617,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6171,x6172),x6171)),a4)),
% 72.72/72.80 inference(scs_inference,[],[616,330,7])).
% 72.72/72.80 cnf(619,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(a4,x6191))),
% 72.72/72.80 inference(scs_inference,[],[483,616,613,330,7,3])).
% 72.72/72.80 cnf(625,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(x6251,a1),x6252))),
% 72.72/72.80 inference(scs_inference,[],[478,619,3])).
% 72.72/72.80 cnf(632,plain,
% 72.72/72.80 (~P1(f2(a3,f2(f2(a1,x6321),f2(a1,x6321))),a4)),
% 72.72/72.80 inference(scs_inference,[],[536,11,16,17])).
% 72.72/72.80 cnf(633,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(a1,x6331),f2(a1,x6331))),a4)),
% 72.72/72.80 inference(scs_inference,[],[632,330,7])).
% 72.72/72.80 cnf(640,plain,
% 72.72/72.80 (~E(a4,f2(a3,a4))),
% 72.72/72.80 inference(scs_inference,[],[599,173,3])).
% 72.72/72.80 cnf(642,plain,
% 72.72/72.80 (~P1(f2(a3,f2(f2(a4,x6421),x6422)),a4)),
% 72.72/72.80 inference(scs_inference,[],[566,11,16,17])).
% 72.72/72.80 cnf(647,plain,
% 72.72/72.80 (~P1(a1,f2(f2(a4,x6471),x6472))),
% 72.72/72.80 inference(scs_inference,[],[642,281,516,330,7,3,15])).
% 72.72/72.80 cnf(650,plain,
% 72.72/72.80 (~E(a4,f2(a3,f2(x6501,a1)))),
% 72.72/72.80 inference(scs_inference,[],[119,640,3])).
% 72.72/72.80 cnf(653,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6531,x6531),f2(x6532,x6531))),f2(x6533,x6533))),
% 72.72/72.80 inference(scs_inference,[],[427,541,3])).
% 72.72/72.80 cnf(655,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6551,x6551),f2(x6552,x6551))),f2(x6553,a1))),
% 72.72/72.80 inference(scs_inference,[],[477,653,3])).
% 72.72/72.80 cnf(659,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6591,x6591),f2(x6592,x6591))),f2(a4,x6593))),
% 72.72/72.80 inference(scs_inference,[],[450,655,3])).
% 72.72/72.80 cnf(662,plain,
% 72.72/72.80 (P1(f2(f2(x6621,x6622),x6623),a4)+~E(a1,x6622)),
% 72.72/72.80 inference(scs_inference,[],[12,159,7])).
% 72.72/72.80 cnf(676,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6761,x6762),x6761)),f2(x6763,x6763))),
% 72.72/72.80 inference(scs_inference,[],[427,617,3])).
% 72.72/72.80 cnf(677,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6771,x6772),x6771)),f2(a4,x6773))),
% 72.72/72.80 inference(scs_inference,[],[502,676,3])).
% 72.72/72.80 cnf(689,plain,
% 72.72/72.80 (~E(a4,a1)),
% 72.72/72.80 inference(scs_inference,[],[659,4,2])).
% 72.72/72.80 cnf(691,plain,
% 72.72/72.80 (~E(f2(a1,f2(f2(x6911,x6912),x6911)),f2(x6913,a1))),
% 72.72/72.80 inference(scs_inference,[],[18,40,677,400,7,3])).
% 72.72/72.80 cnf(695,plain,
% 72.72/72.80 (~P1(a1,a4)),
% 72.72/72.80 inference(scs_inference,[],[689,10,17])).
% 72.72/72.80 cnf(699,plain,
% 72.72/72.80 (~E(f2(a4,x6991),a1)),
% 72.72/72.80 inference(scs_inference,[],[695,12,6])).
% 72.72/72.80 cnf(703,plain,
% 72.72/72.80 (~E(f2(x7031,a1),a1)),
% 72.72/72.80 inference(scs_inference,[],[695,104,6])).
% 72.72/72.80 cnf(705,plain,
% 72.72/72.80 (~P1(a1,f2(a4,x7051))),
% 72.72/72.80 inference(scs_inference,[],[695,104,140,699,6,17])).
% 72.72/72.80 cnf(714,plain,
% 72.72/72.80 (P1(f2(f2(x7141,a4),f2(x7142,a4)),f2(f2(x7141,x7142),f2(x7143,a1)))),
% 72.72/72.80 inference(scs_inference,[],[18,13,5,7])).
% 72.72/72.80 cnf(717,plain,
% 72.72/72.80 (~E(f2(f2(x7171,x7172),f2(a1,x7172)),a1)),
% 72.72/72.80 inference(scs_inference,[],[695,446,6])).
% 72.72/72.80 cnf(719,plain,
% 72.72/72.80 (~E(a1,x7191)+E(f2(f2(f2(x7192,x7191),x7193),a4),a4)),
% 72.72/72.80 inference(scs_inference,[],[662,15])).
% 72.72/72.80 cnf(721,plain,
% 72.72/72.80 (~E(f2(f2(x7211,a1),x7212),a1)),
% 72.72/72.80 inference(scs_inference,[],[695,377,6])).
% 72.72/72.80 cnf(730,plain,
% 72.72/72.80 (~E(f2(x7301,x7301),a1)),
% 72.72/72.80 inference(scs_inference,[],[695,425,6])).
% 72.72/72.80 cnf(737,plain,
% 72.72/72.80 (E(f2(f2(x7371,x7372),x7373),a4)+~E(a1,x7372)),
% 72.72/72.80 inference(scs_inference,[],[11,662,17])).
% 72.72/72.80 cnf(739,plain,
% 72.72/72.80 (~E(a1,f2(a3,f2(a4,x7391)))),
% 72.72/72.80 inference(scs_inference,[],[24,132,3])).
% 72.72/72.80 cnf(743,plain,
% 72.72/72.80 (E(f2(f2(x7431,x7432),x7433),f2(a4,x7434))+~E(a1,x7432)),
% 72.72/72.80 inference(scs_inference,[],[26,737,3])).
% 72.72/72.80 cnf(744,plain,
% 72.72/72.80 (E(f2(f2(x7441,a1),x7442),f2(a4,x7443))),
% 72.72/72.80 inference(equality_inference,[],[743])).
% 72.72/72.80 cnf(745,plain,
% 72.72/72.80 (E(f2(a4,x7451),f2(f2(x7452,a1),x7453))),
% 72.72/72.80 inference(scs_inference,[],[744,2])).
% 72.72/72.80 cnf(746,plain,
% 72.72/72.80 (P1(f2(f2(f2(x7461,x7462),f2(a1,x7462)),x7463),f2(a4,x7464))),
% 72.72/72.80 inference(scs_inference,[],[26,744,432,2,7])).
% 72.72/72.80 cnf(747,plain,
% 72.72/72.80 (E(f2(f2(f2(x7471,x7472),f2(a1,x7472)),x7473),f2(a4,a1))),
% 72.72/72.80 inference(scs_inference,[],[26,744,104,432,2,7,17])).
% 72.72/72.80 cnf(750,plain,
% 72.72/72.80 (P1(f2(f2(x7501,x7502),f2(x7503,x7502)),a4)+~E(a1,x7503)),
% 72.72/72.80 inference(scs_inference,[],[13,737,7])).
% 72.72/72.80 cnf(754,plain,
% 72.72/72.80 (E(f2(f2(f2(x7541,a1),x7542),x7543),f2(a4,a1))),
% 72.72/72.80 inference(scs_inference,[],[26,747,104,371,2,7,17])).
% 72.72/72.80 cnf(761,plain,
% 72.72/72.80 (E(f2(f2(f2(a4,x7611),x7612),x7613),f2(a4,a1))),
% 72.72/72.80 inference(scs_inference,[],[26,754,427,104,633,410,2,7,3,17])).
% 72.72/72.80 cnf(765,plain,
% 72.72/72.80 (P1(f2(f2(f2(x7651,x7652),x7651),x7653),f2(a4,x7654))),
% 72.72/72.80 inference(scs_inference,[],[26,761,400,2,7])).
% 72.72/72.80 cnf(766,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(a4,x7661),x7662))),
% 72.72/72.80 inference(scs_inference,[],[26,136,761,529,400,2,7,3])).
% 72.72/72.80 cnf(786,plain,
% 72.72/72.80 (P1(f2(f2(f2(x7861,x7862),a4),f2(x7863,a4)),a4)+~E(a1,x7862)),
% 72.72/72.80 inference(scs_inference,[],[13,719,7])).
% 72.72/72.80 cnf(805,plain,
% 72.72/72.80 (E(f2(f2(f2(x8051,x8052),x8053),a4),f2(x8054,x8054))+~E(a1,x8052)),
% 72.72/72.80 inference(scs_inference,[],[535,719,3])).
% 72.72/72.80 cnf(806,plain,
% 72.72/72.80 (E(f2(f2(f2(x8061,a1),x8062),a4),f2(x8063,x8063))),
% 72.72/72.80 inference(equality_inference,[],[805])).
% 72.72/72.80 cnf(817,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(x8171,x8171))),
% 72.72/72.80 inference(scs_inference,[],[427,529,3])).
% 72.72/72.80 cnf(827,plain,
% 72.72/72.80 (~P1(a3,f2(f2(x8271,a1),x8272))),
% 72.72/72.80 inference(scs_inference,[],[102,377,17])).
% 72.72/72.80 cnf(839,plain,
% 72.72/72.80 (E(f2(f2(x8391,x8392),f2(x8393,x8392)),a4)+~E(a1,x8393)),
% 72.72/72.80 inference(scs_inference,[],[11,750,17])).
% 72.72/72.80 cnf(841,plain,
% 72.72/72.80 (P1(f2(f2(x8411,a4),f2(x8412,a4)),f2(f2(x8411,x8412),f2(a4,x8413)))),
% 72.72/72.80 inference(scs_inference,[],[131,13,7])).
% 72.72/72.80 cnf(847,plain,
% 72.72/72.80 (E(f2(x8471,x8471),f2(f2(x8471,x8471),a4))),
% 72.72/72.80 inference(scs_inference,[],[132,12,481,7,17])).
% 72.72/72.80 cnf(850,plain,
% 72.72/72.80 (E(f2(f2(x8501,x8501),a4),f2(x8501,x8501))),
% 72.72/72.80 inference(scs_inference,[],[132,12,481,7,17,2])).
% 72.72/72.80 cnf(851,plain,
% 72.72/72.80 (~E(f2(a1,f2(a3,a4)),f2(f2(x8511,x8511),a4))),
% 72.72/72.80 inference(scs_inference,[],[132,12,817,481,7,17,2,3])).
% 72.72/72.80 cnf(858,plain,
% 72.72/72.80 (E(f2(f2(f2(x8581,x8581),f2(x8582,x8581)),x8583),f2(a4,x8584))),
% 72.72/72.80 inference(scs_inference,[],[140,336,17])).
% 72.72/72.80 cnf(862,plain,
% 72.72/72.80 (E(f2(a4,x8621),f2(f2(f2(x8622,x8622),f2(x8623,x8622)),x8624))),
% 72.72/72.80 inference(scs_inference,[],[140,336,17,2])).
% 72.72/72.80 cnf(863,plain,
% 72.72/72.80 (E(f2(f2(f2(x8631,x8632),x8631),x8633),f2(a4,x8634))),
% 72.72/72.80 inference(scs_inference,[],[140,765,17])).
% 72.72/72.80 cnf(868,plain,
% 72.72/72.80 (E(f2(f2(f2(x8681,x8682),f2(a1,x8682)),x8683),f2(a4,x8684))),
% 72.72/72.80 inference(scs_inference,[],[140,746,17])).
% 72.72/72.80 cnf(880,plain,
% 72.72/72.80 (~E(a1,x8801)+E(f2(x8802,f2(f2(x8803,x8804),f2(x8801,x8804))),f2(x8802,a4))),
% 72.72/72.80 inference(scs_inference,[],[839,5])).
% 72.72/72.80 cnf(881,plain,
% 72.72/72.80 (E(f2(x8811,f2(f2(x8812,x8813),f2(a1,x8813))),f2(x8811,a4))),
% 72.72/72.80 inference(equality_inference,[],[880])).
% 72.72/72.80 cnf(882,plain,
% 72.72/72.80 (E(f2(x8821,a4),f2(x8821,f2(f2(x8822,x8823),f2(a1,x8823))))),
% 72.72/72.80 inference(scs_inference,[],[881,2])).
% 72.72/72.80 cnf(900,plain,
% 72.72/72.80 (E(f2(f2(x9001,a1),f2(x9001,a1)),f2(x9002,x9002))),
% 72.72/72.80 inference(scs_inference,[],[847,806,3])).
% 72.72/72.80 cnf(903,plain,
% 72.72/72.80 (E(f2(x9031,x9031),f2(f2(x9032,a1),f2(x9032,a1)))),
% 72.72/72.80 inference(scs_inference,[],[847,806,3,2])).
% 72.72/72.80 cnf(906,plain,
% 72.72/72.80 (E(f2(a4,x9061),f2(a4,x9062))),
% 72.72/72.80 inference(scs_inference,[],[142,744,3])).
% 72.72/72.80 cnf(914,plain,
% 72.72/72.80 (E(f2(f2(a4,x9141),f2(x9142,a1)),f2(f2(x9143,a1),f2(x9143,a1)))),
% 72.72/72.80 inference(scs_inference,[],[900,464,3,2])).
% 72.72/72.80 cnf(917,plain,
% 72.72/72.80 (E(f2(x9171,x9171),f2(a4,x9172))),
% 72.72/72.80 inference(scs_inference,[],[903,863,3])).
% 72.72/72.80 cnf(920,plain,
% 72.72/72.80 (E(f2(a4,x9201),f2(x9202,x9202))),
% 72.72/72.80 inference(scs_inference,[],[903,863,3,2])).
% 72.72/72.80 cnf(923,plain,
% 72.72/72.80 (E(f2(f2(a4,x9231),f2(x9232,a1)),f2(x9233,a1))),
% 72.72/72.80 inference(scs_inference,[],[914,454,3])).
% 72.72/72.80 cnf(927,plain,
% 72.72/72.80 (E(f2(f2(x9271,x9272),f2(x9273,x9272)),f2(f2(a4,x9274),x9275))+~E(a1,x9273)),
% 72.72/72.80 inference(scs_inference,[],[149,839,3])).
% 72.72/72.80 cnf(928,plain,
% 72.72/72.80 (E(f2(f2(x9281,x9282),f2(a1,x9282)),f2(f2(a4,x9283),x9284))),
% 72.72/72.80 inference(equality_inference,[],[927])).
% 72.72/72.80 cnf(929,plain,
% 72.72/72.80 (E(f2(f2(a4,x9291),x9292),f2(f2(x9293,x9294),f2(a1,x9294)))),
% 72.72/72.80 inference(scs_inference,[],[928,2])).
% 72.72/72.80 cnf(930,plain,
% 72.72/72.80 (E(f2(a4,a4),f2(f2(a4,x9301),f2(f2(x9302,x9303),x9302)))),
% 72.72/72.80 inference(scs_inference,[],[142,928,173,2,3])).
% 72.72/72.80 cnf(937,plain,
% 72.72/72.80 (E(f2(f2(a4,x9371),x9372),f2(a4,x9373))),
% 72.72/72.80 inference(scs_inference,[],[930,929,858,535,432,2,7,3])).
% 72.72/72.80 cnf(940,plain,
% 72.72/72.80 (E(f2(f2(x9401,x9402),f2(x9403,x9402)),f2(f2(x9404,x9404),f2(x9405,x9404)))+~E(a1,x9403)),
% 72.72/72.80 inference(scs_inference,[],[211,839,3])).
% 72.72/72.80 cnf(941,plain,
% 72.72/72.80 (E(f2(f2(x9411,x9412),f2(a1,x9412)),f2(f2(x9413,x9413),f2(x9414,x9413)))),
% 72.72/72.80 inference(equality_inference,[],[940])).
% 72.72/72.80 cnf(942,plain,
% 72.72/72.80 (E(f2(f2(x9421,x9421),f2(x9422,x9421)),f2(f2(x9423,x9424),f2(a1,x9424)))),
% 72.72/72.80 inference(scs_inference,[],[941,2])).
% 72.72/72.80 cnf(944,plain,
% 72.72/72.80 (E(f2(f2(x9441,x9442),f2(a1,x9442)),f2(a4,x9443))),
% 72.72/72.80 inference(scs_inference,[],[941,868,162,425,2,7,3])).
% 72.72/72.80 cnf(947,plain,
% 72.72/72.80 (E(f2(x9471,x9471),f2(f2(x9471,x9471),x9471))),
% 72.72/72.80 inference(scs_inference,[],[941,868,162,12,425,2,7,3,17])).
% 72.72/72.80 cnf(950,plain,
% 72.72/72.80 (E(f2(f2(x9501,x9501),x9501),f2(x9501,x9501))),
% 72.72/72.80 inference(scs_inference,[],[947,2])).
% 72.72/72.80 cnf(951,plain,
% 72.72/72.80 (E(f2(x9511,x9511),f2(f2(x9512,x9513),f2(a1,x9513)))),
% 72.72/72.80 inference(scs_inference,[],[947,917,309,2,3])).
% 72.72/72.80 cnf(955,plain,
% 72.72/72.80 (E(f2(f2(x9551,x9552),f2(a1,x9552)),f2(x9553,x9553))),
% 72.72/72.80 inference(scs_inference,[],[951,2])).
% 72.72/72.80 cnf(956,plain,
% 72.72/72.80 (E(f2(f2(a4,a4),a4),f2(f2(a4,x9561),f2(x9562,a1)))),
% 72.72/72.80 inference(scs_inference,[],[950,951,502,2,3])).
% 72.72/72.80 cnf(961,plain,
% 72.72/72.80 (E(f2(f2(x9611,x9612),x9611),f2(f2(a4,x9613),x9614))),
% 72.72/72.80 inference(scs_inference,[],[163,956,149,2,3])).
% 72.72/72.80 cnf(963,plain,
% 72.72/72.80 (E(f2(f2(a4,x9631),x9632),f2(f2(x9633,x9634),x9633))),
% 72.72/72.80 inference(scs_inference,[],[961,2])).
% 72.72/72.80 cnf(964,plain,
% 72.72/72.80 (E(f2(f2(x9641,x9642),f2(a1,x9642)),f2(f2(x9643,x9644),f2(a1,x9644)))),
% 72.72/72.80 inference(scs_inference,[],[320,961,359,2,3])).
% 72.72/72.80 cnf(967,plain,
% 72.72/72.80 (E(f2(a4,x9671),f2(f2(x9672,x9673),f2(a1,x9673)))),
% 72.72/72.80 inference(scs_inference,[],[944,2])).
% 72.72/72.80 cnf(968,plain,
% 72.72/72.80 (E(f2(f2(x9681,a1),x9682),f2(x9683,x9683))),
% 72.72/72.80 inference(scs_inference,[],[99,944,535,2,3])).
% 72.72/72.80 cnf(970,plain,
% 72.72/72.80 (E(f2(x9701,x9701),f2(f2(x9702,a1),x9703))),
% 72.72/72.80 inference(scs_inference,[],[968,2])).
% 72.72/72.80 cnf(971,plain,
% 72.72/72.80 (E(f2(f2(x9711,x9711),f2(x9712,x9711)),f2(f2(x9713,a1),x9714))),
% 72.83/72.80 inference(scs_inference,[],[205,968,106,2,3])).
% 72.83/72.80 cnf(973,plain,
% 72.83/72.80 (E(f2(f2(x9731,a1),x9732),f2(f2(x9733,x9733),f2(x9734,x9733)))),
% 72.83/72.80 inference(scs_inference,[],[971,2])).
% 72.83/72.80 cnf(974,plain,
% 72.83/72.80 (E(f2(f2(x9741,x9741),f2(x9742,x9741)),f2(x9743,x9743))),
% 72.83/72.80 inference(scs_inference,[],[971,806,2,3])).
% 72.83/72.80 cnf(978,plain,
% 72.83/72.80 (E(f2(x9781,x9781),f2(f2(x9782,x9782),f2(x9783,x9782)))),
% 72.83/72.80 inference(scs_inference,[],[974,2])).
% 72.83/72.80 cnf(979,plain,
% 72.83/72.80 (E(f2(x9791,x9791),f2(x9792,x9792))),
% 72.83/72.80 inference(scs_inference,[],[974,970,806,2,3])).
% 72.83/72.80 cnf(982,plain,
% 72.83/72.80 (E(a4,f2(f2(f2(x9821,x9822),a4),f2(x9823,a4)))+~E(a1,x9822)),
% 72.83/72.80 inference(scs_inference,[],[11,786,17])).
% 72.83/72.80 cnf(984,plain,
% 72.83/72.80 (E(f2(a4,x9841),f2(f2(a4,x9842),x9843))),
% 72.83/72.80 inference(scs_inference,[],[937,2])).
% 72.83/72.80 cnf(985,plain,
% 72.83/72.80 (E(f2(x9851,x9851),f2(f2(a4,x9852),a4))),
% 72.83/72.80 inference(scs_inference,[],[142,979,937,2,3])).
% 72.83/72.80 cnf(991,plain,
% 72.83/72.80 (E(f2(f2(a4,x9911),x9912),f2(x9913,x9913))),
% 72.83/72.80 inference(scs_inference,[],[963,985,950,2,3])).
% 72.83/72.80 cnf(994,plain,
% 72.83/72.80 (E(f2(x9941,x9941),f2(f2(a4,x9942),x9943))),
% 72.83/72.80 inference(scs_inference,[],[991,2])).
% 72.83/72.80 cnf(995,plain,
% 72.83/72.80 (E(f2(x9951,x9951),f2(f2(f2(x9952,x9952),f2(x9952,x9952)),f2(x9952,x9952)))),
% 72.83/72.80 inference(scs_inference,[],[978,991,947,2,3])).
% 72.83/72.80 cnf(998,plain,
% 72.83/72.80 (E(f2(x9981,x9981),f2(f2(f2(x9982,x9983),x9984),a4))+~E(a1,x9983)),
% 72.83/72.80 inference(scs_inference,[],[805,2])).
% 72.83/72.80 cnf(1000,plain,
% 72.83/72.80 (E(f2(f2(f2(x10001,x10001),f2(x10001,x10001)),f2(x10001,x10001)),f2(x10002,x10002))),
% 72.83/72.80 inference(scs_inference,[],[995,2])).
% 72.83/72.80 cnf(1001,plain,
% 72.83/72.80 (E(f2(f2(x10011,x10012),f2(a1,x10012)),f2(f2(x10013,x10013),a4))),
% 72.83/72.80 inference(scs_inference,[],[995,955,847,2,3])).
% 72.83/72.80 cnf(1005,plain,
% 72.83/72.80 (E(f2(f2(x10051,x10051),a4),f2(f2(x10052,x10053),f2(a1,x10053)))),
% 72.83/72.80 inference(scs_inference,[],[1001,2])).
% 72.83/72.80 cnf(1006,plain,
% 72.83/72.80 (E(f2(f2(f2(x10061,x10061),f2(x10061,x10061)),f2(x10061,x10061)),f2(f2(x10062,x10062),a4))),
% 72.83/72.80 inference(scs_inference,[],[1000,1001,2,3])).
% 72.83/72.80 cnf(1011,plain,
% 72.83/72.80 (E(f2(f2(x10111,x10111),a4),f2(f2(f2(x10112,x10112),f2(x10112,x10112)),f2(x10112,x10112)))),
% 72.83/72.80 inference(scs_inference,[],[1006,2])).
% 72.83/72.80 cnf(1012,plain,
% 72.83/72.80 (E(f2(a4,x10121),f2(f2(x10122,x10122),a4))),
% 72.83/72.80 inference(scs_inference,[],[1006,862,2,3])).
% 72.83/72.80 cnf(1015,plain,
% 72.83/72.80 (P1(f2(x10151,x10151),f2(a1,f2(f2(x10152,x10153),x10152)))+~E(a1,x10154)),
% 72.83/72.80 inference(scs_inference,[],[353,805,6])).
% 72.83/72.80 cnf(1016,plain,
% 72.83/72.80 (P1(f2(x10161,x10161),f2(a1,f2(f2(x10162,x10163),x10162)))),
% 72.83/72.80 inference(equality_inference,[],[1015])).
% 72.83/72.80 cnf(1017,plain,
% 72.83/72.80 (E(f2(f2(x10171,x10171),a4),f2(a4,x10172))),
% 72.83/72.80 inference(scs_inference,[],[1012,2])).
% 72.83/72.80 cnf(1018,plain,
% 72.83/72.80 (P1(f2(x10181,x10181),f2(a1,a4))),
% 72.83/72.80 inference(scs_inference,[],[1012,119,1016,2,7])).
% 72.83/72.80 cnf(1021,plain,
% 72.83/72.80 (E(f2(f2(a4,a4),a4),f2(f2(x10211,x10211),a4))),
% 72.83/72.80 inference(scs_inference,[],[850,1012,119,1016,2,7,3])).
% 72.83/72.80 cnf(1030,plain,
% 72.83/72.80 (E(f2(f2(x10301,x10301),a4),f2(x10302,x10302))),
% 72.83/72.80 inference(scs_inference,[],[1011,1021,1000,882,1018,2,7,3])).
% 72.83/72.80 cnf(1032,plain,
% 72.83/72.80 (E(f2(x10321,x10321),f2(a1,a4))+~P1(f2(a1,a4),f2(x10321,x10321))),
% 72.83/72.80 inference(scs_inference,[],[1011,1021,1000,882,1018,2,7,3,17])).
% 72.83/72.80 cnf(1034,plain,
% 72.83/72.80 (~P1(f2(a1,a4),f2(x10341,x10341))+E(f2(a1,a4),f2(x10341,x10341))),
% 72.83/72.80 inference(scs_inference,[],[1032,2])).
% 72.83/72.80 cnf(1035,plain,
% 72.83/72.80 (E(f2(x10351,x10351),f2(f2(x10352,x10352),a4))),
% 72.83/72.80 inference(scs_inference,[],[1030,2])).
% 72.83/72.80 cnf(1036,plain,
% 72.83/72.80 (E(f2(f2(x10361,x10361),a4),f2(f2(x10362,a1),x10363))),
% 72.83/72.80 inference(scs_inference,[],[1030,745,2,3])).
% 72.83/72.80 cnf(1041,plain,
% 72.83/72.80 (E(f2(a1,a4),f2(x10411,x10411))+~E(f2(f2(a1,a4),f2(x10411,x10411)),a4)),
% 72.83/72.80 inference(scs_inference,[],[1034,16])).
% 72.83/72.80 cnf(1043,plain,
% 72.83/72.80 (E(f2(f2(x10431,x10431),f2(x10432,x10431)),f2(f2(x10433,x10433),a4))),
% 72.83/72.80 inference(scs_inference,[],[942,1035,1036,2,3])).
% 72.83/72.80 cnf(1047,plain,
% 72.83/72.80 (E(f2(f2(x10471,x10471),a4),f2(f2(x10472,x10472),f2(x10473,x10472)))),
% 72.83/72.80 inference(scs_inference,[],[1043,2])).
% 72.83/72.80 cnf(1048,plain,
% 72.83/72.80 (E(f2(x10481,x10481),f2(x10482,a1))),
% 72.83/72.80 inference(scs_inference,[],[994,1043,923,2,3])).
% 72.83/72.80 cnf(1052,plain,
% 72.83/72.80 (E(f2(x10521,a1),f2(x10522,x10522))),
% 72.83/72.80 inference(scs_inference,[],[1048,2])).
% 72.83/72.80 cnf(1053,plain,
% 72.83/72.80 (E(f2(f2(x10531,x10532),x10531),f2(f2(x10533,x10534),x10533))),
% 72.83/72.80 inference(scs_inference,[],[163,1048,162,2,3])).
% 72.83/72.80 cnf(1054,plain,
% 72.83/72.80 (E(f2(f2(x10541,x10542),x10541),f2(x10543,x10543))),
% 72.83/72.80 inference(scs_inference,[],[1053,950,3])).
% 72.83/72.80 cnf(1057,plain,
% 72.83/72.80 (E(f2(x10571,x10571),f2(f2(x10572,x10573),x10572))),
% 72.83/72.80 inference(scs_inference,[],[1053,950,3,2])).
% 72.83/72.80 cnf(1058,plain,
% 72.83/72.80 (E(f2(f2(x10581,x10582),x10581),f2(f2(x10583,x10583),a4))),
% 72.83/72.80 inference(scs_inference,[],[1054,1035,3])).
% 72.83/72.80 cnf(1060,plain,
% 72.83/72.80 (E(f2(f2(x10601,x10601),a4),f2(f2(x10602,x10603),x10602))),
% 72.83/72.80 inference(scs_inference,[],[1054,1035,3,2])).
% 72.83/72.80 cnf(1062,plain,
% 72.83/72.80 (E(f2(x10621,x10621),f2(f2(f2(x10622,x10623),x10622),f2(x10624,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1057,477,3])).
% 72.83/72.80 cnf(1065,plain,
% 72.83/72.80 (E(f2(f2(f2(x10651,x10652),x10651),f2(x10653,a1)),f2(x10654,x10654))),
% 72.83/72.80 inference(scs_inference,[],[1057,477,3,2])).
% 72.83/72.80 cnf(1066,plain,
% 72.83/72.80 (E(f2(f2(f2(x10661,x10662),x10661),f2(x10663,a1)),f2(f2(a4,x10664),x10665))),
% 72.83/72.80 inference(scs_inference,[],[1065,984,3])).
% 72.83/72.80 cnf(1072,plain,
% 72.83/72.80 (E(f2(f2(f2(x10721,x10722),x10721),f2(x10723,a1)),f2(f2(x10724,x10724),f2(x10725,x10724)))),
% 72.83/72.80 inference(scs_inference,[],[1066,1047,3])).
% 72.83/72.80 cnf(1075,plain,
% 72.83/72.80 (E(f2(f2(x10751,x10751),f2(x10752,x10751)),f2(f2(f2(x10753,x10754),x10753),f2(x10755,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1066,1047,3,2])).
% 72.83/72.80 cnf(1076,plain,
% 72.83/72.80 (E(f2(f2(f2(x10761,x10762),x10761),f2(x10763,a1)),f2(f2(x10764,x10764),a4))),
% 72.83/72.80 inference(scs_inference,[],[1072,1043,3])).
% 72.83/72.80 cnf(1078,plain,
% 72.83/72.80 (E(f2(f2(x10781,x10781),a4),f2(f2(f2(x10782,x10783),x10782),f2(x10784,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1072,1043,3,2])).
% 72.83/72.80 cnf(1083,plain,
% 72.83/72.80 (E(a4,f2(f2(x10831,x10831),a4))),
% 72.83/72.80 inference(scs_inference,[],[149,1035,3])).
% 72.83/72.80 cnf(1086,plain,
% 72.83/72.80 (E(f2(f2(x10861,x10861),a4),a4)),
% 72.83/72.80 inference(scs_inference,[],[149,1035,3,2])).
% 72.83/72.80 cnf(1095,plain,
% 72.83/72.80 (E(f2(f2(x10951,x10952),x10951),f2(x10953,a1))),
% 72.83/72.80 inference(scs_inference,[],[163,18,3])).
% 72.83/72.80 cnf(1096,plain,
% 72.83/72.80 (E(f2(x10961,a1),f2(f2(x10962,x10963),x10962))),
% 72.83/72.80 inference(scs_inference,[],[163,18,3,2])).
% 72.83/72.80 cnf(1102,plain,
% 72.83/72.80 (E(f2(f2(x11021,x11021),f2(f2(x11022,x11023),x11022)),f2(a4,x11024))),
% 72.83/72.80 inference(scs_inference,[],[172,1017,3])).
% 72.83/72.80 cnf(1105,plain,
% 72.83/72.80 (E(f2(f2(x11051,x11051),f2(f2(x11052,x11053),x11052)),a4)),
% 72.83/72.80 inference(scs_inference,[],[172,1102,1086,2,3])).
% 72.83/72.80 cnf(1109,plain,
% 72.83/72.80 (E(a4,f2(f2(x11091,x11091),f2(f2(x11092,x11093),x11092)))),
% 72.83/72.80 inference(scs_inference,[],[1105,2])).
% 72.83/72.80 cnf(1110,plain,
% 72.83/72.80 (E(f2(f2(x11101,x11101),f2(f2(x11102,x11103),x11102)),f2(x11104,x11104))),
% 72.83/72.80 inference(scs_inference,[],[172,1105,1030,2,3])).
% 72.83/72.80 cnf(1114,plain,
% 72.83/72.80 (E(f2(x11141,x11141),f2(f2(x11142,x11142),f2(f2(x11143,x11144),x11143)))),
% 72.83/72.80 inference(scs_inference,[],[1110,2])).
% 72.83/72.80 cnf(1116,plain,
% 72.83/72.80 (E(f2(f2(x11161,x11161),f2(f2(x11162,x11163),x11162)),f2(x11164,a1))),
% 72.83/72.80 inference(scs_inference,[],[1110,923,1109,425,2,7,3])).
% 72.83/72.80 cnf(1122,plain,
% 72.83/72.80 (E(f2(f2(x11221,x11221),a4),f2(x11222,a1))),
% 72.83/72.80 inference(scs_inference,[],[173,1116,3])).
% 72.83/72.80 cnf(1125,plain,
% 72.83/72.80 (E(f2(x11251,a1),f2(f2(x11252,x11252),a4))),
% 72.83/72.80 inference(scs_inference,[],[173,1116,3,2])).
% 72.83/72.80 cnf(1133,plain,
% 72.83/72.80 (E(f2(x11331,a1),f2(f2(f2(x11332,x11333),x11332),a4))),
% 72.83/72.80 inference(scs_inference,[],[173,454,3,2])).
% 72.83/72.80 cnf(1136,plain,
% 72.83/72.80 (P1(f2(f2(f2(x11361,a1),a4),f2(x11362,a4)),f2(f2(x11363,a1),x11364))),
% 72.83/72.80 inference(scs_inference,[],[176,714,7])).
% 72.83/72.80 cnf(1138,plain,
% 72.83/72.80 (E(f2(f2(x11381,x11382),x11381),f2(f2(x11383,a1),x11384))),
% 72.83/72.80 inference(rename_variables,[],[176])).
% 72.83/72.80 cnf(1142,plain,
% 72.83/72.80 (E(f2(f2(a1,a1),f2(x11421,a1)),f2(f2(f2(x11422,a1),a4),f2(x11423,a4)))),
% 72.83/72.80 inference(scs_inference,[],[176,257,714,7,17,2])).
% 72.83/72.80 cnf(1143,plain,
% 72.83/72.80 (E(f2(f2(x11431,x11432),x11431),f2(f2(f2(x11433,a1),a4),f2(x11434,a4)))),
% 72.83/72.80 inference(scs_inference,[],[176,1138,257,714,7,17,2,3])).
% 72.83/72.80 cnf(1146,plain,
% 72.83/72.80 (E(f2(f2(f2(x11461,a1),a4),f2(x11462,a4)),f2(f2(x11463,x11464),x11463))),
% 72.83/72.80 inference(scs_inference,[],[1143,2])).
% 72.83/72.80 cnf(1147,plain,
% 72.83/72.80 (P1(f2(f2(f2(a4,x11471),a4),f2(x11472,a4)),f2(f2(x11473,a1),x11474))),
% 72.83/72.80 inference(scs_inference,[],[176,1143,841,2,7])).
% 72.83/72.80 cnf(1150,plain,
% 72.83/72.80 (E(f2(f2(f2(a4,x11501),a4),f2(x11502,a4)),f2(f2(a1,a1),f2(x11503,a1)))),
% 72.83/72.80 inference(scs_inference,[],[176,1143,257,841,2,7,17])).
% 72.83/72.80 cnf(1153,plain,
% 72.83/72.80 (E(f2(f2(a1,a1),f2(x11531,a1)),f2(f2(f2(a4,x11532),a4),f2(x11533,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1150,2])).
% 72.83/72.80 cnf(1154,plain,
% 72.83/72.80 (E(f2(f2(x11541,x11542),x11541),f2(f2(f2(a4,x11543),a4),f2(x11544,a4)))),
% 72.83/72.80 inference(scs_inference,[],[176,1150,2,3])).
% 72.83/72.80 cnf(1157,plain,
% 72.83/72.80 (E(f2(f2(f2(a4,x11571),a4),f2(x11572,a4)),f2(f2(x11573,x11574),x11573))),
% 72.83/72.80 inference(scs_inference,[],[1154,2])).
% 72.83/72.80 cnf(1158,plain,
% 72.83/72.80 (P1(f2(f2(f2(x11581,a1),a4),f2(x11582,a4)),f2(f2(x11583,x11584),x11583))),
% 72.83/72.80 inference(scs_inference,[],[177,1136,7])).
% 72.83/72.80 cnf(1163,plain,
% 72.83/72.80 (E(f2(f2(f2(x11631,a1),a4),f2(x11632,a4)),f2(x11633,x11633))),
% 72.83/72.80 inference(scs_inference,[],[177,1114,1142,1136,7,3,2])).
% 72.83/72.80 cnf(1166,plain,
% 72.83/72.80 (E(f2(f2(x11661,a1),x11662),f2(f2(f2(a4,x11663),a4),f2(x11664,a4)))),
% 72.83/72.80 inference(scs_inference,[],[177,973,1153,1147,7,3])).
% 72.83/72.80 cnf(1174,plain,
% 72.83/72.80 (E(f2(f2(x11741,x11741),f2(x11742,x11741)),f2(f2(f2(a4,x11743),a4),f2(x11744,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1075,1166,3])).
% 72.83/72.80 cnf(1178,plain,
% 72.83/72.80 (E(f2(f2(f2(x11781,a1),a4),f2(x11782,a4)),f2(f2(x11783,x11784),f2(a1,x11784)))),
% 72.83/72.80 inference(scs_inference,[],[1163,967,3])).
% 72.83/72.80 cnf(1186,plain,
% 72.83/72.80 (E(f2(f2(f2(x11861,a1),a4),f2(x11862,a4)),f2(x11863,a1))),
% 72.83/72.80 inference(scs_inference,[],[1146,1122,3])).
% 72.83/72.80 cnf(1190,plain,
% 72.83/72.80 (E(f2(f2(f2(a4,x11901),a4),f2(x11902,a4)),f2(f2(x11903,x11904),f2(a1,x11904)))),
% 72.83/72.80 inference(scs_inference,[],[1157,1005,3])).
% 72.83/72.80 cnf(1200,plain,
% 72.83/72.80 (E(f2(f2(f2(a4,x12001),a4),f2(x12002,a4)),f2(x12003,x12003))),
% 72.83/72.80 inference(scs_inference,[],[1062,1166,3,2])).
% 72.83/72.80 cnf(1203,plain,
% 72.83/72.80 (E(f2(f2(f2(a4,x12031),a4),f2(x12032,a4)),f2(f2(x12033,x12033),a4))),
% 72.83/72.80 inference(scs_inference,[],[1200,1125,3])).
% 72.83/72.80 cnf(1211,plain,
% 72.83/72.80 (E(f2(f2(x12111,x12111),f2(x12112,x12111)),f2(f2(f2(x12113,x12114),a4),f2(x12115,a4)))+~E(a1,x12114)),
% 72.83/72.80 inference(scs_inference,[],[205,982,3])).
% 72.83/72.80 cnf(1212,plain,
% 72.83/72.80 (E(f2(f2(x12121,x12121),f2(x12122,x12121)),f2(f2(f2(x12123,a1),a4),f2(x12124,a4)))),
% 72.83/72.80 inference(equality_inference,[],[1211])).
% 72.83/72.80 cnf(1213,plain,
% 72.83/72.80 (E(f2(f2(f2(x12131,a1),a4),f2(x12132,a4)),f2(f2(x12133,x12133),f2(x12134,x12133)))),
% 72.83/72.80 inference(scs_inference,[],[1212,2])).
% 72.83/72.80 cnf(1257,plain,
% 72.83/72.80 (E(f2(x12571,a1),f2(f2(f2(x12572,x12573),x12574),a4))+~E(a1,x12573)),
% 72.83/72.80 inference(scs_inference,[],[248,998,3])).
% 72.83/72.80 cnf(1265,plain,
% 72.83/72.80 (E(f2(f2(f2(x12651,a1),a4),f2(x12652,a4)),f2(f2(a4,x12653),x12654))),
% 72.83/72.80 inference(scs_inference,[],[1178,1066,3])).
% 72.83/72.80 cnf(1269,plain,
% 72.83/72.80 (E(f2(f2(f2(a4,x12691),a4),f2(x12692,a4)),f2(f2(a4,x12693),x12694))),
% 72.83/72.80 inference(scs_inference,[],[1190,1265,1066,2,3])).
% 72.83/72.80 cnf(1272,plain,
% 72.83/72.80 (E(f2(x12721,x12721),f2(a1,a4))+~E(f2(f2(a1,a4),f2(x12721,x12721)),a4)),
% 72.83/72.80 inference(scs_inference,[],[1032,16])).
% 72.83/72.80 cnf(1274,plain,
% 72.83/72.80 (E(f2(f2(f2(x12741,x12741),f2(x12742,x12741)),x12743),f2(x12744,x12744))),
% 72.83/72.80 inference(scs_inference,[],[256,1269,535,2,3])).
% 72.83/72.80 cnf(1276,plain,
% 72.83/72.80 (E(f2(x12761,x12761),f2(f2(f2(x12762,x12762),f2(x12763,x12762)),x12764))),
% 72.83/72.80 inference(scs_inference,[],[1274,2])).
% 72.83/72.80 cnf(1277,plain,
% 72.83/72.80 (E(f2(f2(f2(x12771,x12771),f2(x12772,x12771)),x12773),f2(x12774,a1))),
% 72.83/72.80 inference(scs_inference,[],[1274,1186,2,3])).
% 72.83/72.80 cnf(1282,plain,
% 72.83/72.80 (E(f2(x12821,x12821),f2(f2(f2(x12822,x12823),x12822),a4))),
% 72.83/72.80 inference(scs_inference,[],[1276,1277,1133,2,3])).
% 72.83/72.80 cnf(1285,plain,
% 72.83/72.80 (E(f2(f2(f2(x12851,x12852),x12851),a4),f2(x12853,x12853))),
% 72.83/72.80 inference(scs_inference,[],[1282,2])).
% 72.83/72.80 cnf(1286,plain,
% 72.83/72.80 (~P1(f2(a1,a4),f2(x12861,x12861))+E(f2(f2(x12861,x12861),x12862),f2(f2(a1,a4),x12862))),
% 72.83/72.80 inference(scs_inference,[],[1032,4])).
% 72.83/72.80 cnf(1287,plain,
% 72.83/72.80 (E(f2(f2(x12871,x12871),x12872),f2(f2(a1,a4),x12872))+~E(f2(f2(x12873,x12873),f2(x12874,x12873)),f2(a1,a4))),
% 72.83/72.80 inference(scs_inference,[],[257,1286,6])).
% 72.83/72.80 cnf(1288,plain,
% 72.83/72.80 (~E(f2(f2(x12881,x12881),f2(x12882,x12881)),f2(a1,a4))+E(f2(f2(a1,a4),x12883),f2(f2(x12884,x12884),x12883))),
% 72.83/72.80 inference(scs_inference,[],[1287,2])).
% 72.83/72.80 cnf(1290,plain,
% 72.83/72.80 (E(f2(f2(a4,x12901),x12902),f2(x12903,a1))),
% 72.83/72.80 inference(scs_inference,[],[262,397,3])).
% 72.83/72.80 cnf(1293,plain,
% 72.83/72.80 (E(f2(x12931,a1),f2(f2(a4,x12932),x12933))),
% 72.83/72.80 inference(scs_inference,[],[262,397,3,2])).
% 72.83/72.80 cnf(1297,plain,
% 72.83/72.80 (E(f2(x12971,x12971),f2(a1,a4))+~E(f2(f2(x12971,x12971),x12972),f2(a1,a4))),
% 72.83/72.80 inference(scs_inference,[],[12,1032,6])).
% 72.83/72.80 cnf(1300,plain,
% 72.83/72.80 (~E(f2(f2(x13001,x13001),x13002),f2(a1,a4))+E(f2(a1,a4),f2(x13001,x13001))),
% 72.83/72.80 inference(scs_inference,[],[1297,2])).
% 72.83/72.80 cnf(1304,plain,
% 72.83/72.80 (P1(f2(f2(f2(x13041,x13042),x13041),f2(x13043,a1)),f2(a1,a4))),
% 72.83/72.80 inference(scs_inference,[],[297,1018,6])).
% 72.83/72.80 cnf(1306,plain,
% 72.83/72.80 (E(f2(f2(x13061,a1),x13062),f2(f2(f2(x13063,x13064),x13063),f2(x13065,a1)))),
% 72.83/72.80 inference(rename_variables,[],[297])).
% 72.83/72.80 cnf(1307,plain,
% 72.83/72.80 (E(f2(f2(x13071,a1),x13072),f2(f2(a4,x13073),x13074))),
% 72.83/72.80 inference(scs_inference,[],[297,1306,1066,1018,6,3])).
% 72.83/72.80 cnf(1309,plain,
% 72.83/72.80 (E(f2(f2(a4,x13091),x13092),f2(f2(x13093,a1),x13094))),
% 72.83/72.80 inference(scs_inference,[],[297,1306,1066,1018,6,3,2])).
% 72.83/72.80 cnf(1310,plain,
% 72.83/72.80 (E(f2(f2(f2(x13101,x13102),x13101),f2(x13103,a1)),f2(a1,a4))+~P1(f2(a1,a4),f2(f2(f2(x13101,x13102),x13101),f2(x13103,a1)))),
% 72.83/72.80 inference(scs_inference,[],[297,1306,1066,1018,6,3,2,17])).
% 72.83/72.80 cnf(1314,plain,
% 72.83/72.80 (~P1(a3,f2(f2(x13141,x13142),f2(a1,x13142)))),
% 72.83/72.80 inference(scs_inference,[],[301,446,17])).
% 72.83/72.80 cnf(1319,plain,
% 72.83/72.80 (E(f2(x13191,x13191),f2(f2(f2(f2(x13192,x13193),x13192),f2(x13194,a1)),f2(x13195,a1)))),
% 72.83/72.80 inference(scs_inference,[],[306,535,3,2])).
% 72.83/72.80 cnf(1330,plain,
% 72.83/72.80 (P1(f2(f2(f2(x13301,x13302),a4),f2(x13301,a4)),f2(f2(x13303,a1),x13304))),
% 72.83/72.80 inference(scs_inference,[],[319,714,7])).
% 72.83/72.80 cnf(1342,plain,
% 72.83/72.80 (E(f2(f2(a1,a1),f2(x13421,a1)),f2(f2(f2(x13422,x13423),a4),f2(x13422,a4)))),
% 72.83/72.80 inference(scs_inference,[],[257,1330,17,2])).
% 72.83/72.80 cnf(1345,plain,
% 72.83/72.80 (P1(f2(f2(f2(x13451,x13452),a4),f2(x13451,a4)),a4)),
% 72.83/72.80 inference(scs_inference,[],[320,1330,7])).
% 72.83/72.80 cnf(1348,plain,
% 72.83/72.80 (E(f2(f2(a4,x13481),x13482),f2(f2(f2(x13483,x13484),a4),f2(x13483,a4)))),
% 72.83/72.80 inference(scs_inference,[],[320,1309,1342,1330,7,3])).
% 72.83/72.80 cnf(1350,plain,
% 72.83/72.80 (E(f2(f2(f2(x13501,x13502),a4),f2(x13501,a4)),f2(f2(a4,x13503),x13504))),
% 72.83/72.80 inference(scs_inference,[],[320,1309,1342,1330,7,3,2])).
% 72.83/72.80 cnf(1352,plain,
% 72.83/72.80 (E(f2(f2(f2(x13521,x13522),a4),f2(x13521,a4)),a4)),
% 72.83/72.80 inference(scs_inference,[],[320,695,1309,1342,11,1330,7,3,2,6,17])).
% 72.83/72.80 cnf(1358,plain,
% 72.83/72.80 (E(a4,f2(f2(f2(x13581,x13582),a4),f2(x13581,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1352,2])).
% 72.83/72.80 cnf(1359,plain,
% 72.83/72.80 (E(f2(f2(x13591,a1),x13592),f2(f2(f2(x13593,x13594),a4),f2(x13593,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1307,1348,1352,2,3])).
% 72.83/72.80 cnf(1361,plain,
% 72.83/72.80 (E(f2(f2(f2(x13611,x13612),a4),f2(x13611,a4)),f2(f2(x13613,a1),x13614))),
% 72.83/72.80 inference(scs_inference,[],[1359,2])).
% 72.83/72.80 cnf(1363,plain,
% 72.83/72.80 (E(f2(f2(x13631,x13632),f2(a1,x13632)),f2(f2(f2(x13633,x13634),a4),f2(x13633,a4)))),
% 72.83/72.80 inference(scs_inference,[],[320,1359,1358,425,2,7,3])).
% 72.83/72.80 cnf(1366,plain,
% 72.83/72.80 (E(f2(f2(f2(x13661,x13662),a4),f2(x13661,a4)),f2(x13663,x13663))),
% 72.83/72.80 inference(scs_inference,[],[1363,1361,1285,2,3])).
% 72.83/72.80 cnf(1370,plain,
% 72.83/72.80 (E(f2(x13701,x13701),f2(f2(f2(x13702,x13703),a4),f2(x13702,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1366,2])).
% 72.83/72.80 cnf(1371,plain,
% 72.83/72.80 (E(f2(f2(f2(x13711,x13712),a4),f2(x13711,a4)),f2(f2(x13713,x13713),f2(x13714,x13713)))),
% 72.83/72.80 inference(scs_inference,[],[1366,1213,2,3])).
% 72.83/72.80 cnf(1375,plain,
% 72.83/72.80 (E(f2(f2(x13751,x13751),f2(x13752,x13751)),f2(f2(f2(x13753,x13754),a4),f2(x13753,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1371,2])).
% 72.83/72.80 cnf(1376,plain,
% 72.83/72.80 (E(f2(f2(f2(x13761,x13762),a4),f2(x13761,a4)),f2(f2(x13763,x13764),x13763))),
% 72.83/72.80 inference(scs_inference,[],[1371,1057,2,3])).
% 72.83/72.80 cnf(1381,plain,
% 72.83/72.80 (E(f2(f2(f2(x13811,x13812),a4),f2(x13811,a4)),f2(a4,x13813))),
% 72.83/72.80 inference(scs_inference,[],[1376,858,2,3])).
% 72.83/72.80 cnf(1385,plain,
% 72.83/72.80 (E(f2(a4,x13851),f2(f2(f2(x13852,x13853),a4),f2(x13852,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1381,2])).
% 72.83/72.80 cnf(1386,plain,
% 72.83/72.80 (E(f2(f2(f2(x13861,x13862),a4),f2(x13861,a4)),f2(x13863,a1))),
% 72.83/72.80 inference(scs_inference,[],[1350,1381,1122,2,3])).
% 72.83/72.80 cnf(1390,plain,
% 72.83/72.80 (E(f2(x13901,a1),f2(f2(f2(x13902,x13903),a4),f2(x13902,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1386,2])).
% 72.83/72.80 cnf(1401,plain,
% 72.83/72.80 (~P1(f2(a1,a4),f2(f2(x14011,x14011),f2(x14011,x14011)))+E(f2(a1,a4),f2(x14011,x14011))),
% 72.83/72.80 inference(scs_inference,[],[1032,1300])).
% 72.83/72.80 cnf(1402,plain,
% 72.83/72.80 (E(f2(a1,a4),f2(x14021,x14021))+~E(f2(f2(f2(x14021,x14021),f2(x14021,x14021)),x14022),f2(a1,a4))),
% 72.83/72.80 inference(scs_inference,[],[12,1401,6])).
% 72.83/72.80 cnf(1404,plain,
% 72.83/72.80 (~E(f2(a1,a4),f2(f2(f2(x14041,x14041),f2(x14041,x14041)),x14042))+E(f2(a1,a4),f2(x14041,x14041))),
% 72.83/72.80 inference(scs_inference,[],[1402,2])).
% 72.83/72.80 cnf(1405,plain,
% 72.83/72.80 (E(f2(a1,a4),f2(x14051,x14051))+~E(f2(a1,a4),f2(a4,x14052))),
% 72.83/72.80 inference(scs_inference,[],[920,1404,3])).
% 72.83/72.80 cnf(1410,plain,
% 72.83/72.80 (~E(f2(a1,a4),f2(a4,x14101))+E(f2(f2(a1,a4),x14102),f2(f2(x14103,x14103),x14102))),
% 72.83/72.80 inference(scs_inference,[],[1405,4])).
% 72.83/72.80 cnf(1413,plain,
% 72.83/72.80 (E(f2(f2(x14131,x14131),f2(x14132,a1)),f2(f2(x14133,x14134),x14133))),
% 72.83/72.80 inference(scs_inference,[],[1058,118,3,2])).
% 72.83/72.80 cnf(1415,plain,
% 72.83/72.80 (E(f2(f2(x14151,x14151),f2(x14152,a1)),a4)),
% 72.83/72.80 inference(scs_inference,[],[404,1413,3])).
% 72.83/72.80 cnf(1418,plain,
% 72.83/72.80 (E(a4,f2(f2(x14181,x14181),f2(x14182,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1415,2])).
% 72.83/72.80 cnf(1419,plain,
% 72.83/72.80 (E(f2(f2(x14191,a1),x14192),f2(f2(x14193,x14193),f2(x14194,a1)))),
% 72.83/72.80 inference(scs_inference,[],[99,1415,2,3])).
% 72.83/72.80 cnf(1420,plain,
% 72.83/72.80 (~P1(f2(a1,a4),f2(x14201,x14201))+E(f2(x14201,x14201),f2(a1,f2(f2(x14202,x14203),f2(a1,x14203))))),
% 72.83/72.80 inference(scs_inference,[],[882,1032,3])).
% 72.83/72.80 cnf(1421,plain,
% 72.83/72.80 (E(f2(f2(x14211,x14211),f2(x14212,a1)),f2(f2(x14213,a1),x14214))),
% 72.83/72.80 inference(scs_inference,[],[1419,2])).
% 72.83/72.80 cnf(1423,plain,
% 72.83/72.80 (E(f2(f2(a4,x14231),x14232),f2(f2(x14233,x14233),f2(x14234,a1)))),
% 72.83/72.80 inference(scs_inference,[],[136,1419,1418,425,2,7,3])).
% 72.83/72.80 cnf(1424,plain,
% 72.83/72.80 (E(f2(x14241,x14241),f2(a1,f2(f2(x14242,x14243),f2(a1,x14243))))+~E(f2(f2(a1,a4),f2(x14241,x14241)),a4)),
% 72.83/72.80 inference(scs_inference,[],[1420,16])).
% 72.83/72.80 cnf(1425,plain,
% 72.83/72.80 (E(f2(f2(x14251,x14251),f2(x14252,a1)),f2(f2(a4,x14253),x14254))),
% 72.83/72.80 inference(scs_inference,[],[1423,2])).
% 72.83/72.80 cnf(1427,plain,
% 72.83/72.80 (E(f2(f2(x14271,x14271),f2(x14272,a1)),f2(f2(f2(x14273,x14274),x14273),f2(x14275,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1421,1423,1078,1418,1345,2,7,3])).
% 72.83/72.80 cnf(1430,plain,
% 72.83/72.80 (~E(f2(f2(a1,a4),f2(a1,a1)),a4)),
% 72.83/72.80 inference(scs_inference,[],[691,1424,2])).
% 72.83/72.80 cnf(1431,plain,
% 72.83/72.80 (~P1(f2(a1,a4),f2(a1,a1))),
% 72.83/72.80 inference(scs_inference,[],[1430,15])).
% 72.83/72.80 cnf(1433,plain,
% 72.83/72.80 (E(f2(f2(f2(x14331,x14332),x14331),f2(x14333,a1)),f2(f2(x14334,x14334),f2(x14335,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1427,1430,15,2])).
% 72.83/72.80 cnf(1434,plain,
% 72.83/72.80 (E(f2(f2(x14341,x14341),f2(x14342,a1)),f2(f2(f2(x14343,x14344),a4),f2(x14343,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1427,1425,1390,1430,15,2,3])).
% 72.83/72.80 cnf(1438,plain,
% 72.83/72.80 (E(f2(f2(f2(x14381,x14382),a4),f2(x14381,a4)),f2(f2(x14383,x14383),f2(x14384,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1434,2])).
% 72.83/72.80 cnf(1439,plain,
% 72.83/72.80 (E(f2(x14391,x14391),f2(f2(x14392,x14392),f2(x14393,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1319,1433,1434,2,3])).
% 72.83/72.80 cnf(1442,plain,
% 72.83/72.80 (E(f2(f2(x14421,x14421),f2(x14422,a1)),f2(x14423,x14423))),
% 72.83/72.80 inference(scs_inference,[],[1439,2])).
% 72.83/72.80 cnf(1443,plain,
% 72.83/72.80 (E(f2(f2(x14431,x14431),f2(x14432,x14431)),f2(f2(x14433,x14433),f2(x14434,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1439,1375,1438,2,3])).
% 72.83/72.80 cnf(1445,plain,
% 72.83/72.80 (~P1(f2(a1,a4),f2(x14451,x14451))+E(f2(f2(x14452,x14452),f2(x14453,a1)),f2(a1,a4))),
% 72.83/72.80 inference(scs_inference,[],[1442,1032,3])).
% 72.83/72.80 cnf(1446,plain,
% 72.83/72.80 (E(f2(f2(x14461,x14461),f2(x14462,a1)),f2(f2(x14463,x14463),f2(x14464,x14463)))),
% 72.83/72.80 inference(scs_inference,[],[1443,2])).
% 72.83/72.80 cnf(1447,plain,
% 72.83/72.80 (E(f2(f2(x14471,x14471),a4),f2(f2(x14472,x14472),f2(x14473,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1443,1060,1433,2,3])).
% 72.83/72.80 cnf(1450,plain,
% 72.83/72.80 (E(f2(f2(x14501,x14501),f2(x14502,a1)),f2(a1,a4))+~E(f2(f2(a1,a4),f2(x14503,x14503)),a4)),
% 72.83/72.80 inference(scs_inference,[],[1445,16])).
% 72.83/72.80 cnf(1451,plain,
% 72.83/72.80 (E(f2(f2(x14511,x14511),f2(x14512,a1)),f2(f2(x14513,x14513),a4))),
% 72.83/72.80 inference(scs_inference,[],[1447,2])).
% 72.83/72.80 cnf(1452,plain,
% 72.83/72.80 (E(f2(f2(x14521,x14521),f2(x14522,a1)),f2(f2(f2(a4,x14523),a4),f2(x14524,a4)))),
% 72.83/72.80 inference(scs_inference,[],[1446,1174,1447,2,3])).
% 72.83/72.80 cnf(1456,plain,
% 72.83/72.80 (E(f2(x14561,a1),f2(f2(x14562,x14562),f2(x14563,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1452,1096,1447,2,3])).
% 72.83/72.80 cnf(1496,plain,
% 72.83/72.80 (E(f2(a4,x14961),f2(f2(x14962,x14962),f2(x14963,a1)))),
% 72.83/72.80 inference(scs_inference,[],[390,1438,3])).
% 72.83/72.80 cnf(1499,plain,
% 72.83/72.80 (E(f2(f2(x14991,x14991),f2(x14992,a1)),f2(a4,x14993))),
% 72.83/72.80 inference(scs_inference,[],[390,1438,3,2])).
% 72.83/72.80 cnf(1501,plain,
% 72.83/72.80 (~P1(a3,f2(a3,a3))),
% 72.83/72.80 inference(scs_inference,[],[391,12,17])).
% 72.83/72.80 cnf(1507,plain,
% 72.83/72.80 (~E(a3,f2(a3,a3))),
% 72.83/72.80 inference(scs_inference,[],[1501,12,434,6,7])).
% 72.83/72.80 cnf(1526,plain,
% 72.83/72.80 (E(f2(f2(x15261,x15261),f2(x15262,a1)),f2(f2(x15263,x15263),f2(x15264,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1499,1496,3])).
% 72.83/72.80 cnf(1528,plain,
% 72.83/72.80 (E(f2(f2(x15281,x15281),f2(x15282,a1)),f2(f2(x15283,x15283),f2(a4,x15284)))),
% 72.83/72.80 inference(scs_inference,[],[1451,131,3])).
% 72.83/72.80 cnf(1530,plain,
% 72.83/72.80 (E(f2(f2(x15301,x15301),f2(a4,x15302)),f2(f2(x15303,x15303),f2(x15304,a1)))),
% 72.83/72.80 inference(scs_inference,[],[1451,131,3,2])).
% 72.83/72.80 cnf(1531,plain,
% 72.83/72.80 (E(f2(f2(f2(x15311,x15312),x15311),f2(x15313,a1)),f2(f2(x15314,x15314),f2(a4,x15315)))),
% 72.83/72.80 inference(scs_inference,[],[1076,131,3])).
% 72.83/72.80 cnf(1537,plain,
% 72.83/72.80 (E(f2(f2(x15371,x15371),f2(a4,x15372)),f2(x15373,a1))),
% 72.83/72.81 inference(scs_inference,[],[403,1531,3,2])).
% 72.83/72.81 cnf(1542,plain,
% 72.83/72.81 (E(f2(f2(f2(a4,x15421),a4),f2(x15422,a4)),f2(f2(x15423,x15423),f2(a4,x15424)))),
% 72.83/72.81 inference(scs_inference,[],[1203,131,3])).
% 72.83/72.81 cnf(1546,plain,
% 72.83/72.81 (P1(f2(f2(f2(x15461,x15462),x15463),f2(x15461,x15463)),a4)),
% 72.83/72.81 inference(scs_inference,[],[404,13,7])).
% 72.83/72.81 cnf(1551,plain,
% 72.83/72.81 (E(f2(f2(f2(x15511,x15512),x15513),f2(x15511,x15513)),a4)),
% 72.83/72.81 inference(scs_inference,[],[404,28,535,11,13,7,3,2,6,17])).
% 72.83/72.81 cnf(1554,plain,
% 72.83/72.81 (P1(f2(f2(x15541,x15542),x15543),f2(x15541,x15543))),
% 72.83/72.81 inference(scs_inference,[],[404,28,535,11,13,7,3,2,6,17,16])).
% 72.83/72.81 cnf(1556,plain,
% 72.83/72.81 (E(a4,f2(f2(f2(x15561,x15562),x15563),f2(x15561,x15563)))),
% 72.83/72.81 inference(scs_inference,[],[1551,2])).
% 72.83/72.81 cnf(1558,plain,
% 72.83/72.81 (E(f2(f2(f2(x15581,x15581),x15582),f2(x15583,x15581)),f2(f2(x15581,x15581),f2(x15583,x15581)))),
% 72.83/72.81 inference(scs_inference,[],[695,1551,257,1554,1546,2,6,17])).
% 72.83/72.81 cnf(1562,plain,
% 72.83/72.81 (E(f2(x15621,x15621),f2(f2(x15622,x15622),f2(a4,x15623)))),
% 72.83/72.81 inference(scs_inference,[],[695,1370,1542,1551,257,1554,1546,2,6,17,3])).
% 72.83/72.81 cnf(1568,plain,
% 72.83/72.81 (E(f2(f2(x15681,x15681),f2(x15682,x15681)),f2(f2(x15683,x15683),f2(a4,x15684)))),
% 72.83/72.81 inference(scs_inference,[],[1075,1418,1558,1531,1546,2,7,3])).
% 72.83/72.81 cnf(1573,plain,
% 72.83/72.81 (E(f2(f2(x15731,x15731),f2(a4,x15732)),f2(f2(x15733,x15733),f2(x15734,x15733)))),
% 72.83/72.81 inference(scs_inference,[],[1568,2])).
% 72.83/72.81 cnf(1574,plain,
% 72.83/72.81 (P1(f2(f2(f2(x15741,x15742),x15743),f2(x15741,x15743)),f2(f2(x15744,x15744),a4))),
% 72.83/72.81 inference(scs_inference,[],[1083,1568,1546,2,7])).
% 72.83/72.81 cnf(1580,plain,
% 72.83/72.81 (E(f2(f2(x15801,x15801),f2(a4,x15802)),f2(x15803,x15803))),
% 72.83/72.81 inference(scs_inference,[],[1562,2])).
% 72.83/72.81 cnf(1599,plain,
% 72.83/72.81 (P1(f2(f2(f2(x15991,x15991),x15992),f2(x15993,x15991)),a4)),
% 72.83/72.81 inference(scs_inference,[],[205,1554,7])).
% 72.83/72.81 cnf(1604,plain,
% 72.83/72.81 (E(f2(f2(f2(x16041,x16041),x16042),f2(x16043,x16041)),a4)),
% 72.83/72.81 inference(scs_inference,[],[28,205,1556,11,1554,7,3,2,6,17])).
% 72.83/72.81 cnf(1607,plain,
% 72.83/72.81 (P1(f2(f2(x16071,x16071),x16072),f2(x16073,x16071))),
% 72.83/72.81 inference(scs_inference,[],[28,205,1556,11,1554,7,3,2,6,17,16])).
% 72.83/72.81 cnf(1610,plain,
% 72.83/72.81 (E(a4,f2(f2(f2(x16101,x16101),x16102),f2(x16103,x16101)))),
% 72.83/72.81 inference(scs_inference,[],[1604,2])).
% 72.83/72.81 cnf(1612,plain,
% 72.83/72.81 (P1(f2(f2(x16121,x16121),x16122),f2(x16123,x16121))),
% 72.83/72.81 inference(rename_variables,[],[1607])).
% 72.83/72.81 cnf(1613,plain,
% 72.83/72.81 (P1(f2(f2(x16131,x16131),x16132),a4)),
% 72.83/72.81 inference(scs_inference,[],[827,163,1604,1607,1612,2,6,7])).
% 72.83/72.81 cnf(1615,plain,
% 72.83/72.81 (E(f2(f2(x16151,x16152),x16151),f2(f2(f2(x16153,x16154),x16155),f2(x16153,x16155)))),
% 72.83/72.81 inference(scs_inference,[],[827,163,1604,1556,1607,1612,2,6,7,3])).
% 72.83/72.81 cnf(1616,plain,
% 72.83/72.81 (E(f2(f2(x16161,x16161),x16162),a4)),
% 72.83/72.81 inference(scs_inference,[],[827,163,1604,1556,11,1607,1612,2,6,7,3,17])).
% 72.83/72.81 cnf(1619,plain,
% 72.83/72.81 (P1(f2(x16191,x16191),x16192)),
% 72.83/72.81 inference(scs_inference,[],[827,163,1604,1556,11,1607,1612,2,6,7,3,17,16])).
% 72.83/72.81 cnf(1624,plain,
% 72.83/72.81 (~P1(a1,f2(x16241,x16241))),
% 72.83/72.81 inference(scs_inference,[],[695,1615,1619,730,1599,2,6,17])).
% 72.83/72.81 cnf(1627,plain,
% 72.83/72.81 (P1(f2(f2(f2(x16271,x16271),x16272),f2(x16273,x16271)),f2(f2(x16274,x16274),f2(x16275,a1)))),
% 72.83/72.81 inference(scs_inference,[],[695,1418,1615,1619,730,1599,2,6,17,7])).
% 72.83/72.81 cnf(1628,plain,
% 72.83/72.81 (E(f2(f2(x16281,a1),x16282),f2(f2(f2(x16283,x16283),x16284),f2(x16285,x16283)))),
% 72.83/72.81 inference(scs_inference,[],[695,99,1418,1615,1610,1619,730,1599,2,6,17,7,3])).
% 72.83/72.81 cnf(1633,plain,
% 72.83/72.81 (E(f2(f2(a4,x16331),x16332),f2(f2(f2(x16333,x16333),x16334),f2(x16335,x16333)))),
% 72.83/72.81 inference(scs_inference,[],[1624,136,1083,1628,1610,12,1613,2,6,7,3])).
% 72.83/72.81 cnf(1634,plain,
% 72.83/72.81 (E(f2(a1,a4),f2(x16341,x16341))+~E(f2(f2(x16342,x16343),x16342),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[412,1034,6])).
% 72.83/72.81 cnf(1637,plain,
% 72.83/72.81 (E(f2(f2(x16371,x16372),f2(a1,x16372)),f2(f2(f2(x16373,x16374),x16375),f2(x16373,x16375)))),
% 72.83/72.81 inference(scs_inference,[],[320,211,1633,1556,1613,2,7,3])).
% 72.83/72.81 cnf(1640,plain,
% 72.83/72.81 (P1(f2(f2(f2(x16401,x16401),x16402),f2(x16403,x16401)),f2(f2(x16404,x16405),x16404))),
% 72.83/72.81 inference(scs_inference,[],[162,1637,1599,2,7])).
% 72.83/72.81 cnf(1641,plain,
% 72.83/72.81 (E(f2(f2(x16411,a1),x16412),f2(f2(f2(x16413,x16414),x16415),f2(x16413,x16415)))),
% 72.83/72.81 inference(scs_inference,[],[99,162,1637,1556,1599,2,7,3])).
% 72.83/72.81 cnf(1645,plain,
% 72.83/72.81 (E(f2(f2(a4,x16451),x16452),f2(f2(f2(x16453,x16454),x16455),f2(x16453,x16455)))),
% 72.83/72.81 inference(scs_inference,[],[136,359,1641,1556,1613,2,7,3])).
% 72.83/72.81 cnf(1648,plain,
% 72.83/72.81 (P1(f2(f2(f2(x16481,x16482),x16483),x16481),a4)),
% 72.83/72.81 inference(scs_inference,[],[163,1645,1554,2,7])).
% 72.83/72.81 cnf(1650,plain,
% 72.83/72.81 (E(f2(f2(x16501,x16502),x16501),f2(f2(f2(x16503,x16503),x16504),f2(x16505,x16503)))),
% 72.83/72.81 inference(scs_inference,[],[163,1645,1610,1554,2,7,3])).
% 72.83/72.81 cnf(1655,plain,
% 72.83/72.81 (P1(f2(f2(x16551,x16552),x16553),x16551)),
% 72.83/72.81 inference(scs_inference,[],[28,163,1645,1610,11,1554,2,7,3,6,17,16])).
% 72.83/72.81 cnf(1661,plain,
% 72.83/72.81 (P1(f2(f2(f2(x16611,x16612),x16613),f2(a1,x16612)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1624,320,1650,1655,1554,2,6,7])).
% 72.83/72.81 cnf(1663,plain,
% 72.83/72.81 (E(f2(f2(x16631,x16632),f2(a1,x16632)),f2(f2(f2(x16633,x16633),x16634),f2(x16635,x16633)))),
% 72.83/72.81 inference(scs_inference,[],[1624,320,1650,1610,1655,1554,2,6,7,3])).
% 72.83/72.81 cnf(1664,plain,
% 72.83/72.81 (E(f2(f2(f2(x16641,x16642),x16643),f2(a1,x16642)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1624,320,1650,1610,11,1655,1554,2,6,7,3,17])).
% 72.83/72.81 cnf(1667,plain,
% 72.83/72.81 (P1(f2(f2(x16671,x16672),x16673),f2(a1,x16672))),
% 72.83/72.81 inference(scs_inference,[],[1624,320,1650,1610,11,1655,1554,2,6,7,3,17,16])).
% 72.83/72.81 cnf(1671,plain,
% 72.83/72.81 (P1(f2(f2(f2(x16711,x16712),x16713),f2(a1,x16712)),f2(f2(x16714,x16714),f2(x16715,a1)))),
% 72.83/72.81 inference(scs_inference,[],[695,1418,1663,1648,1661,2,6,7])).
% 72.83/72.81 cnf(1673,plain,
% 72.83/72.81 (E(a4,f2(f2(x16731,x16731),x16732))),
% 72.83/72.81 inference(scs_inference,[],[1616,2])).
% 72.83/72.81 cnf(1678,plain,
% 72.83/72.81 (E(f2(f2(x16781,a1),x16782),f2(f2(x16783,x16783),x16784))),
% 72.83/72.81 inference(scs_inference,[],[1314,99,106,1616,1671,1661,2,6,7,3])).
% 72.83/72.81 cnf(1680,plain,
% 72.83/72.81 (E(f2(f2(x16801,x16801),x16802),f2(f2(x16803,a1),x16804))),
% 72.83/72.81 inference(scs_inference,[],[1678,2])).
% 72.83/72.81 cnf(1684,plain,
% 72.83/72.81 (E(f2(f2(a4,x16841),x16842),f2(f2(x16843,x16843),x16844))),
% 72.83/72.81 inference(scs_inference,[],[414,136,1678,1673,1640,2,7,3])).
% 72.83/72.81 cnf(1686,plain,
% 72.83/72.81 (E(f2(f2(x16861,x16861),x16862),f2(f2(a4,x16863),x16864))),
% 72.83/72.81 inference(scs_inference,[],[1684,2])).
% 72.83/72.81 cnf(1702,plain,
% 72.83/72.81 (E(a4,f2(f2(f2(x17021,x17022),x17023),f2(a1,x17022)))),
% 72.83/72.81 inference(scs_inference,[],[1664,2])).
% 72.83/72.81 cnf(1703,plain,
% 72.83/72.81 (P1(f2(f2(f2(x17031,x17032),x17033),f2(x17031,x17033)),f2(f2(x17034,x17035),x17034))),
% 72.83/72.81 inference(scs_inference,[],[162,1664,1546,2,7])).
% 72.83/72.81 cnf(1704,plain,
% 72.83/72.81 (E(f2(f2(x17041,a1),x17042),f2(f2(f2(x17043,x17044),x17045),f2(a1,x17044)))),
% 72.83/72.81 inference(scs_inference,[],[99,162,1664,1546,2,7,3])).
% 72.83/72.81 cnf(1705,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(a4,a4))+E(f2(f2(a1,a4),x17051),f2(f2(x17052,x17052),x17051))),
% 72.83/72.81 inference(scs_inference,[],[1034,1410])).
% 72.83/72.81 cnf(1710,plain,
% 72.83/72.81 (E(f2(f2(a4,x17101),x17102),f2(f2(f2(x17103,x17104),x17105),f2(a1,x17104)))),
% 72.83/72.81 inference(scs_inference,[],[426,136,1704,1702,1703,2,7,3])).
% 72.83/72.81 cnf(1711,plain,
% 72.83/72.81 (E(f2(f2(a1,a4),x17111),f2(f2(x17112,x17112),x17111))+~E(f2(f2(a1,a4),f2(a4,a4)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1705,16])).
% 72.83/72.81 cnf(1713,plain,
% 72.83/72.81 (E(f2(f2(x17131,x17132),x17131),f2(f2(x17133,x17133),x17134))),
% 72.83/72.81 inference(scs_inference,[],[163,1710,1673,2,3])).
% 72.83/72.81 cnf(1714,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(a4,a4)),a4)),
% 72.83/72.81 inference(scs_inference,[],[427,1430,1711,3])).
% 72.83/72.81 cnf(1717,plain,
% 72.83/72.81 (E(f2(f2(x17171,x17171),x17172),f2(f2(x17173,x17174),x17173))),
% 72.83/72.81 inference(scs_inference,[],[1713,1714,15,2])).
% 72.83/72.81 cnf(1718,plain,
% 72.83/72.81 (P1(f2(f2(f2(x17181,x17181),x17182),x17183),a4)),
% 72.83/72.81 inference(scs_inference,[],[427,1713,1714,1655,15,2,7])).
% 72.83/72.81 cnf(1720,plain,
% 72.83/72.81 (E(f2(x17201,x17201),f2(f2(f2(x17202,x17203),f2(a1,x17203)),x17204))),
% 72.83/72.81 inference(scs_inference,[],[427,519,1713,1714,1655,15,2,7,3])).
% 72.83/72.81 cnf(1725,plain,
% 72.83/72.81 (P1(f2(f2(x17251,x17251),x17252),x17253)),
% 72.83/72.81 inference(scs_inference,[],[427,28,519,1713,11,1714,1655,15,2,7,3,6,17,16])).
% 72.83/72.81 cnf(1729,plain,
% 72.83/72.81 (P1(f2(f2(f2(x17291,x17292),x17291),f2(x17293,a1)),f2(f2(x17294,x17295),x17294))),
% 72.83/72.81 inference(scs_inference,[],[438,1720,434,2,7])).
% 72.83/72.81 cnf(1745,plain,
% 72.83/72.81 (P1(f2(f2(f2(x17451,x17452),x17453),f2(x17451,x17453)),f2(f2(x17454,a1),x17455))),
% 72.83/72.81 inference(scs_inference,[],[106,1546,7])).
% 72.83/72.81 cnf(1747,plain,
% 72.83/72.81 (E(f2(a1,a4),f2(x17471,x17471))+~E(f2(f2(x17472,x17473),f2(a1,x17473)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[446,1034,6])).
% 72.83/72.81 cnf(1748,plain,
% 72.83/72.81 (E(f2(x17481,x17481),f2(a1,a4))+~E(f2(f2(x17482,x17483),f2(a1,x17483)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1747,2])).
% 72.83/72.81 cnf(1755,plain,
% 72.83/72.81 (E(f2(a1,a4),f2(x17551,x17551))+~E(f2(f2(a4,x17552),x17553),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[468,1034,6])).
% 72.83/72.81 cnf(1756,plain,
% 72.83/72.81 (E(f2(x17561,x17561),f2(a1,a4))+~E(f2(f2(a4,x17562),x17563),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1755,2])).
% 72.83/72.81 cnf(1762,plain,
% 72.83/72.81 (P1(f2(f2(f2(x17621,x17621),x17622),f2(x17623,x17621)),f2(x17624,a1))),
% 72.83/72.81 inference(scs_inference,[],[478,1627,7])).
% 72.83/72.81 cnf(1768,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x17681,a1),f2(x17681,a1)))+E(f2(a1,a4),f2(x17682,a1))),
% 72.83/72.81 inference(scs_inference,[],[478,1034,3])).
% 72.83/72.81 cnf(1769,plain,
% 72.83/72.81 (E(f2(a1,a4),f2(x17691,a1))+~E(f2(f2(a1,a4),f2(f2(x17692,a1),f2(x17692,a1))),a4)),
% 72.83/72.81 inference(scs_inference,[],[1768,16])).
% 72.83/72.81 cnf(1770,plain,
% 72.83/72.81 (E(f2(x17701,a1),f2(a1,a4))+~E(f2(f2(a1,a4),f2(f2(x17702,a1),f2(x17702,a1))),a4)),
% 72.83/72.81 inference(scs_inference,[],[1769,2])).
% 72.83/72.81 cnf(1771,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(f2(x17711,a1),f2(x17711,a1))),a4)),
% 72.83/72.81 inference(scs_inference,[],[12,1431,1770,6])).
% 72.83/72.81 cnf(1776,plain,
% 72.83/72.81 (E(f2(x17761,a1),f2(f2(x17762,a1),x17763))),
% 72.83/72.81 inference(rename_variables,[],[491])).
% 72.83/72.81 cnf(1777,plain,
% 72.83/72.81 (E(f2(x17771,a1),f2(f2(f2(x17772,x17772),x17773),f2(x17774,x17772)))),
% 72.83/72.81 inference(scs_inference,[],[491,1776,1633,1729,1771,15,7,3])).
% 72.83/72.81 cnf(1780,plain,
% 72.83/72.81 (E(f2(f2(f2(x17801,x17801),x17802),f2(x17803,x17801)),f2(x17804,a1))),
% 72.83/72.81 inference(scs_inference,[],[491,1776,1633,1729,1771,15,7,3,2])).
% 72.83/72.81 cnf(1784,plain,
% 72.83/72.81 (E(f2(x17841,a1),f2(f2(f2(x17842,x17843),x17844),f2(x17842,x17844)))),
% 72.83/72.81 inference(scs_inference,[],[491,1645,1762,7,3])).
% 72.83/72.81 cnf(1787,plain,
% 72.83/72.81 (E(f2(f2(f2(x17871,x17872),x17873),f2(x17871,x17873)),f2(x17874,a1))),
% 72.83/72.81 inference(scs_inference,[],[491,1645,1762,7,3,2])).
% 72.83/72.81 cnf(1789,plain,
% 72.83/72.81 (E(f2(x17891,a1),f2(f2(f2(x17892,x17893),x17894),f2(a1,x17893)))),
% 72.83/72.81 inference(scs_inference,[],[491,1710,3])).
% 72.83/72.81 cnf(1792,plain,
% 72.83/72.81 (E(f2(f2(f2(x17921,x17922),x17923),f2(a1,x17922)),f2(x17924,a1))),
% 72.83/72.81 inference(scs_inference,[],[491,1710,3,2])).
% 72.83/72.81 cnf(1802,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18021)),a4)),
% 72.83/72.81 inference(scs_inference,[],[518,11,17])).
% 72.83/72.81 cnf(1807,plain,
% 72.83/72.81 (~E(f2(a4,x18071),f2(a3,f2(a4,x18072)))),
% 72.83/72.81 inference(scs_inference,[],[1802,12,6])).
% 72.83/72.81 cnf(1811,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18111)),f2(a4,x18112))),
% 72.83/72.81 inference(scs_inference,[],[140,1807,17])).
% 72.83/72.81 cnf(1817,plain,
% 72.83/72.81 (~E(f2(f2(a4,x18171),x18172),f2(a3,f2(a4,x18173)))),
% 72.83/72.81 inference(scs_inference,[],[1811,12,6])).
% 72.83/72.81 cnf(1819,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18191)),f2(f2(a4,x18192),f2(a4,x18192)))),
% 72.83/72.81 inference(scs_inference,[],[1817,1619,17])).
% 72.83/72.81 cnf(1823,plain,
% 72.83/72.81 (~E(f2(x18231,a1),f2(a3,f2(a4,x18232)))),
% 72.83/72.81 inference(scs_inference,[],[1811,104,1817,1619,17,6])).
% 72.83/72.81 cnf(1827,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18271)),f2(a1,a1))),
% 72.83/72.81 inference(scs_inference,[],[1823,1619,17])).
% 72.83/72.81 cnf(1831,plain,
% 72.83/72.81 (~E(f2(f2(x18311,a1),x18312),f2(a3,f2(a4,x18313)))),
% 72.83/72.81 inference(scs_inference,[],[1819,377,1823,1619,17,6])).
% 72.83/72.81 cnf(1833,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18331)),f2(f2(x18332,a1),f2(x18332,a1)))),
% 72.83/72.81 inference(scs_inference,[],[1831,1619,17])).
% 72.83/72.81 cnf(1837,plain,
% 72.83/72.81 (~E(f2(f2(x18371,x18372),x18371),f2(a3,f2(a4,x18373)))),
% 72.83/72.81 inference(scs_inference,[],[1827,412,1831,1619,17,6])).
% 72.83/72.81 cnf(1841,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18411)),f2(f2(a3,a1),f2(a4,x18411)))),
% 72.83/72.81 inference(scs_inference,[],[1831,1554,17])).
% 72.83/72.81 cnf(1845,plain,
% 72.83/72.81 (~E(f2(f2(x18451,a4),f2(a1,a4)),f2(a3,f2(a4,x18452)))),
% 72.83/72.81 inference(scs_inference,[],[1833,714,1831,1554,17,6])).
% 72.83/72.81 cnf(1849,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18491)),f2(f2(a1,a4),f2(a1,a4)))),
% 72.83/72.81 inference(scs_inference,[],[1845,1619,17])).
% 72.83/72.81 cnf(1853,plain,
% 72.83/72.81 (~E(f2(f2(x18531,x18532),f2(a1,x18532)),f2(a3,f2(a4,x18533)))),
% 72.83/72.81 inference(scs_inference,[],[1841,446,1845,1619,17,6])).
% 72.83/72.81 cnf(1863,plain,
% 72.83/72.81 (~E(f2(f2(x18631,x18631),x18632),f2(a3,f2(a4,x18633)))),
% 72.83/72.81 inference(scs_inference,[],[1849,1725,1853,1619,17,6])).
% 72.83/72.81 cnf(1865,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x18651)),f2(f2(a3,a3),f2(a4,x18651)))),
% 72.83/72.81 inference(scs_inference,[],[1863,1554,17])).
% 72.83/72.81 cnf(1873,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(a3,a4)),f2(a3,f2(a4,x18731)))),
% 72.83/72.81 inference(scs_inference,[],[1865,841,6])).
% 72.83/72.81 cnf(1886,plain,
% 72.83/72.81 (P1(f2(f2(f2(x18861,x18862),x18863),a4),x18864)+~E(a1,x18862)),
% 72.83/72.81 inference(scs_inference,[],[12,1257,6])).
% 72.83/72.81 cnf(1887,plain,
% 72.83/72.81 (P1(f2(f2(f2(x18871,a1),x18872),a4),x18873)),
% 72.83/72.81 inference(equality_inference,[],[1886])).
% 72.83/72.81 cnf(1923,plain,
% 72.83/72.81 (~E(f2(a4,x19231),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,12,6])).
% 72.83/72.81 cnf(1926,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(a4,x19261))),
% 72.83/72.81 inference(scs_inference,[],[140,1923,17])).
% 72.83/72.81 cnf(1929,plain,
% 72.83/72.81 (~E(f2(x19291,a1),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,104,140,1923,17,6])).
% 72.83/72.81 cnf(1931,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(a1,a1))),
% 72.83/72.81 inference(scs_inference,[],[1929,1619,17])).
% 72.83/72.81 cnf(1935,plain,
% 72.83/72.81 (~E(f2(f2(a4,x19351),x19352),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,468,1929,1619,17,6])).
% 72.83/72.81 cnf(1941,plain,
% 72.83/72.81 (~E(f2(f2(x19411,a1),x19412),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,377,1935,1619,17,6])).
% 72.83/72.81 cnf(1944,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(a3,a1),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[1941,1554,17])).
% 72.83/72.81 cnf(1948,plain,
% 72.83/72.81 (~E(f2(f2(x19481,x19482),x19481),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,412,1941,1554,17,6])).
% 72.83/72.81 cnf(1950,plain,
% 72.83/72.81 (~E(f2(f2(x19501,x19502),f2(a1,x19502)),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,446,6])).
% 72.83/72.81 cnf(1959,plain,
% 72.83/72.81 (~E(f2(f2(a3,x19591),a4),a3)),
% 72.83/72.81 inference(scs_inference,[],[1944,1745,1950,1619,17,6,4])).
% 72.83/72.81 cnf(1967,plain,
% 72.83/72.81 (~E(f2(a4,x19671),f2(a1,a4))+E(f2(a1,a4),f2(x19672,x19672))),
% 72.83/72.81 inference(scs_inference,[],[1405,2])).
% 72.83/72.81 cnf(1970,plain,
% 72.83/72.81 (~E(f2(a4,x19701),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[119,691,1967,3])).
% 72.83/72.81 cnf(1971,plain,
% 72.83/72.81 (~E(f2(f2(a4,a4),x19711),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1970,1297])).
% 72.83/72.81 cnf(1972,plain,
% 72.83/72.81 (~E(f2(a4,x19721),f2(a1,a4))),
% 72.83/72.81 inference(rename_variables,[],[1970])).
% 72.83/72.81 cnf(1974,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(a4,a1))),
% 72.83/72.81 inference(scs_inference,[],[1970,1972,104,1297,17])).
% 72.83/72.81 cnf(1983,plain,
% 72.83/72.81 (~E(f2(a1,a4),f2(a4,x19831))),
% 72.83/72.81 inference(scs_inference,[],[1970,1405,2])).
% 72.83/72.81 cnf(1984,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(x19841,x19841))),
% 72.83/72.81 inference(scs_inference,[],[1971,1445])).
% 72.83/72.81 cnf(1985,plain,
% 72.83/72.81 (~E(f2(f2(a4,a4),x19851),f2(a1,a4))),
% 72.83/72.81 inference(rename_variables,[],[1971])).
% 72.83/72.81 cnf(1987,plain,
% 72.83/72.81 (~E(f2(f2(x19871,x19872),x19871),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1971,1983,1445,1634])).
% 72.83/72.81 cnf(1996,plain,
% 72.83/72.81 (~E(f2(f2(f2(x19961,x19961),f2(x19962,x19961)),x19963),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1974,1304,336,1971,1985,1983,1445,1634,1297,17,6])).
% 72.83/72.81 cnf(2000,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(a4,x20001))),
% 72.83/72.81 inference(scs_inference,[],[1970,140,17])).
% 72.83/72.81 cnf(2003,plain,
% 72.83/72.81 (~E(f2(f2(f2(x20031,x20032),x20031),x20033),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1984,1970,140,765,17,6])).
% 72.83/72.81 cnf(2006,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(x20061,x20062),x20061),f2(x20063,a1)))),
% 72.83/72.81 inference(scs_inference,[],[1984,1970,140,765,17,6,1310])).
% 72.83/72.81 cnf(2014,plain,
% 72.83/72.81 (~E(f2(f2(f2(x20141,x20142),f2(a1,x20142)),x20143),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2000,746,1987,1667,17,6])).
% 72.83/72.81 cnf(2018,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(a4,x20181),a4),x20182))),
% 72.83/72.81 inference(scs_inference,[],[2003,1667,17])).
% 72.83/72.81 cnf(2024,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(a1,a1),f2(x20241,a1)),a4))),
% 72.83/72.81 inference(scs_inference,[],[1996,1887,17])).
% 72.83/72.81 cnf(2042,plain,
% 72.83/72.81 (~E(f2(f2(x20421,a4),f2(a1,a4)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1984,714,2014,1887,17,6])).
% 72.83/72.81 cnf(2049,plain,
% 72.83/72.81 (~E(f2(f2(f2(x20491,a1),a4),f2(x20492,a4)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2006,1158,6])).
% 72.83/72.81 cnf(2052,plain,
% 72.83/72.81 (~E(f2(f2(f2(x20521,x20522),x20523),f2(x20521,x20523)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2024,1574,6])).
% 72.83/72.81 cnf(2059,plain,
% 72.83/72.81 (~E(f2(f2(f2(x20591,x20591),x20592),f2(x20593,x20591)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2018,2052,1640,1667,17,6])).
% 72.83/72.81 cnf(2062,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(x20621,x20621),a4),f2(x20622,x20621)))),
% 72.83/72.81 inference(scs_inference,[],[2059,1667,17])).
% 72.83/72.81 cnf(2069,plain,
% 72.83/72.81 (~E(f2(f2(f2(x20691,x20691),a4),f2(a4,a4)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2062,841,6])).
% 72.83/72.81 cnf(2074,plain,
% 72.83/72.81 (~E(f2(x20741,x20741),f2(a3,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[522,1619,6])).
% 72.83/72.81 cnf(2076,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(a3,a4),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2074,1554,17])).
% 72.83/72.81 cnf(2090,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),x20901),a1)),
% 72.83/72.81 inference(scs_inference,[],[532,12,6])).
% 72.83/72.81 cnf(2094,plain,
% 72.83/72.81 (~E(f2(f2(a3,x20941),a4),a1)),
% 72.83/72.81 inference(scs_inference,[],[532,1554,6])).
% 72.83/72.81 cnf(2113,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(a4,a4)),f2(f2(x21131,a1),x21132))),
% 72.83/72.81 inference(scs_inference,[],[1983,99,1041,3])).
% 72.83/72.81 cnf(2114,plain,
% 72.83/72.81 (~E(f2(a1,a4),f2(x21141,a1))),
% 72.83/72.81 inference(scs_inference,[],[2113,4])).
% 72.83/72.81 cnf(2117,plain,
% 72.83/72.81 (~E(f2(f2(a1,a1),x21171),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[535,2113,1718,4,7,1300])).
% 72.83/72.81 cnf(2120,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(a1,a1),a4))),
% 72.83/72.81 inference(scs_inference,[],[2117,1554,17])).
% 72.83/72.81 cnf(2130,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a1),a4),x21301),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2120,12,6])).
% 72.83/72.81 cnf(2133,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(a1,a1),a4),x21331))),
% 72.83/72.81 inference(scs_inference,[],[2130,1667,17])).
% 72.83/72.81 cnf(2136,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a1,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2114,11,1041,17])).
% 72.83/72.81 cnf(2137,plain,
% 72.83/72.81 (~E(f2(x21371,a1),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2133,104,6])).
% 72.83/72.81 cnf(2147,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,a4)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1983,11,1041,17])).
% 72.83/72.81 cnf(2150,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(a4,a4)),f2(f2(x21501,x21502),x21501))),
% 72.83/72.81 inference(scs_inference,[],[1970,163,1272,3])).
% 72.83/72.81 cnf(2153,plain,
% 72.83/72.81 (E(f2(f2(x21531,x21532),f2(a1,x21532)),f2(f2(x21533,x21533),x21534))),
% 72.83/72.81 inference(scs_inference,[],[320,1673,2150,4,3])).
% 72.83/72.81 cnf(2154,plain,
% 72.83/72.81 (E(f2(f2(x21541,x21541),x21542),f2(f2(x21543,x21544),f2(a1,x21544)))),
% 72.83/72.81 inference(scs_inference,[],[320,1673,2150,4,3,2])).
% 72.83/72.81 cnf(2157,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(x21571,x21571),a4),f2(a4,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2069,1667,17])).
% 72.83/72.81 cnf(2164,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(x21641,x21641)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1970,1297,1450])).
% 72.83/72.81 cnf(2165,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x21651,a4),f2(a1,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2042,1667,17])).
% 72.83/72.81 cnf(2173,plain,
% 72.83/72.81 (~E(f2(f2(x21731,x21732),f2(a1,x21732)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1970,1297,1748])).
% 72.83/72.81 cnf(2179,plain,
% 72.83/72.81 (~E(f2(f2(a4,x21791),x21792),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1970,1297,1756])).
% 72.83/72.81 cnf(2217,plain,
% 72.83/72.81 (~E(f2(f2(x22171,x22171),f2(x22172,x22171)),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2113,1288])).
% 72.83/72.81 cnf(2220,plain,
% 72.83/72.81 (E(f2(f2(x22201,x22202),f2(x22201,x22202)),f2(f2(x22201,x22201),x22202))),
% 72.83/72.81 inference(scs_inference,[],[2113,1725,1288,51])).
% 72.83/72.81 cnf(2221,plain,
% 72.83/72.81 (P1(f2(f2(x22211,x22211),x22212),x22213)),
% 72.83/72.81 inference(rename_variables,[],[1725])).
% 72.83/72.81 cnf(2223,plain,
% 72.83/72.81 (E(f2(x22231,f2(a4,x22232)),f2(x22231,f2(a4,x22233)))),
% 72.83/72.81 inference(scs_inference,[],[906,2113,1725,1288,51,5])).
% 72.83/72.81 cnf(2224,plain,
% 72.83/72.81 (E(f2(f2(x22241,x22241),x22242),f2(f2(x22243,x22243),x22242))),
% 72.83/72.81 inference(scs_inference,[],[906,2113,979,1725,1288,51,5,4])).
% 72.83/72.81 cnf(2225,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(a1,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1931,906,2113,979,1725,1288,51,5,4,16])).
% 72.83/72.81 cnf(2228,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(f2(a4,x22281),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[1931,2173,906,766,2113,979,1725,330,1288,51,5,4,16,2,17])).
% 72.83/72.81 cnf(2232,plain,
% 72.83/72.81 (P1(f2(f2(f2(x22321,x22321),x22322),f2(x22323,x22321)),x22324)),
% 72.83/72.81 inference(scs_inference,[],[1931,2173,1777,906,766,2113,979,1725,2221,330,1288,51,5,4,16,2,17,6])).
% 72.83/72.81 cnf(2235,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(x22351,x22351),f2(a4,x22352)))),
% 72.83/72.81 inference(scs_inference,[],[1931,1580,2173,1777,906,766,2113,979,1725,2221,330,1288,51,5,4,16,2,17,6,7])).
% 72.83/72.81 cnf(2237,plain,
% 72.83/72.81 (~E(f2(a3,f2(x22371,a1)),a1)),
% 72.83/72.81 inference(scs_inference,[],[590,1931,1580,2173,1777,906,766,2113,979,1725,2221,118,330,1288,51,5,4,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2240,plain,
% 72.83/72.81 (E(f2(x22401,f2(x22402,x22402)),f2(x22401,f2(a4,x22403)))),
% 72.83/72.81 inference(scs_inference,[],[917,5])).
% 72.83/72.81 cnf(2241,plain,
% 72.83/72.81 (E(f2(f2(x22411,x22411),x22412),f2(a4,x22412))),
% 72.83/72.81 inference(scs_inference,[],[917,427,5,4])).
% 72.83/72.81 cnf(2242,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(a4,x22421)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1926,917,427,5,4,16])).
% 72.83/72.81 cnf(2245,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(a4,a4),x22451))),
% 72.83/72.81 inference(scs_inference,[],[2217,2179,1926,917,1725,427,5,4,16,2,17])).
% 72.83/72.81 cnf(2249,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,x22491)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2217,2179,1926,2147,2223,917,1725,427,5,4,16,2,17,6])).
% 72.83/72.81 cnf(2251,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a1,a1)),f2(x22511,a1))),
% 72.83/72.81 inference(scs_inference,[],[8,2217,2179,1926,2136,2147,2223,917,1725,427,5,4,16,2,17,6,7])).
% 72.83/72.81 cnf(2252,plain,
% 72.83/72.81 (~E(a4,f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[8,2137,2217,2179,1926,2136,2147,2223,917,1725,427,5,4,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2255,plain,
% 72.83/72.81 (E(f2(x22551,f2(a4,x22552)),f2(x22551,f2(x22553,x22553)))),
% 72.83/72.81 inference(scs_inference,[],[920,5])).
% 72.83/72.81 cnf(2256,plain,
% 72.83/72.81 (E(f2(a4,x22561),f2(f2(x22562,x22562),x22561))),
% 72.83/72.81 inference(scs_inference,[],[920,535,5,4])).
% 72.83/72.81 cnf(2259,plain,
% 72.83/72.81 (~E(f2(a1,a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2252,2251,920,535,5,4,16,2])).
% 72.83/72.81 cnf(2264,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),a4),f2(x22641,a1))),
% 72.83/72.81 inference(scs_inference,[],[2252,2251,500,2232,920,118,535,5,4,16,2,17,6])).
% 72.83/72.81 cnf(2266,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x22661,x22661),f2(a4,x22662)))),
% 72.83/72.81 inference(scs_inference,[],[2252,2251,1537,2245,500,2232,920,118,535,5,4,16,2,17,6,7])).
% 72.83/72.81 cnf(2269,plain,
% 72.83/72.81 (~E(f2(f2(x22691,x22691),x22692),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[2252,2251,1537,2245,500,2232,920,1673,118,535,5,4,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2270,plain,
% 72.83/72.81 (E(f2(x22701,f2(x22702,x22702)),f2(x22701,f2(x22703,a1)))),
% 72.83/72.81 inference(scs_inference,[],[1048,5])).
% 72.83/72.81 cnf(2273,plain,
% 72.83/72.81 (~E(f2(a1,a4),f2(f2(x22731,x22731),x22732))),
% 72.83/72.81 inference(scs_inference,[],[2269,2264,1048,5,16,2])).
% 72.83/72.81 cnf(2274,plain,
% 72.83/72.81 (~P1(f2(a1,a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2259,2269,2264,1048,11,5,16,2,17])).
% 72.83/72.81 cnf(2277,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x22771,x22771)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2259,2269,2264,2249,2240,1048,11,5,16,2,17,6])).
% 72.83/72.81 cnf(2279,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,x22791)),f2(x22792,a1))),
% 72.83/72.81 inference(scs_inference,[],[8,2259,2269,2264,2249,2240,1048,11,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2280,plain,
% 72.83/72.81 (~E(a3,f2(f2(x22801,x22801),f2(a4,x22802)))),
% 72.83/72.81 inference(scs_inference,[],[8,1507,2259,2269,2264,2249,2240,1580,1048,11,5,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2282,plain,
% 72.83/72.81 (E(f2(x22821,f2(x22822,a1)),f2(x22821,f2(x22823,x22823)))),
% 72.83/72.81 inference(scs_inference,[],[1052,5])).
% 72.83/72.81 cnf(2283,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2274,1052,5,16])).
% 72.83/72.81 cnf(2285,plain,
% 72.83/72.81 (~E(f2(a3,f2(a3,a4)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2274,459,1052,5,16,2])).
% 72.83/72.81 cnf(2286,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(x22861,x22861),f2(x22861,x22861)),f2(x22862,x22861)))),
% 72.83/72.81 inference(scs_inference,[],[2274,459,2273,2232,1052,5,16,2,17])).
% 72.83/72.81 cnf(2290,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x22901,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2274,459,2273,2232,1052,119,5,16,2,17,6])).
% 72.83/72.81 cnf(2292,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(x22921,a1))),
% 72.83/72.81 inference(scs_inference,[],[8,2274,459,2273,2232,1052,119,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2293,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(x22931,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[8,2274,459,2273,2164,2270,2232,1052,119,5,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2295,plain,
% 72.83/72.81 (E(f2(x22951,f2(x22952,x22952)),f2(x22951,f2(x22953,x22953)))),
% 72.83/72.81 inference(scs_inference,[],[979,5])).
% 72.83/72.81 cnf(2298,plain,
% 72.83/72.81 (~E(a4,f2(f2(a1,a4),a4))),
% 72.83/72.81 inference(scs_inference,[],[2279,2283,979,5,16,2])).
% 72.83/72.81 cnf(2303,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x23031,a1)),f2(x23032,a1))),
% 72.83/72.81 inference(scs_inference,[],[2279,2280,2283,2282,2232,979,5,16,2,17,6])).
% 72.83/72.81 cnf(2306,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x23061,x23061)),f2(x23062,a1))),
% 72.83/72.81 inference(scs_inference,[],[8,2279,2277,2280,2283,2282,2232,979,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2310,plain,
% 72.83/72.81 (E(f2(x23101,f2(x23102,a1)),f2(x23101,f2(a4,x23103)))),
% 72.83/72.81 inference(scs_inference,[],[36,5])).
% 72.83/72.81 cnf(2311,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a4),f2(x23111,x23111)),f2(x23112,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2306,36,5,16])).
% 72.83/72.81 cnf(2313,plain,
% 72.83/72.81 (~E(a4,f2(f2(a1,a4),f2(x23131,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2306,2293,36,5,16,2])).
% 72.83/72.81 cnf(2314,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x23141,x23141),a4))),
% 72.83/72.81 inference(scs_inference,[],[2306,2293,2273,36,330,5,16,2,17])).
% 72.83/72.81 cnf(2318,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a4,x23181)),f2(x23182,a1))),
% 72.83/72.81 inference(scs_inference,[],[2292,2306,2293,2273,36,132,330,5,16,2,17,6])).
% 72.83/72.81 cnf(2320,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x23201,a1)),f2(x23202,a1))),
% 72.83/72.81 inference(scs_inference,[],[8,2292,2306,2293,2290,2273,36,132,330,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2324,plain,
% 72.83/72.81 (E(f2(x23241,f2(x23242,a1)),f2(x23241,f2(x23243,a1)))),
% 72.83/72.81 inference(scs_inference,[],[40,5])).
% 72.83/72.81 cnf(2327,plain,
% 72.83/72.81 (~E(f2(a3,f2(x23271,a1)),a3)),
% 72.83/72.81 inference(scs_inference,[],[2303,154,40,5,16,2])).
% 72.83/72.81 cnf(2328,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2303,2298,154,40,11,5,16,2,17])).
% 72.83/72.81 cnf(2331,plain,
% 72.83/72.81 (P1(f2(f2(f2(x23311,x23312),x23313),f2(x23311,x23313)),x23314)),
% 72.83/72.81 inference(scs_inference,[],[2303,2298,154,1784,40,1655,11,5,16,2,17,6])).
% 72.83/72.81 cnf(2334,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x23341,x23341),f2(x23342,x23342)))),
% 72.83/72.81 inference(scs_inference,[],[2303,2266,2298,154,2295,1784,40,1655,11,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2337,plain,
% 72.83/72.81 (~E(f2(a3,f2(a3,a4)),f2(x23371,a1))),
% 72.83/72.81 inference(scs_inference,[],[8,2303,2266,2298,2285,154,2295,1784,40,1655,11,5,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2338,plain,
% 72.83/72.81 (E(f2(x23381,f2(a4,x23382)),f2(x23381,f2(x23383,a1)))),
% 72.83/72.81 inference(scs_inference,[],[27,5])).
% 72.83/72.81 cnf(2348,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(x23481,x23481),f2(x23482,x23481)))),
% 72.83/72.81 inference(scs_inference,[],[2337,2318,2334,157,2076,974,27,1725,119,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2350,plain,
% 72.83/72.81 (~E(f2(f2(x23501,x23501),x23502),f2(f2(a1,a4),f2(x23503,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2337,2318,2334,2313,157,2076,974,27,1725,1673,119,5,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2351,plain,
% 72.83/72.81 (E(f2(x23511,f2(x23512,x23512)),f2(x23511,a4))),
% 72.83/72.81 inference(scs_inference,[],[427,5])).
% 72.83/72.81 cnf(2354,plain,
% 72.83/72.81 (~E(f2(a3,f2(x23541,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2320,650,427,5,16,2])).
% 72.83/72.81 cnf(2359,plain,
% 72.83/72.81 (P1(f2(f2(f2(x23591,x23592),x23593),f2(a1,x23592)),x23594)),
% 72.83/72.81 inference(scs_inference,[],[2320,717,650,2331,1789,1655,427,5,16,2,17,6])).
% 72.83/72.81 cnf(2362,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x23621,a1)),f2(f2(x23622,x23622),x23623))),
% 72.83/72.81 inference(scs_inference,[],[2320,717,650,1717,2331,1789,1655,427,5,16,2,17,6,7])).
% 72.83/72.81 cnf(2365,plain,
% 72.83/72.81 (~E(f2(a3,f2(x23651,x23651)),a1)),
% 72.83/72.81 inference(scs_inference,[],[2320,717,650,2237,1717,2331,2255,1789,1655,427,5,16,2,17,6,7,3])).
% 72.83/72.81 cnf(2368,plain,
% 72.83/72.81 (~E(a1,f2(a3,f2(x23681,x23681)))),
% 72.83/72.81 inference(scs_inference,[],[2365,2])).
% 72.83/72.81 cnf(2369,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(a4,x23691)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2365,2000,2,16])).
% 72.83/72.81 cnf(2371,plain,
% 72.83/72.81 (E(f2(x23711,a4),f2(x23711,f2(x23712,x23712)))),
% 72.83/72.81 inference(scs_inference,[],[2365,2000,535,2,16,5])).
% 72.83/72.81 cnf(2372,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(f2(a1,a1),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2365,2000,625,1554,535,2,16,5,17])).
% 72.83/72.81 cnf(2376,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x23761,x23761)),f2(f2(x23762,a4),f2(a1,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2351,2165,2365,2000,625,1554,535,2,16,5,17,6])).
% 72.83/72.81 cnf(2378,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(x23781,x23781),a4),f2(x23782,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2351,2165,2365,2157,2310,2000,625,1554,535,2,16,5,17,6,7])).
% 72.83/72.81 cnf(2380,plain,
% 72.83/72.81 (~E(a4,f2(f2(a1,a4),f2(a4,x23801)))),
% 72.83/72.81 inference(scs_inference,[],[2369,2])).
% 72.83/72.81 cnf(2387,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x23871,a1)),f2(f2(x23872,a4),f2(a1,a4)))),
% 72.83/72.81 inference(scs_inference,[],[103,2369,2359,2324,2376,1827,2,16,17,6])).
% 72.83/72.81 cnf(2390,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),a4),f2(a4,x23901))),
% 72.83/72.81 inference(scs_inference,[],[9,103,2328,2369,2359,2324,2376,1827,2,16,17,6,7])).
% 72.83/72.81 cnf(2394,plain,
% 72.83/72.81 (~E(f2(f2(x23941,x23941),x23942),f2(f2(a1,a4),f2(a4,x23943)))),
% 72.83/72.81 inference(scs_inference,[],[2390,2380,739,1673,2,16,3])).
% 72.83/72.81 cnf(2395,plain,
% 72.83/72.81 (~P1(f2(a3,f2(x23951,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2390,2380,739,2354,1673,11,2,16,3,17])).
% 72.83/72.81 cnf(2398,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x23981,x23981)),f2(a4,x23982))),
% 72.83/72.81 inference(scs_inference,[],[2390,2380,739,2354,2351,1673,11,2,16,3,17,6])).
% 72.83/72.81 cnf(2400,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),a4),f2(f2(x24001,x24001),x24002))),
% 72.83/72.81 inference(scs_inference,[],[2241,2390,2380,739,2354,2351,1673,11,2,16,3,17,6,7])).
% 72.83/72.81 cnf(2402,plain,
% 72.83/72.81 (~E(a3,f2(f2(a3,x24021),a4))),
% 72.83/72.81 inference(scs_inference,[],[1959,2])).
% 72.83/72.81 cnf(2403,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a4),f2(x24031,x24031)),f2(a4,x24032)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2398,1959,2,16])).
% 72.83/72.81 cnf(2405,plain,
% 72.83/72.81 (~E(f2(f2(a3,x24051),f2(x24052,x24052)),a3)),
% 72.83/72.81 inference(scs_inference,[],[2398,2371,1959,2,16,3])).
% 72.83/72.81 cnf(2411,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,x24111)),f2(a4,x24112))),
% 72.83/72.81 inference(scs_inference,[],[2398,2371,721,1959,2338,2331,2,16,3,17,6])).
% 72.83/72.81 cnf(2414,plain,
% 72.83/72.81 (~P1(f2(a3,f2(x24141,a1)),f2(a4,x24142))),
% 72.83/72.81 inference(scs_inference,[],[9,2398,2371,721,1959,2395,2338,2331,2,16,3,17,6,7])).
% 72.83/72.81 cnf(2417,plain,
% 72.83/72.81 (~E(a3,f2(f2(a3,x24171),f2(x24172,x24172)))),
% 72.83/72.81 inference(scs_inference,[],[2405,2])).
% 72.83/72.81 cnf(2420,plain,
% 72.83/72.81 (~P1(f2(f2(a3,f2(a3,a4)),f2(a1,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2411,2405,2225,11,2,16,17])).
% 72.83/72.81 cnf(2423,plain,
% 72.83/72.81 (~P1(f2(a3,a4),f2(a4,x24231))),
% 72.83/72.81 inference(scs_inference,[],[2411,2414,2405,2225,2371,11,2,16,17,6])).
% 72.83/72.81 cnf(2426,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(a4,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2411,2414,2256,2405,2372,2225,2371,11,2,16,17,6,7])).
% 72.83/72.81 cnf(2431,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(a4,x24311)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2423,2094,2,16])).
% 72.83/72.81 cnf(2433,plain,
% 72.83/72.81 (~P1(a3,f2(f2(a3,x24331),f2(x24332,x24332)))),
% 72.83/72.81 inference(scs_inference,[],[2423,2417,2094,1655,2,16,17])).
% 72.83/72.81 cnf(2440,plain,
% 72.83/72.81 (~P1(f2(f2(a3,f2(a3,a4)),f2(a1,a1)),f2(a4,x24401))),
% 72.83/72.81 inference(scs_inference,[],[9,2423,2417,2094,2362,2420,2295,1655,2,16,17,6,7])).
% 72.83/72.81 cnf(2441,plain,
% 72.83/72.81 (~E(a1,f2(f2(x24411,x24411),f2(x24412,x24413)))),
% 72.83/72.81 inference(scs_inference,[],[9,2423,208,2417,2094,2224,2362,2420,2295,1655,2,16,17,6,7,3])).
% 72.83/72.81 cnf(2444,plain,
% 72.83/72.81 (~P1(a1,f2(f2(x24441,x24442),f2(x24443,x24442)))+~E(a1,x24443)),
% 72.83/72.81 inference(scs_inference,[],[543,940,7])).
% 72.83/72.81 cnf(2445,plain,
% 72.83/72.81 (~P1(a1,f2(f2(x24451,x24452),f2(a1,x24452)))),
% 72.83/72.81 inference(equality_inference,[],[2444])).
% 72.83/72.81 cnf(2446,plain,
% 72.83/72.81 (~E(a4,f2(f2(a3,a4),f2(a4,x24461)))),
% 72.83/72.81 inference(scs_inference,[],[2431,2])).
% 72.83/72.81 cnf(2453,plain,
% 72.83/72.81 (~P1(f2(f2(a3,f2(a3,a4)),f2(a4,x24531)),f2(a4,x24532))),
% 72.83/72.81 inference(scs_inference,[],[2441,2431,2440,2414,2255,2359,2,16,17,6])).
% 72.83/72.81 cnf(2455,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x24551,x24552),f2(a1,x24552)))),
% 72.83/72.81 inference(scs_inference,[],[2314,2441,2431,2440,2153,2414,2255,2359,2,16,17,6,7])).
% 72.83/72.81 cnf(2461,plain,
% 72.83/72.81 (~E(f2(a3,f2(a3,a3)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2049,1501,2,16])).
% 72.83/72.81 cnf(2463,plain,
% 72.83/72.81 (~E(f2(f2(x24631,x24631),x24632),f2(f2(a3,a4),f2(a4,x24633)))),
% 72.83/72.81 inference(scs_inference,[],[2446,2049,1501,1673,2,16,3])).
% 72.83/72.81 cnf(2468,plain,
% 72.83/72.81 (~P1(f2(f2(a3,f2(a3,a4)),f2(x24681,x24681)),f2(a4,x24682))),
% 72.83/72.81 inference(scs_inference,[],[703,2446,2049,2453,2240,1501,1725,1673,2,16,3,17,6])).
% 72.83/72.81 cnf(2474,plain,
% 72.83/72.81 (~E(a4,f2(a3,f2(a3,a3)))),
% 72.83/72.81 inference(scs_inference,[],[2461,2])).
% 72.83/72.81 cnf(2480,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a3)),a4)),
% 72.83/72.81 inference(scs_inference,[],[139,2461,1792,1811,11,2,16,3,17])).
% 72.83/72.81 cnf(2485,plain,
% 72.83/72.81 (~P1(a3,f2(f2(x24851,x24851),f2(a4,x24852)))),
% 72.83/72.81 inference(scs_inference,[],[2455,2433,139,2461,1792,1573,2351,1811,11,2,16,3,17,6,7])).
% 72.83/72.81 cnf(2489,plain,
% 72.83/72.81 (~E(f2(a1,f2(x24891,x24891)),a4)),
% 72.83/72.81 inference(scs_inference,[],[1948,1624,2,16])).
% 72.83/72.81 cnf(2491,plain,
% 72.83/72.81 (~E(f2(f2(x24911,a1),x24912),f2(a1,a4))),
% 72.83/72.81 inference(scs_inference,[],[1948,2137,745,1624,2,16,3])).
% 72.83/72.81 cnf(2494,plain,
% 72.83/72.81 (~P1(a1,f2(a3,f2(x24941,x24941)))),
% 72.83/72.81 inference(scs_inference,[],[2368,1948,2137,745,1624,10,2,16,3,17])).
% 72.83/72.81 cnf(2497,plain,
% 72.83/72.81 (~P1(f2(f2(a3,f2(a3,a4)),f2(x24971,a1)),f2(a4,x24972))),
% 72.83/72.81 inference(scs_inference,[],[2368,2468,1948,2137,2310,745,1624,10,2,16,3,17,6])).
% 72.83/72.81 cnf(2500,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a3)),f2(a4,x25001))),
% 72.83/72.81 inference(scs_inference,[],[9,2368,2480,2468,1948,2137,2310,745,1624,10,2,16,3,17,6,7])).
% 72.83/72.81 cnf(2504,plain,
% 72.83/72.81 (~E(a3,f2(f2(x25041,x25041),x25042))),
% 72.83/72.81 inference(scs_inference,[],[2491,2500,498,2154,2,16,3])).
% 72.83/72.81 cnf(2510,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x25101,x25101)),f2(f2(x25102,x25102),x25103))),
% 72.83/72.81 inference(scs_inference,[],[2491,2500,498,124,2154,2400,2351,10,2,16,3,17,6])).
% 72.83/72.81 cnf(2512,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a3)),f2(f2(x25121,x25122),x25121))),
% 72.83/72.81 inference(scs_inference,[],[2491,2500,498,124,2154,2400,1095,2351,10,2,16,3,17,6,7])).
% 72.83/72.81 cnf(2518,plain,
% 72.83/72.81 (~E(a4,f2(a1,f2(x25181,x25181)))),
% 72.83/72.81 inference(scs_inference,[],[2489,2])).
% 72.83/72.81 cnf(2521,plain,
% 72.83/72.81 (~P1(a1,f2(f2(x25211,x25211),x25212))),
% 72.83/72.81 inference(scs_inference,[],[2445,2489,1680,144,2,16,7])).
% 72.83/72.81 cnf(2530,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(x25301,a1)),f2(f2(x25302,x25302),x25303))),
% 72.83/72.81 inference(scs_inference,[],[2350,2])).
% 72.83/72.81 cnf(2531,plain,
% 72.83/72.81 (~E(f2(a1,f2(a4,x25311)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2350,705,2,16])).
% 72.83/72.81 cnf(2533,plain,
% 72.83/72.81 (~P1(a3,f2(f2(x25331,x25331),x25332))),
% 72.83/72.81 inference(scs_inference,[],[2485,2350,1686,705,2,16,7])).
% 72.83/72.81 cnf(2543,plain,
% 72.83/72.81 (~E(a4,f2(a1,f2(a4,x25431)))),
% 72.83/72.81 inference(scs_inference,[],[2531,2])).
% 72.83/72.81 cnf(2544,plain,
% 72.83/72.81 (~E(f2(a3,a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2531,28,2,16])).
% 72.83/72.81 cnf(2546,plain,
% 72.83/72.81 (~P1(a1,f2(x25461,a1))),
% 72.83/72.81 inference(scs_inference,[],[2521,2531,1293,28,2,16,7])).
% 72.83/72.81 cnf(2549,plain,
% 72.83/72.81 (~E(f2(f2(x25491,x25492),x25491),f2(a3,f2(a3,a3)))),
% 72.83/72.81 inference(scs_inference,[],[2521,2474,2531,1293,162,28,2,16,7,3])).
% 72.83/72.81 cnf(2550,plain,
% 72.83/72.81 (~P1(a1,f2(f2(a3,a4),x25501))),
% 72.83/72.81 inference(scs_inference,[],[10,2521,2090,2474,2531,1293,162,28,2,16,7,3,17])).
% 72.83/72.81 cnf(2553,plain,
% 72.83/72.81 (~P1(f2(a3,f2(x25531,a1)),f2(f2(x25532,x25533),x25532))),
% 72.83/72.81 inference(scs_inference,[],[10,2521,2090,2474,2531,2512,1293,2282,162,28,2,16,7,3,17,6])).
% 72.83/72.81 cnf(2556,plain,
% 72.83/72.81 (~E(f2(a3,f2(a3,a3)),f2(f2(x25561,x25562),x25561))),
% 72.83/72.81 inference(scs_inference,[],[2549,2])).
% 72.83/72.81 cnf(2557,plain,
% 72.83/72.81 (~E(f2(a1,f2(x25571,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2546,2549,2,16])).
% 72.83/72.81 cnf(2562,plain,
% 72.83/72.81 (~E(f2(a3,f2(x25621,x25621)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2544,2546,2286,2549,1526,2371,2,16,7,3])).
% 72.83/72.81 cnf(2564,plain,
% 72.83/72.81 (~P1(f2(a3,a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2544,2546,2286,2549,1526,2371,11,2,16,7,3,17])).
% 72.83/72.81 cnf(2568,plain,
% 72.83/72.81 (~E(a4,f2(a3,f2(x25681,x25681)))),
% 72.83/72.81 inference(scs_inference,[],[2562,2])).
% 72.83/72.81 cnf(2569,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2564,2562,2,16])).
% 72.83/72.81 cnf(2574,plain,
% 72.83/72.81 (~E(f2(f2(x25741,x25742),f2(a1,x25742)),f2(a1,f2(x25743,x25743)))),
% 72.83/72.81 inference(scs_inference,[],[2564,2533,2518,2562,1780,359,2,16,7,3])).
% 72.83/72.81 cnf(2582,plain,
% 72.83/72.81 (~E(a4,f2(f2(a3,a4),a4))),
% 72.83/72.81 inference(scs_inference,[],[2569,2])).
% 72.83/72.81 cnf(2583,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(x25831,x25831),f2(x25832,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2569,2348,1528,2,7])).
% 72.83/72.81 cnf(2586,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),a4)),
% 72.83/72.81 inference(scs_inference,[],[2569,2348,1528,11,2,7,17])).
% 72.83/72.81 cnf(2589,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x25891,x25891)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2569,2348,1528,2371,11,2,7,17,3])).
% 72.83/72.81 cnf(2591,plain,
% 72.83/72.81 (~P1(f2(a3,f2(x25911,x25911)),f2(f2(x25912,x25913),x25912))),
% 72.83/72.81 inference(scs_inference,[],[2569,2348,1528,2553,2270,2371,11,2,7,17,3,6])).
% 72.83/72.81 cnf(2595,plain,
% 72.83/72.81 (~E(a4,f2(f2(a3,a4),f2(x25951,x25951)))),
% 72.83/72.81 inference(scs_inference,[],[2589,2])).
% 72.83/72.81 cnf(2602,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x26021,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2589,2550,1792,2324,11,2,7,17,3])).
% 72.83/72.81 cnf(2608,plain,
% 72.83/72.81 (~E(a4,f2(f2(a3,a4),f2(x26081,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2602,2])).
% 72.83/72.81 cnf(2615,plain,
% 72.83/72.81 (~E(f2(a3,f2(x26151,x26151)),f2(f2(x26152,x26153),x26152))),
% 72.83/72.81 inference(scs_inference,[],[2602,2494,2556,2338,2295,11,2,7,17,3])).
% 72.83/72.81 cnf(2622,plain,
% 72.83/72.81 (~E(a4,f2(a1,f2(x26221,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2557,2])).
% 72.83/72.81 cnf(2623,plain,
% 72.83/72.81 (~P1(a1,f2(f2(x26231,a1),x26232))),
% 72.83/72.81 inference(scs_inference,[],[647,2557,1678,2,7])).
% 72.83/72.81 cnf(2626,plain,
% 72.83/72.81 (~P1(a3,f2(a3,f2(x26261,a1)))),
% 72.83/72.81 inference(scs_inference,[],[647,2327,2557,1678,12,2,7,17])).
% 72.83/72.81 cnf(2629,plain,
% 72.83/72.81 (~E(f2(f2(x26291,a1),x26292),f2(f2(a3,a4),f2(x26293,x26293)))),
% 72.83/72.81 inference(scs_inference,[],[2595,647,2327,2557,1678,106,12,2,7,17,3])).
% 72.83/72.81 cnf(2634,plain,
% 72.83/72.81 (~E(f2(f2(x26341,x26341),f2(x26342,a1)),f2(f2(a3,a4),f2(x26343,x26343)))),
% 72.83/72.81 inference(scs_inference,[],[2626,2394,2629,1530,2240,2,7,3])).
% 72.83/72.81 cnf(2638,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x26381,x26381)),f2(f2(x26382,x26382),f2(x26383,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2634,2])).
% 72.83/72.81 cnf(2639,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(f2(x26391,x26391),x26392))),
% 72.83/72.81 inference(scs_inference,[],[2586,2634,1616,2,7])).
% 72.83/72.81 cnf(2640,plain,
% 72.83/72.81 (~E(f2(f2(a4,x26401),x26402),f2(f2(a3,a4),f2(x26403,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2586,2608,2634,1616,149,2,7,3])).
% 72.83/72.81 cnf(2641,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,x26411)),f2(f2(x26412,x26412),x26413))),
% 72.83/72.81 inference(scs_inference,[],[2586,2608,2510,2634,1616,2255,149,2,7,3,6])).
% 72.83/72.81 cnf(2644,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(a4,x26441)),f2(f2(x26442,x26442),x26443))),
% 72.83/72.81 inference(scs_inference,[],[2463,2])).
% 72.83/72.81 cnf(2645,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x26451,x26451)),f2(f2(x26452,x26452),x26453))),
% 72.83/72.81 inference(scs_inference,[],[2639,2463,2351,2,6])).
% 72.83/72.81 cnf(2647,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(f2(a4,x26471),x26472))),
% 72.83/72.81 inference(scs_inference,[],[2639,2463,1290,2351,2,6,7])).
% 72.83/72.81 cnf(2650,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x26501,a1)),f2(f2(x26502,x26502),f2(x26503,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2639,2638,2463,1290,2270,2351,2,6,7,3])).
% 72.83/72.81 cnf(2658,plain,
% 72.83/72.81 (~E(f2(f2(x26581,x26581),f2(x26582,a1)),f2(f2(a3,a4),f2(x26583,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2650,2])).
% 72.83/72.81 cnf(2659,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x26591,a1)),f2(f2(x26592,x26592),x26593))),
% 72.83/72.81 inference(scs_inference,[],[2645,2650,2282,2,6])).
% 72.83/72.81 cnf(2665,plain,
% 72.83/72.81 (~E(f2(f2(x26651,x26651),x26652),f2(a3,f2(x26653,x26653)))),
% 72.83/72.81 inference(scs_inference,[],[2623,2568,2645,2650,1780,2282,1673,2,6,7,3])).
% 72.83/72.81 cnf(2667,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x26671,a1)),f2(f2(a4,x26672),x26673))),
% 72.83/72.81 inference(scs_inference,[],[2640,2])).
% 72.83/72.81 cnf(2668,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x26681,x26681)),f2(f2(a4,x26682),x26683))),
% 72.83/72.81 inference(scs_inference,[],[2647,2640,2351,2,6])).
% 72.83/72.81 cnf(2670,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(f2(x26701,x26701),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2426,2647,2640,2241,2351,2,6,7])).
% 72.83/72.81 cnf(2671,plain,
% 72.83/72.81 (E(f2(f2(x26711,x26711),x26712),f2(a4,x26712))),
% 72.83/72.81 inference(rename_variables,[],[2241])).
% 72.83/72.81 cnf(2672,plain,
% 72.83/72.81 (~E(f2(a4,f2(x26721,a1)),f2(f2(a3,a4),f2(x26722,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2426,2647,2658,2640,2241,2671,2351,2,6,7,3])).
% 72.83/72.81 cnf(2677,plain,
% 72.83/72.81 (~E(a4,f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[11,2670,2615,2,6])).
% 72.83/72.81 cnf(2679,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(x26791,x26791))),
% 72.83/72.81 inference(scs_inference,[],[11,2670,2235,2615,1562,2,6,7])).
% 72.83/72.81 cnf(2681,plain,
% 72.83/72.81 (~E(f2(a4,x26811),f2(f2(a3,a4),f2(x26812,a1)))),
% 72.83/72.81 inference(scs_inference,[],[11,2670,2235,2615,2672,1562,906,2,6,7,3])).
% 72.83/72.81 cnf(2683,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(x26831,x26831)),a4)),
% 72.83/72.81 inference(scs_inference,[],[11,2670,2235,2615,2672,1562,906,2,6,7,3,16])).
% 72.83/72.81 cnf(2686,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x26861,a1)),f2(a4,x26862))),
% 72.83/72.81 inference(scs_inference,[],[2681,2])).
% 72.83/72.81 cnf(2687,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(x26871,x26871),x26872))),
% 72.83/72.81 inference(scs_inference,[],[2681,2378,1717,2,7])).
% 72.83/72.81 cnf(2690,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(a4,x26901)),f2(f2(a4,x26902),x26903))),
% 72.83/72.81 inference(scs_inference,[],[2681,2378,2667,1717,2223,2,7,3])).
% 72.83/72.81 cnf(2693,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x26931,a1)),f2(a4,a4))),
% 72.83/72.81 inference(scs_inference,[],[2681,2378,2667,1717,2223,1619,2,7,3,17])).
% 72.83/72.81 cnf(2701,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(a4,x27011)),f2(a4,a4))),
% 72.83/72.81 inference(scs_inference,[],[2693,2690,2338,2,6])).
% 72.83/72.81 cnf(2703,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x27031,a1)),f2(a4,x27032))),
% 72.83/72.81 inference(scs_inference,[],[2693,2686,2690,2338,140,2,6,17])).
% 72.83/72.81 cnf(2706,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(x27061,x27061),f2(x27062,x27062)))),
% 72.83/72.81 inference(scs_inference,[],[2679,2693,2686,2690,2224,2338,140,2,6,17,7])).
% 72.83/72.81 cnf(2709,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(a4,x27091)),f2(a4,x27092))),
% 72.83/72.81 inference(scs_inference,[],[2679,2693,2686,2690,2224,2310,2338,140,2,6,17,7,3])).
% 72.83/72.81 cnf(2713,plain,
% 72.83/72.81 (~E(f2(a4,x27131),f2(f2(a3,a4),f2(a4,x27132)))),
% 72.83/72.81 inference(scs_inference,[],[2709,2])).
% 72.83/72.81 cnf(2718,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),a4)),
% 72.83/72.81 inference(scs_inference,[],[11,2703,2709,2687,2677,132,2,16,6,17])).
% 72.83/72.81 cnf(2721,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(a4,x27211)),f2(f2(x27212,x27213),f2(a1,x27213)))),
% 72.83/72.81 inference(scs_inference,[],[11,2701,2703,2709,2687,2677,955,132,2,16,6,17,7])).
% 72.83/72.81 cnf(2723,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x27231,a1)),f2(f2(x27232,x27232),x27233))),
% 72.83/72.81 inference(scs_inference,[],[11,2701,2703,2709,2687,2677,2644,955,2324,132,2,16,6,17,7,3])).
% 72.83/72.81 cnf(2727,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(f2(x27271,x27272),x27271))),
% 72.83/72.81 inference(scs_inference,[],[2706,2723,1713,2,7])).
% 72.83/72.81 cnf(2729,plain,
% 72.83/72.81 (~E(f2(f2(x27291,x27292),f2(a1,x27292)),f2(f2(a3,a4),f2(a4,x27293)))),
% 72.83/72.81 inference(scs_inference,[],[2713,2706,2723,1713,951,2,7,3])).
% 72.83/72.81 cnf(2732,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(a4,x27321)),f2(f2(x27322,x27323),f2(a1,x27323)))),
% 72.83/72.81 inference(scs_inference,[],[2729,2])).
% 72.83/72.81 cnf(2733,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(a4,x27331)),f2(a4,x27332))),
% 72.83/72.81 inference(scs_inference,[],[2721,2729,1385,2,7])).
% 72.83/72.81 cnf(2736,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(x27361,x27361)),f2(f2(x27362,x27362),x27363))),
% 72.83/72.81 inference(scs_inference,[],[2530,2721,2729,1385,2295,2,7,3])).
% 72.83/72.81 cnf(2741,plain,
% 72.83/72.81 (~E(f2(f2(x27411,x27411),x27412),f2(f2(a1,a4),f2(x27413,x27413)))),
% 72.83/72.81 inference(scs_inference,[],[2736,2])).
% 72.83/72.81 cnf(2742,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x27421,x27421)),f2(a4,x27422))),
% 72.83/72.81 inference(scs_inference,[],[2733,2736,2240,2,6])).
% 72.83/72.81 cnf(2747,plain,
% 72.83/72.81 (~E(f2(a4,x27471),f2(f2(a3,a4),a4))),
% 72.83/72.81 inference(scs_inference,[],[2733,2582,2736,1537,2240,26,2,6,7,3])).
% 72.83/72.81 cnf(2752,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),a4),f2(a4,x27521))),
% 72.83/72.81 inference(scs_inference,[],[2747,2])).
% 72.83/72.81 cnf(2753,plain,
% 72.83/72.81 (~E(f2(f2(f2(a3,a4),f2(x27531,x27531)),f2(a4,x27532)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2742,2747,2,16])).
% 72.83/72.81 cnf(2758,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(f2(x27581,x27582),x27583),f2(x27581,x27583)))),
% 72.83/72.81 inference(scs_inference,[],[2742,2747,2659,2292,1787,2255,2,16,6,7])).
% 72.83/72.81 cnf(2763,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(a4,a4))),
% 72.83/72.81 inference(scs_inference,[],[2742,2747,2504,2659,2292,1787,2255,1619,2,16,6,7,3,17])).
% 72.83/72.81 cnf(2768,plain,
% 72.83/72.81 (~E(f2(f2(f2(a3,a4),a4),f2(a4,a4)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2763,16])).
% 72.83/72.81 cnf(2770,plain,
% 72.83/72.81 (~E(f2(a3,f2(x27701,x27701)),f2(f2(x27702,x27702),x27703))),
% 72.83/72.81 inference(scs_inference,[],[2763,2665,16,2])).
% 72.83/72.81 cnf(2771,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(a4,a1))),
% 72.83/72.81 inference(scs_inference,[],[2763,2752,2665,104,16,2,17])).
% 72.83/72.81 cnf(2773,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),a4),f2(a4,x27731))),
% 72.83/72.81 inference(rename_variables,[],[2752])).
% 72.83/72.81 cnf(2775,plain,
% 72.83/72.81 (~P1(f2(a1,a4),f2(f2(a4,x27751),x27752))),
% 72.83/72.81 inference(scs_inference,[],[2763,2752,2758,2665,1684,104,16,2,17,7])).
% 72.83/72.81 cnf(2778,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x27781,x27781)),f2(a4,x27782))),
% 72.83/72.81 inference(scs_inference,[],[2763,2752,2773,2758,2665,1684,2371,104,16,2,17,7,3])).
% 72.83/72.81 cnf(2780,plain,
% 72.83/72.81 (~P1(f2(a3,f2(x27801,x27801)),f2(a4,x27802))),
% 72.83/72.81 inference(scs_inference,[],[2763,2752,2773,2758,2665,2423,1684,2371,2351,104,16,2,17,7,3,6])).
% 72.83/72.81 cnf(2784,plain,
% 72.83/72.81 (~E(f2(a4,x27841),f2(f2(a3,a4),f2(x27842,x27842)))),
% 72.83/72.81 inference(scs_inference,[],[2771,2778,16,2])).
% 72.83/72.81 cnf(2785,plain,
% 72.83/72.81 (~P1(a3,f2(f2(a3,x27851),a4))),
% 72.83/72.81 inference(scs_inference,[],[2771,2778,2402,1655,16,2,17])).
% 72.83/72.81 cnf(2786,plain,
% 72.83/72.81 (~E(a3,f2(f2(a3,x27861),a4))),
% 72.83/72.81 inference(rename_variables,[],[2402])).
% 72.83/72.81 cnf(2789,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(f2(x27891,x27892),x27891))),
% 72.83/72.81 inference(scs_inference,[],[2771,2778,2402,1095,1655,16,2,17,7])).
% 72.83/72.81 cnf(2791,plain,
% 72.83/72.81 (~E(a3,f2(f2(a3,a4),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2771,2778,2402,2786,2220,1095,1655,16,2,17,7,3])).
% 72.83/72.81 cnf(2798,plain,
% 72.83/72.81 (~E(f2(a1,f2(x27981,x27981)),f2(f2(x27982,x27983),f2(a1,x27983)))),
% 72.83/72.81 inference(scs_inference,[],[2780,2574,16,2])).
% 72.83/72.81 cnf(2804,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a3,a4)),f2(x28041,a1))),
% 72.83/72.81 inference(scs_inference,[],[2780,2775,2791,2727,2574,1777,1655,119,16,2,6,17,7])).
% 72.83/72.81 cnf(2807,plain,
% 72.83/72.81 (~E(f2(f2(x28071,x28071),f2(x28072,x28071)),f2(f2(a3,a4),f2(x28073,x28073)))),
% 72.83/72.81 inference(scs_inference,[],[2780,2775,2784,2791,2727,2574,1777,978,1655,119,16,2,6,17,7,3])).
% 72.83/72.81 cnf(2811,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(x28111,a1)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2804,16])).
% 72.83/72.81 cnf(2814,plain,
% 72.83/72.81 (~E(f2(a4,x28141),f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[12,2804,2718,2807,16,2,6])).
% 72.83/72.81 cnf(2819,plain,
% 72.83/72.81 (~E(f2(f2(x28191,x28191),f2(a4,x28192)),f2(f2(a3,a4),f2(x28193,x28193)))),
% 72.83/72.81 inference(scs_inference,[],[12,2804,2718,2807,1568,2153,16,2,6,7,3])).
% 72.83/72.81 cnf(2826,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(a4,x28261)),f2(f2(x28262,x28263),x28262))),
% 72.83/72.81 inference(scs_inference,[],[2789,2819,132,2,6])).
% 72.83/72.81 cnf(2828,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(x28281,a1))),
% 72.83/72.81 inference(scs_inference,[],[2789,2819,1784,132,2,6,7])).
% 72.83/72.81 cnf(2831,plain,
% 72.83/72.81 (~E(f2(f2(x28311,x28311),f2(x28312,a1)),f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2814,2789,2819,1784,1439,132,2,6,7,3])).
% 72.83/72.81 cnf(2837,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x28371,x28371)),f2(x28372,a1))),
% 72.83/72.81 inference(scs_inference,[],[2828,2831,2351,16,2,6])).
% 72.83/72.81 cnf(2839,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(f2(x28391,x28391),f2(a4,x28392)))),
% 72.83/72.81 inference(scs_inference,[],[2828,2831,2228,1573,2351,16,2,6,7])).
% 72.83/72.81 cnf(2848,plain,
% 72.83/72.81 (~E(a4,f2(f2(f2(a3,a4),a4),f2(a4,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2837,2768,16,2])).
% 72.83/72.81 cnf(2849,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x28491,a1)),f2(x28492,a1))),
% 72.83/72.81 inference(scs_inference,[],[2837,2768,2282,16,2,6])).
% 72.83/72.81 cnf(2854,plain,
% 72.83/72.81 (~E(f2(f2(x28541,x28542),x28541),f2(a1,f2(a4,x28543)))),
% 72.83/72.81 inference(scs_inference,[],[2837,2543,2583,2768,2154,2282,162,16,2,6,7,3])).
% 72.83/72.81 cnf(2858,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x28581,x28581)),f2(f2(x28582,x28583),x28582))),
% 72.83/72.81 inference(scs_inference,[],[2849,2826,1837,2270,16,2,6])).
% 72.83/72.81 cnf(2861,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(f2(x28611,x28611),x28612))),
% 72.83/72.81 inference(scs_inference,[],[2849,2839,2826,1837,1680,2270,16,2,6,7])).
% 72.83/72.81 cnf(2863,plain,
% 72.83/72.81 (E(f2(f2(x28631,x28631),x28632),f2(f2(x28633,a1),x28634))),
% 72.83/72.81 inference(rename_variables,[],[1680])).
% 72.83/72.81 cnf(2864,plain,
% 72.83/72.81 (~E(f2(f2(x28641,a1),x28642),f2(f2(a1,a4),f2(x28643,x28643)))),
% 72.83/72.81 inference(scs_inference,[],[2849,2741,2839,2826,1837,1680,2863,2270,16,2,6,7,3])).
% 72.83/72.81 cnf(2866,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x28661)),f2(f2(a3,a4),f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2849,2741,2839,2826,1837,1873,1680,2863,2270,1619,16,2,6,7,3,17])).
% 72.83/72.81 cnf(2871,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(x28711,x28711)),f2(f2(x28712,a1),x28713))),
% 72.83/72.81 inference(scs_inference,[],[2864,2])).
% 72.83/72.81 cnf(2872,plain,
% 72.83/72.81 (~P1(a3,f2(x28721,x28721))),
% 72.83/72.81 inference(scs_inference,[],[2785,2864,970,2,7])).
% 72.83/72.81 cnf(2875,plain,
% 72.83/72.81 (~E(f2(f2(x28751,x28752),f2(a1,x28752)),f2(a1,f2(x28753,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2622,2785,2864,970,359,2,7,3])).
% 72.83/72.81 cnf(2878,plain,
% 72.83/72.81 (~E(f2(a1,f2(a4,x28781)),f2(f2(x28782,x28783),x28782))),
% 72.83/72.81 inference(scs_inference,[],[2854,2])).
% 72.83/72.81 cnf(2889,plain,
% 72.83/72.81 (~E(f2(a4,x28891),f2(f2(f2(a3,a4),a4),f2(a4,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2872,2875,2848,1381,26,2,7,3])).
% 72.83/72.81 cnf(2891,plain,
% 72.83/72.81 (~E(f2(f2(f2(a3,a4),a4),f2(a4,a4)),f2(a4,x28911))),
% 72.83/72.81 inference(scs_inference,[],[2889,2])).
% 72.83/72.81 cnf(2892,plain,
% 72.83/72.81 (~E(f2(f2(a1,a4),f2(x28921,a1)),f2(f2(x28922,a1),x28923))),
% 72.83/72.81 inference(scs_inference,[],[2871,2889,2324,2,3])).
% 72.83/72.81 cnf(2894,plain,
% 72.83/72.81 (E(f2(x28941,f2(x28942,a1)),f2(x28941,f2(x28943,a1)))),
% 72.83/72.81 inference(rename_variables,[],[2324])).
% 72.83/72.81 cnf(2895,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x28951,a1)),f2(f2(x28952,x28953),x28952))),
% 72.83/72.81 inference(scs_inference,[],[2858,2871,2889,2324,2894,2,3,6])).
% 72.83/72.81 cnf(2898,plain,
% 72.83/72.81 (~P1(f2(a3,f2(a4,x28981)),f2(f2(x28982,x28982),f2(x28983,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2858,2871,2889,2866,1442,2324,2894,2,3,6,7])).
% 72.83/72.81 cnf(2905,plain,
% 72.83/72.81 (~P1(f2(f2(f2(a3,a4),a4),f2(a4,a4)),f2(a4,x29051))),
% 72.83/72.81 inference(scs_inference,[],[2891,2892,140,2,17])).
% 72.83/72.81 cnf(2911,plain,
% 72.83/72.81 (~E(f2(f2(x29111,x29111),a4),f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[851,2])).
% 72.83/72.81 cnf(2915,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),a4),f2(f2(x29151,a1),x29152))),
% 72.83/72.81 inference(scs_inference,[],[851,2683,2763,968,11,2,17,7])).
% 72.83/72.81 cnf(2918,plain,
% 72.83/72.81 (~E(a4,f2(f2(f2(a1,a4),f2(x29181,x29181)),f2(x29182,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2311,2])).
% 72.83/72.81 cnf(2921,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a3,a4)),f2(x29211,a1))),
% 72.83/72.81 inference(scs_inference,[],[2861,2915,2311,1789,119,2,6,7])).
% 72.83/72.81 cnf(2926,plain,
% 72.83/72.81 (~E(a4,f2(f2(f2(a1,a4),f2(x29261,x29261)),f2(a4,x29262)))),
% 72.83/72.81 inference(scs_inference,[],[2921,2403,16,2])).
% 72.83/72.81 cnf(2927,plain,
% 72.83/72.81 (~E(f2(f2(a3,a4),f2(x29271,a1)),f2(f2(x29272,x29273),f2(a1,x29273)))),
% 72.83/72.81 inference(scs_inference,[],[2921,2732,2403,2338,16,2,3])).
% 72.83/72.81 cnf(2937,plain,
% 72.83/72.81 (~E(f2(a4,x29371),f2(f2(f2(a1,a4),f2(x29372,x29372)),f2(x29373,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2927,2918,26,2,3])).
% 72.83/72.81 cnf(2941,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a4),f2(x29411,x29411)),f2(x29412,a1)),f2(a4,x29413))),
% 72.83/72.81 inference(scs_inference,[],[2937,2])).
% 72.83/72.81 cnf(2942,plain,
% 72.83/72.81 (~E(f2(x29421,a1),f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2911,2937,1290,2,3])).
% 72.83/72.81 cnf(2945,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x29451,a1)),f2(x29452,x29452))),
% 72.83/72.81 inference(scs_inference,[],[2911,2937,2387,1290,994,2,3,7])).
% 72.83/72.81 cnf(2950,plain,
% 72.83/72.81 (~P1(f2(f2(f2(a3,a4),a4),f2(x29501,x29501)),f2(a4,x29502))),
% 72.83/72.81 inference(scs_inference,[],[2905,2911,2937,2387,1290,994,2295,2,3,7,16,6])).
% 72.83/72.81 cnf(2957,plain,
% 72.83/72.81 (~E(a4,f2(f2(f2(a3,a4),f2(x29571,x29571)),f2(a4,x29572)))),
% 72.83/72.81 inference(scs_inference,[],[2753,2])).
% 72.83/72.81 cnf(2958,plain,
% 72.83/72.81 (~E(f2(f2(x29581,x29582),x29581),f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2942,2753,1096,2,3])).
% 72.83/72.81 cnf(2960,plain,
% 72.83/72.81 (~P1(f2(a1,f2(x29601,x29601)),f2(x29602,x29602))),
% 72.83/72.81 inference(scs_inference,[],[2945,2942,2753,1096,2240,2,3,6])).
% 72.83/72.81 cnf(2963,plain,
% 72.83/72.81 (~P1(f2(f2(f2(a1,a4),f2(x29631,x29631)),f2(x29632,a1)),f2(a4,x29633))),
% 72.83/72.81 inference(scs_inference,[],[2945,2942,2941,2753,1096,2240,140,2,3,6,17])).
% 72.83/72.81 cnf(2966,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,x29661)),f2(f2(x29662,x29663),x29662))),
% 72.83/72.81 inference(scs_inference,[],[2945,2942,2941,2641,2753,1096,1053,2240,140,2,3,6,17,7])).
% 72.83/72.81 cnf(2969,plain,
% 72.83/72.81 (~E(f2(f2(a1,f2(x29691,x29691)),f2(x29692,x29692)),a4)),
% 72.83/72.81 inference(scs_inference,[],[2945,2942,2941,2641,2753,1096,1053,2240,140,2,3,6,17,7,16])).
% 72.83/72.81 cnf(2971,plain,
% 72.83/72.81 (~E(a4,f2(f2(a1,f2(x29711,x29711)),f2(x29712,x29712)))),
% 72.83/72.81 inference(scs_inference,[],[2969,2])).
% 72.83/72.81 cnf(2972,plain,
% 72.83/72.81 (~E(f2(a1,f2(x29721,x29721)),f2(f2(x29722,x29723),x29722))),
% 72.83/72.81 inference(scs_inference,[],[2878,2969,2255,2,3])).
% 72.83/72.81 cnf(2974,plain,
% 72.83/72.81 (E(f2(x29741,f2(a4,x29742)),f2(x29741,f2(x29743,x29743)))),
% 72.83/72.81 inference(rename_variables,[],[2255])).
% 72.83/72.81 cnf(2975,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a4,x29751)),f2(x29752,x29752))),
% 72.83/72.81 inference(scs_inference,[],[2960,2878,2969,2255,2974,2,3,6])).
% 72.83/72.81 cnf(2986,plain,
% 72.83/72.81 (~E(f2(f2(x29861,x29862),x29861),f2(a1,f2(x29863,x29863)))),
% 72.83/72.81 inference(scs_inference,[],[2972,2])).
% 72.83/72.81 cnf(2987,plain,
% 72.83/72.81 (~E(f2(a4,x29871),f2(f2(a1,f2(x29872,x29872)),f2(x29873,x29873)))),
% 72.83/72.81 inference(scs_inference,[],[2972,2971,26,2,3])).
% 72.83/72.81 cnf(2988,plain,
% 72.83/72.81 (~P1(f2(a1,f2(a4,x29881)),f2(f2(x29882,x29883),x29882))),
% 72.83/72.81 inference(scs_inference,[],[2975,2972,2971,961,26,2,3,7])).
% 72.83/72.81 cnf(2991,plain,
% 72.83/72.81 (~E(f2(f2(a1,f2(x29911,x29911)),f2(x29912,x29912)),f2(a4,x29913))),
% 72.83/72.81 inference(scs_inference,[],[2987,2])).
% 72.83/72.81 cnf(2992,plain,
% 72.83/72.81 (~E(f2(f2(x29921,x29921),f2(a4,x29922)),f2(a1,f2(a3,a4)))),
% 72.83/72.81 inference(scs_inference,[],[2958,2987,1528,2,3])).
% 72.83/72.81 cnf(2998,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x29981,x29981)),f2(f2(x29982,x29983),f2(a1,x29983)))),
% 72.83/72.81 inference(scs_inference,[],[2992,2668,964,2,7])).
% 72.83/72.81 cnf(3001,plain,
% 72.83/72.81 (~E(f2(a4,x30011),f2(f2(f2(a1,a4),f2(x30012,x30012)),f2(a4,x30013)))),
% 72.83/72.81 inference(scs_inference,[],[2992,2668,2926,964,26,2,7,3])).
% 72.83/72.81 cnf(3002,plain,
% 72.83/72.81 (~P1(f2(f2(a1,f2(x30021,x30021)),f2(x30022,x30022)),f2(a4,x30023))),
% 72.83/72.81 inference(scs_inference,[],[2991,2992,2668,2926,964,26,140,2,7,3,17])).
% 72.83/72.81 cnf(3005,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a4),f2(x30051,x30051)),f2(a4,x30052)),f2(a4,x30053))),
% 72.83/72.81 inference(scs_inference,[],[3001,2])).
% 72.83/72.81 cnf(3009,plain,
% 72.83/72.81 (~E(f2(a3,f2(x30091,a1)),f2(f2(x30092,x30092),x30093))),
% 72.83/72.81 inference(scs_inference,[],[18,2950,2770,3001,2270,2,7,3])).
% 72.83/72.81 cnf(3011,plain,
% 72.83/72.81 (E(f2(x30111,f2(x30112,x30112)),f2(x30111,f2(x30113,a1)))),
% 72.83/72.81 inference(rename_variables,[],[2270])).
% 72.83/72.81 cnf(3016,plain,
% 72.83/72.81 (~P1(f2(f2(f2(a1,a4),f2(x30161,x30161)),f2(x30162,x30162)),f2(a4,x30163))),
% 72.83/72.81 inference(scs_inference,[],[18,2950,2963,2770,3001,2270,3011,1619,2,7,3,17,6])).
% 72.83/72.81 cnf(3021,plain,
% 72.83/72.81 (E(a4,f2(x30211,a1))),
% 72.83/72.81 inference(rename_variables,[],[18])).
% 72.83/72.81 cnf(3023,plain,
% 72.83/72.81 (~E(f2(x30231,a1),f2(f2(f2(a3,a4),f2(x30232,x30232)),f2(a4,x30233)))),
% 72.83/72.81 inference(scs_inference,[],[18,3021,3016,3009,2957,2,7,3])).
% 72.83/72.81 cnf(3024,plain,
% 72.83/72.81 (~P1(f2(f2(f2(a1,a4),f2(x30241,x30241)),f2(a4,x30242)),f2(a4,x30243))),
% 72.83/72.81 inference(scs_inference,[],[18,3021,3016,3005,3009,2957,140,2,7,3,17])).
% 72.83/72.81 cnf(3031,plain,
% 72.83/72.81 (~E(f2(f2(x30311,x30311),f2(x30312,a1)),f2(a1,f2(x30313,x30313)))),
% 72.83/72.81 inference(scs_inference,[],[18,3024,2986,3023,1530,2,7,3])).
% 72.83/72.81 cnf(3037,plain,
% 72.83/72.81 (~E(f2(a1,f2(x30371,x30371)),f2(f2(x30372,x30372),f2(x30373,a1)))),
% 72.83/72.81 inference(scs_inference,[],[3031,2])).
% 72.83/72.81 cnf(3038,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x30381,x30381)),f2(f2(x30382,a1),x30383))),
% 72.83/72.81 inference(scs_inference,[],[2998,3031,1307,2,7])).
% 72.83/72.81 cnf(3055,plain,
% 72.83/72.81 (~E(a4,f2(f2(a3,f2(a3,a4)),f2(a4,x30551)))),
% 72.83/72.81 inference(scs_inference,[],[2242,2])).
% 72.83/72.81 cnf(3061,plain,
% 72.83/72.81 (~E(a4,f2(f2(a3,f2(a3,a4)),f2(x30611,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2811,2])).
% 72.83/72.81 cnf(3064,plain,
% 72.83/72.81 (E(a4,f2(x30641,a1))),
% 72.83/72.81 inference(rename_variables,[],[18])).
% 72.83/72.81 cnf(3065,plain,
% 72.83/72.81 (~E(f2(x30651,a1),f2(f2(a3,f2(a3,a4)),f2(a4,x30652)))),
% 72.83/72.81 inference(scs_inference,[],[18,3064,2497,2811,3055,2,7,3])).
% 72.83/72.81 cnf(3069,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(a4,x30691)),f2(x30692,a1))),
% 72.83/72.81 inference(scs_inference,[],[3065,2])).
% 72.83/72.81 cnf(3073,plain,
% 72.83/72.81 (~E(f2(a1,f2(a4,x30731)),f2(f2(x30732,x30733),f2(a1,x30733)))),
% 72.83/72.81 inference(scs_inference,[],[2895,2798,3065,929,2223,2,7,3])).
% 72.83/72.81 cnf(3079,plain,
% 72.83/72.81 (~E(f2(x30791,a1),f2(f2(a3,f2(a3,a4)),f2(x30792,a1)))),
% 72.83/72.81 inference(scs_inference,[],[18,2898,3073,3061,1443,2,7,3])).
% 72.83/72.81 cnf(3080,plain,
% 72.83/72.81 (~P1(f2(f2(a1,f2(x30801,x30801)),f2(x30802,a1)),f2(a4,x30803))),
% 72.83/72.81 inference(scs_inference,[],[18,3002,2898,3073,3061,1443,2310,2,7,3,6])).
% 72.83/72.81 cnf(3084,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(a4,x30841)),f2(x30842,x30842))),
% 72.83/72.81 inference(scs_inference,[],[2966,3079,1370,2,7])).
% 72.83/72.81 cnf(3087,plain,
% 72.83/72.81 (~E(f2(a1,f2(x30871,a1)),f2(f2(x30872,x30872),f2(x30873,a1)))),
% 72.83/72.81 inference(scs_inference,[],[2966,3037,3079,1370,2324,2,7,3])).
% 72.83/72.81 cnf(3090,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a4),f2(a4,x30901)),f2(x30902,x30902)),a4)),
% 72.83/72.81 inference(scs_inference,[],[3084,16])).
% 72.83/72.81 cnf(3096,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x30961,x30961)),f2(x30962,x30962))),
% 72.83/72.81 inference(scs_inference,[],[18,3084,3080,3087,2295,16,2,7,6])).
% 72.83/72.81 cnf(3105,plain,
% 72.83/72.81 (~E(f2(f2(f2(a1,a4),f2(x31051,x31051)),f2(x31052,x31052)),a4)),
% 72.83/72.81 inference(scs_inference,[],[3096,16])).
% 72.83/72.81 cnf(3114,plain,
% 72.83/72.81 (~E(a4,f2(f2(f2(a1,a4),f2(x31141,x31141)),f2(x31142,x31142)))),
% 72.83/72.81 inference(scs_inference,[],[3105,2])).
% 72.83/72.81 cnf(3118,plain,
% 72.83/72.81 (~E(a4,f2(f2(f2(a1,a4),f2(a4,x31181)),f2(x31182,x31182)))),
% 72.83/72.81 inference(scs_inference,[],[3090,2])).
% 72.83/72.81 cnf(3119,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(x31191,x31191)),f2(x31192,x31192))),
% 72.83/72.81 inference(scs_inference,[],[3038,3090,1562,2,7])).
% 72.83/72.81 cnf(3122,plain,
% 72.83/72.81 (~E(f2(a4,x31221),f2(f2(f2(a1,a4),f2(x31222,x31222)),f2(x31223,x31223)))),
% 72.83/72.81 inference(scs_inference,[],[3038,3114,3090,1562,26,2,7,3])).
% 72.83/72.81 cnf(3126,plain,
% 72.83/72.81 (~P1(f2(f2(a1,a4),f2(x31261,x31261)),f2(f2(a4,x31262),x31263))),
% 72.83/72.81 inference(scs_inference,[],[3122,2306,1309,2,7])).
% 72.83/72.81 cnf(3129,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(x31291,x31291)),f2(x31292,a1))),
% 72.83/72.81 inference(scs_inference,[],[3069,3122,2306,1309,2255,2,7,3])).
% 72.83/72.81 cnf(3131,plain,
% 72.83/72.81 (E(f2(x31311,f2(a4,x31312)),f2(x31311,f2(x31313,x31313)))),
% 72.83/72.81 inference(rename_variables,[],[2255])).
% 72.83/72.81 cnf(3132,plain,
% 72.83/72.81 (~P1(f2(f2(a3,a4),f2(a4,x31321)),f2(x31322,x31322))),
% 72.83/72.81 inference(scs_inference,[],[3119,3069,3122,2306,1309,2255,3131,2,7,3,6])).
% 72.83/72.81 cnf(3134,plain,
% 72.83/72.81 (~E(f2(f2(f2(a3,a4),f2(a4,x31341)),f2(x31342,x31342)),a4)),
% 72.83/72.81 inference(scs_inference,[],[3119,3069,3122,2306,1309,2255,3131,2,7,3,6,16])).
% 72.83/72.81 cnf(3139,plain,
% 72.83/72.81 (~E(f2(x31391,a1),f2(f2(a3,f2(a3,a4)),f2(x31392,x31392)))),
% 72.83/72.81 inference(scs_inference,[],[3129,2])).
% 72.83/72.81 cnf(3143,plain,
% 72.83/72.81 (~E(f2(a4,x31431),f2(f2(f2(a1,a4),f2(a4,x31432)),f2(x31433,x31433)))),
% 72.83/72.81 inference(scs_inference,[],[3132,3129,3118,1678,26,2,7,3])).
% 72.83/72.81 cnf(3151,plain,
% 72.83/72.81 (~E(f2(a4,x31511),f2(f2(a3,f2(a3,a4)),f2(x31512,x31512)))),
% 72.83/72.81 inference(scs_inference,[],[3139,3143,2303,1499,937,2,7,3])).
% 72.83/72.81 cnf(3157,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(x31571,x31571)),f2(a4,x31572))),
% 72.83/72.81 inference(scs_inference,[],[3151,2])).
% 72.83/72.81 cnf(3161,plain,
% 72.83/72.81 (~E(f2(x31611,x31611),f2(f2(a3,f2(a3,a4)),f2(x31612,x31612)))),
% 72.83/72.81 inference(scs_inference,[],[3126,3151,920,414,2,7,3])).
% 72.83/72.81 cnf(3167,plain,
% 72.83/72.81 (~E(f2(f2(a3,f2(a3,a4)),f2(a4,x31671)),f2(a4,x31672))),
% 72.83/72.81 inference(scs_inference,[],[3157,3161,2988,967,2223,2,7,3])).
% 72.83/72.81 cnf(3176,plain,
% 72.83/72.81 (~E(f2(a4,x31761),f2(f2(a3,f2(a3,a4)),f2(a4,x31762)))),
% 72.83/72.81 inference(scs_inference,[],[3167,2])).
% 72.83/72.81 cnf(3186,plain,
% 72.83/72.81 ($false),
% 72.83/72.81 inference(scs_inference,[],[3176,3134,2591,1456,920,13,1619,2,7,3,17]),
% 72.83/72.81 ['proof']).
% 72.83/72.81 % SZS output end Proof
% 72.83/72.81 % Total time :72.170000s
%------------------------------------------------------------------------------