%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP008-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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:38:26 EDT 2024
% Result : Unsatisfiable 85.30s 85.37s
% Output : CNFRefutation 85.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP008-1 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 09:27:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 85.30/85.36 %-------------------------------------------
% 85.30/85.36 % File :CSE---1.7
% 85.30/85.36 % Problem :theBenchmark
% 85.30/85.36 % Transform :cnf
% 85.30/85.36 % Format :tptp:raw
% 85.30/85.36 % Command :java -jar mcs_scs.jar %d %s
% 85.30/85.36
% 85.30/85.36 % Result :Theorem 84.760000s
% 85.30/85.36 % Output :CNFRefutation 84.760000s
% 85.30/85.36 %-------------------------------------------
% 85.30/85.37 %--------------------------------------------------------------------------
% 85.30/85.37 % File : GRP008-1 : TPTP v8.2.0. Released v1.0.0.
% 85.30/85.37 % Domain : Group Theory
% 85.30/85.37 % Problem : Unknown meaning
% 85.30/85.37 % Version : [MOW76] axioms.
% 85.30/85.37 % English :
% 85.30/85.37
% 85.30/85.37 % Refs : [Wos65] Wos (1965), Unpublished Note
% 85.30/85.37 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 85.30/85.37 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 85.30/85.37 % Source : [SPRFN]
% 85.30/85.37 % Names : Problem 4 [Wos65]
% 85.30/85.37 % : wos4 [WM76]
% 85.30/85.37
% 85.30/85.37 % Status : Unsatisfiable
% 85.30/85.37 % Rating : 0.05 v8.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.20 v5.4.0, 0.15 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0, 0.08 v4.0.1, 0.09 v3.7.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.15 v3.1.0, 0.18 v2.7.0, 0.25 v2.6.0, 0.10 v2.5.0, 0.25 v2.4.0, 0.11 v2.3.0, 0.22 v2.2.1, 0.11 v2.2.0, 0.11 v2.1.0, 0.11 v2.0.0
% 85.30/85.37 % Syntax : Number of clauses : 12 ( 6 unt; 1 nHn; 6 RR)
% 85.30/85.37 % Number of literals : 26 ( 1 equ; 13 neg)
% 85.30/85.37 % Maximal clause size : 4 ( 2 avg)
% 85.30/85.37 % Maximal term depth : 2 ( 1 avg)
% 85.30/85.37 % Number of predicates : 3 ( 2 usr; 0 prp; 1-3 aty)
% 85.30/85.37 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% 85.30/85.37 % Number of variables : 27 ( 0 sgn)
% 85.30/85.37 % SPC : CNF_UNS_RFO_SEQ_NHN
% 85.30/85.37
% 85.30/85.37 % Comments :
% 85.30/85.37 %--------------------------------------------------------------------------
% 85.30/85.37 %----Include group theory axioms
% 85.30/85.37 include('Axioms/GRP003-0.ax').
% 85.30/85.37 %--------------------------------------------------------------------------
% 85.30/85.37 cnf(unknown_meaning2,axiom,
% 85.30/85.37 ( ~ q(A)
% 85.30/85.37 | ~ product(A,B,C)
% 85.30/85.37 | product(B,A,C) ) ).
% 85.30/85.37
% 85.30/85.37 cnf(unknown_meaning3,axiom,
% 85.30/85.37 ( product(j(A),A,h(A))
% 85.30/85.37 | product(A,j(A),h(A))
% 85.30/85.37 | q(A) ) ).
% 85.30/85.37
% 85.30/85.37 cnf(unknown_meaning4,axiom,
% 85.30/85.37 ( ~ product(j(A),A,h(A))
% 85.30/85.37 | ~ product(A,j(A),h(A))
% 85.30/85.37 | q(A) ) ).
% 85.30/85.37
% 85.30/85.37 cnf(prove_identity_is_q,negated_conjecture,
% 85.30/85.37 ~ q(identity) ).
% 85.30/85.37
% 85.30/85.37 %--------------------------------------------------------------------------
% 85.30/85.37 %-------------------------------------------
% 85.30/85.37 % Proof found
% 85.30/85.37 % SZS status Theorem for theBenchmark
% 85.30/85.37 % SZS output start Proof
% 85.30/85.38 %ClaNum:24(EqnAxiom:12)
% 85.30/85.38 %VarNum:65(SingletonVarNum:27)
% 85.30/85.38 %MaxLitNum:4
% 85.30/85.38 %MaxfuncDepth:1
% 85.30/85.38 %SharedTerms:2
% 85.30/85.38 %goalClause: 18
% 85.30/85.38 %singleGoalClaCount:1
% 85.30/85.38 [18]~P2(a1)
% 85.30/85.38 [13]P1(x131,a1,x131)
% 85.30/85.38 [14]P1(a1,x141,x141)
% 85.30/85.38 [15]P1(x151,f3(x151),a1)
% 85.30/85.38 [16]P1(f3(x161),x161,a1)
% 85.30/85.38 [17]P1(x171,x172,f4(x171,x172))
% 85.30/85.38 [19]P2(x191)+P1(x191,f5(x191),f2(x191))+P1(f5(x191),x191,f2(x191))
% 85.30/85.38 [22]P2(x221)+~P1(x221,f5(x221),f2(x221))+~P1(f5(x221),x221,f2(x221))
% 85.30/85.38 [20]~P2(x202)+~P1(x202,x201,x203)+P1(x201,x202,x203)
% 85.30/85.38 [21]~P1(x213,x214,x211)+E(x211,x212)+~P1(x213,x214,x212)
% 85.30/85.38 [23]~P1(x236,x234,x231)+P1(x231,x232,x233)+~P1(x234,x232,x235)+~P1(x236,x235,x233)
% 85.30/85.38 [24]~P1(x241,x246,x244)+P1(x241,x242,x243)+~P1(x244,x245,x243)+~P1(x246,x245,x242)
% 85.30/85.38 %EqnAxiom
% 85.30/85.38 [1]E(x11,x11)
% 85.30/85.38 [2]E(x22,x21)+~E(x21,x22)
% 85.30/85.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 85.30/85.38 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 85.30/85.38 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 85.30/85.38 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 85.30/85.38 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 85.30/85.38 [8]~E(x81,x82)+E(f5(x81),f5(x82))
% 85.30/85.38 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 85.30/85.38 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 85.30/85.38 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 85.30/85.38 [12]~P2(x121)+P2(x122)+~E(x121,x122)
% 85.30/85.38
% 85.30/85.38 %-------------------------------------------
% 85.41/85.39 cnf(25,plain,
% 85.41/85.39 (E(x251,f4(x251,a1))),
% 85.41/85.39 inference(scs_inference,[],[13,17,21])).
% 85.41/85.39 cnf(26,plain,
% 85.41/85.39 (P1(x261,x262,f4(x261,x262))),
% 85.41/85.39 inference(rename_variables,[],[17])).
% 85.41/85.39 cnf(28,plain,
% 85.41/85.39 (P1(f4(x281,a1),a1,x281)),
% 85.41/85.39 inference(scs_inference,[],[13,17,21,9])).
% 85.41/85.39 cnf(30,plain,
% 85.41/85.39 (P1(x301,a1,x301)),
% 85.41/85.39 inference(rename_variables,[],[13])).
% 85.41/85.39 cnf(31,plain,
% 85.41/85.39 (P1(x311,f3(x311),f4(a1,a1))),
% 85.41/85.39 inference(scs_inference,[],[13,17,15,21,9,10,11])).
% 85.41/85.39 cnf(32,plain,
% 85.41/85.39 (P1(x321,f4(a1,a1),x321)),
% 85.41/85.39 inference(scs_inference,[],[13,30,17,26,15,21,9,10,11,24])).
% 85.41/85.39 cnf(36,plain,
% 85.41/85.39 (~P2(f4(a1,a1))),
% 85.41/85.39 inference(scs_inference,[],[18,13,30,17,26,15,21,9,10,11,24,2,12])).
% 85.41/85.39 cnf(37,plain,
% 85.41/85.39 (E(f4(x371,a1),x371)),
% 85.41/85.39 inference(scs_inference,[],[25,2])).
% 85.41/85.39 cnf(38,plain,
% 85.41/85.39 (E(f3(f4(a1,a1)),a1)),
% 85.41/85.39 inference(scs_inference,[],[32,25,16,2,21])).
% 85.41/85.39 cnf(40,plain,
% 85.41/85.39 (P1(x401,f4(a1,a1),x401)),
% 85.41/85.39 inference(rename_variables,[],[32])).
% 85.41/85.39 cnf(42,plain,
% 85.41/85.39 (P1(x421,f4(a1,a1),f4(x421,a1))),
% 85.41/85.39 inference(scs_inference,[],[32,40,25,16,2,21,11])).
% 85.41/85.39 cnf(43,plain,
% 85.41/85.39 (P1(x431,f4(a1,a1),x431)),
% 85.41/85.40 inference(rename_variables,[],[32])).
% 85.41/85.40 cnf(44,plain,
% 85.41/85.40 (P1(x441,f4(f4(a1,a1),a1),x441)),
% 85.41/85.40 inference(scs_inference,[],[32,40,43,25,16,2,21,11,10])).
% 85.41/85.40 cnf(45,plain,
% 85.41/85.40 (E(x451,f4(x451,a1))),
% 85.41/85.40 inference(rename_variables,[],[25])).
% 85.41/85.40 cnf(47,plain,
% 85.41/85.40 (P1(f4(x471,a1),f4(a1,a1),x471)),
% 85.41/85.40 inference(scs_inference,[],[36,32,40,43,25,45,16,2,21,11,10,12,9])).
% 85.41/85.40 cnf(48,plain,
% 85.41/85.40 (P1(x481,f4(a1,a1),x481)),
% 85.41/85.40 inference(rename_variables,[],[32])).
% 85.41/85.40 cnf(49,plain,
% 85.41/85.40 (P1(a1,f3(f4(a1,a1)),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[36,32,40,43,48,31,25,45,14,16,2,21,11,10,12,9,23])).
% 85.41/85.40 cnf(51,plain,
% 85.41/85.40 (P1(x511,f4(a1,a1),x511)),
% 85.41/85.40 inference(rename_variables,[],[32])).
% 85.41/85.40 cnf(54,plain,
% 85.41/85.40 (P1(x541,f4(f4(a1,a1),f4(a1,a1)),x541)),
% 85.41/85.40 inference(scs_inference,[],[36,32,40,43,48,51,31,25,45,14,16,17,2,21,11,10,12,9,23,24])).
% 85.41/85.40 cnf(59,plain,
% 85.41/85.40 (E(a1,f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[38,2])).
% 85.41/85.40 cnf(60,plain,
% 85.41/85.40 (E(f4(f4(x601,a1),a1),x601)),
% 85.41/85.40 inference(scs_inference,[],[42,47,38,2,21])).
% 85.41/85.40 cnf(63,plain,
% 85.41/85.40 (E(f4(a1,a1),f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[42,47,37,38,2,21,3])).
% 85.41/85.40 cnf(64,plain,
% 85.41/85.40 (E(f4(x641,a1),x641)),
% 85.41/85.40 inference(rename_variables,[],[37])).
% 85.41/85.40 cnf(66,plain,
% 85.41/85.40 (P1(a1,x661,f4(x661,a1))),
% 85.41/85.40 inference(scs_inference,[],[18,42,47,37,64,38,14,2,21,3,12,10])).
% 85.41/85.40 cnf(68,plain,
% 85.41/85.40 (P1(f4(x681,a1),f4(f4(a1,a1),f4(a1,a1)),x681)),
% 85.41/85.40 inference(scs_inference,[],[18,54,42,47,37,64,38,14,2,21,3,12,10,11])).
% 85.41/85.40 cnf(69,plain,
% 85.41/85.40 (P1(x691,f4(f4(a1,a1),f4(a1,a1)),x691)),
% 85.41/85.40 inference(rename_variables,[],[54])).
% 85.41/85.40 cnf(70,plain,
% 85.41/85.40 (P1(x701,f4(f4(a1,a1),f4(a1,a1)),f4(x701,a1))),
% 85.41/85.40 inference(scs_inference,[],[18,54,69,42,47,37,64,38,14,2,21,3,12,10,11,9])).
% 85.41/85.40 cnf(71,plain,
% 85.41/85.40 (P1(x711,f4(f4(a1,a1),f4(a1,a1)),x711)),
% 85.41/85.40 inference(rename_variables,[],[54])).
% 85.41/85.40 cnf(72,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[18,54,69,71,42,47,37,64,38,31,14,2,21,3,12,10,11,9,24])).
% 85.41/85.40 cnf(74,plain,
% 85.41/85.40 (P1(x741,f4(f4(a1,a1),f4(a1,a1)),x741)),
% 85.41/85.40 inference(rename_variables,[],[54])).
% 85.41/85.40 cnf(76,plain,
% 85.41/85.40 (P1(f4(x761,a1),f4(f4(a1,a1),a1),x761)),
% 85.41/85.40 inference(scs_inference,[],[18,54,69,71,74,44,42,47,37,64,38,31,14,2,21,3,12,10,11,9,24,23])).
% 85.41/85.40 cnf(80,plain,
% 85.41/85.40 (E(f3(f4(a1,a1)),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[63,2])).
% 85.41/85.40 cnf(81,plain,
% 85.41/85.40 (E(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[72,63,32,2,21])).
% 85.41/85.40 cnf(84,plain,
% 85.41/85.40 (P1(f4(x841,a1),f3(f4(a1,a1)),x841)),
% 85.41/85.40 inference(scs_inference,[],[72,63,28,59,32,2,21,10])).
% 85.41/85.40 cnf(85,plain,
% 85.41/85.40 (P1(a1,a1,f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[72,63,28,66,59,32,2,21,10,11])).
% 85.41/85.40 cnf(87,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),a1,a1)),
% 85.41/85.40 inference(scs_inference,[],[72,63,28,66,59,32,2,21,10,11,9])).
% 85.41/85.40 cnf(89,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,a1)),
% 85.41/85.40 inference(scs_inference,[],[72,63,68,28,66,59,32,2,21,10,11,9,24])).
% 85.41/85.40 cnf(92,plain,
% 85.41/85.40 (P1(f4(f4(x921,a1),a1),f4(a1,a1),x921)),
% 85.41/85.40 inference(scs_inference,[],[72,63,70,68,28,66,59,32,47,2,21,10,11,9,24,23])).
% 85.41/85.40 cnf(95,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[81,2])).
% 85.41/85.40 cnf(96,plain,
% 85.41/85.40 (~P2(f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[36,81,2,12])).
% 85.41/85.40 cnf(97,plain,
% 85.41/85.40 (E(x971,f4(f4(x971,a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[36,81,92,32,2,12,21])).
% 85.41/85.40 cnf(100,plain,
% 85.41/85.40 (P1(x1001,f3(f4(a1,a1)),x1001)),
% 85.41/85.40 inference(scs_inference,[],[36,81,92,59,32,13,2,12,21,10])).
% 85.41/85.40 cnf(101,plain,
% 85.41/85.40 (P1(a1,f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[36,81,92,42,59,32,13,2,12,21,10,11])).
% 85.41/85.40 cnf(103,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),x1031,f4(x1031,a1))),
% 85.41/85.40 inference(scs_inference,[],[36,81,92,42,66,59,32,13,2,12,21,10,11,9])).
% 85.41/85.40 cnf(104,plain,
% 85.41/85.40 (P1(x1041,a1,f4(f4(x1041,a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[36,81,84,92,87,42,66,59,32,17,13,2,12,21,10,11,9,23])).
% 85.41/85.40 cnf(107,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),f4(a1,a1)),a1)),
% 85.41/85.40 inference(scs_inference,[],[95,37,3])).
% 85.41/85.40 cnf(109,plain,
% 85.41/85.40 (E(a1,f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[95,89,37,13,3,21])).
% 85.41/85.40 cnf(112,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),f4(x1121,a1),x1121)),
% 85.41/85.40 inference(scs_inference,[],[95,89,103,60,37,13,3,21,11])).
% 85.41/85.40 cnf(113,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),x1131,f4(x1131,a1))),
% 85.41/85.40 inference(rename_variables,[],[103])).
% 85.41/85.40 cnf(114,plain,
% 85.41/85.40 (P1(f4(a1,a1),x1141,f4(x1141,a1))),
% 85.41/85.40 inference(scs_inference,[],[95,80,89,103,113,60,37,13,3,21,11,9])).
% 85.41/85.40 cnf(115,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[95,100,80,89,103,113,60,37,31,13,3,21,11,9,24])).
% 85.41/85.40 cnf(117,plain,
% 85.41/85.40 (P1(x1171,f3(f4(a1,a1)),x1171)),
% 85.41/85.40 inference(rename_variables,[],[100])).
% 85.41/85.40 cnf(119,plain,
% 85.41/85.40 (P1(f4(f4(x1191,a1),a1),a1,x1191)),
% 85.41/85.40 inference(scs_inference,[],[95,100,117,80,89,103,113,60,92,37,31,13,3,21,11,9,24,23])).
% 85.41/85.40 cnf(123,plain,
% 85.41/85.40 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 85.41/85.40 inference(scs_inference,[],[109,16,10])).
% 85.41/85.40 cnf(125,plain,
% 85.41/85.40 (P1(x1251,f3(x1251),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[109,15,16,10,11])).
% 85.41/85.40 cnf(126,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[109,15,16,10,11,9])).
% 85.41/85.40 cnf(128,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),f4(x1281,a1),f4(x1281,a1))),
% 85.41/85.40 inference(scs_inference,[],[115,114,109,15,16,10,11,9,24])).
% 85.41/85.40 cnf(130,plain,
% 85.41/85.40 (P1(f4(a1,a1),x1301,x1301)),
% 85.41/85.40 inference(scs_inference,[],[115,114,112,109,15,16,10,11,9,24,23])).
% 85.41/85.40 cnf(133,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[125,14,21])).
% 85.41/85.40 cnf(134,plain,
% 85.41/85.40 (P1(a1,x1341,x1341)),
% 85.41/85.40 inference(rename_variables,[],[14])).
% 85.41/85.40 cnf(135,plain,
% 85.41/85.40 (P1(x1351,f3(x1351),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(rename_variables,[],[125])).
% 85.41/85.40 cnf(137,plain,
% 85.41/85.40 (P1(f4(a1,a1),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[130,125,107,14,21,10])).
% 85.41/85.40 cnf(138,plain,
% 85.41/85.40 (P1(f4(a1,a1),x1381,x1381)),
% 85.41/85.40 inference(rename_variables,[],[130])).
% 85.41/85.40 cnf(139,plain,
% 85.41/85.40 (P1(f3(x1391),x1391,f4(f4(a1,a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[130,125,107,97,14,16,21,10,11])).
% 85.41/85.40 cnf(140,plain,
% 85.41/85.40 (E(x1401,f4(f4(x1401,a1),a1))),
% 85.41/85.40 inference(rename_variables,[],[97])).
% 85.41/85.40 cnf(141,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),a1),x1411,x1411)),
% 85.41/85.40 inference(scs_inference,[],[130,125,107,97,140,14,134,16,21,10,11,9])).
% 85.41/85.40 cnf(143,plain,
% 85.41/85.40 (P1(f4(a1,a1),f3(a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[130,138,125,107,97,140,123,54,14,134,16,21,10,11,9,24])).
% 85.41/85.40 cnf(145,plain,
% 85.41/85.40 (P1(f4(a1,a1),x1451,x1451)),
% 85.41/85.40 inference(rename_variables,[],[130])).
% 85.41/85.40 cnf(147,plain,
% 85.41/85.40 (P1(x1471,f3(x1471),f4(f4(a1,a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[130,138,145,125,135,107,97,140,123,54,70,14,134,16,21,10,11,9,24,23])).
% 85.41/85.40 cnf(151,plain,
% 85.41/85.40 (E(f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[130,138,145,125,135,107,97,140,123,54,70,14,134,16,21,10,11,9,24,23,2])).
% 85.41/85.40 cnf(152,plain,
% 85.41/85.40 (~P2(f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[96,130,138,145,125,135,107,97,140,123,54,70,14,134,16,21,10,11,9,24,23,2,12])).
% 85.41/85.40 cnf(153,plain,
% 85.41/85.40 (E(f3(a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[151,95,3])).
% 85.41/85.40 cnf(154,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[147,151,95,14,3,21])).
% 85.41/85.40 cnf(156,plain,
% 85.41/85.40 (P1(x1561,f3(x1561),f4(f4(a1,a1),a1))),
% 85.41/85.40 inference(rename_variables,[],[147])).
% 85.41/85.40 cnf(158,plain,
% 85.41/85.40 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[147,133,151,130,95,14,3,21,10])).
% 85.41/85.40 cnf(160,plain,
% 85.41/85.40 (P1(a1,f4(a1,a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[147,101,133,151,130,95,14,3,21,10,11])).
% 85.41/85.40 cnf(161,plain,
% 85.41/85.40 (P1(x1611,f4(f4(a1,a1),a1),f4(x1611,a1))),
% 85.41/85.40 inference(scs_inference,[],[147,101,76,133,151,130,95,60,14,3,21,10,11,9])).
% 85.41/85.40 cnf(162,plain,
% 85.41/85.40 (P1(f4(x1621,a1),f4(f4(a1,a1),a1),x1621)),
% 85.41/85.40 inference(rename_variables,[],[76])).
% 85.41/85.40 cnf(163,plain,
% 85.41/85.40 (P1(x1631,f3(x1631),f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[147,156,141,101,76,133,151,130,95,100,60,14,3,21,10,11,9,24])).
% 85.41/85.40 cnf(167,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),a1),f4(x1671,a1),x1671)),
% 85.41/85.40 inference(scs_inference,[],[147,156,141,139,101,76,162,133,151,130,95,100,60,14,3,21,10,11,9,24,23])).
% 85.41/85.40 cnf(171,plain,
% 85.41/85.40 (E(f4(a1,a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[147,156,141,139,101,76,162,133,151,130,95,100,60,14,3,21,10,11,9,24,23,2])).
% 85.41/85.40 cnf(172,plain,
% 85.41/85.40 (E(f3(a1),f4(f4(a1,a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[154,2])).
% 85.41/85.40 cnf(173,plain,
% 85.41/85.40 (E(a1,f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[154,97,2,3])).
% 85.41/85.40 cnf(175,plain,
% 85.41/85.40 (E(f3(f4(a1,a1)),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[163,154,97,14,2,3,21])).
% 85.41/85.40 cnf(177,plain,
% 85.41/85.40 (P1(x1771,f3(x1771),f3(f4(a1,a1)))),
% 85.41/85.40 inference(rename_variables,[],[163])).
% 85.41/85.40 cnf(179,plain,
% 85.41/85.40 (P1(a1,f4(a1,a1),f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[163,177,153,154,97,14,2,3,21,10])).
% 85.41/85.40 cnf(181,plain,
% 85.41/85.40 (P1(a1,f4(f4(a1,a1),a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[163,177,161,171,153,154,97,14,2,3,21,10,11])).
% 85.41/85.40 cnf(183,plain,
% 85.41/85.40 (P1(f3(a1),f4(x1831,a1),x1831)),
% 85.41/85.40 inference(scs_inference,[],[163,177,161,167,171,153,154,97,14,2,3,21,10,11,9])).
% 85.41/85.40 cnf(184,plain,
% 85.41/85.40 (E(f3(a1),f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[175,2])).
% 85.41/85.40 cnf(185,plain,
% 85.41/85.40 (E(f3(a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[175,107,151,2,3])).
% 85.41/85.40 cnf(186,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),f3(a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[128,175,107,171,151,2,3,10])).
% 85.41/85.40 cnf(188,plain,
% 85.41/85.40 (P1(a1,f3(f4(a1,a1)),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[49,128,175,107,171,151,2,3,10,11])).
% 85.41/85.40 cnf(189,plain,
% 85.41/85.40 (P1(f3(a1),f3(f4(a1,a1)),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[49,128,175,173,107,171,151,2,3,10,11,9])).
% 85.41/85.40 cnf(192,plain,
% 85.41/85.40 (P1(a1,f4(f3(a1),a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[49,128,183,175,137,143,173,87,107,171,151,2,3,10,11,9,24,23])).
% 85.41/85.40 cnf(195,plain,
% 85.41/85.40 (E(f4(a1,a1),f4(f3(a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[186,103,21])).
% 85.41/85.40 cnf(198,plain,
% 85.41/85.40 (P1(f3(a1),f4(a1,a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[186,189,80,103,21,10])).
% 85.41/85.40 cnf(199,plain,
% 85.41/85.40 (P1(f4(a1,a1),f3(a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[158,186,189,80,103,95,21,10,11])).
% 85.41/85.40 cnf(200,plain,
% 85.41/85.40 (P1(f3(a1),f4(f3(a1),a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[158,186,189,192,80,103,173,95,21,10,11,9])).
% 85.41/85.40 cnf(201,plain,
% 85.41/85.40 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[158,186,189,192,80,103,173,95,21,10,11,9,24])).
% 85.41/85.40 cnf(203,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[158,186,189,192,80,103,183,173,95,28,21,10,11,9,24,23])).
% 85.41/85.40 cnf(207,plain,
% 85.41/85.40 (E(f4(f3(a1),a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[158,186,189,192,80,103,183,173,95,28,21,10,11,9,24,23,2])).
% 85.41/85.40 cnf(208,plain,
% 85.41/85.40 (~P2(f4(f3(a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[36,158,186,189,192,80,103,183,173,95,28,21,10,11,9,24,23,2,12])).
% 85.41/85.40 cnf(209,plain,
% 85.41/85.40 (E(f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 85.41/85.40 inference(scs_inference,[],[199,17,21])).
% 85.41/85.40 cnf(212,plain,
% 85.41/85.40 (E(f4(f3(a1),a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[207,199,37,17,21,3])).
% 85.41/85.40 cnf(214,plain,
% 85.41/85.40 (P1(f3(a1),f4(f3(a1),a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[207,195,199,198,37,17,21,3,10])).
% 85.41/85.40 cnf(215,plain,
% 85.41/85.40 (P1(a1,a1,f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[207,195,199,198,85,175,37,17,21,3,10,11])).
% 85.41/85.40 cnf(216,plain,
% 85.41/85.40 (P1(f4(f3(a1),a1),f3(a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[207,195,199,198,85,175,37,17,21,3,10,11,9])).
% 85.41/85.40 cnf(217,plain,
% 85.41/85.40 (P1(f4(a1,a1),a1,f4(f3(a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[207,195,199,198,200,85,175,130,37,17,21,3,10,11,9,24])).
% 85.41/85.40 cnf(220,plain,
% 85.41/85.40 (P1(f3(a1),f3(a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[207,195,199,198,160,200,85,175,130,37,17,21,3,10,11,9,24,23])).
% 85.41/85.40 cnf(222,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[207,195,199,198,160,200,85,175,130,37,17,21,3,10,11,9,24,23,2])).
% 85.41/85.40 cnf(224,plain,
% 85.41/85.40 (E(a1,f4(f3(a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[212,2])).
% 85.41/85.40 cnf(225,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),f3(a1)),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[222,212,171,2,3])).
% 85.41/85.40 cnf(226,plain,
% 85.41/85.40 (P1(f3(a1),a1,f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[222,214,212,171,2,3,10])).
% 85.41/85.40 cnf(227,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[222,214,203,212,173,171,2,3,10,11])).
% 85.41/85.40 cnf(229,plain,
% 85.41/85.40 (P1(f3(a1),f3(a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[185,222,214,203,212,68,54,173,171,2,3,10,11,9,24])).
% 85.41/85.40 cnf(230,plain,
% 85.41/85.40 (P1(f4(x2301,a1),f4(f4(a1,a1),f4(a1,a1)),x2301)),
% 85.41/85.40 inference(rename_variables,[],[68])).
% 85.41/85.40 cnf(233,plain,
% 85.41/85.40 (P1(f4(a1,a1),f4(a1,a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[185,222,214,216,201,203,212,68,230,54,173,171,2,3,10,11,9,24,23])).
% 85.41/85.40 cnf(236,plain,
% 85.41/85.40 (E(f3(a1),f4(f4(a1,a1),f3(a1)))),
% 85.41/85.40 inference(scs_inference,[],[225,2])).
% 85.41/85.40 cnf(237,plain,
% 85.41/85.40 (E(f3(a1),f4(f3(a1),f3(a1)))),
% 85.41/85.40 inference(scs_inference,[],[220,225,17,2,21])).
% 85.41/85.40 cnf(240,plain,
% 85.41/85.40 (E(f4(f4(a1,a1),f3(a1)),a1)),
% 85.41/85.40 inference(scs_inference,[],[220,225,185,17,2,21,3])).
% 85.41/85.40 cnf(241,plain,
% 85.41/85.40 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[209,220,233,225,185,17,2,21,3,10])).
% 85.41/85.40 cnf(242,plain,
% 85.41/85.40 (P1(f3(a1),f3(a1),f3(f4(a1,a1)))),
% 85.41/85.40 inference(scs_inference,[],[184,209,220,233,225,185,17,2,21,3,10,11])).
% 85.41/85.40 cnf(243,plain,
% 85.41/85.40 (P1(f3(f4(a1,a1)),f3(a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[184,209,220,233,225,185,17,2,21,3,10,11,9])).
% 85.41/85.40 cnf(244,plain,
% 85.41/85.40 (P1(f4(a1,a1),a1,f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[184,209,220,233,225,185,84,100,17,2,21,3,10,11,9,24])).
% 85.41/85.40 cnf(248,plain,
% 85.41/85.40 (P1(f4(a1,a1),f4(f3(a1),a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[184,209,220,233,225,226,185,192,84,100,17,2,21,3,10,11,9,24,23])).
% 85.41/85.40 cnf(250,plain,
% 85.41/85.40 (E(f4(f3(a1),f3(a1)),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[237,2])).
% 85.41/85.40 cnf(252,plain,
% 85.41/85.40 (P1(f3(a1),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 85.41/85.40 inference(scs_inference,[],[152,229,237,209,2,12,11])).
% 85.41/85.40 cnf(253,plain,
% 85.41/85.40 (P1(f4(a1,a1),f4(f3(a1),a1),f3(a1))),
% 85.41/85.40 inference(scs_inference,[],[152,229,237,244,224,209,2,12,11,10])).
% 85.41/85.40 cnf(254,plain,
% 85.41/85.40 (P1(f4(f4(a1,a1),a1),f3(a1),f4(a1,a1))),
% 85.41/85.40 inference(scs_inference,[],[152,172,229,237,244,224,209,2,12,11,10,9])).
% 85.41/85.40 cnf(255,plain,
% 85.41/85.40 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),a1))),
% 85.41/85.40 inference(scs_inference,[],[152,248,172,229,237,244,224,209,161,76,2,12,11,10,9,24])).
% 85.41/85.40 cnf(259,plain,
% 85.41/85.40 (P1(f3(a1),f3(a1),a1)),
% 85.41/85.40 inference(scs_inference,[],[152,248,172,229,243,237,244,224,209,161,112,76,2,12,11,10,9,24,23])).
% 85.41/85.40 cnf(263,plain,
% 85.41/85.40 (E(a1,f4(f4(a1,a1),f3(a1)))),
% 85.41/85.40 inference(scs_inference,[],[240,2])).
% 85.41/85.40 cnf(264,plain,
% 85.41/85.41 (E(f4(f3(a1),f3(a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[250,240,153,2,3])).
% 85.41/85.41 cnf(265,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[241,250,240,153,2,3,11])).
% 85.41/85.41 cnf(268,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[254,241,215,250,242,240,153,198,224,233,2,3,11,10,9,24])).
% 85.41/85.41 cnf(270,plain,
% 85.41/85.41 (P1(a1,a1,f4(f3(a1),a1))),
% 85.41/85.41 inference(scs_inference,[],[254,241,259,215,250,242,104,240,153,198,224,233,183,2,3,11,10,9,24,23])).
% 85.41/85.41 cnf(274,plain,
% 85.41/85.41 (E(f4(a1,a1),f4(f3(a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[264,2])).
% 85.41/85.41 cnf(275,plain,
% 85.41/85.41 (E(f4(f3(a1),f3(a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[264,250,185,2,3])).
% 85.41/85.41 cnf(276,plain,
% 85.41/85.41 (P1(f3(a1),f4(f4(a1,a1),a1),a1)),
% 85.41/85.41 inference(scs_inference,[],[264,172,259,250,185,2,3,10])).
% 85.41/85.41 cnf(277,plain,
% 85.41/85.41 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[264,207,172,259,250,185,70,2,3,10,11])).
% 85.41/85.41 cnf(279,plain,
% 85.41/85.41 (P1(f4(f3(a1),a1),f3(a1),a1)),
% 85.41/85.41 inference(scs_inference,[],[264,207,172,143,259,250,185,195,70,2,3,10,11,9])).
% 85.41/85.41 cnf(280,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),f3(a1),a1)),
% 85.41/85.41 inference(scs_inference,[],[264,253,268,207,172,143,259,250,200,185,195,70,2,3,10,11,9,24])).
% 85.41/85.41 cnf(282,plain,
% 85.41/85.41 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[265,264,253,268,207,172,143,259,250,200,185,195,70,2,3,10,11,9,24,23])).
% 85.41/85.41 cnf(284,plain,
% 85.41/85.41 (E(a1,f4(f3(a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[275,2])).
% 85.41/85.41 cnf(287,plain,
% 85.41/85.41 (P1(a1,f4(f3(a1),f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[274,263,275,160,237,2,9,11,10])).
% 85.41/85.41 cnf(288,plain,
% 85.41/85.41 (P1(f3(a1),f3(a1),f4(f4(a1,a1),a1))),
% 85.41/85.41 inference(scs_inference,[],[274,227,277,263,275,160,237,42,2,9,11,10,24])).
% 85.41/85.41 cnf(291,plain,
% 85.41/85.41 (P1(a1,f4(f4(a1,a1),f3(a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[274,282,126,227,277,263,275,160,237,42,2,9,11,10,24,23])).
% 85.41/85.41 cnf(293,plain,
% 85.41/85.41 (P1(f4(f3(a1),f3(a1)),a1,f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[284,215,9])).
% 85.41/85.41 cnf(294,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[284,215,244,9,10])).
% 85.41/85.41 cnf(299,plain,
% 85.41/85.41 (P1(x2991,f4(f4(a1,a1),f3(a1)),x2991)),
% 85.41/85.41 inference(scs_inference,[],[217,291,179,119,284,215,244,236,47,9,10,11,24,23])).
% 85.41/85.41 cnf(301,plain,
% 85.41/85.41 (P1(f3(a1),a1,f4(f3(a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[274,226,11])).
% 85.41/85.41 cnf(302,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(a1,a1),f3(f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[163,274,226,80,11,10])).
% 85.41/85.41 cnf(304,plain,
% 85.41/85.41 (P1(a1,f4(x3041,a1),x3041)),
% 85.41/85.41 inference(scs_inference,[],[163,274,167,226,80,60,11,10,9])).
% 85.41/85.41 cnf(306,plain,
% 85.41/85.41 (P1(f3(a1),a1,f4(f4(a1,a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[252,276,163,274,167,44,226,80,60,11,10,9,24])).
% 85.41/85.41 cnf(313,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f3(a1)),f4(x3131,a1),x3131)),
% 85.41/85.41 inference(scs_inference,[],[304,263,9])).
% 85.41/85.41 cnf(315,plain,
% 85.41/85.41 (P1(f4(a1,a1),a1,f3(f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[304,263,81,38,163,226,9,11,10])).
% 85.41/85.41 cnf(317,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[302,255,304,263,243,81,38,163,226,9,11,10,24])).
% 85.41/85.41 cnf(319,plain,
% 85.41/85.41 (P1(f3(f4(a1,a1)),f3(a1),a1)),
% 85.41/85.41 inference(scs_inference,[],[302,255,304,263,243,81,38,163,76,226,9,11,10,24,23])).
% 85.41/85.41 cnf(322,plain,
% 85.41/85.41 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[209,198,10])).
% 85.41/85.41 cnf(323,plain,
% 85.41/85.41 (P1(f3(a1),f3(a1),f4(f3(a1),a1))),
% 85.41/85.41 inference(scs_inference,[],[209,224,259,198,10,11])).
% 85.41/85.41 cnf(324,plain,
% 85.41/85.41 (P1(f3(a1),f4(x3241,a1),f4(x3241,a1))),
% 85.41/85.41 inference(scs_inference,[],[128,209,175,224,259,198,10,11,9])).
% 85.41/85.41 cnf(325,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[313,317,181,128,209,175,224,259,198,10,11,9,24])).
% 85.41/85.41 cnf(328,plain,
% 85.41/85.41 (P1(f3(a1),f3(f4(a1,a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[313,317,181,141,128,209,175,224,259,198,84,10,11,9,24,23])).
% 85.41/85.41 cnf(337,plain,
% 85.41/85.41 (P1(f3(f4(a1,a1)),a1,f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[319,328,324,188,240,207,151,112,130,9,10,11,24])).
% 85.41/85.41 cnf(339,plain,
% 85.41/85.41 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[319,328,322,324,325,188,240,313,207,151,112,130,9,10,11,24,23])).
% 85.41/85.41 cnf(342,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[222,32,11])).
% 85.41/85.41 cnf(344,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),a1,f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[222,212,167,32,11,10])).
% 85.41/85.41 cnf(350,plain,
% 85.41/85.41 (P1(x3501,f3(x3501),f4(f4(a1,a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[263,215,15,9,11])).
% 85.41/85.41 cnf(351,plain,
% 85.41/85.41 (P1(x3511,f3(a1),x3511)),
% 85.41/85.41 inference(scs_inference,[],[299,225,263,215,15,9,11,10])).
% 85.41/85.41 cnf(352,plain,
% 85.41/85.41 (P1(f3(a1),f4(f3(a1),f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[288,301,344,299,225,263,215,15,9,11,10,24])).
% 85.41/85.41 cnf(354,plain,
% 85.41/85.41 (P1(f4(a1,a1),a1,f4(f4(a1,a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[342,288,315,301,344,299,225,263,100,215,15,9,11,10,24,23])).
% 85.41/85.41 cnf(357,plain,
% 85.41/85.41 (E(f3(f3(a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[351,16,21])).
% 85.41/85.41 cnf(359,plain,
% 85.41/85.41 (P1(x3591,f3(a1),x3591)),
% 85.41/85.41 inference(rename_variables,[],[351])).
% 85.41/85.41 cnf(362,plain,
% 85.41/85.41 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[351,359,264,284,226,16,21,10,11])).
% 85.41/85.41 cnf(363,plain,
% 85.41/85.41 (P1(x3631,f3(a1),x3631)),
% 85.41/85.41 inference(rename_variables,[],[351])).
% 85.41/85.41 cnf(364,plain,
% 85.41/85.41 (P1(f4(a1,a1),f3(a1),f4(f3(a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[351,359,363,264,284,226,16,21,10,11,9])).
% 85.41/85.41 cnf(365,plain,
% 85.41/85.41 (P1(x3651,f3(a1),x3651)),
% 85.41/85.41 inference(rename_variables,[],[351])).
% 85.41/85.41 cnf(368,plain,
% 85.41/85.41 (P1(x3681,f3(x3681),f4(f4(a1,a1),f3(a1)))),
% 85.41/85.41 inference(rename_variables,[],[350])).
% 85.41/85.41 cnf(370,plain,
% 85.41/85.41 (P1(x3701,f3(x3701),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[350,368,351,359,363,365,306,264,325,284,299,226,16,21,10,11,9,23,24])).
% 85.41/85.41 cnf(373,plain,
% 85.41/85.41 (E(a1,f3(f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[350,368,351,359,363,365,306,264,325,284,299,226,16,21,10,11,9,23,24,2])).
% 85.41/85.41 cnf(375,plain,
% 85.41/85.41 (E(f3(f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[357,173,3])).
% 85.41/85.41 cnf(377,plain,
% 85.41/85.41 (P1(a1,f3(a1),f3(f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[357,373,351,173,143,3,11,9])).
% 85.41/85.41 cnf(379,plain,
% 85.41/85.41 (P1(f4(a1,a1),f3(f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[357,373,351,244,173,143,3,11,9,10])).
% 85.41/85.41 cnf(385,plain,
% 85.41/85.41 (E(f3(a1),f3(f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[294,280,370,362,323,357,373,351,244,173,143,3,11,9,10,23,24,2])).
% 85.41/85.41 cnf(386,plain,
% 85.41/85.41 (E(f3(f3(a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[377,31,21])).
% 85.41/85.41 cnf(389,plain,
% 85.41/85.41 (P1(a1,f3(f3(a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[385,377,370,31,21,10])).
% 85.41/85.41 cnf(390,plain,
% 85.41/85.41 (P1(x3901,f3(x3901),f3(a1))),
% 85.41/85.41 inference(rename_variables,[],[370])).
% 85.41/85.41 cnf(391,plain,
% 85.41/85.41 (P1(f3(f3(a1)),f4(x3911,a1),f4(x3911,a1))),
% 85.41/85.41 inference(scs_inference,[],[385,377,370,324,31,21,10,9])).
% 85.41/85.41 cnf(392,plain,
% 85.41/85.41 (P1(x3921,f3(x3921),f3(f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[385,377,370,390,324,31,21,10,9,11])).
% 85.41/85.41 cnf(393,plain,
% 85.41/85.41 (P1(a1,f4(f3(a1),f3(a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[385,352,279,377,370,390,324,31,21,10,9,11,23])).
% 85.41/85.41 cnf(398,plain,
% 85.41/85.41 (E(f4(a1,a1),f3(f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[339,364,385,352,279,377,370,390,324,299,31,21,10,9,11,23,24,2])).
% 85.41/85.41 cnf(399,plain,
% 85.41/85.41 (P1(f3(f3(a1)),f4(x3991,a1),x3991)),
% 85.41/85.41 inference(scs_inference,[],[304,373,9])).
% 85.41/85.41 cnf(404,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[386,392,216,352,304,373,351,9,11,10,23])).
% 85.41/85.41 cnf(420,plain,
% 85.41/85.41 (P1(x4201,f3(f3(a1)),f4(x4201,a1))),
% 85.41/85.41 inference(scs_inference,[],[398,233,42,9,10])).
% 85.41/85.41 cnf(423,plain,
% 85.41/85.41 (P1(a1,a1,f3(f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[393,293,392,398,233,114,42,9,10,11,23])).
% 85.41/85.41 cnf(431,plain,
% 85.41/85.41 (P1(x4311,f3(a1),f4(x4311,a1))),
% 85.41/85.41 inference(scs_inference,[],[420,375,351,11,10])).
% 85.41/85.41 cnf(432,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),x4321,f4(x4321,a1))),
% 85.41/85.41 inference(scs_inference,[],[420,375,97,351,66,11,10,9])).
% 85.41/85.41 cnf(438,plain,
% 85.41/85.41 (P1(f3(a1),x4381,f4(x4381,a1))),
% 85.41/85.41 inference(scs_inference,[],[432,154,9])).
% 85.41/85.41 cnf(439,plain,
% 85.41/85.41 (P1(f3(x4391),x4391,f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[432,139,154,9,11])).
% 85.41/85.41 cnf(440,plain,
% 85.41/85.41 (P1(f4(x4401,a1),f4(f3(a1),a1),x4401)),
% 85.41/85.41 inference(scs_inference,[],[432,139,195,154,47,9,11,10])).
% 85.41/85.41 cnf(445,plain,
% 85.41/85.41 (P1(a1,f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[404,270,432,391,139,101,399,195,154,47,9,11,10,23,24])).
% 85.41/85.41 cnf(448,plain,
% 85.41/85.41 (P1(x4481,f3(f4(a1,a1)),f4(x4481,a1))),
% 85.41/85.41 inference(scs_inference,[],[63,42,10])).
% 85.41/85.41 cnf(449,plain,
% 85.41/85.41 (P1(f3(x4491),x4491,f3(f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[63,59,42,16,10,11])).
% 85.41/85.41 cnf(450,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(x4501,a1),x4501)),
% 85.41/85.41 inference(scs_inference,[],[80,63,59,112,42,16,10,11,9])).
% 85.41/85.41 cnf(454,plain,
% 85.41/85.41 (P1(a1,x4541,f4(f4(x4541,a1),a1))),
% 85.41/85.41 inference(scs_inference,[],[287,389,438,293,392,399,80,63,59,112,42,16,10,11,9,23,24])).
% 85.41/85.41 cnf(457,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(x4571,a1),x4571)),
% 85.41/85.41 inference(scs_inference,[],[450,81,9])).
% 85.41/85.41 cnf(458,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[450,212,81,9,10])).
% 85.41/85.41 cnf(459,plain,
% 85.41/85.41 (P1(f3(x4591),x4591,f4(f4(a1,a1),f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[450,212,81,109,16,9,10,11])).
% 85.41/85.41 cnf(460,plain,
% 85.41/85.41 (P1(f4(x4601,a1),f3(a1),x4601)),
% 85.41/85.41 inference(scs_inference,[],[450,440,92,216,212,81,109,16,9,10,11,23])).
% 85.41/85.41 cnf(463,plain,
% 85.41/85.41 (P1(f3(x4631),f4(f4(x4631,a1),a1),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[449,450,440,337,104,92,216,212,81,109,16,9,10,11,23,24])).
% 85.41/85.41 cnf(466,plain,
% 85.41/85.41 (P1(x4661,f3(x4661),f4(f3(a1),a1))),
% 85.41/85.41 inference(scs_inference,[],[224,15,11])).
% 85.41/85.41 cnf(467,plain,
% 85.41/85.41 (P1(x4671,f4(f4(a1,a1),f3(a1)),f4(x4671,a1))),
% 85.41/85.41 inference(scs_inference,[],[209,224,15,42,11,10])).
% 85.41/85.41 cnf(468,plain,
% 85.41/85.41 (P1(f4(f3(a1),a1),f4(x4681,a1),x4681)),
% 85.41/85.41 inference(scs_inference,[],[304,209,224,15,42,11,10,9])).
% 85.41/85.41 cnf(469,plain,
% 85.41/85.41 (P1(f3(a1),f4(f4(x4691,a1),a1),x4691)),
% 85.41/85.41 inference(scs_inference,[],[445,457,304,209,224,15,42,11,10,9,23])).
% 85.41/85.41 cnf(470,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(x4701,a1),x4701)),
% 85.41/85.41 inference(rename_variables,[],[457])).
% 85.41/85.41 cnf(472,plain,
% 85.41/85.41 (P1(f3(f3(x4721)),f3(a1),f4(x4721,a1))),
% 85.41/85.41 inference(scs_inference,[],[459,445,457,470,463,304,209,224,15,42,11,10,9,23,24])).
% 85.41/85.41 cnf(476,plain,
% 85.41/85.41 (P1(f4(f3(a1),f3(a1)),f4(x4761,a1),x4761)),
% 85.41/85.41 inference(scs_inference,[],[450,274,9])).
% 85.41/85.41 cnf(477,plain,
% 85.41/85.41 (P1(x4771,f3(x4771),f4(f3(a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[450,274,31,9,11])).
% 85.41/85.41 cnf(478,plain,
% 85.41/85.41 (P1(f4(x4781,a1),f4(f3(a1),f3(a1)),x4781)),
% 85.41/85.41 inference(scs_inference,[],[450,274,284,28,31,9,11,10])).
% 85.41/85.41 cnf(481,plain,
% 85.41/85.41 (P1(x4811,f3(x4811),f4(f3(a1),a1))),
% 85.41/85.41 inference(rename_variables,[],[466])).
% 85.41/85.41 cnf(484,plain,
% 85.41/85.41 (P1(x4841,f4(f3(x4841),a1),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[466,481,439,431,460,450,274,284,28,31,9,11,10,23,24])).
% 85.41/85.41 cnf(490,plain,
% 85.41/85.41 (P1(f3(f3(a1)),x4901,f4(x4901,a1))),
% 85.41/85.41 inference(scs_inference,[],[476,207,373,66,10,9])).
% 85.41/85.41 cnf(495,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[354,25,10])).
% 85.41/85.41 cnf(505,plain,
% 85.41/85.41 (E(f4(x5051,a1),x5051)),
% 85.41/85.41 inference(rename_variables,[],[37])).
% 85.41/85.41 cnf(506,plain,
% 85.41/85.41 (P1(f4(f3(a1),a1),x5061,x5061)),
% 85.41/85.41 inference(scs_inference,[],[495,468,37,505,9,10])).
% 85.41/85.41 cnf(508,plain,
% 85.41/85.41 (P1(f3(f3(a1)),x5081,x5081)),
% 85.41/85.41 inference(scs_inference,[],[495,468,490,37,505,9,10,11])).
% 85.41/85.41 cnf(510,plain,
% 85.41/85.41 (P1(f4(x5101,a1),f4(f4(a1,a1),f3(a1)),x5101)),
% 85.41/85.41 inference(scs_inference,[],[467,60,11])).
% 85.41/85.41 cnf(512,plain,
% 85.41/85.41 (P1(x5121,f4(f3(a1),f3(a1)),f4(x5121,a1))),
% 85.41/85.41 inference(scs_inference,[],[467,478,60,11,9])).
% 85.41/85.41 cnf(514,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x5141,f4(x5141,a1))),
% 85.41/85.41 inference(scs_inference,[],[467,478,457,60,11,9,10])).
% 85.41/85.41 cnf(516,plain,
% 85.41/85.41 (P1(f4(f3(a1),a1),x5161,f4(x5161,a1))),
% 85.41/85.41 inference(scs_inference,[],[506,508,467,478,457,60,399,11,9,10,24])).
% 85.41/85.41 cnf(523,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[514,268,92,24])).
% 85.41/85.41 cnf(531,plain,
% 85.41/85.41 (P1(x5311,f4(f3(a1),a1),f4(x5311,a1))),
% 85.41/85.41 inference(scs_inference,[],[13,484,431,23])).
% 85.41/85.41 cnf(536,plain,
% 85.41/85.41 (P1(f3(a1),x5361,x5361)),
% 85.41/85.41 inference(scs_inference,[],[13,454,469,23])).
% 85.41/85.41 cnf(540,plain,
% 85.41/85.41 (P1(x5401,f4(f3(a1),a1),x5401)),
% 85.41/85.41 inference(scs_inference,[],[13,531,32,23])).
% 85.41/85.41 cnf(547,plain,
% 85.41/85.41 (P1(f3(f4(a1,a1)),x5471,x5471)),
% 85.41/85.41 inference(scs_inference,[],[536,240,184,351,11,9])).
% 85.41/85.41 cnf(548,plain,
% 85.41/85.41 (P1(f3(x5481),x5481,f4(f4(a1,a1),f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[439,236,11])).
% 85.41/85.41 cnf(549,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f3(a1)),x5491,x5491)),
% 85.41/85.41 inference(scs_inference,[],[439,536,236,11,9])).
% 85.41/85.41 cnf(552,plain,
% 85.41/85.41 (P1(f3(x5521),x5521,f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[548,222,237,259,10,11])).
% 85.41/85.41 cnf(556,plain,
% 85.41/85.41 (P1(a1,f4(f4(x5561,a1),a1),x5561)),
% 85.41/85.41 inference(scs_inference,[],[472,469,185,10,9])).
% 85.41/85.41 cnf(559,plain,
% 85.41/85.41 (P1(f3(f4(x5591,a1)),x5591,f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[13,552,540,472,440,275,469,185,10,9,11,24])).
% 85.41/85.41 cnf(564,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x5641,x5641)),
% 85.41/85.41 inference(scs_inference,[],[536,151,9])).
% 85.41/85.41 cnf(565,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f3(a1)),x5651,f4(x5651,a1))),
% 85.41/85.41 inference(scs_inference,[],[549,547,536,151,112,9,24])).
% 85.41/85.41 cnf(571,plain,
% 85.41/85.41 (E(x5711,f4(a1,x5711))),
% 85.41/85.41 inference(scs_inference,[],[14,17,21])).
% 85.41/85.41 cnf(581,plain,
% 85.41/85.41 (E(f4(a1,x5811),x5811)),
% 85.41/85.41 inference(scs_inference,[],[14,477,559,141,222,351,17,21,11,23,2])).
% 85.41/85.41 cnf(583,plain,
% 85.41/85.41 (E(f4(a1,x5831),f4(f4(x5831,a1),a1))),
% 85.41/85.41 inference(scs_inference,[],[581,97,3])).
% 85.41/85.41 cnf(585,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x5851,f4(a1,x5851))),
% 85.41/85.41 inference(scs_inference,[],[564,581,97,3,10])).
% 85.41/85.41 cnf(587,plain,
% 85.41/85.41 (P1(a1,f4(a1,x5871),x5871)),
% 85.41/85.41 inference(scs_inference,[],[14,564,581,97,3,10,11])).
% 85.41/85.41 cnf(589,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(f4(x5891,a1),a1),x5891)),
% 85.41/85.41 inference(scs_inference,[],[14,564,581,556,571,97,3,10,11,9])).
% 85.41/85.41 cnf(591,plain,
% 85.41/85.41 (E(f4(f4(x5911,a1),a1),f4(a1,x5911))),
% 85.41/85.41 inference(scs_inference,[],[14,564,581,556,571,97,3,10,11,9,2])).
% 85.41/85.41 cnf(593,plain,
% 85.41/85.41 (E(f4(a1,f4(x5931,a1)),x5931)),
% 85.41/85.41 inference(scs_inference,[],[585,457,21])).
% 85.41/85.41 cnf(594,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x5941,f4(a1,x5941))),
% 85.41/85.41 inference(rename_variables,[],[585])).
% 85.41/85.41 cnf(596,plain,
% 85.41/85.41 (E(f4(a1,x5961),f4(x5961,a1))),
% 85.41/85.41 inference(scs_inference,[],[585,583,457,37,21,3])).
% 85.41/85.41 cnf(598,plain,
% 85.41/85.41 (P1(a1,f4(f4(x5981,a1),a1),f4(a1,x5981))),
% 85.41/85.41 inference(scs_inference,[],[14,585,583,457,37,21,3,10])).
% 85.41/85.41 cnf(599,plain,
% 85.41/85.41 (P1(a1,x5991,x5991)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(601,plain,
% 85.41/85.41 (P1(a1,x6011,x6011)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(602,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(a1,x6021),x6021)),
% 85.41/85.41 inference(scs_inference,[],[14,599,585,583,587,457,571,37,21,3,10,11,9])).
% 85.41/85.41 cnf(604,plain,
% 85.41/85.41 (P1(f3(a1),x6041,f4(a1,x6041))),
% 85.41/85.41 inference(scs_inference,[],[14,599,601,458,585,594,583,587,457,571,37,21,3,10,11,9,23])).
% 85.41/85.41 cnf(605,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x6051,f4(a1,x6051))),
% 85.41/85.41 inference(rename_variables,[],[585])).
% 85.41/85.41 cnf(611,plain,
% 85.41/85.41 (E(x6111,f4(a1,f4(x6111,a1)))),
% 85.41/85.41 inference(scs_inference,[],[14,599,601,458,585,594,605,583,587,457,571,37,21,3,10,11,9,23,24,2])).
% 85.41/85.41 cnf(614,plain,
% 85.41/85.41 (E(f4(x6141,a1),f4(a1,x6141))),
% 85.41/85.41 inference(scs_inference,[],[596,2])).
% 85.41/85.41 cnf(616,plain,
% 85.41/85.41 (E(f4(a1,x6161),f4(x6161,a1))),
% 85.41/85.41 inference(rename_variables,[],[596])).
% 85.41/85.41 cnf(617,plain,
% 85.41/85.41 (E(f4(a1,a1),f4(a1,f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[208,523,596,585,2,12,21])).
% 85.41/85.41 cnf(620,plain,
% 85.41/85.41 (E(f4(a1,f4(x6201,a1)),f4(a1,x6201))),
% 85.41/85.41 inference(scs_inference,[],[208,523,596,616,585,591,2,12,21,3])).
% 85.41/85.41 cnf(622,plain,
% 85.41/85.41 (P1(a1,f4(a1,f4(x6221,a1)),x6221)),
% 85.41/85.41 inference(scs_inference,[],[14,208,523,611,596,616,585,591,2,12,21,3,10])).
% 85.41/85.41 cnf(623,plain,
% 85.41/85.41 (P1(a1,x6231,x6231)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(626,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),x6261,x6261)),
% 85.41/85.41 inference(scs_inference,[],[14,623,208,523,602,611,596,616,585,591,2,12,21,3,10,11,9])).
% 85.41/85.41 cnf(633,plain,
% 85.41/85.41 (E(f4(a1,x6331),f4(a1,f4(x6331,a1)))),
% 85.41/85.41 inference(scs_inference,[],[620,2])).
% 85.41/85.41 cnf(634,plain,
% 85.41/85.41 (E(f4(x6341,a1),f4(a1,f4(a1,x6341)))),
% 85.41/85.41 inference(scs_inference,[],[614,620,571,2,3])).
% 85.41/85.41 cnf(636,plain,
% 85.41/85.41 (P1(a1,f4(a1,x6361),f4(x6361,a1))),
% 85.41/85.41 inference(scs_inference,[],[14,614,620,571,2,3,10])).
% 85.41/85.41 cnf(637,plain,
% 85.41/85.41 (P1(a1,x6371,x6371)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(638,plain,
% 85.41/85.41 (P1(a1,f4(x6381,a1),f4(a1,x6381))),
% 85.41/85.41 inference(scs_inference,[],[14,637,614,620,571,2,3,10,11])).
% 85.41/85.41 cnf(640,plain,
% 85.41/85.41 (P1(f4(a1,f3(a1)),x6401,f4(x6401,a1))),
% 85.41/85.41 inference(scs_inference,[],[14,637,516,614,620,571,2,3,10,11,9])).
% 85.41/85.41 cnf(643,plain,
% 85.41/85.41 (E(f4(a1,f4(a1,x6431)),f4(x6431,a1))),
% 85.41/85.41 inference(scs_inference,[],[634,2])).
% 85.41/85.41 cnf(644,plain,
% 85.41/85.41 (E(f4(a1,f4(a1,a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[634,593,173,2,3])).
% 85.41/85.41 cnf(647,plain,
% 85.41/85.41 (P1(a1,x6471,x6471)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(650,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),x6501,f4(a1,x6501))),
% 85.41/85.41 inference(scs_inference,[],[14,647,604,634,593,172,173,2,3,10,11,9])).
% 85.41/85.41 cnf(652,plain,
% 85.41/85.41 (E(f4(a1,f3(a1)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[617,2])).
% 85.41/85.41 cnf(653,plain,
% 85.41/85.41 (E(f4(a1,f4(a1,x6531)),x6531)),
% 85.41/85.41 inference(scs_inference,[],[643,617,37,2,3])).
% 85.41/85.41 cnf(657,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),f4(a1,x6571),f4(x6571,a1))),
% 85.41/85.41 inference(scs_inference,[],[650,643,636,617,37,2,3,10,11])).
% 85.41/85.41 cnf(658,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),a1),x6581,f4(a1,x6581))),
% 85.41/85.41 inference(rename_variables,[],[650])).
% 85.41/85.41 cnf(659,plain,
% 85.41/85.41 (P1(f4(a1,a1),x6591,f4(a1,x6591))),
% 85.41/85.41 inference(scs_inference,[],[650,658,643,636,617,591,37,2,3,10,11,9])).
% 85.41/85.41 cnf(669,plain,
% 85.41/85.41 (E(x6691,f4(a1,f4(a1,x6691)))),
% 85.41/85.41 inference(scs_inference,[],[653,2])).
% 85.41/85.41 cnf(670,plain,
% 85.41/85.41 (E(f4(a1,f3(a1)),a1)),
% 85.41/85.41 inference(scs_inference,[],[659,653,460,2,21])).
% 85.41/85.41 cnf(672,plain,
% 85.41/85.41 (P1(f4(a1,a1),x6721,f4(a1,x6721))),
% 85.41/85.41 inference(rename_variables,[],[659])).
% 85.41/85.41 cnf(675,plain,
% 85.41/85.41 (P1(a1,x6751,x6751)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(676,plain,
% 85.41/85.41 (P1(a1,f4(a1,f4(a1,x6761)),x6761)),
% 85.41/85.41 inference(scs_inference,[],[14,675,659,653,460,2,21,10,11])).
% 85.41/85.41 cnf(678,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),x6781,f4(a1,x6781))),
% 85.41/85.41 inference(scs_inference,[],[14,675,659,672,653,633,460,2,21,10,11,9])).
% 85.41/85.41 cnf(680,plain,
% 85.41/85.41 (P1(f3(a1),f4(a1,f4(a1,a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[14,675,659,672,653,657,181,633,460,2,21,10,11,9,23])).
% 85.41/85.41 cnf(689,plain,
% 85.41/85.41 (E(a1,f4(a1,f3(a1)))),
% 85.41/85.41 inference(scs_inference,[],[670,2])).
% 85.41/85.41 cnf(690,plain,
% 85.41/85.41 (P1(f3(x6901),f4(a1,f4(a1,x6901)),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[669,670,552,2,10])).
% 85.41/85.41 cnf(694,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),f4(x6941,a1),f4(a1,x6941))),
% 85.41/85.41 inference(scs_inference,[],[669,638,670,552,450,2,10,11,9])).
% 85.41/85.41 cnf(696,plain,
% 85.41/85.41 (P1(f4(x6961,a1),f4(a1,f4(a1,a1)),f4(x6961,a1))),
% 85.41/85.41 inference(scs_inference,[],[669,680,638,670,552,472,450,2,10,11,9,23])).
% 85.41/85.41 cnf(699,plain,
% 85.41/85.41 (E(f3(a1),f4(a1,f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[644,2])).
% 85.41/85.41 cnf(705,plain,
% 85.41/85.41 (P1(f4(a1,x7051),f4(a1,f4(a1,a1)),f4(a1,x7051))),
% 85.41/85.41 inference(scs_inference,[],[14,678,696,598,652,644,689,617,450,2,10,11,9,23])).
% 85.41/85.41 cnf(709,plain,
% 85.41/85.41 (P1(a1,f4(a1,f4(a1,a1)),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[699,370,10])).
% 85.41/85.41 cnf(713,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(x7131,a1),f4(a1,x7131))),
% 85.41/85.41 inference(scs_inference,[],[14,694,670,699,620,370,10,11,9])).
% 85.41/85.41 cnf(723,plain,
% 85.41/85.41 (P1(f3(a1),f4(x7231,a1),f4(a1,x7231))),
% 85.41/85.41 inference(scs_inference,[],[14,678,694,644,10,11,9])).
% 85.41/85.41 cnf(727,plain,
% 85.41/85.41 (P1(f3(x7271),f4(f4(a1,x7271),a1),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[690,596,10])).
% 85.41/85.41 cnf(728,plain,
% 85.41/85.41 (E(f4(a1,x7281),f4(x7281,a1))),
% 85.41/85.41 inference(rename_variables,[],[596])).
% 85.41/85.41 cnf(729,plain,
% 85.41/85.41 (P1(f4(a1,x7291),f4(a1,f4(a1,a1)),f4(x7291,a1))),
% 85.41/85.41 inference(scs_inference,[],[690,705,596,728,10,11])).
% 85.41/85.41 cnf(730,plain,
% 85.41/85.41 (P1(f4(a1,x7301),f4(a1,f4(a1,a1)),f4(a1,x7301))),
% 85.41/85.41 inference(rename_variables,[],[705])).
% 85.41/85.41 cnf(731,plain,
% 85.41/85.41 (P1(f4(x7311,a1),f4(a1,f4(a1,a1)),f4(a1,x7311))),
% 85.41/85.41 inference(scs_inference,[],[690,705,730,596,728,10,11,9])).
% 85.41/85.41 cnf(733,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),f4(a1,x7331),x7331)),
% 85.41/85.41 inference(scs_inference,[],[14,626,690,705,730,587,596,728,10,11,9,23])).
% 85.41/85.41 cnf(738,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),f4(a1,x7381),f4(x7381,a1))),
% 85.41/85.41 inference(scs_inference,[],[733,620,10])).
% 85.41/85.41 cnf(750,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(a1,f4(x7501,a1)),x7501)),
% 85.41/85.41 inference(scs_inference,[],[602,633,10])).
% 85.41/85.41 cnf(763,plain,
% 85.41/85.41 (P1(f4(a1,x7631),a1,f4(x7631,a1))),
% 85.41/85.41 inference(scs_inference,[],[729,593,10])).
% 85.41/85.41 cnf(766,plain,
% 85.41/85.41 (P1(f4(a1,f3(a1)),x7661,f4(a1,x7661))),
% 85.41/85.41 inference(scs_inference,[],[729,659,552,617,593,10,11,9])).
% 85.41/85.41 cnf(771,plain,
% 85.41/85.41 (P1(f4(a1,x7711),f4(a1,f3(a1)),f4(x7711,a1))),
% 85.41/85.41 inference(scs_inference,[],[763,689,10])).
% 85.41/85.41 cnf(775,plain,
% 85.41/85.41 (P1(f3(a1),f4(a1,f4(x7751,a1)),x7751)),
% 85.41/85.41 inference(scs_inference,[],[379,766,750,763,604,508,385,652,689,10,9,11,23])).
% 85.41/85.41 cnf(779,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),a1,f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[733,670,10])).
% 85.41/85.41 cnf(783,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),x7831,f4(x7831,a1))),
% 85.41/85.41 inference(scs_inference,[],[733,766,438,670,699,10,11,9])).
% 85.41/85.41 cnf(790,plain,
% 85.41/85.41 (E(f4(f4(a1,x7901),a1),x7901)),
% 85.41/85.41 inference(scs_inference,[],[783,733,21])).
% 85.41/85.41 cnf(791,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),x7911,f4(x7911,a1))),
% 85.41/85.41 inference(rename_variables,[],[783])).
% 85.41/85.41 cnf(796,plain,
% 85.41/85.41 (E(x7961,f4(a1,f4(x7961,a1)))),
% 85.41/85.41 inference(rename_variables,[],[611])).
% 85.41/85.41 cnf(797,plain,
% 85.41/85.41 (P1(f3(a1),f3(a1),f4(a1,f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[783,477,733,386,611,796,259,304,21,10,9,11])).
% 85.41/85.41 cnf(803,plain,
% 85.41/85.41 (E(x8031,f4(f4(a1,x8031),a1))),
% 85.41/85.41 inference(scs_inference,[],[14,783,791,477,733,386,611,796,259,304,21,10,9,11,24,2])).
% 85.41/85.41 cnf(805,plain,
% 85.41/85.41 (E(f4(f4(a1,x8051),a1),f4(x8051,a1))),
% 85.41/85.41 inference(scs_inference,[],[790,25,3])).
% 85.41/85.41 cnf(807,plain,
% 85.41/85.41 (P1(f4(f3(a1),f3(a1)),x8071,f4(a1,x8071))),
% 85.41/85.41 inference(scs_inference,[],[790,476,25,3,10])).
% 85.41/85.41 cnf(809,plain,
% 85.41/85.41 (P1(x8091,f4(f4(a1,a1),f3(a1)),f4(a1,x8091))),
% 85.41/85.41 inference(scs_inference,[],[510,790,476,25,3,10,9])).
% 85.41/85.41 cnf(811,plain,
% 85.41/85.41 (P1(a1,f4(f4(a1,x8111),a1),x8111)),
% 85.41/85.41 inference(scs_inference,[],[14,510,790,476,25,3,10,9,11])).
% 85.41/85.41 cnf(813,plain,
% 85.41/85.41 (E(f4(x8131,a1),f4(f4(a1,x8131),a1))),
% 85.41/85.41 inference(scs_inference,[],[14,510,790,476,25,3,10,9,11,2])).
% 85.41/85.41 cnf(816,plain,
% 85.41/85.41 (P1(a1,x8161,x8161)),
% 85.41/85.41 inference(rename_variables,[],[14])).
% 85.41/85.41 cnf(821,plain,
% 85.41/85.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,x8211),x8211)),
% 85.41/85.41 inference(scs_inference,[],[14,816,565,813,811,713,431,10,11,9,23])).
% 85.41/85.41 cnf(826,plain,
% 85.41/85.41 (P1(f3(x8261),f4(x8261,a1),f4(a1,a1))),
% 85.41/85.41 inference(scs_inference,[],[727,805,10])).
% 85.41/85.41 cnf(830,plain,
% 85.41/85.41 (P1(f4(x8301,a1),f4(f4(a1,a1),f3(a1)),f4(a1,x8301))),
% 85.41/85.41 inference(scs_inference,[],[640,727,510,805,10,11,9])).
% 85.41/85.41 cnf(833,plain,
% 85.41/85.41 (P1(x8331,a1,f4(a1,x8331))),
% 85.41/85.41 inference(scs_inference,[],[809,240,10])).
% 85.41/85.41 cnf(834,plain,
% 85.41/85.41 (P1(f4(a1,x8341),f4(f4(a1,a1),f3(a1)),x8341)),
% 85.41/85.41 inference(scs_inference,[],[809,240,653,10,11])).
% 85.41/85.41 cnf(839,plain,
% 85.41/85.41 (P1(x8391,f4(a1,f4(a1,a1)),f4(a1,x8391))),
% 85.41/85.41 inference(scs_inference,[],[833,669,10])).
% 85.41/85.41 cnf(840,plain,
% 85.41/85.41 (E(x8401,f4(a1,f4(a1,x8401)))),
% 85.41/85.41 inference(rename_variables,[],[669])).
% 85.41/85.41 cnf(841,plain,
% 85.41/85.41 (P1(x8411,f3(x8411),f4(a1,f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[833,669,840,15,10,11])).
% 85.41/85.41 cnf(845,plain,
% 85.41/85.41 (P1(x8451,f3(x8451),f4(a1,f4(a1,a1)))),
% 85.41/85.41 inference(rename_variables,[],[841])).
% 85.41/85.41 cnf(848,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,a1)),f3(a1),a1)),
% 85.41/85.41 inference(scs_inference,[],[841,845,547,587,357,803,460,10,9,23])).
% 85.41/85.41 cnf(854,plain,
% 85.41/85.41 (P1(x8541,f4(a1,f4(a1,a1)),f4(x8541,a1))),
% 85.41/85.41 inference(scs_inference,[],[839,596,11])).
% 85.41/85.41 cnf(855,plain,
% 85.41/85.41 (P1(x8551,f4(a1,f4(a1,a1)),f4(a1,x8551))),
% 85.41/85.41 inference(rename_variables,[],[839])).
% 85.41/85.41 cnf(859,plain,
% 85.41/85.41 (P1(f3(a1),f4(a1,x8591),x8591)),
% 85.41/85.41 inference(scs_inference,[],[14,779,839,855,797,596,153,733,11,10,9,23])).
% 85.41/85.41 cnf(867,plain,
% 85.41/85.41 (P1(f4(a1,a1),f4(a1,x8671),f4(x8671,a1))),
% 85.41/85.41 inference(scs_inference,[],[821,826,738,643,583,10,11,9])).
% 85.41/85.41 cnf(872,plain,
% 85.41/85.41 (P1(f4(a1,x8721),f4(a1,a1),x8721)),
% 85.41/85.41 inference(scs_inference,[],[834,826,634,222,11,10])).
% 85.41/85.41 cnf(875,plain,
% 85.41/85.41 (P1(f4(a1,x8751),f3(a1),x8751)),
% 85.41/85.41 inference(scs_inference,[],[872,171,10])).
% 85.41/85.41 cnf(879,plain,
% 85.41/85.41 (P1(f3(x8791),f4(x8791,a1),f3(f4(a1,a1)))),
% 85.41/85.41 inference(scs_inference,[],[826,63,11])).
% 85.41/85.41 cnf(880,plain,
% 85.41/85.41 (P1(f4(a1,x8801),f4(a1,a1),f4(x8801,a1))),
% 85.41/85.41 inference(scs_inference,[],[771,826,652,63,11,10])).
% 85.41/85.41 cnf(881,plain,
% 85.41/85.41 (P1(f3(f4(a1,a1)),f4(a1,x8811),f4(x8811,a1))),
% 85.41/85.41 inference(scs_inference,[],[771,867,826,652,63,11,10,9])).
% 85.41/85.41 cnf(883,plain,
% 85.41/85.41 (P1(f4(x8831,a1),f3(a1),f4(a1,x8831))),
% 85.41/85.41 inference(scs_inference,[],[830,225,10])).
% 85.41/85.41 cnf(884,plain,
% 85.41/85.41 (P1(f3(x8841),f4(x8841,a1),f3(a1))),
% 85.41/85.41 inference(scs_inference,[],[879,830,175,225,10,11])).
% 85.41/85.41 cnf(885,plain,
% 85.41/85.41 (P1(f3(a1),f4(a1,x8851),f4(x8851,a1))),
% 85.41/85.41 inference(scs_inference,[],[879,830,881,175,225,10,11,9])).
% 85.41/85.41 cnf(889,plain,
% 85.41/85.41 (P1(f4(a1,x8891),f4(f4(a1,a1),f4(a1,a1)),f4(x8891,a1))),
% 85.41/85.41 inference(scs_inference,[],[880,885,207,81,11,10])).
% 85.41/85.41 cnf(897,plain,
% 85.41/85.41 (P1(f4(x8971,a1),f3(f4(a1,a1)),f4(a1,x8971))),
% 85.41/85.41 inference(scs_inference,[],[883,826,184,209,11,10])).
% 85.41/85.41 cnf(900,plain,
% 85.41/85.41 (P1(f4(a1,x9001),f4(a1,f4(a1,a1)),x9001)),
% 85.41/85.41 inference(scs_inference,[],[872,571,10])).
% 85.41/85.41 cnf(901,plain,
% 85.41/85.41 (E(x9011,f4(a1,x9011))),
% 85.41/85.41 inference(rename_variables,[],[571])).
% 85.41/85.41 cnf(904,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,x9041)),f4(a1,a1),x9041)),
% 85.41/85.41 inference(scs_inference,[],[872,880,212,571,901,10,11,9])).
% 85.41/85.41 cnf(909,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,x9091)),a1,x9091)),
% 85.41/85.41 inference(scs_inference,[],[807,904,581,11,10])).
% 85.41/85.41 cnf(910,plain,
% 85.41/85.41 (E(f4(a1,x9101),x9101)),
% 85.41/85.41 inference(rename_variables,[],[581])).
% 85.41/85.41 cnf(911,plain,
% 85.41/85.41 (P1(x9111,f4(a1,f4(a1,a1)),x9111)),
% 85.41/85.41 inference(scs_inference,[],[900,807,904,581,910,11,10,9])).
% 85.41/85.41 cnf(914,plain,
% 85.41/85.41 (P1(f4(x9141,a1),a1,f4(a1,x9141))),
% 85.41/85.41 inference(scs_inference,[],[731,593,10])).
% 85.41/85.41 cnf(915,plain,
% 85.41/85.41 (E(f4(a1,f4(x9151,a1)),x9151)),
% 85.41/85.41 inference(rename_variables,[],[593])).
% 85.41/85.41 cnf(916,plain,
% 85.41/85.41 (P1(f4(x9161,a1),f4(a1,f4(a1,a1)),x9161)),
% 85.41/85.41 inference(scs_inference,[],[731,839,593,915,10,11])).
% 85.41/85.41 cnf(919,plain,
% 85.41/85.41 (P1(f4(a1,f4(a1,x9191)),f3(a1),x9191)),
% 85.41/85.41 inference(scs_inference,[],[911,848,731,909,839,885,236,593,915,10,11,9,23])).
% 85.41/85.41 cnf(924,plain,
% 85.41/85.42 (P1(f4(a1,x9241),a1,x9241)),
% 85.41/85.42 inference(scs_inference,[],[884,834,237,240,11,10])).
% 85.41/85.42 cnf(927,plain,
% 85.41/85.42 (P1(f4(a1,x9271),f4(f4(a1,a1),f4(a1,a1)),x9271)),
% 85.41/85.42 inference(scs_inference,[],[924,109,10])).
% 85.41/85.42 cnf(933,plain,
% 85.41/85.42 (P1(f4(a1,x9331),f3(f3(a1)),x9331)),
% 85.41/85.42 inference(scs_inference,[],[448,875,385,790,11,10])).
% 85.41/85.42 cnf(938,plain,
% 85.41/85.42 (P1(f3(x9381),x9381,f4(a1,f4(a1,a1)))),
% 85.41/85.42 inference(scs_inference,[],[763,439,263,699,10,11])).
% 85.41/85.42 cnf(946,plain,
% 85.41/85.42 (P1(x9461,f4(f3(a1),f3(a1)),f4(a1,x9461))),
% 85.41/85.42 inference(scs_inference,[],[833,284,16,11,10])).
% 85.41/85.42 cnf(975,plain,
% 85.41/85.42 (P1(x9751,f4(f3(x9751),a1),f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[484,153,11])).
% 85.41/85.42 cnf(976,plain,
% 85.41/85.42 (P1(x9761,f3(a1),f4(a1,x9761))),
% 85.41/85.42 inference(scs_inference,[],[946,484,153,250,11,10])).
% 85.41/85.42 cnf(979,plain,
% 85.41/85.42 (P1(f4(x9791,a1),f4(a1,a1),f4(a1,x9791))),
% 85.41/85.42 inference(scs_inference,[],[897,80,10])).
% 85.41/85.42 cnf(991,plain,
% 85.41/85.42 (P1(f4(a1,x9911),f3(a1),f4(x9911,a1))),
% 85.41/85.42 inference(scs_inference,[],[889,133,10])).
% 85.41/85.42 cnf(995,plain,
% 85.41/85.42 (P1(x9951,f4(a1,a1),f4(a1,x9951))),
% 85.41/85.42 inference(scs_inference,[],[946,264,10])).
% 85.41/85.42 cnf(997,plain,
% 85.41/85.42 (P1(x9971,f4(f4(a1,a1),f4(a1,a1)),f4(a1,x9971))),
% 85.41/85.42 inference(scs_inference,[],[976,151,10])).
% 85.41/85.42 cnf(1016,plain,
% 85.41/85.42 (P1(f4(a1,a1),f4(a1,f4(a1,x10161)),x10161)),
% 85.41/85.42 inference(scs_inference,[],[676,571,9])).
% 85.41/85.42 cnf(1022,plain,
% 85.41/85.42 (E(a1,f4(x10221,f3(x10221)))),
% 85.41/85.42 inference(scs_inference,[],[15,17,21])).
% 85.41/85.42 cnf(1025,plain,
% 85.41/85.42 (P1(x10251,f4(a1,f3(x10251)),f3(a1))),
% 85.41/85.42 inference(scs_inference,[],[15,709,839,17,21,24])).
% 85.41/85.42 cnf(1028,plain,
% 85.41/85.42 (E(f4(x10281,f3(x10281)),a1)),
% 85.41/85.42 inference(scs_inference,[],[15,709,839,17,21,24,2])).
% 85.41/85.42 cnf(1031,plain,
% 85.41/85.42 (E(f4(x10311,f3(x10311)),f3(a1))),
% 85.41/85.42 inference(scs_inference,[],[1028,173,3])).
% 85.41/85.42 cnf(1032,plain,
% 85.41/85.42 (P1(x10321,f3(x10321),f4(x10322,f3(x10322)))),
% 85.41/85.42 inference(scs_inference,[],[15,1028,1022,173,3,11])).
% 85.41/85.42 cnf(1033,plain,
% 85.41/85.42 (P1(f4(x10331,f3(x10331)),f4(a1,x10332),x10332)),
% 85.41/85.42 inference(scs_inference,[],[15,1028,1022,587,173,3,11,9])).
% 85.41/85.42 cnf(1034,plain,
% 85.41/85.42 (P1(f4(a1,x10341),f4(x10342,f3(x10342)),x10341)),
% 85.41/85.42 inference(scs_inference,[],[15,1028,1022,924,587,173,3,11,9,10])).
% 85.41/85.42 cnf(1043,plain,
% 85.41/85.42 (E(f3(a1),f4(x10431,f3(x10431)))),
% 85.41/85.42 inference(scs_inference,[],[15,938,854,622,1028,1022,924,587,173,3,11,9,10,24,23,2])).
% 85.41/85.42 cnf(1045,plain,
% 85.41/85.42 (E(f4(x10451,f3(x10451)),f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[1031,153,3])).
% 85.41/85.42 cnf(1057,plain,
% 85.41/85.42 (E(f4(a1,a1),f4(x10571,f3(x10571)))),
% 85.41/85.42 inference(scs_inference,[],[1045,2])).
% 85.41/85.42 cnf(1062,plain,
% 85.41/85.42 (E(f4(x10621,f3(x10621)),f4(a1,a1))),
% 85.41/85.42 inference(rename_variables,[],[1045])).
% 85.41/85.42 cnf(1066,plain,
% 85.41/85.42 (P1(x10661,f4(a1,f3(x10661)),f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[15,1033,512,1045,1062,1034,946,536,2,11,9,10,24])).
% 85.41/85.42 cnf(1072,plain,
% 85.41/85.42 (P1(x10721,f4(a1,a1),f4(a1,x10721))),
% 85.41/85.42 inference(rename_variables,[],[995])).
% 85.41/85.42 cnf(1075,plain,
% 85.41/85.42 (P1(x10751,f4(x10752,f3(x10752)),f4(a1,x10751))),
% 85.41/85.42 inference(scs_inference,[],[995,1072,991,1057,11,9,10])).
% 85.41/85.42 cnf(1087,plain,
% 85.41/85.42 (P1(f4(x10871,f3(x10871)),x10872,f4(a1,x10872))),
% 85.41/85.42 inference(scs_inference,[],[604,1043,215,11,9])).
% 85.41/85.42 cnf(1088,plain,
% 85.41/85.42 (P1(f4(x10881,a1),f4(x10882,f3(x10882)),f4(a1,x10881))),
% 85.41/85.42 inference(scs_inference,[],[883,604,1043,215,11,9,10])).
% 85.41/85.42 cnf(1109,plain,
% 85.41/85.42 (P1(f4(a1,a1),f4(a1,a1),f4(x11091,f3(x11091)))),
% 85.41/85.42 inference(scs_inference,[],[1045,32,9])).
% 85.41/85.42 cnf(1113,plain,
% 85.41/85.42 (E(a1,f4(f3(x11131),x11131))),
% 85.41/85.42 inference(scs_inference,[],[16,17,21])).
% 85.41/85.42 cnf(1116,plain,
% 85.41/85.42 (P1(f3(f4(a1,x11161)),x11161,f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[16,997,927,17,21,24])).
% 85.41/85.42 cnf(1121,plain,
% 85.41/85.42 (E(f4(f3(x11211),x11211),a1)),
% 85.41/85.42 inference(scs_inference,[],[1113,2])).
% 85.41/85.42 cnf(1122,plain,
% 85.41/85.42 (~P2(f4(f3(x11221),x11221))),
% 85.41/85.42 inference(scs_inference,[],[18,1113,2,12])).
% 85.41/85.42 cnf(1123,plain,
% 85.41/85.42 (P1(f3(x11231),x11231,f4(f3(x11232),x11232))),
% 85.41/85.42 inference(scs_inference,[],[16,18,1113,2,12,11])).
% 85.41/85.42 cnf(1124,plain,
% 85.41/85.42 (P1(f4(f3(x11241),x11241),f4(a1,a1),f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[16,18,995,1113,2,12,11,9])).
% 85.41/85.42 cnf(1133,plain,
% 85.41/85.42 (E(f4(f3(x11331),x11331),f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[1121,25,3])).
% 85.41/85.42 cnf(1136,plain,
% 85.41/85.42 (P1(f4(a1,a1),x11361,x11361)),
% 85.41/85.42 inference(rename_variables,[],[130])).
% 85.41/85.42 cnf(1143,plain,
% 85.41/85.42 (P1(f3(x11431),x11431,a1)),
% 85.41/85.42 inference(rename_variables,[],[16])).
% 85.41/85.42 cnf(1151,plain,
% 85.41/85.42 (E(f4(a1,a1),f4(f3(x11511),x11511))),
% 85.41/85.42 inference(scs_inference,[],[16,1143,1123,1066,1088,1121,508,130,1136,32,25,3,11,9,10,23,24,2])).
% 85.41/85.42 cnf(1155,plain,
% 85.41/85.42 (P1(f4(a1,x11551),f3(a1),f4(x11551,a1))),
% 85.41/85.42 inference(rename_variables,[],[991])).
% 85.41/85.42 cnf(1158,plain,
% 85.41/85.42 (P1(x11581,f4(f3(x11582),x11582),f4(a1,x11581))),
% 85.41/85.42 inference(scs_inference,[],[1151,1133,991,1155,995,171,3,11,9,10])).
% 85.41/85.42 cnf(1159,plain,
% 85.41/85.42 (P1(f3(x11591),f4(a1,x11591),f3(a1))),
% 85.41/85.42 inference(scs_inference,[],[16,1151,1025,1133,1075,991,1155,995,171,3,11,9,10,24])).
% 85.41/85.42 cnf(1163,plain,
% 85.41/85.42 (E(f3(a1),f4(f3(x11631),x11631))),
% 85.41/85.42 inference(scs_inference,[],[16,1151,1025,1133,1075,991,1155,995,171,3,11,9,10,24,2])).
% 85.41/85.42 cnf(1165,plain,
% 85.41/85.42 (P1(f3(x11651),f4(a1,x11651),f4(f3(x11652),x11652))),
% 85.41/85.42 inference(scs_inference,[],[1159,1163,11])).
% 85.41/85.42 cnf(1167,plain,
% 85.41/85.42 (P1(f3(x11671),x11671,a1)),
% 85.41/85.42 inference(rename_variables,[],[16])).
% 85.41/85.42 cnf(1173,plain,
% 85.41/85.42 (P1(x11731,f4(f3(x11732),x11732),f4(a1,x11731))),
% 85.41/85.42 inference(rename_variables,[],[1158])).
% 85.41/85.42 cnf(1175,plain,
% 85.41/85.42 (P1(f3(x11751),f4(a1,x11751),f4(a1,a1))),
% 85.41/85.42 inference(scs_inference,[],[16,1167,1124,975,1158,1173,916,1159,1163,1151,11,9,10,23,24])).
% 85.41/85.42 cnf(1180,plain,
% 85.41/85.42 (P1(f4(a1,a1),f4(a1,a1),f4(f3(x11801),x11801))),
% 85.41/85.42 inference(scs_inference,[],[979,1151,11])).
% 85.41/85.42 cnf(1230,plain,
% 85.41/85.42 (P1(f4(x12301,a1),f4(x12302,f3(x12302)),x12301)),
% 85.41/85.42 inference(scs_inference,[],[1175,867,1057,47,11,9,10])).
% 85.41/85.42 cnf(1234,plain,
% 85.41/85.42 (P1(f4(x12341,f3(x12341)),f4(x12342,a1),x12342)),
% 85.41/85.42 inference(scs_inference,[],[1087,593,11])).
% 85.41/85.42 cnf(1236,plain,
% 85.41/85.42 (P1(x12361,f4(x12362,f3(x12362)),f4(x12361,a1))),
% 85.41/85.42 inference(scs_inference,[],[1087,1034,593,11,9])).
% 85.41/85.42 cnf(1242,plain,
% 85.41/85.42 (E(f4(x12421,f3(a1)),f4(a1,x12421))),
% 85.41/85.42 inference(scs_inference,[],[17,976,21])).
% 85.41/85.42 cnf(1244,plain,
% 85.41/85.42 (P1(x12441,x12442,f4(x12441,x12442))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1252,plain,
% 85.41/85.42 (P1(x12521,x12522,f4(x12521,x12522))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1254,plain,
% 85.41/85.42 (P1(f4(a1,f4(x12541,a1)),f4(a1,a1),x12541)),
% 85.41/85.42 inference(scs_inference,[],[17,1244,1252,1109,1116,1234,1236,1032,1123,976,357,21,9,10,23,24])).
% 85.41/85.42 cnf(1259,plain,
% 85.41/85.42 (E(f4(a1,x12591),f4(x12591,f3(a1)))),
% 85.41/85.42 inference(scs_inference,[],[17,1244,1252,1109,1116,1234,1236,1032,1123,976,357,21,9,10,23,24,2])).
% 85.41/85.42 cnf(1261,plain,
% 85.41/85.42 (E(f4(f4(a1,a1),x12611),f4(a1,x12611))),
% 85.41/85.42 inference(scs_inference,[],[17,659,21])).
% 85.41/85.42 cnf(1263,plain,
% 85.41/85.42 (P1(x12631,x12632,f4(x12631,x12632))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1265,plain,
% 85.41/85.42 (E(f4(f4(a1,x12651),f3(a1)),f4(x12651,a1))),
% 85.41/85.42 inference(scs_inference,[],[17,1242,659,643,21,3])).
% 85.41/85.42 cnf(1268,plain,
% 85.41/85.42 (P1(x12681,x12682,f4(x12681,x12682))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1269,plain,
% 85.41/85.42 (P1(f4(f4(x12691,a1),f3(a1)),f4(a1,a1),x12691)),
% 85.41/85.42 inference(scs_inference,[],[17,1263,1254,1259,1242,659,643,21,3,11,9])).
% 85.41/85.42 cnf(1270,plain,
% 85.41/85.42 (E(f4(a1,x12701),f4(x12701,f3(a1)))),
% 85.41/85.42 inference(rename_variables,[],[1259])).
% 85.41/85.42 cnf(1273,plain,
% 85.41/85.42 (P1(f4(f4(a1,x12731),a1),a1,x12731)),
% 85.41/85.42 inference(scs_inference,[],[17,1263,1268,423,1254,1016,933,1259,1270,1242,659,643,21,3,11,9,10,23])).
% 85.41/85.42 cnf(1274,plain,
% 85.41/85.42 (P1(x12741,x12742,f4(x12741,x12742))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1279,plain,
% 85.41/85.42 (E(f4(a1,x12791),f4(f4(a1,a1),x12791))),
% 85.41/85.42 inference(scs_inference,[],[17,1263,1268,1274,423,1254,1016,933,1259,1270,1242,659,233,643,21,3,11,9,10,23,24,2])).
% 85.41/85.42 cnf(1282,plain,
% 85.41/85.42 (E(f4(f4(a1,x12821),f4(a1,a1)),x12821)),
% 85.41/85.42 inference(scs_inference,[],[17,1265,872,2,21])).
% 85.41/85.42 cnf(1283,plain,
% 85.41/85.42 (P1(x12831,x12832,f4(x12831,x12832))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1285,plain,
% 85.41/85.42 (E(f4(f4(a1,a1),f4(a1,x12851)),x12851)),
% 85.41/85.42 inference(scs_inference,[],[17,1265,1261,872,653,2,21,3])).
% 85.41/85.42 cnf(1288,plain,
% 85.41/85.42 (P1(x12881,x12882,f4(x12881,x12882))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1290,plain,
% 85.41/85.42 (E(f4(a1,x12901),f4(f4(a1,a1),x12901))),
% 85.41/85.42 inference(rename_variables,[],[1279])).
% 85.41/85.42 cnf(1295,plain,
% 85.41/85.42 (P1(x12951,x12952,f4(x12951,x12952))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1298,plain,
% 85.41/85.42 (P1(f4(x12981,a1),f4(f3(x12982),x12982),x12981)),
% 85.41/85.42 inference(scs_inference,[],[17,1283,1288,1295,1180,1269,1165,1279,1290,1265,919,775,540,1261,872,653,2,21,3,11,9,10,23,24])).
% 85.41/85.42 cnf(1304,plain,
% 85.41/85.42 (E(f4(f3(a1),f4(x13041,a1)),x13041)),
% 85.41/85.42 inference(scs_inference,[],[17,1285,183,2,21])).
% 85.41/85.42 cnf(1307,plain,
% 85.41/85.42 (E(f4(f4(a1,a1),f4(a1,x13071)),f4(a1,x13071))),
% 85.41/85.42 inference(scs_inference,[],[17,1285,183,571,2,21,3])).
% 85.41/85.42 cnf(1322,plain,
% 85.41/85.42 (E(f4(x13221,f3(a1)),f4(x13221,a1))),
% 85.41/85.42 inference(scs_inference,[],[17,1307,431,2,21])).
% 85.41/85.42 cnf(1326,plain,
% 85.41/85.42 (E(f4(f3(a1),f4(a1,a1)),f3(a1))),
% 85.41/85.42 inference(scs_inference,[],[17,1307,1304,431,173,2,21,3])).
% 85.41/85.42 cnf(1344,plain,
% 85.41/85.42 (E(f4(f4(x13441,a1),f3(a1)),f4(a1,x13441))),
% 85.41/85.42 inference(scs_inference,[],[17,1322,438,591,2,21,3])).
% 85.41/85.42 cnf(1358,plain,
% 85.41/85.42 (E(f4(f3(a1),x13581),f4(a1,x13581))),
% 85.41/85.42 inference(scs_inference,[],[17,1344,604,2,21])).
% 85.41/85.42 cnf(1375,plain,
% 85.41/85.42 (E(f4(f3(a1),f4(a1,x13751)),x13751)),
% 85.41/85.42 inference(scs_inference,[],[17,1358,859,2,21])).
% 85.41/85.42 cnf(1393,plain,
% 85.41/85.42 (E(f4(f4(a1,a1),x13931),f4(x13931,a1))),
% 85.41/85.42 inference(scs_inference,[],[17,1375,114,2,21])).
% 85.41/85.42 cnf(1397,plain,
% 85.41/85.42 (E(f4(f3(a1),f4(a1,x13971)),f4(x13971,a1))),
% 85.41/85.42 inference(scs_inference,[],[17,1375,114,25,2,21,3])).
% 85.41/85.42 cnf(1410,plain,
% 85.41/85.42 (E(f4(x14101,a1),f4(f4(a1,a1),x14101))),
% 85.41/85.42 inference(scs_inference,[],[1393,2])).
% 85.41/85.42 cnf(1411,plain,
% 85.41/85.42 (E(f4(x14111,f4(a1,a1)),f4(a1,x14111))),
% 85.41/85.42 inference(scs_inference,[],[17,1393,995,2,21])).
% 85.41/85.42 cnf(1415,plain,
% 85.41/85.42 (E(f4(f4(a1,a1),f4(a1,x14151)),f4(x14151,a1))),
% 85.41/85.42 inference(scs_inference,[],[17,1393,995,805,2,21,3])).
% 85.41/85.42 cnf(1428,plain,
% 85.41/85.42 (E(f4(x14281,a1),f4(f4(a1,a1),f4(a1,x14281)))),
% 85.41/85.42 inference(scs_inference,[],[1415,2])).
% 85.41/85.42 cnf(1429,plain,
% 85.41/85.42 (E(f4(f4(a1,x14291),f3(a1)),x14291)),
% 85.41/85.42 inference(scs_inference,[],[17,1415,875,2,21])).
% 85.41/85.42 cnf(1430,plain,
% 85.41/85.42 (P1(x14301,x14302,f4(x14301,x14302))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1433,plain,
% 85.41/85.42 (P1(x14331,x14332,f4(x14331,x14332))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1435,plain,
% 85.41/85.42 (E(f4(x14351,a1),f4(f4(a1,a1),x14351))),
% 85.41/85.42 inference(rename_variables,[],[1410])).
% 85.41/85.42 cnf(1438,plain,
% 85.41/85.42 (P1(x14381,f4(a1,f3(a1)),x14381)),
% 85.41/85.42 inference(scs_inference,[],[17,1430,1433,1298,589,1410,1435,1415,1273,875,638,2,21,11,9,10,24])).
% 85.41/85.42 cnf(1445,plain,
% 85.41/85.42 (E(f4(f4(a1,a1),f4(x14451,a1)),x14451)),
% 85.41/85.42 inference(scs_inference,[],[17,1397,450,2,21])).
% 85.41/85.42 cnf(1446,plain,
% 85.41/85.42 (P1(x14461,x14462,f4(x14461,x14462))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1449,plain,
% 85.41/85.42 (P1(x14491,x14492,f4(x14491,x14492))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1454,plain,
% 85.41/85.42 (P1(x14541,x14542,f4(x14541,f4(x14542,a1)))),
% 85.41/85.42 inference(scs_inference,[],[17,1446,1449,1438,1230,1428,1397,723,883,450,2,21,11,9,10,24])).
% 85.41/85.42 cnf(1461,plain,
% 85.41/85.42 (E(f4(x14611,x14612),f4(x14611,f4(x14612,a1)))),
% 85.41/85.42 inference(scs_inference,[],[17,1454,1326,2,21])).
% 85.41/85.42 cnf(1476,plain,
% 85.41/85.42 (E(x14761,f4(f4(a1,x14761),f4(a1,a1)))),
% 85.41/85.42 inference(scs_inference,[],[1282,2])).
% 85.41/85.42 cnf(1537,plain,
% 85.41/85.42 (E(f4(x15371,f3(a1)),x15371)),
% 85.41/85.42 inference(scs_inference,[],[17,1445,351,2,21])).
% 85.41/85.42 cnf(1553,plain,
% 85.41/85.42 (E(x15531,f4(x15531,f3(a1)))),
% 85.41/85.42 inference(scs_inference,[],[1537,2])).
% 85.41/85.42 cnf(1554,plain,
% 85.41/85.42 (E(f4(x15541,f4(a1,a1)),x15541)),
% 85.41/85.42 inference(scs_inference,[],[17,1537,32,2,21])).
% 85.41/85.42 cnf(1577,plain,
% 85.41/85.42 (E(x15771,f4(x15771,f3(a1)))),
% 85.41/85.42 inference(rename_variables,[],[1553])).
% 85.41/85.42 cnf(1578,plain,
% 85.41/85.42 (P1(f4(x15781,f3(a1)),x15782,f4(x15781,x15782))),
% 85.41/85.42 inference(scs_inference,[],[17,1553,1577,1554,2,11,9])).
% 85.41/85.42 cnf(1587,plain,
% 85.41/85.42 (E(f4(x15871,f4(x15872,a1)),f4(x15871,x15872))),
% 85.41/85.42 inference(scs_inference,[],[1461,2])).
% 85.41/85.42 cnf(1660,plain,
% 85.41/85.42 (P1(f4(f4(a1,x16601),f4(a1,a1)),x16602,f4(x16601,x16602))),
% 85.41/85.42 inference(scs_inference,[],[17,1476,1429,859,2,11,9])).
% 85.41/85.42 cnf(1661,plain,
% 85.41/85.42 (P1(x16611,x16612,f4(x16611,x16612))),
% 85.41/85.42 inference(rename_variables,[],[17])).
% 85.41/85.42 cnf(1662,plain,
% 85.41/85.42 (P1(x16621,f4(f4(a1,x16622),f4(a1,a1)),f4(x16621,x16622))),
% 85.41/85.42 inference(scs_inference,[],[17,1661,1476,1429,859,2,11,9,10])).
% 85.41/85.42 cnf(1666,plain,
% 85.41/85.42 (E(f4(f4(a1,x16661),f4(a1,a1)),f4(x16661,a1))),
% 85.41/85.42 inference(scs_inference,[],[1411,643,2,3])).
% 85.41/85.42 cnf(1682,plain,
% 85.41/85.42 (E(f4(f4(x16821,a1),x16822),f4(x16821,x16822))),
% 85.41/85.42 inference(scs_inference,[],[17,1660,1662,1578,1666,2,11,9,10,21])).
% 85.41/85.42 cnf(1690,plain,
% 85.41/85.42 (E(f4(f4(x16901,a1),f3(x16901)),f3(a1))),
% 85.41/85.42 inference(scs_inference,[],[1122,1682,1587,1031,2,12,3])).
% 85.41/85.42 cnf(1702,plain,
% 85.41/85.42 (E(f4(f4(x17021,a1),f3(x17021)),a1)),
% 85.41/85.42 inference(scs_inference,[],[1690,185,2,3])).
% 85.41/85.42 cnf(1715,plain,
% 85.41/85.42 (P1(f4(x17151,a1),f3(x17151),a1)),
% 85.41/85.42 inference(scs_inference,[],[17,1702,571,2,3,11])).
% 85.41/85.42 cnf(2369,plain,
% 85.41/85.42 (P1(f5(a1),a1,f2(a1))+P1(a1,f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[18,19])).
% 85.41/85.42 cnf(2373,plain,
% 85.41/85.42 (~P1(f4(a1,a1),f5(a1),f2(a1))+P1(a1,f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[18,37,19,22,9])).
% 85.41/85.42 cnf(2379,plain,
% 85.41/85.42 (~P1(f4(a1,a1),f2(a1),f5(a1))+P1(a1,f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[18,438,160,37,536,14,19,22,9,23,24])).
% 85.41/85.42 cnf(2386,plain,
% 85.41/85.42 (~P1(f5(a1),a1,f2(a1))+~P1(a1,f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[18,22])).
% 85.41/85.42 cnf(2390,plain,
% 85.41/85.42 (~P1(f5(a1),f3(a1),f2(a1))+~P1(a1,f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[1715,581,18,32,22,10,24])).
% 85.41/85.42 cnf(2396,plain,
% 85.41/85.42 (P1(f5(a1),a1,f2(a1))+~P1(f5(a1),f3(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[2390,2369])).
% 85.41/85.42 cnf(2411,plain,
% 85.41/85.42 (P1(f4(a1,a1),f5(a1),f2(a1))+~P1(f4(a1,a1),f2(a1),f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[25,2379,9])).
% 85.41/85.42 cnf(3178,plain,
% 85.41/85.42 (P1(f5(a1),a1,f2(a1))+P1(f3(a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[259,536,2369,24])).
% 85.41/85.42 cnf(3179,plain,
% 85.41/85.42 (~P1(a1,f5(a1),f2(a1))+P1(f3(a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[18,3178,22])).
% 85.41/85.42 cnf(3180,plain,
% 85.41/85.42 (~P1(f4(a1,a1),f5(a1),f2(a1))+P1(f3(a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[3179,2373])).
% 85.41/85.42 cnf(3181,plain,
% 85.41/85.42 (~P1(f4(a1,a1),f2(a1),f5(a1))+P1(f3(a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[3180,2411])).
% 85.41/85.42 cnf(3182,plain,
% 85.41/85.42 (~P1(f3(a1),f2(a1),f5(a1))+P1(f3(a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[153,3181,9])).
% 85.41/85.42 cnf(3183,plain,
% 85.41/85.42 (P1(a1,f5(a1),f2(a1))+~P1(f3(a1),f2(a1),f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[185,3182,9])).
% 85.41/85.42 cnf(3184,plain,
% 85.41/85.42 (~P1(f5(a1),a1,f2(a1))+~P1(f3(a1),f2(a1),f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[3183,2386])).
% 85.41/85.42 cnf(3185,plain,
% 85.41/85.42 (~P1(f5(a1),f3(a1),f2(a1))+~P1(f3(a1),f2(a1),f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[3184,2396])).
% 85.41/85.42 cnf(3211,plain,
% 85.41/85.42 (P1(f5(a1),a1,f2(a1))+P1(f4(a1,a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[604,536,2369,23])).
% 85.41/85.42 cnf(3212,plain,
% 85.41/85.42 (P1(f4(a1,a1),f5(a1),f2(a1))+~P1(a1,f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[18,3211,22])).
% 85.41/85.42 cnf(3221,plain,
% 85.41/85.42 (P1(a1,f5(a1),f2(a1))+P1(f2(a1),a1,f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[215,351,2369,23])).
% 85.41/85.42 cnf(3243,plain,
% 85.41/85.42 (~P1(f5(a1),a1,f2(a1))+~P1(f4(a1,a1),f2(a1),f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[2386,2379])).
% 85.41/85.42 cnf(3255,plain,
% 85.41/85.42 (~P1(a1,f5(a1),f2(a1))+~P1(f4(a1,a1),f5(a1),f2(a1))),
% 85.41/85.42 inference(scs_inference,[],[602,924,2386,23])).
% 85.41/85.42 cnf(3328,plain,
% 85.41/85.42 (P1(f2(a1),a1,f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[17,304,3221,23])).
% 85.41/85.42 cnf(3346,plain,
% 85.41/85.42 (P1(a1,f2(a1),f5(a1))),
% 85.41/85.42 inference(scs_inference,[],[25,3328,587,924,13,21,10,24])).
% 85.41/85.42 cnf(3365,plain,
% 85.41/85.42 ($false),
% 85.41/85.42 inference(scs_inference,[],[3346,914,130,173,9,23,3183,3182,3185,3212,3243,3255]),
% 85.41/85.42 ['proof']).
% 85.41/85.42 % SZS output end Proof
% 85.41/85.42 % Total time :84.760000s
%------------------------------------------------------------------------------