%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG024-6 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n006.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 14:00:40 EDT 2024
% Result : Unsatisfiable 76.30s 76.39s
% Output : CNFRefutation 76.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : RNG024-6 : TPTP v8.2.0. Released v1.0.0.
% 0.09/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Jun 18 13:38:39 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.55/0.60 start to proof:theBenchmark
% 76.30/76.38 %-------------------------------------------
% 76.30/76.38 % File :CSE---1.7
% 76.30/76.38 % Problem :theBenchmark
% 76.30/76.38 % Transform :cnf
% 76.30/76.38 % Format :tptp:raw
% 76.30/76.38 % Command :java -jar mcs_scs.jar %d %s
% 76.30/76.38
% 76.30/76.38 % Result :Theorem 75.740000s
% 76.30/76.38 % Output :CNFRefutation 75.740000s
% 76.30/76.38 %-------------------------------------------
% 76.30/76.39 %--------------------------------------------------------------------------
% 76.30/76.39 % File : RNG024-6 : TPTP v8.2.0. Released v1.0.0.
% 76.30/76.39 % Domain : Ring Theory (Alternative)
% 76.30/76.39 % Problem : Right alternative
% 76.30/76.39 % Version : [Ste87] (equality) axioms.
% 76.30/76.39 % Theorem formulation : In terms of associators
% 76.30/76.39 % English :
% 76.30/76.39
% 76.30/76.39 % Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin
% 76.30/76.39 % : [Ste92] Stevens (1992), Unpublished Note
% 76.30/76.39 % Source : [Ste92]
% 76.30/76.39 % Names : - [Ste87]
% 76.30/76.39
% 76.30/76.39 % Status : Unsatisfiable
% 76.30/76.39 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.07 v5.3.0, 0.00 v2.1.0, 0.13 v2.0.0
% 76.30/76.39 % Syntax : Number of clauses : 16 ( 16 unt; 0 nHn; 1 RR)
% 76.30/76.39 % Number of literals : 16 ( 16 equ; 1 neg)
% 76.30/76.39 % Maximal clause size : 1 ( 1 avg)
% 76.30/76.39 % Maximal term depth : 5 ( 2 avg)
% 76.30/76.39 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 76.30/76.39 % Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% 76.30/76.39 % Number of variables : 27 ( 2 sgn)
% 76.30/76.39 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 76.30/76.39
% 76.30/76.39 % Comments :
% 76.30/76.39 %--------------------------------------------------------------------------
% 76.30/76.39 %----Include nonassociative ring axioms
% 76.30/76.39 include('Axioms/RNG003-0.ax').
% 76.30/76.39 %--------------------------------------------------------------------------
% 76.30/76.39 cnf(prove_right_alternative,negated_conjecture,
% 76.30/76.39 associator(x,y,y) != additive_identity ).
% 76.30/76.39
% 76.30/76.39 %--------------------------------------------------------------------------
% 76.30/76.39 %-------------------------------------------
% 76.30/76.39 % Proof found
% 76.30/76.39 % SZS status Theorem for theBenchmark
% 76.30/76.39 % SZS output start Proof
% 76.30/76.39 %ClaNum:22(EqnAxiom:8)
% 76.30/76.39 %VarNum:48(SingletonVarNum:22)
% 76.30/76.39 %MaxLitNum:1
% 76.30/76.39 %MaxfuncDepth:4
% 76.30/76.39 %SharedTerms:10
% 76.30/76.39 %goalClause: 22
% 76.30/76.39 %singleGoalClaCount:1
% 76.30/76.39 [22]~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),a2)
% 76.30/76.39 [10]E(f4(x101,a2),a2)
% 76.30/76.39 [11]E(f4(a2,x111),a2)
% 76.30/76.39 [12]E(f3(x121,a2),x121)
% 76.30/76.39 [13]E(f3(a2,x131),x131)
% 76.30/76.39 [9]E(f1(f1(x91)),x91)
% 76.30/76.39 [14]E(f3(x141,f1(x141)),a2)
% 76.30/76.39 [15]E(f3(f1(x151),x151),a2)
% 76.30/76.39 [16]E(f3(x161,x162),f3(x162,x161))
% 76.30/76.39 [18]E(f4(f4(x181,x182),x182),f4(x181,f4(x182,x182)))
% 76.30/76.39 [19]E(f4(f4(x191,x191),x192),f4(x191,f4(x191,x192)))
% 76.30/76.39 [17]E(f3(f3(x171,x172),x173),f3(x171,f3(x172,x173)))
% 76.30/76.39 [20]E(f3(f4(x201,x202),f4(x201,x203)),f4(x201,f3(x202,x203)))
% 76.30/76.39 [21]E(f3(f4(x211,x212),f4(x213,x212)),f4(f3(x211,x213),x212))
% 76.30/76.39 %EqnAxiom
% 76.30/76.39 [1]E(x11,x11)
% 76.30/76.39 [2]E(x22,x21)+~E(x21,x22)
% 76.30/76.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 76.30/76.39 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 76.30/76.39 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 76.30/76.39 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 76.30/76.39 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 76.30/76.39 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 76.30/76.39
% 76.30/76.39 %-------------------------------------------
% 76.30/76.40 cnf(23,plain,
% 76.30/76.40 (E(x231,f3(x231,a2))),
% 76.30/76.40 inference(scs_inference,[],[12,2])).
% 76.30/76.40 cnf(24,plain,
% 76.30/76.40 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,a2))),
% 76.30/76.40 inference(scs_inference,[],[22,12,2,3])).
% 76.30/76.40 cnf(26,plain,
% 76.30/76.40 (E(x261,f3(a2,x261))),
% 76.30/76.40 inference(scs_inference,[],[13,2])).
% 76.30/76.40 cnf(27,plain,
% 76.30/76.40 (E(f3(a2,f4(f4(x271,x272),x272)),f4(x271,f4(x272,x272)))),
% 76.30/76.40 inference(scs_inference,[],[13,18,2,3])).
% 76.30/76.40 cnf(29,plain,
% 76.30/76.40 (E(f4(x291,f4(x292,x292)),f3(a2,f4(f4(x291,x292),x292)))),
% 76.30/76.40 inference(scs_inference,[],[27,2])).
% 76.30/76.40 cnf(30,plain,
% 76.30/76.40 (E(f3(f4(x301,x302),f4(x301,x303)),f4(x301,f3(x303,x302)))),
% 76.30/76.40 inference(scs_inference,[],[27,16,20,2,3])).
% 76.30/76.41 cnf(32,plain,
% 76.30/76.41 (E(f4(x321,f3(x322,x323)),f3(f4(x321,x323),f4(x321,x322)))),
% 76.30/76.41 inference(scs_inference,[],[30,2])).
% 76.30/76.41 cnf(33,plain,
% 76.30/76.41 (E(f1(f1(f3(f4(x331,x332),f4(x331,x333)))),f4(x331,f3(x333,x332)))),
% 76.30/76.41 inference(scs_inference,[],[30,9,2,3])).
% 76.30/76.41 cnf(36,plain,
% 76.30/76.41 (E(f4(x361,f3(x362,x362)),f4(f3(x361,x361),x362))),
% 76.30/76.41 inference(scs_inference,[],[32,33,21,2,3])).
% 76.30/76.41 cnf(39,plain,
% 76.30/76.41 (E(f4(f3(x391,x391),x392),f4(x391,f3(x392,x392)))),
% 76.30/76.41 inference(scs_inference,[],[36,2])).
% 76.30/76.41 cnf(54,plain,
% 76.30/76.41 (E(f4(f3(f4(x541,x541),f4(x541,x541)),x542),f4(x541,f4(x541,f3(x542,x542))))),
% 76.30/76.41 inference(scs_inference,[],[39,19,2,3])).
% 76.30/76.41 cnf(58,plain,
% 76.30/76.41 (E(f3(x581,x582),f3(x581,f3(x582,a2)))),
% 76.30/76.41 inference(scs_inference,[],[23,54,17,2,3])).
% 76.30/76.41 cnf(61,plain,
% 76.30/76.41 (E(f3(x611,f3(x612,a2)),f3(x611,x612))),
% 76.30/76.41 inference(scs_inference,[],[58,2])).
% 76.30/76.41 cnf(62,plain,
% 76.30/76.41 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f4(x621,a2))),
% 76.30/76.41 inference(scs_inference,[],[22,58,10,2,3])).
% 76.30/76.41 cnf(63,plain,
% 76.30/76.41 (E(a2,f4(a2,x631))),
% 76.30/76.41 inference(scs_inference,[],[11,2])).
% 76.30/76.41 cnf(67,plain,
% 76.30/76.41 (E(a2,f3(x671,f1(x671)))),
% 76.30/76.41 inference(scs_inference,[],[14,2])).
% 76.30/76.41 cnf(68,plain,
% 76.30/76.41 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,f3(a2,a2)))),
% 76.30/76.41 inference(scs_inference,[],[61,24,14,2,3])).
% 76.30/76.41 cnf(70,plain,
% 76.30/76.41 (E(a2,f3(f1(x701),x701))),
% 76.30/76.41 inference(scs_inference,[],[15,2])).
% 76.30/76.41 cnf(71,plain,
% 76.30/76.41 (E(f3(f1(x711),x711),f3(x712,f1(x712)))),
% 76.30/76.41 inference(scs_inference,[],[67,15,2,3])).
% 76.30/76.41 cnf(72,plain,
% 76.30/76.41 (E(f3(x721,f1(x721)),f3(f1(x722),x722))),
% 76.30/76.41 inference(scs_inference,[],[71,2])).
% 76.30/76.41 cnf(73,plain,
% 76.30/76.41 (E(f1(f1(a2)),f3(f1(x731),x731))),
% 76.30/76.41 inference(scs_inference,[],[70,71,9,2,3])).
% 76.30/76.41 cnf(75,plain,
% 76.30/76.41 (E(f3(f1(x751),x751),f1(f1(a2)))),
% 76.30/76.41 inference(scs_inference,[],[73,2])).
% 76.30/76.41 cnf(76,plain,
% 76.30/76.41 (E(f1(a2),f3(f1(x761),x761))),
% 76.30/76.41 inference(scs_inference,[],[72,26,73,2,3])).
% 76.30/76.41 cnf(79,plain,
% 76.30/76.41 (E(f3(f1(x791),x791),f1(a2))),
% 76.30/76.41 inference(scs_inference,[],[76,2])).
% 76.30/76.41 cnf(80,plain,
% 76.30/76.41 (E(f3(x801,f1(x801)),f1(f1(a2)))),
% 76.30/76.41 inference(scs_inference,[],[75,72,76,2,3])).
% 76.30/76.41 cnf(82,plain,
% 76.30/76.41 (E(f1(f1(a2)),f3(x821,f1(x821)))),
% 76.30/76.41 inference(scs_inference,[],[80,2])).
% 76.30/76.41 cnf(83,plain,
% 76.30/76.41 (E(f3(f1(x831),f3(x831,a2)),f1(a2))),
% 76.30/76.41 inference(scs_inference,[],[79,61,80,2,3])).
% 76.30/76.41 cnf(86,plain,
% 76.30/76.41 (E(f1(a2),f3(f1(x861),f3(x861,a2)))),
% 76.30/76.41 inference(scs_inference,[],[83,2])).
% 76.30/76.41 cnf(87,plain,
% 76.30/76.41 (E(f1(a2),f1(f1(a2)))),
% 76.30/76.41 inference(scs_inference,[],[23,75,83,2,3])).
% 76.30/76.41 cnf(90,plain,
% 76.30/76.41 (E(f1(f1(a2)),f1(a2))),
% 76.30/76.41 inference(scs_inference,[],[87,2])).
% 76.30/76.41 cnf(91,plain,
% 76.30/76.41 (E(f3(f1(x911),x911),f3(f1(x912),f3(x912,a2)))),
% 76.30/76.41 inference(scs_inference,[],[86,79,87,2,3])).
% 76.30/76.41 cnf(92,plain,
% 76.30/76.41 (E(f3(f1(x921),f3(x921,a2)),f3(f1(x922),x922))),
% 76.30/76.41 inference(scs_inference,[],[91,2])).
% 76.30/76.41 cnf(93,plain,
% 76.30/76.41 (E(f1(f1(a2)),f3(f1(x931),f3(x931,a2)))),
% 76.30/76.41 inference(scs_inference,[],[90,86,91,2,3])).
% 76.30/76.41 cnf(94,plain,
% 76.30/76.41 (E(f3(f1(x941),f3(x941,a2)),f1(f1(a2)))),
% 76.30/76.41 inference(scs_inference,[],[93,2])).
% 76.30/76.41 cnf(95,plain,
% 76.30/76.41 (E(f3(f1(x951),f3(f3(x951,a2),a2)),f3(f1(x952),x952))),
% 76.30/76.41 inference(scs_inference,[],[92,61,93,2,3])).
% 76.30/76.41 cnf(97,plain,
% 76.30/76.41 (E(f3(f1(x971),x971),f3(f1(x972),f3(f3(x972,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[95,2])).
% 76.30/76.41 cnf(98,plain,
% 76.30/76.41 (E(f3(f1(x981),f3(x981,a2)),f3(x982,f1(x982)))),
% 76.30/76.41 inference(scs_inference,[],[82,94,95,2,3])).
% 76.30/76.41 cnf(99,plain,
% 76.30/76.41 (E(f3(x991,f1(x991)),f3(f1(x992),f3(x992,a2)))),
% 76.30/76.41 inference(scs_inference,[],[98,2])).
% 76.30/76.41 cnf(100,plain,
% 76.30/76.41 (E(f3(f1(x1001),f3(x1001,a2)),f3(f1(x1002),f3(f3(x1002,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[97,92,98,2,3])).
% 76.30/76.41 cnf(102,plain,
% 76.30/76.41 (E(f3(f1(x1021),f3(f3(x1021,a2),a2)),f3(f1(x1022),f3(x1022,a2)))),
% 76.30/76.41 inference(scs_inference,[],[100,2])).
% 76.30/76.41 cnf(103,plain,
% 76.30/76.41 (E(a2,f3(f1(x1031),f3(f3(x1031,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[97,70,100,2,3])).
% 76.30/76.41 cnf(106,plain,
% 76.30/76.41 (E(f4(x1061,a2),f3(x1062,f1(x1062)))),
% 76.30/76.41 inference(scs_inference,[],[67,103,10,2,3])).
% 76.30/76.41 cnf(107,plain,
% 76.30/76.41 (E(f3(x1071,f1(x1071)),f4(x1072,a2))),
% 76.30/76.41 inference(scs_inference,[],[106,2])).
% 76.30/76.41 cnf(108,plain,
% 76.30/76.41 (E(f3(x1081,f1(x1081)),f3(f1(x1082),f3(f3(x1082,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[72,97,106,2,3])).
% 76.30/76.41 cnf(111,plain,
% 76.30/76.41 (E(f3(f1(x1111),f3(f3(f3(x1111,a2),a2),a2)),f3(f1(x1112),f3(x1112,a2)))),
% 76.30/76.41 inference(scs_inference,[],[102,61,108,2,3])).
% 76.30/76.41 cnf(113,plain,
% 76.30/76.41 (E(f3(f1(x1131),f3(x1131,a2)),f3(f1(x1132),f3(f3(f3(x1132,a2),a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[111,2])).
% 76.30/76.41 cnf(114,plain,
% 76.30/76.41 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(x1141,f1(x1141)))),
% 76.30/76.41 inference(scs_inference,[],[107,111,62,2,3])).
% 76.30/76.41 cnf(117,plain,
% 76.30/76.41 (E(f3(x1171,f1(x1171)),f3(f1(x1172),f3(f3(f3(x1172,a2),a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[99,113,18,2,3])).
% 76.30/76.41 cnf(133,plain,
% 76.30/76.41 (E(f3(x1331,f3(x1332,x1333)),f3(f3(x1331,x1332),x1333))),
% 76.30/76.41 inference(scs_inference,[],[17,2])).
% 76.30/76.41 cnf(141,plain,
% 76.30/76.41 (E(a2,f4(x1411,a2))),
% 76.30/76.41 inference(scs_inference,[],[10,2])).
% 76.30/76.41 cnf(149,plain,
% 76.30/76.41 (E(f1(f1(a2)),f3(f1(x1491),f3(f3(x1491,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[9,103,3])).
% 76.30/76.41 cnf(152,plain,
% 76.30/76.41 (E(f4(x1521,a2),f3(f1(x1522),f3(f3(x1522,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[10,103,3])).
% 76.30/76.41 cnf(154,plain,
% 76.30/76.41 (E(f4(a2,x1541),f3(f1(x1542),f3(f3(x1542,a2),a2)))),
% 76.30/76.41 inference(scs_inference,[],[11,103,3])).
% 76.30/76.41 cnf(156,plain,
% 76.30/76.41 (E(f3(f4(x1561,f4(x1562,x1562)),a2),f3(a2,f4(f4(x1561,x1562),x1562)))),
% 76.30/76.41 inference(scs_inference,[],[12,29,3])).
% 76.30/76.41 cnf(161,plain,
% 76.30/76.41 (E(f3(f1(x1611),f3(f3(x1611,a2),a2)),f3(f3(f1(x1612),x1612),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,97,3,2])).
% 76.41/76.41 cnf(164,plain,
% 76.41/76.41 (E(f3(f1(x1641),f3(f3(x1641,a2),a2)),f3(f1(f1(a2)),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,149,3,2])).
% 76.41/76.41 cnf(165,plain,
% 76.41/76.41 (E(f3(f4(x1651,a2),a2),f3(f1(x1652),f3(f3(x1652,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[12,152,3])).
% 76.41/76.41 cnf(167,plain,
% 76.41/76.41 (E(f3(f1(x1671),f3(f3(x1671,a2),a2)),f3(f4(x1672,a2),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,152,3,2])).
% 76.41/76.41 cnf(170,plain,
% 76.41/76.41 (E(f3(f4(x1701,a2),a2),f3(f3(f1(x1702),f3(f3(x1702,a2),a2)),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,167,3,2])).
% 76.41/76.41 cnf(171,plain,
% 76.41/76.41 (E(f3(f4(a2,x1711),a2),f3(f1(x1712),f3(f3(x1712,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[12,154,3])).
% 76.41/76.41 cnf(173,plain,
% 76.41/76.41 (E(f3(f1(x1731),f3(f3(x1731,a2),a2)),f3(f4(a2,x1732),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,154,3,2])).
% 76.41/76.41 cnf(179,plain,
% 76.41/76.41 (E(f3(f1(x1791),f3(f3(x1791,a2),a2)),f3(f3(f4(x1792,a2),a2),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,165,3,2])).
% 76.41/76.41 cnf(182,plain,
% 76.41/76.41 (E(f3(f1(x1821),f3(f3(x1821,a2),a2)),f3(f3(f4(a2,x1822),a2),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,171,3,2])).
% 76.41/76.41 cnf(185,plain,
% 76.41/76.41 (E(f3(f1(x1851),f3(f3(x1851,a2),a2)),f3(f3(x1852,f1(x1852)),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,108,3,2])).
% 76.41/76.41 cnf(188,plain,
% 76.41/76.41 (E(f3(f1(x1881),f3(f3(x1881,a2),a2)),f3(f3(f1(x1882),f3(x1882,a2)),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,100,3,2])).
% 76.41/76.41 cnf(189,plain,
% 76.41/76.41 (E(f3(a2,a2),f3(f1(x1891),f3(f3(x1891,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[12,103,3])).
% 76.41/76.41 cnf(192,plain,
% 76.41/76.41 (E(f3(f3(a2,a2),a2),f3(f1(x1921),f3(f3(x1921,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[12,189,3])).
% 76.41/76.41 cnf(194,plain,
% 76.41/76.41 (E(f3(f1(x1941),f3(f3(x1941,a2),a2)),f3(f3(a2,a2),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,189,3,2])).
% 76.41/76.41 cnf(200,plain,
% 76.41/76.41 (E(f3(f1(x2001),f3(f3(x2001,a2),a2)),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.41 inference(scs_inference,[],[12,192,3,2])).
% 76.41/76.41 cnf(204,plain,
% 76.41/76.41 (E(f3(a2,f4(x2041,f4(x2042,x2042))),f3(a2,f4(f4(x2041,x2042),x2042)))),
% 76.41/76.41 inference(scs_inference,[],[13,29,3])).
% 76.41/76.41 cnf(206,plain,
% 76.41/76.41 (E(f3(a2,f4(f4(x2061,x2062),x2062)),f3(a2,f4(x2061,f4(x2062,x2062))))),
% 76.41/76.41 inference(scs_inference,[],[13,29,3,2])).
% 76.41/76.41 cnf(215,plain,
% 76.41/76.41 (E(f3(f1(x2151),f3(f3(x2151,a2),a2)),f3(a2,f3(f1(x2152),x2152)))),
% 76.41/76.41 inference(scs_inference,[],[13,97,3,2])).
% 76.41/76.41 cnf(216,plain,
% 76.41/76.41 (E(f3(a2,f3(a2,a2)),f3(f1(x2161),f3(f3(x2161,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,189,3])).
% 76.41/76.41 cnf(221,plain,
% 76.41/76.41 (E(f3(f1(x2211),f3(f3(x2211,a2),a2)),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.41 inference(scs_inference,[],[13,216,3,2])).
% 76.41/76.41 cnf(224,plain,
% 76.41/76.41 (E(f3(f1(x2241),f3(f3(x2241,a2),a2)),f3(a2,f1(f1(a2))))),
% 76.41/76.41 inference(scs_inference,[],[13,149,3,2])).
% 76.41/76.41 cnf(227,plain,
% 76.41/76.41 (E(f3(f1(x2271),f3(f3(x2271,a2),a2)),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,192,3,2])).
% 76.41/76.41 cnf(228,plain,
% 76.41/76.41 (E(f3(a2,f4(x2281,a2)),f3(f1(x2282),f3(f3(x2282,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,152,3])).
% 76.41/76.41 cnf(230,plain,
% 76.41/76.41 (E(f3(f1(x2301),f3(f3(x2301,a2),a2)),f3(a2,f4(x2302,a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,152,3,2])).
% 76.41/76.41 cnf(236,plain,
% 76.41/76.41 (E(f3(f1(x2361),f3(f3(x2361,a2),a2)),f3(a2,f3(a2,f4(x2362,a2))))),
% 76.41/76.41 inference(scs_inference,[],[13,228,3,2])).
% 76.41/76.41 cnf(237,plain,
% 76.41/76.41 (E(f3(a2,f4(a2,x2371)),f3(f1(x2372),f3(f3(x2372,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,154,3])).
% 76.41/76.41 cnf(239,plain,
% 76.41/76.41 (E(f3(f1(x2391),f3(f3(x2391,a2),a2)),f3(a2,f4(a2,x2392)))),
% 76.41/76.41 inference(scs_inference,[],[13,154,3,2])).
% 76.41/76.41 cnf(245,plain,
% 76.41/76.41 (E(f3(f1(x2451),f3(f3(x2451,a2),a2)),f3(a2,f3(a2,f4(a2,x2452))))),
% 76.41/76.41 inference(scs_inference,[],[13,237,3,2])).
% 76.41/76.41 cnf(248,plain,
% 76.41/76.41 (E(f3(f1(x2481),f3(f3(x2481,a2),a2)),f3(a2,f3(f4(x2482,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,165,3,2])).
% 76.41/76.41 cnf(251,plain,
% 76.41/76.41 (E(f3(f1(x2511),f3(f3(x2511,a2),a2)),f3(a2,f3(f4(a2,x2512),a2)))),
% 76.41/76.41 inference(scs_inference,[],[13,171,3,2])).
% 76.41/76.41 cnf(254,plain,
% 76.41/76.41 (E(f3(f1(x2541),f3(f3(x2541,a2),a2)),f3(a2,f3(x2542,f1(x2542))))),
% 76.41/76.41 inference(scs_inference,[],[13,108,3,2])).
% 76.41/76.41 cnf(257,plain,
% 76.41/76.41 (E(f3(f1(x2571),f3(f3(x2571,a2),a2)),f3(a2,f3(f1(x2572),f3(x2572,a2))))),
% 76.41/76.41 inference(scs_inference,[],[13,100,3,2])).
% 76.41/76.41 cnf(267,plain,
% 76.41/76.41 (E(f3(a2,f4(x2671,f4(a2,a2))),f3(f1(x2672),f3(f3(x2672,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[206,230,3,2])).
% 76.41/76.41 cnf(268,plain,
% 76.41/76.41 (E(f3(a2,f4(x2681,f4(a2,a2))),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.41 inference(scs_inference,[],[227,267,3])).
% 76.41/76.41 cnf(270,plain,
% 76.41/76.41 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f4(x2701,f4(a2,a2))))),
% 76.41/76.41 inference(scs_inference,[],[227,267,3,2])).
% 76.41/76.41 cnf(271,plain,
% 76.41/76.41 (E(f3(a2,f4(x2711,f4(a2,a2))),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.41 inference(scs_inference,[],[200,267,3])).
% 76.41/76.41 cnf(273,plain,
% 76.41/76.41 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f4(x2731,f4(a2,a2))))),
% 76.41/76.41 inference(scs_inference,[],[200,267,3,2])).
% 76.41/76.41 cnf(274,plain,
% 76.41/76.41 (E(f3(a2,f4(x2741,f4(a2,a2))),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.41 inference(scs_inference,[],[221,267,3])).
% 76.41/76.41 cnf(276,plain,
% 76.41/76.41 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a2,f4(x2761,f4(a2,a2))))),
% 76.41/76.41 inference(scs_inference,[],[221,267,3,2])).
% 76.41/76.42 cnf(277,plain,
% 76.41/76.42 (E(f3(a2,f4(x2771,f4(a2,a2))),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[164,267,3])).
% 76.41/76.42 cnf(279,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(a2,f4(x2791,f4(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[164,267,3,2])).
% 76.41/76.42 cnf(285,plain,
% 76.41/76.42 (E(f3(a2,f4(a2,x2851)),f3(f1(x2852),f3(f3(f3(x2852,a2),a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[239,61,3,2])).
% 76.41/76.42 cnf(286,plain,
% 76.41/76.42 (E(f3(a2,f4(x2861,f4(a2,a2))),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[224,267,3])).
% 76.41/76.42 cnf(288,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f4(x2881,f4(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[224,267,3,2])).
% 76.41/76.42 cnf(296,plain,
% 76.41/76.42 (E(f3(f1(x2961),f3(f3(f3(x2961,a2),a2),a2)),f3(f3(a2,a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[194,61,3])).
% 76.41/76.42 cnf(302,plain,
% 76.41/76.42 (E(f3(f1(x3021),x3021),f3(f3(f1(x3022),x3022),a2))),
% 76.41/76.42 inference(scs_inference,[],[161,97,3])).
% 76.41/76.42 cnf(304,plain,
% 76.41/76.42 (E(f3(f3(f1(x3041),x3041),a2),f3(f1(x3042),x3042))),
% 76.41/76.42 inference(scs_inference,[],[161,97,3,2])).
% 76.41/76.42 cnf(305,plain,
% 76.41/76.42 (E(f3(a2,f4(x3051,f4(a2,a2))),f3(f3(x3052,f1(x3052)),a2))),
% 76.41/76.42 inference(scs_inference,[],[185,267,3])).
% 76.41/76.42 cnf(307,plain,
% 76.41/76.42 (E(f3(f3(x3071,f1(x3071)),a2),f3(a2,f4(x3072,f4(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[185,267,3,2])).
% 76.41/76.42 cnf(308,plain,
% 76.41/76.42 (E(f3(f1(x3081),f3(f3(f3(x3081,a2),a2),a2)),f3(f4(x3082,a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[167,61,3])).
% 76.41/76.42 cnf(311,plain,
% 76.41/76.42 (E(f3(f1(x3111),x3111),f3(a2,f3(f1(x3112),x3112)))),
% 76.41/76.42 inference(scs_inference,[],[215,97,3])).
% 76.41/76.42 cnf(313,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x3131),x3131)),f3(f1(x3132),x3132))),
% 76.41/76.42 inference(scs_inference,[],[215,97,3,2])).
% 76.41/76.42 cnf(314,plain,
% 76.41/76.42 (E(f3(a2,f4(x3141,f4(a2,a2))),f3(a2,f3(x3142,f1(x3142))))),
% 76.41/76.42 inference(scs_inference,[],[254,267,3])).
% 76.41/76.42 cnf(316,plain,
% 76.41/76.42 (E(f3(a2,f3(x3161,f1(x3161))),f3(a2,f4(x3162,f4(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[254,267,3,2])).
% 76.41/76.42 cnf(317,plain,
% 76.41/76.42 (E(f3(f1(x3171),f3(f3(f3(x3171,a2),a2),a2)),f3(f4(a2,x3172),a2))),
% 76.41/76.42 inference(scs_inference,[],[173,61,3])).
% 76.41/76.42 cnf(319,plain,
% 76.41/76.42 (E(f3(f4(a2,x3191),a2),f3(f1(x3192),f3(f3(f3(x3192,a2),a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[173,61,3,2])).
% 76.41/76.42 cnf(320,plain,
% 76.41/76.42 (E(f3(f1(x3201),x3201),f3(f3(f1(x3202),f3(x3202,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[188,97,3])).
% 76.41/76.42 cnf(322,plain,
% 76.41/76.42 (E(f3(f3(f1(x3221),f3(x3221,a2)),a2),f3(f1(x3222),x3222))),
% 76.41/76.42 inference(scs_inference,[],[188,97,3,2])).
% 76.41/76.42 cnf(323,plain,
% 76.41/76.42 (E(f3(a2,f4(x3231,f4(a2,a2))),f3(a2,f3(f1(x3232),f3(x3232,a2))))),
% 76.41/76.42 inference(scs_inference,[],[257,267,3])).
% 76.41/76.42 cnf(325,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x3251),f3(x3251,a2))),f3(a2,f4(x3252,f4(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[257,267,3,2])).
% 76.41/76.42 cnf(331,plain,
% 76.41/76.42 (E(f3(a2,f4(x3311,a2)),f3(f1(x3312),f3(f3(f3(x3312,a2),a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[230,61,3,2])).
% 76.41/76.42 cnf(332,plain,
% 76.41/76.42 (E(f3(f1(x3321),x3321),f3(f3(f4(x3322,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[179,97,3])).
% 76.41/76.42 cnf(335,plain,
% 76.41/76.42 (E(f3(a2,f4(x3351,f4(a2,a2))),f3(f3(f4(a2,x3352),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[182,267,3])).
% 76.41/76.42 cnf(340,plain,
% 76.41/76.42 (E(f3(f3(a2,a2),a2),f3(a2,f4(a2,x3401)))),
% 76.41/76.42 inference(scs_inference,[],[285,296,3,2])).
% 76.41/76.42 cnf(343,plain,
% 76.41/76.42 (E(f3(a2,f4(a2,x3431)),f3(a2,f3(a2,a2)))),
% 76.41/76.42 inference(scs_inference,[],[340,133,3,2])).
% 76.41/76.42 cnf(344,plain,
% 76.41/76.42 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,f4(a2,x3441)))),
% 76.41/76.42 inference(scs_inference,[],[343,68,3])).
% 76.41/76.42 cnf(345,plain,
% 76.41/76.42 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f3(a2,a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[340,344,3])).
% 76.41/76.42 cnf(347,plain,
% 76.41/76.42 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f3(a2,a2),f3(a2,a2)))),
% 76.41/76.42 inference(scs_inference,[],[61,345,3])).
% 76.41/76.42 cnf(349,plain,
% 76.41/76.42 (E(f3(f1(x3491),x3491),f3(a2,f3(a2,f4(x3492,a2))))),
% 76.41/76.42 inference(scs_inference,[],[236,97,3])).
% 76.41/76.42 cnf(352,plain,
% 76.41/76.42 (E(f3(a2,f4(x3521,f4(a2,a2))),f3(a2,f3(a2,f4(a2,x3522))))),
% 76.41/76.42 inference(scs_inference,[],[245,267,3])).
% 76.41/76.42 cnf(354,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(a2,x3541))),f3(a2,f4(x3542,f4(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[245,267,3,2])).
% 76.41/76.42 cnf(361,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[270,274,3,2])).
% 76.41/76.42 cnf(362,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[276,271,3])).
% 76.41/76.42 cnf(364,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[276,271,3,2])).
% 76.41/76.42 cnf(367,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[273,277,3,2])).
% 76.41/76.42 cnf(369,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[364,367,3,2])).
% 76.41/76.42 cnf(372,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[279,268,3,2])).
% 76.41/76.42 cnf(381,plain,
% 76.41/76.42 (E(f3(f4(x3811,a2),a2),f3(f4(a2,x3812),a2))),
% 76.41/76.42 inference(scs_inference,[],[319,308,3,2])).
% 76.41/76.42 cnf(382,plain,
% 76.41/76.42 (E(f3(a2,f4(x3821,a2)),f3(f4(a2,x3822),a2))),
% 76.41/76.42 inference(scs_inference,[],[331,317,3])).
% 76.41/76.42 cnf(384,plain,
% 76.41/76.42 (E(f3(f4(a2,x3841),a2),f3(a2,f4(x3842,a2)))),
% 76.41/76.42 inference(scs_inference,[],[331,317,3,2])).
% 76.41/76.42 cnf(385,plain,
% 76.41/76.42 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f4(a2,x3851),a2))),
% 76.41/76.42 inference(scs_inference,[],[384,344,3])).
% 76.41/76.42 cnf(388,plain,
% 76.41/76.42 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f4(x3881,a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[381,385,3])).
% 76.41/76.42 cnf(390,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f4(f4(x3901,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[288,204,3])).
% 76.41/76.42 cnf(392,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x3921,a2),a2)),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[288,204,3,2])).
% 76.41/76.42 cnf(393,plain,
% 76.41/76.42 (E(f3(f4(a2,x3931),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[392,384,3])).
% 76.41/76.42 cnf(395,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(f4(a2,x3951),a2))),
% 76.41/76.42 inference(scs_inference,[],[392,384,3,2])).
% 76.41/76.42 cnf(398,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(f3(x3981,f1(x3981)),a2))),
% 76.41/76.42 inference(scs_inference,[],[307,286,3,2])).
% 76.41/76.42 cnf(399,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f4(f4(a2,x3991),x3991)))),
% 76.41/76.42 inference(scs_inference,[],[395,156,3])).
% 76.41/76.42 cnf(402,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4021),x4021)),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[395,156,3,2])).
% 76.41/76.42 cnf(403,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4031),x4031)),f3(f3(x4032,f1(x4032)),a2))),
% 76.41/76.42 inference(scs_inference,[],[398,402,3])).
% 76.41/76.42 cnf(404,plain,
% 76.41/76.42 (E(f3(f3(x4041,f1(x4041)),a2),f3(a2,f4(f4(a2,x4042),x4042)))),
% 76.41/76.42 inference(scs_inference,[],[398,402,3,2])).
% 76.41/76.42 cnf(408,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f3(x4081,f1(x4081))))),
% 76.41/76.42 inference(scs_inference,[],[316,402,3,2])).
% 76.41/76.42 cnf(410,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4101),x4101)),f3(f1(x4102),f3(f3(x4102,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[224,399,3,2])).
% 76.41/76.42 cnf(411,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x4111,a2),a2)),f3(a2,f3(x4112,f1(x4112))))),
% 76.41/76.42 inference(scs_inference,[],[408,392,3])).
% 76.41/76.42 cnf(412,plain,
% 76.41/76.42 (E(f3(a2,f3(x4121,f1(x4121))),f3(a2,f4(f4(x4122,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[408,392,3,2])).
% 76.41/76.42 cnf(413,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4131),x4131)),f3(a2,f3(f4(x4132,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[410,248,3])).
% 76.41/76.42 cnf(415,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x4151,a2),a2)),f3(a2,f4(f4(a2,x4152),x4152)))),
% 76.41/76.42 inference(scs_inference,[],[410,248,3,2])).
% 76.41/76.42 cnf(416,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4161),x4161)),f3(a2,f3(f4(a2,x4162),a2)))),
% 76.41/76.42 inference(scs_inference,[],[251,410,3])).
% 76.41/76.42 cnf(418,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(a2,x4181),a2)),f3(a2,f4(f4(a2,x4182),x4182)))),
% 76.41/76.42 inference(scs_inference,[],[251,410,3,2])).
% 76.41/76.42 cnf(419,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4191),x4191)),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[227,410,3])).
% 76.41/76.42 cnf(421,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f4(f4(a2,x4211),x4211)))),
% 76.41/76.42 inference(scs_inference,[],[227,410,3,2])).
% 76.41/76.42 cnf(423,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4231),x4231)),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[361,421,3,2])).
% 76.41/76.42 cnf(424,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4241),x4241)),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[369,423,3])).
% 76.41/76.42 cnf(425,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(a2,f4(f4(a2,x4251),x4251)))),
% 76.41/76.42 inference(scs_inference,[],[369,423,3,2])).
% 76.41/76.42 cnf(426,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4261),x4261)),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[200,410,3])).
% 76.41/76.42 cnf(428,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f4(f4(a2,x4281),x4281)))),
% 76.41/76.42 inference(scs_inference,[],[200,410,3,2])).
% 76.41/76.42 cnf(429,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4291),x4291)),f3(f3(f1(x4292),x4292),a2))),
% 76.41/76.42 inference(scs_inference,[],[161,410,3])).
% 76.41/76.42 cnf(431,plain,
% 76.41/76.42 (E(f3(f3(f1(x4311),x4311),a2),f3(a2,f4(f4(a2,x4312),x4312)))),
% 76.41/76.42 inference(scs_inference,[],[161,410,3,2])).
% 76.41/76.42 cnf(432,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4321),x4321)),f3(a2,f3(f1(x4322),x4322)))),
% 76.41/76.42 inference(scs_inference,[],[215,410,3])).
% 76.41/76.42 cnf(434,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x4341),x4341)),f3(a2,f4(f4(a2,x4342),x4342)))),
% 76.41/76.42 inference(scs_inference,[],[215,410,3,2])).
% 76.41/76.42 cnf(435,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4351),x4351)),f3(a2,f3(x4352,f1(x4352))))),
% 76.41/76.42 inference(scs_inference,[],[254,410,3])).
% 76.41/76.42 cnf(437,plain,
% 76.41/76.42 (E(f3(a2,f3(x4371,f1(x4371))),f3(a2,f4(f4(a2,x4372),x4372)))),
% 76.41/76.42 inference(scs_inference,[],[254,410,3,2])).
% 76.41/76.42 cnf(438,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4381),x4381)),f3(f3(f1(x4382),f3(x4382,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[188,410,3])).
% 76.41/76.42 cnf(440,plain,
% 76.41/76.42 (E(f3(f3(f1(x4401),f3(x4401,a2)),a2),f3(a2,f4(f4(a2,x4402),x4402)))),
% 76.41/76.42 inference(scs_inference,[],[188,410,3,2])).
% 76.41/76.42 cnf(441,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4411),x4411)),f3(a2,f3(f1(x4412),f3(x4412,a2))))),
% 76.41/76.42 inference(scs_inference,[],[257,410,3])).
% 76.41/76.42 cnf(443,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x4431),f3(x4431,a2))),f3(a2,f4(f4(a2,x4432),x4432)))),
% 76.41/76.42 inference(scs_inference,[],[257,410,3,2])).
% 76.41/76.42 cnf(444,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(a2,x4441),x4441)),f3(f3(f4(x4442,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[179,410,3])).
% 76.41/76.42 cnf(446,plain,
% 76.41/76.42 (E(f3(f3(f4(x4461,a2),a2),a2),f3(a2,f4(f4(a2,x4462),x4462)))),
% 76.41/76.42 inference(scs_inference,[],[179,410,3,2])).
% 76.41/76.42 cnf(449,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[428,402,3,2])).
% 76.41/76.42 cnf(451,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[449,364,3,2])).
% 76.41/76.42 cnf(452,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(x4521,f1(x4521)),a2))),
% 76.41/76.42 inference(scs_inference,[],[451,398,3])).
% 76.41/76.42 cnf(453,plain,
% 76.41/76.42 (E(f3(f3(x4531,f1(x4531)),a2),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[451,398,3,2])).
% 76.41/76.42 cnf(454,plain,
% 76.41/76.42 (E(f3(f3(x4541,f1(x4541)),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[453,369,3])).
% 76.41/76.42 cnf(455,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(f3(x4551,f1(x4551)),a2))),
% 76.41/76.42 inference(scs_inference,[],[453,369,3,2])).
% 76.41/76.42 cnf(457,plain,
% 76.41/76.42 (E(f3(f3(x4571,f1(x4571)),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[372,455,3,2])).
% 76.41/76.42 cnf(458,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a2,f3(x4581,f1(x4581))))),
% 76.41/76.42 inference(scs_inference,[],[451,408,3])).
% 76.41/76.42 cnf(459,plain,
% 76.41/76.42 (E(f3(a2,f3(x4591,f1(x4591))),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[451,408,3,2])).
% 76.41/76.42 cnf(461,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f3(x4611,f1(x4611))))),
% 76.41/76.42 inference(scs_inference,[],[459,361,3,2])).
% 76.41/76.42 cnf(463,plain,
% 76.41/76.42 (E(f3(a2,f3(x4631,f1(x4631))),f3(f3(x4632,f1(x4632)),a2))),
% 76.41/76.42 inference(scs_inference,[],[457,461,3,2])).
% 76.41/76.42 cnf(464,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f4(f4(x4641,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[412,461,3])).
% 76.41/76.42 cnf(466,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x4661,a2),a2)),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[412,461,3,2])).
% 76.41/76.42 cnf(467,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x4671,a2),a2)),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[466,372,3])).
% 76.41/76.42 cnf(468,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(a2,f4(f4(x4681,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[466,372,3,2])).
% 76.41/76.42 cnf(474,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(a2,f3(x4741,f1(x4741))))),
% 76.41/76.42 inference(scs_inference,[],[463,454,3,2])).
% 76.41/76.42 cnf(476,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x4761,a2),a2)),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[361,464,3,2])).
% 76.41/76.42 cnf(477,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x4771,a2),a2)),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[476,362,3])).
% 76.41/76.42 cnf(478,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f4(f4(x4781,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[476,362,3,2])).
% 76.41/76.42 cnf(481,plain,
% 76.41/76.42 (E(f3(f3(f1(x4811),x4811),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[425,429,3,2])).
% 76.41/76.42 cnf(483,plain,
% 76.41/76.42 (E(f3(a2,f3(x4831,f1(x4831))),f3(f3(f1(x4832),x4832),a2))),
% 76.41/76.42 inference(scs_inference,[],[474,481,3,2])).
% 76.41/76.42 cnf(489,plain,
% 76.41/76.42 (E(f3(f3(x4891,f1(x4891)),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[478,403,3,2])).
% 76.41/76.42 cnf(491,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x4911,a2),a2)),f3(f3(x4912,f1(x4912)),a2))),
% 76.41/76.42 inference(scs_inference,[],[489,478,3,2])).
% 76.41/76.42 cnf(495,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x4951),x4951)),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[468,432,3,2])).
% 76.41/76.42 cnf(497,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f3(f1(x4971),x4971)))),
% 76.41/76.42 inference(scs_inference,[],[495,367,3,2])).
% 76.41/76.42 cnf(498,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f3(f1(x4981),x4981)))),
% 76.41/76.42 inference(scs_inference,[],[497,449,3])).
% 76.41/76.42 cnf(499,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x4991),x4991)),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[497,449,3,2])).
% 76.41/76.42 cnf(501,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5011),x5011)),f3(f3(x5012,f1(x5012)),a2))),
% 76.41/76.42 inference(scs_inference,[],[489,497,3,2])).
% 76.41/76.42 cnf(504,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a2,f3(f1(x5041),x5041)))),
% 76.41/76.42 inference(scs_inference,[],[501,453,3,2])).
% 76.41/76.42 cnf(506,plain,
% 76.41/76.42 (E(f3(a2,f3(x5061,f1(x5061))),f3(a2,f3(f1(x5062),x5062)))),
% 76.41/76.42 inference(scs_inference,[],[499,408,3,2])).
% 76.41/76.42 cnf(508,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x5081,a2),a2)),f3(a2,f3(f1(x5082),x5082)))),
% 76.41/76.42 inference(scs_inference,[],[499,390,3,2])).
% 76.41/76.42 cnf(512,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5121),f3(x5121,a2))),f3(f3(x5122,f1(x5122)),a2))),
% 76.41/76.42 inference(scs_inference,[],[404,323,3,2])).
% 76.41/76.42 cnf(516,plain,
% 76.41/76.42 (E(f3(f3(x5161,f1(x5161)),a2),f3(f3(f1(x5162),x5162),a2))),
% 76.41/76.42 inference(scs_inference,[],[431,491,3,2])).
% 76.41/76.42 cnf(517,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5171),f3(x5171,a2))),f3(f3(f1(x5172),x5172),a2))),
% 76.41/76.42 inference(scs_inference,[],[516,512,3])).
% 76.41/76.42 cnf(519,plain,
% 76.41/76.42 (E(f3(f3(f1(x5191),x5191),a2),f3(a2,f3(f1(x5192),f3(x5192,a2))))),
% 76.41/76.42 inference(scs_inference,[],[516,512,3,2])).
% 76.41/76.42 cnf(520,plain,
% 76.41/76.42 (E(f3(a2,f3(x5201,f1(x5201))),f3(a2,f3(f1(x5202),f3(x5202,a2))))),
% 76.41/76.42 inference(scs_inference,[],[519,483,3])).
% 76.41/76.42 cnf(522,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5221),f3(x5221,a2))),f3(a2,f3(x5222,f1(x5222))))),
% 76.41/76.42 inference(scs_inference,[],[519,483,3,2])).
% 76.41/76.42 cnf(525,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5251),x5251)),f3(a2,f3(f1(x5252),f3(x5252,a2))))),
% 76.41/76.42 inference(scs_inference,[],[506,522,3,2])).
% 76.41/76.42 cnf(528,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5281),f3(x5281,a2))),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[504,525,3,2])).
% 76.41/76.42 cnf(531,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(f1(x5311),x5311),a2))),
% 76.41/76.42 inference(scs_inference,[],[528,519,3,2])).
% 76.41/76.42 cnf(532,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x5321,a2),a2)),f3(a2,f3(f1(x5322),f3(x5322,a2))))),
% 76.41/76.42 inference(scs_inference,[],[508,525,3])).
% 76.41/76.42 cnf(534,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5341),f3(x5341,a2))),f3(a2,f4(f4(x5342,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[508,525,3,2])).
% 76.41/76.42 cnf(538,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f3(f1(x5381),x5381)))),
% 76.41/76.42 inference(scs_inference,[],[434,466,3,2])).
% 76.41/76.42 cnf(541,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[538,499,3,2])).
% 76.41/76.42 cnf(544,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f3(x5441,f1(x5441))))),
% 76.41/76.42 inference(scs_inference,[],[437,426,3,2])).
% 76.41/76.42 cnf(548,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(f1(x5481),f3(x5481,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[440,476,3,2])).
% 76.41/76.42 cnf(552,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f3(f1(x5521),f3(x5521,a2))))),
% 76.41/76.42 inference(scs_inference,[],[443,392,3,2])).
% 76.41/76.42 cnf(556,plain,
% 76.41/76.42 (E(f3(f3(x5561,f1(x5561)),a2),f3(a2,f3(f4(x5562,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[415,491,3,2])).
% 76.41/76.42 cnf(559,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x5591,a2),a2)),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[556,455,3,2])).
% 76.41/76.42 cnf(561,plain,
% 76.41/76.42 (E(f3(a2,f3(x5611,f1(x5611))),f3(a2,f3(f4(x5612,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[559,474,3,2])).
% 76.41/76.42 cnf(564,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x5641,a2),a2)),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[544,561,3,2])).
% 76.41/76.42 cnf(568,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x5681),x5681)),f3(a2,f3(f4(a2,x5682),a2)))),
% 76.41/76.42 inference(scs_inference,[],[418,508,3,2])).
% 76.41/76.42 cnf(571,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(a2,x5711),a2)),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[568,504,3,2])).
% 76.41/76.42 cnf(573,plain,
% 76.41/76.42 (E(f3(f3(f1(x5731),x5731),a2),f3(a2,f3(f4(a2,x5732),a2)))),
% 76.41/76.42 inference(scs_inference,[],[531,571,3,2])).
% 76.41/76.42 cnf(577,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(f3(f1(x5771),x5771),a2))),
% 76.41/76.42 inference(scs_inference,[],[564,573,3,2])).
% 76.41/76.42 cnf(579,plain,
% 76.41/76.42 (E(f3(f3(f1(x5791),x5791),a2),f3(a2,f3(f4(x5792,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[577,564,3,2])).
% 76.41/76.42 cnf(582,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x5821,a2),a2)),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[579,531,3,2])).
% 76.41/76.42 cnf(584,plain,
% 76.41/76.42 (E(f3(f3(f1(x5841),f3(x5841,a2)),a2),f3(a2,f3(f4(x5842,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[548,582,3,2])).
% 76.41/76.42 cnf(587,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(f3(f1(x5871),f3(x5871,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[584,559,3,2])).
% 76.41/76.42 cnf(590,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(a2,x5901),a2)),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[538,568,3,2])).
% 76.41/76.42 cnf(593,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(a2,x5931),a2)),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[577,573,3,2])).
% 76.41/76.42 cnf(595,plain,
% 76.41/76.42 (E(f3(a2,f3(x5951,f1(x5951))),f3(a2,f3(f4(a2,x5952),a2)))),
% 76.41/76.42 inference(scs_inference,[],[593,544,3,2])).
% 76.41/76.42 cnf(598,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(a2,x5981),a2)),f3(a2,f3(f1(x5982),f3(x5982,a2))))),
% 76.41/76.42 inference(scs_inference,[],[595,522,3,2])).
% 76.41/76.42 cnf(601,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x6011,a2),a2)),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[561,461,3,2])).
% 76.41/76.42 cnf(605,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(f4(x6051,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[446,476,3,2])).
% 76.41/76.42 cnf(607,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x6071,a2),a2)),f3(a2,f3(f4(a2,x6072),a2)))),
% 76.41/76.42 inference(scs_inference,[],[593,478,3,2])).
% 76.41/76.42 cnf(617,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f3(f1(x6171),f3(x6171,a2))))),
% 76.41/76.42 inference(scs_inference,[],[325,419,3,2])).
% 76.41/76.42 cnf(625,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a2,f3(a2,f4(a2,x6251))))),
% 76.41/76.42 inference(scs_inference,[],[354,423,3,2])).
% 76.41/76.42 cnf(629,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(a2,f3(f4(a2,x6291),a2)))),
% 76.41/76.42 inference(scs_inference,[],[590,372,3,2])).
% 76.41/76.42 cnf(630,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x6301,a2),a2)),f3(a2,f3(f1(x6302),f3(x6302,a2))))),
% 76.41/76.42 inference(scs_inference,[],[617,601,3])).
% 76.41/76.42 cnf(631,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6311),f3(x6311,a2))),f3(a2,f3(f4(x6312,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[617,601,3,2])).
% 76.41/76.42 cnf(634,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6341),f3(x6341,a2))),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[629,598,3,2])).
% 76.41/76.42 cnf(635,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6351),f3(x6351,a2))),f3(f3(f1(x6352),f3(x6352,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[587,634,3])).
% 76.41/76.42 cnf(636,plain,
% 76.41/76.42 (E(f3(f3(f1(x6361),f3(x6361,a2)),a2),f3(a2,f3(f1(x6362),f3(x6362,a2))))),
% 76.41/76.42 inference(scs_inference,[],[587,634,3,2])).
% 76.41/76.42 cnf(639,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x6391,a2),a2)),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[552,631,3,2])).
% 76.41/76.42 cnf(642,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x6421,a2),a2)),f3(f3(f1(x6422),f3(x6422,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[636,534,3,2])).
% 76.41/76.42 cnf(643,plain,
% 76.41/76.42 (E(f3(a2,f4(f4(x6431,a2),a2)),f3(a2,f3(f4(x6432,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[642,584,3])).
% 76.41/76.42 cnf(651,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6511),x6511)),f3(a2,f3(f4(x6512,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[639,498,3,2])).
% 76.41/76.42 cnf(652,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(f3(f1(x6521),x6521),a2))),
% 76.41/76.42 inference(scs_inference,[],[617,517,3])).
% 76.41/76.42 cnf(654,plain,
% 76.41/76.42 (E(f3(f3(f1(x6541),x6541),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[617,517,3,2])).
% 76.41/76.42 cnf(656,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6561),x6561)),f3(f3(f1(x6562),x6562),a2))),
% 76.41/76.42 inference(scs_inference,[],[654,538,3,2])).
% 76.41/76.42 cnf(658,plain,
% 76.41/76.42 (E(f3(f3(f1(x6581),x6581),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[541,652,3,2])).
% 76.41/76.42 cnf(661,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6611),f3(x6611,a2))),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[544,520,3,2])).
% 76.41/76.42 cnf(665,plain,
% 76.41/76.42 (E(f3(f3(f1(x6651),f3(x6651,a2)),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.42 inference(scs_inference,[],[552,635,3,2])).
% 76.41/76.42 cnf(668,plain,
% 76.41/76.42 (E(f3(f3(f3(a2,a2),a2),a2),f3(f3(f1(x6681),f3(x6681,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[661,636,3,2])).
% 76.41/76.42 cnf(672,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(f3(f1(x6721),f3(x6721,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[665,541,3,2])).
% 76.41/76.42 cnf(687,plain,
% 76.41/76.42 (E(f3(f3(f4(a2,x6871),a2),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[270,335,3,2])).
% 76.41/76.42 cnf(689,plain,
% 76.41/76.42 (E(f3(f3(f1(x6891),f3(x6891,a2)),a2),f3(f3(f4(a2,x6892),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[672,687,3,2])).
% 76.41/76.42 cnf(692,plain,
% 76.41/76.42 (E(f3(f3(f4(a2,x6921),a2),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[668,689,3,2])).
% 76.41/76.42 cnf(699,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x6991),x6991)),f3(f3(f4(a2,x6992),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[692,497,3,2])).
% 76.41/76.42 cnf(710,plain,
% 76.41/76.42 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,f4(x7101,a2)))),
% 76.41/76.42 inference(scs_inference,[],[382,388,3])).
% 76.41/76.42 cnf(713,plain,
% 76.41/76.42 (E(f3(f3(f1(x7131),x7131),a2),f3(f3(f4(x7132,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[304,332,3])).
% 76.41/76.42 cnf(721,plain,
% 76.41/76.42 (E(f3(f3(f4(x7211,a2),a2),a2),f3(a2,f3(f1(x7212),x7212)))),
% 76.41/76.42 inference(scs_inference,[],[656,713,3,2])).
% 76.41/76.42 cnf(733,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(f3(f4(x7331,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[495,721,3,2])).
% 76.41/76.42 cnf(746,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7461,a2))),f3(a2,f3(f1(x7462),x7462)))),
% 76.41/76.42 inference(scs_inference,[],[313,349,3,2])).
% 76.41/76.42 cnf(749,plain,
% 76.41/76.42 (E(f3(f3(f4(a2,x7491),a2),a2),f3(a2,f3(a2,f4(x7492,a2))))),
% 76.41/76.42 inference(scs_inference,[],[699,746,3,2])).
% 76.41/76.42 cnf(753,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7531,a2))),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[605,749,3,2])).
% 76.41/76.42 cnf(756,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7561,a2))),f3(a2,f3(f4(x7562,a2),a2)))),
% 76.41/76.42 inference(scs_inference,[],[651,746,3])).
% 76.41/76.42 cnf(758,plain,
% 76.41/76.42 (E(f3(a2,f3(f4(x7581,a2),a2)),f3(a2,f3(a2,f4(x7582,a2))))),
% 76.41/76.42 inference(scs_inference,[],[651,746,3,2])).
% 76.41/76.42 cnf(762,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7621,a2))),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[758,629,3,2])).
% 76.41/76.42 cnf(763,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7631,a2))),f3(f3(f4(x7632,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[733,762,3])).
% 76.41/76.42 cnf(770,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7701,a2))),f3(f3(f1(x7702),f3(x7702,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[322,349,3,2])).
% 76.41/76.42 cnf(773,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(a2,f3(a2,f4(x7731,a2))))),
% 76.41/76.42 inference(scs_inference,[],[770,665,3,2])).
% 76.41/76.42 cnf(775,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7751,a2))),f3(f3(f1(x7752),x7752),a2))),
% 76.41/76.42 inference(scs_inference,[],[773,658,3,2])).
% 76.41/76.42 cnf(778,plain,
% 76.41/76.42 (E(f3(a2,f3(f3(a2,a2),a2)),f3(a2,f3(a2,f4(x7781,a2))))),
% 76.41/76.42 inference(scs_inference,[],[775,654,3,2])).
% 76.41/76.42 cnf(780,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f4(x7801,a2))),f3(a2,f3(f4(a2,x7802),a2)))),
% 76.41/76.42 inference(scs_inference,[],[778,590,3,2])).
% 76.41/76.42 cnf(825,plain,
% 76.41/76.42 (E(f3(f1(x8251),f3(f3(f3(x8251,a2),a2),a2)),f3(f3(x8252,a2),f1(x8252)))),
% 76.41/76.42 inference(scs_inference,[],[16,113,3,2])).
% 76.41/76.42 cnf(826,plain,
% 76.41/76.42 (E(f3(f3(f3(f3(x8261,a2),a2),a2),f1(x8261)),f3(f3(x8262,a2),f1(x8262)))),
% 76.41/76.42 inference(scs_inference,[],[16,825,3])).
% 76.41/76.42 cnf(828,plain,
% 76.41/76.42 (E(f3(f3(x8281,a2),f1(x8281)),f3(f3(f3(f3(x8282,a2),a2),a2),f1(x8282)))),
% 76.41/76.42 inference(scs_inference,[],[826,2])).
% 76.41/76.42 cnf(829,plain,
% 76.41/76.42 (E(f3(f3(f3(x8291,a2),a2),f1(x8291)),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.42 inference(scs_inference,[],[16,221,826,2,3])).
% 76.41/76.42 cnf(831,plain,
% 76.41/76.42 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(f3(x8311,a2),a2),f1(x8311)))),
% 76.41/76.42 inference(scs_inference,[],[829,2])).
% 76.41/76.42 cnf(832,plain,
% 76.41/76.42 (E(f3(f1(x8321),f3(x8321,a2)),f3(f3(f3(f3(x8322,a2),a2),a2),f1(x8322)))),
% 76.41/76.42 inference(scs_inference,[],[16,828,829,2,3])).
% 76.41/76.42 cnf(835,plain,
% 76.41/76.42 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(f3(x8351,a2),a2),f1(x8351)))),
% 76.41/76.42 inference(scs_inference,[],[16,831,832,2,3])).
% 76.41/76.42 cnf(837,plain,
% 76.41/76.42 (E(f3(f3(f3(x8371,a2),a2),f1(x8371)),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[835,2])).
% 76.41/76.42 cnf(838,plain,
% 76.41/76.42 (E(f3(f3(f3(x8381,a2),a2),f1(x8381)),f3(f1(f1(a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[16,164,835,2,3])).
% 76.41/76.42 cnf(840,plain,
% 76.41/76.42 (E(f3(f1(f1(a2)),a2),f3(f3(f3(x8401,a2),a2),f1(x8401)))),
% 76.41/76.42 inference(scs_inference,[],[838,2])).
% 76.41/76.42 cnf(841,plain,
% 76.41/76.42 (E(f3(f1(x8411),f3(f3(x8411,a2),a2)),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[16,837,838,2,3])).
% 76.41/76.42 cnf(844,plain,
% 76.41/76.42 (E(f3(a2,f1(f1(a2))),f3(f3(f3(x8441,a2),a2),f1(x8441)))),
% 76.41/76.42 inference(scs_inference,[],[16,840,841,2,3])).
% 76.41/76.42 cnf(847,plain,
% 76.41/76.42 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(f1(x8471),f3(x8471,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[16,548,844,2,3])).
% 76.41/76.42 cnf(849,plain,
% 76.41/76.42 (E(f3(f3(f1(x8491),f3(x8491,a2)),a2),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[847,2])).
% 76.41/76.42 cnf(850,plain,
% 76.41/76.42 (E(f3(f3(f3(x8501,a2),a2),f1(x8501)),f3(f3(x8502,f1(x8502)),a2))),
% 76.41/76.42 inference(scs_inference,[],[16,185,847,2,3])).
% 76.41/76.42 cnf(852,plain,
% 76.41/76.42 (E(f3(f3(x8521,f1(x8521)),a2),f3(f3(f3(x8522,a2),a2),f1(x8522)))),
% 76.41/76.42 inference(scs_inference,[],[850,2])).
% 76.41/76.42 cnf(853,plain,
% 76.41/76.42 (E(f3(a2,f3(f1(x8531),f3(x8531,a2))),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[16,849,850,2,3])).
% 76.41/76.42 cnf(856,plain,
% 76.41/76.42 (E(f3(a2,f3(x8561,f1(x8561))),f3(f3(f3(x8562,a2),a2),f1(x8562)))),
% 76.41/76.42 inference(scs_inference,[],[16,852,853,2,3])).
% 76.41/76.42 cnf(859,plain,
% 76.41/76.42 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(f4(x8591,a2),a2),a2))),
% 76.41/76.42 inference(scs_inference,[],[16,605,856,2,3])).
% 76.41/76.42 cnf(861,plain,
% 76.41/76.42 (E(f3(f3(f4(x8611,a2),a2),a2),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.42 inference(scs_inference,[],[859,2])).
% 76.41/76.42 cnf(862,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(a2,f3(a2,f4(a2,x8621))))),
% 76.41/76.43 inference(scs_inference,[],[16,625,859,2,3])).
% 76.41/76.43 cnf(864,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f4(a2,x8641))),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[862,2])).
% 76.41/76.43 cnf(865,plain,
% 76.41/76.43 (E(f3(a2,f3(f4(x8651,a2),a2)),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,861,862,2,3])).
% 76.41/76.43 cnf(868,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(a2,x8681)),a2),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,864,865,2,3])).
% 76.41/76.43 cnf(870,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(a2,f4(a2,x8701)),a2))),
% 76.41/76.43 inference(scs_inference,[],[868,2])).
% 76.41/76.43 cnf(871,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x8711,a2)),a2),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,753,868,2,3])).
% 76.41/76.43 cnf(873,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(a2,f4(x8731,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[871,2])).
% 76.41/76.43 cnf(874,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(a2,f4(a2,x8741)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,870,871,2,3])).
% 76.41/76.43 cnf(877,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(a2,f4(x8771,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,873,874,2,3])).
% 76.41/76.43 cnf(879,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x8791,a2)),a2),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[877,2])).
% 76.41/76.43 cnf(880,plain,
% 76.41/76.43 (E(f3(f3(f3(a2,a2),a2),a2),f3(a2,f3(a2,f4(x8801,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,778,877,2,3])).
% 76.41/76.43 cnf(882,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f4(x8821,a2))),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[880,2])).
% 76.41/76.43 cnf(883,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f4(x8831,a2))),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,879,880,2,3])).
% 76.41/76.43 cnf(886,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x8861,a2)),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,882,883,2,3])).
% 76.41/76.43 cnf(888,plain,
% 76.41/76.43 (E(f3(f3(f3(a2,a2),a2),a2),f3(f3(a2,f4(x8881,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[886,2])).
% 76.41/76.43 cnf(889,plain,
% 76.41/76.43 (E(f3(a2,f1(f1(a2))),f3(f3(f4(x8891,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,733,886,2,3])).
% 76.41/76.43 cnf(892,plain,
% 76.41/76.43 (E(f3(a2,f3(f3(a2,a2),a2)),f3(f3(a2,f4(x8921,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,888,889,2,3])).
% 76.41/76.43 cnf(895,plain,
% 76.41/76.43 (E(f3(f3(f3(x8951,a2),a2),f1(x8951)),f3(f3(f4(a2,x8952),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,182,892,2,3])).
% 76.41/76.43 cnf(897,plain,
% 76.41/76.43 (E(f3(f3(f4(a2,x8971),a2),a2),f3(f3(f3(x8972,a2),a2),f1(x8972)))),
% 76.41/76.43 inference(scs_inference,[],[895,2])).
% 76.41/76.43 cnf(898,plain,
% 76.41/76.43 (E(f3(f3(f3(x8981,a2),a2),f1(x8981)),f3(a2,f3(a2,f4(x8982,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,236,895,2,3])).
% 76.41/76.43 cnf(900,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f4(x9001,a2))),f3(f3(f3(x9002,a2),a2),f1(x9002)))),
% 76.41/76.43 inference(scs_inference,[],[898,2])).
% 76.41/76.43 cnf(901,plain,
% 76.41/76.43 (E(f3(a2,f3(f4(a2,x9011),a2)),f3(f3(f3(x9012,a2),a2),f1(x9012)))),
% 76.41/76.43 inference(scs_inference,[],[16,897,898,2,3])).
% 76.41/76.43 cnf(904,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x9041,a2)),a2),f3(f3(f3(x9042,a2),a2),f1(x9042)))),
% 76.41/76.43 inference(scs_inference,[],[16,900,901,2,3])).
% 76.41/76.43 cnf(906,plain,
% 76.41/76.43 (E(f3(f3(f3(x9061,a2),a2),f1(x9061)),f3(f3(a2,f4(x9062,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[904,2])).
% 76.41/76.43 cnf(907,plain,
% 76.41/76.43 (E(f3(f3(f3(x9071,a2),a2),f1(x9071)),f3(a2,f3(a2,f4(a2,x9072))))),
% 76.41/76.43 inference(scs_inference,[],[16,245,904,2,3])).
% 76.41/76.43 cnf(909,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f4(a2,x9091))),f3(f3(f3(x9092,a2),a2),f1(x9092)))),
% 76.41/76.43 inference(scs_inference,[],[907,2])).
% 76.41/76.43 cnf(910,plain,
% 76.41/76.43 (E(f3(f1(x9101),f3(f3(x9101,a2),a2)),f3(f3(a2,f4(x9102,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,906,907,2,3])).
% 76.41/76.43 cnf(913,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(a2,x9131)),a2),f3(f3(f3(x9132,a2),a2),f1(x9132)))),
% 76.41/76.43 inference(scs_inference,[],[16,909,910,2,3])).
% 76.41/76.43 cnf(915,plain,
% 76.41/76.43 (E(f3(f3(f3(x9151,a2),a2),f1(x9151)),f3(f3(a2,f4(a2,x9152)),a2))),
% 76.41/76.43 inference(scs_inference,[],[913,2])).
% 76.41/76.43 cnf(916,plain,
% 76.41/76.43 (E(f3(f3(f3(x9161,a2),a2),f1(x9161)),f3(a2,f3(f4(x9162,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,248,913,2,3])).
% 76.41/76.43 cnf(918,plain,
% 76.41/76.43 (E(f3(a2,f3(f4(x9181,a2),a2)),f3(f3(f3(x9182,a2),a2),f1(x9182)))),
% 76.41/76.43 inference(scs_inference,[],[916,2])).
% 76.41/76.43 cnf(919,plain,
% 76.41/76.43 (E(f3(f1(x9191),f3(f3(x9191,a2),a2)),f3(f3(a2,f4(a2,x9192)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,915,916,2,3])).
% 76.41/76.43 cnf(922,plain,
% 76.41/76.43 (E(f3(f3(f4(x9221,a2),a2),a2),f3(f3(f3(x9222,a2),a2),f1(x9222)))),
% 76.41/76.43 inference(scs_inference,[],[16,918,919,2,3])).
% 76.41/76.43 cnf(925,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x9251,a2)),a2),f3(f3(f1(x9252),x9252),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,775,922,2,3])).
% 76.41/76.43 cnf(927,plain,
% 76.41/76.43 (E(f3(f3(f1(x9271),x9271),a2),f3(f3(a2,f4(x9272,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[925,2])).
% 76.41/76.43 cnf(928,plain,
% 76.41/76.43 (E(f3(a2,f4(x9281,a2)),f3(f3(f1(x9282),f3(f3(x9282,a2),a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,170,925,2,3])).
% 76.41/76.43 cnf(931,plain,
% 76.41/76.43 (E(f3(a2,f3(f1(x9311),x9311)),f3(f3(a2,f4(x9312,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,927,928,2,3])).
% 76.41/76.43 cnf(934,plain,
% 76.41/76.43 (E(f3(f4(f4(x9341,a2),a2),a2),f3(f3(f1(x9342),f3(x9342,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,642,931,2,3])).
% 76.41/76.43 cnf(937,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x9371,a2)),a2),f3(f3(f1(x9372),f3(x9372,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,770,934,2,3])).
% 76.41/76.43 cnf(939,plain,
% 76.41/76.43 (E(f3(f3(f1(x9391),f3(x9391,a2)),a2),f3(f3(a2,f4(x9392,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[937,2])).
% 76.41/76.43 cnf(940,plain,
% 76.41/76.43 (E(f3(f4(f4(x9401,a2),a2),a2),f3(a2,f3(f4(a2,x9402),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,607,937,2,3])).
% 76.41/76.43 cnf(943,plain,
% 76.41/76.43 (E(f3(a2,f3(f1(x9431),f3(x9431,a2))),f3(f3(a2,f4(x9432,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,939,940,2,3])).
% 76.41/76.43 cnf(945,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x9451,a2)),a2),f3(a2,f3(f1(x9452),f3(x9452,a2))))),
% 76.41/76.43 inference(scs_inference,[],[943,2])).
% 76.41/76.43 cnf(946,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x9461,a2)),a2),f3(a2,f3(f4(a2,x9462),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,780,943,2,3])).
% 76.41/76.43 cnf(948,plain,
% 76.41/76.43 (E(f3(a2,f3(f4(a2,x9481),a2)),f3(f3(a2,f4(x9482,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[946,2])).
% 76.41/76.43 cnf(949,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f4(x9491,a2))),f3(a2,f3(f1(x9492),f3(x9492,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,945,946,2,3])).
% 76.41/76.43 cnf(952,plain,
% 76.41/76.43 (E(f3(f3(f4(a2,x9521),a2),a2),f3(f3(a2,f4(x9522,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,948,949,2,3])).
% 76.41/76.43 cnf(955,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,369,952,2,3])).
% 76.41/76.43 cnf(957,plain,
% 76.41/76.43 (E(f3(f1(f1(a2)),a2),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[955,2])).
% 76.41/76.43 cnf(958,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,451,955,2,3])).
% 76.41/76.43 cnf(961,plain,
% 76.41/76.43 (E(f3(f3(f3(x9611,a2),a2),f1(x9611)),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,227,958,2,3])).
% 76.41/76.43 cnf(964,plain,
% 76.41/76.43 (E(f3(f3(f3(x9641,a2),a2),f1(x9641)),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,200,961,2,3])).
% 76.41/76.43 cnf(967,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(a2,f3(f1(x9671),x9671)))),
% 76.41/76.43 inference(scs_inference,[],[16,504,964,2,3])).
% 76.41/76.43 cnf(969,plain,
% 76.41/76.43 (E(f3(a2,f3(f1(x9691),x9691)),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[967,2])).
% 76.41/76.43 cnf(970,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(f1(x9701),x9701),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,531,967,2,3])).
% 76.41/76.43 cnf(973,plain,
% 76.41/76.43 (E(f3(f3(f3(x9731,a2),a2),f1(x9731)),f3(f3(f1(x9732),x9732),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,161,970,2,3])).
% 76.41/76.43 cnf(976,plain,
% 76.41/76.43 (E(f3(f3(f3(x9761,a2),a2),f1(x9761)),f3(a2,f3(f1(x9762),x9762)))),
% 76.41/76.43 inference(scs_inference,[],[16,215,973,2,3])).
% 76.41/76.43 cnf(979,plain,
% 76.41/76.43 (E(f3(f3(f4(x9791,a2),a2),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,601,976,2,3])).
% 76.41/76.43 cnf(982,plain,
% 76.41/76.43 (E(f3(f3(f4(x9821,a2),a2),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,564,979,2,3])).
% 76.41/76.43 cnf(985,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x9851,a2)),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,762,982,2,3])).
% 76.41/76.43 cnf(987,plain,
% 76.41/76.43 (E(f3(f1(f1(a2)),a2),f3(f3(a2,f4(x9871,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[985,2])).
% 76.41/76.43 cnf(988,plain,
% 76.41/76.43 (E(f3(f3(f3(x9881,a2),a2),f1(x9881)),f3(f3(f1(x9882),f3(x9882,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,188,985,2,3])).
% 76.41/76.43 cnf(990,plain,
% 76.41/76.43 (E(f3(f3(f1(x9901),f3(x9901,a2)),a2),f3(f3(f3(x9902,a2),a2),f1(x9902)))),
% 76.41/76.43 inference(scs_inference,[],[988,2])).
% 76.41/76.43 cnf(991,plain,
% 76.41/76.43 (E(f3(a2,f1(f1(a2))),f3(f3(a2,f4(x9911,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,987,988,2,3])).
% 76.41/76.43 cnf(994,plain,
% 76.41/76.43 (E(f3(a2,f3(f1(x9941),f3(x9941,a2))),f3(f3(f3(x9942,a2),a2),f1(x9942)))),
% 76.41/76.43 inference(scs_inference,[],[16,990,991,2,3])).
% 76.41/76.43 cnf(997,plain,
% 76.41/76.43 (E(f3(f4(f4(x9971,a2),a2),a2),f3(f3(x9972,f1(x9972)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,491,994,2,3])).
% 76.41/76.43 cnf(1000,plain,
% 76.41/76.43 (E(f3(f4(f4(x10001,a2),a2),a2),f3(a2,f3(f1(x10002),x10002)))),
% 76.41/76.43 inference(scs_inference,[],[16,508,997,2,3])).
% 76.41/76.43 cnf(1003,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10031),x10031),a2),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,423,1000,2,3])).
% 76.41/76.43 cnf(1006,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10061),x10061),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,402,1003,2,3])).
% 76.41/76.43 cnf(1009,plain,
% 76.41/76.43 (E(f3(f4(f4(x10091,a2),a2),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,466,1006,2,3])).
% 76.41/76.43 cnf(1012,plain,
% 76.41/76.43 (E(f3(f4(f4(x10121,a2),a2),a2),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,476,1009,2,3])).
% 76.41/76.43 cnf(1015,plain,
% 76.41/76.43 (E(f3(f4(f4(x10151,a2),a2),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,392,1012,2,3])).
% 76.41/76.43 cnf(1018,plain,
% 76.41/76.43 (E(f3(f4(x10181,f4(a2,a2)),a2),f3(f1(x10182),f3(f3(x10182,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,267,1015,2,3])).
% 76.41/76.43 cnf(1021,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10211),x10211),a2),f3(f1(x10212),f3(f3(x10212,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,410,1018,2,3])).
% 76.41/76.43 cnf(1024,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(x10241,f1(x10241)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,452,1021,2,3])).
% 76.41/76.43 cnf(1027,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(a2,f3(x10271,f1(x10271))))),
% 76.41/76.43 inference(scs_inference,[],[16,458,1024,2,3])).
% 76.41/76.43 cnf(1029,plain,
% 76.41/76.43 (E(f3(a2,f3(x10291,f1(x10291))),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[1027,2])).
% 76.41/76.43 cnf(1030,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10301),x10301),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1027,424,2,3])).
% 76.41/76.43 cnf(1033,plain,
% 76.41/76.43 (E(f3(a2,f4(a2,x10331)),f3(a2,f1(f1(a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,1030,393,2,3])).
% 76.41/76.43 cnf(1036,plain,
% 76.41/76.43 (E(f3(f4(f4(x10361,a2),a2),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1033,477,2,3])).
% 76.41/76.43 cnf(1039,plain,
% 76.41/76.43 (E(f3(f4(f4(x10391,a2),a2),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1036,467,2,3])).
% 76.41/76.43 cnf(1042,plain,
% 76.41/76.43 (E(f3(f4(x10421,f4(a2,a2)),a2),f3(f3(x10422,f1(x10422)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1039,305,2,3])).
% 76.41/76.43 cnf(1045,plain,
% 76.41/76.43 (E(f3(f4(x10451,f4(a2,a2)),a2),f3(a2,f3(x10452,f1(x10452))))),
% 76.41/76.43 inference(scs_inference,[],[16,314,1042,2,3])).
% 76.41/76.43 cnf(1048,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10481),x10481),a2),f3(a2,f3(x10482,f1(x10482))))),
% 76.41/76.43 inference(scs_inference,[],[16,1045,435,2,3])).
% 76.41/76.43 cnf(1051,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10511),x10511),a2),f3(f3(f1(x10512),f3(x10512,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1048,438,2,3])).
% 76.41/76.43 cnf(1054,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10541),x10541),a2),f3(a2,f3(f1(x10542),f3(x10542,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,441,1051,2,3])).
% 76.41/76.43 cnf(1057,plain,
% 76.41/76.43 (E(f3(f4(f4(x10571,a2),a2),a2),f3(a2,f3(x10572,f1(x10572))))),
% 76.41/76.43 inference(scs_inference,[],[16,1054,411,2,3])).
% 76.41/76.43 cnf(1060,plain,
% 76.41/76.43 (E(f3(f4(x10601,f4(a2,a2)),a2),f3(a2,f3(a2,f4(a2,x10602))))),
% 76.41/76.43 inference(scs_inference,[],[16,1057,352,2,3])).
% 76.41/76.43 cnf(1063,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10631),x10631),a2),f3(a2,f3(f4(x10632,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,1060,413,2,3])).
% 76.41/76.43 cnf(1066,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10661),x10661),a2),f3(a2,f3(f4(a2,x10662),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,416,1063,2,3])).
% 76.41/76.43 cnf(1069,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x10691),x10691),a2),f3(f3(f4(x10692,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,444,1066,2,3])).
% 76.41/76.43 cnf(1072,plain,
% 76.41/76.43 (E(f3(f4(f4(x10721,a2),a2),a2),f3(a2,f3(f1(x10722),f3(x10722,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,532,1069,2,3])).
% 76.41/76.43 cnf(1075,plain,
% 76.41/76.43 (E(f3(f3(f4(x10751,a2),a2),a2),f3(a2,f3(f1(x10752),f3(x10752,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,630,1072,2,3])).
% 76.41/76.43 cnf(1078,plain,
% 76.41/76.43 (E(f3(f4(f4(x10781,a2),a2),a2),f3(a2,f3(f4(x10782,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,1075,643,2,3])).
% 76.41/76.43 cnf(1081,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x10811,a2)),a2),f3(a2,f3(f4(x10812,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,756,1078,2,3])).
% 76.41/76.43 cnf(1084,plain,
% 76.41/76.43 (E(f3(f3(a2,f4(x10841,a2)),a2),f3(f3(f4(x10842,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,763,1081,2,3])).
% 76.41/76.43 cnf(1087,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1084,362,2,3])).
% 76.41/76.43 cnf(1090,plain,
% 76.41/76.43 (E(f3(f1(x10901),x10901),f3(f1(x10902),f3(f3(f3(x10902,a2),a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,1087,117,2,3])).
% 76.41/76.43 cnf(1094,plain,
% 76.41/76.43 (E(f3(x10941,f1(x10941)),f3(f3(f1(x10942),x10942),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1090,302,2,3])).
% 76.41/76.43 cnf(1098,plain,
% 76.41/76.43 (E(f3(x10981,f1(x10981)),f3(a2,f3(f1(x10982),x10982)))),
% 76.41/76.43 inference(scs_inference,[],[16,1094,311,2,3])).
% 76.41/76.43 cnf(1102,plain,
% 76.41/76.43 (E(f3(f4(x11021,f4(a2,a2)),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,1098,268,2,3])).
% 76.41/76.43 cnf(1105,plain,
% 76.41/76.43 (E(f3(f4(x11051,f4(a2,a2)),a2),f3(a2,f3(a2,f3(a2,a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,1102,274,2,3])).
% 76.41/76.43 cnf(1108,plain,
% 76.41/76.43 (E(f3(f4(x11081,f4(a2,a2)),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1105,271,2,3])).
% 76.41/76.43 cnf(1111,plain,
% 76.41/76.43 (E(f3(f4(x11111,f4(a2,a2)),a2),f3(f1(f1(a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1108,277,2,3])).
% 76.41/76.43 cnf(1114,plain,
% 76.41/76.43 (E(f3(f4(x11141,f4(a2,a2)),a2),f3(a2,f1(f1(a2))))),
% 76.41/76.43 inference(scs_inference,[],[16,1111,286,2,3])).
% 76.41/76.43 cnf(1117,plain,
% 76.41/76.43 (E(f3(x11171,f1(x11171)),f3(f3(f1(x11172),f3(x11172,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1114,320,2,3])).
% 76.41/76.43 cnf(1121,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x11211),x11211),a2),f3(a2,f3(f3(a2,a2),a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,1117,419,2,3])).
% 76.41/76.43 cnf(1124,plain,
% 76.41/76.43 (E(f3(f4(f4(a2,x11241),x11241),a2),f3(f3(f3(a2,a2),a2),a2))),
% 76.41/76.43 inference(scs_inference,[],[16,1121,426,2,3])).
% 76.41/76.43 cnf(1127,plain,
% 76.41/76.43 (E(f3(f3(a2,f1(x11271)),x11271),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[17,969,1124,2,3])).
% 76.41/76.43 cnf(1131,plain,
% 76.41/76.43 (E(f3(f3(a2,x11311),f1(x11311)),f3(f3(a2,f3(a2,a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[17,1029,1127,2,3])).
% 76.41/76.43 cnf(1134,plain,
% 76.41/76.43 (E(f3(f3(a2,f3(a2,a2)),a2),f3(f3(a2,x11341),f1(x11341)))),
% 76.41/76.43 inference(scs_inference,[],[1131,2])).
% 76.41/76.43 cnf(1197,plain,
% 76.41/76.43 (E(f3(f3(a2,x11971),f1(x11971)),f3(f1(f1(a2)),a2))),
% 76.41/76.43 inference(scs_inference,[],[957,1134,3,2])).
% 76.41/76.43 cnf(1203,plain,
% 76.41/76.43 (E(f3(f3(a2,x12031),f1(x12031)),f3(f3(f3(x12032,a2),a2),f1(x12032)))),
% 76.41/76.43 inference(scs_inference,[],[1197,840,3])).
% 76.41/76.43 cnf(1232,plain,
% 76.41/76.43 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(a2,x12321),f1(x12321)))),
% 76.41/76.43 inference(scs_inference,[],[17,459,3,2])).
% 76.41/76.43 cnf(1235,plain,
% 76.41/76.43 (E(f3(f3(a2,x12351),f1(x12351)),f3(f3(a2,a2),f3(a2,a2)))),
% 76.41/76.43 inference(scs_inference,[],[17,1232,3,2])).
% 76.41/76.43 cnf(1236,plain,
% 76.41/76.43 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f3(a2,x12361),f1(x12361)))),
% 76.41/76.43 inference(scs_inference,[],[1235,347,3])).
% 76.41/76.43 cnf(1283,plain,
% 76.41/76.43 (E(f4(a2,x12831),f4(f4(a2,x12832),x12831))),
% 76.41/76.43 inference(scs_inference,[],[63,4,5,6,7])).
% 76.41/76.43 cnf(1287,plain,
% 76.41/76.43 (E(f4(x12871,a2),f4(x12871,f4(x12872,a2)))),
% 76.41/76.43 inference(scs_inference,[],[141,8])).
% 76.41/76.43 cnf(1316,plain,
% 76.41/76.43 (~E(f3(f3(a2,x13161),f1(x13161)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 76.41/76.43 inference(scs_inference,[],[1283,1236,7,8,6,4,5,2])).
% 76.41/76.43 cnf(1333,plain,
% 76.41/76.43 (~E(f3(f3(f3(x13331,a2),a2),f1(x13331)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 76.41/76.43 inference(scs_inference,[],[1287,1203,710,1316,8,4,6,5,7,2,3])).
% 76.41/76.43 cnf(1737,plain,
% 76.41/76.43 (E(f4(x17371,f4(x17372,a2)),f4(x17371,a2))),
% 76.41/76.43 inference(scs_inference,[],[10,5,7,8])).
% 76.41/76.43 cnf(1752,plain,
% 76.41/76.43 (E(f4(f4(x17521,f4(x17522,a2)),x17523),f4(f4(x17521,a2),x17523))),
% 76.41/76.43 inference(scs_inference,[],[1737,5,7])).
% 76.41/76.43 cnf(1869,plain,
% 76.41/76.43 (E(f4(f3(x18691,a2),x18692),f4(x18691,x18692))),
% 76.41/76.43 inference(scs_inference,[],[12,1752,8,6,4,7])).
% 76.41/76.43 cnf(1870,plain,
% 76.41/76.43 (E(f3(f3(x18701,a2),x18702),f3(x18701,x18702))),
% 76.41/76.43 inference(scs_inference,[],[12,1752,8,6,4,7,5])).
% 76.41/76.43 cnf(1889,plain,
% 76.41/76.43 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f3(x18891,a2),f1(x18891)))),
% 76.41/76.43 inference(scs_inference,[],[1869,1870,1333,8,6,4,7,5,3,2])).
% 76.41/76.43 cnf(2146,plain,
% 76.41/76.43 (~E(f3(f1(f4(a5,f4(a6,a6))),f4(f4(a5,a6),a6)),f3(f3(x21461,a2),f1(x21461)))),
% 76.41/76.43 inference(scs_inference,[],[16,1889,3])).
% 76.41/76.43 cnf(2148,plain,
% 76.41/76.43 (~E(f3(f3(x21481,a2),f1(x21481)),f3(f1(f4(a5,f4(a6,a6))),f4(f4(a5,a6),a6)))),
% 76.41/76.43 inference(scs_inference,[],[2146,2])).
% 76.41/76.43 cnf(2151,plain,
% 76.41/76.43 (E(f4(x21511,f3(x21512,x21513)),f4(x21511,f3(x21513,x21512)))),
% 76.41/76.43 inference(scs_inference,[],[16,8])).
% 76.41/76.43 cnf(2152,plain,
% 76.41/76.43 (E(f3(x21521,f3(x21522,x21523)),f3(x21521,f3(x21523,x21522)))),
% 76.41/76.43 inference(scs_inference,[],[16,8,6])).
% 76.41/76.43 cnf(2156,plain,
% 76.41/76.43 (~E(f3(f1(x21561),f3(x21561,a2)),f3(f1(f4(a5,f4(a6,a6))),f4(f4(a5,a6),a6)))),
% 76.41/76.43 inference(scs_inference,[],[16,2148,8,6,4,5,7,3])).
% 76.41/76.43 cnf(2158,plain,
% 76.41/76.43 (~E(f3(f1(f4(a5,f4(a6,a6))),f4(f4(a5,a6),a6)),f3(f1(x21581),f3(x21581,a2)))),
% 76.41/76.43 inference(scs_inference,[],[16,2148,8,6,4,5,7,3,2])).
% 76.41/76.43 cnf(2161,plain,
% 76.41/76.43 (~E(f3(f4(a5,f4(a6,a6)),a2),f4(f4(a5,a6),a6))),
% 76.41/76.43 inference(scs_inference,[],[2158,6,2])).
% 76.41/76.43 cnf(2162,plain,
% 76.41/76.43 (~E(f3(f1(x21621),f3(a2,x21621)),f3(f1(f4(a5,f4(a6,a6))),f4(f4(a5,a6),a6)))),
% 76.41/76.43 inference(scs_inference,[],[2152,2158,2156,6,2,3])).
% 76.41/76.43 cnf(2166,plain,
% 76.41/76.43 (~E(f3(a2,f4(a5,f4(a6,a6))),f4(f4(a5,a6),a6))),
% 76.41/76.43 inference(scs_inference,[],[16,2151,2161,2162,6,2,3])).
% 76.41/76.43 cnf(2204,plain,
% 76.41/76.43 (~E(f4(f4(a5,a6),a6),f3(a2,f3(f4(a5,f4(a6,a6)),a2)))),
% 76.41/76.43 inference(scs_inference,[],[2166,58,3,2])).
% 76.41/76.43 cnf(2234,plain,
% 76.41/76.43 (~E(f3(a2,f3(f4(a5,f4(a6,a6)),a2)),f4(a5,f4(a6,a6)))),
% 76.41/76.43 inference(scs_inference,[],[2204,18,3,2])).
% 76.41/76.43 cnf(2245,plain,
% 76.41/76.43 ($false),
% 76.41/76.43 inference(scs_inference,[],[18,2234,2152,114,3,2,8,6,4,7,5]),
% 76.41/76.43 ['proof']).
% 76.41/76.43 % SZS output end Proof
% 76.41/76.43 % Total time :75.740000s
%------------------------------------------------------------------------------