%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN008-5 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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:51 EDT 2024
% Result : Unsatisfiable 180.89s 180.92s
% Output : CNFRefutation 180.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : HEN008-5 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.36 % Computer : n020.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Sat Jun 22 05:36:39 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.51/0.62 start to proof:theBenchmark
% 180.89/180.91 %-------------------------------------------
% 180.89/180.91 % File :CSE---1.7
% 180.89/180.91 % Problem :theBenchmark
% 180.89/180.91 % Transform :cnf
% 180.89/180.91 % Format :tptp:raw
% 180.89/180.91 % Command :java -jar mcs_scs.jar %d %s
% 180.89/180.91
% 180.89/180.91 % Result :Theorem 180.250000s
% 180.89/180.91 % Output :CNFRefutation 180.250000s
% 180.89/180.91 %-------------------------------------------
% 180.89/180.92 %--------------------------------------------------------------------------
% 180.89/180.92 % File : HEN008-5 : TPTP v8.2.0. Released v1.0.0.
% 180.89/180.92 % Domain : Henkin Models
% 180.89/180.92 % Problem : X <= Y => X/Z <= Y/Z
% 180.89/180.92 % Version : [MOW76] (equality) axioms : Reduced & Augmented > Complete.
% 180.89/180.92 % English :
% 180.89/180.92
% 180.89/180.92 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 180.89/180.92 % Source : [ANL]
% 180.89/180.92 % Names : hp8.ver3.in [ANL]
% 180.89/180.92
% 180.89/180.92 % Status : Unsatisfiable
% 180.89/180.92 % Rating : 0.00 v6.3.0, 0.10 v6.2.0, 0.30 v6.1.0, 0.18 v6.0.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.11 v5.3.0, 0.30 v5.2.0, 0.12 v5.1.0, 0.11 v5.0.0, 0.00 v2.0.0
% 180.89/180.92 % Syntax : Number of clauses : 7 ( 6 unt; 0 nHn; 3 RR)
% 180.89/180.92 % Number of literals : 9 ( 9 equ; 3 neg)
% 180.89/180.92 % Maximal clause size : 3 ( 1 avg)
% 180.89/180.92 % Maximal term depth : 4 ( 1 avg)
% 180.89/180.92 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 180.89/180.92 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 180.89/180.92 % Number of variables : 9 ( 3 sgn)
% 180.89/180.92 % SPC : CNF_UNS_RFO_PEQ_NUE
% 180.89/180.92
% 180.89/180.92 % Comments : less_equal replaced by divides
% 180.89/180.92 %--------------------------------------------------------------------------
% 180.89/180.92 %----Include Henkin model axioms, for the equality formulation with
% 180.89/180.92 %----less_equals removed.
% 180.89/180.92 include('Axioms/HEN003-0.ax').
% 180.89/180.92 %--------------------------------------------------------------------------
% 180.89/180.92 cnf(a_divide_b_is_zero,hypothesis,
% 180.89/180.92 divide(a,b) = zero ).
% 180.89/180.92
% 180.89/180.92 cnf(prove_property_of_divide3,negated_conjecture,
% 180.89/180.92 divide(divide(a,c),divide(b,c)) != zero ).
% 180.89/180.92
% 180.89/180.92 %--------------------------------------------------------------------------
% 180.89/180.92 %-------------------------------------------
% 180.89/180.92 % Proof found
% 180.89/180.92 % SZS status Theorem for theBenchmark
% 180.89/180.92 % SZS output start Proof
% 180.89/180.92 %ClaNum:12(EqnAxiom:5)
% 180.89/180.92 %VarNum:18(SingletonVarNum:9)
% 180.89/180.92 %MaxLitNum:3
% 180.89/180.92 %MaxfuncDepth:3
% 180.89/180.92 %SharedTerms:11
% 180.89/180.92 %goalClause: 11
% 180.89/180.92 %singleGoalClaCount:1
% 180.89/180.92 [6]E(f3(a1,a2),a5)
% 180.89/180.92 [11]~E(f3(f3(a1,a4),f3(a2,a4)),a5)
% 180.89/180.92 [7]E(f3(x71,a6),a5)
% 180.89/180.92 [8]E(f3(a5,x81),a5)
% 180.89/180.92 [9]E(f3(f3(x91,x92),x91),a5)
% 180.89/180.92 [10]E(f3(f3(f3(x101,x102),f3(x103,x102)),f3(f3(x101,x103),x102)),a5)
% 180.89/180.92 [12]E(x121,x122)+~E(f3(x122,x121),a5)+~E(f3(x121,x122),a5)
% 180.89/180.92 %EqnAxiom
% 180.89/180.92 [1]E(x11,x11)
% 180.89/180.92 [2]E(x22,x21)+~E(x21,x22)
% 180.89/180.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 180.89/180.92 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 180.89/180.92 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 180.89/180.92
% 180.89/180.92 %-------------------------------------------
% 180.89/180.94 cnf(13,plain,
% 180.89/180.94 (E(a5,f3(x131,a6))),
% 180.89/180.94 inference(scs_inference,[],[7,2])).
% 180.89/180.94 cnf(14,plain,
% 180.89/180.94 (E(a5,f3(a5,x141))),
% 180.89/180.94 inference(scs_inference,[],[7,8,9,2,12])).
% 180.89/180.94 cnf(19,plain,
% 180.89/180.94 (~E(f3(a2,a4),a6)),
% 180.89/180.94 inference(scs_inference,[],[11,7,8,9,2,12,3,5])).
% 180.89/180.94 cnf(20,plain,
% 180.89/180.94 (E(a5,f3(a1,a2))),
% 180.89/180.94 inference(scs_inference,[],[6,2])).
% 180.89/180.94 cnf(21,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(a1,a2))),
% 180.89/180.94 inference(scs_inference,[],[11,6,2,3])).
% 180.89/180.94 cnf(22,plain,
% 180.89/180.94 (E(a2,a1)+~E(f3(a2,a1),a5)),
% 180.89/180.94 inference(scs_inference,[],[11,6,2,3,12])).
% 180.89/180.94 cnf(24,plain,
% 180.89/180.94 (E(a5,f3(f3(f3(x241,x242),f3(x243,x242)),f3(f3(x241,x243),x242)))),
% 180.89/180.94 inference(scs_inference,[],[10,2])).
% 180.89/180.94 cnf(25,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(f3(x251,x252),f3(x253,x252)),f3(f3(x251,x253),x252)))),
% 180.89/180.94 inference(scs_inference,[],[11,10,2,3])).
% 180.89/180.94 cnf(26,plain,
% 180.89/180.94 (E(f3(f3(x261,x262),x263),f3(f3(x261,x263),f3(x262,x263)))+~E(f3(f3(f3(x261,x262),x263),f3(f3(x261,x263),f3(x262,x263))),a5)),
% 180.89/180.94 inference(scs_inference,[],[11,10,2,3,12])).
% 180.89/180.94 cnf(28,plain,
% 180.89/180.94 (E(a5,f3(f3(x281,x282),x281))),
% 180.89/180.94 inference(scs_inference,[],[9,2])).
% 180.89/180.94 cnf(29,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(a5,x291))),
% 180.89/180.94 inference(scs_inference,[],[11,8,9,2,3])).
% 180.89/180.94 cnf(30,plain,
% 180.89/180.94 (~E(f3(a1,a4),a5)),
% 180.89/180.94 inference(scs_inference,[],[11,8,9,2,3,4])).
% 180.89/180.94 cnf(34,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(x341,x342),x341))),
% 180.89/180.94 inference(scs_inference,[],[11,9,3])).
% 180.89/180.94 cnf(35,plain,
% 180.89/180.94 (~E(f3(a2,a4),a1)),
% 180.89/180.94 inference(scs_inference,[],[11,9,3,5])).
% 180.89/180.94 cnf(39,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(f3(a2,a4),x391))),
% 180.89/180.94 inference(scs_inference,[],[34,4])).
% 180.89/180.94 cnf(41,plain,
% 180.89/180.94 (~E(a1,f3(a2,a4))),
% 180.89/180.94 inference(scs_inference,[],[39,4])).
% 180.89/180.94 cnf(56,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(a1,a2))),
% 180.89/180.94 inference(scs_inference,[],[30,6,3])).
% 180.89/180.94 cnf(59,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(f3(f3(x591,x592),f3(x593,x592)),f3(f3(x591,x593),x592)))),
% 180.89/180.94 inference(scs_inference,[],[30,10,3])).
% 180.89/180.94 cnf(61,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(x611,a6))),
% 180.89/180.94 inference(scs_inference,[],[30,7,3])).
% 180.89/180.94 cnf(62,plain,
% 180.89/180.94 (~E(a4,a6)),
% 180.89/180.94 inference(scs_inference,[],[30,7,3,5])).
% 180.89/180.94 cnf(63,plain,
% 180.89/180.94 (E(a6,a1)+~E(f3(a6,a1),a5)),
% 180.89/180.94 inference(scs_inference,[],[30,7,3,5,12])).
% 180.89/180.94 cnf(67,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(a5,x671))),
% 180.89/180.94 inference(scs_inference,[],[30,8,3])).
% 180.89/180.94 cnf(68,plain,
% 180.89/180.94 (~E(a1,a5)),
% 180.89/180.94 inference(scs_inference,[],[30,8,3,4])).
% 180.89/180.94 cnf(73,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(f3(x731,x732),x731))),
% 180.89/180.94 inference(scs_inference,[],[30,9,3])).
% 180.89/180.94 cnf(74,plain,
% 180.89/180.94 (~E(a1,f3(a4,x741))),
% 180.89/180.94 inference(scs_inference,[],[30,9,3,4])).
% 180.89/180.94 cnf(90,plain,
% 180.89/180.94 (~E(a1,f3(a1,a2))),
% 180.89/180.94 inference(scs_inference,[],[68,6,3])).
% 180.89/180.94 cnf(93,plain,
% 180.89/180.94 (~E(a1,f3(a5,x931))),
% 180.89/180.94 inference(scs_inference,[],[68,8,3])).
% 180.89/180.94 cnf(95,plain,
% 180.89/180.94 (~E(a1,f3(f3(x951,x952),x951))),
% 180.89/180.94 inference(scs_inference,[],[68,9,3])).
% 180.89/180.94 cnf(100,plain,
% 180.89/180.94 (E(f3(x1001,f3(a5,x1002)),f3(x1001,a5))),
% 180.89/180.94 inference(scs_inference,[],[14,2,5])).
% 180.89/180.94 cnf(101,plain,
% 180.89/180.94 (E(f3(x1011,a5),f3(x1011,f3(a5,x1012)))),
% 180.89/180.94 inference(scs_inference,[],[100,2])).
% 180.89/180.94 cnf(106,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(f3(a5,x1061),x1062),a5))),
% 180.89/180.94 inference(scs_inference,[],[101,34,3])).
% 180.89/180.94 cnf(109,plain,
% 180.89/180.94 (E(f3(f3(a5,x1091),x1092),f3(a5,x1092))),
% 180.89/180.94 inference(scs_inference,[],[14,2,4])).
% 180.89/180.94 cnf(110,plain,
% 180.89/180.94 (E(f3(a5,x1101),f3(f3(a5,x1102),x1101))),
% 180.89/180.94 inference(scs_inference,[],[109,2])).
% 180.89/180.94 cnf(112,plain,
% 180.89/180.94 (~E(f3(a5,f3(a5,x1121)),a1)),
% 180.89/180.94 inference(scs_inference,[],[93,101,2,3])).
% 180.89/180.94 cnf(116,plain,
% 180.89/180.94 (~E(a1,f3(f3(f3(a5,x1161),x1162),a5))),
% 180.89/180.94 inference(scs_inference,[],[95,101,3])).
% 180.89/180.94 cnf(119,plain,
% 180.89/180.94 (E(a1,a2)+~E(f3(a2,a1),a5)),
% 180.89/180.94 inference(scs_inference,[],[22,2])).
% 180.89/180.94 cnf(120,plain,
% 180.89/180.94 (~E(a5,f3(a2,a1))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[119,2])).
% 180.89/180.94 cnf(121,plain,
% 180.89/180.94 (~E(f3(a5,x1211),f3(a2,a1))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[14,120,3])).
% 180.89/180.94 cnf(122,plain,
% 180.89/180.94 (~E(a5,a2)+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[121,4])).
% 180.89/180.94 cnf(123,plain,
% 180.89/180.94 (~E(a2,a5)+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[122,2])).
% 180.89/180.94 cnf(126,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(f3(a5,x1261),x1262),f3(a5,x1263)))),
% 180.89/180.94 inference(scs_inference,[],[106,100,3])).
% 180.89/180.94 cnf(135,plain,
% 180.89/180.94 (~E(a1,f3(f3(f3(a5,x1351),x1352),f3(a5,x1353)))),
% 180.89/180.94 inference(scs_inference,[],[116,100,3])).
% 180.89/180.94 cnf(154,plain,
% 180.89/180.94 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(a5,x1541),x1542))),
% 180.89/180.94 inference(scs_inference,[],[29,109,3])).
% 180.89/180.94 cnf(166,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(f3(a5,x1661),x1662))),
% 180.89/180.94 inference(scs_inference,[],[67,109,3])).
% 180.89/180.94 cnf(171,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(f3(f3(a5,x1711),x1712),a5))),
% 180.89/180.94 inference(scs_inference,[],[73,101,3])).
% 180.89/180.94 cnf(182,plain,
% 180.89/180.94 (~E(a2,f3(a2,a4))+~E(a5,a2)),
% 180.89/180.94 inference(scs_inference,[],[41,122,3])).
% 180.89/180.94 cnf(183,plain,
% 180.89/180.94 (~E(f3(a2,a4),a2)+~E(a5,a2)),
% 180.89/180.94 inference(scs_inference,[],[182,2])).
% 180.89/180.94 cnf(184,plain,
% 180.89/180.94 (~E(a5,a2)+~E(f3(a2,f3(a2,a4)),a5)),
% 180.89/180.94 inference(scs_inference,[],[9,183,12])).
% 180.89/180.94 cnf(185,plain,
% 180.89/180.94 (~E(a5,f3(a2,f3(a2,a4)))+~E(a5,a2)),
% 180.89/180.94 inference(scs_inference,[],[184,2])).
% 180.89/180.94 cnf(186,plain,
% 180.89/180.94 (~E(f3(a5,x1861),f3(a2,f3(a2,a4)))+~E(a5,a2)),
% 180.89/180.94 inference(scs_inference,[],[14,185,3])).
% 180.89/180.94 cnf(187,plain,
% 180.89/180.94 (~E(a5,a2)),
% 180.89/180.94 inference(scs_inference,[],[186,4])).
% 180.89/180.94 cnf(194,plain,
% 180.89/180.94 (~E(f3(a1,a4),f3(f3(f3(a5,x1941),x1942),f3(a5,x1943)))),
% 180.89/180.94 inference(scs_inference,[],[171,100,3])).
% 180.89/180.94 cnf(298,plain,
% 180.89/180.94 (~E(a2,f3(x2981,a6))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[7,123,3])).
% 180.89/180.94 cnf(299,plain,
% 180.89/180.94 (~E(f3(x2991,a6),a2)+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[298,2])).
% 180.89/180.94 cnf(300,plain,
% 180.89/180.94 (E(a1,a2)+~E(f3(a2,f3(a2,a6)),a5)),
% 180.89/180.94 inference(scs_inference,[],[9,299,12])).
% 180.89/180.94 cnf(301,plain,
% 180.89/180.94 (~E(a5,f3(a2,f3(a2,a6)))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[300,2])).
% 180.89/180.94 cnf(302,plain,
% 180.89/180.94 (~E(f3(x3021,a6),f3(a2,f3(a2,a6)))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[13,301,3])).
% 180.89/180.94 cnf(303,plain,
% 180.89/180.94 (~E(a6,f3(a2,a6))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[302,5])).
% 180.89/180.94 cnf(304,plain,
% 180.89/180.94 (~E(f3(a2,a6),a6)+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[303,2])).
% 180.89/180.94 cnf(305,plain,
% 180.89/180.94 (E(a1,a2)+~E(f3(a6,f3(a2,a6)),a5)),
% 180.89/180.94 inference(scs_inference,[],[7,304,12])).
% 180.89/180.94 cnf(306,plain,
% 180.89/180.94 (~E(a5,f3(a6,f3(a2,a6)))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[305,2])).
% 180.89/180.94 cnf(307,plain,
% 180.89/180.94 (~E(f3(a5,x3071),f3(a6,f3(a2,a6)))+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[14,306,3])).
% 180.89/180.94 cnf(308,plain,
% 180.89/180.94 (~E(a5,a6)+E(a1,a2)),
% 180.89/180.94 inference(scs_inference,[],[307,4])).
% 180.89/180.94 cnf(535,plain,
% 180.89/180.94 (E(a2,a1)+~E(a5,a6)),
% 180.89/180.94 inference(scs_inference,[],[308,2])).
% 180.89/180.94 cnf(1046,plain,
% 180.89/180.94 (~E(a1,x10461)+E(a2,x10461)+~E(a5,a6)),
% 180.89/180.94 inference(scs_inference,[],[535,3])).
% 180.89/180.94 cnf(1657,plain,
% 180.89/180.94 (E(a1,a6)+~E(f3(a6,a1),a5)),
% 180.89/180.94 inference(scs_inference,[],[63,2])).
% 180.89/180.94 cnf(1658,plain,
% 180.89/180.94 (~E(a5,f3(a6,a1))+E(a1,a6)),
% 180.89/180.94 inference(scs_inference,[],[1657,2])).
% 180.89/180.94 cnf(1659,plain,
% 180.89/180.94 (~E(f3(a5,x16591),f3(a6,a1))+E(a1,a6)),
% 180.89/180.94 inference(scs_inference,[],[14,1658,3])).
% 180.89/180.94 cnf(1660,plain,
% 180.89/180.94 (~E(a5,a6)+E(a1,a6)),
% 180.89/180.94 inference(scs_inference,[],[1659,4])).
% 180.89/180.94 cnf(1764,plain,
% 180.89/180.94 (~E(a5,a6)+E(a2,a6)),
% 180.89/180.94 inference(scs_inference,[],[1660,1046])).
% 180.89/180.94 cnf(1868,plain,
% 180.89/180.94 (E(a6,a2)+~E(a5,a6)),
% 180.89/180.94 inference(scs_inference,[],[1764,2])).
% 180.89/180.94 cnf(1964,plain,
% 180.89/180.94 (~E(a5,a6)),
% 180.89/180.94 inference(scs_inference,[],[187,1868,3])).
% 180.89/180.94 cnf(2566,plain,
% 180.89/180.94 (E(f3(x25661,f3(a1,a2)),f3(x25661,a5))),
% 180.89/180.94 inference(scs_inference,[],[6,5])).
% 180.89/180.94 cnf(2567,plain,
% 180.89/180.94 (E(f3(f3(a1,a2),x25671),f3(a5,x25671))),
% 180.89/180.94 inference(scs_inference,[],[6,5,4])).
% 180.89/180.94 cnf(2569,plain,
% 180.89/180.94 (~E(f3(a6,a4),a5)),
% 180.89/180.94 inference(scs_inference,[],[6,62,7,5,4,2,12])).
% 180.89/180.94 cnf(2572,plain,
% 180.89/180.94 (E(f3(a1,a2),f3(x25721,a6))),
% 180.89/180.94 inference(scs_inference,[],[6,62,13,7,5,4,2,12,3])).
% 180.89/180.94 cnf(2574,plain,
% 180.89/180.94 (E(f3(x25741,f3(a1,a2)),f3(x25741,f3(x25742,a6)))),
% 180.89/180.94 inference(scs_inference,[],[2572,5])).
% 180.89/180.94 cnf(2575,plain,
% 180.89/180.94 (E(f3(f3(a1,a2),x25751),f3(f3(x25752,a6),x25751))),
% 180.89/180.94 inference(scs_inference,[],[2572,5,4])).
% 180.89/180.94 cnf(2576,plain,
% 180.89/180.94 (~E(a6,a5)),
% 180.89/180.94 inference(scs_inference,[],[1964,2572,5,4,2])).
% 180.89/180.94 cnf(2577,plain,
% 180.89/180.94 (~E(f3(a6,a5),a5)),
% 180.89/180.94 inference(scs_inference,[],[1964,2572,7,5,4,2,12])).
% 180.89/180.94 cnf(2580,plain,
% 180.89/180.94 (E(f3(a1,a2),f3(f3(x25801,x25802),x25801))),
% 180.89/180.94 inference(scs_inference,[],[6,1964,2572,28,7,5,4,2,12,3])).
% 180.89/180.94 cnf(2582,plain,
% 180.89/180.94 (E(f3(x25821,f3(x25822,f3(a1,a2))),f3(x25821,f3(x25822,a5)))),
% 180.89/180.94 inference(scs_inference,[],[2566,5])).
% 180.89/180.94 cnf(2583,plain,
% 180.89/180.94 (E(f3(f3(x25831,f3(a1,a2)),x25832),f3(f3(x25831,a5),x25832))),
% 180.89/180.94 inference(scs_inference,[],[2566,5,4])).
% 180.89/180.94 cnf(2584,plain,
% 180.89/180.94 (~E(a5,f3(a6,a5))),
% 180.89/180.94 inference(scs_inference,[],[2577,2566,5,4,2])).
% 180.89/180.94 cnf(2585,plain,
% 180.89/180.94 (~E(f3(a6,f3(a2,a4)),a5)),
% 180.89/180.94 inference(scs_inference,[],[19,2577,2566,7,5,4,2,12])).
% 180.89/180.94 cnf(2588,plain,
% 180.89/180.94 (E(f3(f3(a1,a2),f3(a1,a2)),f3(a5,a5))),
% 180.89/180.94 inference(scs_inference,[],[19,2577,2566,2567,7,5,4,2,12,3])).
% 180.89/180.94 cnf(2592,plain,
% 180.89/180.94 (E(f3(x25921,f3(f3(a1,a2),f3(a1,a2))),f3(x25921,f3(a5,a5)))),
% 180.89/180.94 inference(scs_inference,[],[2588,5])).
% 180.89/180.94 cnf(2593,plain,
% 180.89/180.94 (E(f3(f3(f3(a1,a2),f3(a1,a2)),x25931),f3(f3(a5,a5),x25931))),
% 180.89/180.94 inference(scs_inference,[],[2588,5,4])).
% 180.89/180.94 cnf(2594,plain,
% 180.89/180.94 (~E(a5,f3(a6,a4))),
% 180.89/180.94 inference(scs_inference,[],[2569,2588,5,4,2])).
% 180.89/180.94 cnf(2595,plain,
% 180.89/180.94 (~E(f3(f3(a6,a5),a5),a5)),
% 180.89/180.94 inference(scs_inference,[],[2584,2569,2588,8,5,4,2,12])).
% 180.89/180.94 cnf(2598,plain,
% 180.89/180.94 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x25981),a5))),
% 180.89/180.94 inference(scs_inference,[],[2584,2569,2588,110,8,5,4,2,12,3])).
% 180.89/180.94 cnf(2601,plain,
% 180.89/180.94 (E(f3(x26011,f3(a1,a2)),f3(x26011,f3(f3(x26012,x26013),x26012)))),
% 180.89/180.94 inference(scs_inference,[],[2580,5])).
% 180.89/180.94 cnf(2602,plain,
% 180.89/180.94 (E(f3(f3(a1,a2),x26021),f3(f3(f3(x26022,x26023),x26022),x26021))),
% 180.89/180.94 inference(scs_inference,[],[2580,5,4])).
% 180.89/180.94 cnf(2603,plain,
% 180.89/180.94 (~E(f3(a1,a2),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.94 inference(scs_inference,[],[21,2580,5,4,2])).
% 180.89/180.94 cnf(2604,plain,
% 180.89/180.94 (~E(f3(f3(a6,a4),a5),a5)),
% 180.89/180.94 inference(scs_inference,[],[2594,21,2580,8,5,4,2,12])).
% 180.89/180.94 cnf(2607,plain,
% 180.89/180.94 (~E(a5,f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.94 inference(scs_inference,[],[6,2594,21,2580,8,5,4,2,12,3])).
% 180.89/180.94 cnf(2609,plain,
% 180.89/180.94 (E(f3(x26091,f3(f3(a1,a2),x26092)),f3(x26091,f3(a5,x26092)))),
% 180.89/180.94 inference(scs_inference,[],[2567,5])).
% 180.89/180.94 cnf(2610,plain,
% 180.89/180.94 (E(f3(f3(f3(a1,a2),x26101),x26102),f3(f3(a5,x26101),x26102))),
% 180.89/180.94 inference(scs_inference,[],[2567,5,4])).
% 180.89/180.94 cnf(2611,plain,
% 180.89/180.94 (~E(a5,f3(f3(a6,a5),a5))),
% 180.89/180.94 inference(scs_inference,[],[2595,2567,5,4,2])).
% 180.89/180.94 cnf(2612,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a4),f3(a2,a4)),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2595,2607,2567,8,5,4,2,12])).
% 180.89/180.95 cnf(2615,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(x26151,a6),f3(x26152,a6)))),
% 180.89/180.95 inference(scs_inference,[],[2595,2607,2574,2575,2567,8,5,4,2,12,3])).
% 180.89/180.95 cnf(2619,plain,
% 180.89/180.95 (E(f3(x26191,f3(f3(a5,x26192),x26193)),f3(x26191,f3(a5,x26193)))),
% 180.89/180.95 inference(scs_inference,[],[109,5])).
% 180.89/180.95 cnf(2620,plain,
% 180.89/180.95 (E(f3(f3(f3(a5,x26201),x26202),x26203),f3(f3(a5,x26202),x26203))),
% 180.89/180.95 inference(scs_inference,[],[109,5,4])).
% 180.89/180.95 cnf(2621,plain,
% 180.89/180.95 (~E(f3(f3(a5,x26211),x26212),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[166,109,5,4,2])).
% 180.89/180.95 cnf(2622,plain,
% 180.89/180.95 (~E(f3(f3(f3(a6,a5),a5),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2611,166,109,8,5,4,2,12])).
% 180.89/180.95 cnf(2628,plain,
% 180.89/180.95 (E(f3(x26281,a5),f3(x26281,f3(x26282,a6)))),
% 180.89/180.95 inference(scs_inference,[],[13,5])).
% 180.89/180.95 cnf(2629,plain,
% 180.89/180.95 (E(f3(a5,x26291),f3(f3(x26292,a6),x26291))),
% 180.89/180.95 inference(scs_inference,[],[13,5,4])).
% 180.89/180.95 cnf(2630,plain,
% 180.89/180.95 (~E(a5,f3(a6,f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[2585,13,5,4,2])).
% 180.89/180.95 cnf(2635,plain,
% 180.89/180.95 (E(f3(x26351,f3(x26352,a5)),f3(x26351,f3(x26352,f3(x26353,a6))))),
% 180.89/180.95 inference(scs_inference,[],[2628,5])).
% 180.89/180.95 cnf(2636,plain,
% 180.89/180.95 (E(f3(f3(x26361,a5),x26362),f3(f3(x26361,f3(x26363,a6)),x26362))),
% 180.89/180.95 inference(scs_inference,[],[2628,5,4])).
% 180.89/180.95 cnf(2637,plain,
% 180.89/180.95 (~E(a5,f3(f3(a6,a4),a5))),
% 180.89/180.95 inference(scs_inference,[],[2604,2628,5,4,2])).
% 180.89/180.95 cnf(2638,plain,
% 180.89/180.95 (~E(f3(f3(a6,f3(a2,a4)),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2604,2628,2630,8,5,4,2,12])).
% 180.89/180.95 cnf(2641,plain,
% 180.89/180.95 (~E(f3(f3(x26411,a6),f3(a5,x26412)),a1)),
% 180.89/180.95 inference(scs_inference,[],[2604,2628,2629,2630,112,8,5,4,2,12,3])).
% 180.89/180.95 cnf(2644,plain,
% 180.89/180.95 (E(f3(x26441,f3(a5,x26442)),f3(x26441,f3(f3(x26443,a6),x26442)))),
% 180.89/180.95 inference(scs_inference,[],[2629,5])).
% 180.89/180.95 cnf(2645,plain,
% 180.89/180.95 (E(f3(f3(a5,x26451),x26452),f3(f3(f3(x26453,a6),x26451),x26452))),
% 180.89/180.95 inference(scs_inference,[],[2629,5,4])).
% 180.89/180.95 cnf(2647,plain,
% 180.89/180.95 (~E(f3(f3(f3(a6,a4),a5),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2637,2641,2629,8,5,4,2,12])).
% 180.89/180.95 cnf(2650,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(f3(a1,a2),x26501)),f3(f3(f3(x26502,x26503),x26502),f3(a5,x26501)))),
% 180.89/180.95 inference(scs_inference,[],[2637,2641,2609,2602,2629,8,5,4,2,12,3])).
% 180.89/180.95 cnf(2654,plain,
% 180.89/180.95 (E(f3(x26541,a5),f3(x26541,f3(f3(x26542,x26543),x26542)))),
% 180.89/180.95 inference(scs_inference,[],[28,5])).
% 180.89/180.95 cnf(2655,plain,
% 180.89/180.95 (E(f3(a5,x26551),f3(f3(f3(x26552,x26553),x26552),x26551))),
% 180.89/180.95 inference(scs_inference,[],[28,5,4])).
% 180.89/180.95 cnf(2656,plain,
% 180.89/180.95 (~E(f3(f3(f3(a5,x26561),x26562),f3(a5,x26563)),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[194,28,5,4,2])).
% 180.89/180.95 cnf(2657,plain,
% 180.89/180.95 (~E(f3(f3(f3(x26571,a6),x26572),x26573),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[2621,194,2645,28,5,4,2,3])).
% 180.89/180.95 cnf(2660,plain,
% 180.89/180.95 (E(f3(x26601,f3(x26602,a6)),f3(x26601,a5))),
% 180.89/180.95 inference(scs_inference,[],[7,5])).
% 180.89/180.95 cnf(2661,plain,
% 180.89/180.95 (E(f3(f3(x26611,a6),x26612),f3(a5,x26612))),
% 180.89/180.95 inference(scs_inference,[],[7,5,4])).
% 180.89/180.95 cnf(2662,plain,
% 180.89/180.95 (~E(f3(f3(a5,x26621),x26622),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[7,154,5,4,2])).
% 180.89/180.95 cnf(2663,plain,
% 180.89/180.95 (~E(a5,f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[7,154,2657,5,4,2,3])).
% 180.89/180.95 cnf(2667,plain,
% 180.89/180.95 (E(f3(x26671,f3(x26672,f3(x26673,a6))),f3(x26671,f3(x26672,a5)))),
% 180.89/180.95 inference(scs_inference,[],[2660,5])).
% 180.89/180.95 cnf(2668,plain,
% 180.89/180.95 (E(f3(f3(x26681,f3(x26682,a6)),x26683),f3(f3(x26681,a5),x26683))),
% 180.89/180.95 inference(scs_inference,[],[2660,5,4])).
% 180.89/180.95 cnf(2669,plain,
% 180.89/180.95 (~E(f3(f3(f3(a5,x26691),x26692),f3(a5,x26693)),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[2660,126,5,4,2])).
% 180.89/180.95 cnf(2673,plain,
% 180.89/180.95 (~E(f3(f3(a1,a4),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2663,2660,2656,126,8,5,4,2,3,12])).
% 180.89/180.95 cnf(2680,plain,
% 180.89/180.95 (E(f3(x26801,f3(f3(x26802,a6),x26803)),f3(x26801,f3(a5,x26803)))),
% 180.89/180.95 inference(scs_inference,[],[2661,5])).
% 180.89/180.95 cnf(2682,plain,
% 180.89/180.95 (~E(a5,f3(f3(a1,a4),a5))),
% 180.89/180.95 inference(scs_inference,[],[2673,2661,5,4,2])).
% 180.89/180.95 cnf(2683,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x26831),f3(f3(x26832,x26833),x26832)))),
% 180.89/180.95 inference(scs_inference,[],[2673,2598,2654,2661,5,4,2,3])).
% 180.89/180.95 cnf(2686,plain,
% 180.89/180.95 (E(f3(x26861,f3(a5,x26862)),f3(x26861,f3(f3(a5,x26863),x26862)))),
% 180.89/180.95 inference(scs_inference,[],[110,5])).
% 180.89/180.95 cnf(2687,plain,
% 180.89/180.95 (E(f3(f3(a5,x26871),x26872),f3(f3(f3(a5,x26873),x26871),x26872))),
% 180.89/180.95 inference(scs_inference,[],[110,5,4])).
% 180.89/180.95 cnf(2688,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a6,a5),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[2622,110,5,4,2])).
% 180.89/180.95 cnf(2689,plain,
% 180.89/180.95 (~E(f3(f3(f3(x26891,x26892),x26891),f3(a5,x26893)),a1)),
% 180.89/180.95 inference(scs_inference,[],[2622,2655,112,110,5,4,2,3])).
% 180.89/180.95 cnf(2691,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a4),a5),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2682,2622,2655,112,110,8,5,4,2,3,12])).
% 180.89/180.95 cnf(2695,plain,
% 180.89/180.95 (E(f3(x26951,f3(f3(x26952,x26953),x26952)),f3(x26951,a5))),
% 180.89/180.95 inference(scs_inference,[],[9,5])).
% 180.89/180.95 cnf(2696,plain,
% 180.89/180.95 (E(f3(f3(f3(x26961,x26962),x26961),x26963),f3(a5,x26963))),
% 180.89/180.95 inference(scs_inference,[],[9,5,4])).
% 180.89/180.95 cnf(2698,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x26981),f3(a5,a5)))),
% 180.89/180.95 inference(scs_inference,[],[2689,2619,2683,9,5,4,2,3])).
% 180.89/180.95 cnf(2701,plain,
% 180.89/180.95 (E(f3(x27011,a5),f3(x27011,f3(a1,a2)))),
% 180.89/180.95 inference(scs_inference,[],[20,5])).
% 180.89/180.95 cnf(2702,plain,
% 180.89/180.95 (E(f3(a5,x27021),f3(f3(a1,a2),x27021))),
% 180.89/180.95 inference(scs_inference,[],[20,5,4])).
% 180.89/180.95 cnf(2703,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a1,a4),f3(a2,a4)),a5))),
% 180.89/180.95 inference(scs_inference,[],[2612,20,5,4,2])).
% 180.89/180.95 cnf(2704,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x27041),f3(a5,f3(x27042,a6))))),
% 180.89/180.95 inference(scs_inference,[],[2698,2612,2635,20,5,4,2,3])).
% 180.89/180.95 cnf(2707,plain,
% 180.89/180.95 (E(f3(x27071,f3(x27072,a5)),f3(x27071,f3(x27072,f3(a1,a2))))),
% 180.89/180.95 inference(scs_inference,[],[2701,5])).
% 180.89/180.95 cnf(2708,plain,
% 180.89/180.95 (E(f3(f3(x27081,a5),x27082),f3(f3(x27081,f3(a1,a2)),x27082))),
% 180.89/180.95 inference(scs_inference,[],[2701,5,4])).
% 180.89/180.95 cnf(2709,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a1,a4),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[2701,2691,5,4,2])).
% 180.89/180.95 cnf(2710,plain,
% 180.89/180.95 (~E(f3(f3(a1,a2),f3(a5,x27101)),a1)),
% 180.89/180.95 inference(scs_inference,[],[2701,2702,2691,112,5,4,2,3])).
% 180.89/180.95 cnf(2713,plain,
% 180.89/180.95 (E(f3(x27131,f3(a5,x27132)),f3(x27131,f3(f3(a1,a2),x27132)))),
% 180.89/180.95 inference(scs_inference,[],[2702,5])).
% 180.89/180.95 cnf(2714,plain,
% 180.89/180.95 (E(f3(f3(a5,x27141),x27142),f3(f3(f3(a1,a2),x27141),x27142))),
% 180.89/180.95 inference(scs_inference,[],[2702,5,4])).
% 180.89/180.95 cnf(2715,plain,
% 180.89/180.95 (~E(a1,f3(f3(a1,a2),f3(a5,x27151)))),
% 180.89/180.95 inference(scs_inference,[],[2710,2702,5,4,2])).
% 180.89/180.95 cnf(2716,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(x27161,a6),a5))),
% 180.89/180.95 inference(scs_inference,[],[2710,2615,2695,2702,5,4,2,3])).
% 180.89/180.95 cnf(2719,plain,
% 180.89/180.95 (E(f3(x27191,f3(x27192,a5)),f3(x27191,f3(x27192,f3(a5,x27193))))),
% 180.89/180.95 inference(scs_inference,[],[101,5])).
% 180.89/180.95 cnf(2720,plain,
% 180.89/180.95 (E(f3(f3(x27201,a5),x27202),f3(f3(x27201,f3(a5,x27203)),x27202))),
% 180.89/180.95 inference(scs_inference,[],[101,5,4])).
% 180.89/180.95 cnf(2721,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a6,a4),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[2647,101,5,4,2])).
% 180.89/180.95 cnf(2722,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a2),x27221),x27222),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[2662,2647,2714,101,5,4,2,3])).
% 180.89/180.95 cnf(2725,plain,
% 180.89/180.95 (E(f3(x27251,f3(x27252,f3(a5,x27253))),f3(x27251,f3(x27252,a5)))),
% 180.89/180.95 inference(scs_inference,[],[100,5])).
% 180.89/180.95 cnf(2726,plain,
% 180.89/180.95 (E(f3(f3(x27261,f3(a5,x27262)),x27263),f3(f3(x27261,a5),x27263))),
% 180.89/180.95 inference(scs_inference,[],[100,5,4])).
% 180.89/180.95 cnf(2727,plain,
% 180.89/180.95 (~E(a5,f3(f3(a6,f3(a2,a4)),a5))),
% 180.89/180.95 inference(scs_inference,[],[2638,100,5,4,2])).
% 180.89/180.95 cnf(2728,plain,
% 180.89/180.95 (~E(f3(f3(f3(a5,x27281),x27282),f3(f3(a1,a2),x27283)),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[2669,2638,2713,100,5,4,2,3])).
% 180.89/180.95 cnf(2732,plain,
% 180.89/180.95 (~E(f3(f3(f3(a5,x27321),x27322),x27323),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[2722,2687,2621,2,3])).
% 180.89/180.95 cnf(2736,plain,
% 180.89/180.95 (~E(a5,a1)),
% 180.89/180.95 inference(scs_inference,[],[8,2732,112,2,3])).
% 180.89/180.95 cnf(2739,plain,
% 180.89/180.95 (~E(f3(f3(f3(x27391,x27392),f3(x27393,x27392)),f3(f3(x27391,x27393),x27392)),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[59,2])).
% 180.89/180.95 cnf(2740,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(f3(a1,a2),x27401)),f3(f3(a5,a5),f3(a5,x27401)))),
% 180.89/180.95 inference(scs_inference,[],[2620,59,2650,2,3])).
% 180.89/180.95 cnf(2743,plain,
% 180.89/180.95 (~E(f3(a1,a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[8,2736,2620,59,2650,2,3,12])).
% 180.89/180.95 cnf(2747,plain,
% 180.89/180.95 (~E(a5,f3(a1,a5))),
% 180.89/180.95 inference(scs_inference,[],[2743,2])).
% 180.89/180.95 cnf(2748,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(f3(a1,a2),f3(x27481,a6))),f3(f3(a5,a5),f3(a5,a5)))),
% 180.89/180.95 inference(scs_inference,[],[2743,2740,2667,2,3])).
% 180.89/180.95 cnf(2753,plain,
% 180.89/180.95 (~E(f3(f3(a1,a5),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[8,2747,2728,2,12])).
% 180.89/180.95 cnf(2756,plain,
% 180.89/180.95 (~E(f3(f3(f3(x27561,x27562),f3(a6,x27562)),f3(a5,x27562)),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[8,2747,2739,2680,2728,2,12,3])).
% 180.89/180.95 cnf(2760,plain,
% 180.89/180.95 (~E(a5,f3(f3(a1,a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[2753,2])).
% 180.89/180.95 cnf(2761,plain,
% 180.89/180.95 (~E(f3(f3(f3(x27611,f3(a5,x27612)),f3(a6,f3(a5,x27612))),f3(a5,a5)),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[2753,2756,2725,2,3])).
% 180.89/180.95 cnf(2766,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a5),a5),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[8,2760,2761,2,12])).
% 180.89/180.95 cnf(2769,plain,
% 180.89/180.95 (~E(f3(f3(a6,f3(x27691,a6)),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[8,2760,2636,2761,2595,2,12,3])).
% 180.89/180.95 cnf(2771,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a1,a5),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[2766,2])).
% 180.89/180.95 cnf(2772,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a5),f3(a5,x27721)),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2766,2720,2,3])).
% 180.89/180.95 cnf(2774,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a1,a5),f3(a5,x27741)),a5))),
% 180.89/180.95 inference(scs_inference,[],[2772,2])).
% 180.89/180.95 cnf(2775,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x27751),f3(f3(x27752,a6),f3(x27753,a6))))),
% 180.89/180.95 inference(scs_inference,[],[2772,2644,2704,2,3])).
% 180.89/180.95 cnf(2778,plain,
% 180.89/180.95 (~E(a5,f3(f3(a6,f3(x27781,a6)),a5))),
% 180.89/180.95 inference(scs_inference,[],[2769,2])).
% 180.89/180.95 cnf(2779,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x27791),f3(a5,f3(a1,a2))))),
% 180.89/180.95 inference(scs_inference,[],[2769,2707,2698,2,3])).
% 180.89/180.95 cnf(2782,plain,
% 180.89/180.95 (~E(f3(f3(f3(x27821,x27822),f3(x27823,x27822)),f3(f3(x27821,x27823),x27822)),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[25,2])).
% 180.89/180.95 cnf(2783,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(a5,x27831),f3(f3(a5,x27832),f3(a1,a2))))),
% 180.89/180.95 inference(scs_inference,[],[2779,2686,25,2,3])).
% 180.89/180.95 cnf(2786,plain,
% 180.89/180.95 (~E(f3(a1,a2),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[56,2])).
% 180.89/180.95 cnf(2787,plain,
% 180.89/180.95 (~E(f3(f3(f3(x27871,a5),f3(x27872,a5)),f3(f3(x27871,x27872),f3(a5,x27873))),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.95 inference(scs_inference,[],[2719,2782,56,2,3])).
% 180.89/180.95 cnf(2792,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),a5)),
% 180.89/180.95 inference(scs_inference,[],[9,2716,2787,2,3])).
% 180.89/180.95 cnf(2795,plain,
% 180.89/180.95 (E(f3(x27951,f3(f3(a1,a2),f3(a1,a2))),f3(x27951,a5))),
% 180.89/180.95 inference(scs_inference,[],[9,2716,2787,2,3,5])).
% 180.89/180.95 cnf(2796,plain,
% 180.89/180.95 (E(f3(f3(f3(a1,a2),f3(a1,a2)),x27961),f3(a5,x27961))),
% 180.89/180.95 inference(scs_inference,[],[9,2716,2787,2,3,5,4])).
% 180.89/180.95 cnf(2798,plain,
% 180.89/180.95 (~E(f3(x27981,a6),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[61,2])).
% 180.89/180.95 cnf(2800,plain,
% 180.89/180.95 (E(f3(x28001,f3(f3(a1,a2),f3(a1,a2))),f3(x28001,f3(x28002,a6)))),
% 180.89/180.95 inference(scs_inference,[],[2792,61,13,2,3,5])).
% 180.89/180.95 cnf(2801,plain,
% 180.89/180.95 (E(f3(f3(f3(a1,a2),f3(a1,a2)),x28011),f3(f3(x28012,a6),x28011))),
% 180.89/180.95 inference(scs_inference,[],[2792,61,13,2,3,5,4])).
% 180.89/180.95 cnf(2803,plain,
% 180.89/180.95 (~E(f3(a5,x28031),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[67,2])).
% 180.89/180.95 cnf(2804,plain,
% 180.89/180.95 (~E(f3(f3(a1,a4),f3(f3(a1,a4),a6)),a5)),
% 180.89/180.95 inference(scs_inference,[],[9,2798,67,2,12])).
% 180.89/180.95 cnf(2808,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(a1,a2)),f3(f3(x28081,x28082),x28081))),
% 180.89/180.95 inference(scs_inference,[],[9,2798,67,2792,28,2,12,3])).
% 180.89/180.95 cnf(2810,plain,
% 180.89/180.95 (~E(a5,f3(f3(a1,a4),f3(f3(a1,a4),a6)))),
% 180.89/180.95 inference(scs_inference,[],[2804,2])).
% 180.89/180.95 cnf(2811,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),f3(f3(a1,a2),f3(a1,a2))),f3(f3(a5,a5),f3(a5,a5)))),
% 180.89/180.95 inference(scs_inference,[],[2804,2582,2740,2,3])).
% 180.89/180.95 cnf(2814,plain,
% 180.89/180.95 (~E(f3(f3(x28141,x28142),x28141),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[73,2])).
% 180.89/180.95 cnf(2817,plain,
% 180.89/180.95 (E(f3(f3(x28171,x28172),x28171),a5)),
% 180.89/180.95 inference(rename_variables,[],[9])).
% 180.89/180.95 cnf(2818,plain,
% 180.89/180.95 (E(f3(a1,a2),f3(f3(a1,a2),x28181))),
% 180.89/180.95 inference(scs_inference,[],[9,2817,73,2650,2,3,12])).
% 180.89/180.95 cnf(2821,plain,
% 180.89/180.95 (E(f3(x28211,f3(a1,a2)),f3(x28211,f3(f3(a1,a2),x28212)))),
% 180.89/180.95 inference(scs_inference,[],[9,2817,73,2650,2,3,12,5])).
% 180.89/180.95 cnf(2822,plain,
% 180.89/180.95 (E(f3(f3(a1,a2),x28221),f3(f3(f3(a1,a2),x28222),x28221))),
% 180.89/180.95 inference(scs_inference,[],[9,2817,73,2650,2,3,12,5,4])).
% 180.89/180.95 cnf(2825,plain,
% 180.89/180.95 (~E(f3(f3(a1,a4),f3(f3(a1,a4),a1)),a5)),
% 180.89/180.95 inference(scs_inference,[],[9,2814,2756,2,12])).
% 180.89/180.95 cnf(2829,plain,
% 180.89/180.95 (~E(f3(f3(a1,a2),x28291),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[9,2786,2814,2818,2756,2,12,3])).
% 180.89/180.95 cnf(2832,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a2),x28321),x28322),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[2829,2822,2,3])).
% 180.89/180.95 cnf(2836,plain,
% 180.89/180.95 (~E(f3(f3(x28361,a6),x28362),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[2832,2801,2,3])).
% 180.89/180.95 cnf(2842,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a2),a4),f3(f3(a1,a4),f3(a2,a4))),a5)),
% 180.89/180.95 inference(scs_inference,[],[2836,2603,2818,2,3,26])).
% 180.89/180.95 cnf(2849,plain,
% 180.89/180.95 (~E(a5,f3(f3(a1,a4),f3(f3(a1,a4),a1)))),
% 180.89/180.95 inference(scs_inference,[],[2825,2])).
% 180.89/180.95 cnf(2850,plain,
% 180.89/180.95 (~E(f3(f3(f3(x28501,x28502),x28501),x28503),f3(a1,a4))),
% 180.89/180.95 inference(scs_inference,[],[2803,2825,2655,2,3])).
% 180.89/180.95 cnf(2854,plain,
% 180.89/180.95 (~E(f3(x28541,a6),f3(f3(f3(a6,a5),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[2850,2688,13,2,3])).
% 180.89/180.95 cnf(2856,plain,
% 180.89/180.95 (~E(f3(f3(f3(a6,a5),a5),a5),f3(x28561,a6))),
% 180.89/180.95 inference(scs_inference,[],[2854,2])).
% 180.89/180.95 cnf(2857,plain,
% 180.89/180.95 (~E(f3(a6,f3(f3(x28571,x28572),x28571)),a5)),
% 180.89/180.95 inference(scs_inference,[],[2854,2577,2654,2,3])).
% 180.89/180.95 cnf(2859,plain,
% 180.89/180.95 (~E(a5,f3(a6,f3(f3(x28591,x28592),x28591)))),
% 180.89/180.95 inference(scs_inference,[],[2857,2])).
% 180.89/180.95 cnf(2860,plain,
% 180.89/180.95 (~E(f3(a6,f3(a5,a1)),a5)),
% 180.89/180.95 inference(scs_inference,[],[2857,2609,2,3])).
% 180.89/180.95 cnf(2864,plain,
% 180.89/180.95 (~E(a5,f3(a6,f3(a5,a1)))),
% 180.89/180.95 inference(scs_inference,[],[2860,2])).
% 180.89/180.95 cnf(2865,plain,
% 180.89/180.95 (~E(f3(a6,f3(f3(x28651,a6),a1)),a5)),
% 180.89/180.95 inference(scs_inference,[],[2860,2644,2,3])).
% 180.89/180.95 cnf(2868,plain,
% 180.89/180.95 (~E(a5,f3(a6,f3(f3(x28681,a6),a1)))),
% 180.89/180.95 inference(scs_inference,[],[2865,2])).
% 180.89/180.95 cnf(2869,plain,
% 180.89/180.95 (~E(f3(f3(f3(a6,a5),a5),f3(a1,a2)),f3(x28691,a6))),
% 180.89/180.95 inference(scs_inference,[],[2856,2865,2701,2,3])).
% 180.89/180.95 cnf(2871,plain,
% 180.89/180.95 (~E(f3(f3(a6,f3(a5,a1)),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[2864,2856,2865,2701,8,2,3,12])).
% 180.89/180.95 cnf(2876,plain,
% 180.89/180.95 (~E(f3(f3(f3(a6,a5),a5),f3(f3(a1,a2),x28761)),f3(x28762,a6))),
% 180.89/180.95 inference(scs_inference,[],[2869,2821,2,3])).
% 180.89/180.95 cnf(2879,plain,
% 180.89/180.95 (~E(a5,f3(f3(a6,f3(a5,a1)),a5))),
% 180.89/180.95 inference(scs_inference,[],[2871,2])).
% 180.89/180.95 cnf(2880,plain,
% 180.89/180.95 (~E(a6,f3(f3(f3(x28801,x28802),f3(x28803,x28802)),f3(f3(x28801,x28803),x28802)))),
% 180.89/180.95 inference(scs_inference,[],[10,2576,2871,2,3])).
% 180.89/180.95 cnf(2883,plain,
% 180.89/180.95 (~E(f3(f3(f3(a6,a5),a5),f3(x28831,a6)),f3(x28832,a6))),
% 180.89/180.95 inference(scs_inference,[],[2876,2800,2,3])).
% 180.89/180.95 cnf(2888,plain,
% 180.89/180.95 (~E(a1,f3(f3(a1,a2),f3(a1,a2)))),
% 180.89/180.95 inference(scs_inference,[],[2715,2883,2574,2,3])).
% 180.89/180.95 cnf(2893,plain,
% 180.89/180.95 (~E(f3(a1,f3(x28931,a6)),a5)),
% 180.89/180.95 inference(scs_inference,[],[2888,2743,2628,2,3])).
% 180.89/180.95 cnf(2896,plain,
% 180.89/180.95 (~E(a5,f3(a1,f3(x28961,a6)))),
% 180.89/180.95 inference(scs_inference,[],[2893,2])).
% 180.89/180.95 cnf(2899,plain,
% 180.89/180.95 (~E(a5,f3(f3(f3(a1,a2),a4),f3(f3(a1,a4),f3(a2,a4))))),
% 180.89/180.95 inference(scs_inference,[],[2842,2])).
% 180.89/180.95 cnf(2900,plain,
% 180.89/180.95 (~E(f3(x29001,a6),f3(a1,f3(x29002,a6)))),
% 180.89/180.95 inference(scs_inference,[],[13,2896,2842,2,3])).
% 180.89/180.95 cnf(2901,plain,
% 180.89/180.95 (~E(f3(f3(a1,f3(x29011,a6)),a5),a5)),
% 180.89/180.95 inference(scs_inference,[],[13,2896,2842,8,2,3,12])).
% 180.89/180.95 cnf(2905,plain,
% 180.89/180.95 (~E(f3(a1,f3(x29051,a6)),f3(x29052,a6))),
% 180.89/180.95 inference(scs_inference,[],[2900,2])).
% 180.89/180.95 cnf(2906,plain,
% 180.89/180.95 (~E(f3(x29061,a6),f3(f3(f3(a1,a5),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[13,2900,2771,2,3])).
% 180.89/180.95 cnf(2908,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a5),a5),a5),f3(x29081,a6))),
% 180.89/180.95 inference(scs_inference,[],[2906,2])).
% 180.89/180.95 cnf(2909,plain,
% 180.89/180.95 (~E(f3(x29091,a6),f3(f3(a1,a4),f3(f3(a1,a4),a6)))),
% 180.89/180.95 inference(scs_inference,[],[13,2906,2810,2,3])).
% 180.89/180.95 cnf(2910,plain,
% 180.89/180.95 (~E(f3(f3(a1,a4),f3(f3(a1,a4),a6)),f3(x29101,a6))),
% 180.89/180.95 inference(scs_inference,[],[2909,2])).
% 180.89/180.95 cnf(2911,plain,
% 180.89/180.95 (~E(f3(a1,a5),f3(x29111,a6))),
% 180.89/180.95 inference(scs_inference,[],[2905,2909,2695,2,3])).
% 180.89/180.95 cnf(2915,plain,
% 180.89/180.95 (~E(f3(x29151,a6),f3(a1,a5))),
% 180.89/180.95 inference(scs_inference,[],[2911,2])).
% 180.89/180.95 cnf(2916,plain,
% 180.89/180.95 (~E(f3(x29161,a6),f3(f3(a1,a4),f3(f3(a1,a4),a1)))),
% 180.89/180.95 inference(scs_inference,[],[13,2911,2849,2,3])).
% 180.89/180.95 cnf(2919,plain,
% 180.89/180.95 (~E(f3(f3(a1,a4),a5),f3(x29191,a6))),
% 180.89/180.95 inference(scs_inference,[],[2910,2916,2660,2,3])).
% 180.89/180.95 cnf(2921,plain,
% 180.89/180.95 (~E(f3(f3(a1,a5),f3(f3(a1,a5),a6)),a5)),
% 180.89/180.95 inference(scs_inference,[],[2915,2910,2916,2660,9,2,3,12])).
% 180.89/180.95 cnf(2927,plain,
% 180.89/180.95 (~E(f3(x29271,a6),f3(f3(a6,f3(a5,a1)),a5))),
% 180.89/180.95 inference(scs_inference,[],[13,2919,2879,2,3])).
% 180.89/180.95 cnf(2929,plain,
% 180.89/180.95 (~E(f3(f3(a6,f3(a5,a1)),a5),f3(x29291,a6))),
% 180.89/180.95 inference(scs_inference,[],[2927,2])).
% 180.89/180.95 cnf(2934,plain,
% 180.89/180.95 (~E(a5,f3(f3(a1,a5),f3(f3(a1,a5),a6)))),
% 180.89/180.95 inference(scs_inference,[],[2921,2])).
% 180.89/180.95 cnf(2935,plain,
% 180.89/180.95 (~E(f3(x29351,a6),f3(f3(f3(a1,a4),f3(a2,a4)),a5))),
% 180.89/180.95 inference(scs_inference,[],[13,2921,2703,2,3])).
% 180.89/180.95 cnf(2937,plain,
% 180.89/180.95 (~E(f3(f3(f3(a1,a4),f3(a2,a4)),a5),f3(x29371,a6))),
% 180.89/180.95 inference(scs_inference,[],[2935,2])).
% 180.89/180.95 cnf(2938,plain,
% 180.89/180.95 (~E(f3(x29381,a6),f3(f3(a1,a5),f3(f3(a1,a5),a6)))),
% 180.89/180.95 inference(scs_inference,[],[13,2935,2934,2,3])).
% 180.89/180.95 cnf(2940,plain,
% 180.89/180.95 (~E(f3(f3(a1,a5),f3(f3(a1,a5),a6)),f3(x29401,a6))),
% 180.89/180.95 inference(scs_inference,[],[2938,2])).
% 180.89/180.95 cnf(2944,plain,
% 180.89/180.95 (~E(a5,f3(f3(a1,f3(x29441,a6)),a5))),
% 180.89/180.95 inference(scs_inference,[],[2901,2])).
% 180.89/180.95 cnf(2945,plain,
% 180.89/180.95 (~E(f3(a5,x29451),f3(f3(f3(a1,a4),a5),a5))),
% 180.89/180.95 inference(scs_inference,[],[14,2709,2901,2,3])).
% 180.89/180.96 cnf(2947,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a4),a5),a5),f3(a5,x29471))),
% 180.89/180.96 inference(scs_inference,[],[2945,2])).
% 180.89/180.96 cnf(2948,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a1,a5),a6)),f3(x29481,a6))),
% 180.89/180.96 inference(scs_inference,[],[2940,2945,2708,2,3])).
% 180.89/180.96 cnf(2952,plain,
% 180.89/180.96 (~E(f3(a5,x29521),f3(f3(f3(a6,a4),a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[14,2721,2948,2,3])).
% 180.89/180.96 cnf(2955,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a5),f3(x29551,a6)),a5),f3(x29552,a6))),
% 180.89/180.96 inference(scs_inference,[],[2908,2952,2636,2,3])).
% 180.89/180.96 cnf(2959,plain,
% 180.89/180.96 (~E(f3(a5,x29591),f3(a6,f3(f3(x29592,x29593),x29592)))),
% 180.89/180.96 inference(scs_inference,[],[14,2955,2859,2,3])).
% 180.89/180.96 cnf(2961,plain,
% 180.89/180.96 (~E(f3(a6,f3(f3(x29611,x29612),x29611)),f3(a5,x29613))),
% 180.89/180.96 inference(scs_inference,[],[2959,2])).
% 180.89/180.96 cnf(2962,plain,
% 180.89/180.96 (~E(f3(f3(a6,a5),a5),f3(x29621,a6))),
% 180.89/180.96 inference(scs_inference,[],[2929,2959,2726,2,3])).
% 180.89/180.96 cnf(2966,plain,
% 180.89/180.96 (~E(f3(a5,x29661),f3(f3(a6,f3(a2,a4)),a5))),
% 180.89/180.96 inference(scs_inference,[],[14,2962,2727,2,3])).
% 180.89/180.96 cnf(2968,plain,
% 180.89/180.96 (~E(f3(f3(a6,f3(a2,a4)),a5),f3(a5,x29681))),
% 180.89/180.96 inference(scs_inference,[],[2966,2])).
% 180.89/180.96 cnf(2969,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a4),f3(a2,a4)),f3(f3(x29691,x29692),x29691)),f3(x29693,a6))),
% 180.89/180.96 inference(scs_inference,[],[2937,2966,2654,2,3])).
% 180.89/180.96 cnf(2973,plain,
% 180.89/180.96 (~E(f3(a5,x29731),f3(f3(f3(a1,a5),f3(a5,x29732)),a5))),
% 180.89/180.96 inference(scs_inference,[],[14,2774,2969,2,3])).
% 180.89/180.96 cnf(2975,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a5),f3(a5,x29751)),a5),f3(a5,x29752))),
% 180.89/180.96 inference(scs_inference,[],[2973,2])).
% 180.89/180.96 cnf(2976,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a4),f3(a5,x29761)),a5),f3(a5,x29762))),
% 180.89/180.96 inference(scs_inference,[],[2947,2973,2720,2,3])).
% 180.89/180.96 cnf(2980,plain,
% 180.89/180.96 (~E(f3(a5,x29801),f3(f3(a6,f3(x29802,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[14,2976,2778,2,3])).
% 180.89/180.96 cnf(2982,plain,
% 180.89/180.96 (~E(f3(f3(a6,f3(x29821,a6)),a5),f3(a5,x29822))),
% 180.89/180.96 inference(scs_inference,[],[2980,2])).
% 180.89/180.96 cnf(2989,plain,
% 180.89/180.96 (~E(f3(f3(f3(x29891,x29892),f3(x29893,x29892)),f3(f3(x29891,x29893),x29892)),a6)),
% 180.89/180.96 inference(scs_inference,[],[2880,2])).
% 180.89/180.96 cnf(2990,plain,
% 180.89/180.96 (~E(f3(a6,f3(a5,a5)),f3(a5,x29901))),
% 180.89/180.96 inference(scs_inference,[],[2961,2880,2619,2,3])).
% 180.89/180.96 cnf(2995,plain,
% 180.89/180.96 (~E(f3(a6,f3(a5,f3(a1,a2))),f3(a5,x29951))),
% 180.89/180.96 inference(scs_inference,[],[2990,2707,2,3])).
% 180.89/180.96 cnf(2999,plain,
% 180.89/180.96 (~E(f3(a6,f3(f3(a1,a2),f3(a1,a2))),f3(a5,x29991))),
% 180.89/180.96 inference(scs_inference,[],[2995,2713,2,3])).
% 180.89/180.96 cnf(3003,plain,
% 180.89/180.96 (~E(f3(f3(x30031,x30032),x30031),f3(a6,f3(f3(x30033,a6),a1)))),
% 180.89/180.96 inference(scs_inference,[],[2999,2868,28,2,3])).
% 180.89/180.96 cnf(3005,plain,
% 180.89/180.96 (~E(f3(a6,f3(f3(x30051,a6),a1)),f3(f3(x30052,x30053),x30052))),
% 180.89/180.96 inference(scs_inference,[],[3003,2])).
% 180.89/180.96 cnf(3006,plain,
% 180.89/180.96 (~E(f3(f3(a6,f3(a2,a4)),f3(a1,a2)),f3(a5,x30061))),
% 180.89/180.96 inference(scs_inference,[],[2968,3003,2701,2,3])).
% 180.89/180.96 cnf(3010,plain,
% 180.89/180.96 (~E(f3(f3(x30101,x30102),x30101),f3(f3(a1,f3(x30103,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3006,2944,28,2,3])).
% 180.89/180.96 cnf(3012,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(x30121,a6)),a5),f3(f3(x30122,x30123),x30122))),
% 180.89/180.96 inference(scs_inference,[],[3010,2])).
% 180.89/180.96 cnf(3013,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a5),a5),a5),f3(a5,x30131))),
% 180.89/180.96 inference(scs_inference,[],[2975,3010,2726,2,3])).
% 180.89/180.96 cnf(3018,plain,
% 180.89/180.96 (~E(f3(f3(x30181,x30182),x30181),f3(f3(f3(a1,a2),a4),f3(f3(a1,a4),f3(a2,a4))))),
% 180.89/180.96 inference(scs_inference,[],[3013,2899,28,2,3])).
% 180.89/180.96 cnf(3020,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a2),a4),f3(f3(a1,a4),f3(a2,a4))),f3(f3(x30201,x30202),x30201))),
% 180.89/180.96 inference(scs_inference,[],[3018,2])).
% 180.89/180.96 cnf(3021,plain,
% 180.89/180.96 (~E(f3(f3(a6,a5),a5),f3(a5,x30211))),
% 180.89/180.96 inference(scs_inference,[],[2982,3018,2668,2,3])).
% 180.89/180.96 cnf(3026,plain,
% 180.89/180.96 (~E(f3(f3(a6,a5),f3(x30261,a6)),f3(a5,x30262))),
% 180.89/180.96 inference(scs_inference,[],[3021,2628,2,3])).
% 180.89/180.96 cnf(3030,plain,
% 180.89/180.96 (~E(f3(a6,f3(a5,a1)),f3(f3(x30301,x30302),x30301))),
% 180.89/180.96 inference(scs_inference,[],[3026,3005,2680,2,3])).
% 180.89/180.96 cnf(3035,plain,
% 180.89/180.96 (~E(f3(f3(f3(x30351,x30352),f3(x30353,x30352)),f3(f3(x30351,x30353),x30352)),a1)),
% 180.89/180.96 inference(scs_inference,[],[3030,2736,24,2,3])).
% 180.89/180.96 cnf(3038,plain,
% 180.89/180.96 (~E(f3(f3(f3(x30381,x30382),f3(x30383,x30382)),f3(f3(x30381,x30383),x30382)),f3(a6,a5))),
% 180.89/180.96 inference(scs_inference,[],[2584,2657,24,2,3])).
% 180.89/180.96 cnf(3040,plain,
% 180.89/180.96 (~E(f3(a6,a5),f3(f3(f3(x30401,x30402),f3(x30403,x30402)),f3(f3(x30401,x30403),x30402)))),
% 180.89/180.96 inference(scs_inference,[],[3038,2])).
% 180.89/180.96 cnf(3052,plain,
% 180.89/180.96 (~E(f3(a1,a2),a1)),
% 180.89/180.96 inference(scs_inference,[],[90,2])).
% 180.89/180.96 cnf(3055,plain,
% 180.89/180.96 (~E(f3(a1,f3(a1,a2)),a5)),
% 180.89/180.96 inference(scs_inference,[],[3052,74,9,2,12])).
% 180.89/180.96 cnf(3058,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),x30581),a1)),
% 180.89/180.96 inference(scs_inference,[],[3052,2818,74,9,2,12,3])).
% 180.89/180.96 cnf(3061,plain,
% 180.89/180.96 (~E(f3(a1,f3(f3(x30611,x30612),x30611)),a5)),
% 180.89/180.96 inference(scs_inference,[],[3058,3055,2601,2,3])).
% 180.89/180.96 cnf(3064,plain,
% 180.89/180.96 (~E(a5,f3(a1,f3(f3(x30641,x30642),x30641)))),
% 180.89/180.96 inference(scs_inference,[],[3061,2])).
% 180.89/180.96 cnf(3065,plain,
% 180.89/180.96 (~E(f3(f3(x30651,a6),f3(x30652,a6)),a1)),
% 180.89/180.96 inference(scs_inference,[],[3061,3058,2615,2,3])).
% 180.89/180.96 cnf(3069,plain,
% 180.89/180.96 (~E(f3(a1,a2),f3(a1,f3(f3(x30691,x30692),x30691)))),
% 180.89/180.96 inference(scs_inference,[],[20,3065,3064,2,3])).
% 180.89/180.96 cnf(3072,plain,
% 180.89/180.96 (~E(f3(f3(x30721,x30722),x30721),f3(a1,f3(f3(x30723,x30724),x30723)))),
% 180.89/180.96 inference(scs_inference,[],[3069,2580,2,3])).
% 180.89/180.96 cnf(3074,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(x30741,x30742),x30741))),
% 180.89/180.96 inference(scs_inference,[],[3012,3072,2726,2,3])).
% 180.89/180.96 cnf(3078,plain,
% 180.89/180.96 (~E(f3(f3(x30781,x30782),x30781),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3074,2])).
% 180.89/180.96 cnf(3089,plain,
% 180.89/180.96 (~E(a5,f3(a1,f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3055,2])).
% 180.89/180.96 cnf(3091,plain,
% 180.89/180.96 (~E(f3(a1,a2),f3(a1,f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[20,3089,93,2,3])).
% 180.89/180.96 cnf(3092,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),a5)),
% 180.89/180.96 inference(scs_inference,[],[20,3089,93,8,2,3,12])).
% 180.89/180.96 cnf(3095,plain,
% 180.89/180.96 (~E(f3(a1,f3(a1,a2)),f3(a1,a2))),
% 180.89/180.96 inference(scs_inference,[],[3091,2])).
% 180.89/180.96 cnf(3096,plain,
% 180.89/180.96 (~E(f3(x30961,a6),f3(a1,f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3091,2572,2,3])).
% 180.89/180.96 cnf(3097,plain,
% 180.89/180.96 (~E(f3(a1,f3(a1,a2)),f3(x30971,a6))),
% 180.89/180.96 inference(scs_inference,[],[3096,2])).
% 180.89/180.96 cnf(3098,plain,
% 180.89/180.96 (~E(a5,f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3092,2])).
% 180.89/180.96 cnf(3100,plain,
% 180.89/180.96 (~E(f3(a1,a2),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[20,3098,135,2,3])).
% 180.89/180.96 cnf(3101,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(a1,a2))),
% 180.89/180.96 inference(scs_inference,[],[3100,2])).
% 180.89/180.96 cnf(3102,plain,
% 180.89/180.96 (~E(f3(a1,f3(x31021,a6)),f3(a1,a2))),
% 180.89/180.96 inference(scs_inference,[],[3095,3100,2574,2,3])).
% 180.89/180.96 cnf(3104,plain,
% 180.89/180.96 (~E(f3(a1,a2),f3(a1,f3(x31041,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3102,2])).
% 180.89/180.96 cnf(3110,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),x31101),f3(a1,f3(x31102,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3104,116,2818,2,3])).
% 180.89/180.96 cnf(3115,plain,
% 180.89/180.96 (~E(f3(a1,f3(f3(a1,a2),x31151)),f3(x31152,a6))),
% 180.89/180.96 inference(scs_inference,[],[3097,3110,2821,2,3])).
% 180.89/180.96 cnf(3119,plain,
% 180.89/180.96 (~E(f3(f3(a5,x31191),f3(f3(a5,x31192),f3(a1,a2))),f3(a1,f3(x31193,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3115,2783,3110,2,3])).
% 180.89/180.96 cnf(3122,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a1,a2)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3078,3119,2593,2,3])).
% 180.89/180.96 cnf(3125,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(a5,a5),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3122,2])).
% 180.89/180.96 cnf(3135,plain,
% 180.89/180.96 (~E(f3(f3(x31351,x31352),x31351),f3(f3(a1,a4),f3(a2,a4)))),
% 180.89/180.96 inference(scs_inference,[],[34,2])).
% 180.89/180.96 cnf(3164,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a1,a2)),f3(f3(a1,f3(x31641,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3125,2636,3,2])).
% 180.89/180.96 cnf(3175,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a4),f3(a2,a4)),f3(f3(f3(a1,a4),f3(a2,a4)),f3(a1,a4))),a5)),
% 180.89/180.96 inference(scs_inference,[],[35,3135,9,3,12])).
% 180.89/180.96 cnf(3193,plain,
% 180.89/180.96 (~E(f3(f3(x31931,x31932),x31931),f3(f3(f3(a6,a5),a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3175,2688,28,2,3])).
% 180.89/180.96 cnf(3194,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),a5),f3(f3(x31941,x31942),x31941))),
% 180.89/180.96 inference(scs_inference,[],[3193,2])).
% 180.89/180.96 cnf(3195,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(a1,a2))),
% 180.89/180.96 inference(scs_inference,[],[3193,3101,2583,2,3])).
% 180.89/180.96 cnf(3197,plain,
% 180.89/180.96 (~E(f3(a1,a2),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3195,2])).
% 180.89/180.96 cnf(3198,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x31981)),a5),f3(a1,a2))),
% 180.89/180.96 inference(scs_inference,[],[3195,2720,2,3])).
% 180.89/180.96 cnf(3200,plain,
% 180.89/180.96 (~E(f3(a1,a2),f3(f3(a1,f3(a5,x32001)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3198,2])).
% 180.89/180.96 cnf(3201,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),f3(f3(x32011,x32012),x32011)),f3(f3(x32013,x32014),x32013))),
% 180.89/180.96 inference(scs_inference,[],[3198,3194,2654,2,3])).
% 180.89/180.96 cnf(3206,plain,
% 180.89/180.96 (~E(f3(f3(x32061,x32062),x32061),f3(f3(f3(a6,a5),a5),f3(f3(x32063,x32064),x32063)))),
% 180.89/180.96 inference(scs_inference,[],[3201,2])).
% 180.89/180.96 cnf(3207,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),f3(f3(a5,x32071),f3(x32072,a6))),f3(f3(x32073,x32074),x32073))),
% 180.89/180.96 inference(scs_inference,[],[3201,2635,2,3])).
% 180.89/180.96 cnf(3210,plain,
% 180.89/180.96 (~E(f3(f3(x32101,x32102),x32101),f3(f3(f3(a6,a5),a5),f3(f3(a5,x32103),f3(x32104,a6))))),
% 180.89/180.96 inference(scs_inference,[],[3207,2])).
% 180.89/180.96 cnf(3211,plain,
% 180.89/180.96 (~E(f3(f3(x32111,x32112),x32111),f3(f3(a1,f3(a5,x32113)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3200,3207,2580,2,3])).
% 180.89/180.96 cnf(3212,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x32121)),a5),f3(f3(x32122,x32123),x32122))),
% 180.89/180.96 inference(scs_inference,[],[3211,2])).
% 180.89/180.96 cnf(3213,plain,
% 180.89/180.96 (~E(f3(a5,f3(x32131,x32132)),f3(f3(a1,f3(a5,x32133)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3211,2696,2,3])).
% 180.89/180.96 cnf(3216,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x32161)),a5),f3(a5,f3(x32162,x32163)))),
% 180.89/180.96 inference(scs_inference,[],[3213,2])).
% 180.89/180.96 cnf(3217,plain,
% 180.89/180.96 (~E(f3(x32171,a6),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3197,3213,2572,2,3])).
% 180.89/180.96 cnf(3221,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(x32211,a6))),
% 180.89/180.96 inference(scs_inference,[],[3217,2])).
% 180.89/180.96 cnf(3222,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x32221)),f3(f3(x32222,x32223),x32222)),f3(f3(x32224,x32225),x32224))),
% 180.89/180.96 inference(scs_inference,[],[3217,3212,2654,2,3])).
% 180.89/180.96 cnf(3225,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(x32251,a6))),
% 180.89/180.96 inference(scs_inference,[],[3221,3222,2708,2,3])).
% 180.89/180.96 cnf(3228,plain,
% 180.89/180.96 (~E(f3(f3(x32281,a6),a1),f3(f3(f3(a6,a5),a5),f3(f3(x32282,x32283),x32282)))),
% 180.89/180.96 inference(scs_inference,[],[3225,3206,2575,2,3])).
% 180.89/180.96 cnf(3232,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),f3(f3(x32321,x32322),x32321)),f3(f3(x32323,a6),a1))),
% 180.89/180.96 inference(scs_inference,[],[3228,2])).
% 180.89/180.96 cnf(3233,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(a5,f3(x32331,x32332)))),
% 180.89/180.96 inference(scs_inference,[],[3216,3228,2668,2,3])).
% 180.89/180.96 cnf(3239,plain,
% 180.89/180.96 (~E(f3(a5,f3(x32391,x32392)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3233,2])).
% 180.89/180.96 cnf(3240,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),f3(f3(a5,x32401),f3(a5,x32402))),f3(f3(x32403,a6),a1))),
% 180.89/180.96 inference(scs_inference,[],[3233,3232,2719,2,3])).
% 180.89/180.96 cnf(3244,plain,
% 180.89/180.96 (~E(f3(a6,f3(a1,a2)),f3(f3(f3(x32441,x32442),f3(x32443,x32442)),f3(f3(x32441,x32443),x32442)))),
% 180.89/180.96 inference(scs_inference,[],[3240,3040,2701,2,3])).
% 180.89/180.96 cnf(3246,plain,
% 180.89/180.96 (~E(f3(f3(f3(x32461,x32462),f3(x32463,x32462)),f3(f3(x32461,x32463),x32462)),f3(a6,f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3244,2])).
% 180.89/180.96 cnf(3247,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3239,3244,2695,2,3])).
% 180.89/180.96 cnf(3250,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3247,2])).
% 180.89/180.96 cnf(3251,plain,
% 180.89/180.96 (~E(f3(f3(f3(x32511,x32512),x32511),a5),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3247,2655,2,3])).
% 180.89/180.96 cnf(3257,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,x32571),f3(a2,x32571)),f3(a5,x32571)),f3(a6,f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3251,3246,2609,2,3])).
% 180.89/180.96 cnf(3260,plain,
% 180.89/180.96 (~E(f3(a6,f3(a1,a2)),f3(f3(f3(a1,x32601),f3(a2,x32601)),f3(a5,x32601)))),
% 180.89/180.96 inference(scs_inference,[],[3257,2])).
% 180.89/180.96 cnf(3261,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(x32611,a6)),a5),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3250,3257,2636,2,3])).
% 180.89/180.96 cnf(3263,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(x32631,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3261,2])).
% 180.89/180.96 cnf(3264,plain,
% 180.89/180.96 (~E(f3(a6,f3(f3(x32641,x32642),x32641)),f3(f3(f3(a1,x32643),f3(a2,x32643)),f3(a5,x32643)))),
% 180.89/180.96 inference(scs_inference,[],[3261,3260,2601,2,3])).
% 180.89/180.96 cnf(3267,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),a5),f3(f3(a1,f3(x32671,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3263,3264,2702,2,3])).
% 180.89/180.96 cnf(3272,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(x32721,a6)),a5),f3(f3(a1,a2),a5))),
% 180.89/180.96 inference(scs_inference,[],[3267,2])).
% 180.89/180.96 cnf(3273,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),x32731),f3(f3(a1,f3(a5,x32732)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3267,3200,2818,2,3])).
% 180.89/180.96 cnf(3274,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x32741)),a5),f3(f3(a1,a2),x32742))),
% 180.89/180.96 inference(scs_inference,[],[3273,2])).
% 180.89/180.96 cnf(3275,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(a1,a2),a5))),
% 180.89/180.96 inference(scs_inference,[],[3272,3273,2726,2,3])).
% 180.89/180.96 cnf(3278,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),a5),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3275,2])).
% 180.89/180.96 cnf(3279,plain,
% 180.89/180.96 (~E(f3(f3(x32791,a6),a5),f3(f3(a1,f3(a5,x32792)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3275,3273,2716,2,3])).
% 180.89/180.96 cnf(3281,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x32811)),a5),f3(f3(x32812,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3279,2])).
% 180.89/180.96 cnf(3282,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a2),x32821),a5),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3278,3279,2822,2,3])).
% 180.89/180.96 cnf(3288,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a5,a5)),f3(f3(a1,f3(a5,x32881)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3282,2811,3273,2,3])).
% 180.89/180.96 cnf(3290,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x32901)),a5),f3(f3(a5,a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3288,2])).
% 180.89/180.96 cnf(3291,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(a1,a2),x32911))),
% 180.89/180.96 inference(scs_inference,[],[3274,3288,2668,2,3])).
% 180.89/180.96 cnf(3295,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),x32951),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3291,2])).
% 180.89/180.96 cnf(3296,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(f3(a1,a2),x32961))),
% 180.89/180.96 inference(scs_inference,[],[3291,2708,2,3])).
% 180.89/180.96 cnf(3298,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),x32981),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3296,2])).
% 180.89/180.96 cnf(3299,plain,
% 180.89/180.96 (~E(f3(f3(a5,x32991),f3(f3(x32992,a6),f3(x32993,a6))),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3295,3296,2775,2,3])).
% 180.89/180.96 cnf(3305,plain,
% 180.89/180.96 (~E(f3(f3(a5,x33051),f3(f3(x33052,a6),a5)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3299,2667,2,3])).
% 180.89/180.96 cnf(3309,plain,
% 180.89/180.96 (~E(f3(f3(x33091,x33092),x33091),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3305,3298,2808,2,3])).
% 180.89/180.96 cnf(3311,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(f3(x33111,x33112),x33111))),
% 180.89/180.96 inference(scs_inference,[],[3309,2])).
% 180.89/180.96 cnf(3312,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x33121)),f3(x33122,a6)),f3(f3(a5,a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3290,3309,2628,2,3])).
% 180.89/180.96 cnf(3314,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a5,a5)),f3(f3(a1,f3(a5,x33141)),f3(x33142,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3312,2])).
% 180.89/180.96 cnf(3315,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a5,a5)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3312,3295,2748,2,3])).
% 180.89/180.96 cnf(3320,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(a5,a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3315,2])).
% 180.89/180.96 cnf(3321,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a2),a5),f3(a5,a5)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3315,2714,2,3])).
% 180.89/180.96 cnf(3323,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(f3(a1,a2),a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3321,2])).
% 180.89/180.96 cnf(3324,plain,
% 180.89/180.96 (~E(f3(f3(f3(x33241,a6),a5),f3(a5,a5)),f3(f3(a1,f3(a5,x33242)),f3(x33243,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3321,3314,2645,2,3])).
% 180.89/180.96 cnf(3326,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x33261)),f3(x33262,a6)),f3(f3(f3(x33263,a6),a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3324,2])).
% 180.89/180.96 cnf(3327,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x33271)),a5),f3(f3(f3(a1,a2),a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3323,3324,2720,2,3])).
% 180.89/180.96 cnf(3330,plain,
% 180.89/180.96 (~E(f3(f3(a5,x33301),f3(a5,a5)),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3327,3298,2698,2,3])).
% 180.89/180.96 cnf(3335,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(f3(a5,x33351),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3330,2])).
% 180.89/180.96 cnf(3336,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(x33361,a6)),a5),f3(f3(a5,a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3320,3330,2636,2,3])).
% 180.89/180.96 cnf(3338,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a5,a5)),f3(f3(a1,f3(x33381,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3336,2])).
% 180.89/180.96 cnf(3339,plain,
% 180.89/180.96 (~E(f3(f3(a5,x33391),f3(a5,f3(a1,a2))),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3336,2779,3295,2,3])).
% 180.89/180.96 cnf(3342,plain,
% 180.89/180.96 (~E(f3(f3(a5,x33421),f3(f3(a5,x33422),f3(a1,a2))),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3339,2686,2,3])).
% 180.89/180.96 cnf(3345,plain,
% 180.89/180.96 (~E(f3(f3(x33451,a6),f3(x33452,a6)),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3342,3298,2615,2,3])).
% 180.89/180.96 cnf(3350,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(f3(x33501,a6),f3(x33502,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3345,2])).
% 180.89/180.96 cnf(3351,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(a5,x33511),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3335,3345,2583,2,3])).
% 180.89/180.96 cnf(3354,plain,
% 180.89/180.96 (~E(f3(f3(a5,x33541),f3(a5,a5)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3351,2])).
% 180.89/180.96 cnf(3355,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x33551)),a5),f3(f3(f3(x33552,a6),a5),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3351,3326,2695,2,3])).
% 180.89/180.96 cnf(3359,plain,
% 180.89/180.96 (~E(f3(f3(f3(a5,x33591),x33592),f3(a5,a5)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3354,3355,2687,2,3])).
% 180.89/180.96 cnf(3362,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(f3(a5,x33621),x33622),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3359,2])).
% 180.89/180.96 cnf(3363,plain,
% 180.89/180.96 (~E(f3(f3(f3(a5,x33631),x33632),f3(a5,f3(a1,a2))),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3359,2707,2,3])).
% 180.89/180.96 cnf(3369,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a5,x33691)),a5),f3(f3(f3(a5,x33692),x33693),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3362,3363,2720,2,3])).
% 180.89/180.96 cnf(3371,plain,
% 180.89/180.96 (~E(f3(f3(f3(a5,x33711),x33712),f3(a5,a5)),f3(f3(a1,f3(a5,x33713)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3369,2])).
% 180.89/180.96 cnf(3372,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(x33721,x33722),x33721)),f3(f3(x33723,x33724),x33723))),
% 180.89/180.96 inference(scs_inference,[],[3311,3369,2654,2,3])).
% 180.89/180.96 cnf(3374,plain,
% 180.89/180.96 (~E(f3(f3(x33741,x33742),x33741),f3(f3(a1,f3(a1,a2)),f3(f3(x33743,x33744),x33743)))),
% 180.89/180.96 inference(scs_inference,[],[3372,2])).
% 180.89/180.96 cnf(3375,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(x33751,a6),f3(x33752,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3350,3372,2583,2,3])).
% 180.89/180.96 cnf(3378,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(x33781,a6)),a5),f3(f3(x33782,a6),f3(x33783,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3375,2636,2,3])).
% 180.89/180.96 cnf(3383,plain,
% 180.89/180.96 (~E(f3(f3(x33831,a6),f3(x33832,a6)),f3(f3(a1,f3(x33833,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3378,2])).
% 180.89/180.96 cnf(3384,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(x33841,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3378,3281,2726,2,3])).
% 180.89/180.96 cnf(3388,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(f3(x33881,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3384,2708,2,3])).
% 180.89/180.96 cnf(3391,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a1,a2)),f3(f3(x33911,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3388,2701,2,3])).
% 180.89/180.96 cnf(3393,plain,
% 180.89/180.96 (~E(f3(f3(x33931,a6),a5),f3(f3(a1,f3(a1,a2)),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3391,2])).
% 180.89/180.96 cnf(3394,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(x33941,a6)),f3(f3(x33942,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3391,2574,2,3])).
% 180.89/180.96 cnf(3399,plain,
% 180.89/180.96 (~E(f3(f3(x33991,a6),a5),f3(f3(a1,f3(a1,a2)),f3(x33992,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3394,2])).
% 180.89/180.96 cnf(3400,plain,
% 180.89/180.96 (~E(f3(f3(a5,x34001),f3(a5,a5)),f3(f3(a1,f3(a5,x34002)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3394,3371,2620,2,3])).
% 180.89/180.96 cnf(3404,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(a1,a2)),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3393,3400,2696,2,3])).
% 180.89/180.96 cnf(3407,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a1,a2)),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3404,2])).
% 180.89/180.96 cnf(3408,plain,
% 180.89/180.96 (~E(f3(a1,a4),f3(f3(f3(x34081,a5),f3(x34082,a5)),f3(f3(x34081,x34082),f3(a5,x34083))))),
% 180.89/180.96 inference(scs_inference,[],[59,3404,2725,2,3])).
% 180.89/180.96 cnf(3411,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34111,a5),f3(x34112,a5)),f3(f3(x34111,x34112),f3(a5,x34113))),f3(a1,a4))),
% 180.89/180.96 inference(scs_inference,[],[3408,2])).
% 180.89/180.96 cnf(3412,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a1,a2),x34121)),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3407,3408,2821,2,3])).
% 180.89/180.96 cnf(3418,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(a1,a2)),f3(f3(a1,a2),x34181)))),
% 180.89/180.96 inference(scs_inference,[],[3412,2])).
% 180.89/180.96 cnf(3419,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),a5),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3412,2795,2,3])).
% 180.89/180.96 cnf(3422,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3419,2])).
% 180.89/180.96 cnf(3423,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34231,a5),f3(a6,a5)),f3(a5,f3(a5,x34232))),f3(a1,a4))),
% 180.89/180.96 inference(scs_inference,[],[3419,3411,2680,2,3])).
% 180.89/180.96 cnf(3426,plain,
% 180.89/180.96 (~E(f3(a1,a4),f3(f3(f3(x34261,a5),f3(a6,a5)),f3(a5,f3(a5,x34262))))),
% 180.89/180.96 inference(scs_inference,[],[3423,2])).
% 180.89/180.96 cnf(3427,plain,
% 180.89/180.96 (~E(f3(f3(x34271,a6),a5),f3(f3(a1,f3(a1,a2)),f3(f3(a1,a2),x34272)))),
% 180.89/180.96 inference(scs_inference,[],[3423,3418,2629,2,3])).
% 180.89/180.96 cnf(3429,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a1,a2),x34291)),f3(f3(x34292,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3427,2])).
% 180.89/180.96 cnf(3430,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(a1,a2)),f3(x34301,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3399,3427,2696,2,3])).
% 180.89/180.96 cnf(3437,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34371,x34372),x34371),a5),f3(f3(a1,f3(a1,a2)),f3(x34373,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3430,2655,2,3])).
% 180.89/180.96 cnf(3440,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,a5)),f3(f3(x34401,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3437,3429,2592,2,3])).
% 180.89/180.96 cnf(3443,plain,
% 180.89/180.96 (~E(f3(f3(x34431,a6),a5),f3(f3(a1,f3(a1,a2)),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3440,2])).
% 180.89/180.96 cnf(3444,plain,
% 180.89/180.96 (~E(f3(a5,f3(f3(a1,a1),a2)),a6)),
% 180.89/180.96 inference(scs_inference,[],[3440,2989,2796,2,3])).
% 180.89/180.96 cnf(3448,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(a1,a2)),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3443,3444,2661,2,3])).
% 180.89/180.96 cnf(3453,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,a5)),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3448,2])).
% 180.89/180.96 cnf(3454,plain,
% 180.89/180.96 (~E(f3(f3(a1,a2),a5),f3(f3(a1,f3(a1,a2)),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3448,2702,2,3])).
% 180.89/180.96 cnf(3456,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,a5)),f3(f3(a1,a2),a5))),
% 180.89/180.96 inference(scs_inference,[],[3454,2])).
% 180.89/180.96 cnf(3457,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34571,x34572),x34571),a5),f3(f3(a1,f3(a1,a2)),f3(a5,a5)))),
% 180.89/180.96 inference(scs_inference,[],[3454,2602,2,3])).
% 180.89/180.96 cnf(3460,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a1,a2),a5)),f3(f3(a1,a2),a5))),
% 180.89/180.96 inference(scs_inference,[],[3456,3457,2713,2,3])).
% 180.89/180.96 cnf(3463,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,f3(x34631,a6))),f3(a5,a5))),
% 180.89/180.96 inference(scs_inference,[],[3453,3460,2635,2,3])).
% 180.89/180.96 cnf(3468,plain,
% 180.89/180.96 (~E(f3(a5,a5),f3(f3(a1,f3(a1,a2)),f3(a5,f3(x34681,a6))))),
% 180.89/180.96 inference(scs_inference,[],[3463,2])).
% 180.89/180.96 cnf(3469,plain,
% 180.89/180.96 (~E(f3(a1,a4),f3(f3(f3(x34691,a5),f3(a6,a5)),f3(f3(a5,x34692),f3(a5,x34693))))),
% 180.89/180.96 inference(scs_inference,[],[3463,3426,2619,2,3])).
% 180.89/180.96 cnf(3471,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34711,a5),f3(a6,a5)),f3(f3(a5,x34712),f3(a5,x34713))),f3(a1,a4))),
% 180.89/180.96 inference(scs_inference,[],[3469,2])).
% 180.89/180.96 cnf(3472,plain,
% 180.89/180.96 (~E(f3(f3(x34721,a6),a5),f3(f3(a1,f3(x34722,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3469,3383,2695,2,3])).
% 180.89/180.96 cnf(3476,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34761,a5),f3(a6,a5)),f3(f3(a5,x34762),a5)),f3(a1,a4))),
% 180.89/180.96 inference(scs_inference,[],[3471,3472,2667,2,3])).
% 180.89/180.96 cnf(3481,plain,
% 180.89/180.96 (~E(f3(f3(f3(x34811,a5),f3(a6,a5)),f3(f3(a5,x34812),f3(a1,a2))),f3(a1,a4))),
% 180.89/180.96 inference(scs_inference,[],[3476,2707,2,3])).
% 180.89/180.96 cnf(3487,plain,
% 180.89/180.96 (~E(f3(f3(x34871,a6),a5),f3(f3(a1,f3(a1,a2)),f3(a5,f3(x34872,a6))))),
% 180.89/180.96 inference(scs_inference,[],[3481,3468,2629,2,3])).
% 180.89/180.96 cnf(3489,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,f3(x34891,a6))),f3(f3(x34892,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3487,2])).
% 180.89/180.96 cnf(3490,plain,
% 180.89/180.96 (~E(f3(a5,f3(x34901,a6)),f3(f3(a1,f3(a1,a2)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3422,3487,2628,2,3])).
% 180.89/180.96 cnf(3493,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a2),a5),f3(a5,a5)),f3(f3(a1,f3(x34931,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3490,3338,2714,2,3])).
% 180.89/180.96 cnf(3496,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(x34961,a6),f3(x34962,a6))),f3(f3(x34963,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3489,3493,2644,2,3])).
% 180.89/180.96 cnf(3502,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(x35021,a6),a5)),f3(f3(x35022,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3496,2725,2,3])).
% 180.89/180.96 cnf(3506,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(x35061,a6),f3(a5,x35062))),f3(f3(x35063,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3502,2719,2,3])).
% 180.89/180.96 cnf(3509,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,f3(a5,x35091))),f3(f3(x35092,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3506,2619,2,3])).
% 180.89/180.96 cnf(3513,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a5,x35131),f3(a5,x35132))),f3(f3(x35133,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3509,2686,2,3])).
% 180.89/180.96 cnf(3519,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a5,x35191),a5)),f3(f3(x35192,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3513,2667,2,3])).
% 180.89/180.96 cnf(3523,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(a5,x35231),f3(x35232,a6))),f3(f3(x35233,a6),a5))),
% 180.89/180.96 inference(scs_inference,[],[3519,2635,2,3])).
% 180.89/180.96 cnf(3526,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a1,a2)),f3(f3(a1,f3(a1,a2)),f3(f3(x35261,x35262),x35261)))),
% 180.89/180.96 inference(scs_inference,[],[3523,3374,2593,2,3])).
% 180.89/180.96 cnf(3529,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(x35291,x35292),x35291)),f3(f3(a5,a5),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3526,2])).
% 180.89/180.96 cnf(3530,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(x35301,a6)),f3(f3(a1,f3(a1,a2)),f3(f3(x35302,x35303),x35302)))),
% 180.89/180.96 inference(scs_inference,[],[3526,2574,2,3])).
% 180.89/180.96 cnf(3535,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(f3(x35351,x35352),x35351)),f3(f3(a5,a5),f3(x35353,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3530,2])).
% 180.89/180.96 cnf(3536,plain,
% 180.89/180.96 (~E(f3(f3(f3(x35361,a6),a5),f3(a1,a2)),f3(f3(a1,f3(x35362,a6)),a5))),
% 180.89/180.96 inference(scs_inference,[],[3530,3164,2645,2,3])).
% 180.89/180.96 cnf(3538,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(x35381,a6)),a5),f3(f3(f3(x35382,a6),a5),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3536,2])).
% 180.89/180.96 cnf(3539,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,a1)),f3(f3(a5,a5),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3529,3536,2609,2,3])).
% 180.89/180.96 cnf(3543,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(a1,a2)),f3(f3(a1,f3(a1,a2)),f3(a5,a1)))),
% 180.89/180.96 inference(scs_inference,[],[3539,2])).
% 180.89/180.96 cnf(3544,plain,
% 180.89/180.96 (~E(f3(f3(a1,a5),a5),f3(f3(f3(x35441,a6),a5),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3539,3538,2668,2,3])).
% 180.89/180.96 cnf(3547,plain,
% 180.89/180.96 (~E(f3(f3(f3(x35471,a6),a5),f3(a1,a2)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3544,2])).
% 180.89/180.96 cnf(3548,plain,
% 180.89/180.96 (~E(f3(f3(f3(a5,x35481),a5),f3(a1,a2)),f3(f3(a1,f3(a1,a2)),f3(a5,a1)))),
% 180.89/180.96 inference(scs_inference,[],[3543,3544,2687,2,3])).
% 180.89/180.96 cnf(3554,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,f3(a1,a2)),f3(a2,f3(a1,a2))),f3(x35541,a6)),a1)),
% 180.89/180.96 inference(scs_inference,[],[3548,3035,2800,2,3])).
% 180.89/180.96 cnf(3558,plain,
% 180.89/180.96 (~E(f3(f3(a1,f3(a1,a2)),f3(a5,x35581)),f3(f3(a5,a5),f3(x35582,a6)))),
% 180.89/180.96 inference(scs_inference,[],[3535,3554,2680,2,3])).
% 180.89/180.96 cnf(3561,plain,
% 180.89/180.96 (~E(f3(f3(a5,a5),f3(x35611,a6)),f3(f3(a1,f3(a1,a2)),f3(a5,x35612)))),
% 180.89/180.96 inference(scs_inference,[],[3558,2])).
% 180.89/180.96 cnf(3562,plain,
% 180.89/180.96 (~E(f3(f3(x35621,a6),f3(a1,a2)),f3(f3(f3(a6,a5),a5),f3(f3(a5,x35622),f3(x35623,a6))))),
% 180.89/180.96 inference(scs_inference,[],[3558,3210,2801,2,3])).
% 180.89/180.96 cnf(3565,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),f3(f3(a5,x35651),f3(x35652,a6))),f3(f3(x35653,a6),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3562,2])).
% 180.89/180.96 cnf(3566,plain,
% 180.89/180.96 (~E(f3(f3(f3(x35661,a6),a5),f3(f3(x35662,x35663),x35662)),f3(f3(a1,a5),a5))),
% 180.89/180.96 inference(scs_inference,[],[3547,3562,2601,2,3])).
% 180.89/180.96 cnf(3572,plain,
% 180.89/180.96 (~E(f3(f3(f3(a6,a5),a5),f3(f3(a5,x35721),a5)),f3(f3(x35722,a6),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[3566,3565,2725,2,3])).
% 180.89/180.96 cnf(3576,plain,
% 180.89/180.96 (~E(f3(f3(f3(a1,a2),a5),f3(x35761,a6)),f3(f3(a1,f3(a1,a2)),f3(a5,x35762)))),
% 180.89/180.96 inference(scs_inference,[],[3561,3572,2714,2,3])).
% 180.89/180.96 cnf(3579,plain,
% 180.89/180.96 (~E(f3(f3(a5,a4),f3(f3(a1,a4),f3(a2,a4))),f3(f3(x35791,x35792),x35791))),
% 180.89/180.96 inference(scs_inference,[],[3576,3020,2610,2,3])).
% 180.89/180.96 cnf(3781,plain,
% 180.89/180.96 (~E(f3(f3(x37811,x37812),x37811),f3(a6,a5))),
% 180.89/180.96 inference(scs_inference,[],[3295,3201,4,5])).
% 180.89/180.96 cnf(3865,plain,
% 180.89/180.96 (~E(f3(a5,a4),f3(f3(f3(a1,a4),f3(a2,a4)),x38651))),
% 180.89/180.96 inference(scs_inference,[],[2801,3579,2910,5,2,4])).
% 180.89/180.96 cnf(4078,plain,
% 180.89/180.96 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(f3(x40781,x40781),f3(x40782,x40781)),f3(a1,a2)))),
% 180.89/180.96 inference(scs_inference,[],[25,2601,3])).
% 180.89/180.96 cnf(4357,plain,
% 180.89/180.96 ($false),
% 180.89/180.96 inference(scs_inference,[],[9,8,3781,4078,3865,24,12,2,3]),
% 180.89/180.96 ['proof']).
% 180.89/180.96 % SZS output end Proof
% 180.89/180.96 % Total time :180.250000s
%------------------------------------------------------------------------------