%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN008-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 : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 07:26:50 EDT 2024
% Result : Unsatisfiable 60.90s 61.00s
% Output : CNFRefutation 61.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HEN008-3 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n022.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:23:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.44/0.58 start to proof:theBenchmark
% 60.90/60.99 %-------------------------------------------
% 60.90/60.99 % File :CSE---1.7
% 60.90/60.99 % Problem :theBenchmark
% 60.90/60.99 % Transform :cnf
% 60.90/60.99 % Format :tptp:raw
% 60.90/60.99 % Command :java -jar mcs_scs.jar %d %s
% 60.90/60.99
% 60.90/60.99 % Result :Theorem 60.370000s
% 60.90/60.99 % Output :CNFRefutation 60.370000s
% 60.90/60.99 %-------------------------------------------
% 60.90/61.00 %--------------------------------------------------------------------------
% 60.90/61.00 % File : HEN008-3 : TPTP v8.2.0. Released v1.0.0.
% 60.90/61.00 % Domain : Henkin Models
% 60.90/61.00 % Problem : X <= Y => X/Z <= Y/Z
% 60.90/61.00 % Version : [MOW76] axioms.
% 60.90/61.00 % English :
% 60.90/61.00
% 60.90/61.00 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 60.90/61.00 % Source : [ANL]
% 60.90/61.00 % Names : HP8 [ANL]
% 60.90/61.00
% 60.90/61.00 % Status : Unsatisfiable
% 60.90/61.00 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.00 v4.1.0, 0.11 v4.0.1, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 60.90/61.00 % Syntax : Number of clauses : 9 ( 6 unt; 0 nHn; 5 RR)
% 60.90/61.00 % Number of literals : 13 ( 3 equ; 5 neg)
% 60.90/61.00 % Maximal clause size : 3 ( 1 avg)
% 60.90/61.00 % Maximal term depth : 3 ( 1 avg)
% 60.90/61.00 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 60.90/61.00 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 60.90/61.00 % Number of variables : 13 ( 3 sgn)
% 60.90/61.00 % SPC : CNF_UNS_RFO_SEQ_HRN
% 60.90/61.00
% 60.90/61.00 % Comments :
% 60.90/61.00 %--------------------------------------------------------------------------
% 60.90/61.00 %----Include Henkin model axioms for equality formulation
% 60.90/61.00 include('Axioms/HEN002-0.ax').
% 60.90/61.00 %--------------------------------------------------------------------------
% 60.90/61.00 cnf(a_LE_b,hypothesis,
% 60.90/61.00 less_equal(a,b) ).
% 60.90/61.00
% 60.90/61.00 cnf(prove_a_divide_c_LE_b_divide_c,negated_conjecture,
% 60.90/61.00 ~ less_equal(divide(a,c),divide(b,c)) ).
% 60.90/61.00
% 60.90/61.00 %--------------------------------------------------------------------------
% 60.90/61.00 %-------------------------------------------
% 60.90/61.00 % Proof found
% 60.90/61.00 % SZS status Theorem for theBenchmark
% 60.90/61.00 % SZS output start Proof
% 60.90/61.01 %ClaNum:16(EqnAxiom:7)
% 60.90/61.01 %VarNum:26(SingletonVarNum:13)
% 60.90/61.01 %MaxLitNum:3
% 60.90/61.01 %MaxfuncDepth:2
% 60.90/61.01 %SharedTerms:9
% 60.90/61.01 %goalClause: 13
% 60.90/61.01 %singleGoalClaCount:1
% 60.90/61.01 [8]P1(a1,a2)
% 60.90/61.01 [13]~P1(f4(a1,a5),f4(a2,a5))
% 60.90/61.01 [9]P1(x91,a3)
% 60.90/61.01 [10]P1(a6,x101)
% 60.90/61.01 [11]P1(f4(x111,x112),x111)
% 60.90/61.01 [12]P1(f4(f4(x121,x122),f4(x123,x122)),f4(f4(x121,x123),x122))
% 60.90/61.01 [14]~P1(x141,x142)+E(f4(x141,x142),a6)
% 60.90/61.01 [15]P1(x151,x152)+~E(f4(x151,x152),a6)
% 60.90/61.01 [16]~P1(x162,x161)+~P1(x161,x162)+E(x161,x162)
% 60.90/61.01 %EqnAxiom
% 60.90/61.01 [1]E(x11,x11)
% 60.90/61.01 [2]E(x22,x21)+~E(x21,x22)
% 60.90/61.01 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.90/61.01 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 60.90/61.01 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 60.90/61.01 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 60.90/61.01 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 60.90/61.01
% 60.90/61.01 %-------------------------------------------
% 60.90/61.02 cnf(17,plain,
% 60.90/61.02 (~E(a6,f4(a1,a5))),
% 60.90/61.02 inference(scs_inference,[],[13,10,6])).
% 60.90/61.02 cnf(18,plain,
% 60.90/61.02 (P1(a6,x181)),
% 60.90/61.02 inference(rename_variables,[],[10])).
% 60.90/61.02 cnf(19,plain,
% 60.90/61.02 (~E(a3,f4(a2,a5))),
% 60.90/61.02 inference(scs_inference,[],[13,9,10,6,7])).
% 60.90/61.02 cnf(21,plain,
% 60.90/61.02 (~P1(f4(a1,a5),a6)),
% 60.90/61.02 inference(scs_inference,[],[13,9,10,18,6,7,16])).
% 60.90/61.02 cnf(24,plain,
% 60.90/61.02 (E(f4(a6,x241),a6)),
% 60.90/61.02 inference(scs_inference,[],[11,10,16])).
% 60.90/61.02 cnf(25,plain,
% 60.90/61.02 (P1(f4(x251,x252),x251)),
% 60.90/61.02 inference(rename_variables,[],[11])).
% 60.90/61.02 cnf(28,plain,
% 60.90/61.02 (~E(f4(f4(a2,a5),x281),f4(a1,a5))),
% 60.90/61.02 inference(scs_inference,[],[13,11,25,10,16,6])).
% 60.90/61.02 cnf(29,plain,
% 60.90/61.02 (P1(f4(x291,x292),x291)),
% 60.90/61.02 inference(rename_variables,[],[11])).
% 60.90/61.02 cnf(32,plain,
% 60.90/61.02 (E(a6,f4(a6,x321))),
% 60.90/61.02 inference(scs_inference,[],[13,11,25,29,10,16,6,7,2])).
% 60.90/61.02 cnf(34,plain,
% 60.90/61.02 (E(f4(a6,x341),f4(a6,x342))),
% 60.90/61.02 inference(scs_inference,[],[24,32,3])).
% 60.90/61.02 cnf(41,plain,
% 60.90/61.02 (E(f4(f4(x411,x412),f4(x413,x412)),f4(f4(x411,x413),x412))+~P1(f4(f4(x411,x413),x412),f4(f4(x411,x412),f4(x413,x412)))),
% 60.90/61.02 inference(scs_inference,[],[12,16])).
% 60.90/61.02 cnf(44,plain,
% 60.90/61.02 (E(f4(f4(x441,x442),x443),f4(f4(x441,x443),f4(x442,x443)))+~P1(f4(f4(x441,x442),x443),f4(f4(x441,x443),f4(x442,x443)))),
% 60.90/61.02 inference(scs_inference,[],[12,16,6,2])).
% 60.90/61.02 cnf(47,plain,
% 60.90/61.02 (P1(x471,a2)+~E(a1,x471)),
% 60.90/61.02 inference(scs_inference,[],[8,6])).
% 60.90/61.02 cnf(52,plain,
% 60.90/61.02 (P1(x521,f4(f4(x522,x523),x524))+~E(f4(f4(x522,x524),f4(x523,x524)),x521)),
% 60.90/61.02 inference(scs_inference,[],[12,6])).
% 60.90/61.02 cnf(59,plain,
% 60.90/61.02 (P1(a1,x591)+~E(a2,x591)),
% 60.90/61.02 inference(scs_inference,[],[8,7])).
% 60.90/61.02 cnf(64,plain,
% 60.90/61.02 (P1(f4(f4(x641,x642),f4(x643,x642)),x644)+~E(f4(f4(x641,x643),x642),x644)),
% 60.90/61.02 inference(scs_inference,[],[12,7])).
% 60.90/61.02 cnf(80,plain,
% 60.90/61.02 (~E(f4(a6,x801),f4(a1,a5))),
% 60.90/61.02 inference(scs_inference,[],[21,11,6])).
% 61.02/61.02 cnf(81,plain,
% 61.02/61.02 (P1(f4(x811,x812),x811)),
% 61.02/61.02 inference(rename_variables,[],[11])).
% 61.02/61.02 cnf(82,plain,
% 61.02/61.02 (~E(a1,a6)),
% 61.02/61.02 inference(scs_inference,[],[21,11,81,6,7])).
% 61.02/61.02 cnf(84,plain,
% 61.02/61.02 (~E(a6,a1)),
% 61.02/61.02 inference(scs_inference,[],[21,11,81,6,7,4])).
% 61.02/61.02 cnf(85,plain,
% 61.02/61.02 (~E(a1,f4(a6,x851))),
% 61.02/61.02 inference(scs_inference,[],[21,11,81,24,6,7,4,3])).
% 61.02/61.02 cnf(87,plain,
% 61.02/61.02 (~E(a3,a6)),
% 61.02/61.02 inference(scs_inference,[],[21,9,7])).
% 61.02/61.02 cnf(99,plain,
% 61.02/61.02 (~P1(a1,a6)),
% 61.02/61.02 inference(scs_inference,[],[84,10,16])).
% 61.02/61.02 cnf(102,plain,
% 61.02/61.02 (~E(a2,a6)),
% 61.02/61.02 inference(scs_inference,[],[84,8,10,16,7])).
% 61.02/61.02 cnf(106,plain,
% 61.02/61.02 (~E(a3,f4(a6,x1061))),
% 61.02/61.02 inference(scs_inference,[],[87,24,3])).
% 61.02/61.02 cnf(109,plain,
% 61.02/61.02 (~E(f4(a6,x1091),a1)),
% 61.02/61.02 inference(scs_inference,[],[99,11,6])).
% 61.02/61.02 cnf(113,plain,
% 61.02/61.02 (~E(a2,f4(a6,x1131))),
% 61.02/61.02 inference(scs_inference,[],[102,24,3])).
% 61.02/61.02 cnf(229,plain,
% 61.02/61.02 (E(f4(x2291,a6),f4(x2291,f4(a6,x2292)))),
% 61.02/61.02 inference(scs_inference,[],[24,2,5])).
% 61.02/61.02 cnf(230,plain,
% 61.02/61.02 (P1(f4(f4(x2301,a6),f4(x2302,a6)),f4(f4(x2301,x2302),f4(a6,x2303)))),
% 61.02/61.02 inference(scs_inference,[],[229,64])).
% 61.02/61.02 cnf(231,plain,
% 61.02/61.02 (E(f4(x2311,a6),f4(x2311,f4(a6,x2312)))),
% 61.02/61.02 inference(rename_variables,[],[229])).
% 61.02/61.02 cnf(232,plain,
% 61.02/61.02 (E(f4(x2321,f4(a6,x2322)),f4(x2321,a6))),
% 61.02/61.02 inference(scs_inference,[],[229,231,64,2])).
% 61.02/61.02 cnf(233,plain,
% 61.02/61.02 (P1(f4(f4(x2331,x2332),a6),f4(f4(x2331,a6),x2332))),
% 61.02/61.02 inference(scs_inference,[],[12,229,231,64,2,6])).
% 61.02/61.02 cnf(237,plain,
% 61.02/61.02 (E(f4(a6,x2371),f4(f4(a6,x2372),x2371))),
% 61.02/61.02 inference(scs_inference,[],[24,2,4])).
% 61.02/61.02 cnf(238,plain,
% 61.02/61.02 (E(f4(f4(a6,x2381),x2382),f4(a6,x2382))),
% 61.02/61.02 inference(scs_inference,[],[237,2])).
% 61.02/61.02 cnf(239,plain,
% 61.02/61.02 (E(a6,f4(f4(a6,x2391),x2392))),
% 61.02/61.02 inference(scs_inference,[],[32,237,2,3])).
% 61.02/61.02 cnf(241,plain,
% 61.02/61.02 (P1(f4(f4(x2411,a6),a6),f4(f4(x2411,a6),f4(a6,x2412)))),
% 61.02/61.02 inference(scs_inference,[],[230,32,232,237,2,3,6])).
% 61.02/61.02 cnf(244,plain,
% 61.02/61.02 (P1(f4(a6,f4(x2441,x2442)),f4(f4(a6,x2441),x2442))),
% 61.02/61.02 inference(scs_inference,[],[230,32,232,237,2,3,6,52])).
% 61.02/61.02 cnf(248,plain,
% 61.02/61.02 (E(f4(f4(a6,x2481),x2482),a6)),
% 61.02/61.02 inference(scs_inference,[],[239,2])).
% 61.02/61.02 cnf(249,plain,
% 61.02/61.02 (~E(a2,f4(f4(a6,x2491),x2492))),
% 61.02/61.02 inference(scs_inference,[],[113,238,239,2,3])).
% 61.02/61.02 cnf(251,plain,
% 61.02/61.02 (P1(f4(f4(x2511,x2512),f4(a6,x2513)),f4(f4(x2511,a6),x2512))),
% 61.02/61.02 inference(scs_inference,[],[113,233,229,238,239,2,3,6])).
% 61.02/61.02 cnf(252,plain,
% 61.02/61.02 (E(f4(x2521,a6),f4(x2521,f4(a6,x2522)))),
% 61.02/61.02 inference(rename_variables,[],[229])).
% 61.02/61.02 cnf(256,plain,
% 61.02/61.02 (P1(f4(a6,x2561),x2562)),
% 61.02/61.02 inference(scs_inference,[],[113,233,244,229,252,238,239,2,3,6,7,15])).
% 61.02/61.02 cnf(265,plain,
% 61.02/61.02 (~P1(f4(a1,a5),f4(a6,x2651))),
% 61.02/61.02 inference(scs_inference,[],[256,80,16])).
% 61.02/61.02 cnf(271,plain,
% 61.02/61.02 (P1(f4(f4(x2711,f4(a6,x2712)),f4(a6,x2713)),f4(f4(x2711,a6),a6))),
% 61.02/61.02 inference(scs_inference,[],[256,241,80,251,232,229,82,248,16,3,6,7])).
% 61.02/61.02 cnf(283,plain,
% 61.02/61.02 (E(f4(f4(a6,x2831),x2832),f4(a6,x2831))),
% 61.02/61.02 inference(scs_inference,[],[256,11,16])).
% 61.02/61.02 cnf(443,plain,
% 61.02/61.02 (~E(f4(f4(a6,x4431),x4432),f4(a1,a5))),
% 61.02/61.02 inference(scs_inference,[],[265,11,6])).
% 61.02/61.02 cnf(515,plain,
% 61.02/61.02 (~E(a3,f4(f4(a6,x5151),x5152))),
% 61.02/61.02 inference(scs_inference,[],[87,248,3])).
% 61.02/61.02 cnf(521,plain,
% 61.02/61.03 (~P1(a1,f4(a6,x5211))),
% 61.02/61.03 inference(scs_inference,[],[109,256,16])).
% 61.02/61.03 cnf(799,plain,
% 61.02/61.03 (~P1(a1,a5)),
% 61.02/61.03 inference(scs_inference,[],[17,2,14])).
% 61.02/61.03 cnf(801,plain,
% 61.02/61.03 (~E(f4(a6,x8011),a2)),
% 61.02/61.03 inference(scs_inference,[],[521,2,59])).
% 61.02/61.03 cnf(815,plain,
% 61.02/61.03 (E(f4(x8151,f4(f4(a6,x8152),x8153)),f4(x8151,a6))),
% 61.02/61.03 inference(scs_inference,[],[239,2,5])).
% 61.02/61.03 cnf(817,plain,
% 61.02/61.03 (~E(f4(a1,a5),f4(f4(a2,a5),f4(a6,x8171)))),
% 61.02/61.03 inference(scs_inference,[],[28,232,2,3])).
% 61.02/61.03 cnf(818,plain,
% 61.02/61.03 (~E(f4(a1,a5),f4(f4(a2,a5),a6))),
% 61.02/61.03 inference(scs_inference,[],[229,817,3])).
% 61.02/61.03 cnf(820,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x8201),x8202),x8203),f4(a6,x8203))),
% 61.02/61.03 inference(scs_inference,[],[239,2,4])).
% 61.02/61.03 cnf(822,plain,
% 61.02/61.03 (E(f4(a6,x8221),f4(f4(f4(a6,x8222),x8223),x8221))),
% 61.02/61.03 inference(scs_inference,[],[820,64,2])).
% 61.02/61.03 cnf(825,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x8251),x8252),f4(x8253,x8252)),f4(a6,x8252))),
% 61.02/61.03 inference(scs_inference,[],[256,820,85,64,2,3,16])).
% 61.02/61.03 cnf(829,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x8291),x8292),f4(x8293,x8292)),a6)),
% 61.02/61.03 inference(scs_inference,[],[256,24,820,85,521,64,2,3,16,6,7])).
% 61.02/61.03 cnf(831,plain,
% 61.02/61.03 (~E(a3,f4(f4(f4(a6,x8311),x8312),f4(x8313,x8312)))),
% 61.02/61.03 inference(scs_inference,[],[825,106,2,3])).
% 61.02/61.03 cnf(833,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x8331),x8332),f4(x8333,x8332)),a6)),
% 61.02/61.03 inference(scs_inference,[],[829,10,825,106,2,3,16])).
% 61.02/61.03 cnf(837,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x8371),x8372),f4(x8373,x8372)),f4(f4(a6,x8374),x8375))),
% 61.02/61.03 inference(scs_inference,[],[239,829,10,825,106,21,2,3,16,6,7])).
% 61.02/61.03 cnf(838,plain,
% 61.02/61.03 (P1(f4(f4(a6,x8381),x8382),f4(x8383,x8382))),
% 61.02/61.03 inference(scs_inference,[],[239,829,10,825,106,21,2,3,16,6,7,15])).
% 61.02/61.03 cnf(841,plain,
% 61.02/61.03 (E(a6,f4(f4(f4(a6,x8411),x8412),f4(x8413,x8412)))),
% 61.02/61.03 inference(scs_inference,[],[833,2])).
% 61.02/61.03 cnf(845,plain,
% 61.02/61.03 (~P1(f4(a1,a5),f4(f4(a6,x8451),a5))),
% 61.02/61.03 inference(scs_inference,[],[838,443,229,831,833,2,3,16])).
% 61.02/61.03 cnf(846,plain,
% 61.02/61.03 (P1(f4(f4(a6,x8461),x8462),f4(x8463,x8462))),
% 61.02/61.03 inference(rename_variables,[],[838])).
% 61.02/61.03 cnf(849,plain,
% 61.02/61.03 (P1(f4(f4(a6,x8491),x8492),a6)),
% 61.02/61.03 inference(scs_inference,[],[838,846,443,24,229,831,833,2,3,16,7])).
% 61.02/61.03 cnf(854,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x8541),x8542),f4(x8543,x8542)),f4(f4(a6,x8544),f4(x8543,x8542)))),
% 61.02/61.03 inference(scs_inference,[],[838,837,818,815,3,16])).
% 61.02/61.03 cnf(855,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x8551),x8552),f4(x8553,x8552)),f4(f4(a6,x8554),x8555))),
% 61.02/61.03 inference(rename_variables,[],[837])).
% 61.02/61.03 cnf(858,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x8581),x8582),f4(x8583,x8582)),f4(a6,x8584))),
% 61.02/61.03 inference(scs_inference,[],[838,837,855,283,818,815,3,16,7])).
% 61.02/61.03 cnf(862,plain,
% 61.02/61.03 (~E(a2,f4(f4(f4(a6,x8621),x8622),f4(x8623,x8622)))),
% 61.02/61.03 inference(scs_inference,[],[854,249,3])).
% 61.02/61.03 cnf(865,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x8651),x8652),f4(x8653,x8652)),f4(a6,x8654))),
% 61.02/61.03 inference(scs_inference,[],[256,858,854,249,3,16])).
% 61.02/61.03 cnf(869,plain,
% 61.02/61.03 (P1(f4(f4(a6,x8691),x8692),f4(f4(a6,x8693),x8694))),
% 61.02/61.03 inference(scs_inference,[],[239,256,858,849,854,249,3,16,7])).
% 61.02/61.03 cnf(877,plain,
% 61.02/61.03 (E(f4(f4(a6,x8771),x8772),f4(a6,x8773))),
% 61.02/61.03 inference(scs_inference,[],[256,869,283,229,862,3,7,16])).
% 61.02/61.03 cnf(902,plain,
% 61.02/61.03 (~E(f4(a5,x9021),a1)),
% 61.02/61.03 inference(scs_inference,[],[799,11,6])).
% 61.02/61.03 cnf(904,plain,
% 61.02/61.03 (~E(a3,a5)),
% 61.02/61.03 inference(scs_inference,[],[799,11,9,6,7])).
% 61.02/61.03 cnf(909,plain,
% 61.02/61.03 (~P1(a2,f4(a6,x9091))),
% 61.02/61.03 inference(scs_inference,[],[801,256,16])).
% 61.02/61.03 cnf(923,plain,
% 61.02/61.03 (E(f4(x9231,f4(f4(a6,x9232),x9233)),f4(x9231,a6))),
% 61.02/61.03 inference(rename_variables,[],[815])).
% 61.02/61.03 cnf(929,plain,
% 61.02/61.03 (E(f4(f4(x9291,f4(a6,x9292)),f4(a6,x9293)),f4(f4(x9291,a6),a6))),
% 61.02/61.03 inference(scs_inference,[],[815,923,838,271,230,6,7,16,64,2])).
% 61.02/61.03 cnf(953,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x9531),x9532),f4(a6,x9533)),f4(a6,x9532))),
% 61.02/61.03 inference(scs_inference,[],[820,251,7])).
% 61.02/61.03 cnf(962,plain,
% 61.02/61.03 (~E(f4(f4(f4(a6,x9621),x9622),f4(a6,x9623)),f4(a1,a5))),
% 61.02/61.03 inference(scs_inference,[],[953,265,6])).
% 61.02/61.03 cnf(1000,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x10001),x10002),f4(a6,x10003)),f4(a6,x10002))),
% 61.02/61.03 inference(rename_variables,[],[953])).
% 61.02/61.03 cnf(1001,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x10011),x10012),f4(a6,x10013)),a6)),
% 61.02/61.03 inference(scs_inference,[],[953,1000,24,521,6,7])).
% 61.02/61.03 cnf(1006,plain,
% 61.02/61.03 (E(a6,f4(f4(f4(a6,x10061),x10062),f4(a6,x10063)))),
% 61.02/61.03 inference(scs_inference,[],[953,1000,24,10,521,6,7,16,2])).
% 61.02/61.03 cnf(1012,plain,
% 61.02/61.03 (E(f4(a6,x10121),f4(f4(f4(a6,x10122),x10123),f4(a6,x10124)))),
% 61.02/61.03 inference(scs_inference,[],[256,1001,32,7,16,2])).
% 61.02/61.03 cnf(1039,plain,
% 61.02/61.03 (E(f4(f4(a6,x10391),x10392),f4(f4(f4(a6,x10393),x10394),f4(x10395,x10394)))),
% 61.02/61.03 inference(scs_inference,[],[841,837,849,7,16])).
% 61.02/61.03 cnf(1041,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x10411),x10412),f4(x10413,x10412)),f4(f4(a6,x10414),x10415))),
% 61.02/61.03 inference(scs_inference,[],[841,837,849,7,16,2])).
% 61.02/61.03 cnf(1057,plain,
% 61.02/61.03 (E(f4(f4(a6,x10571),f4(a6,x10572)),f4(f4(a6,a6),x10571))),
% 61.02/61.03 inference(scs_inference,[],[869,251,16])).
% 61.02/61.03 cnf(1079,plain,
% 61.02/61.03 (~E(a6,a2)),
% 61.02/61.03 inference(scs_inference,[],[909,10,6])).
% 61.02/61.03 cnf(1082,plain,
% 61.02/61.03 (~P1(a2,a6)),
% 61.02/61.03 inference(scs_inference,[],[1079,10,16])).
% 61.02/61.03 cnf(1098,plain,
% 61.02/61.03 (P1(f4(f4(a6,x10981),f4(a6,x10982)),f4(f4(x10983,a6),a6))),
% 61.02/61.03 inference(scs_inference,[],[929,838,7])).
% 61.02/61.03 cnf(1126,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x11261),x11262),f4(x11263,x11262)),f4(f4(x11264,a6),a6))),
% 61.02/61.03 inference(scs_inference,[],[1039,1098,6])).
% 61.02/61.03 cnf(1130,plain,
% 61.02/61.03 (P1(f4(f4(a6,x11301),x11302),f4(f4(x11303,a6),a6))),
% 61.02/61.03 inference(scs_inference,[],[1041,1126,6])).
% 61.02/61.03 cnf(1216,plain,
% 61.02/61.03 (P1(f4(f4(a6,x12161),f4(a6,x12162)),f4(x12163,a6))),
% 61.02/61.03 inference(scs_inference,[],[232,838,7])).
% 61.02/61.03 cnf(1258,plain,
% 61.02/61.03 (E(f4(f4(a6,x12581),f4(a6,x12582)),f4(f4(a6,x12583),a6))),
% 61.02/61.03 inference(scs_inference,[],[869,1216,16])).
% 61.02/61.03 cnf(1262,plain,
% 61.02/61.03 (E(f4(f4(a6,x12621),a6),f4(f4(a6,x12622),f4(a6,x12623)))),
% 61.02/61.03 inference(scs_inference,[],[869,1216,16,2])).
% 61.02/61.03 cnf(1264,plain,
% 61.02/61.03 (E(f4(f4(a6,x12641),f4(x12642,x12641)),f4(f4(a6,x12642),x12641))),
% 61.02/61.03 inference(scs_inference,[],[869,12,16])).
% 61.02/61.03 cnf(1268,plain,
% 61.02/61.03 (E(f4(f4(a6,x12681),x12682),f4(f4(a6,x12682),f4(x12681,x12682)))),
% 61.02/61.03 inference(scs_inference,[],[869,12,16,2])).
% 61.02/61.03 cnf(1318,plain,
% 61.02/61.03 (~E(a1,x13181)+E(f4(x13181,a2),a6)),
% 61.02/61.03 inference(scs_inference,[],[47,14])).
% 61.02/61.03 cnf(1319,plain,
% 61.02/61.03 (E(f4(a1,a2),a6)),
% 61.02/61.03 inference(equality_inference,[],[1318])).
% 61.02/61.03 cnf(1320,plain,
% 61.02/61.03 (E(a6,f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1319,2])).
% 61.02/61.03 cnf(1325,plain,
% 61.02/61.03 (~E(a3,f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[87,1319,3])).
% 61.02/61.03 cnf(1339,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x13391),x13392),f4(a6,x13393)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1320,1001,7])).
% 61.02/61.03 cnf(1348,plain,
% 61.02/61.03 (P1(f4(f4(f4(a6,x13481),x13482),f4(x13483,x13482)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1320,829,7])).
% 61.02/61.03 cnf(1353,plain,
% 61.02/61.03 (P1(f4(f4(a6,x13531),x13532),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1320,849,7])).
% 61.02/61.03 cnf(1354,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x13541),x13542),f4(x13543,x13542)),f4(a1,a2))+~P1(f4(a1,a2),f4(f4(f4(a6,x13541),x13542),f4(x13543,x13542)))),
% 61.02/61.03 inference(scs_inference,[],[1320,849,1348,7,16])).
% 61.02/61.03 cnf(1356,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(f4(f4(a6,x13561),x13562),x13563))+~P1(f4(a1,a2),f4(f4(f4(a6,x13561),x13563),f4(x13562,x13563)))),
% 61.02/61.03 inference(scs_inference,[],[1320,849,1348,7,16,52])).
% 61.02/61.03 cnf(1357,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(f4(a6,x13571),x13572),f4(x13573,x13572)))+~P1(f4(a1,a2),f4(f4(f4(a6,x13571),x13572),f4(x13573,x13572)))),
% 61.02/61.03 inference(scs_inference,[],[1320,849,1348,7,16,52,2])).
% 61.02/61.03 cnf(1359,plain,
% 61.02/61.03 (E(f4(f4(a6,x13591),x13592),f4(a1,a2))+~P1(f4(a1,a2),f4(f4(a6,x13591),x13592))),
% 61.02/61.03 inference(scs_inference,[],[1353,16])).
% 61.02/61.03 cnf(1361,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(f4(a6,x13611),x13612))+~P1(f4(a1,a2),f4(f4(a6,x13612),f4(x13611,x13612)))),
% 61.02/61.03 inference(scs_inference,[],[1353,16,52])).
% 61.02/61.03 cnf(1362,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(a6,x13621),f4(x13622,x13621)))+~P1(f4(a1,a2),f4(f4(a6,x13621),f4(x13622,x13621)))),
% 61.02/61.03 inference(scs_inference,[],[1353,16,52,2])).
% 61.02/61.03 cnf(1369,plain,
% 61.02/61.03 (~P1(f4(a1,a2),f4(f4(a6,x13691),f4(x13692,x13691)))+E(f4(f4(a6,x13692),x13691),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1359,1361])).
% 61.02/61.03 cnf(1371,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(a6,x13711),x13712))+~P1(f4(a1,a2),f4(f4(a6,x13712),f4(x13711,x13712)))),
% 61.02/61.03 inference(scs_inference,[],[1369,2])).
% 61.02/61.03 cnf(1376,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(a6,x13761),f4(x13762,x13761)))),
% 61.02/61.03 inference(scs_inference,[],[10,1320,1362,6])).
% 61.02/61.03 cnf(1378,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(f4(a6,x13781),x13782))),
% 61.02/61.03 inference(scs_inference,[],[1376,2,52])).
% 61.02/61.03 cnf(1379,plain,
% 61.02/61.03 (E(f4(f4(a6,x13791),x13792),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1353,1376,2,52,16])).
% 61.02/61.03 cnf(1382,plain,
% 61.02/61.03 (~E(f4(a1,a2),f4(a1,a5))),
% 61.02/61.03 inference(scs_inference,[],[1353,1376,845,2,52,16,6])).
% 61.02/61.03 cnf(1383,plain,
% 61.02/61.03 (P1(f4(a1,a2),a6)),
% 61.02/61.03 inference(scs_inference,[],[1353,248,1376,845,2,52,16,6,7])).
% 61.02/61.03 cnf(1386,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(a6,x13861),x13862))),
% 61.02/61.03 inference(scs_inference,[],[1378,1371])).
% 61.02/61.03 cnf(1390,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(a6,x13901))),
% 61.02/61.03 inference(scs_inference,[],[1383,1378,32,1082,1371,6,7])).
% 61.02/61.03 cnf(1391,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(a6,x13911))),
% 61.02/61.03 inference(scs_inference,[],[256,1383,1378,32,1082,1371,6,7,16])).
% 61.02/61.03 cnf(1394,plain,
% 61.02/61.03 (E(f4(a6,x13941),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[256,1383,1378,32,1082,1371,6,7,16,2])).
% 61.02/61.03 cnf(1395,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(f4(f4(a6,x13951),x13952),x13953))),
% 61.02/61.03 inference(scs_inference,[],[1390,822,1356,7])).
% 61.02/61.03 cnf(1396,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x13961),x13962),f4(a6,x13963)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1339,1395,16])).
% 61.02/61.03 cnf(1400,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(f4(a6,x14001),x14002),f4(a6,x14003)))),
% 61.02/61.03 inference(scs_inference,[],[1339,1395,16,2])).
% 61.02/61.03 cnf(1401,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x14011),a6),f4(x14012,a6)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1396,1354,52])).
% 61.02/61.03 cnf(1403,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x14031),x14032),f4(x14033,x14032)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1348,1395,1401,2,16])).
% 61.02/61.03 cnf(1407,plain,
% 61.02/61.03 (E(f4(a1,a2),f4(f4(f4(a6,x14071),x14072),f4(x14073,x14072)))),
% 61.02/61.03 inference(scs_inference,[],[1403,1357,52])).
% 61.02/61.03 cnf(1422,plain,
% 61.02/61.03 (~P1(a1,f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[99,1383,11,6,16])).
% 61.02/61.03 cnf(1431,plain,
% 61.02/61.03 (P1(f4(f4(a6,x14311),f4(a6,x14312)),f4(x14313,f4(a6,x14314)))),
% 61.02/61.03 inference(scs_inference,[],[229,1216,7])).
% 61.02/61.03 cnf(1441,plain,
% 61.02/61.03 (~P1(a2,f4(a1,a2))+~P1(f4(a1,a2),a2)),
% 61.02/61.03 inference(scs_inference,[],[1422,59,16])).
% 61.02/61.03 cnf(1442,plain,
% 61.02/61.03 (~P1(f4(a1,a2),a2)+~E(f4(a2,f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[1441,15])).
% 61.02/61.03 cnf(1443,plain,
% 61.02/61.03 (~E(f4(a2,f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[256,1394,1442,6])).
% 61.02/61.03 cnf(1446,plain,
% 61.02/61.03 (~E(f4(a2,f4(a1,a2)),f4(a6,x14461))),
% 61.02/61.03 inference(scs_inference,[],[1443,24,14,3])).
% 61.02/61.03 cnf(1447,plain,
% 61.02/61.03 (~E(f4(a2,f4(a1,a2)),f4(f4(a6,x14471),x14472))),
% 61.02/61.03 inference(scs_inference,[],[1443,248,3])).
% 61.02/61.03 cnf(1453,plain,
% 61.02/61.03 (~E(f4(a2,f4(a1,a2)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1443,1319,3])).
% 61.02/61.03 cnf(1544,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1320,1383,7])).
% 61.02/61.03 cnf(1560,plain,
% 61.02/61.03 (P1(f4(a1,a2),f4(f4(x15601,a6),a6))),
% 61.02/61.03 inference(scs_inference,[],[1379,1130,6])).
% 61.02/61.03 cnf(1575,plain,
% 61.02/61.03 (~E(f4(f4(a1,a2),x15751),a1)),
% 61.02/61.03 inference(scs_inference,[],[1422,11,6])).
% 61.02/61.03 cnf(2029,plain,
% 61.02/61.03 (E(f4(x20291,f4(a1,a2)),f4(x20291,f4(a6,x20292)))),
% 61.02/61.03 inference(scs_inference,[],[1391,5])).
% 61.02/61.03 cnf(2030,plain,
% 61.02/61.03 (E(f4(f4(a1,a2),f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[1544,1391,5,14])).
% 61.02/61.03 cnf(2032,plain,
% 61.02/61.03 (~E(f4(a2,a6),a6)),
% 61.02/61.03 inference(scs_inference,[],[1544,1391,1082,5,14,15])).
% 61.02/61.03 cnf(2034,plain,
% 61.02/61.03 (E(f4(f4(a1,a2),x20341),f4(f4(a6,x20342),x20341))),
% 61.02/61.03 inference(scs_inference,[],[1544,1391,1082,5,14,15,4])).
% 61.02/61.03 cnf(2036,plain,
% 61.02/61.03 (~P1(f4(a2,f4(a1,a2)),f4(f4(a6,x20361),f4(a1,a2)))),
% 61.02/61.03 inference(scs_inference,[],[904,1544,1391,1447,1082,838,5,14,15,4,2,16])).
% 61.02/61.03 cnf(2040,plain,
% 61.02/61.03 (P1(f4(f4(a6,a6),x20401),f4(x20402,f4(a6,x20403)))),
% 61.02/61.03 inference(scs_inference,[],[904,1544,1391,1447,1264,1082,1431,838,5,14,15,4,2,16,6])).
% 61.02/61.03 cnf(2043,plain,
% 61.02/61.03 (~P1(f4(a1,a5),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[904,1544,1391,1447,1264,1082,1431,265,838,5,14,15,4,2,16,6,7])).
% 61.02/61.03 cnf(2046,plain,
% 61.02/61.03 (E(f4(x20461,f4(a6,x20462)),f4(x20461,f4(a6,x20463)))),
% 61.02/61.03 inference(scs_inference,[],[34,5])).
% 61.02/61.03 cnf(2047,plain,
% 61.02/61.03 (E(f4(f4(a1,a2),f4(a6,x20471)),a6)),
% 61.02/61.03 inference(scs_inference,[],[34,1390,5,14])).
% 61.02/61.03 cnf(2049,plain,
% 61.02/61.03 (~E(f4(f4(a1,a5),f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[2043,34,1390,5,14,15])).
% 61.02/61.03 cnf(2051,plain,
% 61.02/61.03 (E(f4(f4(a6,x20511),x20512),f4(f4(a6,x20513),x20512))),
% 61.02/61.03 inference(scs_inference,[],[2043,34,1390,5,14,15,4])).
% 61.02/61.03 cnf(2053,plain,
% 61.02/61.03 (~E(f4(a2,f4(a6,x20531)),a6)),
% 61.02/61.03 inference(scs_inference,[],[19,2043,2032,34,1390,229,5,14,15,4,2,3])).
% 61.02/61.03 cnf(2055,plain,
% 61.02/61.03 (~P1(f4(a2,a6),a6)),
% 61.02/61.03 inference(scs_inference,[],[19,2043,2032,34,1390,229,10,5,14,15,4,2,3,16])).
% 61.02/61.03 cnf(2061,plain,
% 61.02/61.03 (~P1(f4(a2,f4(a1,a2)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[19,2043,2032,1386,2034,2036,34,1390,233,229,10,5,14,15,4,2,3,16,6,7])).
% 61.02/61.03 cnf(2064,plain,
% 61.02/61.03 (E(f4(x20641,f4(a6,x20642)),f4(x20641,f4(a1,a2)))),
% 61.02/61.03 inference(scs_inference,[],[1394,5])).
% 61.02/61.03 cnf(2065,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x20651),f4(a6,x20652)),f4(x20653,a6)),a6)),
% 61.02/61.03 inference(scs_inference,[],[1394,1216,5,14])).
% 61.02/61.03 cnf(2067,plain,
% 61.02/61.03 (~E(f4(f4(a2,a6),a6),a6)),
% 61.02/61.03 inference(scs_inference,[],[2055,1394,1216,5,14,15])).
% 61.02/61.03 cnf(2069,plain,
% 61.02/61.03 (E(f4(f4(a6,x20691),x20692),f4(f4(a1,a2),x20692))),
% 61.02/61.03 inference(scs_inference,[],[2055,1394,1216,5,14,15,4])).
% 61.02/61.03 cnf(2070,plain,
% 61.02/61.03 (~E(f4(a1,a2),a3)),
% 61.02/61.03 inference(scs_inference,[],[1325,2055,1394,1216,5,14,15,4,2])).
% 61.02/61.03 cnf(2071,plain,
% 61.02/61.03 (~P1(f4(f4(a1,a5),f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[1325,2055,2049,1394,1216,10,5,14,15,4,2,16])).
% 61.02/61.03 cnf(2074,plain,
% 61.02/61.03 (P1(f4(f4(a6,x20741),x20742),f4(x20743,f4(a6,x20744)))),
% 61.02/61.03 inference(scs_inference,[],[1325,2055,2049,2040,2051,1394,1216,10,5,14,15,4,2,16,6])).
% 61.02/61.03 cnf(2076,plain,
% 61.02/61.03 (~P1(f4(a2,a6),f4(f4(a1,a2),f4(a1,a2)))),
% 61.02/61.03 inference(scs_inference,[],[1325,2055,2030,2049,2040,2051,1394,1216,10,5,14,15,4,2,16,6,7])).
% 61.02/61.03 cnf(2078,plain,
% 61.02/61.03 (E(f4(x20781,f4(a1,a2)),f4(x20781,a6))),
% 61.02/61.03 inference(scs_inference,[],[1319,5])).
% 61.02/61.03 cnf(2079,plain,
% 61.02/61.03 (E(f4(f4(f4(a6,x20791),x20792),f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[1353,1319,5,14])).
% 61.02/61.03 cnf(2081,plain,
% 61.02/61.03 (~E(f4(f4(a2,f4(a1,a2)),f4(a1,a2)),a6)),
% 61.02/61.03 inference(scs_inference,[],[2061,1353,1319,5,14,15])).
% 61.02/61.03 cnf(2083,plain,
% 61.02/61.03 (E(f4(f4(a1,a2),x20831),f4(a6,x20831))),
% 61.02/61.03 inference(scs_inference,[],[2061,1353,1319,5,14,15,4])).
% 61.02/61.03 cnf(2085,plain,
% 61.02/61.03 (~P1(f4(f4(a2,a6),a6),a6)),
% 61.02/61.03 inference(scs_inference,[],[1382,2061,2067,1353,1319,10,5,14,15,4,2,16])).
% 61.02/61.03 cnf(2088,plain,
% 61.02/61.03 (~P1(f4(a2,f4(a6,x20881)),f4(a1,a2))),
% 61.02/61.03 inference(scs_inference,[],[1382,2061,2067,2064,1353,1319,10,5,14,15,4,2,16,6])).
% 61.02/61.03 cnf(2090,plain,
% 61.02/61.03 (~P1(f4(f4(a1,a5),f4(a1,a2)),f4(f4(a1,a2),f4(a6,x20901)))),
% 61.02/61.03 inference(scs_inference,[],[1382,2061,2067,2071,2047,2064,1353,1319,10,5,14,15,4,2,16,6,7])).
% 61.02/61.03 cnf(2092,plain,
% 61.02/61.03 (E(f4(x20921,a6),f4(x20921,f4(a1,a2)))),
% 61.02/61.03 inference(scs_inference,[],[1320,5])).
% 61.02/61.03 cnf(2093,plain,
% 61.02/61.03 (E(f4(f4(a1,a2),a6),a6)),
% 61.02/61.03 inference(scs_inference,[],[1383,1320,5,14])).
% 61.02/61.03 cnf(2097,plain,
% 61.02/61.04 (E(f4(a6,x20971),f4(f4(a1,a2),x20971))),
% 61.02/61.04 inference(scs_inference,[],[2088,1383,1320,5,14,15,4])).
% 61.02/61.04 cnf(2099,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x20991)),a6)),
% 61.02/61.04 inference(scs_inference,[],[902,2088,2053,1383,1320,10,5,14,15,4,2,16])).
% 61.02/61.04 cnf(2102,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a1,a2)),f4(f4(a1,a2),f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[902,2078,2088,2076,2053,1383,1320,10,5,14,15,4,2,16,6])).
% 61.02/61.04 cnf(2104,plain,
% 61.02/61.04 (~P1(a1,f4(f4(a1,a2),x21041))),
% 61.02/61.04 inference(scs_inference,[],[902,2078,2083,2088,2076,2053,1383,521,1320,10,5,14,15,4,2,16,6,7])).
% 61.02/61.04 cnf(2106,plain,
% 61.02/61.04 (~E(a2,f4(f4(a1,a2),x21061))),
% 61.02/61.04 inference(scs_inference,[],[902,2078,2083,2088,2076,2053,1383,521,1320,10,5,14,15,4,2,16,6,7,59])).
% 61.02/61.04 cnf(2107,plain,
% 61.02/61.04 (~E(f4(f4(a1,x21071),f4(a2,x21071)),a1)),
% 61.02/61.04 inference(scs_inference,[],[902,2078,2083,2088,2076,2053,1383,521,1320,10,5,14,15,4,2,16,6,7,59,52])).
% 61.02/61.04 cnf(2109,plain,
% 61.02/61.04 (E(f4(f4(x21091,x21092),x21091),a6)),
% 61.02/61.04 inference(scs_inference,[],[11,14])).
% 61.02/61.04 cnf(2111,plain,
% 61.02/61.04 (~E(f4(a1,f4(a1,a2)),a6)),
% 61.02/61.04 inference(scs_inference,[],[1422,11,14,15])).
% 61.02/61.04 cnf(2114,plain,
% 61.02/61.04 (~E(f4(a2,f4(a6,x21141)),f4(a1,a2))),
% 61.02/61.04 inference(scs_inference,[],[1453,2029,1422,11,14,15,2,3])).
% 61.02/61.04 cnf(2116,plain,
% 61.02/61.04 (~P1(f4(f4(a2,f4(a1,a2)),f4(a1,a2)),a6)),
% 61.02/61.04 inference(scs_inference,[],[1453,2029,2081,1422,11,10,14,15,2,3,16])).
% 61.02/61.04 cnf(2119,plain,
% 61.02/61.04 (P1(f4(f4(a1,a2),x21191),a6)),
% 61.02/61.04 inference(scs_inference,[],[1453,2097,2029,2081,1422,11,10,14,15,2,3,16,6])).
% 61.02/61.04 cnf(2122,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),a6),f4(f4(a1,a2),a6))),
% 61.02/61.04 inference(scs_inference,[],[1453,2097,2085,2093,2029,2081,1422,11,10,14,15,2,3,16,6,7])).
% 61.02/61.04 cnf(2125,plain,
% 61.02/61.04 (E(f4(x21251,a3),a6)),
% 61.02/61.04 inference(scs_inference,[],[9,14])).
% 61.02/61.04 cnf(2127,plain,
% 61.02/61.04 (~E(f4(a1,a5),a6)),
% 61.02/61.04 inference(scs_inference,[],[799,9,14,15])).
% 61.02/61.04 cnf(2129,plain,
% 61.02/61.04 (E(f4(f4(x21291,a3),x21292),f4(a6,x21292))),
% 61.02/61.04 inference(scs_inference,[],[799,9,14,15,4])).
% 61.02/61.04 cnf(2131,plain,
% 61.02/61.04 (~E(f4(a2,a6),f4(a6,x21311))),
% 61.02/61.04 inference(scs_inference,[],[2114,1446,2078,799,9,14,15,4,2,3])).
% 61.02/61.04 cnf(2133,plain,
% 61.02/61.04 (E(a6,f4(f4(a1,a2),x21331))),
% 61.02/61.04 inference(scs_inference,[],[2114,1446,2119,2078,799,10,9,14,15,4,2,3,16])).
% 61.02/61.04 cnf(2136,plain,
% 61.02/61.04 (P1(f4(f4(a1,a2),x21361),f4(x21362,f4(a6,x21363)))),
% 61.02/61.04 inference(scs_inference,[],[2114,1446,2119,2069,2074,2078,799,10,9,14,15,4,2,3,16,6])).
% 61.02/61.04 cnf(2138,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x21381)),f4(f4(x21382,x21383),x21382))),
% 61.02/61.04 inference(scs_inference,[],[2114,1446,2109,2119,2099,2069,2074,2078,799,10,9,14,15,4,2,3,16,6,7])).
% 61.02/61.04 cnf(2139,plain,
% 61.02/61.04 (E(f4(x21391,f4(x21392,a3)),f4(x21391,a6))),
% 61.02/61.04 inference(scs_inference,[],[2114,1446,2109,2119,2099,2069,2074,2078,799,10,9,14,15,4,2,3,16,6,7,5])).
% 61.02/61.04 cnf(2142,plain,
% 61.02/61.04 (~E(f4(f4(a1,a5),a6),a6)),
% 61.02/61.04 inference(scs_inference,[],[21,15])).
% 61.02/61.04 cnf(2144,plain,
% 61.02/61.04 (~E(f4(a6,x21441),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2131,21,15,2])).
% 61.02/61.04 cnf(2145,plain,
% 61.02/61.04 (~E(f4(a1,f4(a6,x21451)),a6)),
% 61.02/61.04 inference(scs_inference,[],[2131,2111,2029,21,15,2,3])).
% 61.02/61.04 cnf(2147,plain,
% 61.02/61.04 (E(f4(f4(a1,a2),a6),f4(f4(a6,x21471),f4(a6,x21472)))),
% 61.02/61.04 inference(scs_inference,[],[2131,2111,2136,2029,1216,21,15,2,3,16])).
% 61.02/61.04 cnf(2151,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(x21511,a3)),f4(f4(a1,a2),a6))),
% 61.02/61.04 inference(scs_inference,[],[2131,2139,2111,2136,2122,2029,1216,21,15,2,3,16,6])).
% 61.02/61.04 cnf(2153,plain,
% 61.02/61.04 (~P1(f4(f4(a2,f4(a1,a2)),f4(a1,a2)),f4(x21531,a3))),
% 61.02/61.04 inference(scs_inference,[],[2131,2125,2139,2111,2136,2122,2116,2029,1216,21,15,2,3,16,6,7])).
% 61.02/61.04 cnf(2156,plain,
% 61.02/61.04 (~E(f4(f4(a1,a5),f4(a6,x21561)),a6)),
% 61.02/61.04 inference(scs_inference,[],[265,15])).
% 61.02/61.04 cnf(2161,plain,
% 61.02/61.04 (~P1(a3,f4(f4(a6,x21611),x21612))),
% 61.02/61.04 inference(scs_inference,[],[2144,1575,515,1012,265,9,15,2,3,16])).
% 61.02/61.04 cnf(2164,plain,
% 61.02/61.04 (~P1(f4(f4(a1,a5),a6),f4(f4(a1,a2),f4(a6,x21641)))),
% 61.02/61.04 inference(scs_inference,[],[2144,2092,1575,515,2090,1012,265,9,15,2,3,16,6])).
% 61.02/61.04 cnf(2165,plain,
% 61.02/61.04 (E(f4(x21651,a6),f4(x21651,f4(a1,a2)))),
% 61.02/61.04 inference(rename_variables,[],[2092])).
% 61.02/61.04 cnf(2166,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a1,a2)),f4(f4(a1,a2),a6))),
% 61.02/61.04 inference(scs_inference,[],[2144,2092,2165,1575,515,2102,2090,1012,265,9,15,2,3,16,6,7])).
% 61.02/61.04 cnf(2168,plain,
% 61.02/61.04 (~E(f4(f4(a6,x21681),f4(x21682,x21681)),a3)),
% 61.02/61.04 inference(scs_inference,[],[2144,2092,2165,1575,515,2102,2090,1012,265,9,15,2,3,16,6,7,52])).
% 61.02/61.04 cnf(2170,plain,
% 61.02/61.04 (~E(f4(f4(a1,a5),f4(a2,a5)),a6)),
% 61.02/61.04 inference(scs_inference,[],[13,15])).
% 61.02/61.04 cnf(2177,plain,
% 61.02/61.04 (~P1(a3,a5)),
% 61.02/61.04 inference(scs_inference,[],[2129,2168,2156,2166,904,13,9,15,52,2,3,16])).
% 61.02/61.04 cnf(2180,plain,
% 61.02/61.04 (P1(f4(f4(a1,a2),x21801),x21802)),
% 61.02/61.04 inference(scs_inference,[],[2129,2133,2168,2156,2166,904,13,10,9,15,52,2,3,16,6])).
% 61.02/61.04 cnf(2181,plain,
% 61.02/61.04 (~P1(a3,f4(f4(a1,a2),a6))),
% 61.02/61.04 inference(scs_inference,[],[2129,2133,2168,2156,2161,2166,2147,904,13,10,9,15,52,2,3,16,6,7])).
% 61.02/61.04 cnf(2184,plain,
% 61.02/61.04 (E(f4(f4(a1,x21841),f4(a2,x21841)),f4(f4(a1,a2),x21841))),
% 61.02/61.04 inference(scs_inference,[],[2129,2133,2168,2156,2161,2166,2147,904,13,10,9,15,52,2,3,16,6,7,41])).
% 61.02/61.04 cnf(2186,plain,
% 61.02/61.04 (E(f4(f4(a1,a2),x21861),f4(f4(a1,x21861),f4(a2,x21861)))),
% 61.02/61.04 inference(scs_inference,[],[2129,2133,2168,2156,2161,2166,2147,904,13,10,9,15,52,2,3,16,6,7,41,44])).
% 61.02/61.04 cnf(2191,plain,
% 61.02/61.04 (~E(f4(a3,a5),a6)),
% 61.02/61.04 inference(scs_inference,[],[2177,15])).
% 61.02/61.04 cnf(2193,plain,
% 61.02/61.04 (~E(f4(f4(a1,a6),f4(a2,a6)),a3)),
% 61.02/61.04 inference(scs_inference,[],[2177,2181,15,52])).
% 61.02/61.04 cnf(2194,plain,
% 61.02/61.04 (~E(a6,f4(f4(a1,a5),f4(a2,a5)))),
% 61.02/61.04 inference(scs_inference,[],[2177,2181,2170,15,52,2])).
% 61.02/61.04 cnf(2198,plain,
% 61.02/61.04 (P1(f4(f4(a1,a2),x21981),x21982)),
% 61.02/61.04 inference(rename_variables,[],[2180])).
% 61.02/61.04 cnf(2200,plain,
% 61.02/61.04 (~E(f4(f4(a1,a2),x22001),a3)),
% 61.02/61.04 inference(scs_inference,[],[2177,2180,2198,2104,2106,2181,2170,2184,15,52,2,7,16,6])).
% 61.02/61.04 cnf(2206,plain,
% 61.02/61.04 (~E(f4(a1,a6),a6)),
% 61.02/61.04 inference(scs_inference,[],[99,15])).
% 61.02/61.04 cnf(2208,plain,
% 61.02/61.04 (~E(a6,f4(a3,a5))),
% 61.02/61.04 inference(scs_inference,[],[2191,99,15,2])).
% 61.02/61.04 cnf(2209,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x22091)),f4(f4(a6,x22092),f4(a6,x22093)))),
% 61.02/61.04 inference(scs_inference,[],[2191,2138,1258,99,15,2,7])).
% 61.02/61.04 cnf(2212,plain,
% 61.02/61.04 (~P1(a3,f4(a2,a5))),
% 61.02/61.04 inference(scs_inference,[],[9,2191,2138,1258,19,99,15,2,7,16])).
% 61.02/61.04 cnf(2215,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a6,x22151)),f4(f4(a1,a2),a6))),
% 61.02/61.04 inference(scs_inference,[],[9,2191,2151,2046,2138,1258,19,99,15,2,7,16,6])).
% 61.02/61.04 cnf(2218,plain,
% 61.02/61.04 (~E(a6,a3)),
% 61.02/61.04 inference(scs_inference,[],[9,2191,2200,2151,2046,2138,1258,19,2125,99,15,2,7,16,6,3])).
% 61.02/61.04 cnf(2224,plain,
% 61.02/61.04 (~E(f4(a3,f4(a2,a5)),a6)),
% 61.02/61.04 inference(scs_inference,[],[2212,15])).
% 61.02/61.04 cnf(2226,plain,
% 61.02/61.04 (~E(a6,f4(a1,a6))),
% 61.02/61.04 inference(scs_inference,[],[2206,2212,15,2])).
% 61.02/61.04 cnf(2227,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a6,x22271)),f4(f4(a1,a2),f4(x22272,a3)))),
% 61.02/61.04 inference(scs_inference,[],[2206,2212,2215,2139,15,2,7])).
% 61.02/61.04 cnf(2228,plain,
% 61.02/61.04 (E(f4(x22281,f4(x22282,a3)),f4(x22281,a6))),
% 61.02/61.04 inference(rename_variables,[],[2139])).
% 61.02/61.04 cnf(2229,plain,
% 61.02/61.04 (~P1(a3,f4(a1,a2))),
% 61.02/61.04 inference(scs_inference,[],[9,2206,2212,2215,1325,2139,15,2,7,16])).
% 61.02/61.04 cnf(2232,plain,
% 61.02/61.04 (~P1(f4(f4(a1,a5),f4(x22321,a3)),f4(f4(a1,a2),f4(a6,x22322)))),
% 61.02/61.04 inference(scs_inference,[],[9,2206,2212,2215,2164,1325,2139,2228,15,2,7,16,6])).
% 61.02/61.04 cnf(2238,plain,
% 61.02/61.04 (~E(f4(a3,f4(a1,a2)),a6)),
% 61.02/61.04 inference(scs_inference,[],[2229,15])).
% 61.02/61.04 cnf(2240,plain,
% 61.02/61.04 (~E(a3,f4(f4(a1,a6),f4(a2,a6)))),
% 61.02/61.04 inference(scs_inference,[],[2229,2193,15,2])).
% 61.02/61.04 cnf(2244,plain,
% 61.02/61.04 (~P1(f4(a2,a6),f4(a6,x22441))),
% 61.02/61.04 inference(scs_inference,[],[2229,2193,2209,1268,2131,256,15,2,7,16])).
% 61.02/61.04 cnf(2247,plain,
% 61.02/61.04 (~P1(f4(f4(a2,f4(a1,a2)),f4(a6,x22471)),f4(x22472,a3))),
% 61.02/61.04 inference(scs_inference,[],[2229,2193,2153,2209,1268,2131,2064,256,15,2,7,16,6])).
% 61.02/61.04 cnf(2249,plain,
% 61.02/61.04 (~E(f4(f4(a1,a2),x22491),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2229,2193,2153,2209,1268,2131,2144,2097,2064,256,15,2,7,16,6,3])).
% 61.02/61.04 cnf(2253,plain,
% 61.02/61.04 (~E(f4(f4(a2,a6),f4(a6,x22531)),a6)),
% 61.02/61.04 inference(scs_inference,[],[2244,15])).
% 61.02/61.04 cnf(2255,plain,
% 61.02/61.04 (~E(f4(a2,a6),f4(f4(a1,a2),x22551))),
% 61.02/61.04 inference(scs_inference,[],[2244,2249,15,2])).
% 61.02/61.04 cnf(2256,plain,
% 61.02/61.04 (~E(f4(f4(a2,a6),f4(a1,a2)),f4(x22561,a3))),
% 61.02/61.04 inference(scs_inference,[],[2244,2249,2247,15,2,64])).
% 61.02/61.04 cnf(2258,plain,
% 61.02/61.04 (~P1(f4(a2,a6),f4(f4(a6,x22581),x22582))),
% 61.02/61.04 inference(scs_inference,[],[2244,2249,2247,877,15,2,64,7])).
% 61.02/61.04 cnf(2259,plain,
% 61.02/61.04 (~P1(f4(a2,a6),f4(a6,x22591))),
% 61.02/61.04 inference(rename_variables,[],[2244])).
% 61.02/61.04 cnf(2263,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a1,a2)),f4(a6,x22631))),
% 61.02/61.04 inference(scs_inference,[],[9,2244,2259,2249,2240,2247,877,2078,15,2,64,7,16,6])).
% 61.02/61.04 cnf(2265,plain,
% 61.02/61.04 (~E(a6,f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[9,2244,2259,2249,2240,2247,877,2030,2078,15,2,64,7,16,6,3])).
% 61.02/61.04 cnf(2267,plain,
% 61.02/61.04 (~E(f4(f4(a6,x22671),f4(x22672,x22671)),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[9,2244,2259,2249,2240,2247,877,2030,2078,15,2,64,7,16,6,3,52])).
% 61.02/61.04 cnf(2272,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a1,a2)),f4(f4(a1,a2),x22721))),
% 61.02/61.04 inference(scs_inference,[],[2267,2263,2083,15,2,7])).
% 61.02/61.04 cnf(2274,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a1,a2)),f4(f4(a1,a2),a3))),
% 61.02/61.04 inference(scs_inference,[],[2267,2256,2263,2083,2180,15,2,7,16])).
% 61.02/61.04 cnf(2278,plain,
% 61.02/61.04 (~P1(f4(a2,f4(x22781,a3)),f4(f4(a6,x22782),x22783))),
% 61.02/61.04 inference(scs_inference,[],[2267,2256,2263,2258,2083,2180,2139,15,2,7,16,6])).
% 61.02/61.04 cnf(2280,plain,
% 61.02/61.04 (~E(f4(f4(a6,a6),x22801),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2267,2256,2263,2258,1057,2083,2180,2139,15,2,7,16,6,3])).
% 61.02/61.04 cnf(2287,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a6,x22871)),a6)),
% 61.02/61.04 inference(scs_inference,[],[2280,2227,2274,2133,52,2,7])).
% 61.02/61.04 cnf(2289,plain,
% 61.02/61.04 (~P1(f4(a2,a6),f4(f4(a1,a2),x22891))),
% 61.02/61.04 inference(scs_inference,[],[2280,2255,2227,2274,2133,2180,52,2,7,16])).
% 61.02/61.04 cnf(2295,plain,
% 61.02/61.04 (~E(f4(f4(a6,x22951),f4(a6,x22952)),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2280,2255,2227,2232,2274,1262,2133,2046,2180,52,2,7,16,6,3])).
% 61.02/61.04 cnf(2300,plain,
% 61.02/61.04 (~E(f4(f4(a1,x23001),f4(a2,x23001)),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2289,52])).
% 61.02/61.04 cnf(2302,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a6,x23021)),f4(f4(x23022,x23023),x23022))),
% 61.02/61.04 inference(scs_inference,[],[2295,2289,2287,2109,52,2,7])).
% 61.02/61.04 cnf(2303,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a1,a2)),a6)),
% 61.02/61.04 inference(scs_inference,[],[2295,2289,2287,2109,2029,52,2,7,6])).
% 61.02/61.04 cnf(2306,plain,
% 61.02/61.04 (~E(f4(f4(a2,a6),a6),f4(f4(x23061,x23062),x23061))),
% 61.02/61.04 inference(scs_inference,[],[2218,2295,2289,2287,2109,1006,2029,52,2,7,6,3,64])).
% 61.02/61.04 cnf(2312,plain,
% 61.02/61.04 (~E(f4(a2,a6),f4(f4(a1,x23121),f4(a2,x23121)))),
% 61.02/61.04 inference(scs_inference,[],[2300,2302,52,2])).
% 61.02/61.04 cnf(2313,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a6,x23131)),f4(a1,a2))),
% 61.02/61.04 inference(scs_inference,[],[2300,2302,1400,52,2,7])).
% 61.02/61.04 cnf(2316,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),a6),f4(f4(a6,x23161),a6))),
% 61.02/61.04 inference(scs_inference,[],[2300,2306,2302,1400,1130,52,2,7,16])).
% 61.02/61.04 cnf(2320,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x23201)),f4(f4(a6,x23202),x23203))),
% 61.02/61.04 inference(scs_inference,[],[2300,2306,2302,2278,1400,2046,1130,52,2,7,16,6])).
% 61.02/61.04 cnf(2323,plain,
% 61.02/61.04 (~E(f4(f4(a6,x23231),f4(a2,a2)),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2300,2306,2302,2278,1400,2034,2046,1130,52,2,7,16,6,3])).
% 61.02/61.04 cnf(2328,plain,
% 61.02/61.04 (~E(f4(f4(a2,a6),a6),f4(a1,a2))),
% 61.02/61.04 inference(scs_inference,[],[2300,2306,2302,2278,1400,2034,2046,1130,52,2,7,16,6,3,15,64])).
% 61.02/61.04 cnf(2331,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a1,a2)),f4(f4(a1,a2),a6))),
% 61.02/61.04 inference(scs_inference,[],[2328,2303,2316,2093,52,2,7])).
% 61.02/61.04 cnf(2335,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a1,a2)),f4(f4(a6,x23351),a6))),
% 61.02/61.04 inference(scs_inference,[],[2328,2303,2316,2093,1560,2078,52,2,7,16,6])).
% 61.02/61.04 cnf(2341,plain,
% 61.02/61.04 (~E(f4(f4(a1,a6),f4(a2,a6)),f4(f4(a2,a6),f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[2331,52])).
% 61.02/61.04 cnf(2352,plain,
% 61.02/61.04 (~E(f4(f4(f4(a6,x23521),x23522),f4(x23523,x23522)),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2265,2323,2335,841,52,2,3])).
% 61.02/61.04 cnf(2354,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x23541)),f4(f4(a1,a2),x23542))),
% 61.02/61.04 inference(scs_inference,[],[2265,2323,2272,2335,2085,2047,841,2064,52,2,3,7,6])).
% 61.02/61.04 cnf(2357,plain,
% 61.02/61.04 (~E(a6,f4(a3,f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[2238,2354,52,2])).
% 61.02/61.04 cnf(2361,plain,
% 61.02/61.04 (~P1(f4(f4(a2,a6),f4(a1,a2)),f4(a1,a2))),
% 61.02/61.04 inference(scs_inference,[],[2127,2313,2238,2354,2065,2184,2029,52,2,3,7,6])).
% 61.02/61.04 cnf(2368,plain,
% 61.02/61.04 (~E(f4(a1,a2),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2142,2352,2320,1396,52,2,3])).
% 61.02/61.04 cnf(2371,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x23711)),f4(a6,x23712))),
% 61.02/61.04 inference(scs_inference,[],[2142,2352,2320,1396,2138,1012,52,2,3,7])).
% 61.02/61.04 cnf(2374,plain,
% 61.02/61.04 (~P1(f4(f4(a1,a5),a6),a6)),
% 61.02/61.04 inference(scs_inference,[],[10,2142,2352,2320,1396,2138,1012,52,2,3,7,16])).
% 61.02/61.04 cnf(2383,plain,
% 61.02/61.04 (~E(f4(a2,a6),f4(a1,a2))),
% 61.02/61.04 inference(scs_inference,[],[2368,2371,2278,15,52,2])).
% 61.02/61.04 cnf(2384,plain,
% 61.02/61.04 (~E(f4(f4(a6,x23841),x23842),f4(a2,a6))),
% 61.02/61.04 inference(scs_inference,[],[2368,2371,1386,2278,15,52,2,3])).
% 61.02/61.04 cnf(2385,plain,
% 61.02/61.04 (~P1(f4(a2,f4(a6,x23851)),f4(f4(x23852,a3),x23853))),
% 61.02/61.04 inference(scs_inference,[],[2368,2371,2129,1386,2278,15,52,2,3,7])).
% 61.02/61.04 cnf(2387,plain,
% 61.02/61.04 (~P1(f4(a3,a5),a6)),
% 61.02/61.04 inference(scs_inference,[],[10,2368,2208,2371,2129,1386,2278,15,52,2,3,7,16])).
% 61.02/61.04 cnf(2392,plain,
% 61.02/61.04 (~E(f4(f4(a3,a5),a6),a6)),
% 61.02/61.04 inference(scs_inference,[],[2387,15])).
% 61.02/61.04 cnf(2396,plain,
% 61.02/61.04 (~E(f4(f4(a1,a2),x23961),f4(a1,a6))),
% 61.02/61.04 inference(scs_inference,[],[2387,2226,2384,2385,2133,15,52,2,3])).
% 61.02/61.04 cnf(2397,plain,
% 61.02/61.04 (~P1(f4(a3,a5),f4(f4(f4(a6,x23971),x23972),f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[2387,2226,2384,2385,2079,2133,15,52,2,3,7])).
% 61.02/61.04 cnf(2398,plain,
% 61.02/61.04 (~P1(f4(a3,f4(a2,a5)),a6)),
% 61.02/61.04 inference(scs_inference,[],[10,2387,2226,2384,2224,2385,2079,2133,15,52,2,3,7,16])).
% 61.02/61.04 cnf(2404,plain,
% 61.02/61.04 (~E(f4(a1,a6),f4(f4(a1,a2),x24041))),
% 61.02/61.04 inference(scs_inference,[],[2396,2])).
% 61.02/61.04 cnf(2405,plain,
% 61.02/61.04 (~E(f4(f4(a1,x24051),f4(a2,x24051)),f4(a1,a6))),
% 61.02/61.04 inference(scs_inference,[],[2396,2186,2,3])).
% 61.02/61.04 cnf(2406,plain,
% 61.02/61.04 (~E(f4(f4(a1,a2),x24061),f4(a1,a6))),
% 61.02/61.04 inference(rename_variables,[],[2396])).
% 61.02/61.04 cnf(2414,plain,
% 61.02/61.04 (~E(a6,f4(a3,f4(a2,a5)))),
% 61.02/61.04 inference(scs_inference,[],[10,2396,2406,2398,2397,2186,1407,2180,2,3,16,7,6])).
% 61.02/61.04 cnf(2416,plain,
% 61.02/61.04 (~E(f4(f4(a3,a5),f4(a1,a2)),a6)),
% 61.02/61.04 inference(scs_inference,[],[10,2396,2406,2398,2397,2186,1407,2180,2,3,16,7,6,15])).
% 61.02/61.04 cnf(2418,plain,
% 61.02/61.04 (~E(f4(a1,a6),f4(f4(a1,x24181),f4(a2,x24181)))),
% 61.02/61.04 inference(scs_inference,[],[2405,2])).
% 61.02/61.04 cnf(2419,plain,
% 61.02/61.04 (~E(f4(a6,f4(a2,a2)),f4(a1,a6))),
% 61.02/61.04 inference(scs_inference,[],[2405,2083,2,3])).
% 61.02/61.04 cnf(2425,plain,
% 61.02/61.04 (~P1(f4(f4(a1,a5),a6),f4(f4(a1,a2),f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[10,2405,2392,2374,2083,2030,2,3,16,7])).
% 61.02/61.04 cnf(2428,plain,
% 61.02/61.04 (~E(f4(a1,a6),f4(a6,f4(a2,a2)))),
% 61.02/61.04 inference(scs_inference,[],[2419,2])).
% 61.02/61.04 cnf(2431,plain,
% 61.02/61.04 (~P1(f4(a1,a6),f4(a6,f4(a2,a2)))),
% 61.02/61.04 inference(scs_inference,[],[2419,2404,2092,256,2,3,16])).
% 61.02/61.04 cnf(2439,plain,
% 61.02/61.04 (~E(f4(f4(a1,a2),x24391),f4(a3,f4(a2,a5)))),
% 61.02/61.04 inference(scs_inference,[],[2416,2414,2133,2,3])).
% 61.02/61.04 cnf(2440,plain,
% 61.02/61.04 (~P1(f4(f4(a3,a5),f4(a1,a2)),a6)),
% 61.02/61.04 inference(scs_inference,[],[10,2416,2414,2133,2,3,16])).
% 61.02/61.04 cnf(2441,plain,
% 61.02/61.04 (P1(a6,x24411)),
% 61.02/61.04 inference(rename_variables,[],[10])).
% 61.02/61.04 cnf(2445,plain,
% 61.02/61.04 (P1(f4(f4(f4(a6,x24451),x24452),f4(x24453,x24452)),x24454)),
% 61.02/61.04 inference(scs_inference,[],[10,2441,2431,2416,2414,865,841,2133,2,3,16,7,6])).
% 61.02/61.04 cnf(2452,plain,
% 61.02/61.04 (~P1(f4(f4(a1,a5),a6),f4(a6,f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[10,2428,2357,2253,2425,2097,2092,2,3,16,7])).
% 61.02/61.04 cnf(2454,plain,
% 61.02/61.04 (~P1(f4(f4(a1,a5),f4(a1,a2)),f4(f4(a1,a2),f4(a1,a2)))),
% 61.02/61.04 inference(scs_inference,[],[10,2428,2357,2253,2425,2097,2092,2078,2,3,16,7,6])).
% 61.02/61.04 cnf(2464,plain,
% 61.02/61.04 (P1(f4(a1,a2),x24641)),
% 61.02/61.04 inference(scs_inference,[],[10,2107,2145,2452,2439,2445,877,1396,2147,2,3,16,7,6])).
% 61.02/61.04 cnf(2467,plain,
% 61.02/61.04 (E(f4(f4(a1,a2),x24671),a6)),
% 61.02/61.04 inference(scs_inference,[],[10,2107,2145,2452,2439,2445,877,1396,2147,2,3,16,7,6,14])).
% 61.02/61.04 cnf(2481,plain,
% 61.02/61.04 (~E(f4(f4(a3,a6),a5),a6)),
% 61.02/61.04 inference(scs_inference,[],[2383,2464,2361,2312,2440,962,1379,2064,2092,2,3,16,7,6,15,64])).
% 61.02/61.04 cnf(2494,plain,
% 61.02/61.04 (~P1(f4(a1,a6),f4(f4(a1,a6),f4(a2,a6)))),
% 61.02/61.04 inference(scs_inference,[],[11,2070,2418,2481,1386,2,3,16])).
% 61.02/61.04 cnf(2526,plain,
% 61.02/61.04 ($false),
% 61.02/61.04 inference(scs_inference,[],[2494,2194,2454,2341,2467,2069,2184,2078,10,2,3,16,7,6,64]),
% 61.02/61.04 ['proof']).
% 61.02/61.04 % SZS output end Proof
% 61.02/61.04 % Total time :60.370000s
%------------------------------------------------------------------------------