%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN003-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : 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:46 EDT 2024
% Result : Unsatisfiable 60.02s 60.08s
% Output : CNFRefutation 60.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : HEN003-3 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.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:33:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.49/0.59 start to proof:theBenchmark
% 60.00/60.07 %-------------------------------------------
% 60.00/60.07 % File :CSE---1.7
% 60.00/60.07 % Problem :theBenchmark
% 60.00/60.07 % Transform :cnf
% 60.00/60.07 % Format :tptp:raw
% 60.00/60.07 % Command :java -jar mcs_scs.jar %d %s
% 60.00/60.07
% 60.00/60.07 % Result :Theorem 59.410000s
% 60.00/60.07 % Output :CNFRefutation 59.410000s
% 60.00/60.07 %-------------------------------------------
% 60.02/60.08 %--------------------------------------------------------------------------
% 60.02/60.08 % File : HEN003-3 : TPTP v8.2.0. Released v1.0.0.
% 60.02/60.08 % Domain : Henkin Models
% 60.02/60.08 % Problem : X/X = zero
% 60.02/60.08 % Version : [MOW76] axioms.
% 60.02/60.08 % English :
% 60.02/60.08
% 60.02/60.08 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 60.02/60.08 % Source : [ANL]
% 60.02/60.08 % Names : HP3 [ANL]
% 60.02/60.08
% 60.02/60.08 % Status : Unsatisfiable
% 60.02/60.08 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 60.02/60.08 % Syntax : Number of clauses : 8 ( 5 unt; 0 nHn; 4 RR)
% 60.02/60.08 % Number of literals : 12 ( 4 equ; 5 neg)
% 60.02/60.08 % Maximal clause size : 3 ( 1 avg)
% 60.02/60.08 % Maximal term depth : 3 ( 1 avg)
% 60.02/60.08 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 60.02/60.08 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 60.02/60.08 % Number of variables : 13 ( 3 sgn)
% 60.02/60.08 % SPC : CNF_UNS_RFO_SEQ_HRN
% 60.02/60.08
% 60.02/60.08 % Comments :
% 60.02/60.08 %--------------------------------------------------------------------------
% 60.02/60.08 %----Include Henkin model axioms for equality formulation
% 60.02/60.08 include('Axioms/HEN002-0.ax').
% 60.02/60.08 %--------------------------------------------------------------------------
% 60.02/60.08 cnf(prove_x_divide_x_is_zero,negated_conjecture,
% 60.02/60.08 divide(a,a) != zero ).
% 60.02/60.08
% 60.02/60.08 %--------------------------------------------------------------------------
% 60.02/60.08 %-------------------------------------------
% 60.02/60.08 % Proof found
% 60.02/60.08 % SZS status Theorem for theBenchmark
% 60.02/60.08 % SZS output start Proof
% 60.02/60.09 %ClaNum:15(EqnAxiom:7)
% 60.02/60.09 %VarNum:26(SingletonVarNum:13)
% 60.02/60.09 %MaxLitNum:3
% 60.02/60.09 %MaxfuncDepth:2
% 60.02/60.09 %SharedTerms:5
% 60.02/60.09 %goalClause: 12
% 60.02/60.09 %singleGoalClaCount:1
% 60.02/60.09 [12]~E(f2(a3,a3),a4)
% 60.02/60.09 [8]P1(x81,a1)
% 60.02/60.09 [9]P1(a4,x91)
% 60.02/60.09 [10]P1(f2(x101,x102),x101)
% 60.02/60.09 [11]P1(f2(f2(x111,x112),f2(x113,x112)),f2(f2(x111,x113),x112))
% 60.02/60.09 [13]~P1(x131,x132)+E(f2(x131,x132),a4)
% 60.02/60.09 [14]P1(x141,x142)+~E(f2(x141,x142),a4)
% 60.02/60.09 [15]~P1(x152,x151)+~P1(x151,x152)+E(x151,x152)
% 60.02/60.09 %EqnAxiom
% 60.02/60.09 [1]E(x11,x11)
% 60.02/60.09 [2]E(x22,x21)+~E(x21,x22)
% 60.02/60.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.02/60.09 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 60.02/60.09 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 60.02/60.09 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 60.02/60.09 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 60.02/60.09
% 60.02/60.09 %-------------------------------------------
% 60.02/60.10 cnf(16,plain,
% 60.02/60.10 (~P1(a3,a3)),
% 60.02/60.10 inference(scs_inference,[],[12,13])).
% 60.02/60.10 cnf(18,plain,
% 60.02/60.10 (E(f2(a4,x181),a4)),
% 60.02/60.10 inference(scs_inference,[],[12,9,10,13,15])).
% 60.02/60.10 cnf(20,plain,
% 60.02/60.10 (P1(a4,x201)),
% 60.02/60.10 inference(rename_variables,[],[9])).
% 60.02/60.10 cnf(23,plain,
% 60.02/60.10 (~E(a4,a3)),
% 60.02/60.10 inference(scs_inference,[],[12,9,20,10,13,15,3,6])).
% 60.02/60.10 cnf(27,plain,
% 60.02/60.10 (E(a4,f2(a4,x271))),
% 60.02/60.10 inference(scs_inference,[],[12,8,9,20,10,13,15,3,6,7,2])).
% 60.02/60.10 cnf(28,plain,
% 60.02/60.10 (~E(a3,a4)),
% 60.02/60.10 inference(scs_inference,[],[12,8,9,20,10,13,15,3,6,7,2,4])).
% 60.02/60.10 cnf(29,plain,
% 60.02/60.10 (P1(f2(f2(a4,x291),x292),a4)),
% 60.02/60.10 inference(scs_inference,[],[18,10,7])).
% 60.02/60.10 cnf(30,plain,
% 60.02/60.10 (P1(f2(x301,x302),x301)),
% 60.02/60.10 inference(rename_variables,[],[10])).
% 60.02/60.10 cnf(31,plain,
% 60.02/60.10 (~P1(a3,a4)),
% 60.02/60.10 inference(scs_inference,[],[18,23,9,10,7,15])).
% 60.02/60.10 cnf(34,plain,
% 60.02/60.10 (~E(f2(a3,x341),a3)),
% 60.02/60.10 inference(scs_inference,[],[16,18,23,9,10,30,7,15,6])).
% 60.02/60.10 cnf(36,plain,
% 60.02/60.10 (E(f2(f2(a4,x361),x362),a4)),
% 60.02/60.10 inference(scs_inference,[],[29,9,15])).
% 60.02/60.10 cnf(39,plain,
% 60.02/60.10 (P1(f2(f2(a4,x391),x392),f2(a4,x393))),
% 60.02/60.10 inference(scs_inference,[],[27,29,9,15,7])).
% 60.02/60.10 cnf(40,plain,
% 60.02/60.10 (~E(f2(f2(a4,x401),x402),a3)),
% 60.02/60.10 inference(scs_inference,[],[27,31,29,9,15,7,6])).
% 60.02/60.10 cnf(41,plain,
% 60.02/60.10 (P1(f2(a4,x411),x412)),
% 60.02/60.10 inference(scs_inference,[],[27,31,29,9,15,7,6,14])).
% 60.02/60.10 cnf(43,plain,
% 60.02/60.10 (E(a4,f2(f2(a4,x431),x432))),
% 60.02/60.10 inference(scs_inference,[],[27,31,29,9,15,7,6,14,2])).
% 60.02/60.10 cnf(46,plain,
% 60.02/60.10 (E(f2(f2(a4,x461),x462),f2(a4,x463))),
% 60.02/60.10 inference(scs_inference,[],[41,39,15])).
% 60.02/60.10 cnf(48,plain,
% 60.02/60.10 (P1(f2(a4,x481),x482)),
% 60.02/60.10 inference(rename_variables,[],[41])).
% 60.02/60.10 cnf(50,plain,
% 60.02/60.10 (~E(f2(a4,x501),a3)),
% 60.02/60.10 inference(scs_inference,[],[16,41,48,39,15,6])).
% 60.02/60.10 cnf(52,plain,
% 60.02/60.10 (P1(f2(f2(f2(a4,x521),x522),x523),a4)),
% 60.02/60.10 inference(scs_inference,[],[16,36,41,48,39,10,15,6,7])).
% 60.02/60.10 cnf(54,plain,
% 60.02/60.10 (E(f2(a4,x541),f2(f2(a4,x542),x543))),
% 60.02/60.10 inference(scs_inference,[],[16,36,41,48,39,10,15,6,7,2])).
% 60.02/60.10 cnf(55,plain,
% 60.02/60.10 (E(f2(f2(f2(a4,x551),x552),x553),a4)),
% 60.02/60.10 inference(scs_inference,[],[52,9,15])).
% 60.02/60.10 cnf(61,plain,
% 60.02/60.10 (P1(f2(f2(a4,x611),x612),x613)),
% 60.02/60.10 inference(scs_inference,[],[54,31,52,39,9,15,7,6,14])).
% 60.02/60.10 cnf(63,plain,
% 60.02/60.10 (E(a4,f2(f2(f2(a4,x631),x632),x633))),
% 60.02/60.10 inference(scs_inference,[],[54,31,52,39,9,15,7,6,14,2])).
% 60.02/60.10 cnf(66,plain,
% 60.02/60.10 (~P1(a3,f2(f2(a4,x661),x662))),
% 60.02/60.10 inference(scs_inference,[],[61,40,15])).
% 60.02/60.10 cnf(69,plain,
% 60.02/60.10 (P1(f2(f2(f2(a4,x691),x692),x693),f2(a4,x694))),
% 60.02/60.10 inference(scs_inference,[],[46,61,40,10,15,7])).
% 60.02/60.10 cnf(71,plain,
% 60.02/60.10 (E(f2(f2(f2(a4,x711),x712),x713),f2(a4,x714))),
% 60.02/60.10 inference(scs_inference,[],[69,41,15])).
% 60.02/60.10 cnf(75,plain,
% 60.02/60.10 (E(f2(a4,x751),f2(f2(f2(a4,x752),x753),x754))),
% 60.02/60.10 inference(scs_inference,[],[69,41,15,2])).
% 60.02/60.10 cnf(80,plain,
% 60.02/60.10 (E(f2(f2(a4,x801),x802),f2(f2(a4,x802),f2(x801,x802)))),
% 60.02/60.10 inference(scs_inference,[],[11,61,15,2])).
% 60.02/60.10 cnf(81,plain,
% 60.02/60.10 (~P1(a3,f2(a4,x811))),
% 60.02/60.10 inference(scs_inference,[],[50,41,15])).
% 60.02/60.10 cnf(84,plain,
% 60.02/60.10 (~P1(a3,f2(a3,x841))),
% 60.02/60.10 inference(scs_inference,[],[34,10,15])).
% 60.02/60.10 cnf(95,plain,
% 60.02/60.10 (E(f2(x951,f2(f2(a4,x952),x953)),f2(x951,a4))),
% 60.02/60.10 inference(scs_inference,[],[43,2,5])).
% 60.02/60.10 cnf(96,plain,
% 60.02/60.10 (E(f2(x961,a4),f2(x961,f2(f2(a4,x962),x963)))),
% 60.02/60.10 inference(scs_inference,[],[95,2])).
% 60.02/60.10 cnf(97,plain,
% 60.02/60.10 (E(a4,f2(x971,a1))),
% 60.02/60.10 inference(scs_inference,[],[8,2,13])).
% 60.02/60.10 cnf(98,plain,
% 60.02/60.10 (E(f2(x981,a1),a4)),
% 60.02/60.10 inference(scs_inference,[],[97,2])).
% 60.02/60.10 cnf(100,plain,
% 60.02/60.10 (P1(f2(f2(f2(a4,x1001),x1002),x1003),f2(x1004,a1))),
% 60.02/60.10 inference(scs_inference,[],[12,97,52,2,3,7])).
% 60.02/60.10 cnf(102,plain,
% 60.02/60.10 (~P1(a1,a3)),
% 60.02/60.10 inference(scs_inference,[],[12,97,8,52,2,3,7,5,15])).
% 60.02/60.10 cnf(106,plain,
% 60.02/60.10 (P1(f2(f2(x1061,a1),f2(x1062,a1)),a4)),
% 60.02/60.10 inference(scs_inference,[],[98,11,7])).
% 60.02/60.10 cnf(109,plain,
% 60.02/60.10 (E(f2(f2(x1091,a1),f2(x1092,a1)),a4)),
% 60.02/60.10 inference(scs_inference,[],[98,11,9,7,15])).
% 60.02/60.10 cnf(112,plain,
% 60.02/60.10 (P1(f2(x1121,a1),f2(x1122,a1))),
% 60.02/60.10 inference(scs_inference,[],[98,11,9,7,15,14])).
% 60.02/60.10 cnf(114,plain,
% 60.02/60.10 (E(a4,f2(f2(x1141,a1),f2(x1142,a1)))),
% 60.02/60.10 inference(scs_inference,[],[98,11,9,7,15,14,2])).
% 60.02/60.10 cnf(118,plain,
% 60.02/60.10 (~E(f2(x1181,a1),a3)),
% 60.02/60.10 inference(scs_inference,[],[66,112,6])).
% 60.02/60.10 cnf(119,plain,
% 60.02/60.10 (P1(f2(x1191,a1),f2(x1192,a1))),
% 60.02/60.10 inference(rename_variables,[],[112])).
% 60.02/60.10 cnf(121,plain,
% 60.02/60.10 (P1(f2(x1211,a1),f2(f2(a4,a1),f2(x1212,a1)))),
% 60.02/60.10 inference(scs_inference,[],[66,80,112,119,6,7])).
% 60.02/60.10 cnf(129,plain,
% 60.02/60.10 (P1(f2(x1291,a1),a4)),
% 60.02/60.10 inference(scs_inference,[],[109,121,7])).
% 60.02/60.10 cnf(132,plain,
% 60.02/60.10 (E(a4,f2(f2(f2(x1321,a1),f2(x1322,a1)),a4))),
% 60.02/60.10 inference(scs_inference,[],[106,2,13])).
% 60.02/60.10 cnf(135,plain,
% 60.02/60.10 (P1(f2(x1351,a1),f2(f2(x1352,a1),f2(x1353,a1)))),
% 60.02/60.10 inference(scs_inference,[],[12,114,132,129,2,3,7])).
% 60.02/60.10 cnf(136,plain,
% 60.02/60.10 (E(f2(x1361,a1),f2(f2(f2(a4,x1362),a1),f2(x1363,a1)))),
% 60.02/60.10 inference(scs_inference,[],[12,114,132,129,100,2,3,7,15])).
% 60.02/60.10 cnf(140,plain,
% 60.02/60.10 (E(f2(f2(f2(a4,x1401),a1),f2(x1402,a1)),f2(x1403,a1))),
% 60.02/60.10 inference(scs_inference,[],[136,2])).
% 60.02/60.10 cnf(141,plain,
% 60.02/60.10 (E(f2(f2(x1411,a1),f2(x1412,a1)),f2(f2(x1411,x1412),a1))),
% 60.02/60.10 inference(scs_inference,[],[136,135,11,2,15])).
% 60.02/60.10 cnf(148,plain,
% 60.02/60.10 (P1(f2(x1481,a1),f2(a4,x1482))),
% 60.02/60.10 inference(scs_inference,[],[141,71,112,2,7])).
% 60.02/60.10 cnf(161,plain,
% 60.02/60.10 (P1(f2(f2(x1611,a1),f2(x1612,a1)),f2(a4,x1613))),
% 60.02/60.10 inference(scs_inference,[],[27,106,7])).
% 60.02/60.10 cnf(163,plain,
% 60.02/60.10 (E(f2(a4,a1),f2(f2(x1631,a1),f2(x1632,a1)))),
% 60.02/60.10 inference(scs_inference,[],[161,135,15])).
% 60.02/60.10 cnf(167,plain,
% 60.02/60.10 (P1(f2(x1671,a1),f2(f2(f2(x1672,a1),f2(x1673,a1)),a4))),
% 60.02/60.10 inference(scs_inference,[],[132,161,135,129,15,7])).
% 60.02/60.10 cnf(168,plain,
% 60.02/60.10 (E(f2(f2(x1681,a1),f2(x1682,a1)),f2(a4,a1))),
% 60.02/60.10 inference(scs_inference,[],[132,161,135,129,15,7,2])).
% 60.02/60.10 cnf(170,plain,
% 60.02/60.10 (E(a4,f2(f2(x1701,a1),f2(a4,x1702)))),
% 60.02/60.10 inference(scs_inference,[],[148,2,13])).
% 60.02/60.10 cnf(171,plain,
% 60.02/60.10 (E(f2(f2(x1711,a1),f2(a4,x1712)),a4)),
% 60.02/60.10 inference(scs_inference,[],[170,2])).
% 60.02/60.10 cnf(173,plain,
% 60.02/60.10 (E(f2(x1731,f2(a4,x1732)),f2(x1731,a4))),
% 60.02/60.10 inference(scs_inference,[],[27,2,5])).
% 60.02/60.11 cnf(174,plain,
% 60.02/60.11 (E(f2(x1741,a4),f2(x1741,f2(a4,x1742)))),
% 60.02/60.11 inference(scs_inference,[],[173,2])).
% 60.02/60.11 cnf(176,plain,
% 60.02/60.11 (P1(f2(x1761,a1),f2(f2(f2(x1762,a1),f2(x1763,a1)),f2(a4,x1764)))),
% 60.02/60.11 inference(scs_inference,[],[174,167,7])).
% 60.02/60.11 cnf(179,plain,
% 60.02/60.11 (P1(f2(f2(x1791,a1),f2(x1792,a1)),f2(f2(f2(x1793,a1),f2(x1794,a1)),f2(a4,x1795)))),
% 60.02/60.11 inference(scs_inference,[],[163,176,6])).
% 60.02/60.11 cnf(181,plain,
% 60.02/60.11 (E(f2(f2(x1811,a1),f2(x1812,a1)),f2(f2(f2(x1811,a1),f2(x1812,a1)),f2(a4,x1813)))),
% 60.02/60.11 inference(scs_inference,[],[163,176,10,6,15])).
% 60.02/60.11 cnf(184,plain,
% 60.02/60.11 (E(f2(f2(f2(x1841,a1),f2(x1842,a1)),f2(a4,x1843)),f2(f2(x1841,a1),f2(x1842,a1)))),
% 60.02/60.11 inference(scs_inference,[],[163,176,10,6,15,2])).
% 60.02/60.11 cnf(190,plain,
% 60.02/60.11 (P1(f2(x1901,a1),f2(f2(x1902,a1),f2(a4,x1903)))),
% 60.02/60.11 inference(scs_inference,[],[28,171,170,129,3,7])).
% 60.02/60.11 cnf(195,plain,
% 60.02/60.11 (E(a4,f2(f2(x1951,a1),f2(f2(x1952,a1),f2(a4,x1953))))),
% 60.02/60.11 inference(scs_inference,[],[190,2,13])).
% 60.02/60.11 cnf(198,plain,
% 60.02/60.11 (P1(f2(x1981,a1),f2(f2(x1982,a1),f2(f2(x1983,a1),f2(a4,x1984))))),
% 60.02/60.11 inference(scs_inference,[],[28,195,109,129,2,3,7])).
% 60.02/60.11 cnf(203,plain,
% 60.02/60.11 (P1(f2(f2(f2(x2031,a1),f2(x2032,a1)),x2033),f2(a4,a1))),
% 60.02/60.11 inference(scs_inference,[],[28,168,98,10,3,7])).
% 60.02/60.11 cnf(222,plain,
% 60.02/60.11 (~E(f2(f2(f2(a4,x2221),x2222),x2223),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[12,63,2,3])).
% 60.02/60.11 cnf(227,plain,
% 60.02/60.11 (P1(f2(x2271,a1),f2(f2(a4,x2272),x2273))),
% 60.02/60.11 inference(scs_inference,[],[43,129,7])).
% 60.02/60.11 cnf(228,plain,
% 60.02/60.11 (E(a4,f2(f2(x2281,a1),f2(f2(a4,x2282),x2283)))),
% 60.02/60.11 inference(scs_inference,[],[227,2,13])).
% 60.02/60.11 cnf(229,plain,
% 60.02/60.11 (E(f2(f2(x2291,a1),f2(f2(a4,x2292),x2293)),a4)),
% 60.02/60.11 inference(scs_inference,[],[228,2])).
% 60.02/60.11 cnf(234,plain,
% 60.02/60.11 (~P1(f2(a3,a3),a4)),
% 60.02/60.11 inference(scs_inference,[],[12,9,2,15])).
% 60.02/60.11 cnf(236,plain,
% 60.02/60.11 (~E(f2(f2(x2361,a1),f2(f2(a4,x2362),x2363)),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[12,228,2,3])).
% 60.02/60.11 cnf(237,plain,
% 60.02/60.11 (~E(f2(x2371,a1),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[234,129,6])).
% 60.02/60.11 cnf(238,plain,
% 60.02/60.11 (~P1(f2(a3,a3),f2(f2(a4,a1),f2(f2(a4,x2381),x2382)))),
% 60.02/60.11 inference(scs_inference,[],[234,236,61,129,6,15])).
% 60.02/60.11 cnf(243,plain,
% 60.02/60.11 (~P1(f2(a3,a3),f2(a4,a1))),
% 60.02/60.11 inference(scs_inference,[],[237,41,15])).
% 60.02/60.11 cnf(248,plain,
% 60.02/60.11 (~E(f2(f2(f2(x2481,a1),f2(x2482,a1)),x2483),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[243,203,6])).
% 60.02/60.11 cnf(259,plain,
% 60.02/60.11 (E(f2(f2(a4,x2591),x2592),f2(f2(x2593,a1),f2(x2594,a1)))),
% 60.02/60.11 inference(scs_inference,[],[41,114,13,3])).
% 60.02/60.11 cnf(260,plain,
% 60.02/60.11 (E(f2(f2(x2601,a1),f2(x2602,a1)),f2(f2(a4,x2603),x2604))),
% 60.02/60.11 inference(scs_inference,[],[259,2])).
% 60.02/60.11 cnf(261,plain,
% 60.02/60.11 (E(f2(f2(x2611,a1),f2(x2612,a1)),f2(a4,x2613))),
% 60.02/60.11 inference(scs_inference,[],[41,259,161,2,15])).
% 60.02/60.11 cnf(265,plain,
% 60.02/60.11 (P1(f2(f2(x2651,a1),f2(x2652,a1)),f2(f2(x2653,a1),f2(a4,x2654)))),
% 60.02/60.11 inference(scs_inference,[],[41,259,170,161,106,2,15,7])).
% 60.02/60.11 cnf(266,plain,
% 60.02/60.11 (E(f2(f2(a4,x2661),x2662),f2(x2663,a1))),
% 60.02/60.11 inference(scs_inference,[],[41,97,13,3])).
% 60.02/60.11 cnf(267,plain,
% 60.02/60.11 (E(f2(x2671,a1),f2(f2(a4,x2672),x2673))),
% 60.02/60.11 inference(scs_inference,[],[266,2])).
% 60.02/60.11 cnf(268,plain,
% 60.02/60.11 (E(f2(f2(f2(x2681,a1),f2(x2682,a1)),x2683),f2(a4,a1))),
% 60.02/60.11 inference(scs_inference,[],[41,266,203,2,15])).
% 60.02/60.11 cnf(274,plain,
% 60.02/60.11 (E(f2(a4,a1),f2(f2(f2(x2741,a1),f2(x2742,a1)),x2743))),
% 60.02/60.11 inference(scs_inference,[],[268,2])).
% 60.02/60.11 cnf(279,plain,
% 60.02/60.11 (E(f2(f2(x2791,a1),f2(x2792,a1)),f2(f2(x2793,a1),f2(x2794,a1)))),
% 60.02/60.11 inference(scs_inference,[],[261,163,2,3])).
% 60.02/60.11 cnf(283,plain,
% 60.02/60.11 (E(f2(f2(a4,x2831),x2832),f2(f2(a4,x2833),x2834))),
% 60.02/60.11 inference(scs_inference,[],[41,43,13,3])).
% 60.02/60.11 cnf(284,plain,
% 60.02/60.11 (E(f2(f2(x2841,a1),f2(x2842,a1)),f2(x2843,a1))),
% 60.02/60.11 inference(scs_inference,[],[279,140,3])).
% 60.02/60.11 cnf(287,plain,
% 60.02/60.11 (E(f2(x2871,a1),f2(f2(x2872,a1),f2(x2873,a1)))),
% 60.02/60.11 inference(scs_inference,[],[279,140,3,2])).
% 60.02/60.11 cnf(289,plain,
% 60.02/60.11 (E(f2(f2(x2891,a1),f2(f2(a4,x2892),x2893)),f2(a4,x2894))),
% 60.02/60.11 inference(scs_inference,[],[229,27,3])).
% 60.02/60.11 cnf(290,plain,
% 60.02/60.11 (E(f2(a4,x2901),f2(f2(x2902,a1),f2(f2(a4,x2903),x2904)))),
% 60.02/60.11 inference(scs_inference,[],[229,27,3,2])).
% 60.02/60.11 cnf(292,plain,
% 60.02/60.11 (E(f2(a4,x2921),f2(a4,x2922))),
% 60.02/60.11 inference(scs_inference,[],[290,71,3])).
% 60.02/60.11 cnf(295,plain,
% 60.02/60.11 (E(f2(f2(x2951,a1),f2(f2(a4,x2952),x2953)),f2(x2954,a1))),
% 60.02/60.11 inference(scs_inference,[],[229,97,3])).
% 60.02/60.11 cnf(296,plain,
% 60.02/60.11 (E(f2(x2961,a1),f2(f2(x2962,a1),f2(f2(a4,x2963),x2964)))),
% 60.02/60.11 inference(scs_inference,[],[229,97,3,2])).
% 60.02/60.11 cnf(298,plain,
% 60.02/60.11 (E(f2(f2(x2981,a1),f2(a4,x2982)),f2(f2(x2983,a1),f2(x2984,a1)))),
% 60.02/60.11 inference(scs_inference,[],[171,114,3])).
% 60.02/60.11 cnf(299,plain,
% 60.02/60.11 (E(f2(f2(x2991,a1),f2(x2992,a1)),f2(f2(x2993,a1),f2(a4,x2994)))),
% 60.02/60.11 inference(scs_inference,[],[171,114,3,2])).
% 60.02/60.11 cnf(300,plain,
% 60.02/60.11 (E(f2(f2(x3001,a1),f2(a4,x3002)),f2(a4,x3003))),
% 60.02/60.11 inference(scs_inference,[],[298,71,3])).
% 60.02/60.11 cnf(305,plain,
% 60.02/60.11 (E(f2(f2(x3051,a1),f2(x3052,a1)),f2(f2(f2(a4,a1),f2(x3053,a1)),f2(a4,x3054)))),
% 60.02/60.11 inference(scs_inference,[],[260,300,181,2,3])).
% 60.02/60.11 cnf(309,plain,
% 60.02/60.11 (E(f2(f2(f2(a4,a1),f2(x3091,a1)),f2(a4,x3092)),f2(f2(x3093,a1),f2(x3094,a1)))),
% 60.02/60.11 inference(scs_inference,[],[305,2])).
% 60.02/60.11 cnf(312,plain,
% 60.02/60.11 (P1(f2(f2(x3121,a1),f2(a4,x3122)),f2(f2(x3123,a1),f2(x3124,a1)))),
% 60.02/60.11 inference(scs_inference,[],[299,184,305,179,2,6,7])).
% 60.02/60.11 cnf(313,plain,
% 60.02/60.11 (E(f2(x3131,a1),f2(a4,x3132))),
% 60.02/60.11 inference(scs_inference,[],[299,267,289,184,305,179,2,6,7,3])).
% 60.02/60.11 cnf(317,plain,
% 60.02/60.11 (E(f2(a4,x3171),f2(x3172,a1))),
% 60.02/60.11 inference(scs_inference,[],[313,2])).
% 60.02/60.11 cnf(318,plain,
% 60.02/60.11 (~E(f2(f2(x3181,a1),f2(a4,x3182)),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[313,238,312,2,6])).
% 60.02/60.11 cnf(324,plain,
% 60.02/60.11 (E(f2(x3241,a1),f2(x3242,a1))),
% 60.02/60.11 inference(scs_inference,[],[295,296,284,313,238,265,312,2,6,7,3])).
% 60.02/60.11 cnf(331,plain,
% 60.02/60.11 (P1(f2(f2(x3311,a1),f2(a4,x3312)),f2(f2(a4,x3313),x3314))),
% 60.02/60.11 inference(scs_inference,[],[283,318,312,61,15,7])).
% 60.02/60.11 cnf(334,plain,
% 60.02/60.11 (E(f2(a4,x3341),f2(f2(f2(x3342,a1),f2(x3343,a1)),x3344))),
% 60.02/60.11 inference(scs_inference,[],[292,274,283,318,312,61,15,7,3])).
% 60.02/60.11 cnf(336,plain,
% 60.02/60.11 (E(f2(f2(f2(x3361,a1),f2(x3362,a1)),x3363),f2(a4,x3364))),
% 60.02/60.11 inference(scs_inference,[],[292,274,283,318,312,61,15,7,3,2])).
% 60.02/60.11 cnf(342,plain,
% 60.02/60.11 (E(f2(x3421,a1),f2(f2(f2(x3422,a1),f2(x3423,a1)),f2(a4,x3424)))),
% 60.02/60.11 inference(scs_inference,[],[287,181,331,190,15,3])).
% 60.02/60.11 cnf(344,plain,
% 60.02/60.11 (E(f2(f2(x3441,a1),f2(a4,x3442)),f2(f2(a4,x3443),a1))),
% 60.02/60.11 inference(scs_inference,[],[287,181,331,190,15,3,2])).
% 60.02/60.11 cnf(346,plain,
% 60.02/60.11 (E(f2(f2(f2(x3461,a1),f2(x3462,a1)),f2(a4,x3463)),f2(x3464,a1))),
% 60.02/60.11 inference(scs_inference,[],[342,2])).
% 60.02/60.11 cnf(347,plain,
% 60.02/60.11 (P1(f2(f2(x3471,a1),x3472),f2(f2(f2(x3473,a1),f2(x3474,a1)),f2(a4,x3475)))),
% 60.02/60.11 inference(scs_inference,[],[342,10,2,7])).
% 60.02/60.11 cnf(349,plain,
% 60.02/60.11 (E(f2(f2(x3491,a1),f2(a4,x3492)),f2(f2(f2(x3493,a1),f2(x3494,a1)),f2(a4,x3495)))),
% 60.02/60.11 inference(scs_inference,[],[342,344,10,2,7,3])).
% 60.02/60.11 cnf(352,plain,
% 60.02/60.11 (E(f2(f2(f2(x3521,a1),f2(x3522,a1)),f2(a4,x3523)),f2(f2(x3524,a1),f2(a4,x3525)))),
% 60.02/60.11 inference(scs_inference,[],[349,2])).
% 60.02/60.11 cnf(353,plain,
% 60.02/60.11 (P1(f2(f2(x3531,a1),x3532),f2(x3533,a1))),
% 60.02/60.11 inference(scs_inference,[],[346,349,347,2,7])).
% 60.02/60.11 cnf(355,plain,
% 60.02/60.11 (E(f2(f2(x3551,a1),f2(a4,x3552)),f2(x3553,a1))),
% 60.02/60.11 inference(scs_inference,[],[346,349,347,2,7,3])).
% 60.02/60.11 cnf(363,plain,
% 60.02/60.11 (E(f2(x3631,a1),f2(f2(x3632,a1),f2(a4,x3633)))),
% 60.02/60.11 inference(scs_inference,[],[355,2])).
% 60.02/60.11 cnf(364,plain,
% 60.02/60.11 (~E(f2(f2(x3641,a1),x3642),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[355,243,353,2,6])).
% 60.02/60.11 cnf(365,plain,
% 60.02/60.11 (P1(f2(f2(x3651,a1),x3652),f2(x3653,a1))),
% 60.02/60.11 inference(rename_variables,[],[353])).
% 60.02/60.11 cnf(366,plain,
% 60.02/60.11 (E(f2(x3661,a1),f2(f2(x3662,a1),f2(f2(x3663,a1),f2(a4,x3664))))),
% 60.02/60.11 inference(scs_inference,[],[355,243,353,365,198,2,6,15])).
% 60.02/60.11 cnf(377,plain,
% 60.02/60.11 (E(f2(f2(x3771,a1),f2(f2(x3772,a1),f2(a4,x3773))),f2(x3774,a1))),
% 60.02/60.11 inference(scs_inference,[],[366,2])).
% 60.02/60.11 cnf(382,plain,
% 60.02/60.11 (P1(f2(f2(x3821,a1),x3822),f2(f2(x3823,a1),f2(x3824,a1)))),
% 60.02/60.11 inference(scs_inference,[],[366,309,364,347,61,2,15,7])).
% 60.02/60.11 cnf(402,plain,
% 60.02/60.11 (E(f2(f2(x4021,a1),f2(x4022,a1)),f2(f2(f2(x4023,a1),f2(x4024,a1)),f2(a4,x4025)))),
% 60.02/60.11 inference(scs_inference,[],[260,342,3])).
% 60.02/60.11 cnf(405,plain,
% 60.02/60.11 (E(f2(f2(f2(x4051,a1),f2(x4052,a1)),f2(a4,x4053)),f2(f2(x4054,a1),f2(x4055,a1)))),
% 60.02/60.11 inference(scs_inference,[],[260,342,3,2])).
% 60.02/60.11 cnf(407,plain,
% 60.02/60.11 (E(f2(f2(x4071,a1),a4),f2(x4072,a1))),
% 60.02/60.11 inference(scs_inference,[],[96,377,3])).
% 60.02/60.11 cnf(414,plain,
% 60.02/60.11 (E(f2(f2(x4141,a1),f2(a4,x4142)),f2(f2(x4143,a1),a4))),
% 60.02/60.11 inference(scs_inference,[],[363,407,3,2])).
% 60.02/60.11 cnf(432,plain,
% 60.02/60.11 (E(f2(f2(x4321,a1),a4),f2(f2(f2(x4322,a1),f2(x4323,a1)),f2(a4,x4324)))),
% 60.02/60.11 inference(scs_inference,[],[352,414,3,2])).
% 60.02/60.11 cnf(434,plain,
% 60.02/60.11 (P1(f2(f2(x4341,a4),f2(a1,a4)),f2(f2(f2(x4342,a1),f2(x4343,a1)),f2(a4,x4344)))),
% 60.02/60.11 inference(scs_inference,[],[432,11,7])).
% 60.02/60.11 cnf(439,plain,
% 60.02/60.11 (E(f2(f2(x4391,a4),f2(a1,a4)),f2(f2(f2(x4392,a1),f2(x4393,a1)),f2(a4,x4394)))+~P1(f2(f2(f2(x4392,a1),f2(x4393,a1)),f2(a4,x4394)),f2(f2(x4391,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[432,405,11,7,3,2,15])).
% 60.02/60.11 cnf(441,plain,
% 60.02/60.11 (E(f2(f2(x4411,a4),f2(a1,a4)),f2(f2(f2(x4412,a1),f2(x4413,a1)),f2(a4,x4414)))),
% 60.02/60.11 inference(scs_inference,[],[41,334,439,6])).
% 60.02/60.11 cnf(442,plain,
% 60.02/60.11 (E(f2(f2(f2(x4421,a1),f2(x4422,a1)),f2(a4,x4423)),f2(f2(x4424,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[441,2])).
% 60.02/60.11 cnf(447,plain,
% 60.02/60.11 (P1(f2(f2(x4471,a1),x4472),a4)),
% 60.02/60.11 inference(scs_inference,[],[55,441,382,237,10,2,15,7])).
% 60.02/60.11 cnf(449,plain,
% 60.02/60.11 (E(f2(f2(f2(a4,x4491),x4492),x4493),a4)),
% 60.02/60.11 inference(rename_variables,[],[55])).
% 60.02/60.11 cnf(450,plain,
% 60.02/60.11 (E(f2(f2(x4501,a4),f2(a1,a4)),a4)),
% 60.02/60.11 inference(scs_inference,[],[55,449,441,382,237,10,2,15,7,3])).
% 60.02/60.11 cnf(454,plain,
% 60.02/60.11 (P1(f2(x4541,a4),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[450,14])).
% 60.02/60.11 cnf(456,plain,
% 60.02/60.11 (E(a4,f2(f2(x4561,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[450,14,2])).
% 60.02/60.11 cnf(457,plain,
% 60.02/60.11 (E(f2(f2(x4571,a1),x4572),a4)),
% 60.02/60.11 inference(scs_inference,[],[450,9,447,14,2,15])).
% 60.02/60.11 cnf(460,plain,
% 60.02/60.11 (P1(f2(f2(f2(x4601,a1),f2(x4602,a1)),x4603),a4)),
% 60.02/60.11 inference(scs_inference,[],[18,450,203,9,447,14,2,15,7])).
% 60.02/60.11 cnf(466,plain,
% 60.02/60.11 (P1(f2(x4661,a1),x4662)),
% 60.02/60.11 inference(scs_inference,[],[457,14])).
% 60.02/60.11 cnf(468,plain,
% 60.02/60.11 (E(a4,f2(f2(x4681,a1),x4682))),
% 60.02/60.11 inference(scs_inference,[],[457,14,2])).
% 60.02/60.11 cnf(469,plain,
% 60.02/60.11 (E(f2(f2(f2(x4691,a1),f2(x4692,a1)),x4693),a4)),
% 60.02/60.11 inference(scs_inference,[],[457,9,460,14,2,15])).
% 60.02/60.11 cnf(472,plain,
% 60.02/60.11 (P1(f2(x4721,a4),f2(a1,f2(a4,x4722)))),
% 60.02/60.11 inference(scs_inference,[],[457,174,9,454,460,14,2,15,7])).
% 60.02/60.11 cnf(474,plain,
% 60.02/60.11 (E(f2(x4741,a1),f2(f2(x4742,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[98,457,456,174,9,454,460,14,2,15,7,3])).
% 60.02/60.11 cnf(476,plain,
% 60.02/60.11 (P1(f2(f2(x4761,a1),f2(x4762,a1)),x4763)),
% 60.02/60.11 inference(scs_inference,[],[469,14])).
% 60.02/60.11 cnf(478,plain,
% 60.02/60.11 (E(f2(f2(x4781,a4),f2(a1,a4)),f2(x4782,a1))),
% 60.02/60.11 inference(scs_inference,[],[474,469,14,2])).
% 60.02/60.11 cnf(483,plain,
% 60.02/60.11 (P1(f2(f2(x4831,a4),f2(a1,a4)),a4)),
% 60.02/60.11 inference(scs_inference,[],[55,474,469,222,466,434,14,2,15,7])).
% 60.02/60.11 cnf(486,plain,
% 60.02/60.11 (E(f2(f2(a4,x4861),x4862),f2(f2(x4863,a1),x4864))),
% 60.02/60.11 inference(scs_inference,[],[36,55,474,469,468,222,466,434,14,2,15,7,3])).
% 60.02/60.11 cnf(489,plain,
% 60.02/60.11 (E(f2(f2(x4891,a1),x4892),f2(f2(a4,x4893),x4894))),
% 60.02/60.11 inference(scs_inference,[],[486,2])).
% 60.02/60.11 cnf(495,plain,
% 60.02/60.11 (E(f2(f2(x4951,a1),f2(x4952,a1)),f2(f2(x4953,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[486,442,402,468,364,476,483,2,15,7,3])).
% 60.02/60.11 cnf(505,plain,
% 60.02/60.11 (E(f2(f2(x5051,a1),x5052),f2(f2(x5053,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[489,495,96,248,466,454,2,15,7,3])).
% 60.02/60.11 cnf(509,plain,
% 60.02/60.11 (E(f2(f2(x5091,a4),f2(a1,a4)),f2(f2(x5092,a1),x5093))),
% 60.02/60.11 inference(scs_inference,[],[505,2])).
% 60.02/60.11 cnf(518,plain,
% 60.02/60.11 (E(f2(f2(x5181,a4),f2(a1,a4)),f2(a4,x5182))),
% 60.02/60.11 inference(scs_inference,[],[469,478,336,468,447,2,7,3])).
% 60.02/60.11 cnf(521,plain,
% 60.02/60.11 (E(f2(x5211,a4),f2(a1,f2(a4,x5212)))+~P1(f2(a1,f2(a4,x5212)),f2(x5211,a4))),
% 60.02/60.11 inference(scs_inference,[],[469,478,336,468,472,447,2,7,3,15])).
% 60.02/60.11 cnf(572,plain,
% 60.02/60.11 (~E(a1,f2(x5721,a4))+E(f2(x5721,a4),f2(a1,f2(a4,x5722)))),
% 60.02/60.11 inference(scs_inference,[],[8,521,7])).
% 60.02/60.11 cnf(581,plain,
% 60.02/60.11 (P1(f2(f2(f2(a4,x5811),x5812),x5813),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[75,454,6])).
% 60.02/60.11 cnf(611,plain,
% 60.02/60.11 (E(f2(x6111,a4),f2(a1,a4))+~E(a1,f2(x6111,a4))),
% 60.02/60.11 inference(scs_inference,[],[173,572,3])).
% 60.02/60.11 cnf(617,plain,
% 60.02/60.11 (~E(a4,a1)),
% 60.02/60.11 inference(scs_inference,[],[102,9,6])).
% 60.02/60.11 cnf(619,plain,
% 60.02/60.11 (~E(f2(x6191,a1),a1)),
% 60.02/60.11 inference(scs_inference,[],[102,466,6])).
% 60.02/60.11 cnf(621,plain,
% 60.02/60.11 (~E(f2(x6211,a4),a1)+E(f2(x6211,a4),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[611,2])).
% 60.02/60.11 cnf(624,plain,
% 60.02/60.11 (~P1(a1,f2(a4,a4))+E(f2(a4,a4),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[41,621,15])).
% 60.02/60.11 cnf(625,plain,
% 60.02/60.11 (~E(f2(a3,x6251),a1)),
% 60.02/60.11 inference(scs_inference,[],[102,10,6])).
% 60.02/60.11 cnf(633,plain,
% 60.02/60.11 (~P1(a3,f2(x6331,a1))),
% 60.02/60.11 inference(scs_inference,[],[118,466,15])).
% 60.02/60.11 cnf(642,plain,
% 60.02/60.11 (P1(f2(x6421,f2(a4,x6422)),f2(a1,f2(a4,x6423)))),
% 60.02/60.11 inference(scs_inference,[],[174,472,6])).
% 60.02/60.11 cnf(647,plain,
% 60.02/60.11 (E(f2(f2(x6471,x6472),f2(a4,x6473)),f2(a1,f2(a4,x6474)))+~P1(f2(a1,f2(a4,x6474)),f2(f2(x6471,x6472),f2(a4,x6473)))),
% 60.02/60.11 inference(scs_inference,[],[174,472,11,6,7,15])).
% 60.02/60.11 cnf(654,plain,
% 60.02/60.11 (P1(f2(x6541,f2(a4,x6542)),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[174,454,6])).
% 60.02/60.11 cnf(672,plain,
% 60.02/60.11 (~E(f2(a4,x6721),f2(a3,a3))),
% 60.02/60.11 inference(scs_inference,[],[234,41,6])).
% 60.02/60.11 cnf(679,plain,
% 60.02/60.11 (~P1(f2(a3,a3),f2(x6791,a1))),
% 60.02/60.11 inference(scs_inference,[],[237,466,15])).
% 60.02/60.11 cnf(708,plain,
% 60.02/60.11 (E(f2(a4,a4),f2(a1,a4))+~E(f2(a1,f2(a4,a4)),a4)),
% 60.02/60.11 inference(scs_inference,[],[624,14])).
% 60.02/60.11 cnf(709,plain,
% 60.02/60.11 (E(f2(a1,a4),f2(a4,a4))+~E(f2(a1,f2(a4,a4)),a4)),
% 60.02/60.11 inference(scs_inference,[],[708,2])).
% 60.02/60.11 cnf(714,plain,
% 60.02/60.11 (P1(f2(f2(x7141,a4),f2(a1,a4)),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[442,581,6])).
% 60.02/60.11 cnf(718,plain,
% 60.02/60.11 (P1(f2(f2(x7181,a4),f2(a1,a4)),f2(a1,f2(a4,x7182)))),
% 60.02/60.11 inference(scs_inference,[],[442,642,6])).
% 60.02/60.11 cnf(720,plain,
% 60.02/60.11 (E(f2(f2(x7201,a4),f2(a1,a4)),f2(a1,a4))+~P1(f2(a1,a4),f2(f2(x7201,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[442,642,714,6,15])).
% 60.02/60.11 cnf(723,plain,
% 60.02/60.11 (E(f2(a1,a4),f2(f2(x7231,a4),f2(a1,a4)))+~P1(f2(a1,a4),f2(f2(x7231,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[442,642,714,6,15,3,2])).
% 60.02/60.11 cnf(726,plain,
% 60.02/60.11 (E(f2(f2(x7261,a4),f2(a1,a4)),f2(a1,f2(a4,x7262)))+~P1(f2(a1,f2(a4,x7262)),f2(f2(x7261,a4),f2(a1,a4)))),
% 60.02/60.11 inference(scs_inference,[],[718,15])).
% 60.02/60.11 cnf(732,plain,
% 60.02/60.11 (E(f2(f2(x7321,a4),f2(a1,a4)),f2(a1,a4))+~E(f2(f2(a1,a4),f2(f2(x7321,a4),f2(a1,a4))),a4)),
% 60.02/60.11 inference(scs_inference,[],[720,14])).
% 60.02/60.11 cnf(749,plain,
% 60.02/60.11 (~E(a4,f2(f2(a1,a4),f2(f2(x7491,a4),f2(a1,a4))))+E(f2(f2(x7491,a4),f2(a1,a4)),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[732,2])).
% 60.02/60.11 cnf(751,plain,
% 60.02/60.11 (P1(f2(f2(x7511,x7512),f2(a1,x7512)),a4)),
% 60.02/60.11 inference(scs_inference,[],[457,11,7])).
% 60.02/60.11 cnf(761,plain,
% 60.02/60.11 (~E(a4,f2(f2(a1,a4),a4))+E(f2(f2(a4,a4),f2(a1,a4)),f2(a1,a4))),
% 60.02/60.11 inference(scs_inference,[],[96,749,3])).
% 60.02/60.11 cnf(763,plain,
% 60.02/60.11 (P1(f2(f2(x7631,x7632),f2(a1,x7632)),f2(f2(x7633,a1),x7634))),
% 60.02/60.11 inference(scs_inference,[],[468,234,751,6,7])).
% 60.02/60.11 cnf(764,plain,
% 60.02/60.11 (E(f2(x7641,a1),f2(a1,a4))+~E(a4,f2(f2(a1,a4),a4))),
% 60.02/60.11 inference(scs_inference,[],[474,761,3])).
% 60.12/60.11 cnf(765,plain,
% 60.12/60.11 (~E(f2(f2(a1,a4),a4),a4)+E(f2(x7651,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[764,2])).
% 60.12/60.12 cnf(771,plain,
% 60.12/60.12 (E(f2(f2(x7711,a4),f2(a1,a4)),f2(a1,a4))+~E(f2(f2(a1,a4),a4),a4)),
% 60.12/60.12 inference(scs_inference,[],[509,765,3])).
% 60.12/60.12 cnf(772,plain,
% 60.12/60.12 (~P1(f2(a1,a4),a4)+E(f2(f2(x7721,a4),f2(a1,a4)),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[771,13])).
% 60.12/60.12 cnf(773,plain,
% 60.12/60.12 (E(f2(x7731,a1),f2(a1,a4))+~P1(f2(a1,a4),a4)),
% 60.12/60.12 inference(scs_inference,[],[474,772,3])).
% 60.12/60.12 cnf(774,plain,
% 60.12/60.12 (P1(f2(f2(x7741,x7742),f2(a1,x7742)),f2(f2(x7743,a4),f2(a1,a4)))),
% 60.12/60.12 inference(scs_inference,[],[474,763,7])).
% 60.12/60.12 cnf(777,plain,
% 60.12/60.12 (~E(f2(a4,x7771),f2(a1,a4))+E(f2(x7772,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[41,773,6])).
% 60.12/60.12 cnf(792,plain,
% 60.12/60.12 (E(f2(f2(a4,x7921),x7922),f2(f2(x7923,a1),x7924))),
% 60.12/60.12 inference(rename_variables,[],[486])).
% 60.12/60.12 cnf(793,plain,
% 60.12/60.12 (E(f2(f2(x7931,a1),x7932),f2(a1,f2(a4,x7933)))+~P1(f2(a1,f2(a4,x7933)),f2(f2(x7931,a1),x7932))),
% 60.12/60.12 inference(scs_inference,[],[486,472,6,15])).
% 60.12/60.12 cnf(795,plain,
% 60.12/60.12 (E(f2(f2(a4,x7951),x7952),f2(a1,f2(a4,x7953)))+~P1(f2(a1,f2(a4,x7953)),f2(f2(x7954,a1),x7955))),
% 60.12/60.12 inference(scs_inference,[],[486,792,472,6,15,3])).
% 60.12/60.12 cnf(823,plain,
% 60.12/60.12 (E(f2(a4,x8231),f2(f2(x8232,x8233),f2(a1,x8233)))),
% 60.12/60.12 inference(scs_inference,[],[518,41,774,7,15,2])).
% 60.12/60.12 cnf(873,plain,
% 60.12/60.12 (~P1(a1,a4)),
% 60.12/60.12 inference(scs_inference,[],[617,8,15])).
% 60.12/60.12 cnf(877,plain,
% 60.12/60.12 (~E(f2(a1,f2(a4,x8771)),a4)+E(f2(x8772,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[472,773,7])).
% 60.12/60.12 cnf(879,plain,
% 60.12/60.12 (~E(a4,f2(a1,f2(a4,x8791)))+E(f2(x8792,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[877,2])).
% 60.12/60.12 cnf(881,plain,
% 60.12/60.12 (~E(a4,f2(a1,a4))+E(f2(x8811,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[174,879,3])).
% 60.12/60.12 cnf(882,plain,
% 60.12/60.12 (E(f2(f2(x8821,a4),f2(a1,a4)),f2(a1,a4))+~E(a4,f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[509,881,3])).
% 60.12/60.12 cnf(883,plain,
% 60.12/60.12 (~P1(a1,f2(x8831,a1))),
% 60.12/60.12 inference(scs_inference,[],[619,8,15])).
% 60.12/60.12 cnf(886,plain,
% 60.12/60.12 (~E(f2(a1,a4),a4)+E(f2(f2(x8861,a4),f2(a1,a4)),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[882,2])).
% 60.12/60.12 cnf(887,plain,
% 60.12/60.12 (E(f2(f2(x8871,a1),x8872),f2(a1,a4))+~E(f2(a1,a4),a4)),
% 60.12/60.12 inference(scs_inference,[],[505,886,3])).
% 60.12/60.12 cnf(893,plain,
% 60.12/60.12 (~P1(a1,f2(a3,x8931))),
% 60.12/60.12 inference(scs_inference,[],[625,8,15])).
% 60.12/60.12 cnf(899,plain,
% 60.12/60.12 (~E(f2(a1,a4),a4)+E(f2(x8991,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[881,2])).
% 60.12/60.12 cnf(900,plain,
% 60.12/60.12 (~E(f2(a1,a4),f2(f2(a4,x9001),x9002))+E(f2(x9003,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[36,899,3])).
% 60.12/60.12 cnf(901,plain,
% 60.12/60.12 (~P1(f2(a1,a4),f2(f2(a4,a4),f2(a1,a4)))+E(f2(x9011,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[900,723])).
% 60.12/60.12 cnf(902,plain,
% 60.12/60.12 (E(f2(x9021,a1),f2(a1,a4))+~E(f2(f2(a1,a4),f2(f2(a4,a4),f2(a1,a4))),a4)),
% 60.12/60.12 inference(scs_inference,[],[901,14])).
% 60.12/60.12 cnf(903,plain,
% 60.12/60.12 (E(f2(f2(a4,x9031),x9032),f2(a1,a4))+~E(f2(f2(a1,a4),f2(f2(a4,a4),f2(a1,a4))),a4)),
% 60.12/60.12 inference(scs_inference,[],[46,902,3])).
% 60.12/60.12 cnf(904,plain,
% 60.12/60.12 (~P1(f2(a1,a4),f2(f2(a4,a4),f2(a1,a4)))+E(f2(f2(a4,x9041),x9042),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[903,13])).
% 60.12/60.12 cnf(918,plain,
% 60.12/60.12 (~P1(f2(a3,a3),f2(a4,x9181))),
% 60.12/60.12 inference(scs_inference,[],[672,41,15])).
% 60.12/60.12 cnf(1190,plain,
% 60.12/60.12 (E(f2(a1,a4),a4)+~E(f2(a1,f2(a4,a4)),a4)),
% 60.12/60.12 inference(scs_inference,[],[18,709,3])).
% 60.12/60.12 cnf(1191,plain,
% 60.12/60.12 (~P1(f2(a1,f2(a4,a4)),a4)+E(f2(a1,a4),a4)),
% 60.12/60.12 inference(scs_inference,[],[9,1190,15])).
% 60.12/60.12 cnf(1196,plain,
% 60.12/60.12 (~P1(f2(a1,f2(a4,a4)),a4)),
% 60.12/60.12 inference(scs_inference,[],[873,1191,14])).
% 60.12/60.12 cnf(1215,plain,
% 60.12/60.12 (~E(f2(f2(a1,a4),a4),f2(x12151,a1))+E(f2(x12152,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[98,765,3])).
% 60.12/60.12 cnf(1216,plain,
% 60.12/60.12 (E(f2(x12161,a1),f2(a1,f2(a4,x12162)))+~E(f2(f2(a1,a4),a4),f2(x12163,a1))),
% 60.12/60.12 inference(scs_inference,[],[174,1215,3])).
% 60.12/60.12 cnf(1217,plain,
% 60.12/60.12 (~E(f2(x12171,a1),f2(f2(a1,a4),a4))+E(f2(x12172,a1),f2(a1,f2(a4,x12173)))),
% 60.12/60.12 inference(scs_inference,[],[1216,2])).
% 60.12/60.12 cnf(1243,plain,
% 60.12/60.12 (~P1(f2(a1,a4),f2(a4,x12431))+E(f2(x12432,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[41,777,15])).
% 60.12/60.12 cnf(1250,plain,
% 60.12/60.12 (~E(f2(a1,f2(a4,x12501)),f2(f2(a4,x12502),x12503))+E(f2(x12504,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[36,877,3])).
% 60.12/60.12 cnf(1251,plain,
% 60.12/60.12 (E(f2(x12511,a1),f2(a1,f2(a4,x12512)))+~E(f2(a1,f2(a4,x12513)),f2(f2(a4,x12514),x12515))),
% 60.12/60.12 inference(scs_inference,[],[174,1250,3])).
% 60.12/60.12 cnf(1252,plain,
% 60.12/60.12 (~E(f2(f2(a4,x12521),x12522),f2(a1,f2(a4,x12523)))+E(f2(x12524,a1),f2(a1,f2(a4,x12525)))),
% 60.12/60.12 inference(scs_inference,[],[1251,2])).
% 60.12/60.12 cnf(1280,plain,
% 60.12/60.12 (~P1(f2(a1,a4),a4)+E(f2(f2(x12801,a1),x12802),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[9,887,15])).
% 60.12/60.12 cnf(1281,plain,
% 60.12/60.12 (E(f2(f2(x12811,a1),x12812),f2(a1,a4))+~E(f2(f2(a1,a4),a4),a4)),
% 60.12/60.12 inference(scs_inference,[],[1280,14])).
% 60.12/60.12 cnf(1285,plain,
% 60.12/60.12 (~E(a4,f2(f2(a1,a4),a4))+E(f2(f2(x12851,a1),x12852),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[1281,2])).
% 60.12/60.12 cnf(1321,plain,
% 60.12/60.12 (~E(f2(a4,x13211),f2(a1,f2(a4,a4)))),
% 60.12/60.12 inference(scs_inference,[],[1196,41,6])).
% 60.12/60.12 cnf(1327,plain,
% 60.12/60.12 (~E(f2(x13271,a1),f2(f2(a1,a4),a4))),
% 60.12/60.12 inference(scs_inference,[],[1321,1217])).
% 60.12/60.12 cnf(1331,plain,
% 60.12/60.12 (~E(f2(f2(a4,x13311),x13312),f2(a1,f2(a4,x13313)))),
% 60.12/60.12 inference(scs_inference,[],[1321,1252])).
% 60.12/60.12 cnf(1335,plain,
% 60.12/60.12 (~E(f2(f2(a4,x13351),x13352),f2(a1,f2(a4,x13353)))),
% 60.12/60.12 inference(rename_variables,[],[1331])).
% 60.12/60.12 cnf(1338,plain,
% 60.12/60.12 (~E(f2(f2(a4,x13381),x13382),f2(a1,f2(a4,x13383)))),
% 60.12/60.12 inference(rename_variables,[],[1331])).
% 60.12/60.12 cnf(1341,plain,
% 60.12/60.12 (~E(f2(f2(a4,x13411),x13412),f2(a1,f2(a4,x13413)))),
% 60.12/60.12 inference(rename_variables,[],[1331])).
% 60.12/60.12 cnf(1346,plain,
% 60.12/60.12 (P1(f2(x13461,a1),x13462)),
% 60.12/60.12 inference(rename_variables,[],[466])).
% 60.12/60.12 cnf(1347,plain,
% 60.12/60.12 (~P1(f2(f2(a1,a4),a4),f2(x13471,a1))),
% 60.12/60.12 inference(scs_inference,[],[1196,1327,1331,1335,1338,1341,466,1346,647,793,726,795,6,15])).
% 60.12/60.12 cnf(1350,plain,
% 60.12/60.12 (~E(f2(f2(a4,x13501),x13502),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[1196,174,1327,1331,1335,1338,1341,466,1346,647,793,726,795,6,15,3])).
% 60.12/60.12 cnf(1354,plain,
% 60.12/60.12 (~P1(f2(a1,a4),f2(f2(a4,a4),f2(a1,a4)))),
% 60.12/60.12 inference(scs_inference,[],[1196,174,1327,1331,1335,1338,1341,466,1346,647,793,726,795,6,15,3,772,904])).
% 60.12/60.12 cnf(1372,plain,
% 60.12/60.12 (~E(f2(a4,x13721),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[1350,777])).
% 60.12/60.12 cnf(1391,plain,
% 60.12/60.12 (~P1(f2(a1,a4),f2(a4,x13911))),
% 60.12/60.12 inference(scs_inference,[],[1350,1243])).
% 60.12/60.12 cnf(1408,plain,
% 60.12/60.12 (~E(a4,f2(f2(a1,a4),a4))),
% 60.12/60.12 inference(scs_inference,[],[1350,1285])).
% 60.12/60.12 cnf(1449,plain,
% 60.12/60.12 (~E(a4,f2(f2(a1,a4),f2(a4,x14491)))),
% 60.12/60.12 inference(scs_inference,[],[1408,173,3])).
% 60.12/60.12 cnf(1453,plain,
% 60.12/60.12 (~E(f2(x14531,a1),f2(a1,a4))),
% 60.12/60.12 inference(scs_inference,[],[1354,466,6])).
% 60.12/60.12 cnf(1514,plain,
% 60.12/60.12 (~E(f2(a4,x15141),f2(f2(a1,a4),a4))),
% 60.12/60.12 inference(scs_inference,[],[1347,41,6])).
% 60.12/60.12 cnf(1607,plain,
% 60.12/60.12 (~P1(f2(f2(a1,a4),f2(a4,x16071)),a4)),
% 60.12/60.12 inference(scs_inference,[],[1449,9,15])).
% 60.12/60.12 cnf(1610,plain,
% 60.12/60.12 (~P1(f2(a1,a4),f2(x16101,a1))),
% 60.12/60.12 inference(scs_inference,[],[1453,466,15])).
% 60.12/60.12 cnf(1656,plain,
% 60.12/60.12 (~P1(f2(f2(a1,a4),a4),f2(a4,x16561))),
% 60.12/60.12 inference(scs_inference,[],[1514,41,15])).
% 60.12/60.12 cnf(1850,plain,
% 60.12/60.12 (E(f2(x18501,a4),f2(x18501,f2(x18502,a1)))),
% 60.12/60.12 inference(scs_inference,[],[98,2,5])).
% 60.12/60.12 cnf(1851,plain,
% 60.12/60.12 (E(f2(x18511,f2(x18512,a1)),f2(x18511,a4))),
% 60.12/60.12 inference(scs_inference,[],[1850,2])).
% 60.12/60.12 cnf(1939,plain,
% 60.12/60.12 (~E(f2(x19391,a1),f2(f2(a1,a4),f2(x19392,a1)))),
% 60.12/60.12 inference(scs_inference,[],[1327,1851,3])).
% 60.12/60.12 cnf(1955,plain,
% 60.12/60.12 (~E(f2(a4,x19551),f2(a1,f2(x19552,a1)))),
% 60.12/60.12 inference(scs_inference,[],[1372,1851,3])).
% 60.12/60.12 cnf(1990,plain,
% 60.12/60.12 (E(f2(f2(x19901,f2(a4,x19902)),f2(a1,a4)),a4)),
% 60.12/60.12 inference(scs_inference,[],[654,13])).
% 60.12/60.12 cnf(1992,plain,
% 60.12/60.12 (E(f2(x19921,f2(a4,x19922)),f2(x19921,f2(x19923,a1)))),
% 60.12/60.12 inference(scs_inference,[],[317,654,13,5])).
% 60.12/60.12 cnf(1996,plain,
% 60.12/60.12 (~P1(f2(a1,f2(x19961,a1)),f2(x19962,a1))),
% 60.12/60.12 inference(scs_inference,[],[1610,1939,317,654,1851,13,5,14,2,6])).
% 60.12/60.12 cnf(2003,plain,
% 60.12/60.12 (E(f2(f2(x20031,x20032),x20031),a4)),
% 60.12/60.12 inference(scs_inference,[],[10,13])).
% 60.12/60.12 cnf(2005,plain,
% 60.12/60.12 (E(f2(x20051,f2(x20052,a1)),f2(x20051,f2(x20053,a1)))),
% 60.12/60.12 inference(scs_inference,[],[324,10,13,5])).
% 60.12/60.12 cnf(2009,plain,
% 60.12/60.12 (~P1(f2(f2(a1,a4),f2(x20091,a1)),f2(a4,x20092))),
% 60.12/60.12 inference(scs_inference,[],[883,1656,1955,324,1851,10,13,5,14,2,6])).
% 60.12/60.12 cnf(2026,plain,
% 60.12/60.12 (~E(f2(f2(f2(a1,a4),f2(x20261,a1)),f2(a4,x20262)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2009,14])).
% 60.12/60.12 cnf(2053,plain,
% 60.12/60.12 (~E(f2(f2(a1,f2(x20531,a1)),f2(x20532,a1)),a4)),
% 60.12/60.12 inference(scs_inference,[],[1996,14])).
% 60.12/60.12 cnf(2065,plain,
% 60.12/60.12 (~E(f2(f2(a3,a3),f2(x20651,a1)),a4)),
% 60.12/60.12 inference(scs_inference,[],[679,14])).
% 60.12/60.12 cnf(2068,plain,
% 60.12/60.12 (~E(a4,f2(f2(a3,a3),f2(x20681,a1)))),
% 60.12/60.12 inference(scs_inference,[],[2065,2])).
% 60.12/60.12 cnf(2069,plain,
% 60.12/60.12 (~E(f2(f2(a3,a3),f2(a4,x20691)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2065,918,2,14])).
% 60.12/60.12 cnf(2072,plain,
% 60.12/60.12 (~E(f2(a3,f2(x20721,a1)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2069,633,2,14])).
% 60.12/60.12 cnf(2074,plain,
% 60.12/60.12 (~P1(f2(f2(a1,a4),f2(x20741,a1)),a4)),
% 60.12/60.12 inference(scs_inference,[],[1607,2069,633,2005,2,14,6])).
% 60.12/60.12 cnf(2078,plain,
% 60.12/60.12 (~E(f2(a1,f2(a3,x20781)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2072,893,2,14])).
% 60.12/60.12 cnf(2081,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),f2(x20811,a1)),a4)),
% 60.12/60.12 inference(scs_inference,[],[9,2074,2068,2072,893,2003,2,14,7,15])).
% 60.12/60.12 cnf(2084,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),f2(a4,x20841)),a4)),
% 60.12/60.12 inference(scs_inference,[],[9,2074,2068,2072,893,1992,2003,2,14,7,15,6])).
% 60.12/60.12 cnf(2090,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),a4),a4)),
% 60.12/60.12 inference(scs_inference,[],[2081,2078,1656,1990,1850,873,2,14,7,6])).
% 60.12/60.12 cnf(2096,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),a4),f2(f2(x20961,x20962),x20961))),
% 60.12/60.12 inference(scs_inference,[],[2090,2026,1391,2003,2,14,7])).
% 60.12/60.12 cnf(2101,plain,
% 60.12/60.12 (~E(f2(a3,f2(a4,x21011)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2053,81,2,14])).
% 60.12/60.12 cnf(2103,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),a4),f2(a4,x21031))),
% 60.12/60.12 inference(scs_inference,[],[2096,2053,823,81,2,14,7])).
% 60.12/60.12 cnf(2109,plain,
% 60.12/60.12 (~E(f2(f2(f2(a3,a3),a4),f2(a4,x21091)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2103,2101,2,14])).
% 60.12/60.12 cnf(2111,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),a4),f2(x21111,a1))),
% 60.12/60.12 inference(scs_inference,[],[2103,2101,324,2,14,7])).
% 60.12/60.12 cnf(2113,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),a4),f2(a4,x21131))),
% 60.12/60.12 inference(rename_variables,[],[2103])).
% 60.12/60.12 cnf(2114,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),f2(a4,x21141)),f2(a4,x21142))),
% 60.12/60.12 inference(scs_inference,[],[2103,2113,2101,324,173,2,14,7,6])).
% 60.12/60.12 cnf(2120,plain,
% 60.12/60.12 (~E(f2(f2(f2(a3,a3),a4),f2(x21201,a1)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2111,2109,2,14])).
% 60.12/60.12 cnf(2123,plain,
% 60.12/60.12 (~P1(f2(f2(a3,a3),f2(x21231,a1)),f2(a4,x21232))),
% 60.12/60.12 inference(scs_inference,[],[2111,2114,2109,2005,1990,31,2,14,7,6])).
% 60.12/60.12 cnf(2127,plain,
% 60.12/60.12 (~E(f2(f2(f2(a3,a3),f2(x21271,a1)),f2(a4,x21272)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2123,2120,2,14])).
% 60.12/60.12 cnf(2136,plain,
% 60.12/60.12 (~E(f2(f2(f2(a3,a3),f2(a4,x21361)),f2(a4,x21362)),a4)),
% 60.12/60.12 inference(scs_inference,[],[2127,2114,2,14])).
% 60.12/60.12 cnf(2145,plain,
% 60.12/60.12 ($false),
% 60.12/60.12 inference(scs_inference,[],[2084,2136,84,2003,11,2,14,7]),
% 60.12/60.12 ['proof']).
% 60.12/60.12 % SZS output end Proof
% 60.12/60.12 % Total time :59.410000s
%------------------------------------------------------------------------------