%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP013-1 : 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 : n021.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 06:38:28 EDT 2024
% Result : Unsatisfiable 7.38s 7.41s
% Output : CNFRefutation 7.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GRP013-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 20 08:12:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.47/0.60 start to proof:theBenchmark
% 7.31/7.41 %-------------------------------------------
% 7.31/7.41 % File :CSE---1.7
% 7.31/7.41 % Problem :theBenchmark
% 7.31/7.41 % Transform :cnf
% 7.31/7.41 % Format :tptp:raw
% 7.31/7.41 % Command :java -jar mcs_scs.jar %d %s
% 7.31/7.41
% 7.31/7.41 % Result :Theorem 6.780000s
% 7.31/7.41 % Output :CNFRefutation 6.780000s
% 7.31/7.41 %-------------------------------------------
% 7.31/7.41 %--------------------------------------------------------------------------
% 7.31/7.41 % File : GRP013-1 : TPTP v8.2.0. Released v1.0.0.
% 7.31/7.41 % Domain : Group Theory
% 7.31/7.41 % Problem : Commutator equals identity in these conditions
% 7.31/7.41 % Version : [MOW76] axioms.
% 7.31/7.41 % English : If X.X=identity and if X^-1.Y^-1 = Z then X.Z = Y, then
% 7.31/7.41 % (X.Y).(X^-1.Y^-1) = identity.
% 7.31/7.41
% 7.31/7.41 % Refs : [Wos65] Wos (1965), Unpublished Note
% 7.31/7.41 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 7.31/7.41 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 7.31/7.41 % Source : [SPRFN]
% 7.31/7.41 % Names : Problem 11 [Wos65]
% 7.31/7.41 % : wos11 [WM76]
% 7.38/7.41
% 7.38/7.41 % Status : Unsatisfiable
% 7.38/7.41 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.00 v2.0.0
% 7.38/7.41 % Syntax : Number of clauses : 13 ( 9 unt; 0 nHn; 7 RR)
% 7.38/7.41 % Number of literals : 22 ( 1 equ; 10 neg)
% 7.38/7.41 % Maximal clause size : 4 ( 1 avg)
% 7.38/7.41 % Maximal term depth : 2 ( 1 avg)
% 7.38/7.41 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 7.38/7.41 % Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% 7.38/7.41 % Number of variables : 26 ( 0 sgn)
% 7.38/7.41 % SPC : CNF_UNS_RFO_SEQ_HRN
% 7.38/7.41
% 7.38/7.41 % Comments :
% 7.38/7.41 %--------------------------------------------------------------------------
% 7.38/7.41 %----Include group theory axioms
% 7.38/7.41 include('Axioms/GRP003-0.ax').
% 7.38/7.41 %--------------------------------------------------------------------------
% 7.38/7.41 cnf(squareness,hypothesis,
% 7.38/7.41 product(A,A,identity) ).
% 7.38/7.41
% 7.38/7.41 cnf(a_times_b_is_c,hypothesis,
% 7.38/7.41 product(a,b,c) ).
% 7.38/7.41
% 7.38/7.41 cnf(inverse_a_times_inverse_b_is_d,hypothesis,
% 7.38/7.41 product(inverse(a),inverse(b),d) ).
% 7.38/7.41
% 7.38/7.41 cnf(inverses_have_property,hypothesis,
% 7.38/7.41 ( ~ product(inverse(A),inverse(B),C)
% 7.38/7.41 | product(A,C,B) ) ).
% 7.38/7.41
% 7.38/7.41 cnf(prove_c_times_d_is_identity,negated_conjecture,
% 7.38/7.41 ~ product(c,d,identity) ).
% 7.38/7.41
% 7.38/7.41 %--------------------------------------------------------------------------
% 7.38/7.41 %-------------------------------------------
% 7.38/7.41 % Proof found
% 7.38/7.41 % SZS status Theorem for theBenchmark
% 7.38/7.41 % SZS output start Proof
% 7.38/7.42 %ClaNum:22(EqnAxiom:9)
% 7.38/7.42 %VarNum:52(SingletonVarNum:26)
% 7.38/7.42 %MaxLitNum:4
% 7.38/7.42 %MaxfuncDepth:1
% 7.38/7.42 %SharedTerms:10
% 7.38/7.42 %goalClause: 18
% 7.38/7.42 %singleGoalClaCount:1
% 7.38/7.42 [10]P1(a1,a2,a3)
% 7.38/7.42 [18]~P1(a3,a5,a4)
% 7.38/7.42 [16]P1(f6(a1),f6(a2),a5)
% 7.38/7.42 [11]P1(x111,x111,a4)
% 7.38/7.42 [12]P1(x121,a4,x121)
% 7.38/7.42 [13]P1(a4,x131,x131)
% 7.38/7.42 [14]P1(x141,f6(x141),a4)
% 7.38/7.42 [15]P1(f6(x151),x151,a4)
% 7.38/7.42 [17]P1(x171,x172,f7(x171,x172))
% 7.38/7.42 [19]P1(x191,x192,x193)+~P1(f6(x191),f6(x193),x192)
% 7.38/7.42 [20]~P1(x203,x204,x201)+E(x201,x202)+~P1(x203,x204,x202)
% 7.38/7.42 [21]~P1(x216,x214,x211)+P1(x211,x212,x213)+~P1(x214,x212,x215)+~P1(x216,x215,x213)
% 7.38/7.42 [22]~P1(x221,x226,x224)+P1(x221,x222,x223)+~P1(x224,x225,x223)+~P1(x226,x225,x222)
% 7.38/7.42 %EqnAxiom
% 7.38/7.42 [1]E(x11,x11)
% 7.38/7.42 [2]E(x22,x21)+~E(x21,x22)
% 7.38/7.42 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 7.38/7.42 [4]~E(x41,x42)+E(f6(x41),f6(x42))
% 7.38/7.42 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53))
% 7.38/7.42 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62))
% 7.38/7.42 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 7.38/7.42 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 7.38/7.42 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 7.38/7.42
% 7.38/7.42 %-------------------------------------------
% 7.38/7.42 cnf(23,plain,
% 7.38/7.42 (P1(x231,f7(f6(x231),f6(x232)),x232)),
% 7.38/7.42 inference(scs_inference,[],[17,19])).
% 7.38/7.42 cnf(24,plain,
% 7.38/7.42 (P1(x241,x242,f7(x241,x242))),
% 7.38/7.42 inference(rename_variables,[],[17])).
% 7.38/7.42 cnf(26,plain,
% 7.38/7.42 (~E(a5,a3)),
% 7.38/7.42 inference(scs_inference,[],[18,11,17,19,7])).
% 7.38/7.42 cnf(27,plain,
% 7.38/7.42 (P1(x271,x271,a4)),
% 7.38/7.42 inference(rename_variables,[],[11])).
% 7.38/7.42 cnf(28,plain,
% 7.38/7.42 (E(a4,f7(x281,x281))),
% 7.38/7.42 inference(scs_inference,[],[18,11,27,17,24,19,7,20])).
% 7.38/7.42 cnf(29,plain,
% 7.38/7.42 (P1(x291,x292,f7(x291,x292))),
% 7.38/7.42 inference(rename_variables,[],[17])).
% 7.38/7.42 cnf(32,plain,
% 7.38/7.42 (P1(x321,x321,a4)),
% 7.38/7.42 inference(rename_variables,[],[11])).
% 7.38/7.42 cnf(33,plain,
% 7.38/7.42 (P1(x331,x331,f7(a3,a3))),
% 7.38/7.42 inference(scs_inference,[],[18,11,27,32,17,24,19,7,20,8,9])).
% 7.38/7.42 cnf(34,plain,
% 7.38/7.42 (P1(a4,x341,f7(x341,a4))),
% 7.38/7.42 inference(scs_inference,[],[18,11,27,32,17,24,29,19,7,20,8,9,21])).
% 7.38/7.42 cnf(35,plain,
% 7.38/7.42 (P1(x351,x352,f7(x351,x352))),
% 7.38/7.42 inference(rename_variables,[],[17])).
% 7.38/7.42 cnf(37,plain,
% 7.38/7.42 (P1(a4,f7(a4,a4),a4)),
% 7.38/7.42 inference(scs_inference,[],[18,11,27,32,17,24,29,35,19,7,20,8,9,21,22])).
% 7.38/7.42 cnf(42,plain,
% 7.38/7.42 (E(f7(a3,a3),a4)),
% 7.38/7.42 inference(scs_inference,[],[18,11,27,32,17,24,29,35,19,7,20,8,9,21,22,2])).
% 7.38/7.42 cnf(43,plain,
% 7.38/7.42 (P1(x431,f7(a3,a3),x431)),
% 7.38/7.42 inference(scs_inference,[],[33,19])).
% 7.38/7.42 cnf(44,plain,
% 7.38/7.42 (P1(x441,x441,f7(a3,a3))),
% 7.38/7.42 inference(rename_variables,[],[33])).
% 7.38/7.42 cnf(46,plain,
% 7.38/7.42 (E(f7(x461,x461),a4)),
% 7.38/7.43 inference(scs_inference,[],[33,28,19,2])).
% 7.38/7.43 cnf(47,plain,
% 7.38/7.43 (E(f7(a3,a3),f7(x471,x471))),
% 7.38/7.43 inference(scs_inference,[],[33,42,28,19,2,3])).
% 7.38/7.43 cnf(50,plain,
% 7.38/7.43 (P1(a4,x501,f7(x501,a4))),
% 7.38/7.43 inference(rename_variables,[],[34])).
% 7.38/7.43 cnf(53,plain,
% 7.38/7.43 (P1(x531,f7(f6(x531),f6(x532)),x532)),
% 7.38/7.43 inference(rename_variables,[],[23])).
% 7.38/7.43 cnf(54,plain,
% 7.38/7.43 (P1(f7(x541,x541),x542,f7(x542,a4))),
% 7.38/7.43 inference(scs_inference,[],[18,23,34,50,33,44,42,28,19,2,3,20,8,7])).
% 7.38/7.43 cnf(57,plain,
% 7.38/7.43 (P1(x571,a4,x571)),
% 7.38/7.43 inference(rename_variables,[],[12])).
% 7.38/7.43 cnf(58,plain,
% 7.38/7.43 (P1(x581,f7(f6(x581),f6(x582)),x582)),
% 7.38/7.43 inference(rename_variables,[],[23])).
% 7.38/7.43 cnf(60,plain,
% 7.38/7.43 (P1(x601,f7(f6(x601),f6(a4)),f7(a4,a4))),
% 7.38/7.43 inference(scs_inference,[],[18,23,53,58,34,50,37,33,44,42,12,57,28,19,2,3,20,8,7,9,21,22])).
% 7.38/7.43 cnf(65,plain,
% 7.38/7.43 (P1(x651,a4,f6(x651))),
% 7.38/7.43 inference(scs_inference,[],[14,19])).
% 7.38/7.43 cnf(69,plain,
% 7.38/7.43 (E(f7(x691,x691),f7(f7(a3,a3),a4))),
% 7.38/7.43 inference(scs_inference,[],[43,54,47,14,19,2,20])).
% 7.38/7.43 cnf(71,plain,
% 7.38/7.43 (P1(x711,f7(a3,a3),x711)),
% 7.38/7.43 inference(rename_variables,[],[43])).
% 7.38/7.43 cnf(73,plain,
% 7.38/7.43 (E(f7(x731,x731),f7(x732,x732))),
% 7.38/7.43 inference(scs_inference,[],[43,54,47,46,14,28,19,2,20,3])).
% 7.38/7.43 cnf(74,plain,
% 7.38/7.43 (P1(f7(x741,x741),f7(a3,a3),f7(a3,a3))),
% 7.38/7.43 inference(scs_inference,[],[43,71,54,47,46,14,28,19,2,20,3,7])).
% 7.38/7.43 cnf(75,plain,
% 7.38/7.43 (P1(x751,f7(a3,a3),x751)),
% 7.38/7.43 inference(rename_variables,[],[43])).
% 7.38/7.43 cnf(76,plain,
% 7.38/7.43 (P1(x761,f7(x762,x762),x761)),
% 7.38/7.43 inference(scs_inference,[],[43,71,75,54,47,46,14,28,19,2,20,3,7,8])).
% 7.38/7.43 cnf(78,plain,
% 7.38/7.43 (P1(x781,f7(a3,a3),x781)),
% 7.38/7.43 inference(rename_variables,[],[43])).
% 7.38/7.43 cnf(79,plain,
% 7.38/7.43 (~P1(f7(a3,a3),a5,f7(f6(a3),f6(a4)))),
% 7.38/7.43 inference(scs_inference,[],[18,43,71,75,78,23,54,47,46,14,28,19,2,20,3,7,8,9,21])).
% 7.38/7.43 cnf(81,plain,
% 7.38/7.43 (P1(x811,f7(a3,a3),x811)),
% 7.38/7.43 inference(rename_variables,[],[43])).
% 7.38/7.43 cnf(83,plain,
% 7.38/7.43 (P1(f7(a3,a3),f7(a4,a4),f7(a4,a4))),
% 7.38/7.43 inference(scs_inference,[],[18,43,71,75,78,81,23,60,54,47,46,14,28,19,2,20,3,7,8,9,21,22])).
% 7.38/7.43 cnf(87,plain,
% 7.38/7.43 (P1(f6(x871),a4,x871)),
% 7.38/7.43 inference(scs_inference,[],[15,19])).
% 7.38/7.43 cnf(90,plain,
% 7.38/7.43 (E(f7(f7(a3,a3),a4),f7(x901,x901))),
% 7.38/7.43 inference(scs_inference,[],[69,15,19,2])).
% 7.38/7.43 cnf(91,plain,
% 7.38/7.43 (E(f6(f7(x911,x911)),f7(a4,a4))),
% 7.38/7.43 inference(scs_inference,[],[65,54,69,15,19,2,20])).
% 7.38/7.43 cnf(93,plain,
% 7.38/7.43 (P1(x931,a4,f6(x931))),
% 7.38/7.43 inference(rename_variables,[],[65])).
% 7.38/7.43 cnf(95,plain,
% 7.38/7.43 (P1(x951,f7(x952,x952),f6(x951))),
% 7.38/7.43 inference(scs_inference,[],[65,93,54,69,15,28,19,2,20,8])).
% 7.38/7.43 cnf(96,plain,
% 7.38/7.43 (P1(f7(x961,x961),a4,f6(f7(x962,x962)))),
% 7.38/7.43 inference(scs_inference,[],[65,93,54,73,69,15,28,19,2,20,8,7])).
% 7.38/7.43 cnf(97,plain,
% 7.38/7.43 (P1(x971,a4,f6(x971))),
% 7.38/7.43 inference(rename_variables,[],[65])).
% 7.38/7.43 cnf(100,plain,
% 7.38/7.43 (~P1(f6(a3),f7(f6(a4),f6(a5)),a4)),
% 7.38/7.43 inference(scs_inference,[],[18,65,93,97,23,83,54,73,69,15,28,19,2,20,8,7,9,22])).
% 7.38/7.43 cnf(101,plain,
% 7.38/7.43 (P1(x1011,f7(f6(x1011),f6(x1012)),x1012)),
% 7.38/7.43 inference(rename_variables,[],[23])).
% 7.38/7.43 cnf(102,plain,
% 7.38/7.43 (P1(x1021,a4,f6(x1021))),
% 7.38/7.43 inference(rename_variables,[],[65])).
% 7.38/7.43 cnf(104,plain,
% 7.38/7.43 (P1(f6(x1041),f7(f6(a4),f6(x1041)),f7(a3,a3))),
% 7.38/7.43 inference(scs_inference,[],[18,65,93,97,102,23,101,83,54,73,69,15,33,28,19,2,20,8,7,9,22,21])).
% 7.38/7.43 cnf(111,plain,
% 7.38/7.43 (P1(a1,a5,a2)),
% 7.38/7.43 inference(scs_inference,[],[16,19])).
% 7.38/7.43 cnf(113,plain,
% 7.38/7.43 (E(f7(a4,a4),f6(f7(x1131,x1131)))),
% 7.38/7.43 inference(scs_inference,[],[91,16,19,2])).
% 7.38/7.43 cnf(114,plain,
% 7.38/7.43 (E(x1141,f6(f6(x1141)))),
% 7.38/7.43 inference(scs_inference,[],[87,65,91,16,19,2,20])).
% 7.38/7.43 cnf(115,plain,
% 7.38/7.43 (P1(x1151,a4,f6(x1151))),
% 7.38/7.43 inference(rename_variables,[],[65])).
% 7.38/7.43 cnf(117,plain,
% 7.38/7.43 (E(f6(f7(x1171,x1171)),a4)),
% 7.38/7.43 inference(scs_inference,[],[87,65,91,16,46,19,2,20,3])).
% 7.38/7.43 cnf(122,plain,
% 7.38/7.43 (P1(f7(a4,a4),a4,f7(x1221,x1221))),
% 7.38/7.43 inference(scs_inference,[],[87,65,34,91,90,16,46,28,19,2,20,3,8,9,7])).
% 7.38/7.43 cnf(123,plain,
% 7.38/7.43 (P1(f6(x1231),a4,x1231)),
% 7.38/7.43 inference(rename_variables,[],[87])).
% 7.38/7.43 cnf(124,plain,
% 7.38/7.43 (P1(f6(a4),f6(a4),f6(a4))),
% 7.38/7.43 inference(scs_inference,[],[87,123,65,115,34,91,90,16,46,28,19,2,20,3,8,9,7,22])).
% 7.38/7.43 cnf(126,plain,
% 7.38/7.43 (P1(f6(x1261),a4,x1261)),
% 7.38/7.43 inference(rename_variables,[],[87])).
% 7.38/7.43 cnf(128,plain,
% 7.38/7.43 (~P1(a4,a5,f6(a3))),
% 7.38/7.43 inference(scs_inference,[],[18,87,123,126,65,115,34,91,90,16,11,46,28,19,2,20,3,8,9,7,22,21])).
% 7.38/7.43 cnf(132,plain,
% 7.38/7.43 (E(f6(f6(x1321)),x1321)),
% 7.38/7.43 inference(scs_inference,[],[114,2])).
% 7.38/7.43 cnf(133,plain,
% 7.38/7.43 (E(f6(a4),f7(a4,a4))),
% 7.38/7.43 inference(scs_inference,[],[65,34,114,2,20])).
% 7.38/7.43 cnf(135,plain,
% 7.38/7.43 (P1(x1351,a4,f6(x1351))),
% 7.38/7.43 inference(rename_variables,[],[65])).
% 7.38/7.43 cnf(137,plain,
% 7.38/7.43 (E(f7(f7(a3,a3),a4),a4)),
% 7.38/7.43 inference(scs_inference,[],[65,34,114,90,46,2,20,3])).
% 7.38/7.43 cnf(140,plain,
% 7.38/7.43 (E(x1401,f6(f6(x1401)))),
% 7.38/7.43 inference(rename_variables,[],[114])).
% 7.38/7.43 cnf(142,plain,
% 7.38/7.43 (E(x1421,f6(f6(x1421)))),
% 7.38/7.43 inference(rename_variables,[],[114])).
% 7.38/7.43 cnf(143,plain,
% 7.38/7.43 (P1(f6(f6(a1)),a5,a2)),
% 7.38/7.43 inference(scs_inference,[],[111,65,34,114,140,142,90,46,2,20,3,9,8,7])).
% 7.38/7.43 cnf(145,plain,
% 7.38/7.43 (P1(f7(x1451,x1451),a2,f7(f7(a1,a4),a5))),
% 7.38/7.43 inference(scs_inference,[],[111,65,54,34,114,140,142,90,17,46,2,20,3,9,8,7,22])).
% 7.38/7.43 cnf(149,plain,
% 7.38/7.43 (P1(a2,f7(f6(a5),f6(a4)),f6(a1))),
% 7.38/7.43 inference(scs_inference,[],[111,65,135,23,54,34,114,140,142,90,17,46,2,20,3,9,8,7,22,21])).
% 7.38/7.43 cnf(154,plain,
% 7.38/7.43 (E(x1541,f6(x1541))),
% 7.38/7.43 inference(scs_inference,[],[23,95,133,2,20])).
% 7.38/7.43 cnf(158,plain,
% 7.38/7.43 (~E(a5,f6(f6(a3)))),
% 7.38/7.43 inference(scs_inference,[],[23,26,95,132,133,2,20,3])).
% 7.38/7.43 cnf(164,plain,
% 7.38/7.43 (P1(x1641,f6(f6(a4)),f6(x1641))),
% 7.38/7.43 inference(scs_inference,[],[65,23,74,96,26,95,132,113,133,117,114,2,20,3,9,7,8])).
% 7.38/7.43 cnf(166,plain,
% 7.38/7.43 (P1(f6(a4),f7(a3,a3),f7(a3,a3))),
% 7.38/7.43 inference(scs_inference,[],[65,23,104,74,96,124,26,95,132,113,133,117,114,2,20,3,9,7,8,22])).
% 7.38/7.43 cnf(169,plain,
% 7.38/7.43 (~P1(a4,f7(f6(a4),f6(a5)),f6(a3))),
% 7.38/7.43 inference(scs_inference,[],[65,23,104,74,96,124,100,26,95,132,113,133,117,14,114,2,20,3,9,7,8,22,21])).
% 7.38/7.43 cnf(173,plain,
% 7.38/7.43 (P1(x1731,f6(f6(x1731)),f6(a4))),
% 7.38/7.43 inference(scs_inference,[],[164,19])).
% 7.38/7.43 cnf(176,plain,
% 7.38/7.43 (E(f6(x1761),x1761)),
% 7.38/7.43 inference(scs_inference,[],[154,164,19,2])).
% 7.38/7.43 cnf(177,plain,
% 7.38/7.43 (E(x1771,f7(f6(a4),f6(x1771)))),
% 7.38/7.43 inference(scs_inference,[],[23,154,164,13,19,2,20])).
% 7.38/7.43 cnf(179,plain,
% 7.38/7.43 (P1(x1791,f7(f6(x1791),f6(x1792)),x1792)),
% 7.38/7.43 inference(rename_variables,[],[23])).
% 7.38/7.43 cnf(181,plain,
% 7.38/7.43 (~E(a5,f6(a3))),
% 7.38/7.43 inference(scs_inference,[],[23,154,164,13,158,19,2,20,3])).
% 7.38/7.43 cnf(182,plain,
% 7.38/7.43 (E(x1821,f6(x1821))),
% 7.38/7.43 inference(rename_variables,[],[154])).
% 7.38/7.43 cnf(184,plain,
% 7.38/7.43 (E(x1841,f6(x1841))),
% 7.38/7.43 inference(rename_variables,[],[154])).
% 7.38/7.43 cnf(186,plain,
% 7.38/7.43 (E(x1861,f6(x1861))),
% 7.38/7.43 inference(rename_variables,[],[154])).
% 7.38/7.43 cnf(189,plain,
% 7.38/7.43 (P1(f7(x1891,x1891),f7(f7(a1,a4),a5),f7(a2,a4))),
% 7.38/7.43 inference(scs_inference,[],[87,23,179,111,145,54,154,182,184,186,164,13,158,19,2,20,3,9,8,7,22])).
% 7.38/7.43 cnf(194,plain,
% 7.38/7.43 (~P1(a4,a5,a3)),
% 7.38/7.43 inference(scs_inference,[],[18,87,23,179,111,145,54,154,182,184,186,164,13,158,15,19,2,20,3,9,8,7,22,21])).
% 7.38/7.43 cnf(198,plain,
% 7.38/7.43 (P1(x1981,f6(a4),f6(f6(x1981)))),
% 7.38/7.43 inference(scs_inference,[],[173,19])).
% 7.38/7.43 cnf(199,plain,
% 7.38/7.43 (P1(x1991,f6(f6(x1991)),f6(a4))),
% 7.38/7.43 inference(rename_variables,[],[173])).
% 7.38/7.43 cnf(201,plain,
% 7.38/7.43 (E(f7(f6(a4),f6(x2011)),x2011)),
% 7.38/7.43 inference(scs_inference,[],[173,177,19,2])).
% 7.38/7.43 cnf(202,plain,
% 7.38/7.43 (E(f6(a4),f7(a3,a3))),
% 7.38/7.43 inference(scs_inference,[],[173,65,177,33,19,2,20])).
% 7.38/7.43 cnf(204,plain,
% 7.38/7.43 (P1(x2041,a4,f6(x2041))),
% 7.38/7.43 inference(rename_variables,[],[65])).
% 7.38/7.43 cnf(206,plain,
% 7.38/7.43 (E(f6(x2061),f7(f6(a4),f6(x2061)))),
% 7.38/7.43 inference(scs_inference,[],[173,65,176,177,33,19,2,20,3])).
% 7.38/7.43 cnf(209,plain,
% 7.38/7.43 (E(f6(x2091),x2091)),
% 7.38/7.43 inference(rename_variables,[],[176])).
% 7.38/7.43 cnf(210,plain,
% 7.38/7.43 (P1(x2101,f6(x2101),f6(a4))),
% 7.38/7.43 inference(scs_inference,[],[173,199,65,176,209,177,33,19,2,20,3,9,8])).
% 7.38/7.43 cnf(211,plain,
% 7.38/7.43 (E(f6(x2111),x2111)),
% 7.38/7.43 inference(rename_variables,[],[176])).
% 7.38/7.43 cnf(214,plain,
% 7.38/7.43 (P1(a4,a2,f7(f7(a1,a4),a5))),
% 7.38/7.43 inference(scs_inference,[],[173,199,65,204,111,34,176,209,211,177,33,17,19,2,20,3,9,8,7,22])).
% 7.38/7.43 cnf(218,plain,
% 7.38/7.43 (P1(x2181,f6(a4),f6(x2181))),
% 7.38/7.43 inference(scs_inference,[],[210,19])).
% 7.38/7.43 cnf(221,plain,
% 7.38/7.43 (E(f7(f6(a4),f6(x2211)),f6(x2211))),
% 7.38/7.43 inference(scs_inference,[],[206,210,19,2])).
% 7.38/7.43 cnf(228,plain,
% 7.38/7.43 (P1(f7(f6(a4),f6(x2281)),a4,x2281)),
% 7.38/7.43 inference(scs_inference,[],[65,87,111,26,201,206,210,154,19,2,3,8,9,7])).
% 7.38/7.43 cnf(233,plain,
% 7.38/7.43 (P1(f6(f6(a4)),f6(x2331),x2331)),
% 7.38/7.43 inference(scs_inference,[],[198,23,65,87,111,166,26,76,201,206,210,154,17,19,2,3,8,9,7,22,21])).
% 7.38/7.43 cnf(238,plain,
% 7.38/7.43 (P1(f6(a4),x2381,x2381)),
% 7.38/7.43 inference(scs_inference,[],[233,19])).
% 7.38/7.43 cnf(241,plain,
% 7.38/7.43 (E(f6(a4),f7(f6(a4),a4))),
% 7.38/7.43 inference(scs_inference,[],[218,233,34,202,19,2,20])).
% 7.38/7.43 cnf(243,plain,
% 7.38/7.43 (P1(x2431,f6(a4),f6(x2431))),
% 7.38/7.43 inference(rename_variables,[],[218])).
% 7.38/7.43 cnf(245,plain,
% 7.38/7.43 (E(f6(a4),f7(f7(a3,a3),a4))),
% 7.38/7.43 inference(scs_inference,[],[218,233,34,202,69,19,2,20,3])).
% 7.38/7.43 cnf(247,plain,
% 7.38/7.43 (P1(x2471,x2471,f6(a4))),
% 7.38/7.43 inference(scs_inference,[],[218,173,233,34,202,132,69,19,2,20,3,8])).
% 7.38/7.43 cnf(249,plain,
% 7.38/7.43 (P1(f7(f6(a4),f6(a1)),a5,a2)),
% 7.38/7.43 inference(scs_inference,[],[218,173,111,233,34,202,132,69,177,19,2,20,3,8,7])).
% 7.38/7.43 cnf(252,plain,
% 7.38/7.43 (P1(x2521,f6(a4),f6(x2521))),
% 7.38/7.43 inference(rename_variables,[],[218])).
% 7.38/7.43 cnf(253,plain,
% 7.38/7.43 (P1(a2,f7(f7(a1,a4),a5),a4)),
% 7.38/7.43 inference(scs_inference,[],[218,243,173,65,111,233,214,34,202,132,69,177,15,19,2,20,3,8,7,9,22])).
% 7.38/7.43 cnf(257,plain,
% 7.38/7.43 (~P1(f6(a4),f7(f6(a4),f6(a5)),a3)),
% 7.38/7.43 inference(scs_inference,[],[218,243,252,173,65,111,233,214,100,34,202,132,69,177,11,15,19,2,20,3,8,7,9,22,21])).
% 7.38/7.43 cnf(261,plain,
% 7.38/7.43 (P1(a4,f6(x2611),x2611)),
% 7.38/7.43 inference(scs_inference,[],[238,19])).
% 7.38/7.43 cnf(262,plain,
% 7.38/7.43 (P1(f6(a4),x2621,x2621)),
% 7.38/7.43 inference(rename_variables,[],[238])).
% 7.38/7.43 cnf(264,plain,
% 7.38/7.43 (E(f7(f6(a4),a4),f6(a4))),
% 7.38/7.43 inference(scs_inference,[],[238,241,19,2])).
% 7.38/7.43 cnf(265,plain,
% 7.38/7.43 (E(f7(x2651,x2651),f6(a4))),
% 7.38/7.43 inference(scs_inference,[],[238,262,241,76,19,2,20])).
% 7.38/7.43 cnf(267,plain,
% 7.38/7.43 (P1(f6(a4),x2671,x2671)),
% 7.38/7.43 inference(rename_variables,[],[238])).
% 7.38/7.43 cnf(269,plain,
% 7.38/7.43 (E(f6(a4),f7(x2691,x2691))),
% 7.38/7.43 inference(scs_inference,[],[238,262,241,245,76,90,19,2,20,3])).
% 7.38/7.43 cnf(271,plain,
% 7.38/7.43 (P1(f6(a4),x2711,x2711)),
% 7.38/7.43 inference(rename_variables,[],[238])).
% 7.38/7.43 cnf(272,plain,
% 7.38/7.43 (P1(f7(f6(a4),a4),x2721,x2721)),
% 7.38/7.43 inference(scs_inference,[],[238,262,267,271,257,241,245,76,90,19,2,20,3,8,7])).
% 7.38/7.43 cnf(274,plain,
% 7.38/7.43 (P1(f6(a4),x2741,x2741)),
% 7.38/7.43 inference(rename_variables,[],[238])).
% 7.38/7.43 cnf(275,plain,
% 7.38/7.43 (P1(f6(a4),f6(f6(x2751)),x2751)),
% 7.38/7.43 inference(scs_inference,[],[238,262,267,271,274,87,65,257,241,245,76,90,19,2,20,3,8,7,9,22])).
% 7.38/7.43 cnf(277,plain,
% 7.38/7.43 (P1(f6(a4),x2771,x2771)),
% 7.38/7.43 inference(rename_variables,[],[238])).
% 7.38/7.43 cnf(279,plain,
% 7.38/7.43 (P1(f6(f7(x2791,x2791)),x2792,f7(x2792,a4))),
% 7.38/7.43 inference(scs_inference,[],[238,262,267,271,274,277,218,87,65,257,54,241,245,76,90,19,2,20,3,8,7,9,22,21])).
% 7.38/7.43 cnf(283,plain,
% 7.38/7.43 (P1(f7(x2831,x2831),f7(f6(x2832),a4),x2832)),
% 7.38/7.43 inference(scs_inference,[],[279,19])).
% 7.38/7.43 cnf(286,plain,
% 7.38/7.43 (E(a4,f7(f7(a3,a3),a4))),
% 7.38/7.43 inference(scs_inference,[],[279,137,19,2])).
% 7.38/7.43 cnf(287,plain,
% 7.38/7.43 (E(x2871,f7(f6(x2871),a4))),
% 7.38/7.43 inference(scs_inference,[],[261,279,34,137,19,2,20])).
% 7.38/7.43 cnf(290,plain,
% 7.38/7.43 (E(f6(a4),f6(f7(x2901,x2901)))),
% 7.38/7.43 inference(scs_inference,[],[261,279,34,269,137,113,19,2,20,3])).
% 7.38/7.43 cnf(291,plain,
% 7.38/7.43 (E(f6(a4),f7(x2911,x2911))),
% 7.38/7.43 inference(rename_variables,[],[269])).
% 7.38/7.43 cnf(292,plain,
% 7.38/7.43 (P1(f6(a4),f6(x2921),x2921)),
% 7.38/7.43 inference(scs_inference,[],[261,279,34,269,137,113,154,19,2,20,3,7])).
% 7.38/7.43 cnf(296,plain,
% 7.38/7.43 (~P1(f7(f6(a4),f6(a5)),a4,f6(a3))),
% 7.38/7.43 inference(scs_inference,[],[261,173,198,87,279,169,34,269,291,137,113,154,19,2,20,3,7,8,9,22])).
% 7.38/7.43 cnf(298,plain,
% 7.38/7.43 (P1(a4,f6(x2981),x2981)),
% 7.38/7.43 inference(rename_variables,[],[261])).
% 7.38/7.43 cnf(300,plain,
% 7.38/7.43 (~P1(f6(a3),a5,f7(f6(a4),f6(a4)))),
% 7.38/7.43 inference(scs_inference,[],[18,261,298,173,198,23,87,279,169,34,269,291,137,113,154,19,2,20,3,7,8,9,22,21])).
% 7.38/7.43 cnf(304,plain,
% 7.38/7.43 (P1(a4,x3041,f6(x3041))),
% 7.38/7.43 inference(scs_inference,[],[275,19])).
% 7.38/7.43 cnf(306,plain,
% 7.38/7.43 (E(f7(f6(x3061),a4),x3061)),
% 7.38/7.43 inference(scs_inference,[],[275,287,19,2])).
% 7.38/7.43 cnf(307,plain,
% 7.38/7.43 (E(f7(x3071,x3071),f6(f6(a4)))),
% 7.38/7.43 inference(scs_inference,[],[238,275,287,95,19,2,20])).
% 7.38/7.43 cnf(312,plain,
% 7.38/7.43 (P1(x3121,f6(f7(x3122,x3122)),f6(x3121))),
% 7.38/7.43 inference(scs_inference,[],[238,218,275,26,287,290,95,19,2,20,3,8])).
% 7.38/7.43 cnf(314,plain,
% 7.38/7.43 (P1(f7(x3141,x3141),f7(f6(x3142),a4),x3142)),
% 7.38/7.43 inference(rename_variables,[],[283])).
% 7.38/7.43 cnf(317,plain,
% 7.38/7.43 (P1(x3171,f6(a4),f6(x3171))),
% 7.38/7.43 inference(rename_variables,[],[218])).
% 7.38/7.43 cnf(318,plain,
% 7.38/7.43 (~P1(a4,a5,f7(f6(a3),f6(a4)))),
% 7.38/7.43 inference(scs_inference,[],[283,314,238,218,272,275,79,26,221,287,290,95,19,2,20,3,8,7,9,22])).
% 7.38/7.43 cnf(322,plain,
% 7.38/7.43 (~P1(f6(a4),f7(f6(a4),f6(a5)),f6(a3))),
% 7.38/7.43 inference(scs_inference,[],[283,314,238,218,317,261,272,275,79,257,26,221,287,290,95,19,2,20,3,8,7,9,22,21])).
% 7.38/7.43 cnf(326,plain,
% 7.38/7.43 (P1(x3261,f6(a4),x3261)),
% 7.38/7.43 inference(scs_inference,[],[247,19])).
% 7.38/7.43 cnf(329,plain,
% 7.38/7.43 (E(f6(f6(a4)),f7(x3291,x3291))),
% 7.38/7.43 inference(scs_inference,[],[307,247,19,2])).
% 7.38/7.44 cnf(330,plain,
% 7.38/7.44 (E(f6(x3301),f7(x3301,a4))),
% 7.38/7.44 inference(scs_inference,[],[304,34,307,247,19,2,20])).
% 7.38/7.44 cnf(333,plain,
% 7.38/7.44 (E(f7(f6(a4),a4),f7(x3331,x3331))),
% 7.38/7.44 inference(scs_inference,[],[304,34,306,307,247,28,19,2,20,3])).
% 7.38/7.44 cnf(335,plain,
% 7.38/7.44 (P1(f7(f7(a3,a3),a4),x3351,f6(x3351))),
% 7.38/7.44 inference(scs_inference,[],[304,34,306,307,247,286,28,19,2,20,3,7])).
% 7.38/7.44 cnf(337,plain,
% 7.38/7.44 (P1(f6(a4),x3371,x3371)),
% 7.38/7.44 inference(rename_variables,[],[238])).
% 7.38/7.44 cnf(338,plain,
% 7.38/7.44 (~E(f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[304,238,322,128,34,306,307,247,286,28,19,2,20,3,7,8,9])).
% 7.38/7.44 cnf(339,plain,
% 7.38/7.44 (P1(a4,x3391,f6(x3391))),
% 7.38/7.44 inference(rename_variables,[],[304])).
% 7.38/7.44 cnf(341,plain,
% 7.38/7.44 (P1(f6(a4),x3411,x3411)),
% 7.38/7.44 inference(rename_variables,[],[238])).
% 7.38/7.44 cnf(344,plain,
% 7.38/7.44 (~P1(a3,a5,f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[18,304,339,238,337,341,322,292,128,34,306,307,247,286,28,19,2,20,3,7,8,9,22,21])).
% 7.38/7.44 cnf(348,plain,
% 7.38/7.44 (E(f7(x3481,x3481),f7(f6(a4),a4))),
% 7.38/7.44 inference(scs_inference,[],[333,2])).
% 7.38/7.44 cnf(349,plain,
% 7.38/7.44 (E(x3491,f7(x3491,f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[326,333,17,2,20])).
% 7.38/7.44 cnf(352,plain,
% 7.38/7.44 (E(f7(x3521,x3521),f6(f7(x3522,x3522)))),
% 7.38/7.44 inference(scs_inference,[],[326,333,265,290,17,2,20,3])).
% 7.38/7.44 cnf(354,plain,
% 7.38/7.44 (P1(x3541,f6(f6(x3541)),f6(a4))),
% 7.38/7.44 inference(rename_variables,[],[173])).
% 7.38/7.44 cnf(356,plain,
% 7.38/7.44 (P1(x3561,f6(a4),x3561)),
% 7.38/7.44 inference(rename_variables,[],[326])).
% 7.38/7.44 cnf(357,plain,
% 7.38/7.44 (P1(f7(a4,a4),x3571,x3571)),
% 7.38/7.44 inference(scs_inference,[],[326,173,238,344,333,330,265,290,17,2,20,3,8,9,7])).
% 7.38/7.44 cnf(359,plain,
% 7.38/7.44 (~P1(f6(a4),a5,f6(f6(a3)))),
% 7.38/7.44 inference(scs_inference,[],[326,356,173,354,238,344,333,330,265,290,17,2,20,3,8,9,7,21])).
% 7.38/7.44 cnf(360,plain,
% 7.38/7.44 (P1(x3601,f6(f6(x3601)),f6(a4))),
% 7.38/7.44 inference(rename_variables,[],[173])).
% 7.38/7.44 cnf(363,plain,
% 7.38/7.44 (P1(a1,a2,a5)),
% 7.38/7.44 inference(scs_inference,[],[326,356,173,354,360,238,143,344,333,330,265,290,17,2,20,3,8,9,7,21,22])).
% 7.38/7.44 cnf(368,plain,
% 7.38/7.44 (E(f7(x3681,f6(a4)),x3681)),
% 7.38/7.44 inference(scs_inference,[],[349,2])).
% 7.38/7.44 cnf(369,plain,
% 7.38/7.44 (E(f6(f7(x3691,x3691)),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[304,349,95,2,20])).
% 7.38/7.44 cnf(371,plain,
% 7.38/7.44 (P1(a4,x3711,f6(x3711))),
% 7.38/7.44 inference(rename_variables,[],[304])).
% 7.38/7.44 cnf(375,plain,
% 7.38/7.44 (P1(a4,f6(x3751),x3751)),
% 7.38/7.44 inference(rename_variables,[],[261])).
% 7.38/7.44 cnf(376,plain,
% 7.38/7.44 (P1(f7(f6(a4),a4),x3761,f6(x3761))),
% 7.38/7.44 inference(scs_inference,[],[304,371,261,194,26,349,287,95,2,20,3,8,7])).
% 7.38/7.44 cnf(380,plain,
% 7.38/7.44 (~P1(f6(a4),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[326,198,304,371,261,375,194,26,349,329,287,95,2,20,3,8,7,9,21])).
% 7.38/7.44 cnf(381,plain,
% 7.38/7.44 (P1(a4,f6(x3811),x3811)),
% 7.38/7.44 inference(rename_variables,[],[261])).
% 7.38/7.44 cnf(384,plain,
% 7.38/7.44 (~P1(f6(a4),f6(a5),a3)),
% 7.38/7.44 inference(scs_inference,[],[326,198,304,371,261,375,381,194,26,349,329,287,95,2,20,3,8,7,9,21,22])).
% 7.38/7.44 cnf(388,plain,
% 7.38/7.44 (E(f6(f7(x3881,x3881)),f7(x3882,x3882))),
% 7.38/7.44 inference(scs_inference,[],[352,2])).
% 7.38/7.44 cnf(389,plain,
% 7.38/7.44 (E(f7(f7(x3891,x3891),f6(a4)),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[368,352,265,2,3])).
% 7.38/7.44 cnf(391,plain,
% 7.38/7.44 (~E(a3,f6(a5))),
% 7.38/7.44 inference(scs_inference,[],[238,384,368,352,265,2,3,8])).
% 7.38/7.44 cnf(394,plain,
% 7.38/7.44 (P1(x3941,f6(a4),f6(x3941))),
% 7.38/7.44 inference(rename_variables,[],[218])).
% 7.38/7.44 cnf(395,plain,
% 7.38/7.44 (P1(f7(a4,f6(a4)),x3951,f6(x3951))),
% 7.38/7.44 inference(scs_inference,[],[218,304,238,384,368,369,352,349,265,2,3,8,9,7])).
% 7.38/7.44 cnf(399,plain,
% 7.38/7.44 (P1(f7(x3991,x3991),f7(f6(x3992),a4),x3992)),
% 7.38/7.44 inference(rename_variables,[],[283])).
% 7.38/7.44 cnf(401,plain,
% 7.38/7.44 (P1(f7(x4011,x4011),f7(f6(x4012),a4),f6(x4012))),
% 7.38/7.44 inference(scs_inference,[],[18,283,399,326,218,394,304,238,357,384,368,369,352,349,265,2,3,8,9,7,21,22])).
% 7.38/7.44 cnf(405,plain,
% 7.38/7.44 (E(f6(a4),f7(f7(x4051,x4051),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[389,2])).
% 7.38/7.44 cnf(408,plain,
% 7.38/7.44 (P1(f6(f7(x4081,x4081)),f6(a4),f7(x4082,x4082))),
% 7.38/7.44 inference(scs_inference,[],[326,111,388,389,349,2,8,9])).
% 7.38/7.44 cnf(409,plain,
% 7.38/7.44 (P1(x4091,f6(a4),x4091)),
% 7.38/7.44 inference(rename_variables,[],[326])).
% 7.38/7.44 cnf(412,plain,
% 7.38/7.44 (~P1(f7(f6(a3),a4),a5,f7(x4121,x4121))),
% 7.38/7.44 inference(scs_inference,[],[283,326,409,111,344,388,389,247,349,2,8,9,7,21])).
% 7.38/7.44 cnf(416,plain,
% 7.38/7.44 (~P1(f6(a4),f6(a5),f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[283,326,409,261,304,111,318,344,388,389,247,349,2,8,9,7,21,22])).
% 7.38/7.44 cnf(420,plain,
% 7.38/7.44 (P1(f7(x4201,x4201),f7(x4202,x4202),a4)),
% 7.38/7.44 inference(scs_inference,[],[408,19])).
% 7.38/7.44 cnf(422,plain,
% 7.38/7.44 (E(f7(x4221,a4),f6(x4221))),
% 7.38/7.44 inference(scs_inference,[],[408,330,19,2])).
% 7.38/7.44 cnf(423,plain,
% 7.38/7.44 (~E(a5,f7(a3,a4))),
% 7.38/7.44 inference(scs_inference,[],[181,408,330,19,2,3])).
% 7.38/7.44 cnf(427,plain,
% 7.38/7.44 (P1(f7(f7(x4271,x4271),f6(a4)),x4272,x4272)),
% 7.38/7.44 inference(scs_inference,[],[218,238,181,408,405,330,19,2,3,8,9,7])).
% 7.38/7.44 cnf(433,plain,
% 7.38/7.44 (E(a4,f7(f7(x4331,x4331),a4))),
% 7.38/7.44 inference(scs_inference,[],[420,54,245,2,20])).
% 7.38/7.44 cnf(440,plain,
% 7.38/7.44 (P1(f7(f6(a4),a4),f7(x4401,x4401),a4)),
% 7.38/7.44 inference(scs_inference,[],[420,326,54,348,422,338,245,286,2,20,3,8,9,7])).
% 7.38/7.44 cnf(441,plain,
% 7.38/7.44 (P1(f7(x4411,x4411),f7(x4412,x4412),a4)),
% 7.38/7.44 inference(rename_variables,[],[420])).
% 7.38/7.44 cnf(442,plain,
% 7.38/7.44 (~P1(f7(x4421,x4421),f7(f6(a4),f6(a5)),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[420,441,326,357,169,54,348,422,338,245,286,2,20,3,8,9,7,21])).
% 7.38/7.44 cnf(444,plain,
% 7.38/7.44 (P1(f7(x4441,x4441),f7(x4442,x4442),a4)),
% 7.38/7.44 inference(rename_variables,[],[420])).
% 7.38/7.44 cnf(446,plain,
% 7.38/7.44 (P1(f7(x4461,x4461),f7(x4462,x4462),f6(f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[420,441,444,326,198,357,169,54,348,422,338,245,286,2,20,3,8,9,7,21,22])).
% 7.38/7.44 cnf(450,plain,
% 7.38/7.44 (E(f7(f7(x4501,x4501),a4),a4)),
% 7.38/7.44 inference(scs_inference,[],[433,2])).
% 7.38/7.44 cnf(451,plain,
% 7.38/7.44 (E(a4,f6(f7(x4511,x4511)))),
% 7.38/7.44 inference(scs_inference,[],[420,433,95,2,20])).
% 7.38/7.44 cnf(456,plain,
% 7.38/7.44 (~E(f7(f6(a3),f6(a4)),f6(a5))),
% 7.38/7.44 inference(scs_inference,[],[420,238,416,433,391,422,95,2,20,3,8])).
% 7.38/7.44 cnf(458,plain,
% 7.38/7.44 (P1(f7(f7(x4581,x4581),a4),f6(x4582),x4582)),
% 7.38/7.44 inference(scs_inference,[],[420,261,238,416,433,391,422,95,2,20,3,8,7])).
% 7.38/7.44 cnf(460,plain,
% 7.38/7.44 (P1(a4,a2,f7(f6(a1),a5))),
% 7.38/7.44 inference(scs_inference,[],[420,261,304,238,111,416,433,391,422,95,17,2,20,3,8,7,9,22])).
% 7.38/7.44 cnf(468,plain,
% 7.38/7.44 (P1(f6(a4),f6(a4),f7(f6(a4),a4))),
% 7.38/7.44 inference(scs_inference,[],[420,326,87,264,456,451,422,3,8,9,7])).
% 7.38/7.44 cnf(470,plain,
% 7.38/7.44 (P1(a4,f7(f6(a1),a5),a2)),
% 7.38/7.44 inference(scs_inference,[],[420,326,304,238,87,460,264,456,451,422,3,8,9,7,22])).
% 7.38/7.44 cnf(474,plain,
% 7.38/7.44 (P1(x4741,x4741,f7(x4742,x4742))),
% 7.38/7.44 inference(scs_inference,[],[420,326,304,238,87,460,264,456,451,422,3,8,9,7,22,19])).
% 7.38/7.44 cnf(476,plain,
% 7.38/7.44 (P1(a4,f7(f6(a4),a4),a4)),
% 7.38/7.44 inference(scs_inference,[],[468,19])).
% 7.38/7.44 cnf(478,plain,
% 7.38/7.44 (E(f7(x4781,x4781),f7(f7(x4782,x4782),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[474,427,468,19,20])).
% 7.38/7.44 cnf(480,plain,
% 7.38/7.44 (P1(x4801,x4801,f7(x4802,x4802))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(482,plain,
% 7.38/7.44 (E(f7(f7(x4821,x4821),a4),f7(x4822,x4822))),
% 7.38/7.44 inference(scs_inference,[],[474,427,468,450,28,19,20,3])).
% 7.38/7.44 cnf(484,plain,
% 7.38/7.44 (E(x4841,f7(f6(x4841),a4))),
% 7.38/7.44 inference(rename_variables,[],[287])).
% 7.38/7.44 cnf(485,plain,
% 7.38/7.44 (P1(x4851,x4851,f7(f6(a4),a4))),
% 7.38/7.44 inference(scs_inference,[],[474,480,65,427,468,450,348,287,28,19,20,3,8,9])).
% 7.38/7.44 cnf(486,plain,
% 7.38/7.44 (P1(x4861,x4861,f7(x4862,x4862))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(487,plain,
% 7.38/7.44 (P1(f7(f6(a4),a4),f6(x4871),x4871)),
% 7.38/7.44 inference(scs_inference,[],[474,480,261,65,427,468,450,348,287,484,28,19,20,3,8,9,7])).
% 7.38/7.44 cnf(491,plain,
% 7.38/7.44 (P1(x4911,x4911,f7(x4912,x4912))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(493,plain,
% 7.38/7.44 (~P1(f7(x4931,x4931),f6(a5),f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[474,480,486,491,218,261,65,427,442,468,318,450,348,287,484,28,19,20,3,8,9,7,21,22])).
% 7.38/7.44 cnf(497,plain,
% 7.38/7.44 (E(f7(x4971,x4971),f7(f7(x4972,x4972),a4))),
% 7.38/7.44 inference(scs_inference,[],[474,480,486,491,218,261,65,427,442,468,318,450,348,287,484,28,19,20,3,8,9,7,21,22,2])).
% 7.38/7.44 cnf(498,plain,
% 7.38/7.44 (P1(x4981,f7(f6(a4),a4),x4981)),
% 7.38/7.44 inference(scs_inference,[],[485,19])).
% 7.38/7.44 cnf(501,plain,
% 7.38/7.44 (E(f7(f7(x5011,x5011),f6(a4)),f7(x5012,x5012))),
% 7.38/7.44 inference(scs_inference,[],[485,478,19,2])).
% 7.38/7.44 cnf(502,plain,
% 7.38/7.44 (E(f7(f7(x5021,x5021),a4),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[485,478,482,265,19,2,3])).
% 7.38/7.44 cnf(505,plain,
% 7.38/7.44 (P1(f7(x5051,x5051),f7(x5052,x5052),a4)),
% 7.38/7.44 inference(rename_variables,[],[420])).
% 7.38/7.44 cnf(508,plain,
% 7.38/7.44 (P1(x5081,x5081,f7(f7(x5082,x5082),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[474,420,505,485,478,482,265,19,2,3,8,7,9])).
% 7.38/7.44 cnf(509,plain,
% 7.38/7.44 (P1(x5091,x5091,f7(x5092,x5092))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(510,plain,
% 7.38/7.44 (P1(a4,f7(f6(a4),a4),f7(a4,a4))),
% 7.38/7.44 inference(scs_inference,[],[476,474,509,420,505,60,485,478,482,265,19,2,3,8,7,9,21])).
% 7.38/7.44 cnf(512,plain,
% 7.38/7.44 (P1(x5121,x5121,f7(x5122,x5122))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(514,plain,
% 7.38/7.44 (~P1(f7(x5141,x5141),a5,f6(f6(a3)))),
% 7.38/7.44 inference(scs_inference,[],[476,474,509,512,420,505,238,359,60,485,478,482,265,19,2,3,8,7,9,21,22])).
% 7.38/7.44 cnf(518,plain,
% 7.38/7.44 (P1(x5181,f7(f7(x5182,x5182),f6(a4)),x5181)),
% 7.38/7.44 inference(scs_inference,[],[508,19])).
% 7.38/7.44 cnf(521,plain,
% 7.38/7.44 (E(f6(a4),f7(f7(x5211,x5211),a4))),
% 7.38/7.44 inference(scs_inference,[],[508,502,19,2])).
% 7.38/7.44 cnf(522,plain,
% 7.38/7.44 (E(f7(f7(x5221,x5221),f6(a4)),a4)),
% 7.38/7.44 inference(scs_inference,[],[508,501,502,46,19,2,3])).
% 7.38/7.44 cnf(525,plain,
% 7.38/7.44 (P1(f7(x5251,x5251),f7(x5252,x5252),a4)),
% 7.38/7.44 inference(rename_variables,[],[420])).
% 7.38/7.44 cnf(526,plain,
% 7.38/7.44 (P1(x5261,x5261,f7(f7(x5262,x5262),a4))),
% 7.38/7.44 inference(scs_inference,[],[474,420,508,501,497,502,46,19,2,3,8,9])).
% 7.38/7.44 cnf(527,plain,
% 7.38/7.44 (P1(x5271,x5271,f7(x5272,x5272))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(528,plain,
% 7.38/7.44 (P1(f7(f7(x5281,x5281),a4),f7(x5282,x5282),a4)),
% 7.38/7.44 inference(scs_inference,[],[474,420,525,508,501,497,502,46,19,2,3,8,9,7])).
% 7.38/7.44 cnf(530,plain,
% 7.38/7.44 (~P1(f7(f6(a4),a4),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[498,474,527,420,525,300,508,501,497,502,46,19,2,3,8,9,7,21])).
% 7.38/7.44 cnf(531,plain,
% 7.38/7.44 (P1(x5311,x5311,f7(x5312,x5312))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(534,plain,
% 7.38/7.44 (P1(f6(x5341),x5341,f6(f7(x5342,x5342)))),
% 7.38/7.44 inference(scs_inference,[],[498,474,527,531,420,525,65,87,300,508,501,497,502,46,19,2,3,8,9,7,21,22])).
% 7.38/7.44 cnf(538,plain,
% 7.38/7.44 (P1(x5381,f7(f7(x5382,x5382),a4),x5381)),
% 7.38/7.44 inference(scs_inference,[],[526,19])).
% 7.38/7.44 cnf(541,plain,
% 7.38/7.44 (E(a4,f7(f7(x5411,x5411),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[526,522,19,2])).
% 7.38/7.44 cnf(543,plain,
% 7.38/7.44 (P1(x5431,x5431,f7(x5432,x5432))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(548,plain,
% 7.38/7.44 (~P1(f7(f7(x5481,x5481),f6(a4)),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[518,474,218,326,238,412,380,526,521,522,19,2,8,7,9,21])).
% 7.38/7.44 cnf(549,plain,
% 7.38/7.44 (P1(f6(a4),x5491,x5491)),
% 7.38/7.44 inference(rename_variables,[],[238])).
% 7.38/7.44 cnf(552,plain,
% 7.38/7.44 (~P1(f7(x5521,x5521),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[518,474,543,218,326,238,549,412,380,526,521,522,19,2,8,7,9,21,22])).
% 7.38/7.44 cnf(557,plain,
% 7.38/7.44 (P1(f7(x5571,x5571),f7(x5572,x5572),a4)),
% 7.38/7.44 inference(rename_variables,[],[420])).
% 7.38/7.44 cnf(559,plain,
% 7.38/7.44 (P1(f7(f7(x5591,x5591),f6(a4)),x5592,f6(x5592))),
% 7.38/7.44 inference(scs_inference,[],[304,420,541,221,8,7])).
% 7.38/7.44 cnf(561,plain,
% 7.38/7.44 (~P1(f7(f7(x5611,x5611),a4),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[538,474,304,420,557,300,541,221,8,7,9,21])).
% 7.38/7.44 cnf(562,plain,
% 7.38/7.44 (P1(x5621,x5621,f7(x5622,x5622))),
% 7.38/7.44 inference(rename_variables,[],[474])).
% 7.38/7.44 cnf(563,plain,
% 7.38/7.44 (P1(x5631,f7(f7(x5632,x5632),a4),x5631)),
% 7.38/7.44 inference(rename_variables,[],[538])).
% 7.38/7.44 cnf(565,plain,
% 7.38/7.44 (P1(f7(f7(x5651,x5651),a4),f7(x5652,x5652),f7(x5652,x5652))),
% 7.38/7.44 inference(scs_inference,[],[538,563,474,562,304,420,557,300,541,221,8,7,9,21,22])).
% 7.38/7.44 cnf(571,plain,
% 7.38/7.44 (E(f7(f6(a4),f6(x5711)),x5711)),
% 7.38/7.44 inference(rename_variables,[],[201])).
% 7.38/7.44 cnf(577,plain,
% 7.38/7.44 (~P1(f7(f6(a4),a4),a5,a3)),
% 7.38/7.44 inference(scs_inference,[],[498,283,238,376,446,530,416,201,571,8,7,9,21])).
% 7.38/7.44 cnf(585,plain,
% 7.38/7.44 (E(f7(a4,f6(a4)),f7(x5851,x5851))),
% 7.38/7.44 inference(scs_inference,[],[368,28,3])).
% 7.38/7.44 cnf(591,plain,
% 7.38/7.44 (P1(f6(a4),x5911,x5911)),
% 7.38/7.44 inference(rename_variables,[],[238])).
% 7.38/7.44 cnf(592,plain,
% 7.38/7.44 (~P1(f7(f7(x5921,x5921),f6(a4)),f6(a5),a3)),
% 7.38/7.44 inference(scs_inference,[],[518,261,238,591,363,384,368,451,114,28,3,8,7,9,21])).
% 7.38/7.44 cnf(593,plain,
% 7.38/7.44 (P1(f6(a4),x5931,x5931)),
% 7.38/7.44 inference(rename_variables,[],[238])).
% 7.38/7.44 cnf(596,plain,
% 7.38/7.44 (~P1(f7(x5961,x5961),f6(a5),a3)),
% 7.38/7.44 inference(scs_inference,[],[518,474,261,238,591,593,363,384,368,451,114,28,3,8,7,9,21,22])).
% 7.38/7.44 cnf(600,plain,
% 7.38/7.44 (P1(f7(x6001,x6001),x6002,x6002)),
% 7.38/7.44 inference(scs_inference,[],[518,474,261,238,591,593,363,384,368,451,114,28,3,8,7,9,21,22,19])).
% 7.38/7.44 cnf(602,plain,
% 7.38/7.44 (E(f7(x6021,x6021),f7(a4,f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[518,474,261,238,591,593,363,384,368,451,114,28,3,8,7,9,21,22,19,2])).
% 7.38/7.44 cnf(603,plain,
% 7.38/7.44 (E(x6031,f7(x6031,a4))),
% 7.38/7.44 inference(scs_inference,[],[600,54,20])).
% 7.38/7.44 cnf(606,plain,
% 7.38/7.44 (E(f7(a4,f6(a4)),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[600,54,585,265,20,3])).
% 7.38/7.44 cnf(610,plain,
% 7.38/7.44 (P1(f7(a4,f6(a4)),x6101,x6101)),
% 7.38/7.44 inference(scs_inference,[],[600,420,54,602,585,265,20,3,8,7])).
% 7.38/7.44 cnf(611,plain,
% 7.38/7.44 (P1(f7(x6111,x6111),x6112,x6112)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(616,plain,
% 7.38/7.44 (P1(f7(x6161,x6161),x6162,x6162)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(618,plain,
% 7.38/7.44 (~P1(a5,f6(a4),f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[18,600,611,616,283,474,218,420,493,54,602,585,265,20,3,8,7,9,21,22])).
% 7.38/7.44 cnf(622,plain,
% 7.38/7.44 (P1(x6221,f7(a4,f6(a4)),x6221)),
% 7.38/7.44 inference(scs_inference,[],[18,600,611,616,283,474,218,420,493,54,602,585,265,20,3,8,7,9,21,22,19])).
% 7.38/7.44 cnf(624,plain,
% 7.38/7.44 (E(f7(x6241,a4),x6241)),
% 7.38/7.44 inference(scs_inference,[],[18,600,611,616,283,474,218,420,493,54,602,585,265,20,3,8,7,9,21,22,19,2])).
% 7.38/7.44 cnf(625,plain,
% 7.38/7.44 (E(f7(x6251,f7(x6252,a4)),f7(x6251,x6252))),
% 7.38/7.44 inference(scs_inference,[],[603,6,2])).
% 7.38/7.44 cnf(626,plain,
% 7.38/7.44 (E(f7(x6261,x6262),f7(x6261,f7(x6262,a4)))),
% 7.38/7.44 inference(scs_inference,[],[625,2])).
% 7.38/7.44 cnf(627,plain,
% 7.38/7.44 (E(f6(a4),f7(a4,f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[622,238,625,2,20])).
% 7.38/7.44 cnf(629,plain,
% 7.38/7.44 (P1(x6291,f7(a4,f6(a4)),x6291)),
% 7.38/7.44 inference(rename_variables,[],[622])).
% 7.38/7.44 cnf(631,plain,
% 7.38/7.44 (E(f7(f7(x6311,x6311),f7(a4,a4)),f7(x6312,x6312))),
% 7.38/7.44 inference(scs_inference,[],[622,238,625,482,2,20,3])).
% 7.38/7.44 cnf(632,plain,
% 7.38/7.44 (E(f7(x6321,f7(x6322,a4)),f7(x6321,x6322))),
% 7.38/7.44 inference(rename_variables,[],[625])).
% 7.38/7.44 cnf(635,plain,
% 7.38/7.44 (E(f7(x6351,f7(x6352,a4)),f7(x6351,x6352))),
% 7.38/7.44 inference(rename_variables,[],[625])).
% 7.38/7.44 cnf(636,plain,
% 7.38/7.44 (P1(f7(f7(x6361,a4),x6361),x6362,x6362)),
% 7.38/7.44 inference(scs_inference,[],[622,600,420,238,625,632,635,482,2,20,3,8,7])).
% 7.38/7.44 cnf(637,plain,
% 7.38/7.44 (P1(f7(x6371,x6371),x6372,x6372)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(638,plain,
% 7.38/7.44 (E(f7(x6381,f7(x6382,a4)),f7(x6381,x6382))),
% 7.38/7.44 inference(rename_variables,[],[625])).
% 7.38/7.44 cnf(642,plain,
% 7.38/7.44 (~P1(f7(a4,f6(a4)),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[622,629,600,474,420,238,487,577,625,632,635,638,482,2,20,3,8,7,9,21])).
% 7.38/7.44 cnf(646,plain,
% 7.38/7.44 (~P1(a4,f6(a5),f6(f6(a3)))),
% 7.38/7.44 inference(scs_inference,[],[622,629,600,637,474,261,420,238,487,514,577,625,632,635,638,482,2,20,3,8,7,9,21,22])).
% 7.38/7.44 cnf(650,plain,
% 7.38/7.44 (P1(x6501,f7(f7(x6502,a4),x6502),x6501)),
% 7.38/7.44 inference(scs_inference,[],[622,629,600,637,474,261,420,238,487,514,577,625,632,635,638,482,2,20,3,8,7,9,21,22,19])).
% 7.38/7.44 cnf(652,plain,
% 7.38/7.44 (E(f7(x6521,x6521),f7(f7(x6522,x6522),f7(a4,a4)))),
% 7.38/7.44 inference(scs_inference,[],[631,2])).
% 7.38/7.44 cnf(653,plain,
% 7.38/7.44 (E(f7(x6531,x6531),f7(f7(x6532,a4),x6532))),
% 7.38/7.44 inference(scs_inference,[],[650,600,631,2,20])).
% 7.38/7.44 cnf(654,plain,
% 7.38/7.44 (P1(f7(x6541,x6541),x6542,x6542)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(655,plain,
% 7.38/7.44 (P1(x6551,f7(f7(x6552,a4),x6552),x6551)),
% 7.38/7.44 inference(rename_variables,[],[650])).
% 7.38/7.44 cnf(657,plain,
% 7.38/7.44 (E(f7(f7(x6571,x6571),f7(a4,a4)),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[650,600,631,265,2,20,3])).
% 7.38/7.44 cnf(661,plain,
% 7.38/7.44 (P1(f7(a4,a4),x6611,f6(x6611))),
% 7.38/7.44 inference(scs_inference,[],[650,538,600,304,631,626,603,265,2,20,3,8,7])).
% 7.38/7.44 cnf(665,plain,
% 7.38/7.44 (~P1(f7(f7(x6651,a4),x6651),a5,f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[650,655,538,600,654,326,304,552,618,631,626,603,265,2,20,3,8,7,9,21])).
% 7.38/7.44 cnf(666,plain,
% 7.38/7.44 (P1(f7(x6661,x6661),x6662,x6662)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(669,plain,
% 7.38/7.44 (~P1(f7(x6691,x6691),f7(f6(a5),a4),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[650,655,538,600,654,666,283,326,304,552,618,631,626,603,265,2,20,3,8,7,9,21,22])).
% 7.38/7.44 cnf(673,plain,
% 7.38/7.44 (E(f7(f7(x6731,a4),x6731),f7(x6732,x6732))),
% 7.38/7.44 inference(scs_inference,[],[653,2])).
% 7.38/7.44 cnf(675,plain,
% 7.38/7.44 (P1(f7(x6751,x6751),x6752,x6752)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(676,plain,
% 7.38/7.44 (~E(f7(f6(a5),a4),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[600,675,669,653,2,8,9])).
% 7.38/7.44 cnf(677,plain,
% 7.38/7.44 (P1(f7(x6771,x6771),x6772,x6772)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(679,plain,
% 7.38/7.44 (P1(f7(x6791,x6791),x6792,x6792)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(680,plain,
% 7.38/7.44 (~P1(f7(a4,f6(a4)),f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[622,600,675,677,304,669,646,652,653,2,8,9,7,21])).
% 7.38/7.44 cnf(684,plain,
% 7.38/7.44 (~P1(f6(a4),f7(f6(a5),a4),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[622,600,675,677,679,304,238,669,646,652,653,2,8,9,7,21,22])).
% 7.38/7.44 cnf(688,plain,
% 7.38/7.44 (E(f6(a4),f7(f7(x6881,x6881),f7(a4,a4)))),
% 7.38/7.44 inference(scs_inference,[],[657,2])).
% 7.38/7.44 cnf(689,plain,
% 7.38/7.44 (E(f6(a4),f7(f7(x6891,a4),x6891))),
% 7.38/7.44 inference(scs_inference,[],[650,238,657,2,20])).
% 7.38/7.44 cnf(691,plain,
% 7.38/7.44 (P1(x6911,f7(f7(x6912,a4),x6912),x6911)),
% 7.38/7.44 inference(rename_variables,[],[650])).
% 7.38/7.44 cnf(693,plain,
% 7.38/7.44 (E(f7(f7(x6931,a4),x6931),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[650,238,673,657,2,20,3])).
% 7.38/7.44 cnf(696,plain,
% 7.38/7.44 (~E(f7(f6(a3),a4),f6(a5))),
% 7.38/7.44 inference(scs_inference,[],[650,283,238,596,673,657,2,20,3,8])).
% 7.38/7.44 cnf(698,plain,
% 7.38/7.44 (P1(a1,a5,f7(a2,a4))),
% 7.38/7.44 inference(scs_inference,[],[650,283,111,238,596,673,657,603,2,20,3,8,9])).
% 7.38/7.44 cnf(699,plain,
% 7.38/7.44 (E(x6991,f7(x6991,a4))),
% 7.38/7.44 inference(rename_variables,[],[603])).
% 7.38/7.44 cnf(700,plain,
% 7.38/7.44 (P1(f7(a1,a4),a5,a2)),
% 7.38/7.44 inference(scs_inference,[],[650,283,111,238,596,673,657,603,699,2,20,3,8,9,7])).
% 7.38/7.44 cnf(702,plain,
% 7.38/7.44 (~P1(f7(f7(x7021,a4),x7021),f6(a5),a3)),
% 7.38/7.44 inference(scs_inference,[],[650,691,600,283,111,238,596,673,657,603,699,2,20,3,8,9,7,21])).
% 7.38/7.44 cnf(703,plain,
% 7.38/7.44 (P1(f7(x7031,x7031),x7032,x7032)),
% 7.38/7.44 inference(rename_variables,[],[600])).
% 7.38/7.44 cnf(706,plain,
% 7.38/7.44 (~P1(a4,f6(f6(a5)),a3)),
% 7.38/7.44 inference(scs_inference,[],[650,691,600,703,283,111,261,238,596,673,657,603,699,2,20,3,8,9,7,21,22])).
% 7.38/7.44 cnf(713,plain,
% 7.38/7.44 (P1(f7(f7(x7131,x7131),f6(a4)),f6(x7132),x7132)),
% 7.38/7.44 inference(scs_inference,[],[218,261,627,696,541,422,3,8,7])).
% 7.38/7.44 cnf(716,plain,
% 7.38/7.44 (~P1(f7(f6(a4),a4),f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[498,218,304,261,111,646,627,696,541,177,422,3,8,7,9,21])).
% 7.38/7.44 cnf(720,plain,
% 7.38/7.44 (~P1(f7(a4,a4),a5,f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[498,600,218,304,261,111,661,493,646,627,696,541,177,422,3,8,7,9,21,22])).
% 7.38/7.44 cnf(728,plain,
% 7.38/7.44 (E(x7281,f7(x7281,f6(a4)))),
% 7.38/7.44 inference(rename_variables,[],[349])).
% 7.38/7.44 cnf(735,plain,
% 7.38/7.44 (~P1(a4,f6(a5),f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[622,600,218,420,261,559,720,548,688,676,349,728,154,3,8,7,9,21,22])).
% 7.38/7.44 cnf(739,plain,
% 7.38/7.44 (E(a4,f7(f7(x7391,a4),x7391))),
% 7.38/7.44 inference(scs_inference,[],[650,13,20])).
% 7.38/7.44 cnf(741,plain,
% 7.38/7.44 (P1(x7411,f7(f7(x7412,a4),x7412),x7411)),
% 7.38/7.44 inference(rename_variables,[],[650])).
% 7.38/7.44 cnf(745,plain,
% 7.38/7.44 (E(x7451,f7(x7451,a4))),
% 7.38/7.44 inference(rename_variables,[],[603])).
% 7.38/7.44 cnf(748,plain,
% 7.38/7.44 (~P1(f7(f7(x7481,a4),x7481),f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[650,741,218,420,261,610,680,689,13,603,745,20,8,7,9,21])).
% 7.38/7.44 cnf(752,plain,
% 7.38/7.44 (~P1(f7(x7521,x7521),a5,f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[650,741,474,600,218,420,261,610,680,720,689,13,603,745,20,8,7,9,21,22])).
% 7.38/7.44 cnf(758,plain,
% 7.38/7.44 (P1(f7(f7(x7581,a4),x7581),x7582,f6(x7582))),
% 7.38/7.44 inference(scs_inference,[],[87,304,739,2,8,7])).
% 7.38/7.44 cnf(760,plain,
% 7.38/7.44 (~P1(f7(f7(x7601,x7601),f6(a4)),f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[518,87,304,420,636,748,739,2,8,7,9,21])).
% 7.38/7.44 cnf(769,plain,
% 7.38/7.44 (E(x7691,f7(f6(x7691),a4))),
% 7.38/7.44 inference(rename_variables,[],[287])).
% 7.38/7.44 cnf(770,plain,
% 7.38/7.44 (P1(f7(f6(a1),a4),a5,a2)),
% 7.38/7.44 inference(scs_inference,[],[87,111,287,769,8,7])).
% 7.38/7.44 cnf(771,plain,
% 7.38/7.44 (E(x7711,f7(f6(x7711),a4))),
% 7.38/7.44 inference(rename_variables,[],[287])).
% 7.38/7.44 cnf(774,plain,
% 7.38/7.44 (~P1(f7(f7(x7741,x7741),a4),a5,a3)),
% 7.38/7.44 inference(scs_inference,[],[538,87,111,758,665,287,769,771,8,7,9,21])).
% 7.38/7.44 cnf(782,plain,
% 7.38/7.44 (~E(f6(f6(a3)),f6(a5))),
% 7.38/7.44 inference(scs_inference,[],[713,760,8])).
% 7.38/7.44 cnf(787,plain,
% 7.38/7.44 (~P1(f7(f6(a4),a4),f6(a5),a3)),
% 7.38/7.44 inference(scs_inference,[],[498,304,534,713,716,760,376,369,451,8,7,9,21])).
% 7.38/7.44 cnf(791,plain,
% 7.38/7.44 (P1(a2,f6(a1),f7(f6(a5),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[498,474,600,304,534,713,149,716,760,376,369,451,8,7,9,21,22])).
% 7.38/7.44 cnf(795,plain,
% 7.38/7.44 (P1(f7(x7951,x7951),f6(f6(x7952)),x7952)),
% 7.38/7.44 inference(scs_inference,[],[498,474,600,304,534,713,149,716,760,376,369,451,8,7,9,21,22,19])).
% 7.38/7.44 cnf(799,plain,
% 7.38/7.44 (P1(f6(x7991),f7(f7(x7992,x7992),f6(a4)),x7991)),
% 7.38/7.44 inference(scs_inference,[],[87,782,541,422,3,8])).
% 7.38/7.44 cnf(812,plain,
% 7.38/7.44 (P1(x8121,f7(f6(a4),f7(a4,a4)),x8121)),
% 7.38/7.44 inference(scs_inference,[],[498,626,8])).
% 7.38/7.44 cnf(816,plain,
% 7.38/7.44 (P1(f7(f7(x8161,x8161),a4),x8162,f6(x8162))),
% 7.38/7.44 inference(scs_inference,[],[498,474,304,652,626,433,8,9,7])).
% 7.38/7.44 cnf(817,plain,
% 7.38/7.44 (~P1(f7(f7(x8171,a4),x8171),a5,a3)),
% 7.38/7.44 inference(scs_inference,[],[650,498,474,304,335,561,652,626,433,8,9,7,21])).
% 7.38/7.44 cnf(826,plain,
% 7.38/7.44 (E(f7(f6(a4),f7(a4,a4)),f7(x8261,x8261))),
% 7.38/7.44 inference(scs_inference,[],[600,812,20])).
% 7.38/7.44 cnf(841,plain,
% 7.38/7.44 (~P1(f7(f6(a4),f6(a5)),f7(x8411,x8411),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[518,498,600,420,87,816,395,642,296,440,702,812,653,114,20,8,9,7,21,22])).
% 7.38/7.44 cnf(845,plain,
% 7.38/7.44 (E(f7(f6(a4),f7(a4,a4)),f6(a4))),
% 7.38/7.44 inference(scs_inference,[],[826,657,2,3])).
% 7.38/7.44 cnf(849,plain,
% 7.38/7.44 (E(x8491,f7(f6(a4),f6(x8491)))),
% 7.38/7.44 inference(rename_variables,[],[177])).
% 7.38/7.44 cnf(851,plain,
% 7.38/7.44 (P1(x8511,f7(f6(x8511),f6(x8512)),x8512)),
% 7.38/7.44 inference(rename_variables,[],[23])).
% 7.38/7.44 cnf(853,plain,
% 7.38/7.44 (P1(f7(f6(a4),f6(a4)),x8531,f6(x8531))),
% 7.38/7.44 inference(scs_inference,[],[23,304,111,841,826,657,177,849,2,3,8,9,7])).
% 7.38/7.44 cnf(859,plain,
% 7.38/7.44 (P1(f7(f7(a1,a4),a5),f7(a2,a4),f7(x8591,x8591))),
% 7.38/7.44 inference(scs_inference,[],[538,23,851,474,304,111,841,189,787,487,826,657,177,849,2,3,8,9,7,21,22])).
% 7.38/7.44 cnf(864,plain,
% 7.38/7.44 (E(f6(a4),f7(f6(a4),f7(a4,a4)))),
% 7.38/7.44 inference(scs_inference,[],[845,2])).
% 7.38/7.44 cnf(886,plain,
% 7.38/7.44 (P1(f6(f6(a4)),x8861,x8861)),
% 7.38/7.44 inference(scs_inference,[],[600,474,218,864,307,8,9,7])).
% 7.38/7.44 cnf(888,plain,
% 7.38/7.44 (P1(f6(x8881),f7(f7(x8882,x8882),a4),x8881)),
% 7.38/7.44 inference(scs_inference,[],[518,538,600,474,218,799,864,307,8,9,7,21])).
% 7.38/7.44 cnf(897,plain,
% 7.38/7.44 (P1(x8971,f6(f6(a4)),x8971)),
% 7.38/7.44 inference(scs_inference,[],[518,538,23,600,474,218,735,228,799,864,307,8,9,7,21,22,19])).
% 7.38/7.44 cnf(899,plain,
% 7.38/7.44 (~E(f6(a3),f6(f6(a5)))),
% 7.38/7.44 inference(scs_inference,[],[261,706,8])).
% 7.38/7.44 cnf(902,plain,
% 7.38/7.44 (E(x9021,f7(x9021,f6(a4)))),
% 7.38/7.44 inference(rename_variables,[],[349])).
% 7.38/7.44 cnf(903,plain,
% 7.38/7.44 (P1(f7(a1,f6(a4)),a5,a2)),
% 7.38/7.44 inference(scs_inference,[],[261,111,706,349,902,8,9,7])).
% 7.38/7.44 cnf(913,plain,
% 7.38/7.44 (~E(f6(a3),f6(a5))),
% 7.38/7.44 inference(scs_inference,[],[899,154,3])).
% 7.38/7.44 cnf(917,plain,
% 7.38/7.44 (P1(f7(x9171,x9171),x9172,f6(x9172))),
% 7.38/7.44 inference(scs_inference,[],[111,853,899,73,603,154,3,8,7])).
% 7.38/7.44 cnf(935,plain,
% 7.38/7.44 (P1(x9351,x9351,f6(f7(x9352,x9352)))),
% 7.38/7.44 inference(scs_inference,[],[600,474,420,913,352,422,3,8,7,9])).
% 7.38/7.44 cnf(939,plain,
% 7.38/7.44 (P1(x9391,f6(f6(a4)),x9391)),
% 7.38/7.44 inference(rename_variables,[],[897])).
% 7.38/7.44 cnf(946,plain,
% 7.38/7.44 (P1(f7(x9461,x9461),f6(x9462),x9462)),
% 7.38/7.44 inference(scs_inference,[],[795,897,939,173,600,474,420,592,713,913,352,422,3,8,7,9,21,22,19])).
% 7.38/7.44 cnf(948,plain,
% 7.38/7.44 (P1(x9481,f6(f7(x9482,x9482)),x9481)),
% 7.38/7.44 inference(scs_inference,[],[935,19])).
% 7.38/7.44 cnf(951,plain,
% 7.38/7.44 (E(x9511,f7(f7(x9512,x9512),f6(x9511)))),
% 7.38/7.44 inference(scs_inference,[],[946,935,17,19,20])).
% 7.38/7.44 cnf(956,plain,
% 7.38/7.44 (P1(f7(a1,f7(a4,a4)),a5,a2)),
% 7.38/7.44 inference(scs_inference,[],[946,111,700,935,626,287,17,19,20,8,7])).
% 7.38/7.44 cnf(972,plain,
% 7.38/7.44 (E(x9721,f7(f7(x9722,x9722),f6(x9721)))),
% 7.38/7.44 inference(rename_variables,[],[951])).
% 7.38/7.44 cnf(973,plain,
% 7.38/7.44 (P1(f7(f7(x9731,x9731),f6(x9732)),f6(a4),f6(x9732))),
% 7.38/7.44 inference(scs_inference,[],[218,111,951,972,2,8,7])).
% 7.38/7.44 cnf(982,plain,
% 7.38/7.44 (~P1(f6(a4),a5,f7(f6(a3),f6(a4)))),
% 7.38/7.44 inference(scs_inference,[],[948,946,218,111,458,886,752,817,951,972,2,8,7,9,21,22])).
% 7.38/7.44 cnf(988,plain,
% 7.38/7.44 (E(x9881,f7(f7(x9882,x9882),f6(x9881)))),
% 7.38/7.44 inference(rename_variables,[],[951])).
% 7.38/7.44 cnf(989,plain,
% 7.38/7.44 (P1(f7(f7(x9891,x9891),f6(a1)),a5,a2)),
% 7.38/7.44 inference(scs_inference,[],[111,122,951,988,8,7])).
% 7.38/7.44 cnf(1002,plain,
% 7.38/7.44 (P1(f6(a1),a5,a2)),
% 7.38/7.44 inference(scs_inference,[],[859,249,221,624,8,7])).
% 7.38/7.44 cnf(1004,plain,
% 7.38/7.44 (P1(a2,f6(a1),f6(a5))),
% 7.38/7.44 inference(scs_inference,[],[859,791,249,221,368,624,8,7,9])).
% 7.38/7.44 cnf(1011,plain,
% 7.38/7.44 (P1(f7(f7(a1,a4),a5),f7(x10111,x10111),f7(a2,a4))),
% 7.38/7.44 inference(scs_inference,[],[948,474,600,859,791,249,816,748,221,368,624,8,7,9,21,22])).
% 7.38/7.44 cnf(1016,plain,
% 7.38/7.44 (E(x10161,f7(f7(x10162,x10162),f6(x10161)))),
% 7.38/7.44 inference(rename_variables,[],[951])).
% 7.38/7.44 cnf(1019,plain,
% 7.38/7.44 (P1(f6(a4),x10191,f6(x10191))),
% 7.38/7.44 inference(scs_inference,[],[1002,395,606,951,1016,8,9,7])).
% 7.38/7.44 cnf(1022,plain,
% 7.38/7.44 (P1(f7(x10221,x10221),f6(x10222),x10222)),
% 7.38/7.44 inference(rename_variables,[],[946])).
% 7.38/7.44 cnf(1024,plain,
% 7.38/7.44 (P1(f7(x10241,x10241),f6(f6(a4)),f7(x10242,x10242))),
% 7.38/7.44 inference(scs_inference,[],[18,946,1022,283,65,474,1002,395,606,951,1016,8,9,7,21,22])).
% 7.38/7.44 cnf(1031,plain,
% 7.38/7.44 (P1(f7(f7(a1,a4),f7(a5,a4)),f7(x10311,x10311),f7(a2,a4))),
% 7.38/7.44 inference(scs_inference,[],[1011,1024,176,626,8,7])).
% 7.38/7.44 cnf(1047,plain,
% 7.38/7.44 (P1(f7(f7(x10471,x10471),f7(a4,a4)),a4,f7(x10472,x10472))),
% 7.38/7.44 inference(scs_inference,[],[1031,684,1019,122,652,624,8,9,7])).
% 7.38/7.44 cnf(1049,plain,
% 7.38/7.44 (~P1(f7(x10491,x10491),f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[946,1031,684,1019,279,122,669,652,624,8,9,7,22])).
% 7.38/7.44 cnf(1055,plain,
% 7.38/7.44 (P1(f7(x10551,x10551),a4,f7(x10552,x10552))),
% 7.38/7.44 inference(scs_inference,[],[1047,253,631,626,8,7])).
% 7.38/7.44 cnf(1057,plain,
% 7.38/7.44 (~E(f6(f6(a5)),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[917,1047,1049,253,631,626,8,7,9])).
% 7.38/7.44 cnf(1059,plain,
% 7.38/7.44 (~P1(a4,f6(a5),f6(a3))),
% 7.38/7.44 inference(scs_inference,[],[946,238,917,1047,1049,253,631,626,8,7,9,22])).
% 7.38/7.44 cnf(1067,plain,
% 7.38/7.44 (P1(f7(x10671,x10671),a4,f7(x10672,x10672))),
% 7.38/7.45 inference(rename_variables,[],[1055])).
% 7.38/7.45 cnf(1070,plain,
% 7.38/7.45 (P1(f7(x10701,x10701),f7(a2,a4),f7(f7(a1,a4),a5))),
% 7.38/7.45 inference(scs_inference,[],[23,600,1055,1067,189,1057,348,451,422,3,8,9,7,22])).
% 7.38/7.45 cnf(1083,plain,
% 7.38/7.45 (P1(f7(a2,a4),f7(f7(a1,a4),a5),f7(x10831,x10831))),
% 7.38/7.45 inference(scs_inference,[],[946,23,474,1070,1011,104,625,653,624,8,9,7,22])).
% 7.38/7.45 cnf(1090,plain,
% 7.38/7.45 (E(f7(f6(a4),f6(x10901)),x10901)),
% 7.38/7.45 inference(rename_variables,[],[201])).
% 7.38/7.45 cnf(1091,plain,
% 7.38/7.45 (P1(a4,f7(f6(x10911),a4),f6(x10911))),
% 7.38/7.45 inference(scs_inference,[],[401,528,201,1090,8,7])).
% 7.38/7.45 cnf(1108,plain,
% 7.38/7.45 (~P1(a4,f7(f6(a5),a4),f6(a3))),
% 7.38/7.45 inference(scs_inference,[],[600,565,510,1091,1049,363,73,114,8,9,7,22])).
% 7.38/7.45 cnf(1122,plain,
% 7.38/7.45 (E(f7(x11221,x11222),f7(x11221,f7(x11222,a4)))),
% 7.38/7.45 inference(rename_variables,[],[626])).
% 7.38/7.45 cnf(1124,plain,
% 7.38/7.45 (E(f7(x11241,x11242),f7(x11241,f7(x11242,a4)))),
% 7.38/7.45 inference(rename_variables,[],[626])).
% 7.38/7.45 cnf(1125,plain,
% 7.38/7.45 (P1(f7(f7(a1,a4),f7(a5,a4)),f7(a2,a4),f7(x11251,x11251))),
% 7.38/7.45 inference(scs_inference,[],[470,1070,859,626,1122,1124,8,9,7])).
% 7.38/7.45 cnf(1135,plain,
% 7.38/7.45 (P1(f7(f6(a4),f6(a1)),a2,a5)),
% 7.38/7.45 inference(scs_inference,[],[791,363,423,176,625,177,3,8,7])).
% 7.38/7.45 cnf(1136,plain,
% 7.38/7.45 (E(x11361,f7(f6(a4),f6(x11361)))),
% 7.38/7.45 inference(rename_variables,[],[177])).
% 7.38/7.45 cnf(1139,plain,
% 7.38/7.45 (P1(a4,f7(f7(a1,a4),a5),a2)),
% 7.38/7.45 inference(scs_inference,[],[65,238,214,791,700,363,423,176,625,177,1136,3,8,7,9,22])).
% 7.38/7.45 cnf(1145,plain,
% 7.38/7.45 (P1(f6(a1),a2,a5)),
% 7.38/7.45 inference(scs_inference,[],[1135,1002,221,349,8,7])).
% 7.38/7.45 cnf(1154,plain,
% 7.38/7.45 (E(x11541,f7(x11541,a4))),
% 7.38/7.45 inference(rename_variables,[],[603])).
% 7.38/7.45 cnf(1156,plain,
% 7.38/7.45 (E(x11561,f7(x11561,a4))),
% 7.38/7.45 inference(rename_variables,[],[603])).
% 7.38/7.45 cnf(1157,plain,
% 7.38/7.45 (P1(f7(a2,a4),f6(a1),f7(f6(a5),f6(a4)))),
% 7.38/7.45 inference(scs_inference,[],[1139,956,791,603,1154,1156,8,9,7])).
% 7.38/7.45 cnf(1159,plain,
% 7.38/7.45 (~P1(f7(f6(a5),a4),a4,f6(a3))),
% 7.38/7.45 inference(scs_inference,[],[23,1108,1139,956,228,791,603,1154,1156,8,9,7,22])).
% 7.38/7.45 cnf(1164,plain,
% 7.38/7.45 (E(f7(x11641,a4),x11641)),
% 7.38/7.45 inference(rename_variables,[],[624])).
% 7.38/7.45 cnf(1165,plain,
% 7.38/7.45 (P1(a2,f7(f7(a1,a4),a5),f7(x11651,x11651))),
% 7.38/7.45 inference(scs_inference,[],[1125,1083,624,1164,8,7])).
% 7.38/7.45 cnf(1169,plain,
% 7.38/7.45 (~P1(f6(a4),f6(f6(a5)),f6(a3))),
% 7.38/7.45 inference(scs_inference,[],[304,261,1125,1157,1059,1083,368,624,1164,8,7,9,22])).
% 7.38/7.45 cnf(1174,plain,
% 7.38/7.45 (E(x11741,f7(f6(x11741),a4))),
% 7.38/7.45 inference(rename_variables,[],[287])).
% 7.38/7.45 cnf(1176,plain,
% 7.38/7.45 (E(x11761,f7(f6(x11761),a4))),
% 7.38/7.45 inference(rename_variables,[],[287])).
% 7.38/7.45 cnf(1177,plain,
% 7.38/7.45 (P1(f7(f6(a1),a4),a2,a5)),
% 7.38/7.45 inference(scs_inference,[],[1145,363,287,1174,1176,8,9,7])).
% 7.38/7.45 cnf(1179,plain,
% 7.38/7.45 (P1(f7(a1,f6(a4)),a2,a5)),
% 7.38/7.45 inference(scs_inference,[],[474,600,903,1145,363,287,1174,1176,8,9,7,22])).
% 7.38/7.45 cnf(1184,plain,
% 7.38/7.45 (E(x11841,f6(x11841))),
% 7.38/7.45 inference(rename_variables,[],[154])).
% 7.38/7.45 cnf(1185,plain,
% 7.38/7.45 (P1(f6(a2),f7(f7(a1,a4),a5),f7(x11851,x11851))),
% 7.38/7.45 inference(scs_inference,[],[770,1165,154,1184,8,7])).
% 7.38/7.45 cnf(1186,plain,
% 7.38/7.45 (E(x11861,f6(x11861))),
% 7.38/7.45 inference(rename_variables,[],[154])).
% 7.38/7.45 cnf(1189,plain,
% 7.38/7.45 (~P1(f7(f6(a5),a4),f7(x11891,x11891),f6(a3))),
% 7.38/7.45 inference(scs_inference,[],[498,770,1159,1165,440,154,1184,1186,8,7,9,22])).
% 7.38/7.45 cnf(1196,plain,
% 7.38/7.45 (P1(f7(f7(x11961,a4),x11961),x11962,f7(x11962,a4))),
% 7.38/7.45 inference(scs_inference,[],[1169,1019,1145,34,739,114,8,9,7])).
% 7.38/7.45 cnf(1197,plain,
% 7.38/7.45 (P1(f7(x11971,x11971),f7(x11972,x11972),f7(x11973,x11973))),
% 7.38/7.45 inference(scs_inference,[],[946,1169,1185,1019,1165,1145,34,739,114,8,9,7,22])).
% 7.38/7.45 cnf(1201,plain,
% 7.38/7.45 (P1(f6(a4),x12011,f7(x12011,a4))),
% 7.38/7.45 inference(scs_inference,[],[65,1196,693,433,8,7])).
% 7.38/7.45 cnf(1202,plain,
% 7.38/7.45 (P1(f7(f7(x12021,a4),x12021),x12022,f7(x12022,a4))),
% 7.38/7.45 inference(rename_variables,[],[1196])).
% 7.38/7.45 cnf(1206,plain,
% 7.38/7.45 (P1(a4,f7(f7(a1,a4),a5),f6(a2))),
% 7.38/7.45 inference(scs_inference,[],[23,65,304,1196,1202,774,145,693,433,8,7,9,22])).
% 7.38/7.45 cnf(1223,plain,
% 7.38/7.45 (P1(f7(f6(a4),f7(a4,a4)),x12231,f7(x12231,a4))),
% 7.38/7.45 inference(scs_inference,[],[1206,1201,864,626,8,7])).
% 7.38/7.45 cnf(1231,plain,
% 7.38/7.45 (P1(f7(f6(a4),f6(a2)),f6(a1),f6(a5))),
% 7.38/7.45 inference(scs_inference,[],[973,1004,269,177,8,7])).
% 7.38/7.45 cnf(1242,plain,
% 7.38/7.45 (P1(f7(f6(a4),f7(a4,a4)),f7(a4,a4),f7(x12421,x12421))),
% 7.38/7.45 inference(scs_inference,[],[1223,700,673,349,8,9])).
% 7.38/7.45 cnf(1251,plain,
% 7.38/7.45 (E(x12511,f7(x12511,a4))),
% 7.38/7.45 inference(rename_variables,[],[603])).
% 7.38/7.45 cnf(1252,plain,
% 7.38/7.45 (P1(f7(a2,a4),f7(f6(a5),f6(a4)),f6(a1))),
% 7.38/7.45 inference(scs_inference,[],[1179,149,603,1251,8,7])).
% 7.38/7.45 cnf(1253,plain,
% 7.38/7.45 (E(x12531,f7(x12531,a4))),
% 7.38/7.45 inference(rename_variables,[],[603])).
% 7.38/7.45 cnf(1256,plain,
% 7.38/7.45 (P1(f7(x12561,x12561),f7(x12562,x12562),f6(a4))),
% 7.38/7.45 inference(scs_inference,[],[420,65,1179,1047,149,603,1251,1253,8,7,9,22])).
% 7.38/7.45 cnf(1265,plain,
% 7.38/7.45 (P1(f7(f6(a1),a4),a5,f7(a2,a4))),
% 7.38/7.45 inference(scs_inference,[],[1252,1223,698,306,368,287,8,9,7])).
% 7.38/7.45 cnf(1271,plain,
% 7.38/7.45 (E(x12711,f6(x12711))),
% 7.38/7.45 inference(rename_variables,[],[154])).
% 7.38/7.45 cnf(1273,plain,
% 7.38/7.45 (E(x12731,f6(x12731))),
% 7.38/7.45 inference(rename_variables,[],[154])).
% 7.38/7.45 cnf(1276,plain,
% 7.38/7.45 (P1(f7(x12761,x12761),f7(a2,a4),a2)),
% 7.38/7.45 inference(scs_inference,[],[283,111,1177,1265,253,154,1271,1273,8,7,9,22])).
% 7.38/7.45 cnf(1284,plain,
% 7.38/7.45 (P1(f6(a4),f7(a4,a4),f7(x12841,x12841))),
% 7.38/7.45 inference(scs_inference,[],[1276,104,1242,845,602,114,8,9,7])).
% 7.38/7.45 cnf(1291,plain,
% 7.38/7.45 (P1(f7(f7(x12911,a4),x12911),f7(a4,a4),f7(x12912,x12912))),
% 7.38/7.45 inference(scs_inference,[],[1284,689,653,8,7])).
% 7.38/7.45 cnf(1294,plain,
% 7.38/7.45 (P1(a4,f7(x12941,x12941),f7(f7(x12942,x12942),f7(a4,a4)))),
% 7.38/7.45 inference(scs_inference,[],[87,304,1284,189,1047,689,653,624,8,7,9,22])).
% 7.38/7.45 cnf(1314,plain,
% 7.38/7.45 (P1(f6(x13141),x13141,f7(x13142,x13142))),
% 7.38/7.45 inference(scs_inference,[],[534,1031,888,388,201,8,7,9])).
% 7.38/7.45 cnf(1342,plain,
% 7.38/7.45 (E(f7(f7(x13421,x13421),f7(a4,a4)),f6(a4))),
% 7.38/7.45 inference(rename_variables,[],[657])).
% 7.38/7.45 cnf(1345,plain,
% 7.38/7.45 (E(f7(f7(x13451,x13451),f7(a4,a4)),f6(a4))),
% 7.38/7.45 inference(rename_variables,[],[657])).
% 7.38/7.45 cnf(1346,plain,
% 7.38/7.45 (P1(f6(a4),f7(x13461,x13461),f7(x13462,x13462))),
% 7.38/7.45 inference(scs_inference,[],[1197,1291,1294,657,1342,1345,8,9,7])).
% 7.38/7.45 cnf(1349,plain,
% 7.38/7.45 (P1(f7(a2,a4),f7(f6(a5),f6(a4)),a1)),
% 7.38/7.45 inference(scs_inference,[],[946,474,1197,1291,1157,1294,657,1342,1345,8,9,7,22])).
% 7.38/7.45 cnf(1358,plain,
% 7.38/7.45 (P1(f6(a4),f7(f7(a1,a4),a5),f7(a2,a4))),
% 7.38/7.45 inference(scs_inference,[],[23,238,1349,1346,982,1070,1201,627,368,8,7,9,22])).
% 7.38/7.45 cnf(1366,plain,
% 7.38/7.45 (P1(f7(f6(a4),f7(a4,a4)),f7(x13661,x13661),f7(x13662,x13662))),
% 7.38/7.45 inference(scs_inference,[],[1256,1346,1002,864,177,8,9,7])).
% 7.38/7.45 cnf(1372,plain,
% 7.38/7.45 (P1(x13721,f6(x13721),f6(f7(x13722,x13722)))),
% 7.38/7.45 inference(scs_inference,[],[534,1276,132,349,8,7])).
% 7.38/7.45 cnf(1385,plain,
% 7.38/7.45 (P1(f6(a2),f6(a1),f6(a5))),
% 7.38/7.45 inference(scs_inference,[],[1372,989,1231,329,221,603,8,9,7])).
% 7.38/7.45 cnf(1391,plain,
% 7.38/7.45 (P1(a2,f6(a5),a1)),
% 7.38/7.45 inference(scs_inference,[],[420,474,1372,1366,989,1231,329,221,603,8,9,7,22,19])).
% 7.38/7.45 cnf(1393,plain,
% 7.38/7.45 (E(a1,f7(a2,f6(a5)))),
% 7.38/7.45 inference(scs_inference,[],[1391,17,20])).
% 7.38/7.45 cnf(1399,plain,
% 7.38/7.45 (E(x13991,f7(f6(x13991),a4))),
% 7.38/7.45 inference(rename_variables,[],[287])).
% 7.38/7.45 cnf(1402,plain,
% 7.38/7.45 (P1(a2,f6(a5),f6(f6(a1)))),
% 7.38/7.45 inference(scs_inference,[],[1391,198,326,206,287,1399,17,20,8,7,9,22])).
% 7.38/7.45 cnf(1410,plain,
% 7.38/7.45 (P1(f6(a2),f6(a5),a1)),
% 7.38/7.45 inference(scs_inference,[],[1391,330,154,8,7])).
% 7.38/7.45 cnf(1418,plain,
% 7.38/7.45 (P1(a2,a1,a5)),
% 7.38/7.45 inference(scs_inference,[],[897,1391,1358,1189,1314,330,624,154,8,7,9,22,19])).
% 7.38/7.45 cnf(1420,plain,
% 7.38/7.45 (E(a5,f7(a2,a1))),
% 7.38/7.45 inference(scs_inference,[],[1418,17,20])).
% 7.38/7.45 cnf(1511,plain,
% 7.38/7.45 (P1(f7(f6(a4),f6(a2)),f6(a5),a1)),
% 7.38/7.45 inference(scs_inference,[],[1391,1135,143,1420,177,8,9,7])).
% 7.38/7.45 cnf(1513,plain,
% 7.38/7.45 (P1(f7(x15131,x15131),f7(f7(a1,a4),a5),f6(a2))),
% 7.38/7.45 inference(scs_inference,[],[1391,420,304,1135,143,145,1420,177,8,9,7,22])).
% 7.38/7.45 cnf(1521,plain,
% 7.38/7.45 (P1(f7(a2,f6(a5)),a5,a2)),
% 7.38/7.45 inference(scs_inference,[],[111,1513,1358,1393,422,626,8,9,7])).
% 7.38/7.45 cnf(1531,plain,
% 7.38/7.45 (P1(a2,f6(f6(a1)),a5)),
% 7.38/7.45 inference(scs_inference,[],[946,474,1402,1349,973,1410,269,206,624,8,9,7,22])).
% 7.38/7.45 cnf(1549,plain,
% 7.38/7.45 (P1(a2,a5,f7(a5,a2))),
% 7.38/7.45 inference(scs_inference,[],[1418,1511,1019,1256,363,688,176,17,8,9,7,22])).
% 7.38/7.45 cnf(1554,plain,
% 7.38/7.45 (E(x15541,f7(x15541,f6(a4)))),
% 7.38/7.45 inference(rename_variables,[],[349])).
% 7.38/7.45 cnf(1556,plain,
% 7.38/7.45 (E(x15561,f7(x15561,f6(a4)))),
% 7.38/7.45 inference(rename_variables,[],[349])).
% 7.38/7.45 cnf(1557,plain,
% 7.38/7.45 (P1(f7(a2,f6(a4)),a5,f7(a5,a2))),
% 7.38/7.45 inference(scs_inference,[],[1549,349,1554,1556,8,9,7])).
% 7.38/7.45 cnf(1564,plain,
% 7.38/7.45 (E(x15641,f7(x15641,a4))),
% 7.38/7.45 inference(rename_variables,[],[603])).
% 7.38/7.45 cnf(1566,plain,
% 7.38/7.45 (E(x15661,f7(x15661,a4))),
% 7.38/7.45 inference(rename_variables,[],[603])).
% 7.38/7.45 cnf(1567,plain,
% 7.38/7.45 (P1(f7(a2,a4),f6(f6(a1)),a5)),
% 7.38/7.45 inference(scs_inference,[],[1521,1531,603,1564,1566,8,9,7])).
% 7.38/7.45 cnf(1575,plain,
% 7.38/7.45 (E(f7(x15751,a4),f6(x15751))),
% 7.38/7.45 inference(rename_variables,[],[422])).
% 7.38/7.45 cnf(1584,plain,
% 7.38/7.45 (P1(a2,a5,f6(a1))),
% 7.38/7.45 inference(scs_inference,[],[474,600,1557,1567,1125,1385,206,422,1575,8,9,7,22,19])).
% 7.38/7.45 cnf(1590,plain,
% 7.38/7.45 (E(x15901,f7(f6(x15901),a4))),
% 7.38/7.45 inference(rename_variables,[],[287])).
% 7.38/7.45 cnf(1603,plain,
% 7.38/7.45 (P1(a1,a2,f6(a5))),
% 7.38/7.45 inference(scs_inference,[],[1584,948,173,326,312,330,287,1590,17,20,8,9,7,21,22,19])).
% 7.38/7.45 cnf(1605,plain,
% 7.38/7.45 (E(f7(a2,a5),f6(a1))),
% 7.38/7.45 inference(scs_inference,[],[1584,948,173,326,312,330,287,1590,17,20,8,9,7,21,22,19,2])).
% 7.38/7.45 cnf(1607,plain,
% 7.38/7.45 (P1(x16071,x16072,f7(x16071,x16072))),
% 7.38/7.45 inference(rename_variables,[],[17])).
% 7.38/7.45 cnf(1624,plain,
% 7.38/7.45 (~E(a3,f7(a1,a2))),
% 7.38/7.45 inference(scs_inference,[],[1603,948,173,1418,326,1605,391,1393,154,17,1607,20,8,7,9,21,22,19,2,3])).
% 7.38/7.45 cnf(1643,plain,
% 7.38/7.45 ($false),
% 7.38/7.45 inference(scs_inference,[],[10,1624,17,20]),
% 7.38/7.45 ['proof']).
% 7.38/7.45 % SZS output end Proof
% 7.38/7.45 % Total time :6.780000s
%------------------------------------------------------------------------------