%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP035-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n026.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:34 EDT 2024
% Result : Unsatisfiable 33.29s 33.37s
% Output : CNFRefutation 33.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP035-3 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.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 : Thu Jun 20 10:53:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.54/0.57 start to proof:theBenchmark
% 33.29/33.36 %-------------------------------------------
% 33.29/33.36 % File :CSE---1.7
% 33.29/33.36 % Problem :theBenchmark
% 33.29/33.36 % Transform :cnf
% 33.29/33.36 % Format :tptp:raw
% 33.29/33.36 % Command :java -jar mcs_scs.jar %d %s
% 33.29/33.36
% 33.29/33.36 % Result :Theorem 32.720000s
% 33.29/33.36 % Output :CNFRefutation 32.720000s
% 33.29/33.36 %-------------------------------------------
% 33.29/33.37 %--------------------------------------------------------------------------
% 33.29/33.37 % File : GRP035-3 : TPTP v8.2.0. Released v1.0.0.
% 33.29/33.37 % Domain : Group Theory (Subgroups)
% 33.29/33.37 % Problem : In subgroups, product is closed
% 33.29/33.37 % Version : [Wos65] axioms.
% 33.29/33.37 % English :
% 33.29/33.37
% 33.29/33.37 % Refs : [Wos65] Wos (1965), Unpublished Note
% 33.29/33.37 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 33.29/33.37 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 33.29/33.37 % Source : [SPRFN]
% 33.29/33.37 % Names : Problem 15 [Wos65]
% 33.29/33.37 % : wos15 [WM76]
% 33.29/33.37
% 33.29/33.37 % Status : Unsatisfiable
% 33.29/33.37 % Rating : 0.00 v6.0.0, 0.22 v5.5.0, 0.31 v5.4.0, 0.27 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 33.29/33.37 % Syntax : Number of clauses : 13 ( 9 unt; 0 nHn; 8 RR)
% 33.29/33.37 % Number of literals : 24 ( 1 equ; 12 neg)
% 33.29/33.37 % Maximal clause size : 4 ( 1 avg)
% 33.29/33.37 % Maximal term depth : 2 ( 1 avg)
% 33.29/33.37 % Number of predicates : 3 ( 2 usr; 0 prp; 1-3 aty)
% 33.29/33.37 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 33.29/33.37 % Number of variables : 25 ( 0 sgn)
% 33.29/33.37 % SPC : CNF_UNS_RFO_SEQ_HRN
% 33.29/33.37
% 33.29/33.37 % Comments : Proves one of the [MOW76] axioms.
% 33.29/33.37 %--------------------------------------------------------------------------
% 33.29/33.37 %----Include group theory axioms
% 33.29/33.37 include('Axioms/GRP003-0.ax').
% 33.29/33.37 %----Include sub-group theory axioms
% 33.29/33.37 include('Axioms/GRP003-2.ax').
% 33.29/33.37 %--------------------------------------------------------------------------
% 33.29/33.37 cnf(a_is_in_subgroup,hypothesis,
% 33.29/33.37 subgroup_member(a) ).
% 33.29/33.37
% 33.29/33.37 cnf(b_is_in_subgroup,hypothesis,
% 33.29/33.37 subgroup_member(b) ).
% 33.29/33.37
% 33.29/33.37 cnf(a_times_b_is_c,hypothesis,
% 33.29/33.37 product(a,b,c) ).
% 33.29/33.37
% 33.29/33.37 cnf(prove_c_is_in_subgroup,negated_conjecture,
% 33.29/33.37 ~ subgroup_member(c) ).
% 33.29/33.37
% 33.29/33.37 %--------------------------------------------------------------------------
% 33.29/33.37 %-------------------------------------------
% 33.29/33.37 % Proof found
% 33.29/33.37 % SZS status Theorem for theBenchmark
% 33.29/33.37 % SZS output start Proof
% 33.29/33.38 %ClaNum:23(EqnAxiom:10)
% 33.29/33.38 %VarNum:50(SingletonVarNum:25)
% 33.29/33.38 %MaxLitNum:4
% 33.29/33.38 %MaxfuncDepth:1
% 33.29/33.38 %SharedTerms:8
% 33.29/33.38 %goalClause: 19
% 33.29/33.38 %singleGoalClaCount:1
% 33.29/33.38 [11]P1(a1)
% 33.29/33.38 [12]P1(a2)
% 33.29/33.38 [13]P2(a1,a2,a3)
% 33.29/33.38 [19]~P1(a3)
% 33.29/33.38 [14]P2(x141,a4,x141)
% 33.29/33.38 [15]P2(a4,x151,x151)
% 33.29/33.38 [16]P2(x161,f5(x161),a4)
% 33.29/33.38 [17]P2(f5(x171),x171,a4)
% 33.29/33.38 [18]P2(x181,x182,f6(x181,x182))
% 33.29/33.38 [21]~P2(x213,x214,x211)+E(x211,x212)+~P2(x213,x214,x212)
% 33.29/33.38 [20]P1(x201)+~P1(x202)+~P1(x203)+~P2(x203,f5(x202),x201)
% 33.29/33.38 [22]~P2(x226,x224,x221)+P2(x221,x222,x223)+~P2(x224,x222,x225)+~P2(x226,x225,x223)
% 33.29/33.38 [23]~P2(x231,x236,x234)+P2(x231,x232,x233)+~P2(x234,x235,x233)+~P2(x236,x235,x232)
% 33.29/33.38 %EqnAxiom
% 33.29/33.38 [1]E(x11,x11)
% 33.29/33.38 [2]E(x22,x21)+~E(x21,x22)
% 33.29/33.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 33.29/33.38 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 33.29/33.38 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53))
% 33.29/33.38 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62))
% 33.29/33.38 [7]~P1(x71)+P1(x72)+~E(x71,x72)
% 33.29/33.38 [8]P2(x82,x83,x84)+~E(x81,x82)+~P2(x81,x83,x84)
% 33.29/33.38 [9]P2(x93,x92,x94)+~E(x91,x92)+~P2(x93,x91,x94)
% 33.29/33.38 [10]P2(x103,x104,x102)+~E(x101,x102)+~P2(x103,x104,x101)
% 33.29/33.38
% 33.29/33.38 %-------------------------------------------
% 33.29/33.39 cnf(24,plain,
% 33.29/33.39 (E(x241,f6(a4,x241))),
% 33.29/33.39 inference(scs_inference,[],[15,18,21])).
% 33.29/33.39 cnf(25,plain,
% 33.29/33.39 (P2(x251,x252,f6(x251,x252))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(28,plain,
% 33.29/33.39 (P2(a4,x281,x281)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(29,plain,
% 33.29/33.39 (P2(a4,f6(a4,a4),a4)),
% 33.29/33.39 inference(scs_inference,[],[15,28,18,21,8,9])).
% 33.29/33.39 cnf(30,plain,
% 33.29/33.39 (P2(a4,x301,x301)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(31,plain,
% 33.29/33.39 (P2(x311,f5(x311),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[15,28,18,16,21,8,9,10])).
% 33.29/33.39 cnf(32,plain,
% 33.29/33.39 (P1(f6(a1,f5(a1)))),
% 33.29/33.39 inference(scs_inference,[],[11,15,28,18,25,16,21,8,9,10,20])).
% 33.29/33.39 cnf(33,plain,
% 33.29/33.39 (P2(x331,x332,f6(x331,x332))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(35,plain,
% 33.29/33.39 (P2(f6(f5(x351),a4),x351,a4)),
% 33.29/33.39 inference(scs_inference,[],[11,15,28,30,18,25,33,16,17,21,8,9,10,20,22])).
% 33.29/33.39 cnf(37,plain,
% 33.29/33.39 (P2(x371,x372,f6(x371,x372))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(45,plain,
% 33.29/33.39 (~P1(a4)+P1(f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[11,15,28,30,18,25,33,37,16,17,21,8,9,10,20,22,23,2,7])).
% 33.29/33.39 cnf(46,plain,
% 33.29/33.39 (E(f6(a4,x461),x461)),
% 33.29/33.39 inference(scs_inference,[],[24,2])).
% 33.29/33.39 cnf(47,plain,
% 33.29/33.39 (P2(f6(f5(x471),a4),x471,f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[35,24,2,10])).
% 33.29/33.39 cnf(48,plain,
% 33.29/33.39 (E(x481,f6(a4,x481))),
% 33.29/33.39 inference(rename_variables,[],[24])).
% 33.29/33.39 cnf(51,plain,
% 33.29/33.39 (E(f6(f5(x511),x511),a4)),
% 33.29/33.39 inference(scs_inference,[],[35,18,17,24,48,2,10,9,21])).
% 33.29/33.39 cnf(53,plain,
% 33.29/33.39 (P2(x531,x532,f6(x531,x532))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(55,plain,
% 33.29/33.39 (P2(f6(a4,x551),x552,f6(x551,x552))),
% 33.29/33.39 inference(scs_inference,[],[35,18,53,17,24,48,2,10,9,21,8])).
% 33.29/33.39 cnf(57,plain,
% 33.29/33.39 (P2(a4,f5(f6(a4,a4)),a4)),
% 33.29/33.39 inference(scs_inference,[],[35,18,53,17,31,24,48,29,2,10,9,21,8,22])).
% 33.29/33.39 cnf(60,plain,
% 33.29/33.39 (P1(a4)),
% 33.29/33.39 inference(scs_inference,[],[32,35,18,53,17,16,31,24,48,29,2,10,9,21,8,22,20])).
% 33.29/33.39 cnf(70,plain,
% 33.29/33.39 (P1(f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[60,45])).
% 33.29/33.39 cnf(71,plain,
% 33.29/33.39 (E(a4,f6(f5(x711),x711))),
% 33.29/33.39 inference(scs_inference,[],[51,2])).
% 33.29/33.39 cnf(73,plain,
% 33.29/33.39 (E(f6(a4,x731),x731)),
% 33.29/33.39 inference(rename_variables,[],[46])).
% 33.29/33.39 cnf(74,plain,
% 33.29/33.39 (E(f6(a4,a4),f6(f5(x741),x741))),
% 33.29/33.39 inference(scs_inference,[],[19,46,73,51,2,7,3])).
% 33.29/33.39 cnf(75,plain,
% 33.29/33.39 (E(f6(a4,x751),x751)),
% 33.29/33.39 inference(rename_variables,[],[46])).
% 33.29/33.39 cnf(76,plain,
% 33.29/33.39 (E(a4,f5(f6(a4,a4)))),
% 33.29/33.39 inference(scs_inference,[],[19,57,15,46,73,51,2,7,3,21])).
% 33.29/33.39 cnf(77,plain,
% 33.29/33.39 (P2(a4,x771,x771)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(80,plain,
% 33.29/33.39 (E(x801,f6(a4,x801))),
% 33.29/33.39 inference(rename_variables,[],[24])).
% 33.29/33.39 cnf(81,plain,
% 33.29/33.39 (P2(x811,x812,f6(x811,f6(a4,x812)))),
% 33.29/33.39 inference(scs_inference,[],[19,57,15,18,46,73,75,51,24,2,7,3,21,10,9])).
% 33.29/33.39 cnf(82,plain,
% 33.29/33.39 (P2(x821,x822,f6(x821,x822))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(83,plain,
% 33.29/33.39 (P2(f6(a4,a4),x831,x831)),
% 33.29/33.39 inference(scs_inference,[],[19,57,15,77,18,46,73,75,51,24,80,2,7,3,21,10,9,8])).
% 33.29/33.39 cnf(85,plain,
% 33.29/33.39 (P1(f5(a4))),
% 33.29/33.39 inference(scs_inference,[],[19,60,57,15,77,18,46,73,75,51,24,80,2,7,3,21,10,9,8,20])).
% 33.29/33.39 cnf(86,plain,
% 33.29/33.39 (P2(a4,x861,x861)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(88,plain,
% 33.29/33.39 (P2(a4,f6(x881,x882),f6(f6(a4,x881),x882))),
% 33.29/33.39 inference(scs_inference,[],[19,60,57,15,77,86,18,82,55,46,73,75,51,24,80,2,7,3,21,10,9,8,20,23])).
% 33.29/33.39 cnf(96,plain,
% 33.29/33.39 (E(f6(f5(x961),x961),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[74,2])).
% 33.29/33.39 cnf(97,plain,
% 33.29/33.39 (E(f5(a4),a4)),
% 33.29/33.39 inference(scs_inference,[],[15,16,74,2,21])).
% 33.29/33.39 cnf(99,plain,
% 33.29/33.39 (P2(a4,x991,x991)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(101,plain,
% 33.29/33.39 (E(f6(a4,a4),f5(f6(a4,a4)))),
% 33.29/33.39 inference(scs_inference,[],[15,16,74,76,46,2,21,3])).
% 33.29/33.39 cnf(104,plain,
% 33.29/33.39 (P2(f5(x1041),x1041,f6(f5(x1042),x1042))),
% 33.29/33.39 inference(scs_inference,[],[70,17,15,16,74,71,76,46,2,21,3,7,10])).
% 33.29/33.39 cnf(105,plain,
% 33.29/33.39 (P2(a4,f6(f5(x1051),x1051),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[70,17,15,99,16,74,71,76,46,2,21,3,7,10,9])).
% 33.29/33.39 cnf(106,plain,
% 33.29/33.39 (P2(a4,x1061,x1061)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(109,plain,
% 33.29/33.39 (P2(f6(f5(a1),a4),a3,a2)),
% 33.29/33.39 inference(scs_inference,[],[70,35,17,15,99,106,16,74,71,76,13,46,24,2,21,3,7,10,9,8,23])).
% 33.29/33.39 cnf(116,plain,
% 33.29/33.39 (E(f5(f6(a4,a4)),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[101,2])).
% 33.29/33.39 cnf(117,plain,
% 33.29/33.39 (E(f6(x1171,f5(x1171)),a4)),
% 33.29/33.39 inference(scs_inference,[],[18,16,101,2,21])).
% 33.29/33.39 cnf(119,plain,
% 33.29/33.39 (P2(x1191,x1192,f6(x1191,x1192))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(122,plain,
% 33.29/33.39 (E(f5(a4),f5(f6(a4,a4)))),
% 33.29/33.39 inference(scs_inference,[],[70,18,16,101,97,76,2,21,7,3])).
% 33.29/33.39 cnf(123,plain,
% 33.29/33.39 (P2(f5(x1231),x1231,f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[70,18,119,16,96,101,97,76,2,21,7,3,10])).
% 33.29/33.39 cnf(124,plain,
% 33.29/33.39 (P2(x1241,x1242,f6(x1241,x1242))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(126,plain,
% 33.29/33.39 (P2(a4,x1261,x1261)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(127,plain,
% 33.29/33.39 (P2(f5(f6(a4,a4)),x1271,x1271)),
% 33.29/33.39 inference(scs_inference,[],[70,18,119,15,126,16,96,101,97,76,2,21,7,3,10,9,8])).
% 33.29/33.39 cnf(128,plain,
% 33.29/33.39 (P2(x1281,a3,f6(f6(x1281,a1),f6(a4,a2)))),
% 33.29/33.39 inference(scs_inference,[],[70,18,119,124,15,126,16,96,101,81,97,76,13,2,21,7,3,10,9,8,23])).
% 33.29/33.39 cnf(132,plain,
% 33.29/33.39 (E(f5(f6(a4,a4)),f5(a4))),
% 33.29/33.39 inference(scs_inference,[],[122,2])).
% 33.29/33.39 cnf(133,plain,
% 33.29/33.39 (E(f6(f6(a4,a4),x1331),x1331)),
% 33.29/33.39 inference(scs_inference,[],[18,83,122,2,21])).
% 33.29/33.39 cnf(135,plain,
% 33.29/33.39 (P2(x1351,x1352,f6(x1351,x1352))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(137,plain,
% 33.29/33.39 (E(f5(a4),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[18,83,116,122,2,21,3])).
% 33.29/33.39 cnf(138,plain,
% 33.29/33.39 (~P1(f6(f6(a4,a4),a3))),
% 33.29/33.39 inference(scs_inference,[],[19,18,83,116,122,2,21,3,7])).
% 33.29/33.39 cnf(141,plain,
% 33.29/33.39 (P2(x1411,f5(x1411),f6(f5(x1412),x1412))),
% 33.29/33.39 inference(scs_inference,[],[19,18,15,16,83,116,122,71,2,21,3,7,9,10])).
% 33.29/33.39 cnf(142,plain,
% 33.29/33.39 (P2(f6(a4,a4),f6(a4,a4),a4)),
% 33.29/33.39 inference(scs_inference,[],[19,18,17,15,16,83,116,122,71,2,21,3,7,9,10,8])).
% 33.29/33.39 cnf(144,plain,
% 33.29/33.39 (P2(f6(f5(a1),a4),a3,f6(a4,a2))),
% 33.29/33.39 inference(scs_inference,[],[19,35,18,135,17,15,16,83,116,122,71,13,2,21,3,7,9,10,8,23])).
% 33.29/33.39 cnf(148,plain,
% 33.29/33.39 (E(x1481,f6(f6(a4,a4),x1481))),
% 33.29/33.39 inference(scs_inference,[],[133,2])).
% 33.29/33.39 cnf(149,plain,
% 33.29/33.39 (E(f6(x1491,f5(x1491)),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[18,133,31,2,21])).
% 33.29/33.39 cnf(151,plain,
% 33.29/33.39 (P2(x1511,x1512,f6(x1511,x1512))),
% 33.29/33.39 inference(rename_variables,[],[18])).
% 33.29/33.39 cnf(153,plain,
% 33.29/33.39 (E(f6(f6(a4,a4),f5(a4)),f6(a4,a4))),
% 33.29/33.39 inference(scs_inference,[],[18,133,137,31,2,21,3])).
% 33.29/33.39 cnf(154,plain,
% 33.29/33.39 (E(f6(f6(a4,a4),x1541),x1541)),
% 33.29/33.39 inference(rename_variables,[],[133])).
% 33.29/33.39 cnf(156,plain,
% 33.29/33.39 (P2(a4,x1561,x1561)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(158,plain,
% 33.29/33.39 (P2(a4,x1581,x1581)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(159,plain,
% 33.29/33.39 (P2(f6(f5(x1591),x1591),x1592,x1592)),
% 33.29/33.39 inference(scs_inference,[],[18,15,156,158,133,154,137,31,71,2,21,3,10,9,8])).
% 33.29/33.39 cnf(160,plain,
% 33.29/33.39 (P2(f6(a4,a4),a4,f6(a4,f6(a4,a4)))),
% 33.29/33.39 inference(scs_inference,[],[18,151,15,156,158,133,154,137,142,31,71,2,21,3,10,9,8,23])).
% 33.29/33.39 cnf(164,plain,
% 33.29/33.39 (E(f6(a4,a4),f6(x1641,f5(x1641)))),
% 33.29/33.39 inference(scs_inference,[],[149,2])).
% 33.29/33.39 cnf(165,plain,
% 33.29/33.39 (E(f6(f6(a4,x1651),x1652),f6(x1651,x1652))),
% 33.29/33.39 inference(scs_inference,[],[18,149,55,2,21])).
% 33.29/33.39 cnf(169,plain,
% 33.29/33.39 (E(f5(f6(a4,a4)),a4)),
% 33.29/33.39 inference(scs_inference,[],[18,148,149,117,55,2,21,3])).
% 33.29/33.39 cnf(171,plain,
% 33.29/33.39 (E(x1711,f6(f6(a4,a4),x1711))),
% 33.29/33.39 inference(rename_variables,[],[148])).
% 33.29/33.39 cnf(173,plain,
% 33.29/33.39 (P2(f5(x1731),x1731,f6(f6(a4,a4),a4))),
% 33.29/33.39 inference(scs_inference,[],[70,17,18,148,171,149,117,55,2,21,3,7,10])).
% 33.29/33.39 cnf(174,plain,
% 33.29/33.39 (E(x1741,f6(f6(a4,a4),x1741))),
% 33.29/33.39 inference(rename_variables,[],[148])).
% 33.29/33.39 cnf(176,plain,
% 33.29/33.39 (P2(f5(x1761),x1761,a4)),
% 33.29/33.39 inference(rename_variables,[],[17])).
% 33.29/33.39 cnf(177,plain,
% 33.29/33.39 (P2(f6(f6(a4,a4),f5(x1771)),x1771,a4)),
% 33.29/33.39 inference(scs_inference,[],[70,17,176,18,148,171,174,149,117,55,2,21,3,7,10,9,8])).
% 33.29/33.39 cnf(179,plain,
% 33.29/33.39 (E(f6(x1791,x1792),f6(f6(a4,x1791),x1792))),
% 33.29/33.39 inference(scs_inference,[],[165,2])).
% 33.29/33.39 cnf(180,plain,
% 33.29/33.39 (E(f5(a4),f6(f5(x1801),x1801))),
% 33.29/33.39 inference(scs_inference,[],[15,141,165,2,21])).
% 33.29/33.39 cnf(182,plain,
% 33.29/33.39 (P2(a4,x1821,x1821)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(184,plain,
% 33.29/33.39 (E(f6(a4,a4),f5(a4))),
% 33.29/33.39 inference(scs_inference,[],[15,141,164,165,46,2,21,3])).
% 33.29/33.39 cnf(186,plain,
% 33.29/33.39 (E(f6(a4,a4),f6(x1861,f5(x1861)))),
% 33.29/33.39 inference(rename_variables,[],[164])).
% 33.29/33.39 cnf(188,plain,
% 33.29/33.39 (P2(a4,x1881,x1881)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(190,plain,
% 33.29/33.39 (P2(a4,x1901,x1901)),
% 33.29/33.39 inference(rename_variables,[],[15])).
% 33.29/33.39 cnf(191,plain,
% 33.29/33.39 (P2(f6(f6(a4,a4),a4),x1911,x1911)),
% 33.29/33.39 inference(scs_inference,[],[15,182,188,190,141,164,186,165,148,46,2,21,3,10,9,8])).
% 33.29/33.40 cnf(193,plain,
% 33.29/33.40 (P2(a4,f6(f6(a4,a4),a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[57,15,182,188,190,141,164,186,173,165,148,46,2,21,3,10,9,8,23])).
% 33.29/33.40 cnf(197,plain,
% 33.29/33.40 (E(f6(a4,a4),f6(f6(a4,a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[153,2])).
% 33.29/33.40 cnf(198,plain,
% 33.29/33.40 (E(f6(f6(a4,a4),f5(a4)),a4)),
% 33.29/33.40 inference(scs_inference,[],[153,46,2,3])).
% 33.29/33.40 cnf(204,plain,
% 33.29/33.40 (P2(f6(f5(x2041),x2041),a4,f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[18,16,123,179,153,180,46,2,3,10,9,8])).
% 33.29/33.40 cnf(206,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(f6(a4,a4),a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[18,16,191,123,179,153,193,180,46,2,3,10,9,8,22])).
% 33.29/33.40 cnf(209,plain,
% 33.29/33.40 (E(a4,f6(f6(a4,a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[198,2])).
% 33.29/33.40 cnf(210,plain,
% 33.29/33.40 (E(f6(x2101,f5(x2101)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[184,198,149,2,3])).
% 33.29/33.40 cnf(212,plain,
% 33.29/33.40 (P2(a4,x2121,x2121)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(215,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),f5(a4)),a4,f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[15,212,197,184,14,198,149,2,3,10,9,8])).
% 33.29/33.40 cnf(217,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(f5(x2171),x2171),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[15,212,159,197,184,14,105,198,149,2,3,10,9,8,22])).
% 33.29/33.40 cnf(225,plain,
% 33.29/33.40 (E(f5(a4),f6(x2251,f5(x2251)))),
% 33.29/33.40 inference(scs_inference,[],[210,2])).
% 33.29/33.40 cnf(226,plain,
% 33.29/33.40 (E(a4,f6(a4,f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[210,209,165,2,3])).
% 33.29/33.40 cnf(228,plain,
% 33.29/33.40 (P2(f5(x2281),x2281,f6(f6(a4,a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[17,210,209,165,2,3,10])).
% 33.29/33.40 cnf(230,plain,
% 33.29/33.40 (P2(a4,x2301,x2301)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(231,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),f5(a4)),x2311,x2311)),
% 33.29/33.40 inference(scs_inference,[],[17,15,230,210,209,165,2,3,10,9,8])).
% 33.29/33.40 cnf(237,plain,
% 33.29/33.40 (E(a4,f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[97,2])).
% 33.29/33.40 cnf(238,plain,
% 33.29/33.40 (E(f5(a4),f6(f6(a4,x2381),f5(x2381)))),
% 33.29/33.40 inference(scs_inference,[],[225,97,179,2,3])).
% 33.29/33.40 cnf(240,plain,
% 33.29/33.40 (P2(x2401,f5(x2401),f6(a4,f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[16,225,226,97,179,2,3,10])).
% 33.29/33.40 cnf(242,plain,
% 33.29/33.40 (P2(x2421,f5(x2421),a4)),
% 33.29/33.40 inference(rename_variables,[],[16])).
% 33.29/33.40 cnf(244,plain,
% 33.29/33.40 (P2(f5(x2441),x2441,a4)),
% 33.29/33.40 inference(rename_variables,[],[17])).
% 33.29/33.40 cnf(245,plain,
% 33.29/33.40 (P2(a4,f6(f6(a4,a4),f5(a4)),a4)),
% 33.29/33.40 inference(scs_inference,[],[16,242,17,244,231,225,226,97,179,2,3,10,9,8,22])).
% 33.29/33.40 cnf(251,plain,
% 33.29/33.40 (E(f6(f6(a4,x2511),f5(x2511)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[238,2])).
% 33.29/33.40 cnf(252,plain,
% 33.29/33.40 (P2(f6(f5(x2521),a4),x2521,f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[35,238,237,2,10])).
% 33.29/33.40 cnf(256,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(f6(a4,a4),f5(a4)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[245,35,15,169,238,204,237,2,10,9,8,22])).
% 33.29/33.40 cnf(262,plain,
% 33.29/33.40 (E(a4,f6(x2621,f5(x2621)))),
% 33.29/33.40 inference(scs_inference,[],[117,2])).
% 33.29/33.40 cnf(263,plain,
% 33.29/33.40 (E(f6(a4,a4),f6(f6(a4,x2631),f5(x2631)))),
% 33.29/33.40 inference(scs_inference,[],[164,117,179,2,3])).
% 33.29/33.40 cnf(265,plain,
% 33.29/33.40 (P2(f6(a4,a4),f5(a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[256,251,164,117,179,2,3,9])).
% 33.29/33.40 cnf(266,plain,
% 33.29/33.40 (E(f6(f6(a4,x2661),f5(x2661)),f5(a4))),
% 33.29/33.40 inference(rename_variables,[],[251])).
% 33.29/33.40 cnf(267,plain,
% 33.29/33.40 (P2(f6(a4,x2671),f5(x2671),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[256,18,251,266,164,117,179,2,3,9,10])).
% 33.29/33.40 cnf(269,plain,
% 33.29/33.40 (P2(f5(a4),f6(a4,a4),a4)),
% 33.29/33.40 inference(scs_inference,[],[256,18,17,132,251,266,164,117,179,2,3,9,10,8])).
% 33.29/33.40 cnf(271,plain,
% 33.29/33.40 (P2(a4,f6(f6(a4,a4),a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[206,256,35,18,17,132,252,251,266,164,117,179,2,3,9,10,8,22])).
% 33.29/33.40 cnf(280,plain,
% 33.29/33.40 (E(f6(f6(a4,x2801),f5(x2801)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[263,2])).
% 33.29/33.40 cnf(281,plain,
% 33.29/33.40 (E(f5(a4),f6(f6(a4,a4),a4))),
% 33.29/33.40 inference(scs_inference,[],[271,15,263,2,21])).
% 33.29/33.40 cnf(284,plain,
% 33.29/33.40 (E(a4,f6(f6(a4,x2841),f5(x2841)))),
% 33.29/33.40 inference(scs_inference,[],[271,15,262,263,179,2,21,3])).
% 33.29/33.40 cnf(286,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(f6(a4,a4),a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[271,206,15,262,184,263,179,2,21,3,10])).
% 33.29/33.40 cnf(287,plain,
% 33.29/33.40 (P2(x2871,f6(x2872,f5(x2872)),f6(x2871,a4))),
% 33.29/33.40 inference(scs_inference,[],[271,206,18,15,262,184,263,179,2,21,3,10,9])).
% 33.29/33.40 cnf(288,plain,
% 33.29/33.40 (P2(x2881,x2882,f6(x2881,x2882))),
% 33.29/33.40 inference(rename_variables,[],[18])).
% 33.29/33.40 cnf(289,plain,
% 33.29/33.40 (P2(f5(a4),f6(f6(a4,a4),a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[271,206,18,15,262,184,263,179,2,21,3,10,9,8])).
% 33.29/33.40 cnf(290,plain,
% 33.29/33.40 (P2(f5(a4),f6(f6(a4,a4),a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[271,206,18,15,262,191,184,263,179,2,21,3,10,9,8,22])).
% 33.29/33.40 cnf(291,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),a4),x2911,x2911)),
% 33.29/33.40 inference(rename_variables,[],[191])).
% 33.29/33.40 cnf(293,plain,
% 33.29/33.40 (P2(a4,x2931,f6(f5(a4),x2931))),
% 33.29/33.40 inference(scs_inference,[],[271,206,18,288,15,262,191,291,184,263,179,2,21,3,10,9,8,22,23])).
% 33.29/33.40 cnf(297,plain,
% 33.29/33.40 (E(f6(f6(a4,a4),a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[281,2])).
% 33.29/33.40 cnf(299,plain,
% 33.29/33.40 (E(f6(f6(a4,x2991),f5(x2991)),a4)),
% 33.29/33.40 inference(scs_inference,[],[85,280,281,46,2,7,3])).
% 33.29/33.40 cnf(301,plain,
% 33.29/33.40 (P2(x3011,f5(x3011),f6(f6(a4,x3012),f5(x3012)))),
% 33.29/33.40 inference(scs_inference,[],[85,16,280,281,284,46,2,7,3,10])).
% 33.29/33.40 cnf(303,plain,
% 33.29/33.40 (P2(a4,x3031,x3031)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(304,plain,
% 33.29/33.40 (P2(f6(f6(a4,x3041),f5(x3041)),x3042,x3042)),
% 33.29/33.40 inference(scs_inference,[],[85,16,15,303,280,281,284,46,2,7,3,10,9,8])).
% 33.29/33.40 cnf(305,plain,
% 33.29/33.40 (P2(a4,f6(f6(a4,x3051),f5(x3051)),a4)),
% 33.29/33.40 inference(scs_inference,[],[85,16,17,15,303,280,281,284,46,2,7,3,10,9,8,22])).
% 33.29/33.40 cnf(314,plain,
% 33.29/33.40 (E(f6(f5(x3141),x3141),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[180,2])).
% 33.29/33.40 cnf(315,plain,
% 33.29/33.40 (P2(f6(a4,a4),a4,f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[18,297,180,2,10])).
% 33.29/33.40 cnf(317,plain,
% 33.29/33.40 (P2(f5(a4),f5(a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[290,18,297,180,2,10,9])).
% 33.29/33.40 cnf(318,plain,
% 33.29/33.40 (P2(f6(a4,a4),a4,f6(f5(x3181),x3181))),
% 33.29/33.40 inference(scs_inference,[],[290,18,104,297,137,180,2,10,9,8])).
% 33.29/33.40 cnf(320,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(f6(a4,x3201),f5(x3201)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[290,305,18,104,297,215,137,180,2,10,9,8,22])).
% 33.29/33.40 cnf(322,plain,
% 33.29/33.40 (P2(x3221,f5(x3221),f6(f6(a4,a4),a4))),
% 33.29/33.40 inference(scs_inference,[],[16,148,10])).
% 33.29/33.40 cnf(326,plain,
% 33.29/33.40 (P2(f6(x3261,f5(x3261)),f5(a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[16,240,265,169,164,148,10,9,8])).
% 33.29/33.40 cnf(327,plain,
% 33.29/33.40 (P2(a4,f6(f6(a4,x3271),f5(x3271)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[320,17,16,240,127,265,169,164,148,10,9,8,22])).
% 33.29/33.40 cnf(332,plain,
% 33.29/33.40 (P2(a4,a4,f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[305,271,133,237,10,9])).
% 33.29/33.40 cnf(335,plain,
% 33.29/33.40 (P2(f6(a4,a4),f5(a4),a4)),
% 33.29/33.40 inference(scs_inference,[],[327,305,271,16,304,133,237,10,9,8,22])).
% 33.29/33.40 cnf(348,plain,
% 33.29/33.40 (P2(f5(a4),f6(f6(a4,x3481),f5(x3481)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[335,305,315,238,101,262,10,9,8,22])).
% 33.29/33.40 cnf(350,plain,
% 33.29/33.40 (P2(f6(a4,a4),a4,f5(f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[335,305,15,16,315,238,101,262,10,9,8,22,23])).
% 33.29/33.40 cnf(354,plain,
% 33.29/33.40 (P2(f5(a4),f6(a4,a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[317,137,9])).
% 33.29/33.40 cnf(357,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(a4,a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[348,271,335,317,289,137,284,9,10,8,23])).
% 33.29/33.40 cnf(360,plain,
% 33.29/33.40 (P2(x3601,f6(a4,a4),f6(x3601,a4))),
% 33.29/33.40 inference(scs_inference,[],[348,287,149,97,10,9])).
% 33.29/33.40 cnf(368,plain,
% 33.29/33.40 (P2(f6(a4,f6(a4,a4)),f5(a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[267,132,9])).
% 33.29/33.40 cnf(373,plain,
% 33.29/33.40 (P2(f6(a4,x3731),f5(x3731),a4)),
% 33.29/33.40 inference(scs_inference,[],[18,299,10])).
% 33.29/33.40 cnf(374,plain,
% 33.29/33.40 (P2(x3741,x3742,f6(x3741,x3742))),
% 33.29/33.40 inference(rename_variables,[],[18])).
% 33.29/33.40 cnf(376,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),f6(a4,a4)),f5(a4),a4)),
% 33.29/33.40 inference(scs_inference,[],[335,18,299,281,148,10,9,8])).
% 33.29/33.40 cnf(381,plain,
% 33.29/33.40 (P1(f6(a4,f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[60,70,335,18,374,354,299,281,148,10,9,8,23,20])).
% 33.29/33.40 cnf(387,plain,
% 33.29/33.40 (P2(f5(a4),f6(f5(x3871),x3871),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[381,217,332,184,76,179,7,9,10,8])).
% 33.29/33.40 cnf(388,plain,
% 33.29/33.40 (P2(f5(a4),f5(f6(a4,a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[381,217,332,127,184,76,179,7,9,10,8,22])).
% 33.29/33.40 cnf(395,plain,
% 33.29/33.40 (P2(f5(x3951),x3951,f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[18,314,10])).
% 33.29/33.40 cnf(397,plain,
% 33.29/33.40 (P2(x3971,f5(f6(a4,a4)),f6(x3971,a4))),
% 33.29/33.40 inference(scs_inference,[],[18,360,314,101,10,9])).
% 33.29/33.40 cnf(400,plain,
% 33.29/33.40 (P2(f5(a4),f6(a4,a4),f6(f6(a4,a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[388,17,18,228,360,376,314,165,101,10,9,8,22])).
% 33.29/33.40 cnf(408,plain,
% 33.29/33.40 (P2(x4081,f5(x4081),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[322,269,297,74,9,10])).
% 33.29/33.40 cnf(409,plain,
% 33.29/33.40 (P2(f5(a4),f5(a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[322,269,326,297,210,74,9,10,8])).
% 33.29/33.40 cnf(411,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),f5(a4)),a4,f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[400,322,350,269,326,297,210,74,9,10,8,22])).
% 33.29/33.40 cnf(421,plain,
% 33.29/33.40 (P2(f6(a4,a4),a4,f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[411,327,397,409,293,51,122,10,9,8,22])).
% 33.29/33.40 cnf(423,plain,
% 33.29/33.40 (P2(a4,f6(f6(a4,x4231),f5(x4231)),f6(a4,a4))),
% 33.29/33.40 inference(rename_variables,[],[327])).
% 33.29/33.40 cnf(425,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),f5(a4)),f6(a4,a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[411,327,423,348,397,409,293,51,122,10,9,8,22,23])).
% 33.29/33.40 cnf(428,plain,
% 33.29/33.40 (E(f6(f5(a4),f5(a4)),a4)),
% 33.29/33.40 inference(scs_inference,[],[421,83,21])).
% 33.29/33.40 cnf(438,plain,
% 33.29/33.40 (P2(a4,a4,f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[421,17,301,88,373,83,251,169,127,117,21,9,10,8,22])).
% 33.29/33.40 cnf(444,plain,
% 33.29/33.40 (E(a4,f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[421,400,411,17,301,88,373,83,251,169,127,117,21,9,10,8,22,23,2])).
% 33.29/33.40 cnf(447,plain,
% 33.29/33.40 (E(f6(f5(a4),f5(a4)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[438,18,21])).
% 33.29/33.40 cnf(450,plain,
% 33.29/33.40 (E(f6(f5(a4),f5(a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[438,18,428,237,21,3])).
% 33.29/33.40 cnf(451,plain,
% 33.29/33.40 (P2(f5(a4),f6(a4,a4),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[438,18,387,428,96,237,21,3,9])).
% 33.29/33.40 cnf(453,plain,
% 33.29/33.40 (P2(f6(f5(a4),f5(a4)),x4531,x4531)),
% 33.29/33.40 inference(scs_inference,[],[438,15,18,387,428,444,96,237,21,3,9,8])).
% 33.29/33.40 cnf(454,plain,
% 33.29/33.40 (P2(f5(x4541),x4541,f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[438,17,15,18,387,428,444,96,237,21,3,9,8,10])).
% 33.29/33.40 cnf(455,plain,
% 33.29/33.40 (P2(a4,f6(f5(a4),f5(a4)),a4)),
% 33.29/33.40 inference(scs_inference,[],[438,17,15,16,18,387,428,444,96,237,21,3,9,8,10,22])).
% 33.29/33.40 cnf(462,plain,
% 33.29/33.40 (E(f6(a4,a4),f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[438,320,421,411,17,15,16,18,387,428,444,96,237,21,3,9,8,10,22,23,2])).
% 33.29/33.40 cnf(463,plain,
% 33.29/33.40 (E(f5(a4),f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[450,2])).
% 33.29/33.40 cnf(467,plain,
% 33.29/33.40 (P2(a4,x4671,x4671)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(470,plain,
% 33.29/33.40 (P2(f5(a4),f6(f5(a4),f5(a4)),a4)),
% 33.29/33.40 inference(scs_inference,[],[455,411,15,467,462,454,450,177,132,2,8,9,10,22])).
% 33.29/33.40 cnf(473,plain,
% 33.29/33.40 (P2(f5(a4),f6(a4,f6(a4,a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[455,400,411,15,467,160,462,454,450,177,132,2,8,9,10,22,23])).
% 33.29/33.40 cnf(475,plain,
% 33.29/33.40 (P2(a4,f6(a4,a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[425,299,8])).
% 33.29/33.40 cnf(478,plain,
% 33.29/33.40 (P2(x4781,f5(x4781),f5(a4))),
% 33.29/33.40 inference(rename_variables,[],[408])).
% 33.29/33.40 cnf(480,plain,
% 33.29/33.40 (P2(a4,f5(f5(a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[470,16,453,425,408,478,463,299,444,8,9,10,22])).
% 33.29/33.40 cnf(488,plain,
% 33.29/33.40 (E(f5(a4),f5(f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[480,15,21])).
% 33.29/33.40 cnf(489,plain,
% 33.29/33.40 (P2(a4,x4891,x4891)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(492,plain,
% 33.29/33.40 (P2(a4,a3,f6(a1,f6(a4,a2)))),
% 33.29/33.40 inference(scs_inference,[],[480,15,451,128,462,165,21,9,10])).
% 33.29/33.40 cnf(496,plain,
% 33.29/33.40 (P2(f5(a4),f5(a4),a4)),
% 33.29/33.40 inference(scs_inference,[],[480,17,15,489,451,128,475,462,165,71,21,9,10,8,22])).
% 33.29/33.40 cnf(502,plain,
% 33.29/33.40 (E(f5(f5(a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[488,2])).
% 33.29/33.40 cnf(507,plain,
% 33.29/33.40 (P2(a4,f5(a4),f6(f5(a4),f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[496,17,488,265,81,262,2,10,9,8,22])).
% 33.29/33.40 cnf(516,plain,
% 33.29/33.40 (E(f5(f5(a4)),a4)),
% 33.29/33.40 inference(scs_inference,[],[507,16,502,97,21,3])).
% 33.29/33.40 cnf(526,plain,
% 33.29/33.40 (E(a4,f6(f5(a4),f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[507,496,400,411,16,318,502,141,463,304,97,284,21,3,8,9,10,22,23,2])).
% 33.29/33.40 cnf(527,plain,
% 33.29/33.40 (E(a4,f5(f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[516,2])).
% 33.29/33.40 cnf(528,plain,
% 33.29/33.40 (E(f6(f5(a4),f6(a4,a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[507,516,408,2,21])).
% 33.29/33.40 cnf(538,plain,
% 33.29/33.40 (E(f5(a4),f6(f5(a4),f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[528,2])).
% 33.29/33.40 cnf(539,plain,
% 33.29/33.40 (E(f6(f5(a4),f6(a4,a4)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[528,137,2,3])).
% 33.29/33.40 cnf(540,plain,
% 33.29/33.40 (P2(f5(f5(a4)),x5401,x5401)),
% 33.29/33.40 inference(scs_inference,[],[15,528,527,137,2,3,8])).
% 33.29/33.40 cnf(551,plain,
% 33.29/33.40 (E(f6(a4,a4),f6(f5(a4),f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[539,2])).
% 33.29/33.40 cnf(557,plain,
% 33.29/33.40 (P2(f5(a4),x5571,x5571)),
% 33.29/33.40 inference(scs_inference,[],[540,502,8])).
% 33.29/33.40 cnf(559,plain,
% 33.29/33.40 (P2(f5(x5591),x5591,f6(f5(a4),f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[17,540,332,502,526,8,9,10])).
% 33.29/33.40 cnf(572,plain,
% 33.29/33.40 (P2(f6(f5(a1),a4),f6(a4,a3),f6(a4,a2))),
% 33.29/33.40 inference(scs_inference,[],[144,269,538,24,8,9])).
% 33.29/33.40 cnf(578,plain,
% 33.29/33.40 (P2(f6(a4,a4),f6(a4,a4),f6(f6(a4,x5781),f5(x5781)))),
% 33.29/33.40 inference(scs_inference,[],[357,301,551,516,238,8,9,10])).
% 33.29/33.40 cnf(580,plain,
% 33.29/33.40 (P2(x5801,f6(f5(a4),f5(a4)),x5801)),
% 33.29/33.40 inference(scs_inference,[],[496,14,281,444,8,9])).
% 33.29/33.40 cnf(587,plain,
% 33.29/33.40 (P2(x5871,f6(a4,a4),x5871)),
% 33.29/33.40 inference(scs_inference,[],[447,559,580,116,8,9])).
% 33.29/33.40 cnf(588,plain,
% 33.29/33.40 (P2(f6(a4,x5881),f5(x5881),f6(f5(a4),f5(a4)))),
% 33.29/33.40 inference(scs_inference,[],[447,559,580,267,116,463,8,9,10])).
% 33.29/33.40 cnf(600,plain,
% 33.29/33.40 (P2(f5(x6001),x6001,f6(f6(a4,x6002),f5(x6002)))),
% 33.29/33.40 inference(scs_inference,[],[17,475,142,462,284,8,9,10])).
% 33.29/33.40 cnf(605,plain,
% 33.29/33.40 (P2(x6051,f6(f6(a4,x6052),f5(x6052)),x6051)),
% 33.29/33.40 inference(scs_inference,[],[587,265,263,8,9])).
% 33.29/33.40 cnf(610,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),a4),f6(a4,a4),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[475,148,8])).
% 33.29/33.40 cnf(612,plain,
% 33.29/33.40 (P2(x6121,f6(x6122,f5(x6122)),x6121)),
% 33.29/33.40 inference(scs_inference,[],[587,475,164,148,8,9])).
% 33.29/33.40 cnf(613,plain,
% 33.29/33.40 (P2(f5(x6131),x6131,f6(x6132,f5(x6132)))),
% 33.29/33.40 inference(scs_inference,[],[123,587,475,164,148,8,9,10])).
% 33.29/33.40 cnf(618,plain,
% 33.29/33.40 (P2(f6(f5(a1),a4),f6(a4,a3),a2)),
% 33.29/33.40 inference(scs_inference,[],[368,109,179,24,8,9])).
% 33.29/33.40 cnf(641,plain,
% 33.29/33.40 (E(f6(f6(a4,a4),x6411),x6411)),
% 33.29/33.40 inference(rename_variables,[],[133])).
% 33.29/33.40 cnf(642,plain,
% 33.29/33.40 (P2(f5(x6421),x6421,f5(f6(a4,a4)))),
% 33.29/33.40 inference(scs_inference,[],[612,613,332,133,641,526,8,9,10])).
% 33.29/33.40 cnf(645,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),a1),a2,a3)),
% 33.29/33.40 inference(scs_inference,[],[13,148,8])).
% 33.29/33.40 cnf(647,plain,
% 33.29/33.40 (P2(x6471,f5(f5(a4)),x6471)),
% 33.29/33.40 inference(scs_inference,[],[14,13,527,148,8,9])).
% 33.29/33.40 cnf(651,plain,
% 33.29/33.40 (E(x6511,f6(a4,x6511))),
% 33.29/33.40 inference(rename_variables,[],[24])).
% 33.29/33.40 cnf(652,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),a1),a2,f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[492,645,332,71,24,651,8,9,10])).
% 33.29/33.40 cnf(654,plain,
% 33.29/33.40 (P2(a1,a2,f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[652,133,8])).
% 33.29/33.40 cnf(657,plain,
% 33.29/33.40 (P2(f6(a4,x6571),f5(x6571),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[647,588,652,447,502,133,8,9,10])).
% 33.29/33.40 cnf(665,plain,
% 33.29/33.40 (P2(f6(f5(a4),f6(a4,a4)),x6651,f6(a4,x6651))),
% 33.29/33.40 inference(scs_inference,[],[55,551,8])).
% 33.29/33.40 cnf(667,plain,
% 33.29/33.40 (P2(a1,f6(f6(a4,a4),a2),f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[654,55,551,148,8,9])).
% 33.29/33.40 cnf(671,plain,
% 33.29/33.40 (P2(f6(a4,a1),f6(f6(a4,a4),a2),f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[667,24,8])).
% 33.29/33.40 cnf(672,plain,
% 33.29/33.40 (E(x6721,f6(a4,x6721))),
% 33.29/33.40 inference(rename_variables,[],[24])).
% 33.29/33.40 cnf(673,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),a1),f6(a4,a2),f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[667,652,24,672,8,9])).
% 33.29/33.40 cnf(675,plain,
% 33.29/33.40 (P2(a1,f6(f6(a4,a4),a2),a3)),
% 33.29/33.40 inference(scs_inference,[],[667,652,46,24,672,8,9,10])).
% 33.29/33.40 cnf(677,plain,
% 33.29/33.40 (P2(f6(a4,a1),a2,f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[671,133,9])).
% 33.29/33.40 cnf(678,plain,
% 33.29/33.40 (E(f6(f6(a4,a4),x6781),x6781)),
% 33.29/33.40 inference(rename_variables,[],[133])).
% 33.29/33.40 cnf(679,plain,
% 33.29/33.40 (P2(a1,f6(a4,a2),f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[673,671,133,678,9,8])).
% 33.29/33.40 cnf(681,plain,
% 33.29/33.40 (P2(f6(f6(a4,a4),a1),f6(a4,a2),a3)),
% 33.29/33.40 inference(scs_inference,[],[673,671,133,678,46,9,8,10])).
% 33.29/33.40 cnf(683,plain,
% 33.29/33.40 (P2(f6(a4,a1),f6(a4,a2),a3)),
% 33.29/33.40 inference(scs_inference,[],[681,165,8])).
% 33.29/33.40 cnf(684,plain,
% 33.29/33.40 (E(f6(f6(a4,x6841),x6842),f6(x6841,x6842))),
% 33.29/33.40 inference(rename_variables,[],[165])).
% 33.29/33.40 cnf(685,plain,
% 33.29/33.40 (P2(a1,f6(a4,a2),a3)),
% 33.29/33.40 inference(scs_inference,[],[681,675,165,684,8,9])).
% 33.29/33.40 cnf(687,plain,
% 33.29/33.40 (P2(a1,f6(a4,a2),f6(f6(a4,a4),a3))),
% 33.29/33.40 inference(scs_inference,[],[681,675,679,165,684,179,8,9,10])).
% 33.29/33.40 cnf(689,plain,
% 33.29/33.40 (P2(a1,a2,f6(f6(a4,a4),a3))),
% 33.29/33.40 inference(scs_inference,[],[687,46,9])).
% 33.29/33.40 cnf(694,plain,
% 33.29/33.40 (P2(f6(a4,a1),f6(a4,a2),f6(f6(a4,a4),a3))),
% 33.29/33.40 inference(scs_inference,[],[687,683,267,149,46,148,9,8,10])).
% 33.29/33.40 cnf(696,plain,
% 33.29/33.40 (P2(f6(a4,a1),a2,f6(f6(a4,a4),a3))),
% 33.29/33.40 inference(scs_inference,[],[689,24,8])).
% 33.29/33.40 cnf(697,plain,
% 33.29/33.40 (E(x6971,f6(a4,x6971))),
% 33.29/33.40 inference(rename_variables,[],[24])).
% 33.29/33.40 cnf(698,plain,
% 33.29/33.40 (P2(f6(a4,a1),f6(a4,a2),f6(a4,a3))),
% 33.29/33.40 inference(scs_inference,[],[677,689,24,697,8,9])).
% 33.29/33.40 cnf(707,plain,
% 33.29/33.40 (P2(f6(a4,a1),a2,a3)),
% 33.29/33.40 inference(scs_inference,[],[696,473,657,74,133,179,9,8,10])).
% 33.29/33.40 cnf(710,plain,
% 33.29/33.40 (P2(f6(a4,a1),f6(f6(a4,a4),a2),a3)),
% 33.29/33.40 inference(scs_inference,[],[578,707,184,148,8,9])).
% 33.29/33.40 cnf(723,plain,
% 33.29/33.40 (P2(x7231,f6(f5(x7232),x7232),x7231)),
% 33.29/33.40 inference(scs_inference,[],[14,71,9])).
% 33.29/33.40 cnf(738,plain,
% 33.29/33.40 (P2(f5(a4),x7381,f6(a4,x7381))),
% 33.29/33.40 inference(scs_inference,[],[11,665,528,148,7,8])).
% 33.29/33.40 cnf(745,plain,
% 33.29/33.40 (P1(f6(a4,a1))),
% 33.29/33.40 inference(scs_inference,[],[11,24,7])).
% 33.29/33.40 cnf(758,plain,
% 33.29/33.40 (P1(f6(a4,f5(a1)))),
% 33.29/33.40 inference(scs_inference,[],[11,85,738,20])).
% 33.29/33.40 cnf(764,plain,
% 33.29/33.40 (P2(f6(a4,f6(a4,x7641)),f5(x7641),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[758,280,55,179,7,10])).
% 33.29/33.40 cnf(775,plain,
% 33.29/33.40 (E(a4,f6(f5(x7751),f6(a4,x7751)))),
% 33.29/33.40 inference(scs_inference,[],[17,81,21])).
% 33.29/33.40 cnf(779,plain,
% 33.29/33.40 (P2(a4,x7791,f5(f5(x7791)))),
% 33.29/33.40 inference(scs_inference,[],[60,17,18,723,81,21,7,22])).
% 33.29/33.40 cnf(789,plain,
% 33.29/33.40 (E(f6(f5(x7891),f6(a4,x7891)),a4)),
% 33.29/33.40 inference(scs_inference,[],[775,2])).
% 33.29/33.40 cnf(790,plain,
% 33.29/33.40 (E(f5(f5(x7901)),x7901)),
% 33.29/33.40 inference(scs_inference,[],[779,15,775,2,21])).
% 33.29/33.40 cnf(794,plain,
% 33.29/33.40 (P2(f5(x7941),x7941,a4)),
% 33.29/33.40 inference(rename_variables,[],[17])).
% 33.29/33.40 cnf(797,plain,
% 33.29/33.40 (P2(f5(x7971),x7971,f6(f5(x7972),f6(a4,x7972)))),
% 33.29/33.40 inference(scs_inference,[],[17,794,779,16,15,775,2,21,9,8,10])).
% 33.29/33.40 cnf(798,plain,
% 33.29/33.40 (P2(a4,f5(x7981),f5(f6(a4,x7981)))),
% 33.29/33.40 inference(scs_inference,[],[17,794,779,16,18,15,605,775,2,21,9,8,10,22])).
% 33.29/33.40 cnf(800,plain,
% 33.29/33.40 (P2(f5(x8001),x8001,a4)),
% 33.29/33.40 inference(rename_variables,[],[17])).
% 33.29/33.40 cnf(801,plain,
% 33.29/33.40 (P2(x8011,x8012,f6(x8011,x8012))),
% 33.29/33.40 inference(rename_variables,[],[18])).
% 33.29/33.40 cnf(803,plain,
% 33.29/33.40 (P2(f5(x8031),f6(x8031,x8032),f5(f5(x8032)))),
% 33.29/33.40 inference(scs_inference,[],[17,794,800,779,16,18,801,15,605,775,2,21,9,8,10,22,23])).
% 33.29/33.40 cnf(809,plain,
% 33.29/33.40 (E(x8091,f5(f5(x8091)))),
% 33.29/33.40 inference(scs_inference,[],[790,2])).
% 33.29/33.40 cnf(810,plain,
% 33.29/33.40 (E(f5(f6(a4,x8101)),f5(x8101))),
% 33.29/33.40 inference(scs_inference,[],[798,15,790,2,21])).
% 33.29/33.40 cnf(811,plain,
% 33.29/33.40 (P2(a4,x8111,x8111)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(814,plain,
% 33.29/33.40 (E(f6(f5(x8141),f6(a4,x8141)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[11,798,15,789,790,237,2,21,7,3])).
% 33.29/33.40 cnf(816,plain,
% 33.29/33.40 (P2(a4,x8161,x8161)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(819,plain,
% 33.29/33.40 (P2(f5(f6(a4,x8191)),x8191,a4)),
% 33.29/33.40 inference(scs_inference,[],[11,17,798,496,15,811,816,789,790,775,237,2,21,7,3,9,8,10,22])).
% 33.29/33.40 cnf(828,plain,
% 33.29/33.40 (E(f5(x8281),f5(f6(a4,x8281)))),
% 33.29/33.40 inference(scs_inference,[],[810,2])).
% 33.29/33.40 cnf(831,plain,
% 33.29/33.40 (P2(f5(x8311),f6(a4,x8311),a4)),
% 33.29/33.40 inference(scs_inference,[],[17,810,557,2,9,8])).
% 33.29/33.40 cnf(832,plain,
% 33.29/33.40 (P2(f5(x8321),x8321,a4)),
% 33.29/33.40 inference(rename_variables,[],[17])).
% 33.29/33.40 cnf(833,plain,
% 33.29/33.40 (P2(f5(x8331),f6(a4,x8331),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[17,18,810,557,814,2,9,8,10])).
% 33.29/33.40 cnf(835,plain,
% 33.29/33.40 (P2(a4,a4,f6(f5(x8351),x8351))),
% 33.29/33.40 inference(scs_inference,[],[17,832,779,18,810,557,814,141,2,9,8,10,22])).
% 33.29/33.40 cnf(837,plain,
% 33.29/33.40 (P2(f5(x8371),x8371,a4)),
% 33.29/33.40 inference(rename_variables,[],[17])).
% 33.29/33.40 cnf(838,plain,
% 33.29/33.40 (P2(a4,x8381,f5(f5(x8381)))),
% 33.29/33.40 inference(rename_variables,[],[779])).
% 33.29/33.40 cnf(840,plain,
% 33.29/33.40 (P2(f5(a1),f6(a4,a3),f5(f5(a2)))),
% 33.29/33.40 inference(scs_inference,[],[17,832,837,779,838,18,810,557,814,654,141,2,9,8,10,22,23])).
% 33.29/33.40 cnf(845,plain,
% 33.29/33.40 (E(f5(a4),f6(f5(x8451),f6(a4,x8451)))),
% 33.29/33.40 inference(scs_inference,[],[814,2])).
% 33.29/33.40 cnf(846,plain,
% 33.29/33.40 (E(f6(f5(x8461),f6(a4,x8461)),f6(a4,a4))),
% 33.29/33.40 inference(scs_inference,[],[814,137,2,3])).
% 33.29/33.40 cnf(848,plain,
% 33.29/33.40 (P2(x8481,x8482,f6(x8481,x8482))),
% 33.29/33.40 inference(rename_variables,[],[18])).
% 33.29/33.40 cnf(849,plain,
% 33.29/33.40 (P2(f5(f5(x8491)),x8492,f6(x8491,x8492))),
% 33.29/33.40 inference(scs_inference,[],[18,848,809,814,137,2,3,9,8])).
% 33.29/33.40 cnf(850,plain,
% 33.29/33.40 (P2(x8501,x8502,f6(x8501,x8502))),
% 33.29/33.40 inference(rename_variables,[],[18])).
% 33.29/33.40 cnf(855,plain,
% 33.29/33.40 (P2(a4,f5(x8551),f6(f5(x8551),a4))),
% 33.29/33.40 inference(scs_inference,[],[138,70,17,18,848,850,685,809,814,137,287,2,3,9,8,10,20,22])).
% 33.29/33.40 cnf(864,plain,
% 33.29/33.40 (E(f6(a4,a4),f6(f5(x8641),f6(a4,x8641)))),
% 33.29/33.40 inference(scs_inference,[],[846,2])).
% 33.29/33.40 cnf(865,plain,
% 33.29/33.40 (E(f6(f5(x8651),a4),f5(x8651))),
% 33.29/33.40 inference(scs_inference,[],[855,15,846,2,21])).
% 33.29/33.40 cnf(866,plain,
% 33.29/33.40 (P2(a4,x8661,x8661)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(877,plain,
% 33.29/33.40 (P2(a4,x8771,f6(f6(a4,x8771),a4))),
% 33.29/33.40 inference(scs_inference,[],[11,60,17,819,855,16,15,866,395,849,845,846,2,21,9,8,10,20,22])).
% 33.29/33.40 cnf(886,plain,
% 33.29/33.40 (E(f5(x8861),f6(f5(x8861),a4))),
% 33.29/33.40 inference(scs_inference,[],[865,2])).
% 33.29/33.40 cnf(887,plain,
% 33.29/33.40 (E(f6(f6(a4,x8871),a4),x8871)),
% 33.29/33.40 inference(scs_inference,[],[877,15,865,2,21])).
% 33.29/33.40 cnf(888,plain,
% 33.29/33.40 (P2(a4,x8881,x8881)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(896,plain,
% 33.29/33.40 (P2(f5(x8961),f6(x8961,x8962),f6(f6(a4,x8962),a4))),
% 33.29/33.40 inference(scs_inference,[],[17,877,16,18,15,888,123,865,828,2,21,9,8,10,23])).
% 33.29/33.40 cnf(900,plain,
% 33.29/33.40 (E(x9001,f6(f6(a4,x9001),a4))),
% 33.29/33.40 inference(scs_inference,[],[887,2])).
% 33.29/33.40 cnf(902,plain,
% 33.29/33.40 (E(f6(f6(a4,a1),a4),f6(a4,a1))),
% 33.29/33.40 inference(scs_inference,[],[11,887,24,2,7,3])).
% 33.29/33.40 cnf(904,plain,
% 33.29/33.40 (E(f6(f6(a4,x9041),a4),x9041)),
% 33.29/33.40 inference(rename_variables,[],[887])).
% 33.29/33.40 cnf(909,plain,
% 33.29/33.40 (P2(f6(a4,x9091),a4,x9091)),
% 33.29/33.40 inference(scs_inference,[],[11,16,18,572,887,904,886,865,24,2,7,3,9,8,10])).
% 33.29/33.40 cnf(917,plain,
% 33.29/33.40 (E(x9171,f6(x9171,a4))),
% 33.29/33.40 inference(scs_inference,[],[900,902,165,2,3])).
% 33.29/33.40 cnf(920,plain,
% 33.29/33.40 (P2(f5(x9201),x9201,a4)),
% 33.29/33.40 inference(rename_variables,[],[17])).
% 33.29/33.40 cnf(925,plain,
% 33.29/33.40 (P2(f5(a1),f6(a4,a3),f6(f6(a4,a2),a4))),
% 33.29/33.40 inference(scs_inference,[],[17,920,877,16,900,831,902,654,165,2,3,9,8,10,23])).
% 33.29/33.40 cnf(930,plain,
% 33.29/33.40 (E(f6(x9301,a4),x9301)),
% 33.29/33.40 inference(scs_inference,[],[917,2])).
% 33.29/33.40 cnf(931,plain,
% 33.29/33.40 (E(f6(a4,x9311),f6(x9311,a4))),
% 33.29/33.40 inference(scs_inference,[],[917,165,2,3])).
% 33.29/33.40 cnf(933,plain,
% 33.29/33.40 (E(x9331,f6(x9331,a4))),
% 33.29/33.40 inference(rename_variables,[],[917])).
% 33.29/33.40 cnf(935,plain,
% 33.29/33.40 (P2(a4,x9351,x9351)),
% 33.29/33.40 inference(rename_variables,[],[15])).
% 33.29/33.40 cnf(940,plain,
% 33.29/33.40 (P2(f5(a1),a3,f5(f5(a2)))),
% 33.29/33.40 inference(scs_inference,[],[17,855,779,15,935,864,917,933,13,165,2,3,9,8,10,23])).
% 33.29/33.40 cnf(945,plain,
% 33.29/33.40 (E(f6(x9451,a4),f6(a4,x9451))),
% 33.29/33.40 inference(scs_inference,[],[931,2])).
% 33.29/33.40 cnf(946,plain,
% 33.29/33.40 (E(f6(a4,f6(a4,x9461)),x9461)),
% 33.29/33.40 inference(scs_inference,[],[931,887,2,3])).
% 33.29/33.40 cnf(947,plain,
% 33.29/33.40 (E(f6(a4,x9471),f6(x9471,a4))),
% 33.29/33.40 inference(rename_variables,[],[931])).
% 33.29/33.40 cnf(950,plain,
% 33.29/33.40 (P2(f6(a4,a4),f5(x9501),f5(f6(a4,x9501)))),
% 33.29/33.40 inference(scs_inference,[],[17,798,931,947,887,917,2,3,9,8])).
% 33.29/33.40 cnf(952,plain,
% 33.29/33.40 (P2(a4,x9521,f6(x9521,a4))),
% 33.29/33.40 inference(scs_inference,[],[17,798,18,931,947,887,917,2,3,9,8,10])).
% 33.29/33.40 cnf(959,plain,
% 33.29/33.40 (E(x9591,f6(a4,f6(a4,x9591)))),
% 33.29/33.40 inference(scs_inference,[],[946,2])).
% 33.29/33.40 cnf(961,plain,
% 33.29/33.40 (E(f6(x9611,a4),f6(f6(a4,a4),x9611))),
% 33.29/33.40 inference(scs_inference,[],[11,945,946,179,2,7,3])).
% 33.29/33.40 cnf(965,plain,
% 33.29/33.40 (P2(f6(a4,x9651),x9652,f6(f6(x9651,a4),x9652))),
% 33.29/33.40 inference(scs_inference,[],[11,17,18,945,946,179,2,7,3,9,8])).
% 33.29/33.40 cnf(967,plain,
% 33.29/33.40 (P2(a4,f6(x9671,a4),f6(a4,x9671))),
% 33.29/33.40 inference(scs_inference,[],[11,17,15,18,945,946,179,2,7,3,9,8,10])).
% 33.29/33.40 cnf(974,plain,
% 33.29/33.40 (E(f6(f6(a4,a4),x9741),f6(x9741,a4))),
% 33.29/33.40 inference(scs_inference,[],[961,2])).
% 33.29/33.40 cnf(975,plain,
% 33.29/33.40 (E(f6(x9751,a4),f6(a4,f6(a4,x9751)))),
% 33.29/33.40 inference(scs_inference,[],[959,930,961,2,3])).
% 33.29/33.40 cnf(984,plain,
% 33.29/33.40 (E(f6(a4,f6(a4,x9841)),f6(x9841,a4))),
% 33.29/33.40 inference(scs_inference,[],[975,2])).
% 33.29/33.40 cnf(985,plain,
% 33.29/33.40 (E(f6(f6(a4,a4),f6(a4,x9851)),x9851)),
% 33.29/33.40 inference(scs_inference,[],[974,975,887,2,3])).
% 33.29/33.40 cnf(994,plain,
% 33.29/33.40 (E(x9941,f6(f6(a4,a4),f6(a4,x9941)))),
% 33.29/33.40 inference(scs_inference,[],[985,2])).
% 33.29/33.40 cnf(996,plain,
% 33.29/33.40 (E(f6(a4,f6(a4,a4)),f5(a4))),
% 33.29/33.40 inference(scs_inference,[],[11,984,985,184,2,7,3])).
% 33.29/33.41 cnf(997,plain,
% 33.29/33.41 (E(f6(a4,f6(a4,x9971)),f6(x9971,a4))),
% 33.29/33.41 inference(rename_variables,[],[984])).
% 33.29/33.41 cnf(998,plain,
% 33.29/33.41 (P2(f6(x9981,a4),f5(x9981),f6(a4,a4))),
% 33.29/33.41 inference(scs_inference,[],[11,764,984,997,985,184,2,7,3,8])).
% 33.29/33.41 cnf(1002,plain,
% 33.29/33.41 (P2(a4,f6(a4,x10021),f6(x10021,a4))),
% 33.29/33.41 inference(scs_inference,[],[11,18,15,764,984,997,985,184,2,7,3,8,9,10])).
% 33.29/33.41 cnf(1009,plain,
% 33.29/33.41 (E(f5(a4),f6(a4,f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[996,2])).
% 33.29/33.41 cnf(1010,plain,
% 33.29/33.41 (E(f6(f6(a4,a4),f6(a4,a4)),f5(a4))),
% 33.29/33.41 inference(scs_inference,[],[996,974,297,2,3])).
% 33.29/33.41 cnf(1013,plain,
% 33.29/33.41 (E(x10131,f6(f6(a4,a4),f6(a4,x10131)))),
% 33.29/33.41 inference(rename_variables,[],[994])).
% 33.29/33.41 cnf(1014,plain,
% 33.29/33.41 (P2(f6(a4,x10141),f6(f6(a4,a4),f6(a4,a4)),x10141)),
% 33.29/33.41 inference(scs_inference,[],[15,996,909,994,1013,974,297,2,3,8,9])).
% 33.29/33.41 cnf(1023,plain,
% 33.29/33.41 (E(f5(a4),f6(f6(a4,a4),f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[1010,2])).
% 33.29/33.41 cnf(1026,plain,
% 33.29/33.41 (P2(f6(a4,a4),f6(a4,f6(a4,a4)),f6(a4,a4))),
% 33.29/33.41 inference(scs_inference,[],[395,998,1010,1009,2,8,9])).
% 33.29/33.41 cnf(1028,plain,
% 33.29/33.41 (P2(x10281,f5(x10281),f6(f6(a4,a4),f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[16,395,998,1010,1009,994,2,8,9,10])).
% 33.29/33.41 cnf(1048,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a2,a4),a3)),
% 33.29/33.41 inference(scs_inference,[],[1026,710,930,974,8,9])).
% 33.29/33.41 cnf(1056,plain,
% 33.29/33.41 (E(f5(f5(x10561)),f6(x10561,a4))),
% 33.29/33.41 inference(scs_inference,[],[790,917,3])).
% 33.29/33.41 cnf(1058,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a4,a2),f6(f6(a4,a4),a3))),
% 33.29/33.41 inference(scs_inference,[],[694,790,931,917,3,8])).
% 33.29/33.41 cnf(1060,plain,
% 33.29/33.41 (P2(f6(a4,a4),f6(f6(a4,a4),f6(a4,a4)),f6(a4,a4))),
% 33.29/33.41 inference(scs_inference,[],[206,694,790,961,931,917,3,8,9])).
% 33.29/33.41 cnf(1061,plain,
% 33.29/33.41 (E(f6(x10611,a4),f6(f6(a4,a4),x10611))),
% 33.29/33.41 inference(rename_variables,[],[961])).
% 33.29/33.41 cnf(1064,plain,
% 33.29/33.41 (E(f6(x10641,a4),f5(f5(x10641)))),
% 33.29/33.41 inference(scs_inference,[],[206,877,694,790,961,1061,931,917,3,8,9,10,2])).
% 33.29/33.41 cnf(1073,plain,
% 33.29/33.41 (P2(f6(x10731,a4),f5(x10731),f5(f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[642,1056,8])).
% 33.29/33.41 cnf(1077,plain,
% 33.29/33.41 (P2(f5(x10771),f6(x10771,x10772),f6(x10772,a4))),
% 33.29/33.41 inference(scs_inference,[],[16,642,803,1056,8,9,10])).
% 33.29/33.41 cnf(1086,plain,
% 33.29/33.41 (~P1(f5(a2))),
% 33.29/33.41 inference(scs_inference,[],[19,745,840,797,1048,1064,790,8,9,10,20])).
% 33.29/33.41 cnf(1100,plain,
% 33.29/33.41 (P2(a4,f6(a4,x11001),x11001)),
% 33.29/33.41 inference(scs_inference,[],[18,395,677,946,1023,994,8,9,10])).
% 33.29/33.41 cnf(1107,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a4,a2),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[600,1028,1058,810,974,8,9,10])).
% 33.29/33.41 cnf(1110,plain,
% 33.29/33.41 (P2(a1,f6(a4,a2),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1107,930,8])).
% 33.29/33.41 cnf(1118,plain,
% 33.29/33.41 (E(f6(x11181,a4),f6(f6(a4,a4),x11181))),
% 33.29/33.41 inference(rename_variables,[],[961])).
% 33.29/33.41 cnf(1120,plain,
% 33.29/33.41 (E(f6(x11201,a4),f6(f6(a4,a4),x11201))),
% 33.29/33.41 inference(rename_variables,[],[961])).
% 33.29/33.41 cnf(1121,plain,
% 33.29/33.41 (P2(f5(a1),f6(a4,a3),f6(f6(a4,a4),f6(a4,a2)))),
% 33.29/33.41 inference(scs_inference,[],[286,618,925,961,1118,1120,8,9,10])).
% 33.29/33.41 cnf(1131,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a2,a4),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[496,698,931,180,8,9])).
% 33.29/33.41 cnf(1132,plain,
% 33.29/33.41 (E(f6(a4,x11321),f6(x11321,a4))),
% 33.29/33.41 inference(rename_variables,[],[931])).
% 33.29/33.41 cnf(1133,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a4,a2),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[496,698,931,1132,180,8,9,10])).
% 33.29/33.41 cnf(1138,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a4,f6(a4,a2)),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[123,1131,225,975,8,9])).
% 33.29/33.41 cnf(1139,plain,
% 33.29/33.41 (E(f6(x11391,a4),f6(a4,f6(a4,x11391)))),
% 33.29/33.41 inference(rename_variables,[],[975])).
% 33.29/33.41 cnf(1140,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a4,a2),f6(a4,f6(a4,a3)))),
% 33.29/33.41 inference(scs_inference,[],[123,1133,1131,225,975,1139,8,9,10])).
% 33.29/33.41 cnf(1143,plain,
% 33.29/33.41 (E(f6(f6(a4,a4),f6(a4,x11431)),f6(x11431,a4))),
% 33.29/33.41 inference(scs_inference,[],[985,917,3])).
% 33.29/33.41 cnf(1151,plain,
% 33.29/33.41 (E(f6(x11511,a4),f6(f6(a4,a4),f6(a4,x11511)))),
% 33.29/33.41 inference(scs_inference,[],[15,123,557,985,238,917,3,8,9,10,2])).
% 33.29/33.41 cnf(1164,plain,
% 33.29/33.41 (P2(f6(a4,a4),f6(a4,x11641),f6(x11641,a4))),
% 33.29/33.41 inference(scs_inference,[],[18,15,1110,1143,809,8,9,10])).
% 33.29/33.41 cnf(1171,plain,
% 33.29/33.41 (P2(a4,f6(a4,f6(a4,x11711)),x11711)),
% 33.29/33.41 inference(scs_inference,[],[15,950,1164,946,1151,97,8,9,10])).
% 33.29/33.41 cnf(1188,plain,
% 33.29/33.41 (P2(f6(f6(a4,a4),a4),x11881,f6(x11881,a4))),
% 33.29/33.41 inference(scs_inference,[],[952,900,8])).
% 33.29/33.41 cnf(1190,plain,
% 33.29/33.41 (P2(f6(a4,x11901),f5(a4),x11901)),
% 33.29/33.41 inference(scs_inference,[],[952,1014,1010,900,8,9])).
% 33.29/33.41 cnf(1193,plain,
% 33.29/33.41 (E(f6(f6(a4,x11931),f5(a4)),x11931)),
% 33.29/33.41 inference(scs_inference,[],[18,1121,952,1014,1010,1143,900,8,9,10,21])).
% 33.29/33.41 cnf(1196,plain,
% 33.29/33.41 (E(x11961,f6(f6(a4,x11961),f5(a4)))),
% 33.29/33.41 inference(scs_inference,[],[18,1121,952,1014,1010,1143,900,8,9,10,21,2])).
% 33.29/33.41 cnf(1198,plain,
% 33.29/33.41 (E(f6(a1,a4),f6(f6(a4,a1),f5(a4)))),
% 33.29/33.41 inference(scs_inference,[],[11,18,1121,952,1014,1010,930,1143,900,8,9,10,21,2,7,3])).
% 33.29/33.41 cnf(1200,plain,
% 33.29/33.41 (P2(a1,f6(f6(a4,a4),a4),a1)),
% 33.29/33.41 inference(scs_inference,[],[11,290,18,1121,952,1014,1010,930,1143,900,8,9,10,21,2,7,3,22])).
% 33.29/33.41 cnf(1203,plain,
% 33.29/33.41 (E(f6(f6(a4,a1),f5(a4)),f6(a1,a4))),
% 33.29/33.41 inference(scs_inference,[],[1198,2])).
% 33.29/33.41 cnf(1204,plain,
% 33.29/33.41 (E(f6(a1,a4),f6(a1,f5(a4)))),
% 33.29/33.41 inference(scs_inference,[],[1198,165,2,3])).
% 33.29/33.41 cnf(1206,plain,
% 33.29/33.41 (P2(f6(f6(a4,a4),f5(a4)),f6(a4,x12061),x12061)),
% 33.29/33.41 inference(scs_inference,[],[1198,1196,1100,165,2,3,8])).
% 33.29/33.41 cnf(1214,plain,
% 33.29/33.41 (E(f6(a1,f5(a4)),f6(a1,a4))),
% 33.29/33.41 inference(scs_inference,[],[1204,2])).
% 33.29/33.41 cnf(1215,plain,
% 33.29/33.41 (P2(f6(f6(a4,a4),f5(a4)),f6(x12151,a4),f6(a4,x12151))),
% 33.29/33.41 inference(scs_inference,[],[1204,967,1196,2,8])).
% 33.29/33.41 cnf(1219,plain,
% 33.29/33.41 (P2(f6(a4,a1),f5(a4),f6(a1,a4))),
% 33.29/33.41 inference(scs_inference,[],[18,15,1203,1204,967,1196,2,8,9,10])).
% 33.29/33.41 cnf(1221,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(f6(a4,a4),a4),f6(a1,a4))),
% 33.29/33.41 inference(scs_inference,[],[290,18,15,1203,1204,967,1196,2,8,9,10,22])).
% 33.29/33.41 cnf(1224,plain,
% 33.29/33.41 (E(f6(a1,f5(a4)),a1)),
% 33.29/33.41 inference(scs_inference,[],[1214,930,3])).
% 33.29/33.41 cnf(1229,plain,
% 33.29/33.41 (P2(a4,x12291,x12291)),
% 33.29/33.41 inference(rename_variables,[],[15])).
% 33.29/33.41 cnf(1232,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(f6(a4,a4),a4),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1221,15,1229,1215,1002,1214,1196,930,3,8,9,10,22])).
% 33.29/33.41 cnf(1235,plain,
% 33.29/33.41 (E(a1,f6(a1,f5(a4)))),
% 33.29/33.41 inference(scs_inference,[],[1221,15,1229,1215,1002,1214,1196,930,3,8,9,10,22,2])).
% 33.29/33.41 cnf(1237,plain,
% 33.29/33.41 (E(f6(a1,f5(a4)),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1224,24,3])).
% 33.29/33.41 cnf(1241,plain,
% 33.29/33.41 (P2(a4,x12411,x12411)),
% 33.29/33.41 inference(rename_variables,[],[15])).
% 33.29/33.41 cnf(1244,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a4,a4),a1)),
% 33.29/33.41 inference(scs_inference,[],[1232,15,1241,610,1190,1224,685,1235,24,3,8,9,10,22])).
% 33.29/33.41 cnf(1247,plain,
% 33.29/33.41 (E(f6(a4,a1),f6(a1,f5(a4)))),
% 33.29/33.41 inference(scs_inference,[],[1232,15,1241,610,1190,1224,685,1235,24,3,8,9,10,22,2])).
% 33.29/33.41 cnf(1249,plain,
% 33.29/33.41 (E(a1,f6(f6(a1,a4),f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[1244,965,21])).
% 33.29/33.41 cnf(1256,plain,
% 33.29/33.41 (E(f6(f6(a1,a4),f6(a4,a4)),a1)),
% 33.29/33.41 inference(scs_inference,[],[11,1244,965,1247,1235,864,21,7,8,9,10,2])).
% 33.29/33.41 cnf(1258,plain,
% 33.29/33.41 (E(f6(f6(a1,a4),f6(a4,a4)),f6(a1,a4))),
% 33.29/33.41 inference(scs_inference,[],[1256,917,3])).
% 33.29/33.41 cnf(1263,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a4,a4),a1)),
% 33.29/33.41 inference(scs_inference,[],[18,15,1219,1256,1247,917,3,8,9,10])).
% 33.29/33.41 cnf(1265,plain,
% 33.29/33.41 (E(f6(a1,a4),f6(f6(a1,a4),f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[18,15,1219,1256,1247,917,3,8,9,10,2])).
% 33.29/33.41 cnf(1270,plain,
% 33.29/33.41 (P2(a1,a4,f6(f6(a1,a4),f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[18,15,1265,1263,8,9,10])).
% 33.29/33.41 cnf(1273,plain,
% 33.29/33.41 (P2(f6(f6(a1,a4),f6(a4,a4)),f6(a4,a2),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[679,1249,8])).
% 33.29/33.41 cnf(1274,plain,
% 33.29/33.41 (P2(a4,f6(a1,a4),f6(f6(a1,a4),f6(a4,a4)))),
% 33.29/33.41 inference(scs_inference,[],[15,1258,679,1249,8,9])).
% 33.29/33.41 cnf(1279,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a4,a2),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[1273,1258,8])).
% 33.29/33.41 cnf(1282,plain,
% 33.29/33.41 (P2(a1,f5(a4),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1200,18,1273,1237,1258,961,8,9,10])).
% 33.29/33.41 cnf(1291,plain,
% 33.29/33.41 (P2(f6(f6(a1,a4),f6(a4,a4)),f5(a4),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1282,1249,8])).
% 33.29/33.41 cnf(1297,plain,
% 33.29/33.41 (P2(f6(a1,a4),f5(a4),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1291,1258,8])).
% 33.29/33.41 cnf(1300,plain,
% 33.29/33.41 (P2(f5(x13001),f6(x13001,x13002),x13002)),
% 33.29/33.41 inference(scs_inference,[],[896,1291,833,1258,1247,887,8,9,10])).
% 33.29/33.41 cnf(1302,plain,
% 33.29/33.41 (E(f6(f5(x13021),f6(x13021,x13022)),x13022)),
% 33.29/33.41 inference(scs_inference,[],[18,896,1291,833,1258,1247,887,8,9,10,21])).
% 33.29/33.41 cnf(1305,plain,
% 33.29/33.41 (E(x13051,f6(f5(x13052),f6(x13052,x13051)))),
% 33.29/33.41 inference(scs_inference,[],[18,896,1291,833,1258,1247,887,8,9,10,21,2])).
% 33.29/33.41 cnf(1345,plain,
% 33.29/33.41 (P2(f5(a4),f6(f5(a4),x13451),x13451)),
% 33.29/33.41 inference(scs_inference,[],[1300,502,8])).
% 33.29/33.41 cnf(1354,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(f6(a4,a4),a4),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[395,1297,281,8,9])).
% 33.29/33.41 cnf(1355,plain,
% 33.29/33.41 (P2(a4,f6(a1,a4),a1)),
% 33.29/33.41 inference(scs_inference,[],[395,1274,1297,1256,281,8,9,10])).
% 33.29/33.41 cnf(1357,plain,
% 33.29/33.41 (E(f6(f5(x13571),f6(x13571,x13572)),f6(x13572,a4))),
% 33.29/33.41 inference(scs_inference,[],[1302,917,3])).
% 33.29/33.41 cnf(1362,plain,
% 33.29/33.41 (P2(a4,x13621,x13621)),
% 33.29/33.41 inference(rename_variables,[],[15])).
% 33.29/33.41 cnf(1363,plain,
% 33.29/33.41 (P2(a4,f6(f5(x13631),f6(x13631,x13632)),x13632)),
% 33.29/33.41 inference(scs_inference,[],[15,1362,123,1302,463,917,3,8,9,10])).
% 33.29/33.41 cnf(1365,plain,
% 33.29/33.41 (E(f6(x13651,a4),f6(f5(x13652),f6(x13652,x13651)))),
% 33.29/33.41 inference(scs_inference,[],[15,1362,123,1302,463,917,3,8,9,10,2])).
% 33.29/33.41 cnf(1367,plain,
% 33.29/33.41 (P2(f6(a4,f6(a4,a4)),f6(a1,a4),a1)),
% 33.29/33.41 inference(scs_inference,[],[1355,959,8])).
% 33.29/33.41 cnf(1374,plain,
% 33.29/33.41 (P2(f5(a4),f6(a1,a4),a1)),
% 33.29/33.41 inference(scs_inference,[],[1367,996,8])).
% 33.29/33.41 cnf(1375,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a2,a4),f6(a4,f6(a4,a3)))),
% 33.29/33.41 inference(scs_inference,[],[1140,1367,996,931,8,9])).
% 33.29/33.41 cnf(1381,plain,
% 33.29/33.41 (P2(f5(a4),f6(x13811,a4),f6(a4,x13811))),
% 33.29/33.41 inference(scs_inference,[],[1345,1374,1357,488,8,9])).
% 33.29/33.41 cnf(1384,plain,
% 33.29/33.41 (P2(f5(a1),a3,a2)),
% 33.29/33.41 inference(scs_inference,[],[940,1345,1374,1357,488,790,8,9,10])).
% 33.29/33.41 cnf(1388,plain,
% 33.29/33.41 (P2(f5(a1),f5(f5(a3)),a2)),
% 33.29/33.41 inference(scs_inference,[],[1384,1381,1009,809,8,9])).
% 33.29/33.41 cnf(1394,plain,
% 33.29/33.41 (E(x13941,f6(f5(x13942),f6(x13942,x13941)))),
% 33.29/33.41 inference(rename_variables,[],[1305])).
% 33.29/33.41 cnf(1397,plain,
% 33.29/33.41 (P2(x13971,f5(x13971),f6(f5(x13972),f6(x13972,a4)))),
% 33.29/33.41 inference(scs_inference,[],[16,15,1300,1204,1305,1394,8,9,10])).
% 33.29/33.41 cnf(1407,plain,
% 33.29/33.41 (P2(f6(a4,a4),f6(a4,x14071),x14071)),
% 33.29/33.41 inference(scs_inference,[],[1206,280,8])).
% 33.29/33.41 cnf(1410,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a2,a4),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1375,1206,1219,1023,280,984,8,9,10])).
% 33.29/33.41 cnf(1416,plain,
% 33.29/33.41 (P2(f6(a1,f5(a4)),f6(a2,a4),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1410,1247,8])).
% 33.29/33.41 cnf(1417,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(f5(x14171),f6(x14171,a2)),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1410,1247,1365,8,9])).
% 33.29/33.41 cnf(1422,plain,
% 33.29/33.41 (P2(a1,f6(a2,a4),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1416,1224,8])).
% 33.29/33.41 cnf(1428,plain,
% 33.29/33.41 (P2(f6(f6(a4,a4),f6(a4,a4)),f6(a4,x14281),x14281)),
% 33.29/33.41 inference(scs_inference,[],[1407,1151,8])).
% 33.29/33.41 cnf(1446,plain,
% 33.29/33.41 (P2(f5(a4),x14461,f6(x14461,a4))),
% 33.29/33.41 inference(scs_inference,[],[1188,297,8])).
% 33.29/33.41 cnf(1455,plain,
% 33.29/33.41 (E(f6(f6(a1,a4),f6(a4,a4)),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1256,24,3])).
% 33.29/33.41 cnf(1463,plain,
% 33.29/33.41 (P2(f6(f5(x14631),x14631),x14632,f6(x14632,a4))),
% 33.29/33.41 inference(scs_inference,[],[1446,180,8])).
% 33.29/33.41 cnf(1480,plain,
% 33.29/33.41 (P2(a1,a4,f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1388,1270,1463,1455,96,1056,8,9,10])).
% 33.29/33.41 cnf(1500,plain,
% 33.29/33.41 (P2(f6(f6(a4,a1),f5(a4)),f6(a4,a2),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[1279,1198,8])).
% 33.29/33.41 cnf(1501,plain,
% 33.29/33.41 (P2(f6(a1,a4),a4,f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1354,1279,1198,887,8,9])).
% 33.29/33.41 cnf(1505,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a2,a4),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1416,1214,8])).
% 33.29/33.41 cnf(1506,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a4,f6(a4,a4)),f6(a4,a1))),
% 33.29/33.41 inference(scs_inference,[],[1501,1416,1214,959,8,9])).
% 33.29/33.41 cnf(1515,plain,
% 33.29/33.41 (P2(f6(f6(a4,a1),f5(a4)),f6(a2,a4),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[1500,931,9])).
% 33.29/33.41 cnf(1516,plain,
% 33.29/33.41 (E(f6(a4,x15161),f6(x15161,a4))),
% 33.29/33.41 inference(rename_variables,[],[931])).
% 33.29/33.41 cnf(1517,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a4,f6(a4,a2)),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[1138,1500,931,1516,9,8])).
% 33.29/33.41 cnf(1525,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a2,a4),f6(f6(a4,a4),f6(a4,a3)))),
% 33.29/33.41 inference(scs_inference,[],[1517,1515,1505,1203,946,1151,9,8,10])).
% 33.29/33.41 cnf(1548,plain,
% 33.29/33.41 (P2(a1,f6(a2,a4),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[1244,1515,1193,462,9,8])).
% 33.29/33.41 cnf(1579,plain,
% 33.29/33.41 (P2(f6(a1,a4),f6(a2,a4),a3)),
% 33.29/33.41 inference(scs_inference,[],[1525,1428,1480,996,1249,985,9,8,10])).
% 33.29/33.41 cnf(1601,plain,
% 33.29/33.41 (P2(f6(f6(a4,a1),a4),f6(a2,a4),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1422,900,8])).
% 33.29/33.41 cnf(1611,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(a4,a4),f6(a4,f6(a4,a1)))),
% 33.29/33.41 inference(scs_inference,[],[1244,1397,1579,169,1204,959,9,8,10])).
% 33.29/33.41 cnf(1621,plain,
% 33.29/33.41 (P2(f6(a4,a1),a2,f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1417,1302,9])).
% 33.29/33.41 cnf(1626,plain,
% 33.29/33.41 (P2(f6(x16261,a4),f5(x16261),f5(a4))),
% 33.29/33.41 inference(scs_inference,[],[1073,1417,1077,463,810,1302,9,8,10])).
% 33.29/33.41 cnf(1631,plain,
% 33.29/33.41 (P2(f6(a1,f5(a4)),a2,f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1621,1548,1247,1151,9,8])).
% 33.29/33.41 cnf(1636,plain,
% 33.29/33.41 (E(f6(x16361,a4),f6(a4,x16361))),
% 33.29/33.41 inference(rename_variables,[],[945])).
% 33.29/33.41 cnf(1638,plain,
% 33.29/33.41 (E(f6(x16381,a4),f6(a4,x16381))),
% 33.29/33.41 inference(rename_variables,[],[945])).
% 33.29/33.41 cnf(1639,plain,
% 33.29/33.41 (P2(f6(f6(a4,a1),a4),f6(a2,a4),f6(a4,a3))),
% 33.29/33.41 inference(scs_inference,[],[1506,1601,945,1636,1638,9,8,10])).
% 33.29/33.41 cnf(1642,plain,
% 33.29/33.41 (P2(f6(a1,a4),a2,f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1631,1214,8])).
% 33.29/33.41 cnf(1658,plain,
% 33.29/33.41 (P2(f6(f5(x16581),x16581),f6(a4,x16582),x16582)),
% 33.29/33.41 inference(scs_inference,[],[835,18,1626,1642,1171,1407,180,263,1305,9,8,10,22])).
% 33.29/33.41 cnf(1677,plain,
% 33.29/33.41 (P2(x16771,f5(f6(a4,x16771)),f6(a4,a4))),
% 33.29/33.41 inference(scs_inference,[],[1658,16,764,1060,1611,47,184,9,8,10,22])).
% 33.29/33.41 cnf(1683,plain,
% 33.29/33.41 (P2(f6(a4,a1),f6(f6(a4,a4),f6(a4,a2)),f6(a3,a4))),
% 33.29/33.41 inference(scs_inference,[],[1621,994,9])).
% 33.29/33.41 cnf(1709,plain,
% 33.29/33.41 (E(f6(x17091,a4),x17091)),
% 33.29/33.41 inference(rename_variables,[],[930])).
% 33.29/33.41 cnf(1711,plain,
% 33.29/33.41 (E(f6(x17111,a4),x17111)),
% 33.29/33.41 inference(rename_variables,[],[930])).
% 33.29/33.41 cnf(1719,plain,
% 33.29/33.41 (P1(f5(f6(a4,a2)))),
% 33.29/33.41 inference(scs_inference,[],[12,60,1677,798,18,1683,1639,1363,144,930,1709,1711,900,7,9,8,10,22,20])).
% 33.29/33.41 cnf(1723,plain,
% 33.29/33.41 ($false),
% 33.29/33.41 inference(scs_inference,[],[1719,1086,810,7]),
% 33.29/33.41 ['proof']).
% 33.29/33.41 % SZS output end Proof
% 33.29/33.41 % Total time :32.720000s
%------------------------------------------------------------------------------