%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG024-7 : 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 : n008.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:41 EDT 2024
% Result : Unsatisfiable 70.83s 70.98s
% Output : CNFRefutation 70.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : RNG024-7 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.32 % Computer : n008.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Tue Jun 18 14:03:09 EDT 2024
% 0.18/0.32 % CPUTime :
% 0.55/0.64 start to proof:theBenchmark
% 70.83/70.97 %-------------------------------------------
% 70.83/70.97 % File :CSE---1.7
% 70.83/70.97 % Problem :theBenchmark
% 70.83/70.97 % Transform :cnf
% 70.83/70.97 % Format :tptp:raw
% 70.83/70.97 % Command :java -jar mcs_scs.jar %d %s
% 70.83/70.97
% 70.83/70.97 % Result :Theorem 70.170000s
% 70.83/70.97 % Output :CNFRefutation 70.170000s
% 70.83/70.97 %-------------------------------------------
% 70.83/70.98 %--------------------------------------------------------------------------
% 70.83/70.98 % File : RNG024-7 : TPTP v8.2.0. Released v1.0.0.
% 70.83/70.98 % Domain : Ring Theory (Alternative)
% 70.83/70.98 % Problem : Right alternative
% 70.83/70.98 % Version : [Ste87] (equality) axioms : Augmented.
% 70.83/70.98 % Theorem formulation : In terms of associators
% 70.83/70.98 % English :
% 70.83/70.98
% 70.83/70.98 % Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin
% 70.83/70.98 % : [Ste92] Stevens (1992), Unpublished Note
% 70.83/70.98 % Source : [TPTP]
% 70.83/70.98 % Names :
% 70.83/70.98
% 70.83/70.98 % Status : Unsatisfiable
% 70.83/70.98 % Rating : 0.05 v8.2.0, 0.04 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.11 v6.4.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.12 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.13 v5.3.0, 0.08 v5.2.0, 0.07 v4.1.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.00 v2.1.0, 0.13 v2.0.0
% 70.83/70.98 % Syntax : Number of clauses : 23 ( 23 unt; 0 nHn; 1 RR)
% 70.83/70.98 % Number of literals : 23 ( 23 equ; 1 neg)
% 70.83/70.98 % Maximal clause size : 1 ( 1 avg)
% 70.83/70.98 % Maximal term depth : 5 ( 2 avg)
% 70.83/70.98 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 70.83/70.98 % Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% 70.83/70.98 % Number of variables : 45 ( 2 sgn)
% 70.83/70.98 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 70.83/70.98
% 70.83/70.98 % Comments :
% 70.83/70.98 %--------------------------------------------------------------------------
% 70.83/70.98 %----Include nonassociative ring axioms
% 70.83/70.98 include('Axioms/RNG003-0.ax').
% 70.83/70.98 %--------------------------------------------------------------------------
% 70.83/70.98 %----The next 7 clause are extra lemmas which Stevens found useful
% 70.83/70.98 cnf(product_of_inverses,axiom,
% 70.83/70.98 multiply(additive_inverse(X),additive_inverse(Y)) = multiply(X,Y) ).
% 70.83/70.98
% 70.83/70.98 cnf(inverse_product1,axiom,
% 70.83/70.98 multiply(additive_inverse(X),Y) = additive_inverse(multiply(X,Y)) ).
% 70.83/70.98
% 70.83/70.98 cnf(inverse_product2,axiom,
% 70.83/70.98 multiply(X,additive_inverse(Y)) = additive_inverse(multiply(X,Y)) ).
% 70.83/70.98
% 70.83/70.98 cnf(distributivity_of_difference1,axiom,
% 70.83/70.98 multiply(X,add(Y,additive_inverse(Z))) = add(multiply(X,Y),additive_inverse(multiply(X,Z))) ).
% 70.83/70.98
% 70.83/70.98 cnf(distributivity_of_difference2,axiom,
% 70.83/70.98 multiply(add(X,additive_inverse(Y)),Z) = add(multiply(X,Z),additive_inverse(multiply(Y,Z))) ).
% 70.83/70.98
% 70.83/70.98 cnf(distributivity_of_difference3,axiom,
% 70.83/70.98 multiply(additive_inverse(X),add(Y,Z)) = add(additive_inverse(multiply(X,Y)),additive_inverse(multiply(X,Z))) ).
% 70.83/70.98
% 70.83/70.98 cnf(distributivity_of_difference4,axiom,
% 70.83/70.98 multiply(add(X,Y),additive_inverse(Z)) = add(additive_inverse(multiply(X,Z)),additive_inverse(multiply(Y,Z))) ).
% 70.83/70.98
% 70.83/70.98 cnf(prove_right_alternative,negated_conjecture,
% 70.83/70.98 associator(x,y,y) != additive_identity ).
% 70.83/70.98
% 70.83/70.98 %--------------------------------------------------------------------------
% 70.83/70.98 %-------------------------------------------
% 70.83/70.98 % Proof found
% 70.83/70.98 % SZS status Theorem for theBenchmark
% 70.83/70.98 % SZS output start Proof
% 70.83/70.98 %ClaNum:29(EqnAxiom:8)
% 70.83/70.98 %VarNum:88(SingletonVarNum:40)
% 70.83/70.98 %MaxLitNum:1
% 70.83/70.98 %MaxfuncDepth:4
% 70.83/70.98 %SharedTerms:10
% 70.83/70.98 %goalClause: 29
% 70.83/70.98 %singleGoalClaCount:1
% 70.83/70.98 [29]~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),a2)
% 70.83/70.98 [10]E(f4(x101,a2),a2)
% 70.83/70.98 [11]E(f4(a2,x111),a2)
% 70.83/70.98 [12]E(f3(x121,a2),x121)
% 70.83/70.98 [13]E(f3(a2,x131),x131)
% 70.83/70.98 [9]E(f1(f1(x91)),x91)
% 70.83/70.98 [14]E(f3(x141,f1(x141)),a2)
% 70.83/70.98 [15]E(f3(f1(x151),x151),a2)
% 70.83/70.98 [16]E(f3(x161,x162),f3(x162,x161))
% 70.83/70.98 [17]E(f4(f1(x171),f1(x172)),f4(x171,x172))
% 70.83/70.98 [18]E(f1(f4(x181,x182)),f4(x181,f1(x182)))
% 70.83/70.98 [19]E(f1(f4(x191,x192)),f4(f1(x191),x192))
% 70.83/70.98 [21]E(f4(f4(x211,x212),x212),f4(x211,f4(x212,x212)))
% 70.83/70.98 [22]E(f4(f4(x221,x221),x222),f4(x221,f4(x221,x222)))
% 70.83/70.98 [20]E(f3(f3(x201,x202),x203),f3(x201,f3(x202,x203)))
% 70.83/70.98 [23]E(f3(f4(x231,x232),f4(x231,x233)),f4(x231,f3(x232,x233)))
% 70.83/70.98 [24]E(f3(f4(x241,x242),f4(x243,x242)),f4(f3(x241,x243),x242))
% 70.83/70.98 [25]E(f3(f4(x251,x252),f1(f4(x251,x253))),f4(x251,f3(x252,f1(x253))))
% 70.83/70.98 [26]E(f3(f4(x261,x262),f1(f4(x263,x262))),f4(f3(x261,f1(x263)),x262))
% 70.83/70.98 [27]E(f3(f1(f4(x271,x272)),f1(f4(x271,x273))),f4(f1(x271),f3(x272,x273)))
% 70.83/70.98 [28]E(f3(f1(f4(x281,x282)),f1(f4(x283,x282))),f4(f3(x281,x283),f1(x282)))
% 70.83/70.98 %EqnAxiom
% 70.83/70.98 [1]E(x11,x11)
% 70.83/70.98 [2]E(x22,x21)+~E(x21,x22)
% 70.83/70.98 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 70.83/70.98 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 70.83/70.98 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 70.83/70.98 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 70.83/70.98 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 70.83/70.98 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 70.83/70.98
% 70.83/70.98 %-------------------------------------------
% 70.83/70.99 cnf(30,plain,
% 70.83/70.99 (E(x301,f3(x301,a2))),
% 70.83/70.99 inference(scs_inference,[],[12,2])).
% 70.83/70.99 cnf(31,plain,
% 70.83/70.99 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,a2))),
% 70.83/70.99 inference(scs_inference,[],[29,12,2,3])).
% 70.83/70.99 cnf(33,plain,
% 70.83/70.99 (E(x331,f3(a2,x331))),
% 70.83/70.99 inference(scs_inference,[],[13,2])).
% 70.83/70.99 cnf(34,plain,
% 70.83/70.99 (E(f3(a2,f4(f4(x341,x342),x342)),f4(x341,f4(x342,x342)))),
% 70.83/70.99 inference(scs_inference,[],[13,21,2,3])).
% 70.83/70.99 cnf(36,plain,
% 70.83/70.99 (E(f4(x361,f4(x362,x362)),f3(a2,f4(f4(x361,x362),x362)))),
% 70.83/70.99 inference(scs_inference,[],[34,2])).
% 70.83/70.99 cnf(37,plain,
% 70.83/70.99 (E(f3(f4(x371,x372),f4(x371,x373)),f4(x371,f3(x373,x372)))),
% 70.83/70.99 inference(scs_inference,[],[34,16,23,2,3])).
% 70.83/70.99 cnf(39,plain,
% 70.83/70.99 (E(f4(x391,f3(x392,x393)),f3(f4(x391,x393),f4(x391,x392)))),
% 70.83/70.99 inference(scs_inference,[],[37,2])).
% 70.83/70.99 cnf(40,plain,
% 70.83/70.99 (E(f1(f1(f3(f4(x401,x402),f4(x401,x403)))),f4(x401,f3(x403,x402)))),
% 70.83/70.99 inference(scs_inference,[],[37,9,2,3])).
% 70.83/70.99 cnf(42,plain,
% 70.83/70.99 (E(f4(x421,f3(x422,x423)),f1(f1(f3(f4(x421,x423),f4(x421,x422)))))),
% 70.83/71.00 inference(scs_inference,[],[40,2])).
% 70.83/71.00 cnf(43,plain,
% 70.83/71.00 (E(f4(x431,f3(x432,x432)),f4(f3(x431,x431),x432))),
% 70.83/71.00 inference(scs_inference,[],[39,40,24,2,3])).
% 70.83/71.00 cnf(46,plain,
% 70.83/71.00 (E(f4(f3(x461,x461),x462),f4(x461,f3(x462,x462)))),
% 70.83/71.00 inference(scs_inference,[],[43,2])).
% 70.83/71.00 cnf(47,plain,
% 70.83/71.00 (E(f4(x471,f3(f3(x472,x473),f3(x472,x473))),f3(f4(f3(x471,x471),x473),f4(f3(x471,x471),x472)))),
% 70.83/71.00 inference(scs_inference,[],[39,43,2,3])).
% 70.83/71.00 cnf(50,plain,
% 70.83/71.00 (E(f3(f4(f3(x501,x501),x502),f4(f3(x501,x501),x503)),f4(x501,f3(f3(x503,x502),f3(x503,x502))))),
% 70.83/71.00 inference(scs_inference,[],[47,2])).
% 70.83/71.00 cnf(51,plain,
% 70.83/71.00 (E(f4(f3(x511,x511),x512),f1(f1(f3(f4(x511,x512),f4(x511,x512)))))),
% 70.83/71.00 inference(scs_inference,[],[46,42,47,2,3])).
% 70.83/71.00 cnf(53,plain,
% 70.83/71.00 (E(f1(f1(f3(f4(x531,x532),f4(x531,x532)))),f4(f3(x531,x531),x532))),
% 70.83/71.00 inference(scs_inference,[],[51,2])).
% 70.83/71.00 cnf(54,plain,
% 70.83/71.00 (E(f3(f4(f3(x541,x541),x542),f4(f3(x541,x541),x543)),f3(f4(x541,f3(x543,x542)),f4(x541,f3(x543,x542))))),
% 70.83/71.00 inference(scs_inference,[],[50,39,51,2,3])).
% 70.83/71.00 cnf(56,plain,
% 70.83/71.00 (E(f3(f4(x561,f3(x562,x563)),f4(x561,f3(x562,x563))),f3(f4(f3(x561,x561),x563),f4(f3(x561,x561),x562)))),
% 70.83/71.00 inference(scs_inference,[],[54,2])).
% 70.83/71.00 cnf(61,plain,
% 70.83/71.00 (E(f4(f3(f4(x611,x611),f4(x611,x611)),x612),f4(x611,f4(x611,f3(x612,x612))))),
% 70.83/71.00 inference(scs_inference,[],[46,22,2,3])).
% 70.83/71.00 cnf(64,plain,
% 70.83/71.00 (E(f4(x641,f4(x641,f3(x642,x642))),f4(f3(f4(x641,x641),f4(x641,x641)),x642))),
% 70.83/71.00 inference(scs_inference,[],[61,2])).
% 70.83/71.00 cnf(65,plain,
% 70.83/71.00 (E(f1(f4(f1(x651),x652)),f4(x651,x652))),
% 70.83/71.00 inference(scs_inference,[],[61,17,18,2,3])).
% 70.83/71.00 cnf(68,plain,
% 70.83/71.00 (E(f4(x681,x682),f1(f4(f1(x681),x682)))),
% 70.83/71.00 inference(scs_inference,[],[65,2])).
% 70.83/71.00 cnf(69,plain,
% 70.83/71.00 (E(f1(f1(f1(f4(x691,x692)))),f4(f1(x691),x692))),
% 70.83/71.00 inference(scs_inference,[],[65,19,9,2,3])).
% 70.83/71.00 cnf(71,plain,
% 70.83/71.00 (E(f4(f1(x711),x712),f1(f1(f1(f4(x711,x712)))))),
% 70.83/71.00 inference(scs_inference,[],[69,2])).
% 70.83/71.00 cnf(72,plain,
% 70.83/71.00 (E(f3(x721,x722),f3(x721,f3(x722,a2)))),
% 70.83/71.00 inference(scs_inference,[],[30,69,20,2,3])).
% 70.83/71.00 cnf(75,plain,
% 70.83/71.00 (E(f3(x751,f3(x752,a2)),f3(x751,x752))),
% 70.83/71.00 inference(scs_inference,[],[72,2])).
% 70.83/71.00 cnf(76,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f4(x761,a2))),
% 70.83/71.00 inference(scs_inference,[],[29,72,10,2,3])).
% 70.83/71.00 cnf(77,plain,
% 70.83/71.00 (E(a2,f4(a2,x771))),
% 70.83/71.00 inference(scs_inference,[],[11,2])).
% 70.83/71.00 cnf(81,plain,
% 70.83/71.00 (E(a2,f3(x811,f1(x811)))),
% 70.83/71.00 inference(scs_inference,[],[14,2])).
% 70.83/71.00 cnf(82,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,f3(a2,a2)))),
% 70.83/71.00 inference(scs_inference,[],[75,31,14,2,3])).
% 70.83/71.00 cnf(84,plain,
% 70.83/71.00 (E(a2,f3(f1(x841),x841))),
% 70.83/71.00 inference(scs_inference,[],[15,2])).
% 70.83/71.00 cnf(85,plain,
% 70.83/71.00 (E(f3(f1(x851),x851),f3(x852,f1(x852)))),
% 70.83/71.00 inference(scs_inference,[],[81,15,2,3])).
% 70.83/71.00 cnf(86,plain,
% 70.83/71.00 (E(f3(x861,f1(x861)),f3(f1(x862),x862))),
% 70.83/71.00 inference(scs_inference,[],[85,2])).
% 70.83/71.00 cnf(87,plain,
% 70.83/71.00 (E(f4(x871,a2),f3(f1(x872),x872))),
% 70.83/71.00 inference(scs_inference,[],[84,85,10,2,3])).
% 70.83/71.00 cnf(88,plain,
% 70.83/71.00 (E(f3(f1(x881),x881),f4(x882,a2))),
% 70.83/71.00 inference(scs_inference,[],[87,2])).
% 70.83/71.00 cnf(89,plain,
% 70.83/71.00 (E(f1(a2),f3(f1(x891),x891))),
% 70.83/71.00 inference(scs_inference,[],[86,33,87,2,3])).
% 70.83/71.00 cnf(92,plain,
% 70.83/71.00 (E(f3(f1(x921),x921),f1(a2))),
% 70.83/71.00 inference(scs_inference,[],[89,2])).
% 70.83/71.00 cnf(93,plain,
% 70.83/71.00 (E(f3(f1(x931),x931),f1(f1(f1(f4(x932,a2)))))),
% 70.83/71.00 inference(scs_inference,[],[71,88,89,2,3])).
% 70.83/71.00 cnf(96,plain,
% 70.83/71.00 (E(f1(f1(f1(f4(x961,a2)))),f3(f1(x962),x962))),
% 70.83/71.00 inference(scs_inference,[],[93,2])).
% 70.83/71.00 cnf(97,plain,
% 70.83/71.00 (E(f3(x971,f1(x971)),f1(a2))),
% 70.83/71.00 inference(scs_inference,[],[92,86,93,2,3])).
% 70.83/71.00 cnf(99,plain,
% 70.83/71.00 (E(f1(a2),f3(x991,f1(x991)))),
% 70.83/71.00 inference(scs_inference,[],[97,2])).
% 70.83/71.00 cnf(100,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f1(x1001),x1001))),
% 70.83/71.00 inference(scs_inference,[],[88,97,76,2,3])).
% 70.83/71.00 cnf(106,plain,
% 70.83/71.00 (E(f1(f1(f1(f4(x1061,a2)))),f1(a2))),
% 70.83/71.00 inference(scs_inference,[],[96,92,26,2,3])).
% 70.83/71.00 cnf(108,plain,
% 70.83/71.00 (E(f1(a2),f1(f1(f1(f4(x1081,a2)))))),
% 70.83/71.00 inference(scs_inference,[],[106,2])).
% 70.83/71.00 cnf(109,plain,
% 70.83/71.00 (E(f4(a2,x1091),f3(x1092,f1(x1092)))),
% 70.83/71.00 inference(scs_inference,[],[81,106,11,2,3])).
% 70.83/71.00 cnf(110,plain,
% 70.83/71.00 (E(f3(x1101,f1(x1101)),f4(a2,x1102))),
% 70.83/71.00 inference(scs_inference,[],[109,2])).
% 70.83/71.00 cnf(111,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(x1111,f1(x1111)))),
% 70.83/71.00 inference(scs_inference,[],[86,109,100,2,3])).
% 70.83/71.00 cnf(113,plain,
% 70.83/71.00 (E(f4(f1(x1131),f3(x1132,x1133)),f3(f1(f4(x1131,x1132)),f1(f4(x1131,x1133))))),
% 70.83/71.00 inference(scs_inference,[],[27,2])).
% 70.83/71.00 cnf(114,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f1(a2))),
% 70.83/71.00 inference(scs_inference,[],[99,111,27,2,3])).
% 70.83/71.00 cnf(116,plain,
% 70.83/71.00 (E(f4(f3(x1161,x1162),f1(x1163)),f3(f1(f4(x1161,x1163)),f1(f4(x1162,x1163))))),
% 70.83/71.00 inference(scs_inference,[],[28,2])).
% 70.83/71.00 cnf(123,plain,
% 70.83/71.00 (E(f4(x1231,f3(x1232,x1233)),f3(f4(x1231,x1232),f4(x1231,x1233)))),
% 70.83/71.00 inference(scs_inference,[],[23,2])).
% 70.83/71.00 cnf(127,plain,
% 70.83/71.00 (E(f4(f3(x1271,x1272),x1273),f3(f4(x1271,x1273),f4(x1272,x1273)))),
% 70.83/71.00 inference(scs_inference,[],[24,2])).
% 70.83/71.00 cnf(128,plain,
% 70.83/71.00 (E(f4(f3(x1281,x1281),f3(x1282,x1283)),f3(f4(x1281,f3(x1283,x1282)),f4(x1281,f3(x1283,x1282))))),
% 70.83/71.00 inference(scs_inference,[],[123,54,24,2,3])).
% 70.83/71.00 cnf(131,plain,
% 70.83/71.00 (E(f3(f4(x1311,f3(x1312,x1313)),f4(x1311,f3(x1312,x1313))),f4(f3(x1311,x1311),f3(x1313,x1312)))),
% 70.83/71.00 inference(scs_inference,[],[128,2])).
% 70.83/71.00 cnf(132,plain,
% 70.83/71.00 (E(f4(f3(f3(x1321,x1321),f3(x1321,x1321)),x1322),f3(f4(x1321,f3(x1322,x1322)),f4(x1321,f3(x1322,x1322))))),
% 70.83/71.00 inference(scs_inference,[],[127,128,54,2,3])).
% 70.83/71.00 cnf(135,plain,
% 70.83/71.00 (E(f3(f4(x1351,f3(x1352,x1352)),f4(x1351,f3(x1352,x1352))),f4(f3(f3(x1351,x1351),f3(x1351,x1351)),x1352))),
% 70.83/71.00 inference(scs_inference,[],[132,2])).
% 70.83/71.00 cnf(136,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f3(a2,a2),a2))),
% 70.83/71.00 inference(scs_inference,[],[132,82,16,2,3])).
% 70.83/71.00 cnf(138,plain,
% 70.83/71.00 (E(f4(x1381,x1382),f4(f1(x1381),f1(x1382)))),
% 70.83/71.00 inference(scs_inference,[],[17,2])).
% 70.83/71.00 cnf(141,plain,
% 70.83/71.00 (E(f4(x1411,f1(x1412)),f1(f4(x1411,x1412)))),
% 70.83/71.00 inference(scs_inference,[],[18,2])).
% 70.83/71.00 cnf(142,plain,
% 70.83/71.00 (E(f1(f1(f3(f4(x1421,x1422),f4(x1421,x1422)))),f4(f1(f3(x1421,x1421)),f1(x1422)))),
% 70.83/71.00 inference(scs_inference,[],[53,138,18,2,3])).
% 70.83/71.00 cnf(145,plain,
% 70.83/71.00 (E(f3(f4(x1451,f3(x1452,x1453)),f4(x1451,f3(x1452,x1453))),f1(f4(f1(f3(x1451,x1451)),f3(x1453,x1452))))),
% 70.83/71.00 inference(scs_inference,[],[131,68,142,2,3])).
% 70.83/71.00 cnf(147,plain,
% 70.83/71.00 (E(f1(f4(f1(f3(x1471,x1471)),f3(x1472,x1473))),f3(f4(x1471,f3(x1473,x1472)),f4(x1471,f3(x1473,x1472))))),
% 70.83/71.00 inference(scs_inference,[],[145,2])).
% 70.83/71.00 cnf(148,plain,
% 70.83/71.00 (E(f3(f4(x1481,f3(x1482,x1482)),f4(x1481,f3(x1482,x1482))),f4(f1(f3(f3(x1481,x1481),f3(x1481,x1481))),f1(x1482)))),
% 70.83/71.00 inference(scs_inference,[],[135,138,145,2,3])).
% 70.83/71.00 cnf(150,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x1501,x1501),f3(x1501,x1501))),f1(x1502)),f3(f4(x1501,f3(x1502,x1502)),f4(x1501,f3(x1502,x1502))))),
% 70.83/71.00 inference(scs_inference,[],[148,2])).
% 70.83/71.00 cnf(151,plain,
% 70.83/71.00 (E(f1(f4(f1(f3(x1511,x1511)),f3(x1512,x1513))),f3(f4(f3(x1511,x1511),x1512),f4(f3(x1511,x1511),x1513)))),
% 70.83/71.00 inference(scs_inference,[],[56,147,148,2,3])).
% 70.83/71.00 cnf(153,plain,
% 70.83/71.00 (E(f3(f4(f3(x1531,x1531),x1532),f4(f3(x1531,x1531),x1533)),f1(f4(f1(f3(x1531,x1531)),f3(x1532,x1533))))),
% 70.83/71.00 inference(scs_inference,[],[151,2])).
% 70.83/71.00 cnf(154,plain,
% 70.83/71.00 (E(f4(x1541,f4(x1541,f3(x1542,x1542))),f3(f4(f4(x1541,x1541),x1542),f4(f4(x1541,x1541),x1542)))),
% 70.83/71.00 inference(scs_inference,[],[64,127,151,2,3])).
% 70.83/71.00 cnf(157,plain,
% 70.83/71.00 (E(f3(x1571,f1(x1571)),f1(f4(a2,x1572)))),
% 70.83/71.00 inference(scs_inference,[],[141,110,154,2,3])).
% 70.83/71.00 cnf(161,plain,
% 70.83/71.00 (E(a2,f3(f4(a2,x1611),f4(a2,x1612)))),
% 70.83/71.00 inference(scs_inference,[],[77,123,157,2,3])).
% 70.83/71.00 cnf(164,plain,
% 70.83/71.00 (E(f3(f4(a2,x1641),f4(a2,x1642)),a2)),
% 70.83/71.00 inference(scs_inference,[],[161,2])).
% 70.83/71.00 cnf(167,plain,
% 70.83/71.00 (E(f4(f1(x1671),x1672),f1(f4(x1671,x1672)))),
% 70.83/71.00 inference(scs_inference,[],[19,2])).
% 70.83/71.00 cnf(168,plain,
% 70.83/71.00 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(f4(a2,x1681),f4(a2,x1682)))),
% 70.83/71.00 inference(scs_inference,[],[29,164,19,2,3])).
% 70.83/71.00 cnf(169,plain,
% 70.83/71.00 (E(f3(x1691,f3(x1692,x1693)),f3(f3(x1691,x1692),x1693))),
% 70.83/71.00 inference(scs_inference,[],[20,2])).
% 70.83/71.00 cnf(172,plain,
% 70.83/71.00 (E(x1721,f1(f1(x1721)))),
% 70.83/71.00 inference(scs_inference,[],[9,2])).
% 70.83/71.00 cnf(173,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x1731,x1731),f3(x1731,x1731))),f1(x1732)),f3(f4(f3(x1731,x1731),x1732),f4(f3(x1731,x1731),x1732)))),
% 70.83/71.00 inference(scs_inference,[],[150,56,9,2,3])).
% 70.83/71.00 cnf(175,plain,
% 70.83/71.00 (E(f3(f4(f3(x1751,x1751),x1752),f4(f3(x1751,x1751),x1752)),f4(f1(f3(f3(x1751,x1751),f3(x1751,x1751))),f1(x1752)))),
% 70.83/71.00 inference(scs_inference,[],[173,2])).
% 70.83/71.00 cnf(176,plain,
% 70.83/71.00 (E(f3(x1761,f3(x1762,x1763)),f1(f1(f3(f3(x1761,x1762),x1763))))),
% 70.83/71.00 inference(scs_inference,[],[169,172,173,2,3])).
% 70.83/71.00 cnf(179,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x1791,x1791),f3(x1791,x1791))),f1(x1792)),f1(f4(f1(f3(x1791,x1791)),f3(x1792,x1792))))),
% 70.83/71.00 inference(scs_inference,[],[150,176,145,2,3])).
% 70.83/71.00 cnf(181,plain,
% 70.83/71.00 (E(f1(f4(f1(f3(x1811,x1811)),f3(x1812,x1812))),f4(f1(f3(f3(x1811,x1811),f3(x1811,x1811))),f1(x1812)))),
% 70.83/71.00 inference(scs_inference,[],[179,2])).
% 70.83/71.00 cnf(184,plain,
% 70.83/71.00 (E(a2,f4(x1841,a2))),
% 70.83/71.00 inference(scs_inference,[],[10,2])).
% 70.83/71.00 cnf(185,plain,
% 70.83/71.00 (E(f1(f1(f4(x1851,x1852))),f1(f4(f1(x1851),x1852)))),
% 70.83/71.00 inference(scs_inference,[],[9,68,3])).
% 70.83/71.00 cnf(187,plain,
% 70.83/71.00 (E(f1(f4(f1(x1871),x1872)),f1(f1(f4(x1871,x1872))))),
% 70.83/71.00 inference(scs_inference,[],[9,68,3,2])).
% 70.83/71.00 cnf(190,plain,
% 70.83/71.00 (E(f3(f1(f4(x1901,x1902)),f1(f4(x1901,x1903))),f3(f4(f1(x1901),f3(x1902,x1903)),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,113,3,2])).
% 70.83/71.00 cnf(193,plain,
% 70.83/71.00 (E(f3(f1(f4(x1931,x1932)),f1(f4(x1933,x1932))),f3(f4(f3(x1931,x1933),f1(x1932)),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,116,3,2])).
% 70.83/71.00 cnf(196,plain,
% 70.83/71.00 (E(f3(a2,f4(f4(x1961,x1962),x1962)),f3(f4(x1961,f4(x1962,x1962)),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,36,3,2])).
% 70.83/71.00 cnf(197,plain,
% 70.83/71.00 (E(f3(f4(x1971,x1972),a2),f1(f4(f1(x1971),x1972)))),
% 70.83/71.00 inference(scs_inference,[],[12,68,3])).
% 70.83/71.00 cnf(199,plain,
% 70.83/71.00 (E(f1(f4(f1(x1991),x1992)),f3(f4(x1991,x1992),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,68,3,2])).
% 70.83/71.00 cnf(200,plain,
% 70.83/71.00 (E(f3(f1(f4(f1(x2001),x2002)),a2),f3(f4(x2001,x2002),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,199,3])).
% 70.83/71.00 cnf(202,plain,
% 70.83/71.00 (E(f3(f4(x2021,x2022),a2),f3(f1(f4(f1(x2021),x2022)),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,199,3,2])).
% 70.83/71.00 cnf(203,plain,
% 70.83/71.00 (E(f3(f3(f4(x2031,x2032),a2),a2),f1(f4(f1(x2031),x2032)))),
% 70.83/71.00 inference(scs_inference,[],[12,197,3])).
% 70.83/71.00 cnf(205,plain,
% 70.83/71.00 (E(f1(f4(f1(x2051),x2052)),f3(f3(f4(x2051,x2052),a2),a2))),
% 70.83/71.00 inference(scs_inference,[],[12,197,3,2])).
% 70.83/71.00 cnf(211,plain,
% 70.83/71.00 (E(f3(f1(f4(x2111,x2112)),f1(f4(x2111,x2113))),f3(a2,f4(f1(x2111),f3(x2112,x2113))))),
% 70.83/71.00 inference(scs_inference,[],[13,113,3,2])).
% 70.83/71.00 cnf(214,plain,
% 70.83/71.00 (E(f3(f1(f4(x2141,x2142)),f1(f4(x2143,x2142))),f3(a2,f4(f3(x2141,x2143),f1(x2142))))),
% 70.83/71.00 inference(scs_inference,[],[13,116,3,2])).
% 70.83/71.00 cnf(220,plain,
% 70.83/71.00 (E(f3(a2,f4(f4(x2201,x2202),x2202)),f3(a2,f4(x2201,f4(x2202,x2202))))),
% 70.83/71.00 inference(scs_inference,[],[13,36,3,2])).
% 70.83/71.00 cnf(221,plain,
% 70.83/71.00 (E(f3(a2,f4(x2211,x2212)),f1(f4(f1(x2211),x2212)))),
% 70.83/71.00 inference(scs_inference,[],[13,68,3])).
% 70.83/71.00 cnf(223,plain,
% 70.83/71.00 (E(f1(f4(f1(x2231),x2232)),f3(a2,f4(x2231,x2232)))),
% 70.83/71.00 inference(scs_inference,[],[13,68,3,2])).
% 70.83/71.00 cnf(227,plain,
% 70.83/71.00 (E(f3(a2,f3(a2,f4(x2271,x2272))),f1(f4(f1(x2271),x2272)))),
% 70.83/71.00 inference(scs_inference,[],[13,221,3])).
% 70.83/71.00 cnf(229,plain,
% 70.83/71.00 (E(f1(f4(f1(x2291),x2292)),f3(a2,f3(a2,f4(x2291,x2292))))),
% 70.83/71.00 inference(scs_inference,[],[13,221,3,2])).
% 70.83/71.00 cnf(232,plain,
% 70.83/71.00 (E(f1(f4(f1(x2321),x2322)),f3(a2,f3(f4(x2321,x2322),a2)))),
% 70.83/71.00 inference(scs_inference,[],[13,197,3,2])).
% 70.83/71.00 cnf(233,plain,
% 70.83/71.00 (E(f4(f1(x2331),f3(x2332,x2332)),f3(f4(f3(x2331,x2331),f1(x2332)),a2))),
% 70.83/71.00 inference(scs_inference,[],[193,113,3])).
% 70.83/71.00 cnf(237,plain,
% 70.83/71.00 (E(f4(f3(x2371,x2371),f1(x2372)),f3(f4(f1(x2371),f3(x2372,x2372)),a2))),
% 70.83/71.00 inference(scs_inference,[],[190,116,3])).
% 70.83/71.00 cnf(241,plain,
% 70.83/71.00 (E(f4(f1(x2411),f3(x2412,x2412)),f3(a2,f4(f3(x2411,x2411),f1(x2412))))),
% 70.83/71.00 inference(scs_inference,[],[214,113,3])).
% 70.83/71.00 cnf(245,plain,
% 70.83/71.00 (E(f4(f3(x2451,x2451),f1(x2452)),f3(a2,f4(f1(x2451),f3(x2452,x2452))))),
% 70.83/71.00 inference(scs_inference,[],[211,116,3])).
% 70.83/71.00 cnf(249,plain,
% 70.83/71.00 (E(f4(f4(x2491,x2492),x2492),f3(a2,f4(x2491,f4(x2492,x2492))))),
% 70.83/71.00 inference(scs_inference,[],[220,33,3])).
% 70.83/71.00 cnf(254,plain,
% 70.83/71.00 (E(f3(a2,f4(f3(x2541,x2541),f3(x2542,x2543))),f3(f4(f3(x2541,x2541),x2542),f4(f3(x2541,x2541),x2543)))),
% 70.83/71.00 inference(scs_inference,[],[153,223,3,2])).
% 70.83/71.00 cnf(258,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x2581,x2581),f3(x2581,x2581))),f1(x2582)),f3(a2,f4(f3(x2581,x2581),f3(x2582,x2582))))),
% 70.83/71.00 inference(scs_inference,[],[175,254,3,2])).
% 70.83/71.00 cnf(261,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x2611,x2611),f3(x2611,x2611))),f1(x2612)),f4(f1(f3(x2611,x2611)),f1(f3(x2612,x2612))))),
% 70.83/71.00 inference(scs_inference,[],[181,141,3,2])).
% 70.83/71.00 cnf(271,plain,
% 70.83/71.00 (E(f3(f4(f3(x2711,x2711),f3(x2712,x2713)),a2),f3(f4(f3(x2711,x2711),x2712),f4(f3(x2711,x2711),x2713)))),
% 70.83/71.00 inference(scs_inference,[],[153,199,3,2])).
% 70.83/71.00 cnf(272,plain,
% 70.83/71.00 (E(f4(f1(x2721),f1(x2722)),f3(f3(f4(x2721,x2722),a2),a2))),
% 70.83/71.00 inference(scs_inference,[],[205,141,3])).
% 70.83/71.00 cnf(275,plain,
% 70.83/71.00 (E(f3(f3(f4(x2751,x2752),a2),a2),f4(f1(x2751),f1(x2752)))),
% 70.83/71.00 inference(scs_inference,[],[205,141,3,2])).
% 70.83/71.00 cnf(286,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x2861,x2861),f3(x2861,x2861))),f1(x2862)),f3(f4(f3(x2861,x2861),f3(x2862,x2862)),a2))),
% 70.83/71.00 inference(scs_inference,[],[271,175,3,2])).
% 70.83/71.00 cnf(290,plain,
% 70.83/71.00 (E(f3(f4(x2901,x2902),f3(a2,a2)),f1(f4(f1(x2901),x2902)))),
% 70.83/71.00 inference(scs_inference,[],[169,203,3])).
% 70.83/71.00 cnf(292,plain,
% 70.83/71.00 (E(f1(f4(f1(x2921),x2922)),f3(f4(x2921,x2922),f3(a2,a2)))),
% 70.83/71.00 inference(scs_inference,[],[169,203,3,2])).
% 70.83/71.00 cnf(295,plain,
% 70.83/71.00 (E(f3(f4(f3(x2951,x2951),f3(x2952,x2953)),f3(a2,a2)),f3(f4(f3(x2951,x2951),x2952),f4(f3(x2951,x2951),x2953)))),
% 70.83/71.00 inference(scs_inference,[],[292,153,3,2])).
% 70.83/71.00 cnf(296,plain,
% 70.83/71.00 (E(f4(f1(x2961),f1(x2962)),f3(a2,f3(f4(x2961,x2962),a2)))),
% 70.83/71.00 inference(scs_inference,[],[232,141,3])).
% 70.83/71.00 cnf(302,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x3021,x3021),f3(x3021,x3021))),f1(x3022)),f4(f1(f1(f3(x3021,x3021))),f3(x3022,x3022)))),
% 70.83/71.00 inference(scs_inference,[],[181,167,3,2])).
% 70.83/71.00 cnf(303,plain,
% 70.83/71.00 (E(f3(f4(f3(x3031,x3031),f3(x3032,x3032)),f3(a2,a2)),f4(f1(f3(f3(x3031,x3031),f3(x3031,x3031))),f1(x3032)))),
% 70.83/71.00 inference(scs_inference,[],[295,175,3])).
% 70.83/71.00 cnf(306,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x3061,x3061),f3(x3061,x3061))),f1(x3062)),f3(f4(f3(x3061,x3061),f3(x3062,x3062)),f3(a2,a2)))),
% 70.83/71.00 inference(scs_inference,[],[295,175,3,2])).
% 70.83/71.00 cnf(317,plain,
% 70.83/71.00 (E(f3(f4(x3171,f4(x3172,x3172)),a2),f3(f4(f4(x3171,x3172),x3172),a2))),
% 70.83/71.00 inference(scs_inference,[],[16,196,3,2])).
% 70.83/71.00 cnf(320,plain,
% 70.83/71.00 (E(f3(f4(f4(x3201,x3202),x3202),a2),f3(a2,f4(x3201,f4(x3202,x3202))))),
% 70.83/71.00 inference(scs_inference,[],[16,317,3,2])).
% 70.83/71.00 cnf(323,plain,
% 70.83/71.00 (E(f3(f1(f4(f1(x3231),x3232)),a2),f3(a2,f4(x3231,x3232)))),
% 70.83/71.00 inference(scs_inference,[],[16,202,3,2])).
% 70.83/71.00 cnf(335,plain,
% 70.83/71.00 (E(f3(f4(f1(x3351),f3(x3352,x3353)),a2),f3(f1(f4(x3351,x3353)),f1(f4(x3351,x3352))))),
% 70.83/71.00 inference(scs_inference,[],[16,190,3,2])).
% 70.83/71.00 cnf(338,plain,
% 70.83/71.00 (E(f3(f1(f4(x3381,x3382)),f1(f4(x3381,x3383))),f3(a2,f4(f1(x3381),f3(x3383,x3382))))),
% 70.83/71.00 inference(scs_inference,[],[16,335,3,2])).
% 70.83/71.00 cnf(341,plain,
% 70.83/71.00 (E(f3(f4(f3(x3411,x3412),f1(x3413)),a2),f3(f1(f4(x3412,x3413)),f1(f4(x3411,x3413))))),
% 70.83/71.00 inference(scs_inference,[],[16,193,3,2])).
% 70.83/71.00 cnf(344,plain,
% 70.83/71.00 (E(f3(f1(f4(x3441,x3442)),f1(f4(x3443,x3442))),f3(a2,f4(f3(x3443,x3441),f1(x3442))))),
% 70.83/71.00 inference(scs_inference,[],[16,341,3,2])).
% 70.83/71.00 cnf(347,plain,
% 70.83/71.00 (E(f1(f4(f1(f3(x3471,x3471)),f3(x3472,x3473))),f3(f4(f3(x3471,x3471),x3473),f4(f3(x3471,x3471),x3472)))),
% 70.83/71.00 inference(scs_inference,[],[16,153,3,2])).
% 70.83/71.00 cnf(354,plain,
% 70.83/71.00 (E(f4(f1(f1(x3541)),x3542),f3(f4(x3541,x3542),f3(a2,a2)))),
% 70.83/71.00 inference(scs_inference,[],[292,167,3])).
% 70.83/71.00 cnf(357,plain,
% 70.83/71.00 (E(f3(f4(x3571,x3572),f3(a2,a2)),f4(f1(f1(x3571)),x3572))),
% 70.83/71.00 inference(scs_inference,[],[292,167,3,2])).
% 70.83/71.00 cnf(360,plain,
% 70.83/71.00 (E(f4(f1(f3(f3(x3601,x3601),f3(x3601,x3601))),f1(x3602)),f3(f3(a2,a2),f4(f3(x3601,x3601),f3(x3602,x3602))))),
% 70.83/71.00 inference(scs_inference,[],[16,303,3,2])).
% 70.83/71.00 cnf(361,plain,
% 70.83/71.00 (E(f3(f3(a2,a2),f4(x3611,x3612)),f1(f4(f1(x3611),x3612)))),
% 70.83/71.00 inference(scs_inference,[],[16,290,3])).
% 70.83/71.00 cnf(363,plain,
% 70.83/71.00 (E(f1(f4(f1(x3631),x3632)),f3(f3(a2,a2),f4(x3631,x3632)))),
% 70.83/71.00 inference(scs_inference,[],[16,290,3,2])).
% 70.83/71.00 cnf(366,plain,
% 70.83/71.00 (E(f1(f4(f1(x3661),x3662)),f3(f3(a2,f4(x3661,x3662)),a2))),
% 70.83/71.00 inference(scs_inference,[],[16,227,3,2])).
% 70.83/71.00 cnf(370,plain,
% 70.83/71.00 (E(f1(f1(f3(f3(x3701,x3702),x3703))),f3(f3(x3702,x3703),x3701))),
% 70.83/71.00 inference(scs_inference,[],[16,176,3,2])).
% 70.83/71.00 cnf(384,plain,
% 70.83/71.00 (E(f3(f4(f1(x3841),f3(x3842,x3842)),a2),f3(a2,f4(f3(x3841,x3841),f1(x3842))))),
% 70.83/71.00 inference(scs_inference,[],[344,335,3])).
% 70.83/71.00 cnf(387,plain,
% 70.83/71.00 (E(f3(a2,f4(f3(x3871,x3871),f1(x3872))),f3(f4(f1(x3871),f3(x3872,x3872)),a2))),
% 70.83/71.00 inference(scs_inference,[],[344,335,3,2])).
% 70.83/71.00 cnf(391,plain,
% 70.83/71.00 (E(f3(a2,f4(f1(x3911),f3(x3912,x3912))),f3(f4(f3(x3911,x3911),f1(x3912)),a2))),
% 70.83/71.00 inference(scs_inference,[],[338,341,3,2])).
% 70.83/71.00 cnf(395,plain,
% 70.83/71.00 (E(f1(f1(f1(f4(x3951,x3952)))),f4(f1(f1(x3951)),f1(x3952)))),
% 70.83/71.00 inference(scs_inference,[],[17,71,3,2])).
% 70.83/71.00 cnf(396,plain,
% 70.83/71.00 (E(f1(f4(x3961,x3962)),f4(f1(f1(x3961)),f1(x3962)))),
% 70.83/71.00 inference(scs_inference,[],[395,172,3])).
% 70.83/71.00 cnf(398,plain,
% 70.83/71.00 (E(f4(f1(f1(x3981)),f1(x3982)),f1(f4(x3981,x3982)))),
% 70.83/71.00 inference(scs_inference,[],[395,172,3,2])).
% 70.83/71.00 cnf(399,plain,
% 70.83/71.00 (E(f4(f1(f1(f1(x3991))),f1(x3992)),f3(f3(a2,a2),f4(x3991,x3992)))),
% 70.83/71.00 inference(scs_inference,[],[363,398,3])).
% 70.83/71.00 cnf(403,plain,
% 70.83/71.00 (E(f4(f1(f1(f1(x4031))),f1(x4032)),f3(f3(a2,f4(x4031,x4032)),a2))),
% 70.83/71.00 inference(scs_inference,[],[366,398,3])).
% 70.83/71.00 cnf(406,plain,
% 70.83/71.00 (E(f3(f3(a2,f4(x4061,x4062)),a2),f4(f1(f1(f1(x4061))),f1(x4062)))),
% 70.83/71.00 inference(scs_inference,[],[366,398,3,2])).
% 70.83/71.00 cnf(407,plain,
% 70.83/71.00 (E(f1(a2),f4(f1(f1(x4071)),f1(a2)))),
% 70.83/71.00 inference(scs_inference,[],[395,108,3])).
% 70.83/71.00 cnf(409,plain,
% 70.83/71.00 (E(f4(f1(f1(x4091)),f1(a2)),f1(a2))),
% 70.83/71.00 inference(scs_inference,[],[395,108,3,2])).
% 70.83/71.00 cnf(413,plain,
% 70.83/71.00 (E(f1(f1(f4(x4131,x4132))),f4(f1(f1(f1(x4131))),f1(x4132)))),
% 70.83/71.00 inference(scs_inference,[],[187,398,3,2])).
% 70.83/71.00 cnf(414,plain,
% 70.83/71.00 (E(f4(x4141,x4142),f4(f1(f1(f1(x4141))),f1(x4142)))),
% 70.83/71.00 inference(scs_inference,[],[413,172,3])).
% 70.83/71.00 cnf(417,plain,
% 70.83/71.00 (E(f3(f4(f1(x4171),f3(x4172,x4173)),a2),f3(a2,f4(f1(x4171),f3(x4173,x4172))))),
% 70.83/71.00 inference(scs_inference,[],[211,335,3])).
% 70.83/71.00 cnf(419,plain,
% 70.83/71.00 (E(f3(a2,f4(f1(x4191),f3(x4192,x4193))),f3(f4(f1(x4191),f3(x4193,x4192)),a2))),
% 70.83/71.00 inference(scs_inference,[],[211,335,3,2])).
% 70.83/71.00 cnf(422,plain,
% 70.83/71.00 (E(f3(a2,f4(f3(x4221,x4222),f1(x4223))),f3(f4(f3(x4222,x4221),f1(x4223)),a2))),
% 70.83/71.00 inference(scs_inference,[],[214,341,3,2])).
% 70.83/71.00 cnf(427,plain,
% 70.83/71.00 (E(f4(f1(f1(f1(x4271))),f1(x4272)),f3(a2,f3(a2,f4(x4271,x4272))))),
% 70.83/71.00 inference(scs_inference,[],[229,398,3])).
% 70.83/71.00 cnf(431,plain,
% 70.83/71.00 (E(f4(x4311,f4(x4312,x4312)),f3(f4(f4(x4311,x4312),x4312),a2))),
% 70.83/71.00 inference(scs_inference,[],[30,317,3])).
% 70.83/71.00 cnf(434,plain,
% 70.83/71.00 (E(f4(f1(x4341),f1(f4(x4342,x4342))),f3(a2,f4(f4(x4341,x4342),x4342)))),
% 70.83/71.00 inference(scs_inference,[],[17,36,3])).
% 70.83/71.00 cnf(439,plain,
% 70.83/71.00 (E(f1(f1(f1(f4(x4391,a2)))),f4(f1(f1(x4392)),f1(a2)))),
% 70.83/71.00 inference(scs_inference,[],[409,108,3,2])).
% 70.83/71.00 cnf(444,plain,
% 70.83/71.00 (E(f1(f4(x4441,a2)),f4(f1(f1(x4442)),f1(a2)))),
% 70.83/71.00 inference(scs_inference,[],[439,172,3])).
% 70.83/71.00 cnf(446,plain,
% 70.83/71.00 (E(f4(f1(f1(x4461)),f1(a2)),f1(f4(x4462,a2)))),
% 70.83/71.00 inference(scs_inference,[],[439,172,3,2])).
% 70.83/71.00 cnf(447,plain,
% 70.83/71.00 (E(f4(f1(f1(x4471)),f1(a2)),f3(f3(a2,a2),f4(x4472,a2)))),
% 70.83/71.00 inference(scs_inference,[],[446,363,3])).
% 70.83/71.00 cnf(451,plain,
% 70.83/71.00 (E(f4(f1(f1(x4511)),f1(a2)),f3(a2,f3(f4(x4512,a2),a2)))),
% 70.83/71.00 inference(scs_inference,[],[446,232,3])).
% 70.83/71.00 cnf(455,plain,
% 70.83/71.00 (E(f4(f1(f1(x4551)),f1(a2)),f3(f3(a2,f4(x4552,a2)),a2))),
% 70.83/71.00 inference(scs_inference,[],[366,446,3])).
% 70.83/71.00 cnf(458,plain,
% 70.83/71.00 (E(f3(f3(a2,f4(x4581,a2)),a2),f4(f1(f1(x4582)),f1(a2)))),
% 70.83/71.00 inference(scs_inference,[],[366,446,3,2])).
% 70.83/71.00 cnf(459,plain,
% 70.83/71.00 (E(f1(f1(f3(f3(a2,a2),f4(x4591,a2)))),f4(f1(f1(x4592)),f1(a2)))),
% 70.83/71.00 inference(scs_inference,[],[370,458,3])).
% 70.83/71.00 cnf(462,plain,
% 70.83/71.00 (E(f4(f1(f1(x4621)),f1(a2)),f3(f4(x4622,a2),f3(a2,a2)))),
% 70.83/71.00 inference(scs_inference,[],[292,446,459,2,3])).
% 70.83/71.00 cnf(466,plain,
% 70.83/71.00 (E(f4(f1(f1(x4661)),f1(f3(x4662,x4663))),f3(f1(f4(x4661,x4662)),f1(f4(x4661,x4663))))),
% 70.83/71.00 inference(scs_inference,[],[17,113,462,2,3])).
% 70.83/71.00 cnf(468,plain,
% 70.83/71.00 (E(f3(f1(f4(x4681,x4682)),f1(f4(x4681,x4683))),f4(f1(f1(x4681)),f1(f3(x4682,x4683))))),
% 70.83/71.00 inference(scs_inference,[],[466,2])).
% 70.83/71.00 cnf(469,plain,
% 70.83/71.00 (E(f4(f1(f3(x4691,x4692)),f1(f1(x4693))),f3(f1(f4(x4691,x4693)),f1(f4(x4692,x4693))))),
% 70.83/71.00 inference(scs_inference,[],[17,116,466,2,3])).
% 70.83/71.00 cnf(471,plain,
% 70.83/71.00 (E(f3(f1(f4(x4711,x4712)),f1(f4(x4713,x4712))),f4(f1(f3(x4711,x4713)),f1(f1(x4712))))),
% 70.83/71.00 inference(scs_inference,[],[469,2])).
% 70.83/71.00 cnf(472,plain,
% 70.83/71.00 (E(f4(f1(f1(f1(x4721))),f1(x4722)),f3(f4(x4721,x4722),f3(a2,a2)))),
% 70.83/71.00 inference(scs_inference,[],[17,354,469,2,3])).
% 70.83/71.00 cnf(476,plain,
% 70.83/71.00 (E(f4(f1(x4761),f1(x4762)),f4(f1(f1(f1(x4761))),f1(x4762)))),
% 70.83/71.00 inference(scs_inference,[],[17,414,472,2,3])).
% 70.83/71.00 cnf(479,plain,
% 70.83/71.00 (E(f4(f1(f1(x4791)),f1(f1(x4792))),f4(f1(f1(f1(x4791))),f1(x4792)))),
% 70.83/71.00 inference(scs_inference,[],[17,476,2,3])).
% 70.83/71.00 cnf(482,plain,
% 70.83/71.00 (E(f4(f1(f1(f1(x4821))),f1(f1(a2))),f3(f3(a2,a2),f4(x4822,a2)))),
% 70.83/71.00 inference(scs_inference,[],[17,479,447,2,3])).
% 70.83/71.00 cnf(485,plain,
% 70.83/71.00 (E(f4(x4851,a2),f4(f1(f1(x4852)),f1(a2)))),
% 70.83/71.00 inference(scs_inference,[],[68,482,444,2,3])).
% 70.83/71.00 cnf(489,plain,
% 70.83/71.00 (E(f4(f1(f1(x4891)),f1(f3(x4892,x4892))),f3(f4(f3(x4891,x4891),f1(x4892)),a2))),
% 70.83/71.00 inference(scs_inference,[],[17,233,485,2,3])).
% 70.83/71.00 cnf(491,plain,
% 70.83/71.00 (E(f3(f4(f3(x4911,x4911),f1(x4912)),a2),f4(f1(f1(x4911)),f1(f3(x4912,x4912))))),
% 70.83/71.00 inference(scs_inference,[],[489,2])).
% 70.83/71.00 cnf(492,plain,
% 70.83/71.00 (E(f4(f1(f3(x4921,x4921)),f1(f1(x4922))),f3(f4(f1(x4921),f3(x4922,x4922)),a2))),
% 70.83/71.00 inference(scs_inference,[],[17,237,489,2,3])).
% 70.83/71.00 cnf(494,plain,
% 70.83/71.00 (E(f3(f4(f1(x4941),f3(x4942,x4942)),a2),f4(f1(f3(x4941,x4941)),f1(f1(x4942))))),
% 70.83/71.00 inference(scs_inference,[],[492,2])).
% 70.83/71.00 cnf(495,plain,
% 70.83/71.00 (E(f3(a2,f4(f1(x4951),f3(x4952,x4952))),f4(f1(f1(x4951)),f1(f3(x4952,x4952))))),
% 70.83/71.00 inference(scs_inference,[],[491,391,492,2,3])).
% 70.83/71.00 cnf(497,plain,
% 70.83/71.00 (E(f4(f1(f1(x4971)),f1(f3(x4972,x4972))),f3(a2,f4(f1(x4971),f3(x4972,x4972))))),
% 70.83/71.00 inference(scs_inference,[],[495,2])).
% 70.83/71.00 cnf(498,plain,
% 70.83/71.00 (E(f3(a2,f4(f3(x4981,x4981),f1(x4982))),f4(f1(f3(x4981,x4981)),f1(f1(x4982))))),
% 70.83/71.00 inference(scs_inference,[],[494,387,495,2,3])).
% 70.83/71.00 cnf(500,plain,
% 70.83/71.00 (E(f4(f1(f3(x5001,x5001)),f1(f1(x5002))),f3(a2,f4(f3(x5001,x5001),f1(x5002))))),
% 70.83/71.00 inference(scs_inference,[],[498,2])).
% 70.83/71.00 cnf(501,plain,
% 70.83/71.00 (E(f4(f1(f1(x5011)),f1(f3(x5012,x5012))),f3(f4(f1(x5011),f3(x5012,x5012)),a2))),
% 70.83/71.00 inference(scs_inference,[],[497,419,498,2,3])).
% 70.83/71.00 cnf(503,plain,
% 70.83/71.00 (E(f3(f4(f1(x5031),f3(x5032,x5032)),a2),f4(f1(f1(x5031)),f1(f3(x5032,x5032))))),
% 70.83/71.00 inference(scs_inference,[],[501,2])).
% 70.83/71.00 cnf(504,plain,
% 70.83/71.00 (E(f4(f1(f3(x5041,x5041)),f1(f1(x5042))),f3(f4(f3(x5041,x5041),f1(x5042)),a2))),
% 70.83/71.00 inference(scs_inference,[],[500,422,501,2,3])).
% 70.83/71.00 cnf(506,plain,
% 70.83/71.00 (E(f3(f4(f3(x5061,x5061),f1(x5062)),a2),f4(f1(f3(x5061,x5061)),f1(f1(x5062))))),
% 70.83/71.00 inference(scs_inference,[],[504,2])).
% 70.83/71.00 cnf(507,plain,
% 70.83/71.00 (E(f3(a2,f4(f3(x5071,x5071),f1(x5072))),f4(f1(f1(x5071)),f1(f3(x5072,x5072))))),
% 70.83/71.00 inference(scs_inference,[],[503,387,504,2,3])).
% 70.83/71.00 cnf(509,plain,
% 70.83/71.00 (E(f4(f1(f1(x5091)),f1(f3(x5092,x5092))),f3(a2,f4(f3(x5091,x5091),f1(x5092))))),
% 70.83/71.00 inference(scs_inference,[],[507,2])).
% 70.83/71.00 cnf(510,plain,
% 70.83/71.00 (E(f3(a2,f4(f1(x5101),f3(x5102,x5102))),f4(f1(f3(x5101,x5101)),f1(f1(x5102))))),
% 70.83/71.00 inference(scs_inference,[],[506,391,507,2,3])).
% 70.83/71.00 cnf(512,plain,
% 70.83/71.00 (E(f4(f1(f3(x5121,x5121)),f1(f1(x5122))),f3(a2,f4(f1(x5121),f3(x5122,x5122))))),
% 70.83/71.00 inference(scs_inference,[],[510,2])).
% 70.83/71.00 cnf(513,plain,
% 70.83/71.00 (E(f4(f1(f4(x5131,x5132)),f1(x5132)),f3(a2,f4(x5131,f4(x5132,x5132))))),
% 70.83/71.00 inference(scs_inference,[],[17,249,510,2,3])).
% 70.83/71.00 cnf(516,plain,
% 70.83/71.01 (E(f3(a2,f4(x5161,f4(x5162,x5162))),f4(f1(f4(x5161,x5162)),f1(x5162)))),
% 70.83/71.01 inference(scs_inference,[],[513,2])).
% 70.83/71.01 cnf(517,plain,
% 70.83/71.01 (E(f4(f1(x5171),f1(f4(x5172,x5172))),f3(f4(f4(x5171,x5172),x5172),a2))),
% 70.83/71.01 inference(scs_inference,[],[17,431,513,2,3])).
% 70.83/71.01 cnf(521,plain,
% 70.83/71.01 (E(f3(f1(f4(f1(x5211),f4(x5212,x5212))),a2),f4(f1(f4(x5211,x5212)),f1(x5212)))),
% 70.83/71.01 inference(scs_inference,[],[516,323,517,2,3])).
% 70.83/71.01 cnf(524,plain,
% 70.83/71.01 (E(f4(f1(f4(x5241,x5242)),f1(x5242)),f3(f1(f4(f1(x5241),f4(x5242,x5242))),a2))),
% 70.83/71.01 inference(scs_inference,[],[521,2])).
% 70.83/71.01 cnf(525,plain,
% 70.83/71.01 (E(f3(f4(f4(x5251,x5252),x5252),a2),f4(f1(f4(x5251,x5252)),f1(x5252)))),
% 70.83/71.01 inference(scs_inference,[],[320,516,521,2,3])).
% 70.83/71.01 cnf(527,plain,
% 70.83/71.01 (E(f4(f1(f4(x5271,x5272)),f1(x5272)),f3(f4(f4(x5271,x5272),x5272),a2))),
% 70.83/71.01 inference(scs_inference,[],[525,2])).
% 70.83/71.01 cnf(528,plain,
% 70.83/71.01 (E(f4(f1(f1(x5281)),f1(f1(x5282))),f3(f3(f4(x5281,x5282),a2),a2))),
% 70.83/71.01 inference(scs_inference,[],[17,525,272,2,3])).
% 70.83/71.01 cnf(530,plain,
% 70.83/71.01 (E(f3(f3(f4(x5301,x5302),a2),a2),f4(f1(f1(x5301)),f1(f1(x5302))))),
% 70.83/71.01 inference(scs_inference,[],[528,2])).
% 70.83/71.01 cnf(531,plain,
% 70.83/71.01 (E(f4(f1(f1(x5311)),f1(f1(x5312))),f3(a2,f3(f4(x5311,x5312),a2)))),
% 70.83/71.01 inference(scs_inference,[],[17,296,528,2,3])).
% 70.83/71.01 cnf(534,plain,
% 70.83/71.01 (E(f4(f1(f4(x5341,x5342)),f1(x5342)),f3(f4(x5341,f4(x5342,x5342)),a2))),
% 70.83/71.01 inference(scs_inference,[],[524,531,200,2,3])).
% 70.83/71.01 cnf(537,plain,
% 70.83/71.01 (E(f3(a2,f4(f1(x5371),f3(x5372,x5372))),f3(a2,f4(f3(x5371,x5371),f1(x5372))))),
% 70.83/71.01 inference(scs_inference,[],[419,534,384,2,3])).
% 70.83/71.01 cnf(540,plain,
% 70.83/71.01 (E(f3(a2,f4(f3(x5401,x5401),f1(x5402))),f3(a2,f4(f1(x5401),f3(x5402,x5402))))),
% 70.83/71.01 inference(scs_inference,[],[537,2])).
% 70.83/71.01 cnf(541,plain,
% 70.83/71.01 (E(f4(f1(x5411),f3(x5412,x5412)),f4(f1(f3(x5411,x5411)),f1(f1(x5412))))),
% 70.83/71.01 inference(scs_inference,[],[494,30,537,2,3])).
% 70.83/71.01 cnf(544,plain,
% 70.83/71.01 (E(f4(f1(f1(x5441)),f1(f3(x5442,x5442))),f4(f1(f3(x5441,x5441)),f1(f1(x5442))))),
% 70.83/71.01 inference(scs_inference,[],[17,541,2,3])).
% 70.83/71.01 cnf(546,plain,
% 70.83/71.01 (E(f4(f1(f3(x5461,x5461)),f1(f1(x5462))),f4(f1(f1(x5461)),f1(f3(x5462,x5462))))),
% 70.83/71.01 inference(scs_inference,[],[544,2])).
% 70.83/71.01 cnf(548,plain,
% 70.83/71.01 (E(f4(f1(f1(f1(x5481))),f1(f1(a2))),f3(f4(x5482,a2),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[17,462,3])).
% 70.83/71.01 cnf(555,plain,
% 70.83/71.01 (E(f3(f1(x5551),x5551),f4(f1(f1(x5552)),f1(a2)))),
% 70.83/71.01 inference(scs_inference,[],[92,407,3])).
% 70.83/71.01 cnf(559,plain,
% 70.83/71.01 (E(f4(f1(f1(x5591)),f1(f3(x5592,x5592))),f1(f4(f1(f3(x5591,x5591)),f1(x5592))))),
% 70.83/71.01 inference(scs_inference,[],[18,546,3,2])).
% 70.83/71.01 cnf(562,plain,
% 70.83/71.01 (E(f1(f4(f1(f3(x5621,x5621)),f1(x5622))),f1(f4(f1(f1(x5621)),f3(x5622,x5622))))),
% 70.83/71.01 inference(scs_inference,[],[18,559,3,2])).
% 70.83/71.01 cnf(563,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x5631)),f3(x5632,x5632))),f3(a2,f4(f3(x5631,x5631),f1(x5632))))),
% 70.83/71.01 inference(scs_inference,[],[18,509,3])).
% 70.83/71.01 cnf(565,plain,
% 70.83/71.01 (E(f3(a2,f4(f3(x5651,x5651),f1(x5652))),f1(f4(f1(f1(x5651)),f3(x5652,x5652))))),
% 70.83/71.01 inference(scs_inference,[],[18,509,3,2])).
% 70.83/71.01 cnf(568,plain,
% 70.83/71.01 (E(f3(a2,f4(f1(x5681),f3(x5682,x5682))),f1(f4(f1(f3(x5681,x5681)),f1(x5682))))),
% 70.83/71.01 inference(scs_inference,[],[18,512,3,2])).
% 70.83/71.01 cnf(571,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x5711)),f3(x5712,x5712))),f4(f1(f3(x5711,x5711)),f1(f1(x5712))))),
% 70.83/71.01 inference(scs_inference,[],[565,500,3,2])).
% 70.83/71.01 cnf(572,plain,
% 70.83/71.01 (E(f1(f4(f1(f3(x5721,x5721)),f1(x5722))),f3(f3(a2,a2),f4(f1(x5721),f3(x5722,x5722))))),
% 70.83/71.01 inference(scs_inference,[],[562,363,3])).
% 70.83/71.01 cnf(574,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x5741),f3(x5742,x5742))),f1(f4(f1(f3(x5741,x5741)),f1(x5742))))),
% 70.83/71.01 inference(scs_inference,[],[562,363,3,2])).
% 70.83/71.01 cnf(575,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x5751),f3(x5752,x5752))),f3(a2,f4(f3(x5751,x5751),f1(x5752))))),
% 70.83/71.01 inference(scs_inference,[],[574,223,3])).
% 70.83/71.01 cnf(577,plain,
% 70.83/71.01 (E(f3(a2,f4(f3(x5771,x5771),f1(x5772))),f3(f3(a2,a2),f4(f1(x5771),f3(x5772,x5772))))),
% 70.83/71.01 inference(scs_inference,[],[574,223,3,2])).
% 70.83/71.01 cnf(580,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x5801),f3(x5802,x5802))),f4(f1(f1(x5801)),f1(f3(x5802,x5802))))),
% 70.83/71.01 inference(scs_inference,[],[577,509,3,2])).
% 70.83/71.01 cnf(584,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x5841)),f3(x5842,x5842))),f3(f1(f4(x5841,x5842)),f1(f4(x5841,x5842))))),
% 70.83/71.01 inference(scs_inference,[],[565,344,3,2])).
% 70.83/71.01 cnf(587,plain,
% 70.83/71.01 (E(f3(f1(f4(x5871,x5872)),f1(f4(x5871,x5872))),f1(f4(f1(f3(x5871,x5871)),f1(x5872))))),
% 70.83/71.01 inference(scs_inference,[],[584,562,3,2])).
% 70.83/71.01 cnf(590,plain,
% 70.83/71.01 (E(f3(f4(f3(x5901,x5901),f1(x5902)),a2),f1(f4(f1(f1(x5901)),f3(x5902,x5902))))),
% 70.83/71.01 inference(scs_inference,[],[584,193,3,2])).
% 70.83/71.01 cnf(593,plain,
% 70.83/71.01 (E(f3(f4(f3(x5931,x5931),f1(x5932)),f3(a2,a2)),f3(f1(f4(x5931,x5932)),f1(f4(x5931,x5932))))),
% 70.83/71.01 inference(scs_inference,[],[587,292,3,2])).
% 70.83/71.01 cnf(596,plain,
% 70.83/71.01 (E(f4(f1(f1(x5961)),f1(f3(x5962,x5962))),f3(f4(f3(x5961,x5961),f1(x5962)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[593,468,3,2])).
% 70.83/71.01 cnf(599,plain,
% 70.83/71.01 (E(f3(f4(f3(x5991,x5991),f1(x5992)),f3(a2,a2)),f1(f4(f1(f1(x5991)),f3(x5992,x5992))))),
% 70.83/71.01 inference(scs_inference,[],[18,596,3,2])).
% 70.83/71.01 cnf(602,plain,
% 70.83/71.01 (E(f4(f1(f3(x6021,x6021)),f1(f1(x6022))),f3(f4(f3(x6021,x6021),f1(x6022)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[571,599,3,2])).
% 70.83/71.01 cnf(605,plain,
% 70.83/71.01 (E(f3(a2,f4(f1(x6051),f3(x6052,x6052))),f3(f4(f3(x6051,x6051),f1(x6052)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[593,338,3,2])).
% 70.83/71.01 cnf(608,plain,
% 70.83/71.01 (E(f3(f4(f3(x6081,x6081),f1(x6082)),f3(a2,a2)),f3(a2,f4(f3(x6081,x6081),f1(x6082))))),
% 70.83/71.01 inference(scs_inference,[],[605,540,3,2])).
% 70.83/71.01 cnf(611,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x6111),f3(x6112,x6112))),f3(f4(f3(x6111,x6111),f1(x6112)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[608,577,3,2])).
% 70.83/71.01 cnf(614,plain,
% 70.83/71.01 (E(f3(f4(f1(x6141),f3(x6142,x6142)),a2),f3(f4(f3(x6141,x6141),f1(x6142)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[608,387,3,2])).
% 70.83/71.01 cnf(617,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x6171,x6171),f1(x6172))),f3(a2,f4(f1(x6171),f3(x6172,x6172))))),
% 70.83/71.01 inference(scs_inference,[],[568,363,3,2])).
% 70.83/71.01 cnf(620,plain,
% 70.83/71.01 (E(f3(f4(f3(x6201,x6201),f1(x6202)),a2),f3(f3(a2,a2),f4(f3(x6201,x6201),f1(x6202))))),
% 70.83/71.01 inference(scs_inference,[],[617,391,3,2])).
% 70.83/71.01 cnf(624,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x6241,x6241),f1(x6242))),f3(a2,f4(f3(x6241,x6241),f1(x6242))))),
% 70.83/71.01 inference(scs_inference,[],[620,422,3,2])).
% 70.83/71.01 cnf(627,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x6271)),f3(x6272,x6272))),f3(f3(a2,a2),f4(f3(x6271,x6271),f1(x6272))))),
% 70.83/71.01 inference(scs_inference,[],[624,565,3,2])).
% 70.83/71.01 cnf(630,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x6301),f3(x6302,x6302))),f3(f3(a2,a2),f4(f3(x6301,x6301),f1(x6302))))),
% 70.83/71.01 inference(scs_inference,[],[624,577,3,2])).
% 70.83/71.01 cnf(631,plain,
% 70.83/71.01 (E(f3(f4(f3(x6311,x6311),f1(x6312)),a2),f3(f4(f1(x6311),f3(x6312,x6312)),a2))),
% 70.83/71.01 inference(scs_inference,[],[590,199,3])).
% 70.83/71.01 cnf(633,plain,
% 70.83/71.01 (E(f3(f4(f1(x6331),f3(x6332,x6332)),a2),f3(f4(f3(x6331,x6331),f1(x6332)),a2))),
% 70.83/71.01 inference(scs_inference,[],[590,199,3,2])).
% 70.83/71.01 cnf(636,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x6361,x6361),f1(x6362))),f3(f4(f1(x6361),f3(x6362,x6362)),a2))),
% 70.83/71.01 inference(scs_inference,[],[633,620,3,2])).
% 70.83/71.01 cnf(645,plain,
% 70.83/71.01 (E(f3(f1(f4(x6451,x6452)),f1(f4(x6451,x6452))),f3(f3(a2,a2),f4(f3(x6451,x6451),f1(x6452))))),
% 70.83/71.01 inference(scs_inference,[],[636,335,3,2])).
% 70.83/71.01 cnf(649,plain,
% 70.83/71.01 (E(f3(f1(f4(x6491,x6492)),f1(f4(x6493,x6492))),f1(f4(f3(x6491,x6493),x6492)))),
% 70.83/71.01 inference(scs_inference,[],[18,116,3,2])).
% 70.83/71.01 cnf(650,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x6501)),f3(x6502,x6502))),f1(f4(f3(x6501,x6501),x6502)))),
% 70.83/71.01 inference(scs_inference,[],[649,584,3])).
% 70.83/71.01 cnf(652,plain,
% 70.83/71.01 (E(f1(f4(f3(x6521,x6521),x6522)),f1(f4(f1(f1(x6521)),f3(x6522,x6522))))),
% 70.83/71.01 inference(scs_inference,[],[649,584,3,2])).
% 70.83/71.01 cnf(655,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x6551,x6551),f1(x6552))),f1(f4(f3(x6551,x6551),x6552)))),
% 70.83/71.01 inference(scs_inference,[],[627,652,3,2])).
% 70.83/71.01 cnf(658,plain,
% 70.83/71.01 (E(f1(f4(f3(x6581,x6581),x6582)),f3(f4(f3(x6581,x6581),f1(x6582)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[649,593,3,2])).
% 70.83/71.01 cnf(659,plain,
% 70.83/71.01 (E(f1(f4(x6591,x6592)),f1(f4(f1(x6591),f1(x6592))))),
% 70.83/71.01 inference(scs_inference,[],[18,68,3])).
% 70.83/71.01 cnf(661,plain,
% 70.83/71.01 (E(f1(f4(f1(x6611),f1(x6612))),f1(f4(x6611,x6612)))),
% 70.83/71.01 inference(scs_inference,[],[18,68,3,2])).
% 70.83/71.01 cnf(662,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x6621)),f1(x6622))),f1(f1(f4(x6621,x6622))))),
% 70.83/71.01 inference(scs_inference,[],[661,187,3])).
% 70.83/71.01 cnf(665,plain,
% 70.83/71.01 (E(f1(f1(f4(x6651,x6652))),f1(f4(f1(f1(x6651)),f1(x6652))))),
% 70.83/71.01 inference(scs_inference,[],[661,187,3,2])).
% 70.83/71.01 cnf(666,plain,
% 70.83/71.01 (E(f1(f1(f4(x6661,x6662))),f3(a2,f4(f1(x6661),f1(x6662))))),
% 70.83/71.01 inference(scs_inference,[],[665,223,3])).
% 70.83/71.01 cnf(668,plain,
% 70.83/71.01 (E(f3(a2,f4(f1(x6681),f1(x6682))),f1(f1(f4(x6681,x6682))))),
% 70.83/71.01 inference(scs_inference,[],[665,223,3,2])).
% 70.83/71.01 cnf(672,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x6721)),f1(x6722))),f3(f3(f4(x6721,x6722),a2),a2))),
% 70.83/71.01 inference(scs_inference,[],[661,205,3])).
% 70.83/71.01 cnf(675,plain,
% 70.83/71.01 (E(f3(f3(f4(x6751,x6752),a2),a2),f1(f4(f1(f1(x6751)),f1(x6752))))),
% 70.83/71.01 inference(scs_inference,[],[661,205,3,2])).
% 70.83/71.01 cnf(676,plain,
% 70.83/71.01 (E(f3(f3(f4(x6761,x6762),a2),a2),f3(f4(f1(x6761),f1(x6762)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[675,292,3])).
% 70.83/71.01 cnf(678,plain,
% 70.83/71.01 (E(f3(f4(f1(x6781),f1(x6782)),f3(a2,a2)),f3(f3(f4(x6781,x6782),a2),a2))),
% 70.83/71.01 inference(scs_inference,[],[675,292,3,2])).
% 70.83/71.01 cnf(681,plain,
% 70.83/71.01 (E(f4(f1(f1(x6811)),f1(f1(x6812))),f3(f4(f1(x6811),f1(x6812)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[530,678,3,2])).
% 70.83/71.01 cnf(688,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x6881,x6881),f1(x6882))),f4(f1(f1(f3(x6881,x6881))),f1(x6882)))),
% 70.83/71.01 inference(scs_inference,[],[655,396,3])).
% 70.83/71.01 cnf(693,plain,
% 70.83/71.01 (E(f4(f1(f1(f3(x6931,x6931))),f1(x6932)),f3(f1(f4(x6931,x6932)),f1(f4(x6931,x6932))))),
% 70.83/71.01 inference(scs_inference,[],[645,688,3,2])).
% 70.83/71.01 cnf(699,plain,
% 70.83/71.01 (E(f1(f4(f3(x6991,x6991),x6992)),f3(f3(a2,a2),f4(f1(x6991),f3(x6992,x6992))))),
% 70.83/71.01 inference(scs_inference,[],[630,655,3,2])).
% 70.83/71.01 cnf(702,plain,
% 70.83/71.01 (E(f4(f1(f1(x7021)),f1(f3(x7022,x7022))),f1(f4(f3(x7021,x7021),x7022)))),
% 70.83/71.01 inference(scs_inference,[],[580,699,3,2])).
% 70.83/71.01 cnf(705,plain,
% 70.83/71.01 (E(f4(f1(f1(x7051)),f1(f3(x7052,x7052))),f4(f1(f1(f3(x7051,x7051))),f1(x7052)))),
% 70.83/71.01 inference(scs_inference,[],[693,468,3,2])).
% 70.83/71.01 cnf(708,plain,
% 70.83/71.01 (E(f4(f1(f1(f3(x7081,x7081))),f1(x7082)),f1(f4(f1(f1(x7081)),f3(x7082,x7082))))),
% 70.83/71.01 inference(scs_inference,[],[18,705,3,2])).
% 70.83/71.01 cnf(709,plain,
% 70.83/71.01 (E(f4(f1(f1(f3(x7091,x7091))),f1(x7092)),f3(f4(f1(x7091),f3(x7092,x7092)),a2))),
% 70.83/71.01 inference(scs_inference,[],[693,190,3])).
% 70.83/71.01 cnf(711,plain,
% 70.83/71.01 (E(f3(f4(f1(x7111),f3(x7112,x7112)),a2),f4(f1(f1(f3(x7111,x7111))),f1(x7112)))),
% 70.83/71.01 inference(scs_inference,[],[693,190,3,2])).
% 70.83/71.01 cnf(718,plain,
% 70.83/71.01 (E(f3(f4(f3(x7181,x7181),f1(x7182)),f3(a2,a2)),f3(f4(f1(x7181),f3(x7182,x7182)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[614,75,3,2])).
% 70.83/71.01 cnf(719,plain,
% 70.83/71.01 (E(f4(f1(f3(x7191,x7191)),f1(f1(x7192))),f3(f4(f1(x7191),f3(x7192,x7192)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[602,718,3])).
% 70.83/71.01 cnf(722,plain,
% 70.83/71.01 (E(f4(f1(x7221),f3(x7222,x7222)),f3(f4(f3(x7221,x7221),f1(x7222)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[614,30,3])).
% 70.83/71.01 cnf(728,plain,
% 70.83/71.01 (E(f1(f4(f3(x7281,x7281),x7282)),f3(f4(f1(x7281),f3(x7282,x7282)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[658,718,3])).
% 70.83/71.01 cnf(730,plain,
% 70.83/71.01 (E(f3(f4(f1(x7301),f3(x7302,x7302)),f3(a2,a2)),f1(f4(f3(x7301,x7301),x7302)))),
% 70.83/71.01 inference(scs_inference,[],[658,718,3,2])).
% 70.83/71.01 cnf(737,plain,
% 70.83/71.01 (E(f1(f4(f1(f3(x7371,x7371)),f1(x7372))),f3(f4(f1(x7371),f3(x7372,x7372)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,719,3])).
% 70.83/71.01 cnf(743,plain,
% 70.83/71.01 (E(f4(f1(f1(x7431)),f1(f3(x7432,x7432))),f3(f4(f1(x7431),f3(x7432,x7432)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[702,728,3])).
% 70.83/71.01 cnf(746,plain,
% 70.83/71.01 (E(f3(f1(f4(x7461,x7462)),f1(f4(x7461,x7462))),f3(f4(f1(x7461),f3(x7462,x7462)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[587,737,3])).
% 70.83/71.01 cnf(748,plain,
% 70.83/71.01 (E(f3(f4(f1(x7481),f3(x7482,x7482)),f3(a2,a2)),f3(f1(f4(x7481,x7482)),f1(f4(x7481,x7482))))),
% 70.83/71.01 inference(scs_inference,[],[587,737,3,2])).
% 70.83/71.01 cnf(751,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x7511,x7511),f1(x7512))),f3(f4(f1(x7511),f3(x7512,x7512)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[748,645,3,2])).
% 70.83/71.01 cnf(757,plain,
% 70.83/71.01 (E(f3(a2,f4(f3(x7571,x7571),f1(x7572))),f3(f4(f1(x7571),f3(x7572,x7572)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[748,214,3,2])).
% 70.83/71.01 cnf(760,plain,
% 70.83/71.01 (E(f1(f4(f1(x7601),x7602)),f3(a2,f4(f1(x7601),f1(x7602))))),
% 70.83/71.01 inference(scs_inference,[],[668,185,3,2])).
% 70.83/71.01 cnf(761,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(f1(x7611))),f1(a2))),f3(f4(x7612,a2),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,548,3])).
% 70.83/71.01 cnf(763,plain,
% 70.83/71.01 (E(f3(f4(x7631,a2),f3(a2,a2)),f1(f4(f1(f1(f1(x7632))),f1(a2))))),
% 70.83/71.01 inference(scs_inference,[],[761,2])).
% 70.83/71.01 cnf(764,plain,
% 70.83/71.01 (E(f1(f1(f4(f1(x7641),a2))),f3(f4(x7642,a2),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[665,761,2,3])).
% 70.83/71.01 cnf(766,plain,
% 70.83/71.01 (E(f3(f4(x7661,a2),f3(a2,a2)),f1(f1(f4(f1(x7662),a2))))),
% 70.83/71.01 inference(scs_inference,[],[764,2])).
% 70.83/71.01 cnf(767,plain,
% 70.83/71.01 (E(f3(f4(x7671,a2),f3(a2,a2)),f3(f3(a2,f4(f1(f1(x7672)),f1(a2))),a2))),
% 70.83/71.01 inference(scs_inference,[],[763,366,764,2,3])).
% 70.83/71.01 cnf(769,plain,
% 70.83/71.01 (E(f3(f3(a2,f4(f1(f1(x7691)),f1(a2))),a2),f3(f4(x7692,a2),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[767,2])).
% 70.83/71.01 cnf(770,plain,
% 70.83/71.01 (E(f1(f4(f3(x7701,x7701),x7702)),f3(a2,f4(f1(x7701),f3(x7702,x7702))))),
% 70.83/71.01 inference(scs_inference,[],[18,245,767,2,3])).
% 70.83/71.01 cnf(774,plain,
% 70.83/71.01 (E(f1(f4(f1(x7741),f4(x7742,x7742))),f3(a2,f4(f4(x7741,x7742),x7742)))),
% 70.83/71.01 inference(scs_inference,[],[18,434,770,2,3])).
% 70.83/71.01 cnf(776,plain,
% 70.83/71.01 (E(f3(a2,f4(f4(x7761,x7762),x7762)),f1(f4(f1(x7761),f4(x7762,x7762))))),
% 70.83/71.01 inference(scs_inference,[],[774,2])).
% 70.83/71.01 cnf(777,plain,
% 70.83/71.01 (E(f3(f4(x7771,a2),f3(a2,a2)),f3(a2,f4(f1(f1(x7772)),f1(a2))))),
% 70.83/71.01 inference(scs_inference,[],[766,774,666,2,3])).
% 70.83/71.01 cnf(780,plain,
% 70.83/71.01 (E(f3(a2,f4(f4(x7801,x7802),x7802)),f3(f4(x7801,f4(x7802,x7802)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[776,292,777,2,3])).
% 70.83/71.01 cnf(782,plain,
% 70.83/71.01 (E(f3(f4(x7821,f4(x7822,x7822)),f3(a2,a2)),f3(a2,f4(f4(x7821,x7822),x7822)))),
% 70.83/71.01 inference(scs_inference,[],[780,2])).
% 70.83/71.01 cnf(783,plain,
% 70.83/71.01 (E(f3(f4(x7831,a2),f3(a2,a2)),f3(f3(f4(f1(x7832),a2),a2),a2))),
% 70.83/71.01 inference(scs_inference,[],[763,780,672,2,3])).
% 70.83/71.01 cnf(785,plain,
% 70.83/71.01 (E(f3(f3(f4(f1(x7851),a2),a2),a2),f3(f4(x7852,a2),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[783,2])).
% 70.83/71.01 cnf(786,plain,
% 70.83/71.01 (E(f3(f4(x7861,f4(x7862,x7862)),f3(a2,a2)),f3(a2,f4(x7861,f4(x7862,x7862))))),
% 70.83/71.01 inference(scs_inference,[],[782,220,783,2,3])).
% 70.83/71.01 cnf(788,plain,
% 70.83/71.01 (E(f3(a2,f4(x7881,f4(x7882,x7882))),f3(f4(x7881,f4(x7882,x7882)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[786,2])).
% 70.83/71.01 cnf(789,plain,
% 70.83/71.01 (E(f3(f3(f4(x7891,x7892),a2),a2),f1(f1(f4(x7891,x7892))))),
% 70.83/71.01 inference(scs_inference,[],[675,662,786,2,3])).
% 70.83/71.01 cnf(791,plain,
% 70.83/71.01 (E(f1(f1(f4(x7911,x7912))),f3(f3(f4(x7911,x7912),a2),a2))),
% 70.83/71.01 inference(scs_inference,[],[789,2])).
% 70.83/71.01 cnf(792,plain,
% 70.83/71.01 (E(f3(f4(x7921,f4(f4(x7922,x7922),f4(x7922,x7922))),f3(a2,a2)),f3(f4(f4(x7921,f4(x7922,x7922)),f4(x7922,x7922)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[788,782,789,2,3])).
% 70.83/71.01 cnf(796,plain,
% 70.83/71.01 (E(f3(f1(f4(f1(x7961),f4(x7962,x7962))),a2),f3(f4(x7961,f4(x7962,x7962)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[788,323,792,2,3])).
% 70.83/71.01 cnf(799,plain,
% 70.83/71.01 (E(f3(f4(x7991,f4(x7992,x7992)),f3(a2,a2)),f3(f1(f4(f1(x7991),f4(x7992,x7992))),a2))),
% 70.83/71.01 inference(scs_inference,[],[796,2])).
% 70.83/71.01 cnf(800,plain,
% 70.83/71.01 (E(f4(f3(x8001,x8001),f1(x8002)),f3(f4(f1(x8001),f3(x8002,x8002)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[757,33,796,2,3])).
% 70.83/71.01 cnf(803,plain,
% 70.83/71.01 (E(f1(f1(f4(x8031,x8032))),f4(f1(f1(x8031)),f1(f1(x8032))))),
% 70.83/71.01 inference(scs_inference,[],[791,530,800,2,3])).
% 70.83/71.01 cnf(805,plain,
% 70.83/71.01 (E(f4(f1(f1(x8051)),f1(f1(x8052))),f1(f1(f4(x8051,x8052))))),
% 70.83/71.01 inference(scs_inference,[],[803,2])).
% 70.83/71.01 cnf(806,plain,
% 70.83/71.01 (E(f3(f4(f4(x8061,x8062),x8062),a2),f3(f4(x8061,f4(x8062,x8062)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[320,788,803,2,3])).
% 70.83/71.01 cnf(808,plain,
% 70.83/71.01 (E(f3(f4(x8081,f4(x8082,x8082)),f3(a2,a2)),f3(f4(f4(x8081,x8082),x8082),a2))),
% 70.83/71.01 inference(scs_inference,[],[806,2])).
% 70.83/71.01 cnf(809,plain,
% 70.83/71.01 (E(f4(f1(f3(x8091,x8091)),f1(f1(x8092))),f3(f3(a2,a2),f4(f1(x8091),f3(x8092,x8092))))),
% 70.83/71.01 inference(scs_inference,[],[500,577,806,2,3])).
% 70.83/71.01 cnf(812,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x8121)),x8122)),f3(f4(x8121,f1(x8122)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,809,354,2,3])).
% 70.83/71.01 cnf(815,plain,
% 70.83/71.01 (E(f3(f4(x8151,f1(x8152)),f3(a2,a2)),f1(f4(f1(f1(x8151)),x8152)))),
% 70.83/71.01 inference(scs_inference,[],[812,2])).
% 70.83/71.01 cnf(816,plain,
% 70.83/71.01 (E(f3(f4(f3(x8161,x8161),f1(x8162)),f3(a2,a2)),f3(f4(x8161,f1(f3(x8162,x8162))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[599,812,2,3])).
% 70.83/71.01 cnf(818,plain,
% 70.83/71.01 (E(f3(f4(x8181,f1(f3(x8182,x8182))),f3(a2,a2)),f3(f4(f3(x8181,x8181),f1(x8182)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[816,2])).
% 70.83/71.01 cnf(819,plain,
% 70.83/71.01 (E(f3(f4(x8191,f1(x8192)),f3(a2,a2)),f3(a2,f4(f1(f1(x8191)),f1(x8192))))),
% 70.83/71.01 inference(scs_inference,[],[815,760,816,2,3])).
% 70.83/71.01 cnf(822,plain,
% 70.83/71.01 (E(f1(f4(f3(x8221,x8221),x8222)),f4(f1(f3(x8221,x8221)),f1(f1(x8222))))),
% 70.83/71.01 inference(scs_inference,[],[571,652,819,2,3])).
% 70.83/71.01 cnf(825,plain,
% 70.83/71.01 (E(f3(f4(x8251,f1(f3(x8252,x8252))),f3(a2,a2)),f3(f4(f1(x8251),f3(x8252,x8252)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[818,718,822,2,3])).
% 70.83/71.01 cnf(827,plain,
% 70.83/71.01 (E(f3(f4(f1(x8271),f3(x8272,x8272)),f3(a2,a2)),f3(f4(x8271,f1(f3(x8272,x8272))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[825,2])).
% 70.83/71.01 cnf(828,plain,
% 70.83/71.01 (E(f4(f1(f1(f3(x8281,x8281))),f1(x8282)),f3(a2,f4(f3(x8281,x8281),f1(x8282))))),
% 70.83/71.01 inference(scs_inference,[],[708,825,563,2,3])).
% 70.83/71.01 cnf(831,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x8311,x8311),f1(x8312))),f3(f4(x8311,f1(f3(x8312,x8312))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[751,827,828,2,3])).
% 70.83/71.01 cnf(834,plain,
% 70.83/71.01 (E(f3(f4(x8341,f1(f3(x8342,x8342))),f3(a2,a2)),f4(f1(f3(x8341,x8341)),f1(f1(x8342))))),
% 70.83/71.01 inference(scs_inference,[],[815,571,831,2,3])).
% 70.83/71.01 cnf(837,plain,
% 70.83/71.01 (E(f4(f1(f3(x8371,x8371)),f1(f1(x8372))),f3(f4(x8371,f1(f3(x8372,x8372))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[834,2])).
% 70.83/71.01 cnf(838,plain,
% 70.83/71.01 (E(f3(f4(f3(x8381,x8381),f1(x8382)),a2),f1(f4(f3(x8381,x8381),x8382)))),
% 70.83/71.01 inference(scs_inference,[],[590,650,834,2,3])).
% 70.83/71.01 cnf(840,plain,
% 70.83/71.01 (E(f1(f4(f3(x8401,x8401),x8402)),f3(f4(f3(x8401,x8401),f1(x8402)),a2))),
% 70.83/71.01 inference(scs_inference,[],[838,2])).
% 70.83/71.01 cnf(841,plain,
% 70.83/71.01 (E(f1(f4(f1(f3(x8411,x8411)),f1(x8412))),f3(f4(x8411,f1(f3(x8412,x8412))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,837,838,2,3])).
% 70.83/71.01 cnf(843,plain,
% 70.83/71.01 (E(f3(f4(x8431,f1(f3(x8432,x8432))),f3(a2,a2)),f1(f4(f1(f3(x8431,x8431)),f1(x8432))))),
% 70.83/71.01 inference(scs_inference,[],[841,2])).
% 70.83/71.01 cnf(844,plain,
% 70.83/71.01 (E(f3(f4(f1(x8441),f3(x8442,x8442)),f3(a2,a2)),f3(f4(f3(x8441,x8441),f1(x8442)),a2))),
% 70.83/71.01 inference(scs_inference,[],[730,840,841,2,3])).
% 70.83/71.01 cnf(847,plain,
% 70.83/71.01 (E(f3(f4(x8471,f1(f3(x8472,x8472))),f3(a2,a2)),f3(f4(f3(x8471,x8471),f1(x8472)),a2))),
% 70.83/71.01 inference(scs_inference,[],[843,199,844,2,3])).
% 70.83/71.01 cnf(849,plain,
% 70.83/71.01 (E(f3(f4(f3(x8491,x8491),f1(x8492)),a2),f3(f4(x8491,f1(f3(x8492,x8492))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[847,2])).
% 70.83/71.01 cnf(850,plain,
% 70.83/71.01 (E(f1(f4(f3(x8501,x8501),x8502)),f3(f4(f1(x8501),f3(x8502,x8502)),a2))),
% 70.83/71.01 inference(scs_inference,[],[840,847,631,2,3])).
% 70.83/71.01 cnf(853,plain,
% 70.83/71.01 (E(f3(f4(f1(x8531),f3(x8532,x8532)),a2),f3(f4(x8531,f1(f3(x8532,x8532))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[849,633,850,2,3])).
% 70.83/71.01 cnf(855,plain,
% 70.83/71.01 (E(f3(f4(x8551,f1(f3(x8552,x8552))),f3(a2,a2)),f3(f4(f1(x8551),f3(x8552,x8552)),a2))),
% 70.83/71.01 inference(scs_inference,[],[853,2])).
% 70.83/71.01 cnf(856,plain,
% 70.83/71.01 (E(f1(f4(f3(x8561,x8561),x8562)),f3(f4(x8561,f1(f3(x8562,x8562))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[849,840,853,2,3])).
% 70.83/71.01 cnf(859,plain,
% 70.83/71.01 (E(f3(f4(x8591,f1(f3(x8592,x8592))),f3(a2,a2)),f4(f1(f1(f3(x8591,x8591))),f1(x8592)))),
% 70.83/71.01 inference(scs_inference,[],[855,711,856,2,3])).
% 70.83/71.01 cnf(862,plain,
% 70.83/71.01 (E(f3(f4(x8621,f1(f3(x8622,x8622))),f3(a2,a2)),f3(f1(f4(x8621,x8622)),f1(f4(x8621,x8622))))),
% 70.83/71.01 inference(scs_inference,[],[855,335,859,2,3])).
% 70.83/71.01 cnf(864,plain,
% 70.83/71.01 (E(f3(f1(f4(x8641,x8642)),f1(f4(x8641,x8642))),f3(f4(x8641,f1(f3(x8642,x8642))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[862,2])).
% 70.83/71.01 cnf(865,plain,
% 70.83/71.01 (E(f3(f4(x8651,f1(f3(x8652,x8652))),f3(a2,a2)),f3(a2,f4(f1(x8651),f3(x8652,x8652))))),
% 70.83/71.01 inference(scs_inference,[],[855,862,417,2,3])).
% 70.83/71.01 cnf(868,plain,
% 70.83/71.01 (E(f1(f4(x8681,x8682)),f4(f1(f1(f1(x8681))),f1(f1(x8682))))),
% 70.83/71.01 inference(scs_inference,[],[18,865,414,2,3])).
% 70.83/71.01 cnf(870,plain,
% 70.83/71.01 (E(f4(f1(f1(f1(x8701))),f1(f1(x8702))),f1(f4(x8701,x8702)))),
% 70.83/71.01 inference(scs_inference,[],[868,2])).
% 70.83/71.01 cnf(871,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x8711)),f3(x8712,x8713))),f3(f1(f4(x8711,x8712)),f1(f4(x8711,x8713))))),
% 70.83/71.01 inference(scs_inference,[],[18,868,466,2,3])).
% 70.83/71.01 cnf(873,plain,
% 70.83/71.01 (E(f3(f1(f4(x8731,x8732)),f1(f4(x8731,x8733))),f1(f4(f1(f1(x8731)),f3(x8732,x8733))))),
% 70.83/71.01 inference(scs_inference,[],[871,2])).
% 70.83/71.01 cnf(874,plain,
% 70.83/71.01 (E(f4(f1(f1(f3(x8741,x8741))),f1(x8742)),f3(f4(f1(x8741),f3(x8742,x8742)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[693,746,871,2,3])).
% 70.83/71.01 cnf(877,plain,
% 70.83/71.01 (E(f1(f4(f1(f3(x8771,x8772)),f1(x8773))),f3(f1(f4(x8771,x8773)),f1(f4(x8772,x8773))))),
% 70.83/71.01 inference(scs_inference,[],[18,874,469,2,3])).
% 70.83/71.01 cnf(879,plain,
% 70.83/71.01 (E(f3(f1(f4(x8791,x8792)),f1(f4(x8793,x8792))),f1(f4(f1(f3(x8791,x8793)),f1(x8792))))),
% 70.83/71.01 inference(scs_inference,[],[877,2])).
% 70.83/71.01 cnf(880,plain,
% 70.83/71.01 (E(f4(f1(f1(x8801)),f1(f1(x8802))),f1(f4(f1(x8801),x8802)))),
% 70.83/71.01 inference(scs_inference,[],[805,877,185,2,3])).
% 70.83/71.01 cnf(882,plain,
% 70.83/71.01 (E(f1(f4(f1(x8821),x8822)),f4(f1(f1(x8821)),f1(f1(x8822))))),
% 70.83/71.01 inference(scs_inference,[],[880,2])).
% 70.83/71.01 cnf(883,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(f1(x8831))),f1(a2))),f3(f3(a2,a2),f4(x8832,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,880,482,2,3])).
% 70.83/71.01 cnf(885,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(x8851,a2)),f1(f4(f1(f1(f1(x8852))),f1(a2))))),
% 70.83/71.01 inference(scs_inference,[],[883,2])).
% 70.83/71.01 cnf(886,plain,
% 70.83/71.01 (E(f1(f4(f1(f1(x8861)),a2)),f3(f3(a2,a2),f4(x8862,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,883,447,2,3])).
% 70.83/71.01 cnf(889,plain,
% 70.83/71.01 (E(f3(f4(x8891,f4(x8892,x8892)),f3(a2,a2)),f4(f1(f4(x8891,x8892)),f1(x8892)))),
% 70.83/71.01 inference(scs_inference,[],[799,886,521,2,3])).
% 70.83/71.01 cnf(891,plain,
% 70.83/71.01 (E(f4(f1(f4(x8911,x8912)),f1(x8912)),f3(f4(x8911,f4(x8912,x8912)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[889,2])).
% 70.83/71.01 cnf(892,plain,
% 70.83/71.01 (E(f4(f1(f1(f1(x8921))),f1(f1(a2))),f4(f1(f1(x8922)),f1(a2)))),
% 70.83/71.01 inference(scs_inference,[],[870,889,444,2,3])).
% 70.83/71.01 cnf(896,plain,
% 70.83/71.01 (E(f1(f4(f1(f4(x8961,x8962)),x8962)),f3(f4(x8961,f4(x8962,x8962)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[18,891,892,2,3])).
% 70.83/71.01 cnf(899,plain,
% 70.83/71.01 (E(f3(f4(x8991,f4(x8992,x8992)),f3(a2,a2)),f1(f4(f1(f4(x8991,x8992)),x8992)))),
% 70.83/71.01 inference(scs_inference,[],[896,2])).
% 70.83/71.01 cnf(900,plain,
% 70.83/71.01 (E(f3(f1(f4(x9001,x9002)),f1(f4(x9001,x9003))),f3(f3(a2,a2),f4(f1(x9001),f3(x9002,x9003))))),
% 70.83/71.01 inference(scs_inference,[],[873,363,896,2,3])).
% 70.83/71.01 cnf(902,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x9021),f3(x9022,x9023))),f3(f1(f4(x9021,x9022)),f1(f4(x9021,x9023))))),
% 70.83/71.01 inference(scs_inference,[],[900,2])).
% 70.83/71.01 cnf(903,plain,
% 70.83/71.01 (E(f3(f1(f4(x9031,x9032)),f1(f4(x9033,x9032))),f3(f4(f3(x9031,x9033),f1(x9032)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[879,292,900,2,3])).
% 70.83/71.01 cnf(905,plain,
% 70.83/71.01 (E(f3(f4(f3(x9051,x9052),f1(x9053)),f3(a2,a2)),f3(f1(f4(x9051,x9053)),f1(f4(x9052,x9053))))),
% 70.83/71.01 inference(scs_inference,[],[903,2])).
% 70.83/71.01 cnf(906,plain,
% 70.83/71.01 (E(f1(f4(f3(f3(x9061,x9061),f3(x9061,x9061)),f1(x9062))),f4(f1(f1(f3(x9061,x9061))),f3(x9062,x9062)))),
% 70.83/71.01 inference(scs_inference,[],[19,302,903,2,3])).
% 70.83/71.01 cnf(908,plain,
% 70.83/71.01 (E(f4(f1(f1(f3(x9081,x9081))),f3(x9082,x9082)),f1(f4(f3(f3(x9081,x9081),f3(x9081,x9081)),f1(x9082))))),
% 70.83/71.01 inference(scs_inference,[],[906,2])).
% 70.83/71.01 cnf(909,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f1(x9091),f3(x9092,x9092))),f3(f4(x9091,f1(f3(x9092,x9092))),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[864,902,906,2,3])).
% 70.83/71.01 cnf(912,plain,
% 70.83/71.01 (E(f3(f4(x9121,f1(f3(x9122,x9122))),f3(a2,a2)),f3(f3(a2,a2),f4(f1(x9121),f3(x9122,x9122))))),
% 70.83/71.01 inference(scs_inference,[],[909,2])).
% 70.83/71.01 cnf(913,plain,
% 70.83/71.01 (E(f1(f4(f1(x9131),f1(f1(x9132)))),f3(f4(f1(x9131),f1(x9132)),f3(a2,a2)))),
% 70.83/71.01 inference(scs_inference,[],[19,681,909,2,3])).
% 70.83/71.01 cnf(915,plain,
% 70.83/71.01 (E(f3(f4(f1(x9151),f1(x9152)),f3(a2,a2)),f1(f4(f1(x9151),f1(f1(x9152)))))),
% 70.83/71.01 inference(scs_inference,[],[913,2])).
% 70.83/71.01 cnf(916,plain,
% 70.83/71.01 (E(f1(f4(f3(f3(x9161,x9161),f3(x9161,x9161)),f1(x9162))),f3(f3(a2,a2),f4(f3(x9161,x9161),f3(x9162,x9162))))),
% 70.83/71.01 inference(scs_inference,[],[19,360,913,2,3])).
% 70.83/71.01 cnf(918,plain,
% 70.83/71.01 (E(f3(f3(a2,a2),f4(f3(x9181,x9181),f3(x9182,x9182))),f1(f4(f3(f3(x9181,x9181),f3(x9181,x9181)),f1(x9182))))),
% 70.83/71.01 inference(scs_inference,[],[916,2])).
% 70.83/71.01 cnf(919,plain,
% 70.83/71.01 (E(f1(f4(f1(f3(x9191,x9191)),f3(x9192,x9192))),f1(f4(f3(f3(x9191,x9191),f3(x9191,x9191)),f1(x9192))))),
% 70.83/71.01 inference(scs_inference,[],[19,908,916,2,3])).
% 70.83/71.01 cnf(921,plain,
% 70.83/71.01 (E(f1(f4(f3(f3(x9211,x9211),f3(x9211,x9211)),f1(x9212))),f1(f4(f1(f3(x9211,x9211)),f3(x9212,x9212))))),
% 70.83/71.01 inference(scs_inference,[],[919,2])).
% 70.83/71.01 cnf(922,plain,
% 70.83/71.01 (E(f3(f4(x9221,f4(x9222,x9222)),f3(a2,a2)),f4(f1(f1(f4(x9221,x9222))),f1(f1(x9222))))),
% 70.97/71.01 inference(scs_inference,[],[882,899,919,2,3])).
% 70.97/71.01 cnf(925,plain,
% 70.97/71.01 (E(f1(f4(f3(f3(x9251,x9251),f3(x9251,x9251)),f1(x9252))),f3(a2,f4(f3(x9251,x9251),f3(x9252,x9252))))),
% 70.97/71.01 inference(scs_inference,[],[19,258,922,2,3])).
% 70.97/71.01 cnf(928,plain,
% 70.97/71.01 (E(f1(f4(f3(f3(x9281,x9281),f3(x9281,x9281)),f1(x9282))),f3(f4(f3(x9281,x9281),f3(x9282,x9282)),a2))),
% 70.97/71.01 inference(scs_inference,[],[19,286,925,2,3])).
% 70.97/71.01 cnf(931,plain,
% 70.97/71.01 (E(f1(f4(f4(x9311,x9312),f1(x9312))),f3(f4(f4(x9311,x9312),x9312),a2))),
% 70.97/71.01 inference(scs_inference,[],[19,527,928,2,3])).
% 70.97/71.01 cnf(933,plain,
% 70.97/71.01 (E(f3(f4(f4(x9331,x9332),x9332),a2),f1(f4(f4(x9331,x9332),f1(x9332))))),
% 70.97/71.01 inference(scs_inference,[],[931,2])).
% 70.97/71.01 cnf(934,plain,
% 70.97/71.01 (E(f1(f4(f1(x9341),f1(f3(x9342,x9342)))),f3(f4(f3(x9341,x9341),f1(x9342)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,596,931,2,3])).
% 70.97/71.01 cnf(936,plain,
% 70.97/71.01 (E(f3(f4(f3(x9361,x9361),f1(x9362)),f3(a2,a2)),f1(f4(f1(x9361),f1(f3(x9362,x9362)))))),
% 70.97/71.01 inference(scs_inference,[],[934,2])).
% 70.97/71.01 cnf(937,plain,
% 70.97/71.01 (E(f3(f4(x9371,f4(x9372,x9372)),f3(a2,a2)),f1(f4(f4(x9371,x9372),f1(x9372))))),
% 70.97/71.01 inference(scs_inference,[],[808,933,934,2,3])).
% 70.97/71.01 cnf(939,plain,
% 70.97/71.01 (E(f1(f4(f4(x9391,x9392),f1(x9392))),f3(f4(x9391,f4(x9392,x9392)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[937,2])).
% 70.97/71.01 cnf(940,plain,
% 70.97/71.01 (E(f1(f4(f3(x9401,x9401),f1(f1(x9402)))),f3(f4(f3(x9401,x9401),f1(x9402)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,602,937,2,3])).
% 70.97/71.01 cnf(943,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(f3(x9431,x9431),f3(x9432,x9432))),f3(f4(f3(f3(x9431,x9431),f3(x9431,x9431)),f1(f1(x9432))),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[918,658,940,2,3])).
% 70.97/71.01 cnf(946,plain,
% 70.97/71.01 (E(f1(f4(f3(f3(x9461,x9461),f3(x9461,x9461)),f1(x9462))),f4(f1(f3(x9461,x9461)),f1(f3(x9462,x9462))))),
% 70.97/71.01 inference(scs_inference,[],[19,261,943,2,3])).
% 70.97/71.01 cnf(949,plain,
% 70.97/71.01 (E(f1(f4(f3(f3(x9491,x9491),f3(x9491,x9491)),f1(x9492))),f3(f4(f3(x9491,x9491),x9492),f4(f3(x9491,x9491),x9492)))),
% 70.97/71.01 inference(scs_inference,[],[921,347,946,2,3])).
% 70.97/71.01 cnf(952,plain,
% 70.97/71.01 (E(f3(f4(f3(x9521,x9522),f1(x9523)),f3(a2,a2)),f4(f1(f3(x9521,x9522)),f1(f1(x9523))))),
% 70.97/71.01 inference(scs_inference,[],[905,471,949,2,3])).
% 70.97/71.01 cnf(954,plain,
% 70.97/71.01 (E(f4(f1(f3(x9541,x9542)),f1(f1(x9543))),f3(f4(f3(x9541,x9542),f1(x9543)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[952,2])).
% 70.97/71.01 cnf(955,plain,
% 70.97/71.01 (E(f1(f4(f3(f3(x9551,x9551),f3(x9551,x9551)),f1(x9552))),f3(f4(f3(x9551,x9551),f3(x9552,x9552)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,306,952,2,3])).
% 70.97/71.01 cnf(958,plain,
% 70.97/71.01 (E(f1(f4(f3(x9581,x9582),f1(f1(x9583)))),f3(f4(f3(x9581,x9582),f1(x9583)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,954,955,2,3])).
% 70.97/71.01 cnf(961,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(f1(x9611),f3(x9612,x9613))),f4(f1(f1(x9611)),f1(f3(x9612,x9613))))),
% 70.97/71.01 inference(scs_inference,[],[902,468,958,2,3])).
% 70.97/71.01 cnf(964,plain,
% 70.97/71.01 (E(f3(f4(f3(x9641,x9642),f1(x9643)),f3(a2,a2)),f1(f4(f3(x9641,x9642),x9643)))),
% 70.97/71.01 inference(scs_inference,[],[905,649,961,2,3])).
% 70.97/71.01 cnf(967,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(f1(x9671),f3(x9672,x9673))),f3(a2,f4(f1(x9671),f3(x9673,x9672))))),
% 70.97/71.01 inference(scs_inference,[],[902,338,964,2,3])).
% 70.97/71.01 cnf(970,plain,
% 70.97/71.01 (E(f3(f4(f3(x9701,x9702),f1(x9703)),f3(a2,a2)),f3(a2,f4(f3(x9702,x9701),f1(x9703))))),
% 70.97/71.01 inference(scs_inference,[],[905,344,967,2,3])).
% 70.97/71.01 cnf(973,plain,
% 70.97/71.01 (E(f3(f4(f3(x9731,x9731),f1(x9732)),f3(a2,a2)),f3(a2,f4(x9731,f1(f3(x9732,x9732)))))),
% 70.97/71.01 inference(scs_inference,[],[936,223,970,2,3])).
% 70.97/71.01 cnf(976,plain,
% 70.97/71.01 (E(f1(f4(x9761,f3(x9762,x9763))),f3(f1(f4(x9761,x9762)),f1(f4(x9761,x9763))))),
% 70.97/71.01 inference(scs_inference,[],[19,113,973,2,3])).
% 70.97/71.01 cnf(980,plain,
% 70.97/71.01 (E(f3(f4(f1(x9801),f1(x9802)),f3(a2,a2)),f3(f4(x9801,f1(f1(x9802))),a2))),
% 70.97/71.01 inference(scs_inference,[],[915,199,976,2,3])).
% 70.97/71.01 cnf(983,plain,
% 70.97/71.01 (E(f1(f4(x9831,x9832)),f1(f4(f1(f1(x9831)),x9832)))),
% 70.97/71.01 inference(scs_inference,[],[19,68,980,2,3])).
% 70.97/71.01 cnf(985,plain,
% 70.97/71.01 (E(f1(f4(f1(f1(x9851)),x9852)),f1(f4(x9851,x9852)))),
% 70.97/71.01 inference(scs_inference,[],[983,2])).
% 70.97/71.01 cnf(986,plain,
% 70.97/71.01 (E(f1(f4(x9861,f3(x9862,x9862))),f3(f4(f3(x9861,x9861),f1(x9862)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,722,983,2,3])).
% 70.97/71.01 cnf(989,plain,
% 70.97/71.01 (E(f3(f4(f3(x9891,x9891),f1(x9892)),f3(a2,a2)),f1(f4(x9891,f3(x9892,x9892))))),
% 70.97/71.01 inference(scs_inference,[],[986,2])).
% 70.97/71.01 cnf(990,plain,
% 70.97/71.01 (E(f1(f4(f1(f1(f4(x9901,x9902))),f1(x9902))),f3(f4(x9901,f4(x9902,x9902)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[939,985,986,2,3])).
% 70.97/71.01 cnf(992,plain,
% 70.97/71.01 (E(f3(f4(x9921,f4(x9922,x9922)),f3(a2,a2)),f1(f4(f1(f1(f4(x9921,x9922))),f1(x9922))))),
% 70.97/71.01 inference(scs_inference,[],[990,2])).
% 70.97/71.01 cnf(993,plain,
% 70.97/71.01 (E(f3(f4(f3(f1(x9931),f1(x9931)),f1(x9932)),f3(a2,a2)),f3(a2,f4(x9931,f3(x9932,x9932))))),
% 70.97/71.01 inference(scs_inference,[],[989,223,990,2,3])).
% 70.97/71.01 cnf(997,plain,
% 70.97/71.01 (E(f3(f4(x9971,f4(x9972,x9972)),f3(a2,a2)),f3(f3(a2,a2),f4(f1(f4(x9971,x9972)),f1(x9972))))),
% 70.97/71.01 inference(scs_inference,[],[992,363,993,2,3])).
% 70.97/71.01 cnf(1000,plain,
% 70.97/71.01 (E(f1(f4(f1(x10001),f1(f3(x10002,x10002)))),f3(f4(f1(x10001),f3(x10002,x10002)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,743,997,2,3])).
% 70.97/71.01 cnf(1002,plain,
% 70.97/71.01 (E(f3(f4(f1(x10021),f3(x10022,x10022)),f3(a2,a2)),f1(f4(f1(x10021),f1(f3(x10022,x10022)))))),
% 70.97/71.01 inference(scs_inference,[],[1000,2])).
% 70.97/71.01 cnf(1003,plain,
% 70.97/71.01 (E(f1(f4(f1(f1(x10031)),f1(x10032))),f3(f3(a2,a2),f4(x10031,x10032)))),
% 70.97/71.01 inference(scs_inference,[],[19,1000,399,2,3])).
% 70.97/71.01 cnf(1005,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(x10051,x10052)),f1(f4(f1(f1(x10051)),f1(x10052))))),
% 70.97/71.01 inference(scs_inference,[],[1003,2])).
% 70.97/71.01 cnf(1006,plain,
% 70.97/71.01 (E(f3(f4(f1(f1(x10061)),f3(x10062,x10062)),f3(a2,a2)),f3(f3(a2,a2),f4(x10061,f3(x10062,x10062))))),
% 70.97/71.01 inference(scs_inference,[],[1002,1003,2,3])).
% 70.97/71.01 cnf(1009,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(x10091,f3(x10092,x10092))),f3(f4(f1(f1(x10091)),f3(x10092,x10092)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[1006,2])).
% 70.97/71.01 cnf(1010,plain,
% 70.97/71.01 (E(f1(f4(x10101,f3(x10102,x10102))),f3(a2,f4(f3(x10101,x10101),f1(x10102))))),
% 70.97/71.01 inference(scs_inference,[],[19,1006,241,2,3])).
% 70.97/71.01 cnf(1014,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(x10141,f3(x10142,x10142))),f3(f4(f1(x10141),f1(f3(x10142,x10142))),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[1009,827,1010,2,3])).
% 70.97/71.01 cnf(1016,plain,
% 70.97/71.01 (E(f3(f4(f1(x10161),f1(f3(x10162,x10162))),f3(a2,a2)),f3(f3(a2,a2),f4(x10161,f3(x10162,x10162))))),
% 70.97/71.01 inference(scs_inference,[],[1014,2])).
% 70.97/71.01 cnf(1017,plain,
% 70.97/71.01 (E(f3(f4(x10171,f1(f3(x10172,x10172))),f3(a2,a2)),f3(a2,f4(f3(x10171,x10171),f1(x10172))))),
% 70.97/71.01 inference(scs_inference,[],[912,1014,575,2,3])).
% 70.97/71.01 cnf(1020,plain,
% 70.97/71.01 (E(f3(f4(f1(f1(x10201)),f1(f3(x10202,x10202))),f3(a2,a2)),f3(f4(f3(x10201,x10201),f1(x10202)),f3(a2,a2)))),
% 70.97/71.01 inference(scs_inference,[],[1016,611,1017,2,3])).
% 70.97/71.01 cnf(1024,plain,
% 70.97/71.01 (E(f1(f4(f1(f3(x10241,x10241)),f1(x10242))),f3(f4(f1(x10241),f3(x10242,x10242)),a2))),
% 70.97/71.01 inference(scs_inference,[],[19,1020,709,2,3])).
% 70.97/71.01 cnf(1026,plain,
% 70.97/71.01 (E(f3(f4(f1(x10261),f3(x10262,x10262)),a2),f1(f4(f1(f3(x10261,x10261)),f1(x10262))))),
% 70.97/71.01 inference(scs_inference,[],[1024,2])).
% 70.97/71.01 cnf(1027,plain,
% 70.97/71.01 (E(f1(f4(f1(f1(x10271)),f1(x10272))),f3(f3(a2,f4(x10271,x10272)),a2))),
% 70.97/71.01 inference(scs_inference,[],[19,1024,403,2,3])).
% 70.97/71.01 cnf(1029,plain,
% 70.97/71.01 (E(f3(f3(a2,f4(x10291,x10292)),a2),f1(f4(f1(f1(x10291)),f1(x10292))))),
% 70.97/71.01 inference(scs_inference,[],[1027,2])).
% 70.97/71.01 cnf(1030,plain,
% 70.97/71.01 (E(f3(f4(f1(x10301),f3(x10302,x10302)),a2),f3(f3(a2,a2),f4(f1(x10301),f3(x10302,x10302))))),
% 70.97/71.01 inference(scs_inference,[],[1026,572,1027,2,3])).
% 70.97/71.01 cnf(1032,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(f1(x10321),f3(x10322,x10322))),f3(f4(f1(x10321),f3(x10322,x10322)),a2))),
% 70.97/71.01 inference(scs_inference,[],[1030,2])).
% 70.97/71.01 cnf(1033,plain,
% 70.97/71.01 (E(f1(f4(f1(f1(x10331)),f1(x10332))),f3(a2,f3(a2,f4(x10331,x10332))))),
% 70.97/71.01 inference(scs_inference,[],[19,1030,427,2,3])).
% 70.97/71.01 cnf(1035,plain,
% 70.97/71.01 (E(f3(a2,f3(a2,f4(x10351,x10352))),f1(f4(f1(f1(x10351)),f1(x10352))))),
% 70.97/71.01 inference(scs_inference,[],[1033,2])).
% 70.97/71.01 cnf(1036,plain,
% 70.97/71.01 (E(f3(f3(a2,a2),f4(f1(x10361),f3(x10362,x10362))),f3(f4(f3(x10361,x10361),f1(x10362)),a2))),
% 70.97/71.01 inference(scs_inference,[],[1032,633,1033,2,3])).
% 70.97/71.01 cnf(1039,plain,
% 70.97/71.01 (E(f1(f4(f1(x10391),f1(a2))),f3(a2,f3(f4(x10392,a2),a2)))),
% 70.97/71.01 inference(scs_inference,[],[19,1036,451,2,3])).
% 70.97/71.01 cnf(1041,plain,
% 70.97/71.01 (E(f3(a2,f3(f4(x10411,a2),a2)),f1(f4(f1(x10412),f1(a2))))),
% 70.97/71.01 inference(scs_inference,[],[1039,2])).
% 70.97/71.01 cnf(1042,plain,
% 70.97/71.02 (E(f3(f3(a2,a2),f4(x10421,a2)),f3(a2,f3(f4(x10422,a2),a2)))),
% 70.97/71.02 inference(scs_inference,[],[1005,1039,2,3])).
% 70.97/71.02 cnf(1046,plain,
% 70.97/71.02 (E(f3(a2,f3(f4(x10461,a2),a2)),f1(f4(f1(f1(x10462)),f3(a2,a2))))),
% 70.97/71.02 inference(scs_inference,[],[1041,562,1042,2,3])).
% 70.97/71.02 cnf(1050,plain,
% 70.97/71.02 (E(f1(f4(f1(x10501),f1(a2))),f3(f3(a2,f4(x10502,a2)),a2))),
% 70.97/71.02 inference(scs_inference,[],[19,1046,455,2,3])).
% 70.97/71.02 cnf(1052,plain,
% 70.97/71.02 (E(f3(f3(a2,f4(x10521,a2)),a2),f1(f4(f1(x10522),f1(a2))))),
% 70.97/71.02 inference(scs_inference,[],[1050,2])).
% 70.97/71.02 cnf(1053,plain,
% 70.97/71.02 (E(f3(f3(a2,a2),f4(x10531,a2)),f3(f3(a2,f4(x10532,a2)),a2))),
% 70.97/71.02 inference(scs_inference,[],[885,1050,2,3])).
% 70.97/71.02 cnf(1055,plain,
% 70.97/71.02 (E(f3(f3(a2,f4(x10551,a2)),a2),f3(f3(a2,a2),f4(x10552,a2)))),
% 70.97/71.02 inference(scs_inference,[],[1053,2])).
% 70.97/71.02 cnf(1056,plain,
% 70.97/71.02 (E(f3(f3(a2,f4(x10561,a2)),a2),f1(f4(f1(f1(x10562)),f3(a2,a2))))),
% 70.97/71.02 inference(scs_inference,[],[1052,562,1053,2,3])).
% 70.97/71.02 cnf(1059,plain,
% 70.97/71.02 (E(f1(f4(f1(f1(x10591)),f3(a2,a2))),f3(f3(a2,f4(x10592,a2)),a2))),
% 70.97/71.02 inference(scs_inference,[],[1056,2])).
% 70.97/71.02 cnf(1060,plain,
% 70.97/71.02 (E(f1(f1(f3(f3(a2,a2),f4(x10601,a2)))),f3(f3(a2,a2),f4(x10602,a2)))),
% 70.97/71.02 inference(scs_inference,[],[1055,370,1056,2,3])).
% 70.97/71.02 cnf(1063,plain,
% 70.97/71.02 (E(f1(f4(f1(f1(x10631)),f3(a2,a2))),f4(f1(f1(f1(x10632))),f1(a2)))),
% 70.97/71.02 inference(scs_inference,[],[406,1059,1060,2,3])).
% 70.97/71.02 cnf(1066,plain,
% 70.97/71.02 (E(f1(f4(f1(f1(x10661)),f3(a2,a2))),f1(f4(f1(f1(x10662)),f1(a2))))),
% 70.97/71.02 inference(scs_inference,[],[1029,1059,1063,2,3])).
% 70.97/71.02 cnf(1068,plain,
% 70.97/71.02 (E(f1(f4(f1(f1(x10681)),f1(a2))),f1(f4(f1(f1(x10682)),f3(a2,a2))))),
% 70.97/71.02 inference(scs_inference,[],[1066,2])).
% 70.97/71.02 cnf(1069,plain,
% 70.97/71.02 (E(f3(a2,f3(f4(f1(f1(x10691)),f1(a2)),a2)),f3(f4(x10692,a2),f3(a2,a2)))),
% 70.97/71.02 inference(scs_inference,[],[769,169,1066,2,3])).
% 70.97/71.02 cnf(1072,plain,
% 70.97/71.02 (E(f3(a2,f3(a2,f4(x10721,a2))),f1(f4(f1(f1(x10722)),f3(a2,a2))))),
% 70.97/71.02 inference(scs_inference,[],[1068,1035,1069,2,3])).
% 70.97/71.02 cnf(1076,plain,
% 70.97/71.02 (E(f3(f4(f1(f1(x10761)),f1(a2)),f3(a2,a2)),f3(f4(x10762,a2),f3(a2,a2)))),
% 70.97/71.02 inference(scs_inference,[],[785,678,1072,2,3])).
% 70.97/71.02 cnf(1079,plain,
% 70.97/71.02 (E(f1(f1(f4(x10791,x10792))),f3(f4(f1(x10791),f1(x10792)),f3(a2,a2)))),
% 70.97/71.02 inference(scs_inference,[],[791,1076,676,2,3])).
% 70.97/71.02 cnf(1081,plain,
% 70.97/71.02 (E(f3(f4(f1(x10811),f1(x10812)),f3(a2,a2)),f1(f1(f4(x10811,x10812))))),
% 70.97/71.02 inference(scs_inference,[],[1079,2])).
% 70.97/71.02 cnf(1172,plain,
% 70.97/71.02 (E(f1(f4(f1(f1(x11721)),f1(f1(a2)))),f3(f3(a2,a2),f4(x11722,a2)))),
% 70.97/71.02 inference(scs_inference,[],[19,482,3])).
% 70.97/71.02 cnf(1175,plain,
% 70.97/71.02 (E(f1(f4(f1(x11751),f1(a2))),f3(f3(a2,a2),f4(x11752,a2)))),
% 70.97/71.02 inference(scs_inference,[],[19,1172,447,2,3])).
% 70.97/71.02 cnf(1177,plain,
% 70.97/71.02 (E(f3(f3(a2,a2),f4(x11771,a2)),f1(f4(f1(x11772),f1(a2))))),
% 70.97/71.02 inference(scs_inference,[],[1175,2])).
% 70.97/71.02 cnf(1178,plain,
% 70.97/71.02 (E(f1(f4(f1(x11781),f1(a2))),f3(f4(x11782,a2),f3(a2,a2)))),
% 70.97/71.02 inference(scs_inference,[],[19,1175,462,2,3])).
% 70.97/71.02 cnf(1181,plain,
% 70.97/71.02 (E(f4(f1(f1(x11811)),f1(f1(x11812))),f3(a2,f4(f1(x11811),f1(x11812))))),
% 70.97/71.02 inference(scs_inference,[],[805,1178,666,2,3])).
% 70.97/71.02 cnf(1184,plain,
% 70.97/71.02 (E(f3(f4(f1(x11841),f1(x11842)),f3(a2,a2)),f1(f4(f1(x11841),x11842)))),
% 70.97/71.02 inference(scs_inference,[],[1081,1181,185,2,3])).
% 70.97/71.02 cnf(1186,plain,
% 70.97/71.02 (E(f1(f4(f1(x11861),x11862)),f3(f4(f1(x11861),f1(x11862)),f3(a2,a2)))),
% 70.97/71.02 inference(scs_inference,[],[1184,2])).
% 70.97/71.02 cnf(1217,plain,
% 70.97/71.02 (E(f3(a2,x12171),f3(f4(x12172,a2),x12171))),
% 70.97/71.02 inference(scs_inference,[],[184,4,5])).
% 70.97/71.02 cnf(1218,plain,
% 70.97/71.02 (E(f3(x12181,a2),f3(x12181,f4(x12182,a2)))),
% 70.97/71.02 inference(scs_inference,[],[184,4,5,6])).
% 70.97/71.02 cnf(1219,plain,
% 70.97/71.02 (E(f4(a2,x12191),f4(f4(x12192,a2),x12191))),
% 70.97/71.02 inference(scs_inference,[],[184,4,5,6,7])).
% 70.97/71.02 cnf(1220,plain,
% 70.97/71.02 (E(f4(x12201,a2),f4(x12201,f4(x12202,a2)))),
% 70.97/71.02 inference(scs_inference,[],[184,4,5,6,7,8])).
% 70.97/71.02 cnf(1224,plain,
% 70.97/71.02 (E(f4(x12241,f3(a2,x12242)),f4(x12241,f3(f4(x12243,a2),x12242)))),
% 70.97/71.02 inference(scs_inference,[],[1217,8])).
% 70.97/71.02 cnf(1226,plain,
% 70.97/71.02 (E(f3(f3(a2,x12261),x12262),f3(f3(f4(x12263,a2),x12261),x12262))),
% 70.97/71.02 inference(scs_inference,[],[1217,8,4,5])).
% 70.97/71.02 cnf(1230,plain,
% 70.97/71.02 (E(f3(a2,a2),f3(f4(x12301,a2),f4(x12302,a2)))),
% 70.97/71.02 inference(scs_inference,[],[1217,1218,114,8,4,5,6,7,2,3])).
% 70.97/71.02 cnf(1237,plain,
% 70.97/71.02 (E(f3(x12371,f3(a2,a2)),f3(x12371,f3(f4(x12372,a2),f4(x12373,a2))))),
% 70.97/71.02 inference(scs_inference,[],[1230,8,4,7,5,6])).
% 70.97/71.02 cnf(1242,plain,
% 70.97/71.02 (E(f3(x12421,f4(a2,x12422)),f3(x12421,f4(f4(x12423,a2),x12422)))),
% 70.97/71.02 inference(scs_inference,[],[1219,8,4,6])).
% 70.97/71.02 cnf(1244,plain,
% 70.97/71.02 (E(f3(f4(a2,x12441),x12442),f3(f4(f4(x12443,a2),x12441),x12442))),
% 70.97/71.02 inference(scs_inference,[],[1219,8,4,6,7,5])).
% 70.97/71.02 cnf(1250,plain,
% 70.97/71.02 (E(f3(f4(x12501,a2),x12502),f3(f4(x12501,f4(x12503,a2)),x12502))),
% 70.97/71.02 inference(scs_inference,[],[1220,8,4,5])).
% 70.97/71.02 cnf(1251,plain,
% 70.97/71.02 (E(f3(x12511,f4(x12512,a2)),f3(x12511,f4(x12512,f4(x12513,a2))))),
% 70.97/71.02 inference(scs_inference,[],[1220,8,4,5,6])).
% 70.97/71.02 cnf(1286,plain,
% 70.97/71.02 (~E(f3(f4(a2,x12861),f4(a2,x12862)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[555,168,8,4,5,6,7,2])).
% 70.97/71.02 cnf(1407,plain,
% 70.97/71.02 (~E(f3(a2,a2),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[275,31,8,4,5,6,7,2])).
% 70.97/71.02 cnf(1424,plain,
% 70.97/71.02 (~E(f3(f3(a2,a2),a2),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[357,136,8,4,5,6,7,2])).
% 70.97/71.02 cnf(1425,plain,
% 70.97/71.02 (~E(f3(a2,f4(x14251,a2)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[357,1407,1218,136,8,4,5,6,7,2,3])).
% 70.97/71.02 cnf(1432,plain,
% 70.97/71.02 (~E(f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))),f3(a2,f4(x14321,a2)))),
% 70.97/71.02 inference(scs_inference,[],[361,1425,8,5,4,6,7,2])).
% 70.97/71.02 cnf(1438,plain,
% 70.97/71.02 (E(f3(x14381,f1(f4(x14382,x14383))),f3(x14381,f1(f4(f1(x14382),f1(x14383)))))),
% 70.97/71.02 inference(scs_inference,[],[659,8,4,5,6])).
% 70.97/71.02 cnf(1440,plain,
% 70.97/71.02 (~E(f3(a2,f3(a2,a2)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[659,82,8,4,5,6,7,2])).
% 70.97/71.02 cnf(1441,plain,
% 70.97/71.02 (~E(f3(f4(f4(a5,a6),a6),f3(f1(f4(a5,f4(a6,a6))),a2)),f3(a2,f4(x14411,a2)))),
% 70.97/71.02 inference(scs_inference,[],[659,1432,82,72,8,4,5,6,7,2,3])).
% 70.97/71.02 cnf(1449,plain,
% 70.97/71.02 (~E(f3(f3(f4(x14491,a2),a2),a2),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[1224,1226,1424,1441,8,5,4,6,7,2,3])).
% 70.97/71.02 cnf(1457,plain,
% 70.97/71.02 (~E(f3(f4(f4(a5,a6),a6),f1(f4(f1(a5),f1(f4(a6,a6))))),a2)),
% 70.97/71.02 inference(scs_inference,[],[29,1242,1438,1449,8,4,5,6,7,2,3])).
% 70.97/71.02 cnf(1465,plain,
% 70.97/71.02 (~E(f3(f4(f4(x14651,a2),x14652),f4(a2,x14653)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[1244,1286,1457,8,5,4,6,7,2,3])).
% 70.97/71.02 cnf(1473,plain,
% 70.97/71.02 (~E(f3(a2,f3(f4(x14731,a2),f4(x14732,a2))),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[1250,1440,1465,1237,8,4,5,6,7,2,3])).
% 70.97/71.02 cnf(1481,plain,
% 70.97/71.02 (E(f3(f3(a2,a2),f4(x14811,a2)),f3(f4(f1(x14812),f1(f1(a2))),f3(a2,a2)))),
% 70.97/71.02 inference(scs_inference,[],[1251,1177,1186,1473,8,5,4,6,7,2,3])).
% 70.97/71.02 cnf(1555,plain,
% 70.97/71.02 (~E(f3(x15551,f1(x15551)),f3(f4(f4(a5,a6),a6),f1(f4(a5,f4(a6,a6)))))),
% 70.97/71.02 inference(scs_inference,[],[1481,111,8,4,5,6,7,2])).
% 70.97/71.02 cnf(2158,plain,
% 70.97/71.02 ($false),
% 70.97/71.02 inference(scs_inference,[],[1555,21,6,4]),
% 70.97/71.02 ['proof']).
% 70.97/71.02 % SZS output end Proof
% 70.97/71.02 % Total time :70.170000s
%------------------------------------------------------------------------------