%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG023-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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:00:40 EDT 2024
% Result : Unsatisfiable 70.77s 70.89s
% Output : CNFRefutation 70.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : RNG023-7 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 14:52:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 70.77/70.87 %-------------------------------------------
% 70.77/70.87 % File :CSE---1.7
% 70.77/70.87 % Problem :theBenchmark
% 70.77/70.87 % Transform :cnf
% 70.77/70.87 % Format :tptp:raw
% 70.77/70.87 % Command :java -jar mcs_scs.jar %d %s
% 70.77/70.87
% 70.77/70.87 % Result :Theorem 70.300000s
% 70.77/70.87 % Output :CNFRefutation 70.300000s
% 70.77/70.87 %-------------------------------------------
% 70.77/70.88 %--------------------------------------------------------------------------
% 70.77/70.88 % File : RNG023-7 : TPTP v8.2.0. Released v1.0.0.
% 70.77/70.88 % Domain : Ring Theory (Alternative)
% 70.77/70.88 % Problem : Left alternative
% 70.77/70.88 % Version : [Ste87] (equality) axioms : Augmented.
% 70.77/70.88 % Theorem formulation : In terms of associators
% 70.77/70.88 % English :
% 70.77/70.88
% 70.77/70.88 % Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin
% 70.77/70.88 % : [Ste92] Stevens (1992), Unpublished Note
% 70.77/70.88 % Source : [TPTP]
% 70.77/70.88 % Names :
% 70.77/70.88
% 70.77/70.88 % Status : Unsatisfiable
% 70.77/70.88 % Rating : 0.00 v8.2.0, 0.04 v8.1.0, 0.10 v7.5.0, 0.08 v7.4.0, 0.13 v7.3.0, 0.05 v7.1.0, 0.06 v7.0.0, 0.05 v6.4.0, 0.00 v6.3.0, 0.06 v6.2.0, 0.07 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.2.1, 0.11 v2.2.0, 0.00 v2.1.0, 0.13 v2.0.0
% 70.77/70.88 % Syntax : Number of clauses : 23 ( 23 unt; 0 nHn; 1 RR)
% 70.77/70.88 % Number of literals : 23 ( 23 equ; 1 neg)
% 70.77/70.88 % Maximal clause size : 1 ( 1 avg)
% 70.77/70.88 % Maximal term depth : 5 ( 2 avg)
% 70.77/70.88 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 70.77/70.88 % Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% 70.77/70.88 % Number of variables : 45 ( 2 sgn)
% 70.77/70.88 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 70.77/70.88
% 70.77/70.88 % Comments :
% 70.77/70.88 %--------------------------------------------------------------------------
% 70.77/70.88 %----Include nonassociative ring axioms
% 70.77/70.88 include('Axioms/RNG003-0.ax').
% 70.77/70.88 %--------------------------------------------------------------------------
% 70.77/70.88 %----The next 7 clause are extra lemmas which Stevens found useful
% 70.77/70.88 cnf(product_of_inverses,axiom,
% 70.77/70.88 multiply(additive_inverse(X),additive_inverse(Y)) = multiply(X,Y) ).
% 70.77/70.88
% 70.77/70.88 cnf(inverse_product1,axiom,
% 70.77/70.88 multiply(additive_inverse(X),Y) = additive_inverse(multiply(X,Y)) ).
% 70.77/70.88
% 70.77/70.88 cnf(inverse_product2,axiom,
% 70.77/70.88 multiply(X,additive_inverse(Y)) = additive_inverse(multiply(X,Y)) ).
% 70.77/70.88
% 70.77/70.88 cnf(distributivity_of_difference1,axiom,
% 70.77/70.88 multiply(X,add(Y,additive_inverse(Z))) = add(multiply(X,Y),additive_inverse(multiply(X,Z))) ).
% 70.77/70.88
% 70.77/70.88 cnf(distributivity_of_difference2,axiom,
% 70.77/70.88 multiply(add(X,additive_inverse(Y)),Z) = add(multiply(X,Z),additive_inverse(multiply(Y,Z))) ).
% 70.77/70.88
% 70.77/70.88 cnf(distributivity_of_difference3,axiom,
% 70.77/70.88 multiply(additive_inverse(X),add(Y,Z)) = add(additive_inverse(multiply(X,Y)),additive_inverse(multiply(X,Z))) ).
% 70.77/70.88
% 70.77/70.88 cnf(distributivity_of_difference4,axiom,
% 70.77/70.88 multiply(add(X,Y),additive_inverse(Z)) = add(additive_inverse(multiply(X,Z)),additive_inverse(multiply(Y,Z))) ).
% 70.77/70.88
% 70.77/70.88 cnf(prove_left_alternative,negated_conjecture,
% 70.77/70.88 associator(x,x,y) != additive_identity ).
% 70.77/70.89
% 70.77/70.89 %--------------------------------------------------------------------------
% 70.77/70.89 %-------------------------------------------
% 70.77/70.89 % Proof found
% 70.77/70.89 % SZS status Theorem for theBenchmark
% 70.77/70.89 % SZS output start Proof
% 70.77/70.89 %ClaNum:29(EqnAxiom:8)
% 70.77/70.89 %VarNum:88(SingletonVarNum:40)
% 70.77/70.89 %MaxLitNum:1
% 70.77/70.89 %MaxfuncDepth:4
% 70.77/70.89 %SharedTerms:10
% 70.77/70.89 %goalClause: 29
% 70.77/70.89 %singleGoalClaCount:1
% 70.77/70.89 [29]~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),a2)
% 70.77/70.89 [10]E(f4(x101,a2),a2)
% 70.77/70.89 [11]E(f4(a2,x111),a2)
% 70.77/70.89 [12]E(f3(x121,a2),x121)
% 70.77/70.89 [13]E(f3(a2,x131),x131)
% 70.77/70.89 [9]E(f1(f1(x91)),x91)
% 70.77/70.89 [14]E(f3(x141,f1(x141)),a2)
% 70.77/70.89 [15]E(f3(f1(x151),x151),a2)
% 70.77/70.89 [16]E(f3(x161,x162),f3(x162,x161))
% 70.77/70.89 [17]E(f4(f1(x171),f1(x172)),f4(x171,x172))
% 70.77/70.89 [18]E(f1(f4(x181,x182)),f4(x181,f1(x182)))
% 70.77/70.89 [19]E(f1(f4(x191,x192)),f4(f1(x191),x192))
% 70.77/70.89 [21]E(f4(f4(x211,x212),x212),f4(x211,f4(x212,x212)))
% 70.77/70.89 [22]E(f4(f4(x221,x221),x222),f4(x221,f4(x221,x222)))
% 70.77/70.89 [20]E(f3(f3(x201,x202),x203),f3(x201,f3(x202,x203)))
% 70.77/70.89 [23]E(f3(f4(x231,x232),f4(x231,x233)),f4(x231,f3(x232,x233)))
% 70.77/70.89 [24]E(f3(f4(x241,x242),f4(x243,x242)),f4(f3(x241,x243),x242))
% 70.77/70.89 [25]E(f3(f4(x251,x252),f1(f4(x251,x253))),f4(x251,f3(x252,f1(x253))))
% 70.77/70.89 [26]E(f3(f4(x261,x262),f1(f4(x263,x262))),f4(f3(x261,f1(x263)),x262))
% 70.77/70.89 [27]E(f3(f1(f4(x271,x272)),f1(f4(x271,x273))),f4(f1(x271),f3(x272,x273)))
% 70.77/70.89 [28]E(f3(f1(f4(x281,x282)),f1(f4(x283,x282))),f4(f3(x281,x283),f1(x282)))
% 70.77/70.89 %EqnAxiom
% 70.77/70.89 [1]E(x11,x11)
% 70.77/70.89 [2]E(x22,x21)+~E(x21,x22)
% 70.77/70.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 70.77/70.89 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 70.77/70.89 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 70.77/70.89 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 70.77/70.89 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 70.77/70.89 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 70.77/70.89
% 70.77/70.89 %-------------------------------------------
% 70.88/70.90 cnf(30,plain,
% 70.88/70.90 (E(x301,f3(x301,a2))),
% 70.88/70.90 inference(scs_inference,[],[12,2])).
% 70.88/70.90 cnf(33,plain,
% 70.88/70.90 (E(x331,f3(a2,x331))),
% 70.88/70.90 inference(scs_inference,[],[13,2])).
% 70.88/70.90 cnf(34,plain,
% 70.88/70.90 (E(f3(a2,f4(f4(x341,x342),x342)),f4(x341,f4(x342,x342)))),
% 70.88/70.90 inference(scs_inference,[],[13,21,2,3])).
% 70.88/70.90 cnf(36,plain,
% 70.88/70.90 (E(f4(x361,f4(x362,x362)),f3(a2,f4(f4(x361,x362),x362)))),
% 70.88/70.90 inference(scs_inference,[],[34,2])).
% 70.88/70.90 cnf(37,plain,
% 70.88/70.90 (E(f3(f4(x371,x372),f4(x371,x373)),f4(x371,f3(x373,x372)))),
% 70.88/70.90 inference(scs_inference,[],[34,16,23,2,3])).
% 70.88/70.90 cnf(39,plain,
% 70.88/70.90 (E(f4(x391,f3(x392,x393)),f3(f4(x391,x393),f4(x391,x392)))),
% 70.88/70.90 inference(scs_inference,[],[37,2])).
% 70.88/70.90 cnf(40,plain,
% 70.88/70.90 (E(f1(f1(f3(f4(x401,x402),f4(x401,x403)))),f4(x401,f3(x403,x402)))),
% 70.88/70.90 inference(scs_inference,[],[37,9,2,3])).
% 70.88/70.90 cnf(42,plain,
% 70.88/70.90 (E(f4(x421,f3(x422,x423)),f1(f1(f3(f4(x421,x423),f4(x421,x422)))))),
% 70.88/70.90 inference(scs_inference,[],[40,2])).
% 70.88/70.90 cnf(43,plain,
% 70.88/70.90 (E(f4(x431,f3(x432,x432)),f4(f3(x431,x431),x432))),
% 70.88/70.90 inference(scs_inference,[],[39,40,24,2,3])).
% 70.88/70.90 cnf(46,plain,
% 70.88/70.90 (E(f4(f3(x461,x461),x462),f4(x461,f3(x462,x462)))),
% 70.88/70.90 inference(scs_inference,[],[43,2])).
% 70.88/70.90 cnf(47,plain,
% 70.88/70.90 (E(f4(x471,f3(f3(x472,x473),f3(x472,x473))),f3(f4(f3(x471,x471),x473),f4(f3(x471,x471),x472)))),
% 70.88/70.90 inference(scs_inference,[],[39,43,2,3])).
% 70.88/70.90 cnf(50,plain,
% 70.88/70.90 (E(f3(f4(f3(x501,x501),x502),f4(f3(x501,x501),x503)),f4(x501,f3(f3(x503,x502),f3(x503,x502))))),
% 70.88/70.90 inference(scs_inference,[],[47,2])).
% 70.88/70.90 cnf(51,plain,
% 70.88/70.90 (E(f4(f3(x511,x511),x512),f1(f1(f3(f4(x511,x512),f4(x511,x512)))))),
% 70.88/70.90 inference(scs_inference,[],[46,42,47,2,3])).
% 70.88/70.90 cnf(53,plain,
% 70.88/70.90 (E(f1(f1(f3(f4(x531,x532),f4(x531,x532)))),f4(f3(x531,x531),x532))),
% 70.88/70.90 inference(scs_inference,[],[51,2])).
% 70.88/70.90 cnf(54,plain,
% 70.88/70.90 (E(f3(f4(f3(x541,x541),x542),f4(f3(x541,x541),x543)),f3(f4(x541,f3(x543,x542)),f4(x541,f3(x543,x542))))),
% 70.88/70.90 inference(scs_inference,[],[50,39,51,2,3])).
% 70.88/70.90 cnf(56,plain,
% 70.88/70.90 (E(f3(f4(x561,f3(x562,x563)),f4(x561,f3(x562,x563))),f3(f4(f3(x561,x561),x563),f4(f3(x561,x561),x562)))),
% 70.88/70.90 inference(scs_inference,[],[54,2])).
% 70.88/70.90 cnf(60,plain,
% 70.88/70.90 (E(f4(x601,f4(x601,x602)),f4(f4(x601,x601),x602))),
% 70.88/70.90 inference(scs_inference,[],[22,2])).
% 70.88/70.90 cnf(61,plain,
% 70.88/70.90 (E(f4(f3(f4(x611,x611),f4(x611,x611)),x612),f4(x611,f4(x611,f3(x612,x612))))),
% 70.88/70.90 inference(scs_inference,[],[46,22,2,3])).
% 70.88/70.90 cnf(65,plain,
% 70.88/70.90 (E(f1(f4(f1(x651),x652)),f4(x651,x652))),
% 70.88/70.90 inference(scs_inference,[],[61,17,18,2,3])).
% 70.88/70.90 cnf(68,plain,
% 70.88/70.90 (E(f4(x681,x682),f1(f4(f1(x681),x682)))),
% 70.88/70.90 inference(scs_inference,[],[65,2])).
% 70.88/70.90 cnf(69,plain,
% 70.88/70.90 (E(f1(f1(f1(f4(x691,x692)))),f4(f1(x691),x692))),
% 70.88/70.90 inference(scs_inference,[],[65,19,9,2,3])).
% 70.88/70.90 cnf(71,plain,
% 70.88/70.90 (E(f4(f1(x711),x712),f1(f1(f1(f4(x711,x712)))))),
% 70.88/70.90 inference(scs_inference,[],[69,2])).
% 70.88/70.90 cnf(72,plain,
% 70.88/70.90 (E(f3(x721,x722),f3(x721,f3(x722,a2)))),
% 70.88/70.90 inference(scs_inference,[],[30,69,20,2,3])).
% 70.88/70.90 cnf(75,plain,
% 70.88/70.90 (E(f3(x751,f3(x752,a2)),f3(x751,x752))),
% 70.88/70.90 inference(scs_inference,[],[72,2])).
% 70.88/70.90 cnf(76,plain,
% 70.88/70.90 (~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),f4(x761,a2))),
% 70.88/70.90 inference(scs_inference,[],[29,72,10,2,3])).
% 70.88/70.90 cnf(81,plain,
% 70.88/70.90 (E(a2,f3(x811,f1(x811)))),
% 70.88/70.90 inference(scs_inference,[],[14,2])).
% 70.88/70.90 cnf(84,plain,
% 70.88/70.90 (E(a2,f3(f1(x841),x841))),
% 70.88/70.90 inference(scs_inference,[],[15,2])).
% 70.88/70.90 cnf(85,plain,
% 70.88/70.90 (E(f3(f1(x851),x851),f3(x852,f1(x852)))),
% 70.88/70.90 inference(scs_inference,[],[81,15,2,3])).
% 70.88/70.90 cnf(86,plain,
% 70.88/70.90 (E(f3(x861,f1(x861)),f3(f1(x862),x862))),
% 70.88/70.90 inference(scs_inference,[],[85,2])).
% 70.88/70.90 cnf(87,plain,
% 70.88/70.90 (E(f4(x871,a2),f3(f1(x872),x872))),
% 70.88/70.90 inference(scs_inference,[],[84,85,10,2,3])).
% 70.88/70.90 cnf(88,plain,
% 70.88/70.90 (E(f3(f1(x881),x881),f4(x882,a2))),
% 70.88/70.90 inference(scs_inference,[],[87,2])).
% 70.88/70.90 cnf(89,plain,
% 70.88/70.90 (E(f1(a2),f3(f1(x891),x891))),
% 70.88/70.90 inference(scs_inference,[],[86,33,87,2,3])).
% 70.88/70.90 cnf(92,plain,
% 70.88/70.90 (E(f3(f1(x921),x921),f1(a2))),
% 70.88/70.90 inference(scs_inference,[],[89,2])).
% 70.88/70.90 cnf(93,plain,
% 70.88/70.90 (E(f3(f1(x931),x931),f1(f1(f1(f4(x932,a2)))))),
% 70.88/70.90 inference(scs_inference,[],[71,88,89,2,3])).
% 70.88/70.90 cnf(96,plain,
% 70.88/70.90 (E(f1(f1(f1(f4(x961,a2)))),f3(f1(x962),x962))),
% 70.88/70.90 inference(scs_inference,[],[93,2])).
% 70.88/70.90 cnf(97,plain,
% 70.88/70.90 (E(f3(x971,f1(x971)),f1(a2))),
% 70.88/70.90 inference(scs_inference,[],[92,86,93,2,3])).
% 70.88/70.90 cnf(100,plain,
% 70.88/70.90 (~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),f3(f1(x1001),x1001))),
% 70.88/70.90 inference(scs_inference,[],[88,97,76,2,3])).
% 70.88/70.90 cnf(106,plain,
% 70.88/70.90 (E(f1(f1(f1(f4(x1061,a2)))),f1(a2))),
% 70.88/70.90 inference(scs_inference,[],[96,92,26,2,3])).
% 70.88/70.90 cnf(108,plain,
% 70.88/70.90 (E(f1(a2),f1(f1(f1(f4(x1081,a2)))))),
% 70.88/70.90 inference(scs_inference,[],[106,2])).
% 70.88/70.90 cnf(109,plain,
% 70.88/70.90 (E(f4(a2,x1091),f3(x1092,f1(x1092)))),
% 70.88/70.90 inference(scs_inference,[],[81,106,11,2,3])).
% 70.88/70.90 cnf(111,plain,
% 70.88/70.90 (~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),f3(x1111,f1(x1111)))),
% 70.88/70.90 inference(scs_inference,[],[86,109,100,2,3])).
% 70.88/70.90 cnf(113,plain,
% 70.88/70.90 (E(f4(f1(x1131),f3(x1132,x1133)),f3(f1(f4(x1131,x1132)),f1(f4(x1131,x1133))))),
% 70.88/70.90 inference(scs_inference,[],[27,2])).
% 70.88/70.90 cnf(116,plain,
% 70.88/70.90 (E(f4(f3(x1161,x1162),f1(x1163)),f3(f1(f4(x1161,x1163)),f1(f4(x1162,x1163))))),
% 70.88/70.90 inference(scs_inference,[],[28,2])).
% 70.88/70.90 cnf(123,plain,
% 70.88/70.90 (E(f4(x1231,f3(x1232,x1233)),f3(f4(x1231,x1232),f4(x1231,x1233)))),
% 70.88/70.90 inference(scs_inference,[],[23,2])).
% 70.88/70.90 cnf(127,plain,
% 70.88/70.90 (E(f4(f3(x1271,x1272),x1273),f3(f4(x1271,x1273),f4(x1272,x1273)))),
% 70.88/70.90 inference(scs_inference,[],[24,2])).
% 70.88/70.90 cnf(128,plain,
% 70.88/70.90 (E(f4(f3(x1281,x1281),f3(x1282,x1283)),f3(f4(x1281,f3(x1283,x1282)),f4(x1281,f3(x1283,x1282))))),
% 70.88/70.90 inference(scs_inference,[],[123,54,24,2,3])).
% 70.88/70.90 cnf(131,plain,
% 70.88/70.90 (E(f3(f4(x1311,f3(x1312,x1313)),f4(x1311,f3(x1312,x1313))),f4(f3(x1311,x1311),f3(x1313,x1312)))),
% 70.88/70.90 inference(scs_inference,[],[128,2])).
% 70.88/70.90 cnf(132,plain,
% 70.88/70.90 (E(f4(f3(f3(x1321,x1321),f3(x1321,x1321)),x1322),f3(f4(x1321,f3(x1322,x1322)),f4(x1321,f3(x1322,x1322))))),
% 70.88/70.90 inference(scs_inference,[],[127,128,54,2,3])).
% 70.88/70.90 cnf(135,plain,
% 70.88/70.90 (E(f3(f4(x1351,f3(x1352,x1352)),f4(x1351,f3(x1352,x1352))),f4(f3(f3(x1351,x1351),f3(x1351,x1351)),x1352))),
% 70.88/70.90 inference(scs_inference,[],[132,2])).
% 70.88/70.90 cnf(138,plain,
% 70.88/70.90 (E(f4(x1381,x1382),f4(f1(x1381),f1(x1382)))),
% 70.88/70.90 inference(scs_inference,[],[17,2])).
% 70.88/70.90 cnf(141,plain,
% 70.88/70.90 (E(f4(x1411,f1(x1412)),f1(f4(x1411,x1412)))),
% 70.88/70.90 inference(scs_inference,[],[18,2])).
% 70.88/70.90 cnf(142,plain,
% 70.88/70.90 (E(f1(f1(f3(f4(x1421,x1422),f4(x1421,x1422)))),f4(f1(f3(x1421,x1421)),f1(x1422)))),
% 70.88/70.90 inference(scs_inference,[],[53,138,18,2,3])).
% 70.88/70.90 cnf(145,plain,
% 70.88/70.90 (E(f3(f4(x1451,f3(x1452,x1453)),f4(x1451,f3(x1452,x1453))),f1(f4(f1(f3(x1451,x1451)),f3(x1453,x1452))))),
% 70.88/70.90 inference(scs_inference,[],[131,68,142,2,3])).
% 70.88/70.90 cnf(148,plain,
% 70.88/70.90 (E(f3(f4(x1481,f3(x1482,x1482)),f4(x1481,f3(x1482,x1482))),f4(f1(f3(f3(x1481,x1481),f3(x1481,x1481))),f1(x1482)))),
% 70.88/70.90 inference(scs_inference,[],[135,138,145,2,3])).
% 70.88/70.90 cnf(150,plain,
% 70.88/70.90 (E(f4(f1(f3(f3(x1501,x1501),f3(x1501,x1501))),f1(x1502)),f3(f4(x1501,f3(x1502,x1502)),f4(x1501,f3(x1502,x1502))))),
% 70.88/70.90 inference(scs_inference,[],[148,2])).
% 70.88/70.90 cnf(167,plain,
% 70.88/70.90 (E(f4(f1(x1671),x1672),f1(f4(x1671,x1672)))),
% 70.88/70.90 inference(scs_inference,[],[19,2])).
% 70.88/70.90 cnf(169,plain,
% 70.88/70.90 (E(f3(x1691,f3(x1692,x1693)),f3(f3(x1691,x1692),x1693))),
% 70.88/70.90 inference(scs_inference,[],[20,2])).
% 70.88/70.90 cnf(172,plain,
% 70.88/70.91 (E(x1721,f1(f1(x1721)))),
% 70.88/70.91 inference(scs_inference,[],[9,2])).
% 70.88/70.91 cnf(173,plain,
% 70.88/70.91 (E(f4(f1(f3(f3(x1731,x1731),f3(x1731,x1731))),f1(x1732)),f3(f4(f3(x1731,x1731),x1732),f4(f3(x1731,x1731),x1732)))),
% 70.88/70.91 inference(scs_inference,[],[150,56,9,2,3])).
% 70.88/70.91 cnf(176,plain,
% 70.88/70.91 (E(f3(x1761,f3(x1762,x1763)),f1(f1(f3(f3(x1761,x1762),x1763))))),
% 70.88/70.91 inference(scs_inference,[],[169,172,173,2,3])).
% 70.88/70.91 cnf(185,plain,
% 70.88/70.91 (E(f1(f1(f4(x1851,x1852))),f1(f4(f1(x1851),x1852)))),
% 70.88/70.91 inference(scs_inference,[],[9,68,3])).
% 70.88/70.91 cnf(187,plain,
% 70.88/70.91 (E(f1(f4(f1(x1871),x1872)),f1(f1(f4(x1871,x1872))))),
% 70.88/70.91 inference(scs_inference,[],[9,68,3,2])).
% 70.88/70.91 cnf(190,plain,
% 70.88/70.91 (E(f3(f1(f4(x1901,x1902)),f1(f4(x1901,x1903))),f3(f4(f1(x1901),f3(x1902,x1903)),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,113,3,2])).
% 70.88/70.91 cnf(193,plain,
% 70.88/70.91 (E(f3(f1(f4(x1931,x1932)),f1(f4(x1933,x1932))),f3(f4(f3(x1931,x1933),f1(x1932)),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,116,3,2])).
% 70.88/70.91 cnf(196,plain,
% 70.88/70.91 (E(f3(a2,f4(f4(x1961,x1962),x1962)),f3(f4(x1961,f4(x1962,x1962)),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,36,3,2])).
% 70.88/70.91 cnf(197,plain,
% 70.88/70.91 (E(f3(f4(x1971,x1972),a2),f1(f4(f1(x1971),x1972)))),
% 70.88/70.91 inference(scs_inference,[],[12,68,3])).
% 70.88/70.91 cnf(199,plain,
% 70.88/70.91 (E(f1(f4(f1(x1991),x1992)),f3(f4(x1991,x1992),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,68,3,2])).
% 70.88/70.91 cnf(200,plain,
% 70.88/70.91 (E(f3(f1(f4(f1(x2001),x2002)),a2),f3(f4(x2001,x2002),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,199,3])).
% 70.88/70.91 cnf(202,plain,
% 70.88/70.91 (E(f3(f4(x2021,x2022),a2),f3(f1(f4(f1(x2021),x2022)),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,199,3,2])).
% 70.88/70.91 cnf(203,plain,
% 70.88/70.91 (E(f3(f3(f4(x2031,x2032),a2),a2),f1(f4(f1(x2031),x2032)))),
% 70.88/70.91 inference(scs_inference,[],[12,197,3])).
% 70.88/70.91 cnf(205,plain,
% 70.88/70.91 (E(f1(f4(f1(x2051),x2052)),f3(f3(f4(x2051,x2052),a2),a2))),
% 70.88/70.91 inference(scs_inference,[],[12,197,3,2])).
% 70.88/70.91 cnf(211,plain,
% 70.88/70.91 (E(f3(f1(f4(x2111,x2112)),f1(f4(x2111,x2113))),f3(a2,f4(f1(x2111),f3(x2112,x2113))))),
% 70.88/70.91 inference(scs_inference,[],[13,113,3,2])).
% 70.88/70.91 cnf(214,plain,
% 70.88/70.91 (E(f3(f1(f4(x2141,x2142)),f1(f4(x2143,x2142))),f3(a2,f4(f3(x2141,x2143),f1(x2142))))),
% 70.88/70.91 inference(scs_inference,[],[13,116,3,2])).
% 70.88/70.91 cnf(220,plain,
% 70.88/70.91 (E(f3(a2,f4(f4(x2201,x2202),x2202)),f3(a2,f4(x2201,f4(x2202,x2202))))),
% 70.88/70.91 inference(scs_inference,[],[13,36,3,2])).
% 70.88/70.91 cnf(221,plain,
% 70.88/70.91 (E(f3(a2,f4(x2211,x2212)),f1(f4(f1(x2211),x2212)))),
% 70.88/70.91 inference(scs_inference,[],[13,68,3])).
% 70.88/70.91 cnf(223,plain,
% 70.88/70.91 (E(f1(f4(f1(x2231),x2232)),f3(a2,f4(x2231,x2232)))),
% 70.88/70.91 inference(scs_inference,[],[13,68,3,2])).
% 70.88/70.91 cnf(227,plain,
% 70.88/70.91 (E(f3(a2,f3(a2,f4(x2271,x2272))),f1(f4(f1(x2271),x2272)))),
% 70.88/70.91 inference(scs_inference,[],[13,221,3])).
% 70.88/70.91 cnf(232,plain,
% 70.88/70.91 (E(f1(f4(f1(x2321),x2322)),f3(a2,f3(f4(x2321,x2322),a2)))),
% 70.88/70.91 inference(scs_inference,[],[13,197,3,2])).
% 70.88/70.91 cnf(233,plain,
% 70.88/70.91 (E(f4(f1(x2331),f3(x2332,x2332)),f3(f4(f3(x2331,x2331),f1(x2332)),a2))),
% 70.88/70.91 inference(scs_inference,[],[193,113,3])).
% 70.88/70.91 cnf(237,plain,
% 70.88/70.91 (E(f4(f3(x2371,x2371),f1(x2372)),f3(f4(f1(x2371),f3(x2372,x2372)),a2))),
% 70.88/70.91 inference(scs_inference,[],[190,116,3])).
% 70.88/70.91 cnf(245,plain,
% 70.88/70.91 (E(f4(f3(x2451,x2451),f1(x2452)),f3(a2,f4(f1(x2451),f3(x2452,x2452))))),
% 70.88/70.91 inference(scs_inference,[],[211,116,3])).
% 70.88/70.91 cnf(249,plain,
% 70.88/70.91 (E(f4(f4(x2491,x2492),x2492),f3(a2,f4(x2491,f4(x2492,x2492))))),
% 70.88/70.91 inference(scs_inference,[],[220,33,3])).
% 70.88/70.91 cnf(272,plain,
% 70.88/70.91 (E(f4(f1(x2721),f1(x2722)),f3(f3(f4(x2721,x2722),a2),a2))),
% 70.88/70.91 inference(scs_inference,[],[205,141,3])).
% 70.88/70.91 cnf(290,plain,
% 70.88/70.91 (E(f3(f4(x2901,x2902),f3(a2,a2)),f1(f4(f1(x2901),x2902)))),
% 70.88/70.91 inference(scs_inference,[],[169,203,3])).
% 70.88/70.91 cnf(292,plain,
% 70.88/70.91 (E(f1(f4(f1(x2921),x2922)),f3(f4(x2921,x2922),f3(a2,a2)))),
% 70.88/70.91 inference(scs_inference,[],[169,203,3,2])).
% 70.88/70.91 cnf(296,plain,
% 70.88/70.91 (E(f4(f1(x2961),f1(x2962)),f3(a2,f3(f4(x2961,x2962),a2)))),
% 70.88/70.91 inference(scs_inference,[],[232,141,3])).
% 70.88/70.91 cnf(317,plain,
% 70.88/70.91 (E(f3(f4(x3171,f4(x3172,x3172)),a2),f3(f4(f4(x3171,x3172),x3172),a2))),
% 70.88/70.91 inference(scs_inference,[],[16,196,3,2])).
% 70.88/70.91 cnf(320,plain,
% 70.88/70.91 (E(f3(f4(f4(x3201,x3202),x3202),a2),f3(a2,f4(x3201,f4(x3202,x3202))))),
% 70.88/70.91 inference(scs_inference,[],[16,317,3,2])).
% 70.88/70.91 cnf(323,plain,
% 70.88/70.91 (E(f3(f1(f4(f1(x3231),x3232)),a2),f3(a2,f4(x3231,x3232)))),
% 70.88/70.91 inference(scs_inference,[],[16,202,3,2])).
% 70.88/70.91 cnf(335,plain,
% 70.88/70.91 (E(f3(f4(f1(x3351),f3(x3352,x3353)),a2),f3(f1(f4(x3351,x3353)),f1(f4(x3351,x3352))))),
% 70.88/70.91 inference(scs_inference,[],[16,190,3,2])).
% 70.88/70.91 cnf(338,plain,
% 70.88/70.91 (E(f3(f1(f4(x3381,x3382)),f1(f4(x3381,x3383))),f3(a2,f4(f1(x3381),f3(x3383,x3382))))),
% 70.88/70.91 inference(scs_inference,[],[16,335,3,2])).
% 70.88/70.91 cnf(341,plain,
% 70.88/70.91 (E(f3(f4(f3(x3411,x3412),f1(x3413)),a2),f3(f1(f4(x3412,x3413)),f1(f4(x3411,x3413))))),
% 70.88/70.91 inference(scs_inference,[],[16,193,3,2])).
% 70.88/70.91 cnf(344,plain,
% 70.88/70.91 (E(f3(f1(f4(x3441,x3442)),f1(f4(x3443,x3442))),f3(a2,f4(f3(x3443,x3441),f1(x3442))))),
% 70.88/70.91 inference(scs_inference,[],[16,341,3,2])).
% 70.88/70.91 cnf(354,plain,
% 70.88/70.91 (E(f4(f1(f1(x3541)),x3542),f3(f4(x3541,x3542),f3(a2,a2)))),
% 70.88/70.91 inference(scs_inference,[],[292,167,3])).
% 70.88/70.91 cnf(363,plain,
% 70.88/70.91 (E(f1(f4(f1(x3631),x3632)),f3(f3(a2,a2),f4(x3631,x3632)))),
% 70.88/70.91 inference(scs_inference,[],[16,290,3,2])).
% 70.88/70.91 cnf(366,plain,
% 70.88/70.91 (E(f1(f4(f1(x3661),x3662)),f3(f3(a2,f4(x3661,x3662)),a2))),
% 70.88/70.91 inference(scs_inference,[],[16,227,3,2])).
% 70.88/70.91 cnf(370,plain,
% 70.88/70.91 (E(f1(f1(f3(f3(x3701,x3702),x3703))),f3(f3(x3702,x3703),x3701))),
% 70.94/70.91 inference(scs_inference,[],[16,176,3,2])).
% 70.94/70.91 cnf(384,plain,
% 70.94/70.91 (E(f3(f4(f1(x3841),f3(x3842,x3842)),a2),f3(a2,f4(f3(x3841,x3841),f1(x3842))))),
% 70.94/70.91 inference(scs_inference,[],[344,335,3])).
% 70.94/70.91 cnf(387,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x3871,x3871),f1(x3872))),f3(f4(f1(x3871),f3(x3872,x3872)),a2))),
% 70.94/70.91 inference(scs_inference,[],[344,335,3,2])).
% 70.94/70.91 cnf(391,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x3911),f3(x3912,x3912))),f3(f4(f3(x3911,x3911),f1(x3912)),a2))),
% 70.94/70.91 inference(scs_inference,[],[338,341,3,2])).
% 70.94/70.91 cnf(395,plain,
% 70.94/70.91 (E(f1(f1(f1(f4(x3951,x3952)))),f4(f1(f1(x3951)),f1(x3952)))),
% 70.94/70.91 inference(scs_inference,[],[17,71,3,2])).
% 70.94/70.91 cnf(396,plain,
% 70.94/70.91 (E(f1(f4(x3961,x3962)),f4(f1(f1(x3961)),f1(x3962)))),
% 70.94/70.91 inference(scs_inference,[],[395,172,3])).
% 70.94/70.91 cnf(398,plain,
% 70.94/70.91 (E(f4(f1(f1(x3981)),f1(x3982)),f1(f4(x3981,x3982)))),
% 70.94/70.91 inference(scs_inference,[],[395,172,3,2])).
% 70.94/70.91 cnf(409,plain,
% 70.94/70.91 (E(f4(f1(f1(x4091)),f1(a2)),f1(a2))),
% 70.94/70.91 inference(scs_inference,[],[395,108,3,2])).
% 70.94/70.91 cnf(413,plain,
% 70.94/70.91 (E(f1(f1(f4(x4131,x4132))),f4(f1(f1(f1(x4131))),f1(x4132)))),
% 70.94/70.91 inference(scs_inference,[],[187,398,3,2])).
% 70.94/70.91 cnf(414,plain,
% 70.94/70.91 (E(f4(x4141,x4142),f4(f1(f1(f1(x4141))),f1(x4142)))),
% 70.94/70.91 inference(scs_inference,[],[413,172,3])).
% 70.94/70.91 cnf(419,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x4191),f3(x4192,x4193))),f3(f4(f1(x4191),f3(x4193,x4192)),a2))),
% 70.94/70.91 inference(scs_inference,[],[211,335,3,2])).
% 70.94/70.91 cnf(422,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x4221,x4222),f1(x4223))),f3(f4(f3(x4222,x4221),f1(x4223)),a2))),
% 70.94/70.91 inference(scs_inference,[],[214,341,3,2])).
% 70.94/70.91 cnf(431,plain,
% 70.94/70.91 (E(f4(x4311,f4(x4312,x4312)),f3(f4(f4(x4311,x4312),x4312),a2))),
% 70.94/70.91 inference(scs_inference,[],[30,317,3])).
% 70.94/70.91 cnf(434,plain,
% 70.94/70.91 (E(f4(f1(x4341),f1(f4(x4342,x4342))),f3(a2,f4(f4(x4341,x4342),x4342)))),
% 70.94/70.91 inference(scs_inference,[],[17,36,3])).
% 70.94/70.91 cnf(439,plain,
% 70.94/70.91 (E(f1(f1(f1(f4(x4391,a2)))),f4(f1(f1(x4392)),f1(a2)))),
% 70.94/70.91 inference(scs_inference,[],[409,108,3,2])).
% 70.94/70.91 cnf(444,plain,
% 70.94/70.91 (E(f1(f4(x4441,a2)),f4(f1(f1(x4442)),f1(a2)))),
% 70.94/70.91 inference(scs_inference,[],[439,172,3])).
% 70.94/70.91 cnf(446,plain,
% 70.94/70.91 (E(f4(f1(f1(x4461)),f1(a2)),f1(f4(x4462,a2)))),
% 70.94/70.91 inference(scs_inference,[],[439,172,3,2])).
% 70.94/70.91 cnf(447,plain,
% 70.94/70.91 (E(f4(f1(f1(x4471)),f1(a2)),f3(f3(a2,a2),f4(x4472,a2)))),
% 70.94/70.91 inference(scs_inference,[],[446,363,3])).
% 70.94/70.91 cnf(458,plain,
% 70.94/70.91 (E(f3(f3(a2,f4(x4581,a2)),a2),f4(f1(f1(x4582)),f1(a2)))),
% 70.94/70.91 inference(scs_inference,[],[366,446,3,2])).
% 70.94/70.91 cnf(459,plain,
% 70.94/70.91 (E(f1(f1(f3(f3(a2,a2),f4(x4591,a2)))),f4(f1(f1(x4592)),f1(a2)))),
% 70.94/70.91 inference(scs_inference,[],[370,458,3])).
% 70.94/70.91 cnf(462,plain,
% 70.94/70.91 (E(f4(f1(f1(x4621)),f1(a2)),f3(f4(x4622,a2),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[292,446,459,2,3])).
% 70.94/70.91 cnf(466,plain,
% 70.94/70.91 (E(f4(f1(f1(x4661)),f1(f3(x4662,x4663))),f3(f1(f4(x4661,x4662)),f1(f4(x4661,x4663))))),
% 70.94/70.91 inference(scs_inference,[],[17,113,462,2,3])).
% 70.94/70.91 cnf(468,plain,
% 70.94/70.91 (E(f3(f1(f4(x4681,x4682)),f1(f4(x4681,x4683))),f4(f1(f1(x4681)),f1(f3(x4682,x4683))))),
% 70.94/70.91 inference(scs_inference,[],[466,2])).
% 70.94/70.91 cnf(469,plain,
% 70.94/70.91 (E(f4(f1(f3(x4691,x4692)),f1(f1(x4693))),f3(f1(f4(x4691,x4693)),f1(f4(x4692,x4693))))),
% 70.94/70.91 inference(scs_inference,[],[17,116,466,2,3])).
% 70.94/70.91 cnf(472,plain,
% 70.94/70.91 (E(f4(f1(f1(f1(x4721))),f1(x4722)),f3(f4(x4721,x4722),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[17,354,469,2,3])).
% 70.94/70.91 cnf(476,plain,
% 70.94/70.91 (E(f4(f1(x4761),f1(x4762)),f4(f1(f1(f1(x4761))),f1(x4762)))),
% 70.94/70.91 inference(scs_inference,[],[17,414,472,2,3])).
% 70.94/70.91 cnf(479,plain,
% 70.94/70.91 (E(f4(f1(f1(x4791)),f1(f1(x4792))),f4(f1(f1(f1(x4791))),f1(x4792)))),
% 70.94/70.91 inference(scs_inference,[],[17,476,2,3])).
% 70.94/70.91 cnf(482,plain,
% 70.94/70.91 (E(f4(f1(f1(f1(x4821))),f1(f1(a2))),f3(f3(a2,a2),f4(x4822,a2)))),
% 70.94/70.91 inference(scs_inference,[],[17,479,447,2,3])).
% 70.94/70.91 cnf(485,plain,
% 70.94/70.91 (E(f4(x4851,a2),f4(f1(f1(x4852)),f1(a2)))),
% 70.94/70.91 inference(scs_inference,[],[68,482,444,2,3])).
% 70.94/70.91 cnf(489,plain,
% 70.94/70.91 (E(f4(f1(f1(x4891)),f1(f3(x4892,x4892))),f3(f4(f3(x4891,x4891),f1(x4892)),a2))),
% 70.94/70.91 inference(scs_inference,[],[17,233,485,2,3])).
% 70.94/70.91 cnf(491,plain,
% 70.94/70.91 (E(f3(f4(f3(x4911,x4911),f1(x4912)),a2),f4(f1(f1(x4911)),f1(f3(x4912,x4912))))),
% 70.94/70.91 inference(scs_inference,[],[489,2])).
% 70.94/70.91 cnf(492,plain,
% 70.94/70.91 (E(f4(f1(f3(x4921,x4921)),f1(f1(x4922))),f3(f4(f1(x4921),f3(x4922,x4922)),a2))),
% 70.94/70.91 inference(scs_inference,[],[17,237,489,2,3])).
% 70.94/70.91 cnf(494,plain,
% 70.94/70.91 (E(f3(f4(f1(x4941),f3(x4942,x4942)),a2),f4(f1(f3(x4941,x4941)),f1(f1(x4942))))),
% 70.94/70.91 inference(scs_inference,[],[492,2])).
% 70.94/70.91 cnf(495,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x4951),f3(x4952,x4952))),f4(f1(f1(x4951)),f1(f3(x4952,x4952))))),
% 70.94/70.91 inference(scs_inference,[],[491,391,492,2,3])).
% 70.94/70.91 cnf(497,plain,
% 70.94/70.91 (E(f4(f1(f1(x4971)),f1(f3(x4972,x4972))),f3(a2,f4(f1(x4971),f3(x4972,x4972))))),
% 70.94/70.91 inference(scs_inference,[],[495,2])).
% 70.94/70.91 cnf(498,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x4981,x4981),f1(x4982))),f4(f1(f3(x4981,x4981)),f1(f1(x4982))))),
% 70.94/70.91 inference(scs_inference,[],[494,387,495,2,3])).
% 70.94/70.91 cnf(500,plain,
% 70.94/70.91 (E(f4(f1(f3(x5001,x5001)),f1(f1(x5002))),f3(a2,f4(f3(x5001,x5001),f1(x5002))))),
% 70.94/70.91 inference(scs_inference,[],[498,2])).
% 70.94/70.91 cnf(501,plain,
% 70.94/70.91 (E(f4(f1(f1(x5011)),f1(f3(x5012,x5012))),f3(f4(f1(x5011),f3(x5012,x5012)),a2))),
% 70.94/70.91 inference(scs_inference,[],[497,419,498,2,3])).
% 70.94/70.91 cnf(503,plain,
% 70.94/70.91 (E(f3(f4(f1(x5031),f3(x5032,x5032)),a2),f4(f1(f1(x5031)),f1(f3(x5032,x5032))))),
% 70.94/70.91 inference(scs_inference,[],[501,2])).
% 70.94/70.91 cnf(504,plain,
% 70.94/70.91 (E(f4(f1(f3(x5041,x5041)),f1(f1(x5042))),f3(f4(f3(x5041,x5041),f1(x5042)),a2))),
% 70.94/70.91 inference(scs_inference,[],[500,422,501,2,3])).
% 70.94/70.91 cnf(506,plain,
% 70.94/70.91 (E(f3(f4(f3(x5061,x5061),f1(x5062)),a2),f4(f1(f3(x5061,x5061)),f1(f1(x5062))))),
% 70.94/70.91 inference(scs_inference,[],[504,2])).
% 70.94/70.91 cnf(507,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x5071,x5071),f1(x5072))),f4(f1(f1(x5071)),f1(f3(x5072,x5072))))),
% 70.94/70.91 inference(scs_inference,[],[503,387,504,2,3])).
% 70.94/70.91 cnf(509,plain,
% 70.94/70.91 (E(f4(f1(f1(x5091)),f1(f3(x5092,x5092))),f3(a2,f4(f3(x5091,x5091),f1(x5092))))),
% 70.94/70.91 inference(scs_inference,[],[507,2])).
% 70.94/70.91 cnf(510,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x5101),f3(x5102,x5102))),f4(f1(f3(x5101,x5101)),f1(f1(x5102))))),
% 70.94/70.91 inference(scs_inference,[],[506,391,507,2,3])).
% 70.94/70.91 cnf(512,plain,
% 70.94/70.91 (E(f4(f1(f3(x5121,x5121)),f1(f1(x5122))),f3(a2,f4(f1(x5121),f3(x5122,x5122))))),
% 70.94/70.91 inference(scs_inference,[],[510,2])).
% 70.94/70.91 cnf(513,plain,
% 70.94/70.91 (E(f4(f1(f4(x5131,x5132)),f1(x5132)),f3(a2,f4(x5131,f4(x5132,x5132))))),
% 70.94/70.91 inference(scs_inference,[],[17,249,510,2,3])).
% 70.94/70.91 cnf(516,plain,
% 70.94/70.91 (E(f3(a2,f4(x5161,f4(x5162,x5162))),f4(f1(f4(x5161,x5162)),f1(x5162)))),
% 70.94/70.91 inference(scs_inference,[],[513,2])).
% 70.94/70.91 cnf(517,plain,
% 70.94/70.91 (E(f4(f1(x5171),f1(f4(x5172,x5172))),f3(f4(f4(x5171,x5172),x5172),a2))),
% 70.94/70.91 inference(scs_inference,[],[17,431,513,2,3])).
% 70.94/70.91 cnf(521,plain,
% 70.94/70.91 (E(f3(f1(f4(f1(x5211),f4(x5212,x5212))),a2),f4(f1(f4(x5211,x5212)),f1(x5212)))),
% 70.94/70.91 inference(scs_inference,[],[516,323,517,2,3])).
% 70.94/70.91 cnf(524,plain,
% 70.94/70.91 (E(f4(f1(f4(x5241,x5242)),f1(x5242)),f3(f1(f4(f1(x5241),f4(x5242,x5242))),a2))),
% 70.94/70.91 inference(scs_inference,[],[521,2])).
% 70.94/70.91 cnf(525,plain,
% 70.94/70.91 (E(f3(f4(f4(x5251,x5252),x5252),a2),f4(f1(f4(x5251,x5252)),f1(x5252)))),
% 70.94/70.91 inference(scs_inference,[],[320,516,521,2,3])).
% 70.94/70.91 cnf(528,plain,
% 70.94/70.91 (E(f4(f1(f1(x5281)),f1(f1(x5282))),f3(f3(f4(x5281,x5282),a2),a2))),
% 70.94/70.91 inference(scs_inference,[],[17,525,272,2,3])).
% 70.94/70.91 cnf(530,plain,
% 70.94/70.91 (E(f3(f3(f4(x5301,x5302),a2),a2),f4(f1(f1(x5301)),f1(f1(x5302))))),
% 70.94/70.91 inference(scs_inference,[],[528,2])).
% 70.94/70.91 cnf(531,plain,
% 70.94/70.91 (E(f4(f1(f1(x5311)),f1(f1(x5312))),f3(a2,f3(f4(x5311,x5312),a2)))),
% 70.94/70.91 inference(scs_inference,[],[17,296,528,2,3])).
% 70.94/70.91 cnf(534,plain,
% 70.94/70.91 (E(f4(f1(f4(x5341,x5342)),f1(x5342)),f3(f4(x5341,f4(x5342,x5342)),a2))),
% 70.94/70.91 inference(scs_inference,[],[524,531,200,2,3])).
% 70.94/70.91 cnf(537,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x5371),f3(x5372,x5372))),f3(a2,f4(f3(x5371,x5371),f1(x5372))))),
% 70.94/70.91 inference(scs_inference,[],[419,534,384,2,3])).
% 70.94/70.91 cnf(540,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x5401,x5401),f1(x5402))),f3(a2,f4(f1(x5401),f3(x5402,x5402))))),
% 70.94/70.91 inference(scs_inference,[],[537,2])).
% 70.94/70.91 cnf(541,plain,
% 70.94/70.91 (E(f4(f1(x5411),f3(x5412,x5412)),f4(f1(f3(x5411,x5411)),f1(f1(x5412))))),
% 70.94/70.91 inference(scs_inference,[],[494,30,537,2,3])).
% 70.94/70.91 cnf(544,plain,
% 70.94/70.91 (E(f4(f1(f1(x5441)),f1(f3(x5442,x5442))),f4(f1(f3(x5441,x5441)),f1(f1(x5442))))),
% 70.94/70.91 inference(scs_inference,[],[17,541,2,3])).
% 70.94/70.91 cnf(546,plain,
% 70.94/70.91 (E(f4(f1(f3(x5461,x5461)),f1(f1(x5462))),f4(f1(f1(x5461)),f1(f3(x5462,x5462))))),
% 70.94/70.91 inference(scs_inference,[],[544,2])).
% 70.94/70.91 cnf(548,plain,
% 70.94/70.91 (E(f4(f1(f1(f1(x5481))),f1(f1(a2))),f3(f4(x5482,a2),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[17,462,3])).
% 70.94/70.91 cnf(559,plain,
% 70.94/70.91 (E(f4(f1(f1(x5591)),f1(f3(x5592,x5592))),f1(f4(f1(f3(x5591,x5591)),f1(x5592))))),
% 70.94/70.91 inference(scs_inference,[],[18,546,3,2])).
% 70.94/70.91 cnf(562,plain,
% 70.94/70.91 (E(f1(f4(f1(f3(x5621,x5621)),f1(x5622))),f1(f4(f1(f1(x5621)),f3(x5622,x5622))))),
% 70.94/70.91 inference(scs_inference,[],[18,559,3,2])).
% 70.94/70.91 cnf(563,plain,
% 70.94/70.91 (E(f1(f4(f1(f1(x5631)),f3(x5632,x5632))),f3(a2,f4(f3(x5631,x5631),f1(x5632))))),
% 70.94/70.91 inference(scs_inference,[],[18,509,3])).
% 70.94/70.91 cnf(565,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x5651,x5651),f1(x5652))),f1(f4(f1(f1(x5651)),f3(x5652,x5652))))),
% 70.94/70.91 inference(scs_inference,[],[18,509,3,2])).
% 70.94/70.91 cnf(568,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x5681),f3(x5682,x5682))),f1(f4(f1(f3(x5681,x5681)),f1(x5682))))),
% 70.94/70.91 inference(scs_inference,[],[18,512,3,2])).
% 70.94/70.91 cnf(571,plain,
% 70.94/70.91 (E(f1(f4(f1(f1(x5711)),f3(x5712,x5712))),f4(f1(f3(x5711,x5711)),f1(f1(x5712))))),
% 70.94/70.91 inference(scs_inference,[],[565,500,3,2])).
% 70.94/70.91 cnf(574,plain,
% 70.94/70.91 (E(f3(f3(a2,a2),f4(f1(x5741),f3(x5742,x5742))),f1(f4(f1(f3(x5741,x5741)),f1(x5742))))),
% 70.94/70.91 inference(scs_inference,[],[562,363,3,2])).
% 70.94/70.91 cnf(577,plain,
% 70.94/70.91 (E(f3(a2,f4(f3(x5771,x5771),f1(x5772))),f3(f3(a2,a2),f4(f1(x5771),f3(x5772,x5772))))),
% 70.94/70.91 inference(scs_inference,[],[574,223,3,2])).
% 70.94/70.91 cnf(584,plain,
% 70.94/70.91 (E(f1(f4(f1(f1(x5841)),f3(x5842,x5842))),f3(f1(f4(x5841,x5842)),f1(f4(x5841,x5842))))),
% 70.94/70.91 inference(scs_inference,[],[565,344,3,2])).
% 70.94/70.91 cnf(587,plain,
% 70.94/70.91 (E(f3(f1(f4(x5871,x5872)),f1(f4(x5871,x5872))),f1(f4(f1(f3(x5871,x5871)),f1(x5872))))),
% 70.94/70.91 inference(scs_inference,[],[584,562,3,2])).
% 70.94/70.91 cnf(590,plain,
% 70.94/70.91 (E(f3(f4(f3(x5901,x5901),f1(x5902)),a2),f1(f4(f1(f1(x5901)),f3(x5902,x5902))))),
% 70.94/70.91 inference(scs_inference,[],[584,193,3,2])).
% 70.94/70.91 cnf(593,plain,
% 70.94/70.91 (E(f3(f4(f3(x5931,x5931),f1(x5932)),f3(a2,a2)),f3(f1(f4(x5931,x5932)),f1(f4(x5931,x5932))))),
% 70.94/70.91 inference(scs_inference,[],[587,292,3,2])).
% 70.94/70.91 cnf(596,plain,
% 70.94/70.91 (E(f4(f1(f1(x5961)),f1(f3(x5962,x5962))),f3(f4(f3(x5961,x5961),f1(x5962)),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[593,468,3,2])).
% 70.94/70.91 cnf(599,plain,
% 70.94/70.91 (E(f3(f4(f3(x5991,x5991),f1(x5992)),f3(a2,a2)),f1(f4(f1(f1(x5991)),f3(x5992,x5992))))),
% 70.94/70.91 inference(scs_inference,[],[18,596,3,2])).
% 70.94/70.91 cnf(602,plain,
% 70.94/70.91 (E(f4(f1(f3(x6021,x6021)),f1(f1(x6022))),f3(f4(f3(x6021,x6021),f1(x6022)),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[571,599,3,2])).
% 70.94/70.91 cnf(605,plain,
% 70.94/70.91 (E(f3(a2,f4(f1(x6051),f3(x6052,x6052))),f3(f4(f3(x6051,x6051),f1(x6052)),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[593,338,3,2])).
% 70.94/70.91 cnf(608,plain,
% 70.94/70.91 (E(f3(f4(f3(x6081,x6081),f1(x6082)),f3(a2,a2)),f3(a2,f4(f3(x6081,x6081),f1(x6082))))),
% 70.94/70.91 inference(scs_inference,[],[605,540,3,2])).
% 70.94/70.91 cnf(614,plain,
% 70.94/70.91 (E(f3(f4(f1(x6141),f3(x6142,x6142)),a2),f3(f4(f3(x6141,x6141),f1(x6142)),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[608,387,3,2])).
% 70.94/70.91 cnf(617,plain,
% 70.94/70.91 (E(f3(f3(a2,a2),f4(f3(x6171,x6171),f1(x6172))),f3(a2,f4(f1(x6171),f3(x6172,x6172))))),
% 70.94/70.91 inference(scs_inference,[],[568,363,3,2])).
% 70.94/70.91 cnf(620,plain,
% 70.94/70.91 (E(f3(f4(f3(x6201,x6201),f1(x6202)),a2),f3(f3(a2,a2),f4(f3(x6201,x6201),f1(x6202))))),
% 70.94/70.91 inference(scs_inference,[],[617,391,3,2])).
% 70.94/70.91 cnf(624,plain,
% 70.94/70.91 (E(f3(f3(a2,a2),f4(f3(x6241,x6241),f1(x6242))),f3(a2,f4(f3(x6241,x6241),f1(x6242))))),
% 70.94/70.91 inference(scs_inference,[],[620,422,3,2])).
% 70.94/70.91 cnf(627,plain,
% 70.94/70.91 (E(f1(f4(f1(f1(x6271)),f3(x6272,x6272))),f3(f3(a2,a2),f4(f3(x6271,x6271),f1(x6272))))),
% 70.94/70.91 inference(scs_inference,[],[624,565,3,2])).
% 70.94/70.91 cnf(633,plain,
% 70.94/70.91 (E(f3(f4(f1(x6331),f3(x6332,x6332)),a2),f3(f4(f3(x6331,x6331),f1(x6332)),a2))),
% 70.94/70.91 inference(scs_inference,[],[590,199,3,2])).
% 70.94/70.91 cnf(636,plain,
% 70.94/70.91 (E(f3(f3(a2,a2),f4(f3(x6361,x6361),f1(x6362))),f3(f4(f1(x6361),f3(x6362,x6362)),a2))),
% 70.94/70.91 inference(scs_inference,[],[633,620,3,2])).
% 70.94/70.91 cnf(645,plain,
% 70.94/70.91 (E(f3(f1(f4(x6451,x6452)),f1(f4(x6451,x6452))),f3(f3(a2,a2),f4(f3(x6451,x6451),f1(x6452))))),
% 70.94/70.91 inference(scs_inference,[],[636,335,3,2])).
% 70.94/70.91 cnf(649,plain,
% 70.94/70.91 (E(f3(f1(f4(x6491,x6492)),f1(f4(x6493,x6492))),f1(f4(f3(x6491,x6493),x6492)))),
% 70.94/70.91 inference(scs_inference,[],[18,116,3,2])).
% 70.94/70.91 cnf(650,plain,
% 70.94/70.91 (E(f1(f4(f1(f1(x6501)),f3(x6502,x6502))),f1(f4(f3(x6501,x6501),x6502)))),
% 70.94/70.91 inference(scs_inference,[],[649,584,3])).
% 70.94/70.91 cnf(652,plain,
% 70.94/70.91 (E(f1(f4(f3(x6521,x6521),x6522)),f1(f4(f1(f1(x6521)),f3(x6522,x6522))))),
% 70.94/70.91 inference(scs_inference,[],[649,584,3,2])).
% 70.94/70.91 cnf(655,plain,
% 70.94/70.91 (E(f3(f3(a2,a2),f4(f3(x6551,x6551),f1(x6552))),f1(f4(f3(x6551,x6551),x6552)))),
% 70.94/70.91 inference(scs_inference,[],[627,652,3,2])).
% 70.94/70.91 cnf(658,plain,
% 70.94/70.91 (E(f1(f4(f3(x6581,x6581),x6582)),f3(f4(f3(x6581,x6581),f1(x6582)),f3(a2,a2)))),
% 70.94/70.91 inference(scs_inference,[],[649,593,3,2])).
% 70.94/70.91 cnf(661,plain,
% 70.94/70.91 (E(f1(f4(f1(x6611),f1(x6612))),f1(f4(x6611,x6612)))),
% 70.94/70.91 inference(scs_inference,[],[18,68,3,2])).
% 70.94/70.91 cnf(662,plain,
% 70.94/70.91 (E(f1(f4(f1(f1(x6621)),f1(x6622))),f1(f1(f4(x6621,x6622))))),
% 70.94/70.91 inference(scs_inference,[],[661,187,3])).
% 70.94/70.91 cnf(665,plain,
% 70.94/70.91 (E(f1(f1(f4(x6651,x6652))),f1(f4(f1(f1(x6651)),f1(x6652))))),
% 70.94/70.92 inference(scs_inference,[],[661,187,3,2])).
% 70.94/70.92 cnf(666,plain,
% 70.94/70.92 (E(f1(f1(f4(x6661,x6662))),f3(a2,f4(f1(x6661),f1(x6662))))),
% 70.94/70.92 inference(scs_inference,[],[665,223,3])).
% 70.94/70.92 cnf(668,plain,
% 70.94/70.92 (E(f3(a2,f4(f1(x6681),f1(x6682))),f1(f1(f4(x6681,x6682))))),
% 70.94/70.92 inference(scs_inference,[],[665,223,3,2])).
% 70.94/70.92 cnf(672,plain,
% 70.94/70.92 (E(f1(f4(f1(f1(x6721)),f1(x6722))),f3(f3(f4(x6721,x6722),a2),a2))),
% 70.94/70.92 inference(scs_inference,[],[661,205,3])).
% 70.94/70.92 cnf(675,plain,
% 70.94/70.92 (E(f3(f3(f4(x6751,x6752),a2),a2),f1(f4(f1(f1(x6751)),f1(x6752))))),
% 70.94/70.92 inference(scs_inference,[],[661,205,3,2])).
% 70.94/70.92 cnf(688,plain,
% 70.94/70.92 (E(f3(f3(a2,a2),f4(f3(x6881,x6881),f1(x6882))),f4(f1(f1(f3(x6881,x6881))),f1(x6882)))),
% 70.94/70.92 inference(scs_inference,[],[655,396,3])).
% 70.94/70.92 cnf(693,plain,
% 70.94/70.92 (E(f4(f1(f1(f3(x6931,x6931))),f1(x6932)),f3(f1(f4(x6931,x6932)),f1(f4(x6931,x6932))))),
% 70.94/70.92 inference(scs_inference,[],[645,688,3,2])).
% 70.94/70.92 cnf(705,plain,
% 70.94/70.92 (E(f4(f1(f1(x7051)),f1(f3(x7052,x7052))),f4(f1(f1(f3(x7051,x7051))),f1(x7052)))),
% 70.94/70.92 inference(scs_inference,[],[693,468,3,2])).
% 70.94/70.92 cnf(708,plain,
% 70.94/70.92 (E(f4(f1(f1(f3(x7081,x7081))),f1(x7082)),f1(f4(f1(f1(x7081)),f3(x7082,x7082))))),
% 70.94/70.92 inference(scs_inference,[],[18,705,3,2])).
% 70.94/70.92 cnf(718,plain,
% 70.94/70.92 (E(f3(f4(f3(x7181,x7181),f1(x7182)),f3(a2,a2)),f3(f4(f1(x7181),f3(x7182,x7182)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[614,75,3,2])).
% 70.94/70.92 cnf(719,plain,
% 70.94/70.92 (E(f4(f1(f3(x7191,x7191)),f1(f1(x7192))),f3(f4(f1(x7191),f3(x7192,x7192)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[602,718,3])).
% 70.94/70.92 cnf(730,plain,
% 70.94/70.92 (E(f3(f4(f1(x7301),f3(x7302,x7302)),f3(a2,a2)),f1(f4(f3(x7301,x7301),x7302)))),
% 70.94/70.92 inference(scs_inference,[],[658,718,3,2])).
% 70.94/70.92 cnf(737,plain,
% 70.94/70.92 (E(f1(f4(f1(f3(x7371,x7371)),f1(x7372))),f3(f4(f1(x7371),f3(x7372,x7372)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[18,719,3])).
% 70.94/70.92 cnf(748,plain,
% 70.94/70.92 (E(f3(f4(f1(x7481),f3(x7482,x7482)),f3(a2,a2)),f3(f1(f4(x7481,x7482)),f1(f4(x7481,x7482))))),
% 70.94/70.92 inference(scs_inference,[],[587,737,3,2])).
% 70.94/70.92 cnf(751,plain,
% 70.94/70.92 (E(f3(f3(a2,a2),f4(f3(x7511,x7511),f1(x7512))),f3(f4(f1(x7511),f3(x7512,x7512)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[748,645,3,2])).
% 70.94/70.92 cnf(757,plain,
% 70.94/70.92 (E(f3(a2,f4(f3(x7571,x7571),f1(x7572))),f3(f4(f1(x7571),f3(x7572,x7572)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[748,214,3,2])).
% 70.94/70.92 cnf(760,plain,
% 70.94/70.92 (E(f1(f4(f1(x7601),x7602)),f3(a2,f4(f1(x7601),f1(x7602))))),
% 70.94/70.92 inference(scs_inference,[],[668,185,3,2])).
% 70.94/70.92 cnf(761,plain,
% 70.94/70.92 (E(f1(f4(f1(f1(f1(x7611))),f1(a2))),f3(f4(x7612,a2),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[18,548,3])).
% 70.94/70.92 cnf(763,plain,
% 70.94/70.92 (E(f3(f4(x7631,a2),f3(a2,a2)),f1(f4(f1(f1(f1(x7632))),f1(a2))))),
% 70.94/70.92 inference(scs_inference,[],[761,2])).
% 70.94/70.92 cnf(764,plain,
% 70.94/70.92 (E(f1(f1(f4(f1(x7641),a2))),f3(f4(x7642,a2),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[665,761,2,3])).
% 70.94/70.92 cnf(766,plain,
% 70.94/70.92 (E(f3(f4(x7661,a2),f3(a2,a2)),f1(f1(f4(f1(x7662),a2))))),
% 70.94/70.92 inference(scs_inference,[],[764,2])).
% 70.94/70.92 cnf(767,plain,
% 70.94/70.92 (E(f3(f4(x7671,a2),f3(a2,a2)),f3(f3(a2,f4(f1(f1(x7672)),f1(a2))),a2))),
% 70.94/70.92 inference(scs_inference,[],[763,366,764,2,3])).
% 70.94/70.92 cnf(770,plain,
% 70.94/70.92 (E(f1(f4(f3(x7701,x7701),x7702)),f3(a2,f4(f1(x7701),f3(x7702,x7702))))),
% 70.94/70.92 inference(scs_inference,[],[18,245,767,2,3])).
% 70.94/70.92 cnf(774,plain,
% 70.94/70.92 (E(f1(f4(f1(x7741),f4(x7742,x7742))),f3(a2,f4(f4(x7741,x7742),x7742)))),
% 70.94/70.92 inference(scs_inference,[],[18,434,770,2,3])).
% 70.94/70.92 cnf(776,plain,
% 70.94/70.92 (E(f3(a2,f4(f4(x7761,x7762),x7762)),f1(f4(f1(x7761),f4(x7762,x7762))))),
% 70.94/70.92 inference(scs_inference,[],[774,2])).
% 70.94/70.92 cnf(777,plain,
% 70.94/70.92 (E(f3(f4(x7771,a2),f3(a2,a2)),f3(a2,f4(f1(f1(x7772)),f1(a2))))),
% 70.94/70.92 inference(scs_inference,[],[766,774,666,2,3])).
% 70.94/70.92 cnf(780,plain,
% 70.94/70.92 (E(f3(a2,f4(f4(x7801,x7802),x7802)),f3(f4(x7801,f4(x7802,x7802)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[776,292,777,2,3])).
% 70.94/70.92 cnf(782,plain,
% 70.94/70.92 (E(f3(f4(x7821,f4(x7822,x7822)),f3(a2,a2)),f3(a2,f4(f4(x7821,x7822),x7822)))),
% 70.94/70.92 inference(scs_inference,[],[780,2])).
% 70.94/70.92 cnf(783,plain,
% 70.94/70.92 (E(f3(f4(x7831,a2),f3(a2,a2)),f3(f3(f4(f1(x7832),a2),a2),a2))),
% 70.94/70.92 inference(scs_inference,[],[763,780,672,2,3])).
% 70.94/70.92 cnf(786,plain,
% 70.94/70.92 (E(f3(f4(x7861,f4(x7862,x7862)),f3(a2,a2)),f3(a2,f4(x7861,f4(x7862,x7862))))),
% 70.94/70.92 inference(scs_inference,[],[782,220,783,2,3])).
% 70.94/70.92 cnf(788,plain,
% 70.94/70.92 (E(f3(a2,f4(x7881,f4(x7882,x7882))),f3(f4(x7881,f4(x7882,x7882)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[786,2])).
% 70.94/70.92 cnf(789,plain,
% 70.94/70.92 (E(f3(f3(f4(x7891,x7892),a2),a2),f1(f1(f4(x7891,x7892))))),
% 70.94/70.92 inference(scs_inference,[],[675,662,786,2,3])).
% 70.94/70.92 cnf(791,plain,
% 70.94/70.92 (E(f1(f1(f4(x7911,x7912))),f3(f3(f4(x7911,x7912),a2),a2))),
% 70.94/70.92 inference(scs_inference,[],[789,2])).
% 70.94/70.92 cnf(792,plain,
% 70.94/70.92 (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.94/70.92 inference(scs_inference,[],[788,782,789,2,3])).
% 70.94/70.92 cnf(796,plain,
% 70.94/70.92 (E(f3(f1(f4(f1(x7961),f4(x7962,x7962))),a2),f3(f4(x7961,f4(x7962,x7962)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[788,323,792,2,3])).
% 70.94/70.92 cnf(800,plain,
% 70.94/70.92 (E(f4(f3(x8001,x8001),f1(x8002)),f3(f4(f1(x8001),f3(x8002,x8002)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[757,33,796,2,3])).
% 70.94/70.92 cnf(803,plain,
% 70.94/70.92 (E(f1(f1(f4(x8031,x8032))),f4(f1(f1(x8031)),f1(f1(x8032))))),
% 70.94/70.92 inference(scs_inference,[],[791,530,800,2,3])).
% 70.94/70.92 cnf(806,plain,
% 70.94/70.92 (E(f3(f4(f4(x8061,x8062),x8062),a2),f3(f4(x8061,f4(x8062,x8062)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[320,788,803,2,3])).
% 70.94/70.92 cnf(809,plain,
% 70.94/70.92 (E(f4(f1(f3(x8091,x8091)),f1(f1(x8092))),f3(f3(a2,a2),f4(f1(x8091),f3(x8092,x8092))))),
% 70.94/70.92 inference(scs_inference,[],[500,577,806,2,3])).
% 70.94/70.92 cnf(812,plain,
% 70.94/70.92 (E(f1(f4(f1(f1(x8121)),x8122)),f3(f4(x8121,f1(x8122)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[18,809,354,2,3])).
% 70.94/70.92 cnf(815,plain,
% 70.94/70.92 (E(f3(f4(x8151,f1(x8152)),f3(a2,a2)),f1(f4(f1(f1(x8151)),x8152)))),
% 70.94/70.92 inference(scs_inference,[],[812,2])).
% 70.94/70.92 cnf(816,plain,
% 70.94/70.92 (E(f3(f4(f3(x8161,x8161),f1(x8162)),f3(a2,a2)),f3(f4(x8161,f1(f3(x8162,x8162))),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[599,812,2,3])).
% 70.94/70.92 cnf(818,plain,
% 70.94/70.92 (E(f3(f4(x8181,f1(f3(x8182,x8182))),f3(a2,a2)),f3(f4(f3(x8181,x8181),f1(x8182)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[816,2])).
% 70.94/70.92 cnf(819,plain,
% 70.94/70.92 (E(f3(f4(x8191,f1(x8192)),f3(a2,a2)),f3(a2,f4(f1(f1(x8191)),f1(x8192))))),
% 70.94/70.92 inference(scs_inference,[],[815,760,816,2,3])).
% 70.94/70.92 cnf(822,plain,
% 70.94/70.92 (E(f1(f4(f3(x8221,x8221),x8222)),f4(f1(f3(x8221,x8221)),f1(f1(x8222))))),
% 70.94/70.92 inference(scs_inference,[],[571,652,819,2,3])).
% 70.94/70.92 cnf(825,plain,
% 70.94/70.92 (E(f3(f4(x8251,f1(f3(x8252,x8252))),f3(a2,a2)),f3(f4(f1(x8251),f3(x8252,x8252)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[818,718,822,2,3])).
% 70.94/70.92 cnf(827,plain,
% 70.94/70.92 (E(f3(f4(f1(x8271),f3(x8272,x8272)),f3(a2,a2)),f3(f4(x8271,f1(f3(x8272,x8272))),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[825,2])).
% 70.94/70.92 cnf(828,plain,
% 70.94/70.92 (E(f4(f1(f1(f3(x8281,x8281))),f1(x8282)),f3(a2,f4(f3(x8281,x8281),f1(x8282))))),
% 70.94/70.92 inference(scs_inference,[],[708,825,563,2,3])).
% 70.94/70.92 cnf(831,plain,
% 70.94/70.92 (E(f3(f3(a2,a2),f4(f3(x8311,x8311),f1(x8312))),f3(f4(x8311,f1(f3(x8312,x8312))),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[751,827,828,2,3])).
% 70.94/70.92 cnf(834,plain,
% 70.94/70.92 (E(f3(f4(x8341,f1(f3(x8342,x8342))),f3(a2,a2)),f4(f1(f3(x8341,x8341)),f1(f1(x8342))))),
% 70.94/70.92 inference(scs_inference,[],[815,571,831,2,3])).
% 70.94/70.92 cnf(837,plain,
% 70.94/70.92 (E(f4(f1(f3(x8371,x8371)),f1(f1(x8372))),f3(f4(x8371,f1(f3(x8372,x8372))),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[834,2])).
% 70.94/70.92 cnf(838,plain,
% 70.94/70.92 (E(f3(f4(f3(x8381,x8381),f1(x8382)),a2),f1(f4(f3(x8381,x8381),x8382)))),
% 70.94/70.92 inference(scs_inference,[],[590,650,834,2,3])).
% 70.94/70.92 cnf(840,plain,
% 70.94/70.92 (E(f1(f4(f3(x8401,x8401),x8402)),f3(f4(f3(x8401,x8401),f1(x8402)),a2))),
% 70.94/70.92 inference(scs_inference,[],[838,2])).
% 70.94/70.92 cnf(841,plain,
% 70.94/70.92 (E(f1(f4(f1(f3(x8411,x8411)),f1(x8412))),f3(f4(x8411,f1(f3(x8412,x8412))),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[18,837,838,2,3])).
% 70.94/70.92 cnf(844,plain,
% 70.94/70.92 (E(f3(f4(f1(x8441),f3(x8442,x8442)),f3(a2,a2)),f3(f4(f3(x8441,x8441),f1(x8442)),a2))),
% 70.94/70.92 inference(scs_inference,[],[730,840,841,2,3])).
% 70.94/70.92 cnf(846,plain,
% 70.94/70.92 (E(f3(f4(f3(x8461,x8461),f1(x8462)),a2),f3(f4(f1(x8461),f3(x8462,x8462)),f3(a2,a2)))),
% 70.94/70.92 inference(scs_inference,[],[844,2])).
% 70.94/70.92 cnf(1764,plain,
% 70.94/70.92 (~E(f3(x17641,f1(x17641)),f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))))),
% 70.94/70.92 inference(scs_inference,[],[846,111,8,4,6,5,7,2])).
% 70.94/70.92 cnf(2488,plain,
% 70.94/70.92 (~E(f3(x24881,f1(x24881)),f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))))),
% 70.94/70.92 inference(rename_variables,[],[1764])).
% 70.94/70.92 cnf(2489,plain,
% 70.94/70.92 ($false),
% 70.94/70.92 inference(scs_inference,[],[60,1764,2488,6,5]),
% 70.94/70.92 ['proof']).
% 70.94/70.92 % SZS output end Proof
% 70.94/70.92 % Total time :70.300000s
%------------------------------------------------------------------------------