%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN004-3 : 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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 07:26:46 EDT 2024
% Result : Unsatisfiable 82.16s 82.18s
% Output : CNFRefutation 82.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : HEN004-3 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sat Jun 22 05:24:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 82.16/82.17 %-------------------------------------------
% 82.16/82.17 % File :CSE---1.7
% 82.16/82.17 % Problem :theBenchmark
% 82.16/82.17 % Transform :cnf
% 82.16/82.17 % Format :tptp:raw
% 82.16/82.17 % Command :java -jar mcs_scs.jar %d %s
% 82.16/82.17
% 82.16/82.17 % Result :Theorem 81.580000s
% 82.16/82.17 % Output :CNFRefutation 81.580000s
% 82.16/82.17 %-------------------------------------------
% 82.16/82.18 %--------------------------------------------------------------------------
% 82.16/82.18 % File : HEN004-3 : TPTP v8.2.0. Released v1.0.0.
% 82.16/82.18 % Domain : Henkin Models
% 82.16/82.18 % Problem : X/zero = X
% 82.16/82.18 % Version : [MOW76] axioms.
% 82.16/82.18 % English :
% 82.16/82.18
% 82.16/82.18 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 82.16/82.18 % Source : [ANL]
% 82.16/82.18 % Names : HP4 [ANL]
% 82.16/82.18
% 82.16/82.18 % Status : Unsatisfiable
% 82.16/82.18 % 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
% 82.16/82.18 % Syntax : Number of clauses : 8 ( 5 unt; 0 nHn; 4 RR)
% 82.16/82.18 % Number of literals : 12 ( 4 equ; 5 neg)
% 82.16/82.18 % Maximal clause size : 3 ( 1 avg)
% 82.16/82.18 % Maximal term depth : 3 ( 1 avg)
% 82.16/82.18 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 82.16/82.18 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 82.16/82.18 % Number of variables : 13 ( 3 sgn)
% 82.16/82.18 % SPC : CNF_UNS_RFO_SEQ_HRN
% 82.16/82.18
% 82.16/82.18 % Comments :
% 82.16/82.18 %--------------------------------------------------------------------------
% 82.16/82.18 %----Include Henkin model axioms for equality formulation
% 82.16/82.18 include('Axioms/HEN002-0.ax').
% 82.16/82.18 %--------------------------------------------------------------------------
% 82.16/82.18 cnf(prove_x_divide_zero_is_x,negated_conjecture,
% 82.16/82.18 divide(a,zero) != a ).
% 82.16/82.18
% 82.16/82.18 %--------------------------------------------------------------------------
% 82.16/82.18 %-------------------------------------------
% 82.16/82.18 % Proof found
% 82.16/82.18 % SZS status Theorem for theBenchmark
% 82.16/82.18 % SZS output start Proof
% 82.16/82.19 %ClaNum:15(EqnAxiom:7)
% 82.16/82.19 %VarNum:26(SingletonVarNum:13)
% 82.16/82.19 %MaxLitNum:3
% 82.16/82.19 %MaxfuncDepth:2
% 82.16/82.19 %SharedTerms:5
% 82.16/82.19 %goalClause: 12
% 82.16/82.19 %singleGoalClaCount:1
% 82.16/82.19 [12]~E(f2(a3,a4),a3)
% 82.16/82.19 [8]P1(x81,a1)
% 82.16/82.19 [9]P1(a4,x91)
% 82.16/82.19 [10]P1(f2(x101,x102),x101)
% 82.16/82.19 [11]P1(f2(f2(x111,x112),f2(x113,x112)),f2(f2(x111,x113),x112))
% 82.16/82.19 [13]~P1(x131,x132)+E(f2(x131,x132),a4)
% 82.16/82.19 [14]P1(x141,x142)+~E(f2(x141,x142),a4)
% 82.16/82.19 [15]~P1(x152,x151)+~P1(x151,x152)+E(x151,x152)
% 82.16/82.19 %EqnAxiom
% 82.16/82.19 [1]E(x11,x11)
% 82.16/82.19 [2]E(x22,x21)+~E(x21,x22)
% 82.16/82.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 82.16/82.19 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 82.16/82.19 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 82.16/82.19 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 82.16/82.19 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 82.16/82.19
% 82.16/82.19 %-------------------------------------------
% 82.21/82.20 cnf(16,plain,
% 82.21/82.20 (~P1(a3,f2(a3,a4))),
% 82.21/82.20 inference(scs_inference,[],[12,10,15])).
% 82.21/82.20 cnf(19,plain,
% 82.21/82.20 (~E(a4,a3)),
% 82.21/82.20 inference(scs_inference,[],[12,9,10,15,6])).
% 82.21/82.20 cnf(23,plain,
% 82.21/82.20 (~P1(a3,a4)),
% 82.21/82.20 inference(scs_inference,[],[19,9,15])).
% 82.21/82.20 cnf(28,plain,
% 82.21/82.20 (P1(f2(f2(x281,x282),f2(x283,x282)),x284)+~E(f2(f2(x281,x283),x282),x284)),
% 82.21/82.20 inference(scs_inference,[],[16,19,11,9,10,15,6,7])).
% 82.21/82.20 cnf(30,plain,
% 82.21/82.20 (~E(a1,a4)),
% 82.21/82.20 inference(scs_inference,[],[23,8,7])).
% 82.21/82.20 cnf(32,plain,
% 82.21/82.20 (~E(f2(a4,x321),a3)),
% 82.21/82.20 inference(scs_inference,[],[23,8,10,7,6])).
% 82.21/82.20 cnf(38,plain,
% 82.21/82.20 (P1(f2(x381,x382),x383)+~E(x381,x383)),
% 82.21/82.20 inference(scs_inference,[],[10,7])).
% 82.21/82.20 cnf(39,plain,
% 82.21/82.20 (~E(f2(x391,x392),a3)+~E(x391,f2(a3,a4))),
% 82.21/82.20 inference(scs_inference,[],[16,10,7,6])).
% 82.21/82.20 cnf(43,plain,
% 82.21/82.20 (P1(x431,f2(f2(x432,x433),x434))+~E(f2(f2(x432,x434),f2(x433,x434)),x431)),
% 82.21/82.20 inference(scs_inference,[],[11,6])).
% 82.21/82.20 cnf(51,plain,
% 82.21/82.20 (E(f2(f2(a4,x511),x512),f2(a4,x512))),
% 82.21/82.20 inference(scs_inference,[],[9,4,13])).
% 82.21/82.20 cnf(52,plain,
% 82.21/82.20 (P1(f2(f2(f2(a4,x521),x522),x523),f2(a4,x522))),
% 82.21/82.20 inference(scs_inference,[],[51,38])).
% 82.21/82.20 cnf(53,plain,
% 82.21/82.20 (P1(f2(a4,f2(x531,x532)),f2(f2(a4,x531),x532))),
% 82.21/82.20 inference(scs_inference,[],[51,38,43])).
% 82.21/82.20 cnf(54,plain,
% 82.21/82.20 (E(f2(f2(a4,x541),x542),f2(a4,x542))),
% 82.21/82.20 inference(rename_variables,[],[51])).
% 82.21/82.20 cnf(55,plain,
% 82.21/82.20 (E(f2(a4,x551),f2(f2(a4,x552),x551))),
% 82.21/82.20 inference(scs_inference,[],[51,54,38,43,2])).
% 82.21/82.20 cnf(56,plain,
% 82.21/82.20 (P1(f2(a4,f2(x561,x562)),f2(a4,x562))),
% 82.21/82.20 inference(scs_inference,[],[51,54,38,43,2,7])).
% 82.21/82.20 cnf(60,plain,
% 82.21/82.20 (~P1(f2(f2(a4,x601),x602),f2(a4,f2(x601,x602)))+E(x603,f2(f2(a4,x601),x602))+~E(x603,f2(a4,f2(x601,x602)))),
% 82.21/82.20 inference(scs_inference,[],[51,54,38,43,2,7,15,6,3])).
% 82.21/82.20 cnf(63,plain,
% 82.21/82.20 (P1(f2(f2(a4,x631),x632),f2(f2(a4,x633),x631))),
% 82.21/82.20 inference(scs_inference,[],[55,38])).
% 82.21/82.20 cnf(64,plain,
% 82.21/82.20 (E(f2(f2(a4,x641),x642),f2(f2(a4,x643),x642))),
% 82.21/82.20 inference(scs_inference,[],[55,51,38,3])).
% 82.21/82.20 cnf(65,plain,
% 82.21/82.20 (E(f2(a4,x651),f2(f2(a4,x652),x651))),
% 82.21/82.20 inference(rename_variables,[],[55])).
% 82.21/82.20 cnf(68,plain,
% 82.21/82.20 (P1(f2(f2(a4,x681),f2(x682,x683)),f2(f2(a4,x682),x683))),
% 82.21/82.20 inference(scs_inference,[],[55,65,53,56,51,38,3,7,6])).
% 82.21/82.20 cnf(70,plain,
% 82.21/82.20 (E(f2(f2(f2(a4,x701),x702),x703),f2(a4,x702))+~P1(f2(a4,x702),f2(f2(f2(a4,x701),x702),x703))),
% 82.21/82.20 inference(scs_inference,[],[55,65,52,53,56,51,38,3,7,6,15])).
% 82.21/82.20 cnf(72,plain,
% 82.21/82.20 (P1(f2(a4,x721),f2(f2(f2(a4,x722),x723),x721))+~P1(f2(a4,x721),f2(f2(f2(a4,x722),x721),f2(x723,x721)))),
% 82.21/82.20 inference(scs_inference,[],[55,65,52,53,56,51,38,3,7,6,15,43])).
% 82.21/82.20 cnf(77,plain,
% 82.21/82.20 (P1(f2(f2(a4,x771),x772),f2(f2(a4,x773),x774))),
% 82.21/82.20 inference(scs_inference,[],[64,68,63,7,6])).
% 82.21/82.20 cnf(83,plain,
% 82.21/82.20 (E(f2(a4,f2(x831,x832)),f2(f2(a4,x831),x832))),
% 82.21/82.20 inference(scs_inference,[],[64,55,11,68,63,7,6,15,2,3])).
% 82.21/82.20 cnf(88,plain,
% 82.21/82.20 (P1(f2(f2(a4,x881),x882),f2(a4,x882))),
% 82.21/82.20 inference(scs_inference,[],[83,51,56,2,3,6])).
% 82.21/82.20 cnf(105,plain,
% 82.21/82.20 (~E(f2(a3,a4),x1051)+~E(f2(x1051,x1052),a3)),
% 82.21/82.20 inference(scs_inference,[],[39,2])).
% 82.21/82.20 cnf(131,plain,
% 82.21/82.20 (P1(f2(f2(a4,x1311),x1312),f2(a4,x1313))),
% 82.21/82.20 inference(scs_inference,[],[51,77,7])).
% 82.21/82.20 cnf(133,plain,
% 82.21/82.20 (P1(f2(a4,x1331),f2(a4,x1331))),
% 82.21/82.20 inference(scs_inference,[],[51,88,77,7,6])).
% 82.21/82.20 cnf(138,plain,
% 82.21/82.20 (P1(f2(a4,x1381),f2(f2(a4,x1382),x1383))),
% 82.21/82.20 inference(scs_inference,[],[51,55,77,133,7,6])).
% 82.21/82.20 cnf(143,plain,
% 82.21/82.20 (E(f2(f2(a4,x1431),x1432),f2(f2(a4,x1432),x1433))),
% 82.21/82.20 inference(scs_inference,[],[51,55,10,77,133,7,6,15,3])).
% 82.21/82.20 cnf(144,plain,
% 82.21/82.20 (E(f2(f2(a4,x1441),x1442),f2(a4,x1441))),
% 82.21/82.20 inference(scs_inference,[],[51,55,10,77,133,7,6,15,3,2])).
% 82.21/82.20 cnf(148,plain,
% 82.21/82.20 (E(f2(f2(a4,x1481),x1482),f2(a4,x1483))),
% 82.21/82.20 inference(scs_inference,[],[143,144,131,138,38,2,15])).
% 82.21/82.20 cnf(156,plain,
% 82.21/82.20 (P1(f2(f2(f2(a4,x1561),x1562),x1563),f2(a4,x1564))),
% 82.21/82.20 inference(scs_inference,[],[148,38])).
% 82.21/82.20 cnf(157,plain,
% 82.21/82.20 (E(f2(a4,x1571),f2(f2(a4,x1572),x1573))),
% 82.21/82.20 inference(scs_inference,[],[148,38,2])).
% 82.21/82.20 cnf(158,plain,
% 82.21/82.20 (E(f2(f2(a4,x1581),x1582),f2(f2(a4,x1583),x1584))),
% 82.21/82.20 inference(scs_inference,[],[148,131,38,2,60])).
% 82.21/82.20 cnf(168,plain,
% 82.21/82.20 (~E(f2(f2(f2(a4,x1681),x1682),f2(x1683,x1682)),f2(a4,x1683))+E(f2(f2(f2(a4,x1681),x1683),x1682),f2(a4,x1683))),
% 82.21/82.20 inference(scs_inference,[],[70,43])).
% 82.21/82.20 cnf(171,plain,
% 82.21/82.20 (~P1(f2(a4,x1711),f2(f2(f2(a4,x1712),x1713),f2(x1711,x1713)))+E(f2(f2(f2(a4,x1712),x1711),x1713),f2(a4,x1711))),
% 82.21/82.20 inference(scs_inference,[],[156,15,168])).
% 82.21/82.20 cnf(173,plain,
% 82.21/82.20 (P1(f2(a4,x1731),f2(f2(f2(a4,x1732),x1731),x1733))+~P1(f2(a4,x1731),f2(f2(f2(a4,x1732),x1733),f2(x1731,x1733)))),
% 82.21/82.21 inference(scs_inference,[],[156,15,168,43])).
% 82.21/82.21 cnf(178,plain,
% 82.21/82.21 (E(f2(a4,x1781),f2(a4,x1782))),
% 82.21/82.21 inference(scs_inference,[],[148,157,3])).
% 82.21/82.21 cnf(181,plain,
% 82.21/82.21 (E(a1,f2(a4,x1811))+~E(f2(f2(f2(a4,x1812),x1813),x1814),a1)),
% 82.21/82.21 inference(scs_inference,[],[148,157,8,156,3,6,15])).
% 82.21/82.21 cnf(186,plain,
% 82.21/82.21 (~E(a1,f2(f2(f2(a4,x1861),x1862),x1863))+E(a1,f2(a4,x1864))),
% 82.21/82.21 inference(scs_inference,[],[181,2])).
% 82.21/82.21 cnf(187,plain,
% 82.21/82.21 (~P1(a1,f2(f2(f2(a4,x1871),x1872),x1873))+E(a1,f2(a4,x1874))),
% 82.21/82.21 inference(scs_inference,[],[8,186,15])).
% 82.21/82.21 cnf(193,plain,
% 82.21/82.21 (~E(a4,f2(f2(f2(a4,x1931),x1932),f2(x1933,x1932)))+P1(f2(a4,x1932),f2(f2(f2(a4,x1931),x1933),x1932))),
% 82.21/82.21 inference(scs_inference,[],[72,38])).
% 82.21/82.21 cnf(197,plain,
% 82.21/82.21 (~E(a4,f2(f2(f2(a4,x1971),x1972),f2(x1973,x1972)))+P1(f2(a4,x1973),f2(f2(f2(a4,x1971),x1973),x1972))),
% 82.21/82.21 inference(scs_inference,[],[173,38])).
% 82.21/82.21 cnf(210,plain,
% 82.21/82.21 (~E(a4,f2(a3,a4))),
% 82.21/82.21 inference(scs_inference,[],[23,2,14])).
% 82.21/82.21 cnf(211,plain,
% 82.21/82.21 (~P1(f2(a3,a4),a4)),
% 82.21/82.21 inference(scs_inference,[],[210,9,15])).
% 82.21/82.21 cnf(214,plain,
% 82.21/82.21 (~E(a3,a4)),
% 82.21/82.21 inference(scs_inference,[],[210,9,10,15,7])).
% 82.21/82.21 cnf(217,plain,
% 82.21/82.21 (~E(a4,f2(f2(a3,a4),a4))),
% 82.21/82.21 inference(scs_inference,[],[211,2,14])).
% 82.21/82.21 cnf(218,plain,
% 82.21/82.21 (~P1(f2(f2(a3,a4),a4),a4)),
% 82.21/82.21 inference(scs_inference,[],[217,9,15])).
% 82.21/82.21 cnf(221,plain,
% 82.21/82.21 (~E(f2(a4,x2211),f2(a3,a4))),
% 82.21/82.21 inference(scs_inference,[],[211,217,9,10,15,6])).
% 82.21/82.21 cnf(223,plain,
% 82.21/82.21 (~E(a4,f2(f2(f2(a3,a4),a4),a4))),
% 82.21/82.21 inference(scs_inference,[],[218,2,14])).
% 82.21/82.21 cnf(224,plain,
% 82.21/82.21 (~P1(f2(f2(f2(a3,a4),a4),a4),a4)),
% 82.21/82.21 inference(scs_inference,[],[223,9,15])).
% 82.21/82.21 cnf(227,plain,
% 82.21/82.21 (~E(f2(a4,x2271),f2(f2(a3,a4),a4))),
% 82.21/82.21 inference(scs_inference,[],[218,223,9,10,15,6])).
% 82.21/82.21 cnf(232,plain,
% 82.21/82.21 (~E(a4,f2(a3,f2(a3,a4)))),
% 82.21/82.21 inference(scs_inference,[],[16,2,14])).
% 82.21/82.21 cnf(233,plain,
% 82.21/82.21 (~P1(f2(a3,f2(a3,a4)),a4)),
% 82.21/82.21 inference(scs_inference,[],[232,9,15])).
% 82.21/82.21 cnf(236,plain,
% 82.21/82.21 (~E(a4,f2(f2(a3,f2(a3,a4)),a4))),
% 82.21/82.21 inference(scs_inference,[],[233,2,14])).
% 82.21/82.21 cnf(237,plain,
% 82.21/82.21 (~P1(f2(f2(a3,f2(a3,a4)),a4),a4)),
% 82.21/82.21 inference(scs_inference,[],[236,9,15])).
% 82.21/82.21 cnf(240,plain,
% 82.21/82.21 (~E(f2(a4,x2401),f2(a3,f2(a3,a4)))),
% 82.21/82.21 inference(scs_inference,[],[233,236,9,10,15,6])).
% 82.21/82.21 cnf(243,plain,
% 82.21/82.21 (~E(f2(a4,x2431),f2(f2(a3,f2(a3,a4)),a4))),
% 82.21/82.21 inference(scs_inference,[],[237,10,6])).
% 82.21/82.21 cnf(246,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x2461),f2(x2462,x2461)),f2(a4,x2463)),a4)),
% 82.21/82.21 inference(scs_inference,[],[148,13,28])).
% 82.21/82.21 cnf(247,plain,
% 82.21/82.21 (E(a4,f2(f2(f2(a4,x2471),f2(x2472,x2471)),f2(a4,x2473)))),
% 82.21/82.21 inference(scs_inference,[],[246,2])).
% 82.21/82.21 cnf(248,plain,
% 82.21/82.21 (~E(a1,f2(f2(f2(a4,x2481),f2(x2482,x2481)),f2(a4,x2483)))),
% 82.21/82.21 inference(scs_inference,[],[30,246,2,3])).
% 82.21/82.21 cnf(253,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x2531),a4),f2(x2532,x2531)),f2(a4,f2(x2532,x2531)))),
% 82.21/82.21 inference(scs_inference,[],[156,30,246,2,3,193,197,15])).
% 82.21/82.21 cnf(256,plain,
% 82.21/82.21 (P1(f2(f2(a4,x2561),x2562),f2(f2(f2(a4,x2563),a4),f2(x2564,x2563)))),
% 82.21/82.21 inference(scs_inference,[],[157,156,30,246,2,3,193,197,15,6])).
% 82.21/82.21 cnf(258,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,a4),a4),a4),f2(a4,a4))),
% 82.21/82.21 inference(scs_inference,[],[157,156,30,246,2,3,193,197,15,6,171])).
% 82.21/82.21 cnf(261,plain,
% 82.21/82.21 (P1(f2(a4,x2611),f2(f2(f2(a4,x2612),f2(x2613,x2612)),f2(a4,x2614)))),
% 82.21/82.21 inference(scs_inference,[],[247,38])).
% 82.21/82.21 cnf(263,plain,
% 82.21/82.21 (E(f2(f2(a4,x2631),a4),f2(f2(f2(a4,x2631),a4),f2(x2632,x2631)))),
% 82.21/82.21 inference(scs_inference,[],[258,247,10,256,38,2,15])).
% 82.21/82.21 cnf(264,plain,
% 82.21/82.21 (P1(f2(f2(a4,x2641),x2642),f2(f2(f2(a4,x2643),a4),f2(x2644,x2643)))),
% 82.21/82.21 inference(rename_variables,[],[256])).
% 82.21/82.21 cnf(268,plain,
% 82.21/82.21 (P1(f2(a4,x2681),f2(f2(f2(a4,x2682),a4),f2(x2683,x2682)))),
% 82.21/82.21 inference(scs_inference,[],[148,258,247,10,214,256,264,246,38,2,15,3,6])).
% 82.21/82.21 cnf(270,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x2701),a4),f2(x2702,x2701)),f2(a4,a4))),
% 82.21/82.21 inference(scs_inference,[],[148,258,247,10,214,256,264,246,38,2,15,3,6,171])).
% 82.21/82.21 cnf(272,plain,
% 82.21/82.21 (P1(f2(a4,a4),f2(f2(f2(a4,a4),x2721),a4))),
% 82.21/82.21 inference(scs_inference,[],[148,258,247,10,214,256,264,246,38,2,15,3,6,171,43])).
% 82.21/82.21 cnf(281,plain,
% 82.21/82.21 (E(f2(f2(a4,x2811),x2812),f2(f2(f2(a4,x2813),a4),f2(x2814,x2813)))),
% 82.21/82.21 inference(scs_inference,[],[158,270,263,156,272,268,171,2,15,3])).
% 82.21/82.21 cnf(284,plain,
% 82.21/82.21 (P1(f2(f2(a4,x2841),x2842),f2(f2(f2(a4,x2843),f2(x2844,x2843)),f2(a4,x2845)))),
% 82.21/82.21 inference(scs_inference,[],[158,157,270,263,156,272,268,261,171,2,15,3,6])).
% 82.21/82.21 cnf(286,plain,
% 82.21/82.21 (P1(f2(f2(a4,x2861),x2862),a4)),
% 82.21/82.21 inference(scs_inference,[],[158,157,270,263,156,272,268,261,246,171,2,15,3,6,7])).
% 82.21/82.21 cnf(288,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x2881),a4),f2(x2882,x2881)),f2(f2(a4,x2883),x2884))),
% 82.21/82.21 inference(scs_inference,[],[281,2])).
% 82.21/82.21 cnf(289,plain,
% 82.21/82.21 (E(f2(f2(a4,x2891),f2(x2892,x2891)),f2(f2(f2(a4,x2891),f2(x2892,x2891)),f2(a4,x2893)))),
% 82.21/82.21 inference(scs_inference,[],[281,10,284,2,15])).
% 82.21/82.21 cnf(293,plain,
% 82.21/82.21 (~E(a1,f2(f2(a4,x2931),f2(x2932,x2931)))),
% 82.21/82.21 inference(scs_inference,[],[281,10,284,248,2,15,3])).
% 82.21/82.21 cnf(294,plain,
% 82.21/82.21 (~E(f2(f2(a4,x2941),x2942),f2(a3,a4))),
% 82.21/82.21 inference(scs_inference,[],[211,281,10,284,286,248,2,15,3,6])).
% 82.21/82.21 cnf(301,plain,
% 82.21/82.21 (~E(a1,f2(f2(a4,x3011),x3012))),
% 82.21/82.21 inference(scs_inference,[],[158,289,156,293,272,2,15,3])).
% 82.21/82.21 cnf(303,plain,
% 82.21/82.21 (~E(f2(f2(a4,x3031),x3032),f2(a3,f2(a3,a4)))),
% 82.21/82.21 inference(scs_inference,[],[233,158,289,156,293,272,286,2,15,3,6])).
% 82.21/82.21 cnf(306,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x3061),a4),f2(x3062,x3061)),f2(a4,x3063))),
% 82.21/82.21 inference(scs_inference,[],[253,156,268,2,15])).
% 82.21/82.21 cnf(311,plain,
% 82.21/82.21 (~E(f2(f2(a4,x3111),x3112),f2(f2(a3,a4),a4))),
% 82.21/82.21 inference(scs_inference,[],[218,157,253,156,301,268,286,2,15,3,6])).
% 82.21/82.21 cnf(316,plain,
% 82.21/82.21 (~P1(a1,f2(f2(f2(a4,x3161),x3162),x3163))),
% 82.21/82.21 inference(scs_inference,[],[218,157,253,156,301,268,286,2,15,3,6,181,186,187])).
% 82.21/82.21 cnf(318,plain,
% 82.21/82.21 (P1(f2(a4,x3181),f2(f2(f2(a4,a4),x3182),a4))),
% 82.21/82.21 inference(scs_inference,[],[218,157,253,156,301,268,286,2,15,3,6,181,186,187,43])).
% 82.21/82.21 cnf(322,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,a4),x3221),a4),f2(a4,x3222))),
% 82.21/82.21 inference(scs_inference,[],[306,156,318,2,15])).
% 82.21/82.21 cnf(325,plain,
% 82.21/82.21 (~E(f2(a4,x3251),a1)),
% 82.21/82.21 inference(scs_inference,[],[306,316,156,318,2,15,6])).
% 82.21/82.21 cnf(330,plain,
% 82.21/82.21 (E(f2(a4,x3301),f2(f2(f2(a4,x3302),f2(x3303,x3302)),f2(a4,x3304)))),
% 82.21/82.21 inference(scs_inference,[],[322,156,261,2,15])).
% 82.21/82.21 cnf(334,plain,
% 82.21/82.21 (~E(f2(f2(a4,x3341),x3342),a1)),
% 82.21/82.21 inference(scs_inference,[],[322,316,156,256,261,2,15,6])).
% 82.21/82.21 cnf(339,plain,
% 82.21/82.21 (E(f2(f2(a4,x3391),x3392),a4)),
% 82.21/82.21 inference(scs_inference,[],[330,9,286,2,15])).
% 82.21/82.21 cnf(342,plain,
% 82.21/82.21 (P1(f2(a4,x3421),x3422)),
% 82.21/82.21 inference(scs_inference,[],[330,9,286,2,15,14])).
% 82.21/82.21 cnf(344,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x3441),x3442),x3443),f2(a4,x3442))),
% 82.21/82.21 inference(scs_inference,[],[330,9,286,2,15,14,171])).
% 82.21/82.21 cnf(347,plain,
% 82.21/82.21 (P1(f2(f2(f2(a4,x3471),x3472),x3473),a4)),
% 82.21/82.21 inference(scs_inference,[],[339,38])).
% 82.21/82.21 cnf(349,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x3491),x3492),x3493),f2(a4,x3494))),
% 82.21/82.21 inference(scs_inference,[],[344,339,156,342,38,2,15])).
% 82.21/82.21 cnf(353,plain,
% 82.21/82.21 (~E(a3,f2(f2(a4,x3531),x3532))),
% 82.21/82.21 inference(scs_inference,[],[344,339,156,342,214,38,2,15,3])).
% 82.21/82.21 cnf(355,plain,
% 82.21/82.21 (E(f2(a4,x3551),f2(f2(f2(a4,x3552),x3553),x3554))),
% 82.21/82.21 inference(scs_inference,[],[349,2])).
% 82.21/82.21 cnf(358,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x3581),x3582),x3583),a4)),
% 82.21/82.21 inference(scs_inference,[],[224,349,9,10,347,2,7,15])).
% 82.21/82.21 cnf(363,plain,
% 82.21/82.21 (P1(f2(f2(a4,x3631),x3632),x3633)),
% 82.21/82.21 inference(scs_inference,[],[224,157,349,9,10,347,353,2,7,15,3,14])).
% 82.21/82.21 cnf(367,plain,
% 82.21/82.21 (~P1(f2(a3,a4),f2(f2(a4,x3671),x3672))),
% 82.21/82.21 inference(scs_inference,[],[358,294,363,2,15])).
% 82.21/82.21 cnf(375,plain,
% 82.21/82.21 (E(a4,f2(f2(a4,x3751),x3752))),
% 82.21/82.21 inference(scs_inference,[],[339,2])).
% 82.21/82.21 cnf(376,plain,
% 82.21/82.21 (~P1(f2(f2(a3,a4),a4),f2(f2(a4,x3761),x3762))),
% 82.21/82.21 inference(scs_inference,[],[339,311,363,2,15])).
% 82.21/82.21 cnf(379,plain,
% 82.21/82.21 (E(f2(f2(a4,x3791),x3792),f2(f2(f2(a4,x3793),f2(x3794,x3793)),f2(a4,x3795)))),
% 82.21/82.21 inference(scs_inference,[],[158,289,339,311,363,2,15,3])).
% 82.21/82.21 cnf(386,plain,
% 82.21/82.21 (E(f2(f2(f2(a4,x3861),f2(x3862,x3861)),f2(a4,x3863)),f2(f2(a4,x3864),x3865))),
% 82.21/82.21 inference(scs_inference,[],[379,2])).
% 82.21/82.21 cnf(389,plain,
% 82.21/82.21 (~P1(a3,f2(a4,x3891))),
% 82.21/82.21 inference(scs_inference,[],[32,376,379,10,342,2,7,15])).
% 82.21/82.21 cnf(398,plain,
% 82.21/82.21 (E(f2(a4,x3981),a4)),
% 82.21/82.21 inference(scs_inference,[],[355,358,303,363,15,3])).
% 82.21/82.21 cnf(400,plain,
% 82.21/82.21 (E(a4,f2(a4,x4001))),
% 82.21/82.21 inference(scs_inference,[],[355,358,303,363,15,3,2])).
% 82.21/82.21 cnf(402,plain,
% 82.21/82.21 (~P1(a1,f2(f2(a4,x4021),x4022))),
% 82.21/82.21 inference(scs_inference,[],[334,363,15])).
% 82.21/82.21 cnf(410,plain,
% 82.21/82.21 (~E(a4,a1)),
% 82.21/82.21 inference(scs_inference,[],[402,9,6])).
% 82.21/82.21 cnf(416,plain,
% 82.21/82.21 (~E(a4,f2(a3,f2(a4,x4161)))),
% 82.21/82.21 inference(scs_inference,[],[389,14,2])).
% 82.21/82.21 cnf(417,plain,
% 82.21/82.21 (~P1(f2(a3,f2(a4,x4171)),a4)),
% 82.21/82.21 inference(scs_inference,[],[416,9,15])).
% 82.21/82.21 cnf(427,plain,
% 82.21/82.21 (~P1(a1,a4)),
% 82.21/82.21 inference(scs_inference,[],[8,410,15])).
% 82.21/82.21 cnf(430,plain,
% 82.21/82.21 (~E(a4,f2(a1,a4))),
% 82.21/82.21 inference(scs_inference,[],[427,14,2])).
% 82.21/82.21 cnf(431,plain,
% 82.21/82.21 (~P1(f2(a1,a4),a4)),
% 82.21/82.21 inference(scs_inference,[],[430,9,15])).
% 82.21/82.21 cnf(434,plain,
% 82.21/82.21 (~E(a4,f2(f2(a1,a4),a4))),
% 82.21/82.21 inference(scs_inference,[],[431,14,2])).
% 82.21/82.21 cnf(435,plain,
% 82.21/82.21 (~P1(f2(f2(a1,a4),a4),a4)),
% 82.21/82.21 inference(scs_inference,[],[434,9,15])).
% 82.21/82.21 cnf(444,plain,
% 82.21/82.21 (~E(a4,f2(f2(a3,a4),f2(f2(a4,x4441),x4442)))),
% 82.21/82.21 inference(scs_inference,[],[367,14,2])).
% 82.21/82.21 cnf(445,plain,
% 82.21/82.21 (~P1(f2(f2(a3,a4),f2(f2(a4,x4451),x4452)),a4)),
% 82.21/82.21 inference(scs_inference,[],[444,9,15])).
% 82.21/82.21 cnf(451,plain,
% 82.21/82.21 (~P1(f2(a3,a4),f2(a4,x4511))),
% 82.21/82.21 inference(scs_inference,[],[221,342,15])).
% 82.21/82.21 cnf(454,plain,
% 82.21/82.21 (~E(a4,f2(f2(a3,a4),f2(a4,x4541)))),
% 82.21/82.21 inference(scs_inference,[],[451,14,2])).
% 82.21/82.21 cnf(455,plain,
% 82.21/82.21 (~P1(f2(f2(a3,a4),f2(a4,x4551)),a4)),
% 82.21/82.21 inference(scs_inference,[],[454,9,15])).
% 82.21/82.21 cnf(463,plain,
% 82.21/82.21 (~P1(f2(f2(a3,a4),a4),f2(a4,x4631))),
% 82.21/82.21 inference(scs_inference,[],[227,342,15])).
% 82.21/82.21 cnf(471,plain,
% 82.21/82.21 (~P1(f2(a3,f2(a3,a4)),f2(a4,x4711))),
% 82.21/82.21 inference(scs_inference,[],[240,342,15])).
% 82.21/82.21 cnf(474,plain,
% 82.21/82.21 (~E(a4,f2(f2(a3,f2(a3,a4)),f2(a4,x4741)))),
% 82.21/82.21 inference(scs_inference,[],[471,14,2])).
% 82.21/82.21 cnf(475,plain,
% 82.21/82.21 (~P1(f2(f2(a3,f2(a3,a4)),f2(a4,x4751)),a4)),
% 82.21/82.21 inference(scs_inference,[],[474,9,15])).
% 82.21/82.21 cnf(487,plain,
% 82.21/82.21 (~P1(f2(f2(a3,f2(a3,a4)),a4),f2(a4,x4871))),
% 82.21/82.21 inference(scs_inference,[],[243,342,15])).
% 82.21/82.21 cnf(491,plain,
% 82.21/82.21 (~P1(a1,f2(a4,x4911))),
% 82.21/82.21 inference(scs_inference,[],[325,342,15])).
% 82.21/82.21 cnf(494,plain,
% 82.21/82.21 (~E(a4,f2(a1,f2(a4,x4941)))),
% 82.21/82.21 inference(scs_inference,[],[491,14,2])).
% 82.21/82.21 cnf(495,plain,
% 82.21/82.21 (~P1(f2(a1,f2(a4,x4951)),a4)),
% 82.21/82.21 inference(scs_inference,[],[494,9,15])).
% 82.21/82.21 cnf(515,plain,
% 82.21/82.21 (~E(f2(f2(f2(a3,a4),a4),f2(a4,x5151)),f2(a4,x5152))),
% 82.21/82.21 inference(scs_inference,[],[463,398,14,3])).
% 82.21/82.21 cnf(531,plain,
% 82.21/82.21 (~E(f2(a3,f2(a3,a4)),f2(a4,x5311))),
% 82.21/82.21 inference(scs_inference,[],[487,10,7])).
% 82.21/82.21 cnf(537,plain,
% 82.21/82.21 (P1(f2(x5371,x5372),x5371)),
% 82.21/82.21 inference(rename_variables,[],[10])).
% 82.21/82.21 cnf(538,plain,
% 82.21/82.21 (~E(f2(a3,f2(a3,a4)),f2(f2(a4,x5381),x5382))),
% 82.21/82.21 inference(scs_inference,[],[435,148,10,531,7,3])).
% 82.21/82.21 cnf(540,plain,
% 82.21/82.21 (~E(f2(a4,x5401),f2(f2(a1,a4),a4))),
% 82.21/82.21 inference(scs_inference,[],[435,148,10,537,531,7,3,6])).
% 82.21/82.21 cnf(542,plain,
% 82.21/82.21 (~P1(f2(f2(a1,a4),a4),f2(a4,x5421))),
% 82.21/82.21 inference(scs_inference,[],[339,540,14,15])).
% 82.21/82.21 cnf(543,plain,
% 82.21/82.21 (~E(f2(f2(f2(a3,a4),a4),f2(a4,x5431)),f2(f2(a4,x5432),x5433))),
% 82.21/82.21 inference(scs_inference,[],[148,515,3])).
% 82.21/82.21 cnf(547,plain,
% 82.21/82.21 (~E(f2(a4,x5471),f2(a1,a4))),
% 82.21/82.21 inference(scs_inference,[],[542,148,10,515,3,6,4])).
% 82.21/82.21 cnf(548,plain,
% 82.21/82.21 (~E(a4,f2(f2(f2(a1,a4),a4),f2(a4,x5481)))),
% 82.21/82.21 inference(scs_inference,[],[542,14,2])).
% 82.21/82.21 cnf(554,plain,
% 82.21/82.21 (~E(f2(a4,x5541),f2(f2(a3,a4),f2(f2(a4,x5542),x5543)))),
% 82.21/82.21 inference(scs_inference,[],[445,548,386,9,10,538,3,15,6])).
% 82.21/82.21 cnf(565,plain,
% 82.21/82.21 (~P1(f2(f2(a3,a4),f2(f2(a4,x5651),x5652)),f2(a4,x5653))),
% 82.21/82.21 inference(scs_inference,[],[375,543,554,342,3,15])).
% 82.21/82.21 cnf(574,plain,
% 82.21/82.21 (~P1(f2(a1,a4),f2(a4,x5741))),
% 82.21/82.21 inference(scs_inference,[],[565,288,11,547,538,342,7,3,15])).
% 82.21/82.21 cnf(578,plain,
% 82.21/82.21 (~E(a4,f2(f2(a1,a4),f2(a4,x5781)))),
% 82.21/82.21 inference(scs_inference,[],[574,14,2])).
% 82.21/82.21 cnf(579,plain,
% 82.21/82.21 (~P1(f2(f2(a1,a4),f2(a4,x5791)),a4)),
% 82.21/82.21 inference(scs_inference,[],[578,9,15])).
% 82.21/82.21 cnf(612,plain,
% 82.21/82.21 (~E(f2(a4,x6121),f2(f2(a3,a4),f2(a4,x6122)))),
% 82.21/82.21 inference(scs_inference,[],[455,10,6])).
% 82.21/82.21 cnf(615,plain,
% 82.21/82.22 (~P1(f2(f2(a3,a4),f2(a4,x6151)),f2(a4,x6152))),
% 82.21/82.22 inference(scs_inference,[],[612,342,15])).
% 82.21/82.22 cnf(618,plain,
% 82.21/82.22 (~E(f2(a4,x6181),f2(f2(a1,a4),f2(a4,x6182)))),
% 82.21/82.22 inference(scs_inference,[],[579,10,612,342,15,6])).
% 82.21/82.22 cnf(620,plain,
% 82.21/82.22 (~E(a4,f2(f2(f2(a3,a4),f2(a4,x6201)),f2(a4,x6202)))),
% 82.21/82.22 inference(scs_inference,[],[615,14,2])).
% 82.21/82.22 cnf(621,plain,
% 82.21/82.22 (~P1(f2(f2(a1,a4),f2(a4,x6211)),f2(a4,x6212))),
% 82.21/82.22 inference(scs_inference,[],[618,342,15])).
% 82.21/82.22 cnf(626,plain,
% 82.21/82.22 (~E(a4,f2(f2(f2(a1,a4),f2(a4,x6261)),f2(a4,x6262)))),
% 82.21/82.22 inference(scs_inference,[],[621,14,2])).
% 82.21/82.22 cnf(669,plain,
% 82.21/82.22 (~P1(f2(f2(f2(a3,a4),f2(a4,x6691)),f2(a4,x6692)),a4)),
% 82.21/82.22 inference(scs_inference,[],[620,9,15])).
% 82.21/82.22 cnf(676,plain,
% 82.21/82.22 (~P1(f2(f2(f2(a1,a4),f2(a4,x6761)),f2(a4,x6762)),a4)),
% 82.21/82.22 inference(scs_inference,[],[626,9,15])).
% 82.21/82.22 cnf(722,plain,
% 82.21/82.22 (~P1(a1,f2(a3,a4))+~E(f2(a1,x7221),a3)),
% 82.21/82.22 inference(scs_inference,[],[8,105,15])).
% 82.21/82.22 cnf(723,plain,
% 82.21/82.22 (~E(f2(a1,x7231),a3)+~E(f2(a1,f2(a3,a4)),a4)),
% 82.21/82.22 inference(scs_inference,[],[722,14])).
% 82.21/82.22 cnf(756,plain,
% 82.21/82.22 (~E(f2(a4,x7561),f2(a3,f2(a4,x7562)))),
% 82.21/82.22 inference(scs_inference,[],[417,10,6])).
% 82.21/82.22 cnf(759,plain,
% 82.21/82.22 (~P1(f2(a3,f2(a4,x7591)),f2(a4,x7592))),
% 82.21/82.22 inference(scs_inference,[],[756,342,15])).
% 82.21/82.22 cnf(762,plain,
% 82.21/82.22 (~E(f2(f2(a4,x7621),x7622),f2(a3,f2(a4,x7623)))),
% 82.21/82.22 inference(scs_inference,[],[417,756,363,342,15,6])).
% 82.21/82.22 cnf(765,plain,
% 82.21/82.22 (~P1(f2(a3,f2(a4,x7651)),f2(f2(a4,x7652),x7653))),
% 82.21/82.22 inference(scs_inference,[],[762,363,15])).
% 82.21/82.22 cnf(805,plain,
% 82.21/82.22 (~E(f2(f2(a3,a4),f2(a3,a4)),a4)),
% 82.21/82.22 inference(scs_inference,[],[475,11,7])).
% 82.21/82.22 cnf(807,plain,
% 82.21/82.22 (~P1(f2(f2(a3,f2(a3,a4)),f2(a4,x8071)),a4)),
% 82.21/82.22 inference(rename_variables,[],[475])).
% 82.21/82.22 cnf(808,plain,
% 82.21/82.22 (~E(f2(a4,x8081),f2(f2(a3,f2(a3,a4)),f2(a4,x8082)))),
% 82.21/82.22 inference(scs_inference,[],[475,807,11,10,7,6])).
% 82.21/82.22 cnf(810,plain,
% 82.21/82.22 (~P1(f2(a3,a4),f2(a3,a4))),
% 82.21/82.22 inference(scs_inference,[],[475,807,11,10,7,6,13])).
% 82.21/82.22 cnf(813,plain,
% 82.21/82.22 (~P1(f2(f2(a3,f2(a3,a4)),f2(a4,x8131)),f2(a4,x8132))),
% 82.21/82.22 inference(scs_inference,[],[808,342,15])).
% 82.21/82.22 cnf(826,plain,
% 82.21/82.22 (~E(f2(f2(a3,a4),f2(a3,a4)),f2(a4,x8261))),
% 82.21/82.22 inference(scs_inference,[],[813,11,7])).
% 82.21/82.22 cnf(835,plain,
% 82.21/82.22 (~E(f2(a4,x8351),f2(a1,f2(a4,x8352)))),
% 82.21/82.22 inference(scs_inference,[],[495,10,6])).
% 82.21/82.22 cnf(838,plain,
% 82.21/82.22 (~P1(f2(a1,f2(a4,x8381)),f2(a4,x8382))),
% 82.21/82.22 inference(scs_inference,[],[835,342,15])).
% 82.21/82.22 cnf(841,plain,
% 82.21/82.22 (~E(f2(f2(a4,x8411),x8412),f2(a1,f2(a4,x8413)))),
% 82.21/82.22 inference(scs_inference,[],[495,835,363,342,15,6])).
% 82.21/82.22 cnf(844,plain,
% 82.21/82.22 (~P1(f2(a1,f2(a4,x8441)),f2(f2(a4,x8442),x8443))),
% 82.21/82.22 inference(scs_inference,[],[841,363,15])).
% 82.21/82.22 cnf(906,plain,
% 82.21/82.22 (~E(f2(a1,f2(a3,a4)),f2(a4,x9061))+~E(f2(a1,x9062),a3)),
% 82.21/82.22 inference(scs_inference,[],[398,723,3])).
% 82.21/82.22 cnf(907,plain,
% 82.21/82.22 (~E(f2(a4,x9071),f2(a1,f2(a3,a4)))+~E(f2(a1,x9072),a3)),
% 82.21/82.22 inference(scs_inference,[],[906,2])).
% 82.21/82.22 cnf(908,plain,
% 82.21/82.22 (~P1(f2(a1,f2(a3,a4)),f2(a4,x9081))+~E(f2(a1,x9082),a3)),
% 82.21/82.22 inference(scs_inference,[],[342,907,15])).
% 82.21/82.22 cnf(909,plain,
% 82.21/82.22 (~E(f2(a1,x9091),a3)+~E(f2(f2(a1,f2(a3,a4)),f2(a4,x9092)),a4)),
% 82.21/82.22 inference(scs_inference,[],[908,14])).
% 82.21/82.22 cnf(910,plain,
% 82.21/82.22 (~E(a4,f2(f2(a1,f2(a3,a4)),f2(a4,x9101)))+~E(f2(a1,x9102),a3)),
% 82.21/82.22 inference(scs_inference,[],[909,2])).
% 82.21/82.22 cnf(915,plain,
% 82.21/82.22 (~E(f2(a4,x9151),f2(f2(a1,f2(a3,a4)),f2(a4,x9152)))+~E(f2(a1,x9153),a3)),
% 82.21/82.22 inference(scs_inference,[],[400,910,3])).
% 82.21/82.22 cnf(919,plain,
% 82.21/82.22 (~E(f2(f2(a1,f2(a3,a4)),f2(a4,x9191)),f2(a4,x9192))+~E(f2(a1,x9193),a3)),
% 82.21/82.22 inference(scs_inference,[],[915,2])).
% 82.21/82.22 cnf(920,plain,
% 82.21/82.22 (~P1(f2(f2(a1,f2(a3,a4)),f2(a4,x9201)),f2(a4,x9202))+~E(f2(a1,x9203),a3)),
% 82.21/82.22 inference(scs_inference,[],[342,919,15])).
% 82.21/82.22 cnf(921,plain,
% 82.21/82.22 (~E(f2(f2(a1,a4),f2(a3,a4)),f2(a4,x9211))+~E(f2(a1,x9212),a3)),
% 82.21/82.22 inference(scs_inference,[],[920,28])).
% 82.21/82.22 cnf(1000,plain,
% 82.21/82.22 (P1(f2(x10001,x10002),x10001)),
% 82.21/82.22 inference(rename_variables,[],[10])).
% 82.21/82.22 cnf(1001,plain,
% 82.21/82.22 (~E(f2(f2(a3,a4),x10011),f2(a3,a4))),
% 82.21/82.22 inference(scs_inference,[],[810,10,1000,7,6])).
% 82.21/82.22 cnf(1044,plain,
% 82.21/82.22 (~P1(f2(a3,a4),f2(f2(a3,a4),x10441))),
% 82.21/82.22 inference(scs_inference,[],[1001,10,15])).
% 82.21/82.22 cnf(1048,plain,
% 82.21/82.22 (~E(a1,f2(f2(a3,a4),x10481))),
% 82.21/82.22 inference(scs_inference,[],[1044,8,7])).
% 82.21/82.22 cnf(1474,plain,
% 82.21/82.22 (P1(f2(f2(x14741,x14742),f2(a4,x14743)),f2(f2(x14741,a4),x14742))),
% 82.21/82.22 inference(scs_inference,[],[178,43,5])).
% 82.21/82.22 cnf(1505,plain,
% 82.21/82.22 (P1(f2(f2(x15051,x15052),a4),f2(f2(x15051,a4),x15052))),
% 82.21/82.22 inference(scs_inference,[],[398,43,5])).
% 82.21/82.22 cnf(1531,plain,
% 82.21/82.22 (~E(a3,f2(a1,x15311))+~E(f2(f2(a1,a4),f2(a3,a4)),f2(a4,x15312))),
% 82.21/82.22 inference(scs_inference,[],[921,2])).
% 82.21/82.22 cnf(1532,plain,
% 82.21/82.22 (~E(f2(a4,x15321),f2(f2(a1,a4),f2(a3,a4)))+~E(a3,f2(a1,x15322))),
% 82.21/82.22 inference(scs_inference,[],[1531,2])).
% 82.21/82.22 cnf(1533,plain,
% 82.21/82.22 (~P1(f2(f2(a1,a4),f2(a3,a4)),f2(a4,x15331))+~E(a3,f2(a1,x15332))),
% 82.21/82.22 inference(scs_inference,[],[342,1532,15])).
% 82.21/82.22 cnf(1534,plain,
% 82.21/82.22 (~E(a3,f2(a1,x15341))+~E(f2(f2(f2(a1,a4),f2(a3,a4)),f2(a4,x15342)),a4)),
% 82.21/82.22 inference(scs_inference,[],[1533,14])).
% 82.21/82.22 cnf(1535,plain,
% 82.21/82.22 (~E(a4,f2(f2(f2(a1,a4),f2(a3,a4)),f2(a4,x15351)))+~E(a3,f2(a1,x15352))),
% 82.21/82.22 inference(scs_inference,[],[1534,2])).
% 82.21/82.22 cnf(1536,plain,
% 82.21/82.22 (~E(f2(a4,x15361),f2(f2(f2(a1,a4),f2(a3,a4)),f2(a4,x15362)))+~E(a3,f2(a1,x15363))),
% 82.21/82.22 inference(scs_inference,[],[400,1535,3])).
% 82.21/82.22 cnf(1537,plain,
% 82.21/82.22 (~E(a4,f2(f2(a1,a4),f2(a3,a4)))+~E(a3,f2(a1,x15371))),
% 82.21/82.22 inference(scs_inference,[],[1536,4])).
% 82.21/82.22 cnf(1538,plain,
% 82.21/82.22 (~E(f2(f2(a1,a4),f2(a3,a4)),a4)+~E(a3,f2(a1,x15381))),
% 82.21/82.22 inference(scs_inference,[],[1537,2])).
% 82.21/82.22 cnf(1539,plain,
% 82.21/82.22 (~P1(f2(a1,a4),f2(a3,a4))+~E(a3,f2(a1,x15391))),
% 82.21/82.22 inference(scs_inference,[],[1538,13])).
% 82.21/82.22 cnf(1544,plain,
% 82.21/82.22 (~E(x15441,f2(a1,x15442))+~E(a3,x15441)+~P1(f2(a1,a4),f2(a3,a4))),
% 82.21/82.22 inference(scs_inference,[],[1539,3])).
% 82.21/82.22 cnf(1545,plain,
% 82.21/82.22 (~E(x15451,f2(a1,x15452))+~E(a3,x15451)+~E(f2(f2(a1,a4),f2(a3,a4)),a4)),
% 82.21/82.22 inference(scs_inference,[],[1544,14])).
% 82.21/82.22 cnf(1546,plain,
% 82.21/82.22 (~E(a4,f2(f2(a1,a4),f2(a3,a4)))+~E(x15461,f2(a1,x15462))+~E(a3,x15461)),
% 82.21/82.22 inference(scs_inference,[],[1545,2])).
% 82.21/82.22 cnf(1547,plain,
% 82.21/82.22 (~P1(f2(f2(a1,a4),f2(a3,a4)),a4)+~E(x15471,f2(a1,x15472))+~E(a3,x15471)),
% 82.21/82.22 inference(scs_inference,[],[9,1546,15])).
% 82.21/82.22 cnf(1650,plain,
% 82.21/82.22 (~E(f2(f2(a3,x16501),f2(a4,x16502)),f2(a3,a4))),
% 82.21/82.22 inference(scs_inference,[],[1044,1474,6])).
% 82.21/82.22 cnf(1653,plain,
% 82.21/82.22 (~E(f2(f2(a3,x16531),a4),f2(a3,a4))),
% 82.21/82.22 inference(scs_inference,[],[1044,1505,6])).
% 82.21/82.22 cnf(1655,plain,
% 82.21/82.22 (~E(f2(a3,x16551),a3)),
% 82.21/82.22 inference(scs_inference,[],[1044,1505,6,4])).
% 82.21/82.22 cnf(1667,plain,
% 82.21/82.22 (~P1(a3,f2(a3,x16671))),
% 82.21/82.22 inference(scs_inference,[],[1655,10,15])).
% 82.21/82.22 cnf(1671,plain,
% 82.21/82.22 (~E(a1,f2(a3,x16711))),
% 82.21/82.22 inference(scs_inference,[],[1667,8,7])).
% 82.21/82.22 cnf(1673,plain,
% 82.21/82.22 (~E(f2(f2(a3,x16731),x16732),a3)),
% 82.21/82.22 inference(scs_inference,[],[1667,8,10,7,6])).
% 82.21/82.22 cnf(1769,plain,
% 82.21/82.22 (E(f2(x17691,f2(a4,x17692)),f2(x17691,f2(a4,x17693)))),
% 82.21/82.22 inference(scs_inference,[],[178,5])).
% 82.21/82.22 cnf(1770,plain,
% 82.21/82.22 (E(f2(x17701,a1),a4)),
% 82.21/82.22 inference(scs_inference,[],[178,8,5,13])).
% 82.21/82.22 cnf(1772,plain,
% 82.21/82.22 (~E(f2(f2(a3,f2(a4,x17721)),f2(a4,x17722)),a4)),
% 82.21/82.22 inference(scs_inference,[],[178,759,8,5,13,14])).
% 82.21/82.22 cnf(1774,plain,
% 82.21/82.22 (E(f2(f2(x17741,a1),x17742),f2(a4,x17742))),
% 82.21/82.22 inference(scs_inference,[],[178,759,8,5,13,14,4])).
% 82.21/82.22 cnf(1775,plain,
% 82.21/82.22 (~E(f2(a3,x17751),a1)),
% 82.21/82.22 inference(scs_inference,[],[1671,178,759,8,5,13,14,4,2])).
% 82.21/82.22 cnf(1776,plain,
% 82.21/82.22 (E(f2(f2(x17761,a1),f2(x17762,x17763)),f2(f2(a4,x17762),x17763))),
% 82.21/82.22 inference(scs_inference,[],[1671,178,759,8,363,5,13,14,4,2,60])).
% 82.21/82.22 cnf(1779,plain,
% 82.21/82.22 (~P1(a1,f2(x17791,a1))),
% 82.21/82.22 inference(scs_inference,[],[1671,178,759,427,8,363,5,13,14,4,2,60,7])).
% 82.21/82.22 cnf(1783,plain,
% 82.21/82.22 (E(f2(f2(f2(x17831,x17832),a1),f2(x17833,x17834)),f2(a4,x17835))),
% 82.21/82.22 inference(scs_inference,[],[1671,178,759,427,8,363,5,13,14,4,2,60,7,43,1547,3])).
% 82.21/82.22 cnf(1788,plain,
% 82.21/82.22 (E(f2(x17881,f2(x17882,a1)),f2(x17881,a4))),
% 82.21/82.22 inference(scs_inference,[],[1770,5])).
% 82.21/82.22 cnf(1789,plain,
% 82.21/82.22 (E(f2(f2(x17891,x17892),x17891),a4)),
% 82.21/82.22 inference(scs_inference,[],[1770,10,5,13])).
% 82.21/82.22 cnf(1791,plain,
% 82.21/82.22 (~E(f2(a1,f2(x17911,a1)),a4)),
% 82.21/82.22 inference(scs_inference,[],[1770,1779,10,5,13,14])).
% 82.21/82.22 cnf(1793,plain,
% 82.21/82.22 (~E(f2(a3,a4),f2(f2(a3,x17931),f2(a4,x17932)))),
% 82.21/82.22 inference(scs_inference,[],[1770,1779,1650,10,5,13,14,2])).
% 82.21/82.22 cnf(1794,plain,
% 82.21/82.22 (~P1(f2(a3,f2(a4,x17941)),f2(f2(x17942,a1),f2(x17943,x17944)))),
% 82.28/82.22 inference(scs_inference,[],[1770,1779,1650,1776,765,10,5,13,14,2,7])).
% 82.28/82.22 cnf(1796,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x17961,a1)),a4)),
% 82.28/82.22 inference(scs_inference,[],[1770,1779,1650,1776,765,431,10,5,13,14,2,7,6])).
% 82.28/82.22 cnf(1804,plain,
% 82.28/82.22 (E(f2(x18041,f2(a4,x18042)),f2(x18041,a4))),
% 82.28/82.22 inference(scs_inference,[],[398,5])).
% 82.28/82.22 cnf(1807,plain,
% 82.28/82.22 (~E(f2(a4,x18071),f2(f2(a3,a4),f2(a3,a4)))),
% 82.28/82.22 inference(scs_inference,[],[826,838,398,5,14,2])).
% 82.28/82.22 cnf(1808,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x18081,a1)),f2(f2(x18082,x18083),x18082))),
% 82.28/82.22 inference(scs_inference,[],[826,1789,1796,838,398,5,14,2,7])).
% 82.28/82.22 cnf(1809,plain,
% 82.28/82.22 (~P1(f2(a3,f2(x18091,a1)),f2(a3,a4))),
% 82.28/82.22 inference(scs_inference,[],[826,1788,1789,1796,838,810,398,5,14,2,7,6])).
% 82.28/82.22 cnf(1811,plain,
% 82.28/82.22 (~E(a1,f2(f2(x18111,x18112),x18111))),
% 82.28/82.22 inference(scs_inference,[],[826,1788,1789,1796,838,810,398,5,14,2,7,6,38])).
% 82.28/82.22 cnf(1821,plain,
% 82.28/82.22 (E(f2(x18211,a4),f2(x18211,f2(a4,x18212)))),
% 82.28/82.22 inference(scs_inference,[],[400,5])).
% 82.28/82.22 cnf(1827,plain,
% 82.28/82.22 (~E(a4,f2(f2(a3,a4),f2(a3,a4)))),
% 82.28/82.22 inference(scs_inference,[],[1804,1653,1809,1807,398,400,5,14,2,7,3])).
% 82.28/82.22 cnf(1829,plain,
% 82.28/82.22 (~P1(f2(a3,f2(x18291,a1)),f2(a4,x18292))),
% 82.28/82.22 inference(scs_inference,[],[1804,1653,1809,1807,1788,451,398,400,5,14,2,7,3,6])).
% 82.28/82.22 cnf(1842,plain,
% 82.28/82.22 (~P1(f2(a3,f2(x18421,a1)),f2(f2(x18422,a1),x18423))),
% 82.28/82.22 inference(scs_inference,[],[1829,1811,1774,14,2,7])).
% 82.28/82.22 cnf(1845,plain,
% 82.28/82.22 (~P1(f2(a3,a4),f2(f2(x18451,a1),f2(x18452,x18453)))),
% 82.28/82.22 inference(scs_inference,[],[1829,1821,1811,1827,1794,1774,375,14,2,7,3,6])).
% 82.28/82.22 cnf(1849,plain,
% 82.28/82.22 (~E(a3,f2(f2(x18491,a1),x18492))),
% 82.28/82.22 inference(scs_inference,[],[1829,1821,1811,1827,1794,1774,375,14,2,7,3,6,43,38])).
% 82.28/82.22 cnf(1857,plain,
% 82.28/82.22 (~E(f2(a3,f2(a3,x18571)),a4)),
% 82.28/82.22 inference(scs_inference,[],[1667,14])).
% 82.28/82.22 cnf(1862,plain,
% 82.28/82.22 (E(f2(x18621,a4),f2(x18621,f2(a4,x18622)))),
% 82.28/82.22 inference(rename_variables,[],[1821])).
% 82.28/82.22 cnf(1863,plain,
% 82.28/82.22 (~P1(f2(a3,a4),f2(f2(x18631,a1),x18632))),
% 82.28/82.22 inference(scs_inference,[],[1845,1048,1842,1821,1862,1667,14,2,7,6])).
% 82.28/82.22 cnf(1875,plain,
% 82.28/82.22 (~E(f2(f2(x18751,x18752),f2(a1,x18752)),f2(a3,a4))),
% 82.28/82.22 inference(scs_inference,[],[1863,471,14,43])).
% 82.28/82.22 cnf(1890,plain,
% 82.28/82.22 (~E(f2(a3,a4),f2(f2(x18901,x18902),f2(a1,x18902)))),
% 82.28/82.22 inference(scs_inference,[],[1875,615,14,2])).
% 82.28/82.22 cnf(1891,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x18911,a1)),f2(f2(x18912,a1),f2(x18913,a4)))),
% 82.28/82.22 inference(scs_inference,[],[1875,1808,1776,615,14,2,7])).
% 82.28/82.22 cnf(1905,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x19051,a1)),f2(x19052,a1))),
% 82.28/82.22 inference(scs_inference,[],[1673,1796,1770,2,7])).
% 82.28/82.22 cnf(1911,plain,
% 82.28/82.22 (~E(a1,f2(x19111,a1))),
% 82.28/82.22 inference(scs_inference,[],[1673,1891,1796,1770,1769,2,7,6,14,38])).
% 82.28/82.22 cnf(1922,plain,
% 82.28/82.22 (~P1(f2(a1,f2(a4,x19221)),f2(x19222,a1))),
% 82.28/82.22 inference(scs_inference,[],[1911,1905,844,1776,1769,2,7,6])).
% 82.28/82.22 cnf(1927,plain,
% 82.28/82.22 (~E(a1,f2(f2(x19271,a1),f2(x19272,x19273)))),
% 82.28/82.22 inference(scs_inference,[],[1911,1905,844,1776,1769,2,7,6,14,38])).
% 82.28/82.22 cnf(1936,plain,
% 82.28/82.22 (~P1(f2(a1,f2(a4,x19361)),f2(f2(x19362,x19363),x19362))),
% 82.28/82.22 inference(scs_inference,[],[1849,1808,1769,2,6])).
% 82.28/82.22 cnf(1939,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x19391,a1)),f2(f2(a4,x19392),x19393))),
% 82.28/82.22 inference(scs_inference,[],[1849,1808,1796,1769,339,2,6,7])).
% 82.28/82.22 cnf(1949,plain,
% 82.28/82.22 (~P1(f2(a1,a4),f2(x19491,a1))),
% 82.28/82.22 inference(scs_inference,[],[1922,1927,1939,1821,43,2,6])).
% 82.28/82.22 cnf(1953,plain,
% 82.28/82.22 (~E(f2(f2(a1,a4),f2(x19531,a1)),a4)),
% 82.28/82.22 inference(scs_inference,[],[1922,1927,1939,1776,1821,43,2,6,7,14])).
% 82.28/82.22 cnf(1961,plain,
% 82.28/82.22 (~E(f2(f2(x19611,a1),f2(x19612,a1)),f2(a1,a4))),
% 82.28/82.22 inference(scs_inference,[],[1949,43])).
% 82.28/82.22 cnf(1963,plain,
% 82.28/82.22 (~E(a4,f2(f2(a1,a4),f2(x19631,a1)))),
% 82.28/82.22 inference(scs_inference,[],[1949,1953,43,2])).
% 82.28/82.22 cnf(1964,plain,
% 82.28/82.22 (~E(f2(f2(x19641,a1),x19642),a1)),
% 82.28/82.22 inference(scs_inference,[],[10,1949,1953,1779,43,2,6])).
% 82.28/82.22 cnf(1978,plain,
% 82.28/82.22 (~E(f2(f2(a4,x19781),x19782),f2(f2(a1,a4),f2(x19783,a1)))),
% 82.28/82.22 inference(scs_inference,[],[1961,1963,1936,1821,375,2,6,3])).
% 82.28/82.22 cnf(1979,plain,
% 82.28/82.22 (~P1(a3,f2(f2(x19791,a1),x19792))),
% 82.28/82.22 inference(scs_inference,[],[1961,1963,1936,1774,389,1821,375,2,6,3,7])).
% 82.28/82.22 cnf(1988,plain,
% 82.28/82.22 (~E(f2(f2(x19881,x19882),f2(a1,x19882)),a3)),
% 82.28/82.22 inference(scs_inference,[],[1979,43])).
% 82.28/82.22 cnf(2014,plain,
% 82.28/82.22 (~P1(f2(f2(a3,a4),f2(a4,x20141)),f2(f2(x20142,x20143),x20142))),
% 82.28/82.22 inference(scs_inference,[],[1988,1789,455,2,7])).
% 82.28/82.22 cnf(2015,plain,
% 82.28/82.22 (~E(f2(f2(x20151,x20151),f2(x20152,x20151)),f2(f2(a3,a4),f2(a4,x20153)))),
% 82.28/82.22 inference(scs_inference,[],[1988,1789,455,2,7,43])).
% 82.28/82.22 cnf(2017,plain,
% 82.28/82.22 (~E(f2(a3,a4),f2(f2(x20171,x20172),x20171))),
% 82.28/82.22 inference(scs_inference,[],[1988,1789,455,2,7,43,28,38])).
% 82.28/82.22 cnf(2025,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x20251,a1)),f2(a4,x20252))),
% 82.28/82.22 inference(scs_inference,[],[2017,574,1788,2,6])).
% 82.28/82.22 cnf(2039,plain,
% 82.28/82.22 (~P1(f2(a1,f2(x20391,a1)),f2(f2(x20392,a1),x20393))),
% 82.28/82.22 inference(scs_inference,[],[2025,1964,1774,2,7])).
% 82.28/82.22 cnf(2048,plain,
% 82.28/82.22 (~E(a4,f2(a1,f2(x20481,a1)))),
% 82.28/82.22 inference(scs_inference,[],[1791,2])).
% 82.28/82.22 cnf(2052,plain,
% 82.28/82.22 (~P1(f2(f2(a3,a4),f2(a4,x20521)),f2(f2(x20522,a1),f2(x20523,a4)))),
% 82.28/82.22 inference(scs_inference,[],[1791,2039,2014,1776,1769,2,6,7])).
% 82.28/82.22 cnf(2056,plain,
% 82.28/82.22 (~E(f2(f2(a3,a4),a4),f2(f2(x20561,a1),f2(x20562,a4)))),
% 82.28/82.22 inference(scs_inference,[],[1791,2039,2014,1776,1769,2,6,7,43,28])).
% 82.28/82.22 cnf(2057,plain,
% 82.28/82.22 (~E(f2(a3,a4),f2(f2(x20571,a1),f2(x20572,a4)))),
% 82.28/82.22 inference(scs_inference,[],[1791,2039,2014,1776,1769,2,6,7,43,28,38])).
% 82.28/82.22 cnf(2064,plain,
% 82.28/82.22 (~E(f2(a4,x20641),f2(a1,f2(x20642,a1)))),
% 82.28/82.22 inference(scs_inference,[],[2057,2048,1804,1044,400,2,6,3])).
% 82.28/82.22 cnf(2065,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),f2(a4,x20651)),f2(f2(x20652,x20653),x20652))),
% 82.28/82.22 inference(scs_inference,[],[2057,2048,579,1789,1804,1044,400,2,6,3,7])).
% 82.28/82.22 cnf(2067,plain,
% 82.28/82.22 (~E(f2(f2(a1,a4),a4),f2(f2(x20671,x20672),x20671))),
% 82.28/82.22 inference(scs_inference,[],[2057,2048,579,1789,1804,1044,400,2,6,3,7,43,28])).
% 82.28/82.22 cnf(2068,plain,
% 82.28/82.22 (~E(f2(a1,a4),f2(f2(x20681,x20682),x20681))),
% 82.28/82.22 inference(scs_inference,[],[2057,2048,579,1789,1804,1044,400,2,6,3,7,43,28,38])).
% 82.28/82.22 cnf(2070,plain,
% 82.28/82.22 (~E(f2(f2(x20701,x20701),f2(x20702,x20701)),f2(f2(a1,a4),f2(a4,x20703)))),
% 82.28/82.22 inference(scs_inference,[],[2068,2065,2,43])).
% 82.28/82.22 cnf(2072,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),f2(a4,x20721)),f2(f2(x20722,x20723),x20722))),
% 82.28/82.22 inference(rename_variables,[],[2065])).
% 82.28/82.22 cnf(2074,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),a4),f2(f2(x20741,x20742),x20741))),
% 82.28/82.22 inference(scs_inference,[],[2068,2065,2072,1776,1821,2,43,7,6])).
% 82.28/82.22 cnf(2076,plain,
% 82.28/82.22 (~E(f2(a1,a4),f2(f2(x20761,a1),f2(x20762,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2068,2065,2072,1776,1821,2,43,7,6,38])).
% 82.28/82.22 cnf(2080,plain,
% 82.28/82.22 (~E(f2(f2(x20801,x20801),f2(x20802,x20801)),f2(f2(a1,a4),a4))),
% 82.28/82.22 inference(scs_inference,[],[2076,2074,2,43])).
% 82.28/82.22 cnf(2082,plain,
% 82.28/82.22 (~E(f2(f2(a3,a4),f2(a4,x20821)),f2(x20822,a1))),
% 82.28/82.22 inference(scs_inference,[],[2076,2074,669,1770,2,43,7,38])).
% 82.28/82.22 cnf(2083,plain,
% 82.28/82.22 (~E(f2(f2(f2(a3,a4),a4),f2(a4,x20831)),f2(x20832,a1))),
% 82.28/82.22 inference(scs_inference,[],[2076,2074,669,1770,2,43,7,38,28])).
% 82.28/82.22 cnf(2085,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),a4),f2(f2(x20851,a1),f2(x20852,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2082,2074,1776,2,7])).
% 82.28/82.22 cnf(2090,plain,
% 82.28/82.22 (~E(f2(f2(a1,a4),f2(a4,x20901)),f2(x20902,a1))),
% 82.28/82.22 inference(scs_inference,[],[2064,676,1770,2,7,38])).
% 82.28/82.22 cnf(2091,plain,
% 82.28/82.22 (~E(f2(f2(f2(a1,a4),a4),f2(a4,x20911)),f2(x20912,a1))),
% 82.28/82.22 inference(scs_inference,[],[2064,676,1770,2,7,38,28])).
% 82.28/82.22 cnf(2092,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),f2(x20921,a1)),f2(f2(x20922,a1),f2(x20923,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2064,2085,676,1770,1788,2,7,38,28,6])).
% 82.28/82.22 cnf(2095,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),f2(x20951,a1)),f2(f2(a4,x20952),x20953))),
% 82.28/82.22 inference(scs_inference,[],[2090,2092,158,2,7])).
% 82.28/82.22 cnf(2098,plain,
% 82.28/82.22 (~E(a4,f2(a3,f2(a3,x20981)))),
% 82.28/82.22 inference(scs_inference,[],[1857,2])).
% 82.28/82.22 cnf(2099,plain,
% 82.28/82.22 (~P1(a3,f2(f2(x20991,x20992),x20991))),
% 82.28/82.22 inference(scs_inference,[],[1857,23,1789,2,7])).
% 82.28/82.22 cnf(2100,plain,
% 82.28/82.22 (~E(f2(f2(x21001,x21001),f2(x21002,x21001)),a3)),
% 82.28/82.22 inference(scs_inference,[],[11,1857,23,1789,2,7,6])).
% 82.28/82.22 cnf(2103,plain,
% 82.28/82.22 (~P1(a1,f2(f2(x21031,x21032),x21031))),
% 82.28/82.22 inference(scs_inference,[],[2100,427,1789,2,7])).
% 82.28/82.22 cnf(2105,plain,
% 82.28/82.22 (~E(f2(f2(x21051,x21051),f2(x21052,x21051)),a1)),
% 82.28/82.22 inference(scs_inference,[],[2100,2098,427,1789,375,2,7,3,43])).
% 82.28/82.22 cnf(2106,plain,
% 82.28/82.22 (~E(a1,f2(f2(x21061,x21061),f2(x21062,x21061)))),
% 82.28/82.22 inference(scs_inference,[],[2105,2])).
% 82.28/82.22 cnf(2111,plain,
% 82.28/82.22 (~P1(f2(f2(a3,a4),a4),f2(f2(x21111,x21112),x21111))),
% 82.28/82.22 inference(scs_inference,[],[2083,218,1789,2,7])).
% 82.28/82.22 cnf(2115,plain,
% 82.28/82.22 (~E(f2(f2(x21151,x21151),f2(x21152,x21151)),f2(f2(a3,a4),a4))),
% 82.28/82.22 inference(scs_inference,[],[2083,2052,218,1789,1821,2,7,6,43])).
% 82.28/82.22 cnf(2117,plain,
% 82.28/82.22 (~P1(a1,f2(f2(x21171,a1),f2(x21172,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2103,2091,1776,2,7])).
% 82.28/82.22 cnf(2120,plain,
% 82.28/82.22 (~P1(f2(f2(a3,a4),f2(x21201,a1)),f2(f2(x21202,x21203),x21202))),
% 82.28/82.22 inference(scs_inference,[],[2103,2091,2111,1776,1788,2,7,6])).
% 82.28/82.22 cnf(2122,plain,
% 82.28/82.22 (~E(f2(f2(x21221,x21221),f2(x21222,x21221)),f2(f2(a3,a4),f2(x21223,a1)))),
% 82.28/82.22 inference(scs_inference,[],[2103,2091,2111,1776,1788,2,7,6,43])).
% 82.28/82.22 cnf(2124,plain,
% 82.28/82.22 (~P1(f2(f2(a3,a4),f2(x21241,a1)),f2(f2(a4,x21242),f2(a4,x21243)))),
% 82.28/82.22 inference(scs_inference,[],[2080,2120,1804,2,7])).
% 82.28/82.22 cnf(2130,plain,
% 82.28/82.22 (~P1(a1,f2(f2(x21301,a1),f2(a4,x21302)))),
% 82.28/82.22 inference(scs_inference,[],[2117,2115,1769,2,7])).
% 82.28/82.22 cnf(2137,plain,
% 82.28/82.22 (~E(f2(f2(x21371,x21371),a4),a3)),
% 82.28/82.22 inference(scs_inference,[],[2067,2124,2099,1505,158,2,7,6])).
% 82.28/82.22 cnf(2144,plain,
% 82.28/82.22 (~E(f2(f2(x21441,a4),f2(a1,a4)),a1)),
% 82.28/82.22 inference(scs_inference,[],[2130,2137,1821,2,7,43])).
% 82.28/82.22 cnf(2146,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),a4),f2(x21461,a1))),
% 82.28/82.22 inference(scs_inference,[],[2144,435,1770,2,7])).
% 82.28/82.22 cnf(2147,plain,
% 82.28/82.22 (~E(f2(a1,a4),f2(x21471,a1))),
% 82.28/82.22 inference(scs_inference,[],[2144,435,1770,2,7,38])).
% 82.28/82.22 cnf(2149,plain,
% 82.28/82.22 (~E(f2(f2(x21491,x21491),f2(a4,x21492)),a1)),
% 82.28/82.22 inference(scs_inference,[],[2144,2103,1474,435,1770,2,7,38,43,6])).
% 82.28/82.22 cnf(2157,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),a4),f2(x21571,a1))),
% 82.28/82.22 inference(rename_variables,[],[2146])).
% 82.28/82.22 cnf(2158,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),f2(a4,x21581)),f2(x21582,a1))),
% 82.28/82.22 inference(scs_inference,[],[2147,2146,2157,1804,1776,14,2,7,6])).
% 82.28/82.22 cnf(2164,plain,
% 82.28/82.22 (~E(a1,f2(f2(x21641,x21641),f2(a4,x21642)))),
% 82.28/82.22 inference(scs_inference,[],[2158,2149,14,2])).
% 82.28/82.22 cnf(2179,plain,
% 82.28/82.22 (~P1(f2(f2(a1,a4),f2(x21791,a1)),f2(f2(x21792,a1),f2(x21793,x21794)))),
% 82.28/82.22 inference(scs_inference,[],[2015,2095,1776,2,7])).
% 82.28/82.22 cnf(2188,plain,
% 82.28/82.22 (~E(f2(f2(a1,a4),a4),f2(f2(x21881,a1),f2(x21882,x21883)))),
% 82.28/82.22 inference(scs_inference,[],[805,2070,2179,1789,1769,2,3,6,28])).
% 82.28/82.22 cnf(2189,plain,
% 82.28/82.22 (~P1(f2(a3,f2(a3,a4)),f2(f2(x21891,x21892),x21891))),
% 82.28/82.22 inference(scs_inference,[],[805,2070,2179,233,1789,1769,2,3,6,28,7])).
% 82.28/82.22 cnf(2191,plain,
% 82.28/82.22 (~E(f2(f2(x21911,x21911),f2(x21912,x21911)),f2(a3,f2(a3,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2189,38,43])).
% 82.28/82.22 cnf(2196,plain,
% 82.28/82.22 (~E(f2(a3,f2(x21961,a1)),a4)),
% 82.28/82.22 inference(scs_inference,[],[23,2191,1770,2,7,14])).
% 82.28/82.22 cnf(2198,plain,
% 82.28/82.22 (~E(a4,f2(a3,f2(x21981,a1)))),
% 82.28/82.22 inference(scs_inference,[],[2196,2])).
% 82.28/82.22 cnf(2199,plain,
% 82.28/82.22 (~P1(f2(a3,f2(a4,x21991)),f2(x21992,a1))),
% 82.28/82.22 inference(scs_inference,[],[2196,417,1770,2,7])).
% 82.28/82.22 cnf(2200,plain,
% 82.28/82.22 (~E(a3,f2(x22001,a1))),
% 82.28/82.22 inference(scs_inference,[],[2196,417,1770,2,7,38])).
% 82.28/82.22 cnf(2211,plain,
% 82.28/82.22 (~P1(f2(a3,a4),f2(x22111,a1))),
% 82.28/82.22 inference(scs_inference,[],[2200,2199,2198,1821,400,14,2,3,6])).
% 82.28/82.22 cnf(2213,plain,
% 82.28/82.22 (~E(f2(f2(x22131,a1),f2(x22132,a1)),f2(a3,a4))),
% 82.28/82.22 inference(scs_inference,[],[2200,2199,2198,1821,400,14,2,3,6,43])).
% 82.28/82.22 cnf(2214,plain,
% 82.28/82.22 (~E(f2(f2(a3,a4),f2(x22141,a1)),a4)),
% 82.28/82.22 inference(scs_inference,[],[2211,14])).
% 82.28/82.22 cnf(2219,plain,
% 82.28/82.22 (~E(f2(f2(x22191,x22191),a4),a1)),
% 82.28/82.22 inference(scs_inference,[],[2211,2213,1890,2103,1505,1821,14,2,3,6])).
% 82.28/82.22 cnf(2225,plain,
% 82.28/82.22 (~E(a4,f2(f2(a3,a4),f2(x22251,a1)))),
% 82.28/82.22 inference(scs_inference,[],[2214,2])).
% 82.28/82.22 cnf(2227,plain,
% 82.28/82.22 (~E(f2(f2(a4,x22271),x22272),f2(f2(a3,a4),f2(x22273,a1)))),
% 82.28/82.22 inference(scs_inference,[],[2225,2219,375,2,3])).
% 82.28/82.22 cnf(2234,plain,
% 82.28/82.22 (~E(f2(a1,f2(a3,x22341)),a4)),
% 82.28/82.22 inference(scs_inference,[],[1775,1793,2122,1821,8,2,15,3,14])).
% 82.28/82.22 cnf(2240,plain,
% 82.28/82.22 (~E(f2(a3,a4),f2(x22401,a1))),
% 82.28/82.22 inference(scs_inference,[],[1775,1793,2122,2099,1474,455,1770,1821,8,2,15,3,14,7,6,38])).
% 82.28/82.22 cnf(2256,plain,
% 82.28/82.22 (~E(a4,f2(a1,f2(a3,x22561)))),
% 82.28/82.22 inference(scs_inference,[],[2234,2])).
% 82.28/82.22 cnf(2257,plain,
% 82.28/82.22 (~P1(a1,f2(f2(x22571,x22571),f2(x22572,x22571)))),
% 82.28/82.22 inference(scs_inference,[],[2106,2234,8,2,15])).
% 82.28/82.22 cnf(2263,plain,
% 82.28/82.22 (~E(f2(a4,x22631),f2(a1,f2(a3,x22632)))),
% 82.28/82.22 inference(scs_inference,[],[2256,2188,400,2,3])).
% 82.28/82.22 cnf(2265,plain,
% 82.28/82.22 (~E(f2(a4,x22651),f2(f2(a1,a4),f2(x22652,a1)))),
% 82.28/82.22 inference(scs_inference,[],[2263,1978,1774,2,3])).
% 82.28/82.22 cnf(2268,plain,
% 82.28/82.22 (~E(f2(f2(x22681,x22681),a4),f2(a3,f2(a3,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2263,1978,2189,1505,1774,2,3,6])).
% 82.28/82.22 cnf(2271,plain,
% 82.28/82.22 (~E(f2(f2(a1,a4),f2(x22711,a1)),f2(a4,x22712))),
% 82.28/82.22 inference(scs_inference,[],[2265,2])).
% 82.28/82.22 cnf(2281,plain,
% 82.28/82.22 (~E(f2(f2(f2(a1,a4),f2(x22811,a1)),f2(a4,x22812)),a4)),
% 82.28/82.22 inference(scs_inference,[],[2271,2056,417,1789,1821,342,2,15,7,3,43,14])).
% 82.28/82.22 cnf(2284,plain,
% 82.28/82.22 (~E(f2(f2(a3,a4),f2(x22841,a1)),f2(a4,f2(x22842,x22843)))),
% 82.28/82.22 inference(scs_inference,[],[2227,363,2,60])).
% 82.28/82.22 cnf(2320,plain,
% 82.28/82.22 (~P1(f2(a3,f2(a3,a4)),f2(x23201,a1))),
% 82.28/82.22 inference(scs_inference,[],[2164,2268,233,1770,8,2,15,7])).
% 82.28/82.22 cnf(2321,plain,
% 82.28/82.22 (~E(f2(f2(x23211,a1),f2(x23212,a1)),f2(a3,f2(a3,a4)))),
% 82.28/82.22 inference(scs_inference,[],[2164,2268,233,1770,8,2,15,7,43])).
% 82.28/82.22 cnf(2325,plain,
% 82.28/82.22 (~E(f2(f2(x23251,a1),a4),f2(a3,f2(a3,a4)))),
% 82.28/82.23 inference(scs_inference,[],[2320,2321,1505,2,14,6])).
% 82.28/82.23 cnf(2332,plain,
% 82.28/82.23 (~E(f2(a4,f2(x23321,x23322)),f2(f2(a3,a4),f2(x23323,a1)))),
% 82.28/82.23 inference(scs_inference,[],[2284,2])).
% 82.28/82.23 cnf(2340,plain,
% 82.28/82.23 (~E(f2(f2(x23401,a4),f2(x23401,a4)),a1)),
% 82.28/82.23 inference(scs_inference,[],[2325,2257,1821,2,7,43])).
% 82.28/82.23 cnf(2341,plain,
% 82.28/82.23 (~E(f2(f2(x23411,a1),f2(a4,x23412)),f2(a3,f2(a3,a4)))),
% 82.28/82.23 inference(scs_inference,[],[2325,2257,2320,1474,1821,2,7,43,6])).
% 82.28/82.23 cnf(2345,plain,
% 82.28/82.23 (~E(f2(a4,x23451),f2(f2(a3,a4),f2(x23452,a1)))),
% 82.28/82.23 inference(scs_inference,[],[2340,2332,178,2,3])).
% 82.28/82.23 cnf(2349,plain,
% 82.28/82.23 (~E(f2(f2(a3,a4),f2(x23491,a1)),f2(a4,x23492))),
% 82.28/82.23 inference(scs_inference,[],[2345,2])).
% 82.28/82.23 cnf(2355,plain,
% 82.28/82.23 (~E(f2(f2(f2(a3,a4),f2(x23551,a1)),f2(a4,x23552)),a4)),
% 82.28/82.23 inference(scs_inference,[],[2349,2341,342,2,15,14])).
% 82.28/82.23 cnf(2496,plain,
% 82.28/82.23 (~E(a4,f2(f2(f2(a1,a4),f2(x24961,a1)),f2(a4,x24962)))),
% 82.28/82.23 inference(scs_inference,[],[2281,2])).
% 82.28/82.23 cnf(2497,plain,
% 82.28/82.23 (~E(a4,f2(f2(f2(a3,a4),f2(x24971,a1)),f2(a4,x24972)))),
% 82.28/82.23 inference(scs_inference,[],[2355,2])).
% 82.28/82.23 cnf(2498,plain,
% 82.28/82.23 (~E(f2(a4,x24981),f2(f2(f2(a1,a4),f2(x24982,a1)),f2(a4,x24983)))),
% 82.28/82.23 inference(scs_inference,[],[2355,2496,400,2,3])).
% 82.28/82.23 cnf(2499,plain,
% 82.28/82.23 (~E(f2(f2(f2(a1,a4),f2(x24991,a1)),f2(a4,x24992)),f2(a4,x24993))),
% 82.28/82.23 inference(scs_inference,[],[2498,2])).
% 82.28/82.23 cnf(2500,plain,
% 82.28/82.23 (~E(f2(a3,f2(a4,x25001)),f2(x25002,a1))),
% 82.28/82.23 inference(scs_inference,[],[2498,2240,1821,2,3])).
% 82.28/82.23 cnf(2507,plain,
% 82.28/82.23 (~E(f2(a4,x25071),f2(f2(f2(a3,a4),f2(x25072,a1)),f2(a4,x25073)))),
% 82.28/82.23 inference(scs_inference,[],[2500,2497,400,2,3])).
% 82.28/82.23 cnf(2509,plain,
% 82.28/82.23 (~E(f2(f2(a3,a4),f2(a3,a4)),f2(x25091,a1))),
% 82.28/82.23 inference(scs_inference,[],[2507,805,1770,2,3])).
% 82.28/82.23 cnf(2513,plain,
% 82.28/82.23 (~P1(f2(f2(a3,a4),f2(a3,a4)),f2(f2(a4,x25131),a1))),
% 82.28/82.23 inference(scs_inference,[],[2509,363,2,15])).
% 82.28/82.23 cnf(2517,plain,
% 82.28/82.23 (~E(f2(f2(a3,a3),a4),f2(f2(a4,x25171),a1))),
% 82.28/82.23 inference(scs_inference,[],[2509,363,2,15,28])).
% 82.28/82.23 cnf(2534,plain,
% 82.28/82.23 (~P1(f2(f2(a3,a4),f2(a3,a4)),f2(f2(a4,x25341),x25342))),
% 82.28/82.23 inference(scs_inference,[],[2499,2513,2517,158,342,2,15,7])).
% 82.28/82.23 cnf(2537,plain,
% 82.28/82.23 (~E(f2(f2(a3,a3),a4),f2(f2(a4,x25371),x25372))),
% 82.28/82.23 inference(scs_inference,[],[2499,2513,2517,158,342,2,15,7,28])).
% 82.28/82.23 cnf(2538,plain,
% 82.28/82.23 (~E(f2(f2(a4,x25381),x25382),f2(f2(a3,a3),a4))),
% 82.28/82.23 inference(scs_inference,[],[2537,2])).
% 82.28/82.23 cnf(2539,plain,
% 82.28/82.23 (~E(f2(f2(a3,a3),a4),f2(a4,f2(x25391,x25392)))),
% 82.28/82.23 inference(scs_inference,[],[2537,363,2,60])).
% 82.28/82.23 cnf(2544,plain,
% 82.28/82.23 (~E(f2(a4,x25441),f2(f2(a3,a3),a4))),
% 82.28/82.23 inference(scs_inference,[],[2538,2539,1774,2,3])).
% 82.28/82.23 cnf(2547,plain,
% 82.28/82.23 (~E(f2(f2(a3,a3),a4),f2(a4,x25471))),
% 82.28/82.23 inference(scs_inference,[],[2544,2])).
% 82.28/82.23 cnf(2549,plain,
% 82.28/82.23 (~P1(f2(f2(a3,a3),a4),f2(a4,x25491))),
% 82.28/82.23 inference(scs_inference,[],[2547,1772,342,2,15])).
% 82.28/82.23 cnf(2555,plain,
% 82.28/82.23 (~E(f2(a3,a3),f2(a4,x25551))),
% 82.28/82.23 inference(scs_inference,[],[2547,2534,1772,1776,342,2,15,7,38])).
% 82.28/82.23 cnf(2559,plain,
% 82.28/82.23 (~P1(f2(f2(a3,a3),f2(a4,x25591)),f2(a4,x25592))),
% 82.28/82.23 inference(scs_inference,[],[2547,2534,1772,1776,1804,342,2,15,7,38,14,28,6])).
% 82.28/82.23 cnf(2564,plain,
% 82.28/82.23 (~E(f2(f2(a3,a4),a3),f2(a4,x25641))),
% 82.28/82.23 inference(scs_inference,[],[2555,2559,2,14,28])).
% 82.28/82.23 cnf(2568,plain,
% 82.28/82.23 (~P1(f2(a3,a3),f2(a4,x25681))),
% 82.28/82.23 inference(scs_inference,[],[2555,2549,2559,1788,342,2,14,28,6,15])).
% 82.28/82.23 cnf(2579,plain,
% 82.28/82.23 (~P1(f2(a3,a3),f2(a4,x25791))),
% 82.28/82.23 inference(rename_variables,[],[2568])).
% 82.28/82.23 cnf(2583,plain,
% 82.28/82.23 (~E(f2(f2(a3,a4),a3),f2(a4,x25831))),
% 82.28/82.23 inference(rename_variables,[],[2564])).
% 82.28/82.23 cnf(2586,plain,
% 82.28/82.23 ($false),
% 82.28/82.23 inference(scs_inference,[],[2568,2579,2564,2583,1783,1789,400,10,342,2,14,7,6,15,3]),
% 82.28/82.23 ['proof']).
% 82.28/82.23 % SZS output end Proof
% 82.28/82.23 % Total time :81.580000s
%------------------------------------------------------------------------------