%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT001-4 : 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 : n013.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 04:40:07 EDT 2024
% Result : Unsatisfiable 86.37s 86.49s
% Output : CNFRefutation 86.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.09 % Problem : CAT001-4 : TPTP v8.2.0. Released v1.0.0.
% 0.09/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n013.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Tue Jun 18 12:12:54 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.15/0.51 start to proof:theBenchmark
% 86.37/86.48 %-------------------------------------------
% 86.37/86.48 % File :CSE---1.7
% 86.37/86.48 % Problem :theBenchmark
% 86.37/86.48 % Transform :cnf
% 86.37/86.48 % Format :tptp:raw
% 86.37/86.48 % Command :java -jar mcs_scs.jar %d %s
% 86.37/86.48
% 86.37/86.48 % Result :Theorem 85.880000s
% 86.37/86.48 % Output :CNFRefutation 85.880000s
% 86.37/86.48 %-------------------------------------------
% 86.37/86.49 %--------------------------------------------------------------------------
% 86.37/86.49 % File : CAT001-4 : TPTP v8.2.0. Released v1.0.0.
% 86.37/86.49 % Domain : Category Theory
% 86.37/86.49 % Problem : XY monomorphism => Y monomorphism
% 86.37/86.49 % Version : [Sco79] axioms : Reduced > Complete.
% 86.37/86.49 % English : If xy is a monomorphism, then y is a monomorphism.
% 86.37/86.49
% 86.37/86.49 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 86.37/86.49 % Source : [TPTP]
% 86.37/86.49 % Names :
% 86.37/86.49
% 86.37/86.49 % Status : Unsatisfiable
% 86.37/86.49 % Rating : 0.06 v8.2.0, 0.00 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v7.0.0, 0.00 v6.0.0, 0.22 v5.5.0, 0.25 v5.4.0, 0.20 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.20 v2.0.0
% 86.37/86.49 % Syntax : Number of clauses : 16 ( 7 unt; 0 nHn; 13 RR)
% 86.37/86.49 % Number of literals : 28 ( 12 equ; 13 neg)
% 86.37/86.49 % Maximal clause size : 3 ( 1 avg)
% 86.37/86.49 % Maximal term depth : 3 ( 1 avg)
% 86.37/86.49 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 86.37/86.49 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 86.37/86.49 % Number of variables : 22 ( 2 sgn)
% 86.37/86.49 % SPC : CNF_UNS_RFO_SEQ_HRN
% 86.37/86.49
% 86.37/86.49 % Comments : The dependent axioms have been removed. The ANL version has
% 86.37/86.49 % been extended to use all axioms.
% 86.37/86.49 %--------------------------------------------------------------------------
% 86.37/86.49 %----Include Scott's axioms for category theory
% 86.37/86.49 include('Axioms/CAT004-0.ax').
% 86.37/86.49 %--------------------------------------------------------------------------
% 86.37/86.49 cnf(assume_ab_exists,hypothesis,
% 86.37/86.49 there_exists(compose(a,b)) ).
% 86.37/86.49
% 86.37/86.49 cnf(monomorphism,hypothesis,
% 86.37/86.49 ( compose(compose(a,b),X) != Y
% 86.37/86.49 | compose(compose(a,b),Z) != Y
% 86.37/86.49 | X = Z ) ).
% 86.37/86.49
% 86.37/86.49 cnf(assume_bh_exists,hypothesis,
% 86.37/86.49 there_exists(compose(b,h)) ).
% 86.37/86.49
% 86.37/86.49 cnf(bh_equals_bg,hypothesis,
% 86.37/86.49 compose(b,h) = compose(b,g) ).
% 86.37/86.49
% 86.37/86.49 cnf(prove_h_equals_g,negated_conjecture,
% 86.37/86.49 h != g ).
% 86.37/86.49
% 86.37/86.49 %--------------------------------------------------------------------------
% 86.37/86.49 %-------------------------------------------
% 86.37/86.49 % Proof found
% 86.37/86.49 % SZS status Theorem for theBenchmark
% 86.37/86.49 % SZS output start Proof
% 86.37/86.50 %ClaNum:26(EqnAxiom:10)
% 86.37/86.50 %VarNum:46(SingletonVarNum:22)
% 86.37/86.50 %MaxLitNum:3
% 86.37/86.50 %MaxfuncDepth:2
% 86.37/86.50 %SharedTerms:11
% 86.37/86.50 %goalClause: 17
% 86.37/86.50 %singleGoalClaCount:1
% 86.37/86.50 [17]~E(a6,a7)
% 86.37/86.50 [13]E(f2(a4,a6),f2(a4,a7))
% 86.37/86.50 [14]P1(f2(a5,a4))
% 86.37/86.50 [15]P1(f2(a4,a7))
% 86.37/86.50 [11]E(f2(x111,f1(x111)),x111)
% 86.37/86.50 [12]E(f2(f3(x121),x121),x121)
% 86.37/86.50 [16]E(f2(f2(x161,x162),x163),f2(x161,f2(x162,x163)))
% 86.37/86.50 [18]P1(x181)+~P1(f1(x181))
% 86.37/86.50 [19]P1(x191)+~P1(f3(x191))
% 86.37/86.50 [20]~P2(x201,x202)+E(x201,x202)
% 86.37/86.50 [22]P1(x221)+~P2(x221,x222)
% 86.37/86.50 [23]E(f3(x231),f1(x232))+~P1(f2(x232,x231))
% 86.37/86.50 [24]P1(f1(x241))+~P1(f2(x241,x242))
% 86.37/86.50 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 86.37/86.50 [25]~E(f3(x252),f1(x251))+~P1(f1(x251))+P1(f2(x251,x252))
% 86.37/86.50 [26]E(x261,x262)+~E(f2(f2(a5,a4),x261),x263)+~E(f2(f2(a5,a4),x262),x263)
% 86.37/86.50 %EqnAxiom
% 86.37/86.50 [1]E(x11,x11)
% 86.37/86.50 [2]E(x22,x21)+~E(x21,x22)
% 86.37/86.50 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 86.37/86.50 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 86.37/86.50 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 86.37/86.50 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 86.37/86.50 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 86.37/86.50 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 86.37/86.50 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93)
% 86.37/86.50 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101)
% 86.37/86.50
% 86.37/86.50 %-------------------------------------------
% 86.37/86.51 cnf(27,plain,
% 86.37/86.51 (~P1(x271)+P2(x271,x271)),
% 86.37/86.52 inference(equality_inference,[],[21])).
% 86.37/86.52 cnf(28,plain,
% 86.37/86.52 (~P2(a6,a7)),
% 86.37/86.52 inference(scs_inference,[],[17,20])).
% 86.37/86.52 cnf(30,plain,
% 86.37/86.52 (E(f2(a4,a7),f2(a4,a6))),
% 86.37/86.52 inference(scs_inference,[],[17,13,20,2])).
% 86.37/86.52 cnf(31,plain,
% 86.37/86.52 (E(f3(a7),f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[17,13,15,20,2,23])).
% 86.37/86.52 cnf(33,plain,
% 86.37/86.52 (P2(f2(a4,a7),f2(a4,a6))),
% 86.37/86.52 inference(scs_inference,[],[17,13,15,20,2,23,21])).
% 86.37/86.52 cnf(35,plain,
% 86.37/86.52 (E(f2(f2(a4,a6),f1(f2(a4,a6))),f2(a4,a7))),
% 86.37/86.52 inference(scs_inference,[],[17,13,11,15,20,2,23,21,3])).
% 86.37/86.52 cnf(37,plain,
% 86.37/86.52 (P1(f2(a4,a6))),
% 86.37/86.52 inference(scs_inference,[],[17,13,11,15,20,2,23,21,3,8])).
% 86.37/86.52 cnf(39,plain,
% 86.37/86.52 (P2(f2(a4,a7),f2(a4,a7))),
% 86.37/86.52 inference(scs_inference,[],[17,13,11,15,20,2,23,21,3,8,9,10])).
% 86.37/86.52 cnf(40,plain,
% 86.37/86.52 (E(f2(a4,a7),f2(f2(a4,a6),f1(f2(a4,a6))))),
% 86.37/86.52 inference(scs_inference,[],[35,2])).
% 86.37/86.52 cnf(41,plain,
% 86.37/86.52 (E(f3(a6),f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[35,37,2,23])).
% 86.37/86.52 cnf(43,plain,
% 86.37/86.52 (P2(f2(a4,a6),f2(a4,a7))),
% 86.37/86.52 inference(scs_inference,[],[35,37,13,2,23,21])).
% 86.37/86.52 cnf(45,plain,
% 86.37/86.52 (E(f2(f3(f3(a7)),f3(a7)),f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[35,31,37,12,13,2,23,21,3])).
% 86.37/86.52 cnf(47,plain,
% 86.37/86.52 (P1(f2(f2(a4,a6),f1(f2(a4,a6))))),
% 86.37/86.52 inference(scs_inference,[],[35,31,37,12,13,15,2,23,21,3,8])).
% 86.37/86.52 cnf(48,plain,
% 86.37/86.52 (E(f3(a4),f1(a5))),
% 86.37/86.52 inference(scs_inference,[],[14,23])).
% 86.37/86.52 cnf(52,plain,
% 86.37/86.52 (P2(f2(a4,a6),f2(f2(a4,a6),f1(f2(a4,a6))))),
% 86.37/86.52 inference(scs_inference,[],[40,45,33,43,14,23,2,9,10])).
% 86.37/86.52 cnf(55,plain,
% 86.37/86.52 (E(f2(f3(a6),f1(f3(a6))),f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[40,45,35,33,43,47,41,14,11,23,2,9,10,21,3])).
% 86.37/86.52 cnf(57,plain,
% 86.37/86.52 (~P1(f2(f3(f3(a7)),f3(a7)))+P1(f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[40,45,35,33,43,47,41,14,11,23,2,9,10,21,3,8])).
% 86.37/86.52 cnf(58,plain,
% 86.37/86.52 (~P2(f2(f3(f3(a7)),f3(a7)),x581)+P1(f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[40,45,35,33,43,47,41,14,11,23,2,9,10,21,3,8,22])).
% 86.37/86.52 cnf(61,plain,
% 86.37/86.52 (E(f1(a4),f2(f3(a6),f1(f3(a6))))),
% 86.37/86.52 inference(scs_inference,[],[55,2])).
% 86.37/86.52 cnf(63,plain,
% 86.37/86.52 (E(f2(f3(f3(a4)),f3(a4)),f1(a5))),
% 86.37/86.52 inference(scs_inference,[],[55,52,48,12,13,2,9,3])).
% 86.37/86.52 cnf(65,plain,
% 86.37/86.52 (P2(f2(a5,a4),x651)+~E(f2(a5,a4),x651)),
% 86.37/86.52 inference(scs_inference,[],[55,52,48,12,14,13,2,9,3,21])).
% 86.37/86.52 cnf(68,plain,
% 86.37/86.52 (~E(f2(a5,a4),f2(f3(a6),f1(f3(a6))))+~P1(f2(f3(a6),f1(f3(a6))))+P1(f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[55,52,48,12,14,13,2,9,3,21,10,8])).
% 86.37/86.52 cnf(69,plain,
% 86.37/86.52 (P2(f2(a5,a4),f2(a5,a4))),
% 86.37/86.52 inference(equality_inference,[],[65])).
% 86.37/86.52 cnf(70,plain,
% 86.37/86.52 (E(f1(a5),f2(f3(f3(a4)),f3(a4)))),
% 86.37/86.52 inference(scs_inference,[],[63,2])).
% 86.37/86.52 cnf(71,plain,
% 86.37/86.52 (~E(a6,f2(a7,f1(a7)))),
% 86.37/86.52 inference(scs_inference,[],[17,63,11,2,3])).
% 86.37/86.52 cnf(73,plain,
% 86.37/86.52 (~P2(a6,f2(a7,f1(a7)))),
% 86.37/86.52 inference(scs_inference,[],[17,63,11,2,3,20])).
% 86.37/86.52 cnf(75,plain,
% 86.37/86.52 (P2(x751,f2(a5,a4))+~E(f2(a5,a4),x751)),
% 86.37/86.52 inference(scs_inference,[],[17,63,69,11,2,3,20,9])).
% 86.37/86.52 cnf(79,plain,
% 86.37/86.52 (E(x791,f2(x791,f1(x791)))),
% 86.37/86.52 inference(scs_inference,[],[11,2])).
% 86.37/86.52 cnf(84,plain,
% 86.37/86.52 (E(f2(f3(f3(a6)),f3(a6)),f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[69,14,11,41,12,2,21,9,8,3])).
% 86.37/86.52 cnf(86,plain,
% 86.37/86.52 (E(f1(a4),f2(f3(f3(a6)),f3(a6)))),
% 86.37/86.52 inference(scs_inference,[],[84,2])).
% 86.37/86.52 cnf(87,plain,
% 86.37/86.52 (E(f2(f3(a7),f1(f3(a7))),f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[84,11,31,2,3])).
% 86.37/86.52 cnf(89,plain,
% 86.37/86.52 (~P1(f2(f3(f3(a6)),f3(a6)))+P1(f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[84,11,31,2,3,8])).
% 86.37/86.52 cnf(90,plain,
% 86.37/86.52 (~P2(f2(f3(f3(a6)),f3(a6)),x901)+P1(f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[84,11,31,2,3,8,22])).
% 86.37/86.52 cnf(92,plain,
% 86.37/86.52 (~E(f2(a4,a6),f2(f3(f3(a6)),f3(a6)))+P1(f1(a4))),
% 86.37/86.52 inference(scs_inference,[],[84,43,11,31,2,3,8,22,25,9])).
% 86.37/86.52 cnf(93,plain,
% 86.37/86.52 (E(f1(a4),f2(f3(a7),f1(f3(a7))))),
% 86.37/86.52 inference(scs_inference,[],[87,2])).
% 86.37/86.52 cnf(94,plain,
% 86.37/86.52 (E(f2(f3(a4),f1(f3(a4))),f1(a5))),
% 86.37/86.52 inference(scs_inference,[],[87,11,48,2,3])).
% 86.37/86.52 cnf(108,plain,
% 86.37/86.52 (E(f1(a5),f2(f3(a4),f1(f3(a4))))),
% 86.37/86.52 inference(scs_inference,[],[94,2])).
% 86.37/86.52 cnf(109,plain,
% 86.37/86.52 (P2(f2(a4,a7),f2(f2(a4,a7),f1(f2(a4,a7))))),
% 86.37/86.52 inference(scs_inference,[],[79,94,15,2,21])).
% 86.37/86.52 cnf(110,plain,
% 86.37/86.52 (E(x1101,f2(x1101,f1(x1101)))),
% 86.37/86.52 inference(rename_variables,[],[79])).
% 86.37/86.52 cnf(113,plain,
% 86.37/86.52 (E(x1131,f2(x1131,f1(x1131)))),
% 86.37/86.52 inference(rename_variables,[],[79])).
% 86.37/86.52 cnf(118,plain,
% 86.37/86.52 (~P2(a6,f2(f3(a7),a7))),
% 86.37/86.52 inference(scs_inference,[],[17,79,110,113,94,33,43,15,12,2,21,10,9,3,20])).
% 86.37/86.52 cnf(120,plain,
% 86.37/86.52 (~P1(f1(a5))+P1(f2(f3(f3(a4)),f3(a4)))),
% 86.37/86.52 inference(scs_inference,[],[17,79,110,113,70,94,33,43,15,12,2,21,10,9,3,20,8])).
% 86.37/86.52 cnf(122,plain,
% 86.37/86.52 (~P2(f1(a5),x1221)+P1(f2(f3(f3(a4)),f3(a4)))),
% 86.37/86.52 inference(scs_inference,[],[17,79,110,113,70,94,33,43,14,15,12,2,21,10,9,3,20,8,24,22])).
% 86.37/86.52 cnf(125,plain,
% 86.37/86.52 (E(f2(x1251,f2(x1252,x1253)),f2(f2(x1251,x1252),x1253))),
% 86.37/86.52 inference(scs_inference,[],[16,2])).
% 86.37/86.52 cnf(131,plain,
% 86.37/86.52 (P1(f2(f3(a6),f1(f3(a6))))+~P1(f2(f3(f3(a7)),f3(a7)))),
% 86.37/86.52 inference(scs_inference,[],[79,61,39,16,2,9,8,58,90,57])).
% 86.37/86.52 cnf(137,plain,
% 86.37/86.52 (~P2(f2(a4,a6),f2(f3(f3(a6)),f3(a6)))+P1(f2(f3(a6),f1(f3(a6))))),
% 86.37/86.52 inference(scs_inference,[],[79,61,37,39,16,2,9,8,58,90,57,92,24,89,22,20])).
% 86.37/86.52 cnf(143,plain,
% 86.37/86.52 (E(f1(a4),f3(a6))),
% 86.37/86.52 inference(scs_inference,[],[41,2])).
% 86.37/86.52 cnf(144,plain,
% 86.37/86.52 (E(f2(f3(a7),f1(f3(a7))),f3(a6))),
% 86.37/86.52 inference(scs_inference,[],[87,41,2,3])).
% 86.37/86.52 cnf(145,plain,
% 86.37/86.52 (~P1(f2(x1451,f2(x1452,x1453)))+P1(f2(f2(x1451,x1452),x1453))),
% 86.37/86.52 inference(scs_inference,[],[125,87,41,2,3,8])).
% 86.37/86.52 cnf(146,plain,
% 86.37/86.52 (~P1(f2(x1461,f2(x1462,x1463)))+E(f3(x1463),f1(f2(x1461,x1462)))),
% 86.37/86.52 inference(scs_inference,[],[125,87,41,2,3,8,23])).
% 86.37/86.52 cnf(149,plain,
% 86.37/86.52 (E(f3(a7),f3(a6))),
% 86.37/86.52 inference(scs_inference,[],[79,144,2,3])).
% 86.37/86.52 cnf(155,plain,
% 86.37/86.52 (P1(f2(f3(f3(a6)),f3(a6)))+~P1(f2(f3(f3(a7)),f3(a7)))),
% 86.37/86.52 inference(scs_inference,[],[79,86,144,37,2,3,8,58,24,92,57])).
% 86.37/86.52 cnf(156,plain,
% 86.37/86.52 (P1(f2(f3(f3(a6)),f3(a6)))+~P1(f2(f3(f3(a6)),f3(a6)))),
% 86.37/86.52 inference(scs_inference,[],[79,86,144,37,2,3,8,58,24,92,57,89])).
% 86.46/86.52 cnf(157,plain,
% 86.46/86.52 (~P2(f1(a4),x1571)+P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[79,86,144,37,2,3,8,58,24,92,57,89,22])).
% 86.46/86.52 cnf(163,plain,
% 86.46/86.52 (E(f3(a6),f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[149,2])).
% 86.46/86.52 cnf(164,plain,
% 86.46/86.52 (E(f1(a4),f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[143,149,2,3])).
% 86.46/86.52 cnf(169,plain,
% 86.46/86.52 (P1(f2(f3(a7),f1(f3(a7))))+~P1(f2(f3(f3(a7)),f3(a7)))),
% 86.46/86.52 inference(scs_inference,[],[93,143,149,37,2,3,8,90,58,24,57])).
% 86.46/86.52 cnf(176,plain,
% 86.46/86.52 (~E(f2(a4,a7),f2(f3(f3(a6)),f3(a6)))+P1(f2(f3(a7),f1(f3(a7))))),
% 86.46/86.52 inference(scs_inference,[],[93,143,149,43,37,2,3,8,90,58,24,57,92,89,20,22,68,25,10])).
% 86.46/86.52 cnf(178,plain,
% 86.46/86.52 (E(f1(a5),f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[48,2])).
% 86.46/86.52 cnf(181,plain,
% 86.46/86.52 (~P2(f1(a5),x1811)+P1(f2(f3(a4),f1(f3(a4))))),
% 86.46/86.52 inference(scs_inference,[],[108,14,48,2,8,24,22])).
% 86.46/86.52 cnf(187,plain,
% 86.46/86.52 (E(x1871,f2(f3(x1871),x1871))),
% 86.46/86.52 inference(scs_inference,[],[12,2])).
% 86.46/86.52 cnf(188,plain,
% 86.46/86.52 (P1(f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 86.46/86.52 inference(scs_inference,[],[14,12,2,8])).
% 86.46/86.52 cnf(198,plain,
% 86.46/86.52 (~P1(f1(a4))+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[164,8])).
% 86.46/86.52 cnf(204,plain,
% 86.46/86.52 (~P2(f2(a4,a6),f2(f3(f3(a6)),f3(a6)))+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[164,15,8,90,58,24,57,92,20])).
% 86.46/86.52 cnf(210,plain,
% 86.46/86.52 (~E(f2(a5,a4),f2(f3(f3(a6)),f3(a6)))+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[164,43,69,15,8,90,58,24,57,92,20,89,22,68,25,10,9])).
% 86.46/86.52 cnf(211,plain,
% 86.46/86.52 (~E(f2(a4,a6),f1(a4))+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[164,86,43,69,15,8,90,58,24,57,92,20,89,22,68,25,10,9,3])).
% 86.46/86.52 cnf(212,plain,
% 86.46/86.52 (~P1(f1(a5))+P1(f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[178,8])).
% 86.46/86.52 cnf(214,plain,
% 86.46/86.52 (~P2(f1(a5),x2141)+P1(f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[178,14,8,24,22])).
% 86.46/86.52 cnf(220,plain,
% 86.46/86.52 (~P1(f2(f3(a4),f1(f3(a4))))+P1(f1(a5))),
% 86.46/86.52 inference(scs_inference,[],[94,8])).
% 86.46/86.52 cnf(226,plain,
% 86.46/86.52 (~P2(f3(a6),x2261)+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[163,8,22])).
% 86.46/86.52 cnf(228,plain,
% 86.46/86.52 (~E(f2(a4,a7),f3(a6))+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[163,33,8,22,9])).
% 86.46/86.52 cnf(229,plain,
% 86.46/86.52 (~E(f2(a4,a7),f1(a4))+P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[163,143,33,8,22,9,3])).
% 86.46/86.52 cnf(234,plain,
% 86.46/86.52 (P1(f3(a6))+~P1(f2(f3(f3(a7)),f3(a7)))),
% 86.46/86.52 inference(scs_inference,[],[143,37,8,90,58,24,57])).
% 86.46/86.52 cnf(236,plain,
% 86.46/86.52 (P1(f3(a6))+~P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[143,37,8,90,58,24,57,92,89])).
% 86.46/86.52 cnf(239,plain,
% 86.46/86.52 (~E(f2(a4,a6),f1(a4))+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[143,86,37,8,90,58,24,57,92,89,22,68,25,3])).
% 86.46/86.52 cnf(241,plain,
% 86.46/86.52 (~P1(f2(f3(a7),f1(f3(a7))))+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[144,8])).
% 86.46/86.52 cnf(242,plain,
% 86.46/86.52 (~P2(f2(f3(a7),f1(f3(a7))),x2421)+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[144,8,22])).
% 86.46/86.52 cnf(244,plain,
% 86.46/86.52 (~E(f2(a4,a7),f2(f3(a7),f1(f3(a7))))+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[144,33,8,22,25,9])).
% 86.46/86.52 cnf(245,plain,
% 86.46/86.52 (~P1(f3(a7))+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[149,8])).
% 86.46/86.52 cnf(247,plain,
% 86.46/86.52 (P1(f3(a6))+~E(f2(a4,a7),f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[149,8,204,229])).
% 86.46/86.52 cnf(249,plain,
% 86.46/86.52 (P1(f3(a6))+~E(f2(a4,a7),f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[149,8,204,229,210,228])).
% 86.46/86.52 cnf(250,plain,
% 86.46/86.52 (~P2(f2(a4,a7),f1(a4))+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[149,8,204,229,210,228,20])).
% 86.46/86.52 cnf(252,plain,
% 86.46/86.52 (~P2(f3(a7),x2521)+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[149,8,204,229,210,228,20,22])).
% 86.46/86.52 cnf(255,plain,
% 86.46/86.52 (~E(f2(a4,a7),f3(a7))+P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[149,109,8,204,229,210,228,20,22,10,3])).
% 86.46/86.52 cnf(261,plain,
% 86.46/86.52 (~P2(f2(f3(a7),f1(f3(a7))),x2611)+P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[87,8,176,20,22])).
% 86.46/86.52 cnf(266,plain,
% 86.46/86.52 (E(f3(a7),f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[164,84,3,2])).
% 86.46/86.52 cnf(267,plain,
% 86.46/86.52 (~P1(f2(f3(f3(a4)),f3(a4)))+P1(f1(a5))),
% 86.46/86.52 inference(scs_inference,[],[164,84,63,3,2,8])).
% 86.46/86.52 cnf(272,plain,
% 86.46/86.52 (E(f3(a6),f2(f3(f3(a7)),f3(a7)))),
% 86.46/86.52 inference(scs_inference,[],[143,45,3,2])).
% 86.46/86.52 cnf(273,plain,
% 86.46/86.52 (~P1(f2(f3(a6),f1(f3(a6))))+P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[143,45,55,3,2,8])).
% 86.46/86.52 cnf(275,plain,
% 86.46/86.52 (~P2(f2(f3(a6),f1(f3(a6))),x2751)+P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[143,45,55,3,2,8,137,22])).
% 86.46/86.52 cnf(278,plain,
% 86.46/86.52 (~P1(f3(a7))+P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[266,8])).
% 86.46/86.52 cnf(286,plain,
% 86.46/86.52 (~P2(f3(a7),x2861)+P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[266,8,211,226,228,210,229,20,22])).
% 86.46/86.52 cnf(300,plain,
% 86.46/86.52 (P1(f2(f3(f3(a7)),f3(a7)))+~P2(f3(a7),x3001)),
% 86.46/86.52 inference(scs_inference,[],[272,8,250,239,247,255,241,242,244,249,252])).
% 86.46/86.52 cnf(310,plain,
% 86.46/86.52 (~P1(f3(a7))+P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[31,8])).
% 86.46/86.52 cnf(317,plain,
% 86.46/86.52 (~P2(f3(a7),x3171)+P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[31,8,211,226,210,228,20,22])).
% 86.46/86.52 cnf(334,plain,
% 86.46/86.52 (P2(f1(a5),f1(a5))),
% 86.46/86.52 inference(scs_inference,[],[14,27,24])).
% 86.46/86.52 cnf(335,plain,
% 86.46/86.52 (P1(f2(f3(f3(a4)),f3(a4)))),
% 86.46/86.52 inference(scs_inference,[],[334,122])).
% 86.46/86.52 cnf(336,plain,
% 86.46/86.52 (P1(f2(f3(a4),f1(f3(a4))))),
% 86.46/86.52 inference(scs_inference,[],[334,181])).
% 86.46/86.52 cnf(337,plain,
% 86.46/86.52 (P1(f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[334,214])).
% 86.46/86.52 cnf(342,plain,
% 86.46/86.52 (P1(f1(a5))),
% 86.46/86.52 inference(scs_inference,[],[336,220])).
% 86.46/86.52 cnf(343,plain,
% 86.46/86.52 (P1(f1(a5))),
% 86.46/86.52 inference(scs_inference,[],[335,267])).
% 86.46/86.52 cnf(345,plain,
% 86.46/86.52 (P1(a4)),
% 86.46/86.52 inference(scs_inference,[],[337,19])).
% 86.46/86.52 cnf(347,plain,
% 86.46/86.52 (P2(f3(a4),f2(f3(a4),f1(f3(a4))))),
% 86.46/86.52 inference(scs_inference,[],[79,337,19,21])).
% 86.46/86.52 cnf(350,plain,
% 86.46/86.52 (P1(f2(f3(f3(a4)),f3(a4)))),
% 86.46/86.52 inference(scs_inference,[],[342,120])).
% 86.46/86.52 cnf(352,plain,
% 86.46/86.52 (P1(f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[342,212])).
% 86.46/86.52 cnf(354,plain,
% 86.46/86.52 (P1(a5)),
% 86.46/86.52 inference(scs_inference,[],[342,18])).
% 86.46/86.52 cnf(356,plain,
% 86.46/86.52 (P2(a4,f2(a4,f1(a4)))),
% 86.46/86.52 inference(scs_inference,[],[79,342,345,18,21])).
% 86.46/86.52 cnf(361,plain,
% 86.46/86.52 (P2(a5,f2(a5,f1(a5)))),
% 86.46/86.52 inference(scs_inference,[],[79,354,21])).
% 86.46/86.52 cnf(367,plain,
% 86.46/86.52 (P2(f2(f3(a4),f1(f3(a4))),f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[11,336,21])).
% 86.46/86.52 cnf(368,plain,
% 86.46/86.52 (E(f2(x3681,f1(x3681)),x3681)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(370,plain,
% 86.46/86.52 (P2(f3(a4),f3(a4))),
% 86.46/86.52 inference(scs_inference,[],[11,368,347,336,21,10])).
% 86.46/86.52 cnf(371,plain,
% 86.46/86.52 (E(f2(x3711,f1(x3711)),x3711)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(374,plain,
% 86.46/86.52 (E(f3(a7),f2(f1(a4),f1(f1(a4))))),
% 86.46/86.52 inference(scs_inference,[],[11,368,371,164,347,336,21,10,3,2])).
% 86.46/86.52 cnf(384,plain,
% 86.46/86.52 (P1(f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[15,198,24])).
% 86.46/86.52 cnf(385,plain,
% 86.46/86.52 (P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[384,245])).
% 86.46/86.52 cnf(386,plain,
% 86.46/86.52 (P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[384,278])).
% 86.46/86.52 cnf(387,plain,
% 86.46/86.52 (P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[384,310])).
% 86.46/86.52 cnf(388,plain,
% 86.46/86.52 (P1(a7)),
% 86.46/86.52 inference(scs_inference,[],[384,19])).
% 86.46/86.52 cnf(390,plain,
% 86.46/86.52 (P2(f3(a7),f2(f3(a7),f1(f3(a7))))),
% 86.46/86.52 inference(scs_inference,[],[79,384,19,21])).
% 86.46/86.52 cnf(391,plain,
% 86.46/86.52 (E(x3911,f2(x3911,f1(x3911)))),
% 86.46/86.52 inference(rename_variables,[],[79])).
% 86.46/86.52 cnf(394,plain,
% 86.46/86.52 (E(f2(x3941,f1(x3941)),x3941)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(397,plain,
% 86.46/86.52 (P2(f2(a4,f1(a4)),a4)),
% 86.46/86.52 inference(scs_inference,[],[11,394,79,391,163,356,384,19,21,10,3,9])).
% 86.46/86.52 cnf(399,plain,
% 86.46/86.52 (P1(f2(f1(a4),f1(f1(a4))))),
% 86.46/86.52 inference(scs_inference,[],[11,394,79,391,163,374,356,384,19,21,10,3,9,8])).
% 86.46/86.52 cnf(400,plain,
% 86.46/86.52 (P1(f2(f3(f3(a7)),f3(a7)))),
% 86.46/86.52 inference(scs_inference,[],[11,394,79,391,163,374,356,384,19,21,10,3,9,8,300])).
% 86.46/86.52 cnf(403,plain,
% 86.46/86.52 (P1(f2(f3(a6),f1(f3(a6))))),
% 86.46/86.52 inference(scs_inference,[],[11,394,79,391,163,374,356,384,19,21,10,3,9,8,300,2,131])).
% 86.46/86.52 cnf(404,plain,
% 86.46/86.52 (P1(f2(f3(a7),f1(f3(a7))))),
% 86.46/86.52 inference(scs_inference,[],[11,394,79,391,163,374,356,384,19,21,10,3,9,8,300,2,131,169])).
% 86.46/86.52 cnf(406,plain,
% 86.46/86.52 (P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[386,89])).
% 86.46/86.52 cnf(408,plain,
% 86.46/86.52 (P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[400,155])).
% 86.46/86.52 cnf(409,plain,
% 86.46/86.52 (P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[386,156])).
% 86.46/86.52 cnf(411,plain,
% 86.46/86.52 (P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[400,234])).
% 86.46/86.52 cnf(412,plain,
% 86.46/86.52 (P1(f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[386,236])).
% 86.46/86.52 cnf(416,plain,
% 86.46/86.52 (P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[403,273])).
% 86.46/86.52 cnf(417,plain,
% 86.46/86.52 (P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[390,286])).
% 86.46/86.52 cnf(418,plain,
% 86.46/86.52 (P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[390,317])).
% 86.46/86.52 cnf(423,plain,
% 86.46/86.52 (P1(a6)),
% 86.46/86.52 inference(scs_inference,[],[385,19])).
% 86.46/86.52 cnf(426,plain,
% 86.46/86.52 (E(f2(x4261,f1(x4261)),x4261)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(428,plain,
% 86.46/86.52 (P2(a5,a5)),
% 86.46/86.52 inference(scs_inference,[],[11,426,361,399,385,19,21,10])).
% 86.46/86.52 cnf(429,plain,
% 86.46/86.52 (E(f2(x4291,f1(x4291)),x4291)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(431,plain,
% 86.46/86.52 (E(f2(x4311,f1(x4311)),x4311)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(432,plain,
% 86.46/86.52 (P2(f1(a4),f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[11,426,429,431,143,361,399,385,19,21,10,3,9])).
% 86.46/86.52 cnf(435,plain,
% 86.46/86.52 (P1(f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.52 inference(scs_inference,[],[432,157])).
% 86.46/86.52 cnf(437,plain,
% 86.46/86.52 (P2(f2(f3(a7),f1(f3(a7))),f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[11,404,21])).
% 86.46/86.52 cnf(438,plain,
% 86.46/86.52 (E(f2(x4381,f1(x4381)),x4381)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(440,plain,
% 86.46/86.52 (P2(f3(a7),f3(a7))),
% 86.46/86.52 inference(scs_inference,[],[11,438,390,404,21,10])).
% 86.46/86.52 cnf(441,plain,
% 86.46/86.52 (E(f2(x4411,f1(x4411)),x4411)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(447,plain,
% 86.46/86.52 (P1(f2(f1(a5),f1(f1(a5))))),
% 86.46/86.52 inference(scs_inference,[],[11,438,441,79,178,390,352,404,428,21,10,3,9,2,8])).
% 86.46/86.52 cnf(449,plain,
% 86.46/86.52 (P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[437,261])).
% 86.46/86.52 cnf(450,plain,
% 86.46/86.52 (P2(f2(f3(a6),f1(f3(a6))),f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[11,403,21])).
% 86.46/86.52 cnf(451,plain,
% 86.46/86.52 (E(f2(x4511,f1(x4511)),x4511)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(456,plain,
% 86.46/86.52 (E(f2(x4561,f1(x4561)),x4561)),
% 86.46/86.52 inference(rename_variables,[],[11])).
% 86.46/86.52 cnf(457,plain,
% 86.46/86.52 (P2(f3(a6),f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[11,451,456,79,30,403,432,21,10,3,9])).
% 86.46/86.52 cnf(461,plain,
% 86.46/86.52 (P1(f1(a4))),
% 86.46/86.52 inference(scs_inference,[],[450,275])).
% 86.46/86.52 cnf(467,plain,
% 86.46/86.52 (P2(a7,f2(a7,f1(a7)))),
% 86.46/86.52 inference(scs_inference,[],[79,388,21])).
% 86.46/86.52 cnf(472,plain,
% 86.46/86.52 (~E(a7,a6)),
% 86.46/86.52 inference(scs_inference,[],[11,73,79,388,21,10,9])).
% 86.46/86.52 cnf(473,plain,
% 86.46/86.52 (~P2(a7,a6)),
% 86.46/86.52 inference(scs_inference,[],[11,73,79,388,21,10,9,20])).
% 86.46/86.52 cnf(478,plain,
% 86.46/86.52 (E(f1(x4781),f1(f2(f3(x4781),x4781)))),
% 86.46/86.52 inference(scs_inference,[],[12,4,2])).
% 86.46/86.52 cnf(480,plain,
% 86.46/86.52 (P2(f2(f3(f3(a6)),f3(a6)),f3(a6))),
% 86.46/86.52 inference(scs_inference,[],[12,478,386,2,21])).
% 86.46/86.52 cnf(481,plain,
% 86.46/86.52 (E(f2(f3(x4811),x4811),x4811)),
% 86.46/86.52 inference(rename_variables,[],[12])).
% 86.46/86.52 cnf(483,plain,
% 86.46/86.52 (E(f2(f3(f1(a4)),f1(a4)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[12,481,164,478,386,2,21,3])).
% 86.46/86.53 cnf(485,plain,
% 86.46/86.53 (P1(f1(f2(f3(a5),a5)))),
% 86.46/86.53 inference(scs_inference,[],[12,481,164,343,478,386,2,21,3,8])).
% 86.46/86.53 cnf(487,plain,
% 86.46/86.53 (P1(f2(f3(a5),a5))),
% 86.46/86.53 inference(scs_inference,[],[12,481,164,343,478,386,2,21,3,8,18])).
% 86.46/86.53 cnf(489,plain,
% 86.46/86.53 (E(f3(a5),f1(f3(a5)))),
% 86.46/86.53 inference(scs_inference,[],[12,481,164,343,478,386,2,21,3,8,18,23])).
% 86.46/86.53 cnf(494,plain,
% 86.46/86.53 (E(f3(a7),f2(f3(f1(a4)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[483,2])).
% 86.46/86.53 cnf(495,plain,
% 86.46/86.53 (P2(f2(f3(f3(a7)),f3(a7)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[12,483,400,2,21])).
% 86.46/86.53 cnf(496,plain,
% 86.46/86.53 (E(f2(f3(x4961),x4961),x4961)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(498,plain,
% 86.46/86.53 (E(f2(f3(f1(a4)),f1(a4)),f3(a6))),
% 86.46/86.53 inference(scs_inference,[],[12,496,143,483,400,2,21,3])).
% 86.46/86.53 cnf(500,plain,
% 86.46/86.53 (P1(f2(f3(f1(a4)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[12,496,143,483,400,384,2,21,3,8])).
% 86.46/86.53 cnf(505,plain,
% 86.46/86.53 (P2(f2(f3(f1(a4)),f1(a4)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[12,498,500,2,21])).
% 86.46/86.53 cnf(506,plain,
% 86.46/86.53 (E(f2(f3(x5061),x5061),x5061)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(508,plain,
% 86.46/86.53 (E(f2(f3(f1(a5)),f1(a5)),f3(a4))),
% 86.46/86.53 inference(scs_inference,[],[12,506,178,498,500,2,21,3])).
% 86.46/86.53 cnf(516,plain,
% 86.46/86.53 (E(f2(f3(x5161),x5161),x5161)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(520,plain,
% 86.46/86.53 (E(f2(f3(f2(a4,a7)),f2(a4,a7)),f2(a4,a6))),
% 86.46/86.53 inference(scs_inference,[],[12,516,79,30,508,487,2,21,10,3])).
% 86.46/86.53 cnf(522,plain,
% 86.46/86.53 (P1(f2(f3(f1(a5)),f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[12,516,79,30,508,352,487,2,21,10,3,8])).
% 86.46/86.53 cnf(525,plain,
% 86.46/86.53 (E(f2(f3(x5251),x5251),x5251)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(527,plain,
% 86.46/86.53 (E(f2(f3(f2(a4,a6)),f2(a4,a6)),f2(a4,a7))),
% 86.46/86.53 inference(scs_inference,[],[12,525,520,13,522,2,21,3])).
% 86.46/86.53 cnf(529,plain,
% 86.46/86.53 (P1(f2(f3(f2(a4,a7)),f2(a4,a7)))),
% 86.46/86.53 inference(scs_inference,[],[12,525,520,37,13,522,2,21,3,8])).
% 86.46/86.53 cnf(532,plain,
% 86.46/86.53 (E(f2(f3(x5321),x5321),x5321)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(536,plain,
% 86.46/86.53 (P1(f2(f3(f2(a4,a6)),f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[12,532,527,15,529,489,2,21,3,8])).
% 86.46/86.53 cnf(545,plain,
% 86.46/86.53 (E(f1(f3(a5)),f3(a5))),
% 86.46/86.53 inference(scs_inference,[],[489,2])).
% 86.46/86.53 cnf(546,plain,
% 86.46/86.53 (P2(f2(f3(f3(a4)),f3(a4)),f3(a4))),
% 86.46/86.53 inference(scs_inference,[],[12,489,335,2,21])).
% 86.46/86.53 cnf(554,plain,
% 86.46/86.53 (P2(f3(a7),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[31,384,21])).
% 86.46/86.53 cnf(556,plain,
% 86.46/86.53 (P2(f2(f3(f3(a7)),f3(a7)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[31,495,384,21,10])).
% 86.46/86.53 cnf(558,plain,
% 86.46/86.53 (E(f3(a7),f1(f2(f3(a4),a4)))),
% 86.46/86.53 inference(scs_inference,[],[31,495,390,384,478,21,10,9,3])).
% 86.46/86.53 cnf(560,plain,
% 86.46/86.53 (P1(f1(f2(f3(a4),a4)))),
% 86.46/86.53 inference(scs_inference,[],[31,495,390,384,478,21,10,9,3,8])).
% 86.46/86.53 cnf(561,plain,
% 86.46/86.53 (P1(f2(f3(a4),a4))),
% 86.46/86.53 inference(scs_inference,[],[31,495,390,384,478,21,10,9,3,8,18])).
% 86.46/86.53 cnf(563,plain,
% 86.46/86.53 (E(f3(a4),f1(f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[31,495,390,384,478,21,10,9,3,8,18,23])).
% 86.46/86.53 cnf(568,plain,
% 86.46/86.53 (P2(f1(a4),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[31,437,440,563,2,10,9])).
% 86.46/86.53 cnf(569,plain,
% 86.46/86.53 (E(f1(a5),f1(f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[31,178,437,440,563,2,10,9,3])).
% 86.46/86.53 cnf(570,plain,
% 86.46/86.53 (P1(f1(f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[31,178,437,440,337,563,2,10,9,3,8])).
% 86.46/86.53 cnf(571,plain,
% 86.46/86.53 (E(f2(x5711,f1(a4)),f2(x5711,f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[31,6,2])).
% 86.46/86.53 cnf(572,plain,
% 86.46/86.53 (E(f1(f3(a4)),f1(a5))),
% 86.46/86.53 inference(scs_inference,[],[569,2])).
% 86.46/86.53 cnf(574,plain,
% 86.46/86.53 (E(x5741,f2(x5741,f1(x5741)))),
% 86.46/86.53 inference(rename_variables,[],[79])).
% 86.46/86.53 cnf(576,plain,
% 86.46/86.53 (E(x5761,f2(x5761,f1(x5761)))),
% 86.46/86.53 inference(rename_variables,[],[79])).
% 86.46/86.53 cnf(577,plain,
% 86.46/86.53 (E(a4,f2(a4,f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[79,574,576,569,554,571,568,2,10,9,3])).
% 86.46/86.53 cnf(583,plain,
% 86.46/86.53 (E(f2(a4,f3(a7)),a4)),
% 86.46/86.53 inference(scs_inference,[],[577,2])).
% 86.46/86.53 cnf(584,plain,
% 86.46/86.53 (P1(f2(a4,f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[577,345,2,8])).
% 86.46/86.53 cnf(585,plain,
% 86.46/86.53 (E(f3(f3(a7)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[577,345,2,8,23])).
% 86.46/86.53 cnf(588,plain,
% 86.46/86.53 (E(f1(a4),f3(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[585,2])).
% 86.46/86.53 cnf(589,plain,
% 86.46/86.53 (E(f3(a7),f3(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[31,585,2,3])).
% 86.46/86.53 cnf(590,plain,
% 86.46/86.53 (P1(f3(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[31,387,585,2,3,8])).
% 86.46/86.53 cnf(595,plain,
% 86.46/86.53 (E(f3(a7),f2(f3(f3(a7)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[187,571,2,3])).
% 86.46/86.53 cnf(597,plain,
% 86.46/86.53 (P1(f2(f3(f3(a7)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[187,400,571,2,3,8])).
% 86.46/86.53 cnf(598,plain,
% 86.46/86.53 (E(f2(f3(f3(a7)),f1(a4)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[595,2])).
% 86.46/86.53 cnf(611,plain,
% 86.46/86.53 (P2(f3(a6),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[41,411,21])).
% 86.46/86.53 cnf(613,plain,
% 86.46/86.53 (P2(f2(f3(f3(a6)),f3(a6)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[41,480,411,21,10])).
% 86.46/86.53 cnf(618,plain,
% 86.46/86.53 (P2(f1(a4),f3(a6))),
% 86.46/86.53 inference(scs_inference,[],[41,450,457,10,9])).
% 86.46/86.53 cnf(626,plain,
% 86.46/86.53 (E(f2(f3(f3(a7)),f3(a7)),f3(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[45,588,3])).
% 86.46/86.53 cnf(633,plain,
% 86.46/86.53 (E(f3(a4),f1(f2(f3(a5),a5)))),
% 86.46/86.53 inference(scs_inference,[],[48,367,347,352,478,21,10,9,3])).
% 86.46/86.53 cnf(638,plain,
% 86.46/86.53 (P2(f1(a5),f3(a4))),
% 86.46/86.53 inference(scs_inference,[],[48,546,370,10,9])).
% 86.46/86.53 cnf(672,plain,
% 86.46/86.53 (P2(f3(a6),f2(f3(f3(a6)),f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[86,611,406,21,10])).
% 86.46/86.53 cnf(673,plain,
% 86.46/86.53 (P2(f2(f3(f3(a6)),f3(a6)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[86,611,406,568,21,10,9])).
% 86.46/86.53 cnf(693,plain,
% 86.46/86.53 (P2(f3(a6),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[143,505,568,10,9])).
% 86.46/86.53 cnf(709,plain,
% 86.46/86.53 (E(x7091,f2(f3(x7091),x7091))),
% 86.46/86.53 inference(rename_variables,[],[187])).
% 86.46/86.53 cnf(712,plain,
% 86.46/86.53 (E(x7121,f2(f3(x7121),x7121))),
% 86.46/86.53 inference(rename_variables,[],[187])).
% 86.46/86.53 cnf(713,plain,
% 86.46/86.53 (P2(f2(f3(a4),a4),f2(a4,f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[187,709,712,33,356,37,21,10,9])).
% 86.46/86.53 cnf(714,plain,
% 86.46/86.53 (E(x7141,f2(f3(x7141),x7141))),
% 86.46/86.53 inference(rename_variables,[],[187])).
% 86.46/86.53 cnf(715,plain,
% 86.46/86.53 (E(f1(a4),f2(f3(f1(a4)),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[187,709,712,714,33,356,37,571,21,10,9,3])).
% 86.46/86.53 cnf(718,plain,
% 86.46/86.53 (E(f2(f3(f1(a4)),f3(a7)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[187,709,712,714,33,356,37,571,21,10,9,3,2])).
% 86.46/86.53 cnf(754,plain,
% 86.46/86.53 (P2(f2(a4,f1(a4)),f2(f3(a4),a4))),
% 86.46/86.53 inference(scs_inference,[],[187,397,10])).
% 86.46/86.53 cnf(779,plain,
% 86.46/86.53 (E(f3(f1(a4)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[345,79,8,23])).
% 86.46/86.53 cnf(781,plain,
% 86.46/86.53 (E(f1(a4),f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[345,79,8,23,2])).
% 86.46/86.53 cnf(782,plain,
% 86.46/86.53 (E(f2(f3(f3(a6)),f3(a6)),f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[345,79,84,8,23,2,3])).
% 86.46/86.53 cnf(785,plain,
% 86.46/86.53 (P1(f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[782,408,2,8])).
% 86.46/86.53 cnf(797,plain,
% 86.46/86.53 (P1(f2(a5,f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[354,79,8])).
% 86.46/86.53 cnf(801,plain,
% 86.46/86.53 (E(f1(a5),f3(f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[354,79,8,23,2])).
% 86.46/86.53 cnf(803,plain,
% 86.46/86.53 (P1(f3(f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[801,342,8])).
% 86.46/86.53 cnf(819,plain,
% 86.46/86.53 (P1(f2(a7,f1(a7)))),
% 86.46/86.53 inference(scs_inference,[],[388,79,8])).
% 86.46/86.53 cnf(823,plain,
% 86.46/86.53 (E(f1(a7),f3(f1(a7)))),
% 86.46/86.53 inference(scs_inference,[],[388,79,8,23,2])).
% 86.46/86.53 cnf(825,plain,
% 86.46/86.53 (P1(f2(f3(a7),a7))),
% 86.46/86.53 inference(scs_inference,[],[388,187,8])).
% 86.46/86.53 cnf(830,plain,
% 86.46/86.53 (E(f1(a4),f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[388,187,164,8,23,2,3])).
% 86.46/86.53 cnf(833,plain,
% 86.46/86.53 (E(f2(f3(f3(a6)),f3(a6)),f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[84,830,2,3])).
% 86.46/86.53 cnf(834,plain,
% 86.46/86.53 (P1(f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[84,830,416,2,3,8])).
% 86.46/86.53 cnf(839,plain,
% 86.46/86.53 (~P1(f1(a7))+P1(f3(f1(a7)))),
% 86.46/86.53 inference(scs_inference,[],[187,823,833,2,3,8])).
% 86.46/86.53 cnf(864,plain,
% 86.46/86.53 (P1(f2(a6,f1(a6)))),
% 86.46/86.53 inference(scs_inference,[],[423,79,8])).
% 86.46/86.53 cnf(869,plain,
% 86.46/86.53 (P1(f2(f3(a6),a6))),
% 86.46/86.53 inference(scs_inference,[],[423,187,8])).
% 86.46/86.53 cnf(874,plain,
% 86.46/86.53 (E(f1(a4),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[423,187,143,8,23,2,3])).
% 86.46/86.53 cnf(877,plain,
% 86.46/86.53 (P1(f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[84,874,418,2,3,8])).
% 86.46/86.53 cnf(888,plain,
% 86.46/86.53 (P1(f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[435,18,24])).
% 86.46/86.53 cnf(889,plain,
% 86.46/86.53 (P1(f1(f3(a5)))),
% 86.46/86.53 inference(scs_inference,[],[485,18,24])).
% 86.46/86.53 cnf(892,plain,
% 86.46/86.53 (P1(f3(a5))),
% 86.46/86.53 inference(scs_inference,[],[889,18])).
% 86.46/86.53 cnf(896,plain,
% 86.46/86.53 (P2(f3(a5),f3(a5))),
% 86.46/86.53 inference(scs_inference,[],[545,889,18,21,9])).
% 86.46/86.53 cnf(906,plain,
% 86.46/86.53 (P2(f2(f3(a5),f1(f3(a5))),f3(a5))),
% 86.46/86.53 inference(scs_inference,[],[79,896,9])).
% 86.46/86.53 cnf(923,plain,
% 86.46/86.53 (~E(a7,f2(a6,f1(a6)))),
% 86.46/86.53 inference(scs_inference,[],[472,11,3])).
% 86.46/86.53 cnf(925,plain,
% 86.46/86.53 (~P2(a7,f2(a6,f1(a6)))),
% 86.46/86.53 inference(scs_inference,[],[472,11,3,20])).
% 86.46/86.53 cnf(929,plain,
% 86.46/86.53 (~E(a7,f2(f3(a6),a6))),
% 86.46/86.53 inference(scs_inference,[],[472,925,467,12,10,3])).
% 86.46/86.53 cnf(934,plain,
% 86.46/86.53 (~P2(a7,f2(f3(a6),a6))),
% 86.46/86.53 inference(scs_inference,[],[929,20])).
% 86.46/86.53 cnf(937,plain,
% 86.46/86.53 (~E(f2(a7,f1(a7)),f2(f3(a6),a6))),
% 86.46/86.53 inference(scs_inference,[],[934,467,10])).
% 86.46/86.53 cnf(938,plain,
% 86.46/86.53 (~P2(f2(a7,f1(a7)),f2(f3(a6),a6))),
% 86.46/86.53 inference(scs_inference,[],[934,467,10,20])).
% 86.46/86.53 cnf(964,plain,
% 86.46/86.53 (E(f2(f2(a4,a7),x9641),f2(f2(a4,a6),x9641))),
% 86.46/86.53 inference(scs_inference,[],[33,20,5])).
% 86.46/86.53 cnf(965,plain,
% 86.46/86.53 (E(f2(f2(a4,a6),x9651),f2(f2(a4,a7),x9651))),
% 86.46/86.53 inference(scs_inference,[],[964,2])).
% 86.46/86.53 cnf(967,plain,
% 86.46/86.53 (E(f1(x9671),f1(f2(f3(x9671),x9671)))),
% 86.46/86.53 inference(rename_variables,[],[478])).
% 86.46/86.53 cnf(970,plain,
% 86.46/86.53 (E(f2(a4,a7),f2(f2(a4,a6),f1(f2(a4,a7))))),
% 86.46/86.53 inference(scs_inference,[],[478,967,79,554,638,964,2,10,9,3])).
% 86.46/86.53 cnf(975,plain,
% 86.46/86.53 (E(f2(x9751,f2(a4,a7)),f2(x9751,f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[33,20,6])).
% 86.46/86.53 cnf(979,plain,
% 86.46/86.53 (E(f2(a4,a6),f2(f2(a4,a7),f1(f2(a4,a6))))),
% 86.46/86.53 inference(scs_inference,[],[478,79,965,970,618,2,9,3])).
% 86.46/86.53 cnf(984,plain,
% 86.46/86.53 (E(f3(f2(a4,a7)),f3(f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[33,20,7])).
% 86.46/86.53 cnf(988,plain,
% 86.46/86.53 (E(f2(a4,a7),f2(f2(a4,a7),f1(f2(a4,a6))))),
% 86.46/86.53 inference(scs_inference,[],[478,30,979,568,2,9,3])).
% 86.46/86.53 cnf(989,plain,
% 86.46/86.53 (P1(f2(f3(f2(a4,a7)),f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[478,30,979,568,975,529,2,9,3,8])).
% 86.46/86.53 cnf(995,plain,
% 86.46/86.53 (~P1(f3(f2(a4,a7)))+P1(f3(f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[187,988,984,975,2,3,8])).
% 86.46/86.53 cnf(996,plain,
% 86.46/86.53 (P1(f3(f2(a4,a6)))+~P1(f1(f3(f2(a4,a7))))),
% 86.46/86.53 inference(scs_inference,[],[995,18])).
% 86.46/86.53 cnf(998,plain,
% 86.46/86.53 (P1(f3(f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[989,996,24])).
% 86.46/86.53 cnf(1000,plain,
% 86.46/86.53 (P1(f3(f2(a4,a7)))),
% 86.46/86.53 inference(scs_inference,[],[984,998,2,8])).
% 86.46/86.53 cnf(1002,plain,
% 86.46/86.53 (E(f2(x10021,f2(a4,a6)),f2(x10021,f2(a4,a7)))),
% 86.46/86.53 inference(scs_inference,[],[975,2])).
% 86.46/86.53 cnf(1017,plain,
% 86.46/86.53 (P1(f3(f1(a7)))),
% 86.46/86.53 inference(scs_inference,[],[819,24,839])).
% 86.46/86.53 cnf(1018,plain,
% 86.46/86.53 (P1(f1(a7))),
% 86.46/86.53 inference(scs_inference,[],[1017,19])).
% 86.46/86.53 cnf(1041,plain,
% 86.46/86.53 (E(f3(a7),f2(f3(f1(a4)),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[494,571,3])).
% 86.46/86.53 cnf(1104,plain,
% 86.46/86.53 (E(f1(f1(f3(a5))),f3(a5))),
% 86.46/86.53 inference(scs_inference,[],[545,4,3])).
% 86.46/86.53 cnf(1105,plain,
% 86.46/86.53 (E(f3(a5),f1(f1(f3(a5))))),
% 86.46/86.53 inference(scs_inference,[],[1104,2])).
% 86.46/86.53 cnf(1106,plain,
% 86.46/86.53 (P1(f1(f1(f3(a5))))),
% 86.46/86.53 inference(scs_inference,[],[1104,892,2,8])).
% 86.46/86.53 cnf(1113,plain,
% 86.46/86.53 (E(f1(f3(a7)),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[554,4,20])).
% 86.46/86.53 cnf(1115,plain,
% 86.46/86.53 (P1(f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[834,1113,2,8])).
% 86.46/86.53 cnf(1116,plain,
% 86.46/86.53 (E(f2(f3(f3(a6)),f3(a6)),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[833,834,1113,2,8,3])).
% 86.46/86.53 cnf(1118,plain,
% 86.46/86.53 (E(f3(a6),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[187,1116,2,3])).
% 86.46/86.53 cnf(1122,plain,
% 86.46/86.53 (E(f1(a4),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[143,1118,2,3])).
% 86.46/86.53 cnf(1146,plain,
% 86.46/86.53 (E(f3(f3(a4)),f3(f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[14,7,23])).
% 86.46/86.53 cnf(1149,plain,
% 86.46/86.53 (E(f1(a5),f3(f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[801,803,1146,2,8,3])).
% 86.46/86.53 cnf(1230,plain,
% 86.46/86.53 (E(f3(f3(a4)),f1(f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[572,1149,3,2])).
% 86.46/86.53 cnf(1233,plain,
% 86.46/86.53 (E(f3(f1(a5)),f1(f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[572,801,3,2])).
% 86.46/86.53 cnf(1261,plain,
% 86.46/86.53 (E(f3(f3(a7)),f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[585,830,590,21,3])).
% 86.46/86.53 cnf(1264,plain,
% 86.46/86.53 (E(f3(f3(a7)),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[585,874,3])).
% 86.46/86.53 cnf(1267,plain,
% 86.46/86.53 (E(f3(f3(a7)),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[585,1122,3])).
% 86.46/86.53 cnf(1268,plain,
% 86.46/86.53 (E(f1(f1(a4)),f3(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[585,1122,3,2])).
% 86.46/86.53 cnf(1287,plain,
% 86.46/86.53 (P2(f3(f3(a7)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[588,568,556,10,9])).
% 86.46/86.53 cnf(1295,plain,
% 86.46/86.53 (E(f3(a7),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[589,1264,3])).
% 86.46/86.53 cnf(1298,plain,
% 86.46/86.53 (E(f3(a7),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[589,1267,3])).
% 86.46/86.53 cnf(1299,plain,
% 86.46/86.53 (E(f1(f1(a4)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[589,1267,3,2])).
% 86.46/86.53 cnf(1338,plain,
% 86.46/86.53 (E(f1(f3(a6)),f2(f3(f3(a7)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[598,1295,3,2])).
% 86.46/86.53 cnf(1369,plain,
% 86.46/86.53 (E(f1(f1(a4)),f2(f3(f3(a7)),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[626,1267,3,2])).
% 86.46/86.53 cnf(1378,plain,
% 86.46/86.53 (E(f2(f3(a4),x13781),f2(f1(a5),x13781))),
% 86.46/86.53 inference(scs_inference,[],[14,23,5])).
% 86.46/86.53 cnf(1379,plain,
% 86.46/86.53 (E(f2(f1(a5),x13791),f2(f3(a4),x13791))),
% 86.46/86.53 inference(scs_inference,[],[1378,2])).
% 86.46/86.53 cnf(1380,plain,
% 86.46/86.53 (P1(f2(f1(a5),a4))),
% 86.46/86.53 inference(scs_inference,[],[561,1378,2,8])).
% 86.46/86.53 cnf(1381,plain,
% 86.46/86.53 (E(f2(f3(a4),x13811),f2(f1(a5),x13811))),
% 86.46/86.53 inference(rename_variables,[],[1378])).
% 86.46/86.53 cnf(1382,plain,
% 86.46/86.53 (E(f3(a4),f2(f1(a5),f1(f3(a4))))),
% 86.46/86.53 inference(scs_inference,[],[79,561,1378,1381,2,8,3])).
% 86.46/86.53 cnf(1388,plain,
% 86.46/86.53 (E(f2(f1(a5),x13881),f2(f3(a4),x13881))),
% 86.46/86.53 inference(rename_variables,[],[1379])).
% 86.46/86.53 cnf(1389,plain,
% 86.46/86.53 (E(f1(a5),f2(f3(a4),f1(f1(a5))))),
% 86.46/86.53 inference(scs_inference,[],[79,1379,1388,1382,447,2,8,3])).
% 86.46/86.53 cnf(1392,plain,
% 86.46/86.53 (E(f2(x13921,f3(a4)),f2(x13921,f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[14,23,6])).
% 86.46/86.53 cnf(1395,plain,
% 86.46/86.53 (E(f1(a5),f2(f1(a5),f1(f3(a4))))),
% 86.46/86.53 inference(scs_inference,[],[178,1389,1382,352,2,8,3])).
% 86.46/86.53 cnf(1397,plain,
% 86.46/86.53 (P1(f2(f3(f3(a4)),f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[1395,1392,350,2,8])).
% 86.46/86.53 cnf(1398,plain,
% 86.46/86.53 (E(f2(x13981,f3(a4)),f2(x13981,f1(a5)))),
% 86.46/86.53 inference(rename_variables,[],[1392])).
% 86.46/86.53 cnf(1399,plain,
% 86.46/86.53 (E(f3(a4),f2(f3(f3(a4)),f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[187,1395,1392,1398,350,2,8,3])).
% 86.46/86.53 cnf(1403,plain,
% 86.46/86.53 (E(f1(a5),f2(f3(f3(a4)),f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[178,1399,2,3])).
% 86.46/86.53 cnf(1404,plain,
% 86.46/86.53 (E(f2(f3(f3(a4)),f1(a5)),f1(a5))),
% 86.46/86.53 inference(scs_inference,[],[1403,2])).
% 86.46/86.53 cnf(1405,plain,
% 86.46/86.53 (E(f2(x14051,f1(a5)),f2(x14051,f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1392,2])).
% 86.46/86.53 cnf(1406,plain,
% 86.46/86.53 (P1(f2(a5,f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[797,1392,2,8])).
% 86.46/86.53 cnf(1407,plain,
% 86.46/86.53 (E(a5,f2(a5,f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[79,797,1392,2,8,3])).
% 86.46/86.53 cnf(1409,plain,
% 86.46/86.53 (E(f2(a5,f3(a4)),a5)),
% 86.46/86.53 inference(scs_inference,[],[1407,2])).
% 86.46/86.53 cnf(1410,plain,
% 86.46/86.53 (E(f2(f3(a5),a5),f2(a5,f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1407,12,2,3])).
% 86.46/86.53 cnf(1412,plain,
% 86.46/86.53 (E(f2(a5,f3(a4)),f2(f3(a5),a5))),
% 86.46/86.53 inference(scs_inference,[],[1410,2])).
% 86.46/86.53 cnf(1413,plain,
% 86.46/86.53 (E(f2(a5,f1(a5)),f2(f3(a5),a5))),
% 86.46/86.53 inference(scs_inference,[],[1412,1405,3])).
% 86.46/86.53 cnf(1415,plain,
% 86.46/86.53 (E(f2(f3(a5),a5),f2(a5,f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[1412,1405,3,2])).
% 86.46/86.53 cnf(1419,plain,
% 86.46/86.53 (P2(f2(a5,a4),f2(f2(a5,f1(a5)),a4))),
% 86.46/86.53 inference(scs_inference,[],[79,5,65])).
% 86.46/86.53 cnf(1421,plain,
% 86.46/86.53 (P2(f2(f2(a5,f1(a5)),a4),f2(a5,a4))),
% 86.46/86.53 inference(scs_inference,[],[79,5,75])).
% 86.46/86.53 cnf(1436,plain,
% 86.46/86.53 (E(f2(f1(f2(a5,a4)),x14361),x14361)),
% 86.46/86.53 inference(scs_inference,[],[79,125,5,26])).
% 86.46/86.53 cnf(1437,plain,
% 86.46/86.53 (E(x14371,f2(f1(f2(a5,a4)),x14371))),
% 86.46/86.53 inference(scs_inference,[],[1436,2])).
% 86.46/86.53 cnf(1452,plain,
% 86.46/86.53 (E(f2(f3(a6),x14521),f2(f3(a7),x14521))),
% 86.46/86.53 inference(scs_inference,[],[693,5,20])).
% 86.46/86.53 cnf(1453,plain,
% 86.46/86.53 (E(f2(f3(a7),x14531),f2(f3(a6),x14531))),
% 86.46/86.53 inference(scs_inference,[],[1452,2])).
% 86.46/86.53 cnf(1454,plain,
% 86.46/86.53 (P1(f2(f3(a7),a6))),
% 86.46/86.53 inference(scs_inference,[],[869,1452,2,8])).
% 86.46/86.53 cnf(1455,plain,
% 86.46/86.53 (E(f2(f3(a6),x14551),f2(f3(a7),x14551))),
% 86.46/86.53 inference(rename_variables,[],[1452])).
% 86.46/86.53 cnf(1456,plain,
% 86.46/86.53 (E(f3(a6),f2(f3(a7),f1(f3(a6))))),
% 86.46/86.53 inference(scs_inference,[],[79,869,1452,1455,2,8,3])).
% 86.46/86.53 cnf(1460,plain,
% 86.46/86.53 (P1(f2(f3(a6),a7))),
% 86.46/86.53 inference(scs_inference,[],[1453,1456,825,2,8])).
% 86.46/86.53 cnf(1461,plain,
% 86.46/86.53 (E(f2(f3(a7),x14611),f2(f3(a6),x14611))),
% 86.46/86.53 inference(rename_variables,[],[1453])).
% 86.46/86.53 cnf(1462,plain,
% 86.46/86.53 (E(f3(a7),f2(f3(a6),f1(f3(a7))))),
% 86.46/86.53 inference(scs_inference,[],[79,1453,1461,1456,825,2,8,3])).
% 86.46/86.53 cnf(1465,plain,
% 86.46/86.53 (P2(f2(a5,a4),f2(a5,f2(a4,f1(a4))))),
% 86.46/86.53 inference(scs_inference,[],[79,6,65])).
% 86.46/86.53 cnf(1468,plain,
% 86.46/86.53 (E(f1(a4),f2(f3(a6),f1(f3(a7))))),
% 86.46/86.53 inference(scs_inference,[],[164,1462,384,2,8,3])).
% 86.46/86.53 cnf(1469,plain,
% 86.46/86.53 (E(f2(x14691,f3(a6)),f2(x14691,f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[693,6,20])).
% 86.46/86.53 cnf(1472,plain,
% 86.46/86.53 (E(f1(a4),f2(f3(a7),f1(f3(a6))))),
% 86.46/86.53 inference(scs_inference,[],[143,1468,1456,412,2,8,3])).
% 86.46/86.53 cnf(1473,plain,
% 86.46/86.53 (P2(f2(a5,f2(a4,f1(a4))),f2(a5,a4))),
% 86.46/86.53 inference(scs_inference,[],[79,6,75])).
% 86.46/86.53 cnf(1476,plain,
% 86.46/86.53 (E(f2(x14761,f3(a6)),f2(x14761,f3(a7)))),
% 86.46/86.53 inference(rename_variables,[],[1469])).
% 86.46/86.53 cnf(1477,plain,
% 86.46/86.53 (E(f3(a6),f2(f3(f3(a6)),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[187,1472,409,1469,1476,2,8,3])).
% 86.46/86.53 cnf(1482,plain,
% 86.46/86.53 (E(f1(a4),f2(f3(f3(a6)),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[143,1477,2,3])).
% 86.46/86.53 cnf(1486,plain,
% 86.46/86.53 (E(f2(x14861,f3(a7)),f2(x14861,f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1469,2])).
% 86.46/86.53 cnf(1487,plain,
% 86.46/86.53 (P1(f2(a4,f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[584,1469,2,8])).
% 86.46/86.53 cnf(1488,plain,
% 86.46/86.53 (E(a4,f2(a4,f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[577,584,1469,2,8,3])).
% 86.46/86.53 cnf(1489,plain,
% 86.46/86.53 (E(f3(f3(a6)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[577,584,1469,2,8,3,23])).
% 86.46/86.53 cnf(1492,plain,
% 86.46/86.53 (E(f2(a4,f3(a6)),a4)),
% 86.46/86.53 inference(scs_inference,[],[1488,2])).
% 86.46/86.53 cnf(1513,plain,
% 86.46/86.53 (E(f1(a4),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1489,2])).
% 86.46/86.53 cnf(1514,plain,
% 86.46/86.53 (E(f2(f3(f3(a6)),f3(a6)),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[84,1489,2,3])).
% 86.46/86.53 cnf(1516,plain,
% 86.46/86.53 (E(f3(a6),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[187,1514,2,3])).
% 86.46/86.53 cnf(1518,plain,
% 86.46/86.53 (E(f3(f3(a6)),f3(a6))),
% 86.46/86.53 inference(scs_inference,[],[1516,2])).
% 86.46/86.53 cnf(1525,plain,
% 86.46/86.53 (E(f1(a4),f2(f3(f1(a4)),f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[715,1486,3])).
% 86.46/86.53 cnf(1529,plain,
% 86.46/86.53 (P1(f2(f3(f1(a4)),f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1525,449,2,8])).
% 86.46/86.53 cnf(1535,plain,
% 86.46/86.53 (E(f2(f3(f1(a4)),f3(a7)),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[718,1513,3])).
% 86.46/86.53 cnf(1538,plain,
% 86.46/86.53 (E(f3(a7),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1041,1535,3])).
% 86.46/86.53 cnf(1539,plain,
% 86.46/86.53 (E(f3(f3(a6)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[1041,1535,3,2])).
% 86.46/86.53 cnf(1553,plain,
% 86.46/86.53 (P2(f3(f1(a4)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[779,785,21])).
% 86.46/86.53 cnf(1555,plain,
% 86.46/86.53 (E(f3(f1(a4)),f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[779,830,785,21,3])).
% 86.46/86.53 cnf(1558,plain,
% 86.46/86.53 (E(f3(f1(a4)),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[779,874,3])).
% 86.46/86.53 cnf(1559,plain,
% 86.46/86.53 (E(f1(f3(a6)),f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[779,874,3,2])).
% 86.46/86.53 cnf(1560,plain,
% 86.46/86.53 (E(f3(f1(a4)),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[779,1122,3])).
% 86.46/86.53 cnf(1563,plain,
% 86.46/86.53 (E(f3(f1(a4)),f2(f1(f2(a5,a4)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[779,1437,3])).
% 86.46/86.53 cnf(1567,plain,
% 86.46/86.53 (P1(f2(f1(f2(a5,a4)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1563,785,2,8])).
% 86.46/86.53 cnf(1568,plain,
% 86.46/86.53 (E(f3(f1(a4)),f2(f3(f3(a6)),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[779,1563,1482,785,2,8,3])).
% 86.46/86.53 cnf(1570,plain,
% 86.46/86.53 (E(f3(f1(a4)),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[779,1568,1513,2,3])).
% 86.46/86.53 cnf(1572,plain,
% 86.46/86.53 (E(f3(f3(a6)),f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1570,2])).
% 86.46/86.53 cnf(1579,plain,
% 86.46/86.53 (P2(f3(a6),f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[781,611,461,21,10])).
% 86.46/86.53 cnf(1582,plain,
% 86.46/86.53 (P2(f3(a7),f3(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[781,554,10])).
% 86.46/86.53 cnf(1595,plain,
% 86.46/86.53 (P2(f3(f1(a4)),f3(a6))),
% 86.46/86.53 inference(scs_inference,[],[781,618,613,10,9])).
% 86.46/86.53 cnf(1611,plain,
% 86.46/86.53 (E(f2(f2(x16111,f1(x16111)),x16112),f2(x16111,x16112))),
% 86.46/86.53 inference(scs_inference,[],[11,1380,27,4,7,5])).
% 86.46/86.53 cnf(1612,plain,
% 86.46/86.53 (E(f2(x16121,f2(x16122,f1(x16122))),f2(x16121,x16122))),
% 86.46/86.53 inference(scs_inference,[],[11,1380,27,4,7,5,6])).
% 86.46/86.53 cnf(1619,plain,
% 86.46/86.53 (~E(f2(a6,f1(a6)),a7)),
% 86.46/86.53 inference(scs_inference,[],[11,1567,906,1419,1380,923,27,4,7,5,6,24,22,20,2])).
% 86.46/86.53 cnf(1620,plain,
% 86.46/86.53 (~E(f2(f2(a5,a4),a7),f2(f2(f2(a5,a4),a6),f1(a6)))),
% 86.46/86.53 inference(scs_inference,[],[11,1567,906,1419,1380,923,125,27,4,7,5,6,24,22,20,2,26])).
% 86.46/86.53 cnf(1623,plain,
% 86.46/86.53 (P1(f2(f3(a7),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[11,1555,1567,906,1419,1380,923,834,125,27,4,7,5,6,24,22,20,2,26,25])).
% 86.46/86.53 cnf(1627,plain,
% 86.46/86.53 (P2(f3(f3(a7)),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[11,1299,1287,1538,1555,1567,906,1419,1380,1115,923,834,125,27,4,7,5,6,24,22,20,2,26,25,21,10])).
% 86.46/86.53 cnf(1629,plain,
% 86.46/86.53 (E(x16291,f2(f1(f2(a5,a4)),x16291))),
% 86.46/86.53 inference(rename_variables,[],[1437])).
% 86.46/86.53 cnf(1630,plain,
% 86.46/86.53 (~P2(f2(a6,f1(a6)),f2(f3(a7),a7))),
% 86.46/86.53 inference(scs_inference,[],[11,1299,1287,118,1538,1555,1567,906,1419,1380,1115,923,1018,834,125,1437,27,4,7,5,6,24,22,20,2,26,25,21,10,8,9])).
% 86.46/86.53 cnf(1632,plain,
% 86.46/86.53 (~E(f2(f1(f2(a5,a4)),a7),a6)),
% 86.46/86.53 inference(scs_inference,[],[11,1299,1287,118,1538,1555,1567,906,1419,1380,1115,923,1018,834,472,125,1437,1629,27,4,7,5,6,24,22,20,2,26,25,21,10,8,9,3])).
% 86.46/86.53 cnf(1635,plain,
% 86.46/86.53 (E(f2(x16351,f2(a5,f3(a4))),f2(x16351,a5))),
% 86.46/86.53 inference(scs_inference,[],[1409,6])).
% 86.46/86.53 cnf(1639,plain,
% 86.46/86.53 (E(f2(f2(a5,f3(a4)),x16391),f2(a5,x16391))),
% 86.46/86.53 inference(scs_inference,[],[1409,1623,6,27,4,5])).
% 86.46/86.53 cnf(1643,plain,
% 86.46/86.53 (P1(f2(f2(a5,f1(a5)),a4))),
% 86.46/86.53 inference(scs_inference,[],[1409,1623,417,1421,6,27,4,5,7,24,22])).
% 86.46/86.53 cnf(1645,plain,
% 86.46/86.53 (E(f3(f3(a7)),f3(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1409,1623,417,1627,1421,6,27,4,5,7,24,22,20])).
% 86.46/86.53 cnf(1648,plain,
% 86.46/86.53 (~E(f2(f2(a5,a4),a7),f2(f2(a5,a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[1409,1623,417,1627,1612,1421,1620,923,6,27,4,5,7,24,22,20,2,26])).
% 86.46/86.53 cnf(1651,plain,
% 86.46/86.53 (P1(f2(f2(f3(a4),a4),a7))),
% 86.46/86.53 inference(scs_inference,[],[1409,1623,417,1627,1612,1421,1620,560,923,558,6,27,4,5,7,24,22,20,2,26,25])).
% 86.46/86.53 cnf(1653,plain,
% 86.46/86.53 (~E(f2(a6,f1(a6)),f2(f3(a7),a7))),
% 86.46/86.53 inference(scs_inference,[],[1409,1623,1630,417,1627,1612,1421,1620,560,864,923,558,6,27,4,5,7,24,22,20,2,26,25,21])).
% 86.46/86.53 cnf(1655,plain,
% 86.46/86.53 (P2(f3(a6),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1409,1579,1623,1558,1630,417,1627,1612,1421,1620,560,864,923,558,6,27,4,5,7,24,22,20,2,26,25,21,10])).
% 86.46/86.53 cnf(1656,plain,
% 86.46/86.53 (P2(f1(f3(a6)),f1(a4))),
% 86.46/86.53 inference(scs_inference,[],[1553,1409,1579,1623,1558,1630,417,1627,1612,1421,1620,560,864,923,558,6,27,4,5,7,24,22,20,2,26,25,21,10,9])).
% 86.46/86.53 cnf(1671,plain,
% 86.46/86.53 (~E(f2(f3(a7),a7),f2(a6,f1(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1492,1653,597,1473,1465,1406,27,6,5,7,4,24,22,20,2])).
% 86.46/86.53 cnf(1672,plain,
% 86.46/86.53 (P1(f2(f1(a4),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1492,1560,1653,597,1473,1465,1406,1115,27,6,5,7,4,24,22,20,2,25])).
% 86.46/86.53 cnf(1677,plain,
% 86.46/86.53 (E(f2(x16771,f1(x16771)),x16771)),
% 86.46/86.53 inference(rename_variables,[],[11])).
% 86.46/86.53 cnf(1678,plain,
% 86.46/86.53 (~E(f2(a5,f2(a4,a7)),f2(f2(a5,a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[11,1518,1492,1560,1653,1648,597,1473,1465,1406,888,28,1115,16,27,6,5,7,4,24,22,20,2,25,21,9,3])).
% 86.46/86.53 cnf(1680,plain,
% 86.46/86.53 (P1(f2(f2(a5,a4),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[11,1518,1492,1560,1653,1648,597,1473,1465,1406,888,28,1115,16,27,6,5,7,4,24,22,20,2,25,21,9,3,145])).
% 86.46/86.53 cnf(1681,plain,
% 86.46/86.53 (E(f3(f1(a4)),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[11,1518,1492,1560,1653,1648,597,1473,1465,1406,888,28,1115,16,27,6,5,7,4,24,22,20,2,25,21,9,3,145,146])).
% 86.46/86.53 cnf(1683,plain,
% 86.46/86.53 (~P2(f2(a6,f1(a6)),f2(a7,f1(a7)))),
% 86.46/86.53 inference(scs_inference,[],[11,1677,1518,1492,1560,1653,1648,597,1473,1465,1406,888,28,1115,16,27,6,5,7,4,24,22,20,2,25,21,9,3,145,146,10])).
% 86.46/86.53 cnf(1691,plain,
% 86.46/86.53 (E(f2(a4,x16911),f2(f2(a4,f3(a6)),x16911))),
% 86.46/86.53 inference(scs_inference,[],[1680,1488,27,6,4,7,5])).
% 86.46/86.53 cnf(1692,plain,
% 86.46/86.53 (P1(f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[1680,1488,27,6,4,7,5,24])).
% 86.46/86.53 cnf(1697,plain,
% 86.46/86.53 (~E(f2(f2(a5,a4),a7),f2(a5,f2(a4,a6)))),
% 86.46/86.53 inference(scs_inference,[],[1680,1678,1488,713,16,472,27,6,4,7,5,24,20,2,26])).
% 86.46/86.53 cnf(1698,plain,
% 86.46/86.53 (E(f2(f2(x16981,x16982),x16983),f2(x16981,f2(x16982,x16983)))),
% 86.46/86.53 inference(rename_variables,[],[16])).
% 86.46/86.53 cnf(1704,plain,
% 86.46/86.53 (P2(f3(a7),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[1582,1680,1683,1678,1681,1105,1488,713,1106,864,16,472,27,6,4,7,5,24,20,2,26,25,21,10])).
% 86.46/86.53 cnf(1705,plain,
% 86.46/86.53 (P2(f1(f2(a5,a4)),f3(a6))),
% 86.46/86.53 inference(scs_inference,[],[1595,1582,1680,1683,1678,1681,1105,1488,713,1106,864,16,472,27,6,4,7,5,24,20,2,26,25,21,10,9])).
% 86.46/86.53 cnf(1707,plain,
% 86.46/86.53 (P1(f2(f3(a4),f2(a4,a7)))),
% 86.46/86.53 inference(scs_inference,[],[1595,1582,1680,1268,1683,1678,1681,1645,1651,1105,1488,713,1106,864,16,1698,472,27,6,4,7,5,24,20,2,26,25,21,10,9,3,8])).
% 86.46/86.53 cnf(1710,plain,
% 86.46/86.53 (P2(f1(f2(a5,a4)),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[1692,27])).
% 86.46/86.53 cnf(1716,plain,
% 86.46/86.53 (P1(f1(f3(f1(a4))))),
% 86.46/86.53 inference(scs_inference,[],[1692,1529,583,27,6,7,5,4,24])).
% 86.46/86.53 cnf(1718,plain,
% 86.46/86.53 (E(f1(f2(a5,a4)),f3(a6))),
% 86.46/86.53 inference(scs_inference,[],[1705,1692,1529,583,27,6,7,5,4,24,20])).
% 86.46/86.53 cnf(1720,plain,
% 86.46/86.53 (~E(f2(a5,f2(a4,a6)),f2(f2(a5,a4),a7))),
% 86.46/86.53 inference(scs_inference,[],[1705,1692,1697,1529,583,27,6,7,5,4,24,20,2])).
% 86.46/86.53 cnf(1721,plain,
% 86.46/86.53 (P1(f2(f3(a4),f3(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1705,1692,1697,1529,1230,583,570,27,6,7,5,4,24,20,2,25])).
% 86.46/86.53 cnf(1725,plain,
% 86.46/86.53 (~E(f2(f3(a6),a7),f2(a6,f1(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1539,1705,1692,1671,1697,1529,1230,583,1453,888,570,27,6,7,5,4,24,20,2,25,21,3])).
% 86.46/86.53 cnf(1732,plain,
% 86.46/86.53 (E(f2(a5,x17321),f2(f2(a5,f3(a4)),x17321))),
% 86.46/86.53 inference(scs_inference,[],[1707,1407,27,6,4,5])).
% 86.46/86.53 cnf(1736,plain,
% 86.46/86.53 (E(f3(a7),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[1707,1704,1397,1407,27,6,4,5,7,24,20])).
% 86.46/86.53 cnf(1738,plain,
% 86.46/86.53 (~E(f2(a6,f1(a6)),f2(f3(a6),a7))),
% 86.46/86.53 inference(scs_inference,[],[1707,1704,1725,1397,1407,27,6,4,5,7,24,20,2])).
% 86.46/86.53 cnf(1745,plain,
% 86.46/86.53 (E(f2(x17451,a4),f2(x17451,f2(a4,f3(a7))))),
% 86.46/86.53 inference(scs_inference,[],[1672,577,27,6])).
% 86.46/86.53 cnf(1749,plain,
% 86.46/86.53 (P1(f1(f2(a5,f1(a5))))),
% 86.46/86.53 inference(scs_inference,[],[1672,1643,577,27,6,5,7,4,24])).
% 86.46/86.53 cnf(1754,plain,
% 86.46/86.53 (P1(f2(f2(a5,a4),a7))),
% 86.46/86.53 inference(scs_inference,[],[1672,1736,1643,1632,1692,754,577,27,6,5,7,4,24,20,2,25])).
% 86.46/86.53 cnf(1756,plain,
% 86.46/86.53 (P2(f3(a6),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[1718,1672,1736,1710,1643,1632,1692,754,577,27,6,5,7,4,24,20,2,25,9])).
% 86.46/86.53 cnf(1757,plain,
% 86.46/86.53 (~E(a6,f2(f3(a6),a7))),
% 86.46/86.53 inference(scs_inference,[],[11,1718,1672,1736,1738,1710,1643,1632,1692,754,577,27,6,5,7,4,24,20,2,25,9,3])).
% 86.46/86.53 cnf(1763,plain,
% 86.46/86.53 (E(f2(f1(a4),x17631),f2(f3(a7),x17631))),
% 86.46/86.53 inference(scs_inference,[],[1754,164,27,5])).
% 86.46/86.53 cnf(1764,plain,
% 86.46/86.53 (E(f2(x17641,f3(a6)),f2(x17641,f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1754,164,41,27,5,6])).
% 86.46/86.53 cnf(1766,plain,
% 86.46/86.53 (E(f1(f3(a6)),f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[1754,163,164,41,27,5,6,7,4])).
% 86.46/86.53 cnf(1769,plain,
% 86.46/86.53 (E(f3(a6),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[1754,1756,522,163,164,41,27,5,6,7,4,24,20])).
% 86.46/86.53 cnf(1771,plain,
% 86.46/86.53 (~E(f2(f3(a6),a7),a6)),
% 86.46/86.53 inference(scs_inference,[],[1754,1756,1757,522,163,164,41,27,5,6,7,4,24,20,2])).
% 86.46/86.53 cnf(1781,plain,
% 86.46/86.53 (P1(f2(a5,f2(a4,a7)))),
% 86.46/86.53 inference(scs_inference,[],[11,1754,1756,1757,1404,1611,1397,1612,485,522,633,16,71,163,164,41,27,5,6,7,4,24,20,2,25,21,3,26,8])).
% 86.46/86.53 cnf(1785,plain,
% 86.46/86.53 (E(f2(x17851,f1(a4)),f2(x17851,f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1781,143,27,6])).
% 86.46/86.53 cnf(1787,plain,
% 86.46/86.53 (E(f2(f3(a7),x17871),f2(f1(a4),x17871))),
% 86.46/86.53 inference(scs_inference,[],[1781,31,143,12,27,6,7,5])).
% 86.46/86.53 cnf(1792,plain,
% 86.46/86.53 (P1(f2(f2(a5,a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[1781,1769,937,1692,188,31,41,143,12,27,6,7,5,4,24,2,25])).
% 86.46/86.53 cnf(1794,plain,
% 86.46/86.53 (~E(f2(f3(a7),a7),a6)),
% 86.46/86.53 inference(scs_inference,[],[1781,1769,1771,937,1692,1452,188,31,41,143,12,27,6,7,5,4,24,2,25,3])).
% 86.46/86.53 cnf(1802,plain,
% 86.46/86.53 (E(f1(f1(a4)),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1792,41,143,12,187,27,7,6,5,4])).
% 86.46/86.53 cnf(1803,plain,
% 86.46/86.53 (P1(f1(f3(f2(a4,a7))))),
% 86.46/86.53 inference(scs_inference,[],[1792,989,41,143,12,187,27,7,6,5,4,24])).
% 86.46/86.53 cnf(1806,plain,
% 86.46/86.53 (P1(f2(f3(a4),f1(a5)))),
% 86.46/86.53 inference(scs_inference,[],[1792,1233,929,570,989,41,143,12,187,27,7,6,5,4,24,2,25])).
% 86.46/86.53 cnf(1817,plain,
% 86.46/86.53 (E(f2(x18171,x18172),f2(x18171,f2(f3(x18172),x18172)))),
% 86.46/86.53 inference(scs_inference,[],[1721,536,187,27,24,6])).
% 86.46/86.53 cnf(1818,plain,
% 86.46/86.53 (E(f2(f1(a4),x18181),f2(f3(a6),x18181))),
% 86.46/86.53 inference(scs_inference,[],[1721,536,143,187,27,24,6,5])).
% 86.46/86.53 cnf(1821,plain,
% 86.46/86.53 (~E(f2(f1(a4),a7),a6)),
% 86.46/86.53 inference(scs_inference,[],[1794,1721,1787,536,143,187,79,27,24,6,5,7,4,3])).
% 86.46/86.53 cnf(1823,plain,
% 86.46/86.53 (P1(f2(f1(a4),a7))),
% 86.46/86.53 inference(scs_inference,[],[1794,1721,1787,1298,1115,536,143,187,79,27,24,6,5,7,4,3,25])).
% 86.46/86.53 cnf(1834,plain,
% 86.46/86.53 (E(f2(x18341,x18342),f2(x18341,f2(x18342,f1(x18342))))),
% 86.46/86.53 inference(scs_inference,[],[1823,79,27,6])).
% 86.46/86.53 cnf(1835,plain,
% 86.46/86.53 (E(f2(f2(f3(x18351),x18351),x18352),f2(x18351,x18352))),
% 86.46/86.53 inference(scs_inference,[],[12,1823,79,27,6,5])).
% 86.46/86.53 cnf(1838,plain,
% 86.46/86.53 (E(f2(f3(x18381),x18381),x18381)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(1840,plain,
% 86.46/86.53 (E(f2(f3(x18401),x18401),x18401)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(1841,plain,
% 86.46/86.53 (~P2(f2(f3(a7),a7),f2(f3(a6),a6))),
% 86.46/86.53 inference(scs_inference,[],[12,1838,1840,1823,1785,473,79,27,6,5,3,9,10])).
% 86.46/86.53 cnf(1852,plain,
% 86.46/86.53 (E(f2(x18521,x18522),f2(f2(f3(x18521),x18521),x18522))),
% 86.46/86.53 inference(scs_inference,[],[1806,187,27,5])).
% 86.46/86.53 cnf(1853,plain,
% 86.46/86.53 (P2(f3(a6),f1(f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[1766,1806,1655,187,27,5,10])).
% 86.46/86.53 cnf(1854,plain,
% 86.46/86.53 (~E(f2(f3(a6),f2(f3(a7),a7)),a6)),
% 86.46/86.53 inference(scs_inference,[],[1766,1817,1806,1655,1771,187,27,5,10,3])).
% 86.46/86.53 cnf(1859,plain,
% 86.46/86.53 (P1(f2(f3(a7),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[1841,1766,1817,1806,1656,1655,1771,1261,825,834,187,27,5,10,3,21,9,25])).
% 86.46/86.53 cnf(1864,plain,
% 86.46/86.53 (E(f2(x18641,x18642),f2(f2(x18641,f1(x18641)),x18642))),
% 86.46/86.53 inference(scs_inference,[],[1859,79,27,5])).
% 86.46/86.53 cnf(1868,plain,
% 86.46/86.53 (E(f2(f3(x18681),x18681),x18681)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(1871,plain,
% 86.46/86.53 (~P2(f2(f3(a6),a6),f2(a7,f1(a7)))),
% 86.46/86.53 inference(scs_inference,[],[12,1868,1859,1559,1635,1854,877,73,79,27,5,2,3,21,9])).
% 86.46/86.53 cnf(1873,plain,
% 86.46/86.53 (P1(f2(f3(a6),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[12,1868,1859,1559,1635,1854,877,73,1264,79,27,5,2,3,21,9,25])).
% 86.46/86.53 cnf(1877,plain,
% 86.46/86.53 (~E(f2(f3(a6),f2(a7,f1(a7))),a6)),
% 86.46/86.53 inference(scs_inference,[],[1873,1834,1771,27,3])).
% 86.46/86.53 cnf(1887,plain,
% 86.46/86.53 (~P2(f2(f3(a6),a6),f2(f3(a7),a7))),
% 86.46/86.53 inference(scs_inference,[],[12,1413,1639,1877,1454,118,27,2,3,9])).
% 86.46/86.53 cnf(1889,plain,
% 86.46/86.53 (P1(f2(f1(a4),f3(a7)))),
% 86.46/86.53 inference(scs_inference,[],[12,1413,1639,1877,1454,118,1267,1115,27,2,3,9,25])).
% 86.46/86.53 cnf(1895,plain,
% 86.46/86.53 (P2(f3(a6),f2(f3(f3(a6)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1889,1764,672,27,10])).
% 86.46/86.53 cnf(1896,plain,
% 86.46/86.53 (E(f2(x18961,f3(a6)),f2(x18961,f1(a4)))),
% 86.46/86.53 inference(rename_variables,[],[1764])).
% 86.46/86.53 cnf(1897,plain,
% 86.46/86.53 (~E(f2(f2(f3(a6),a6),f1(a6)),a7)),
% 86.46/86.53 inference(scs_inference,[],[1889,1764,1852,1619,672,27,10,3])).
% 86.46/86.53 cnf(1899,plain,
% 86.46/86.53 (P2(f2(f3(f3(a6)),f1(a4)),f3(a7))),
% 86.46/86.53 inference(scs_inference,[],[1889,1764,1896,1852,1619,673,672,27,10,3,9])).
% 86.46/86.53 cnf(1918,plain,
% 86.46/86.53 (P1(f2(f1(a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[12,1899,1415,1897,1864,1460,925,1118,1115,27,22,2,20,3,9,25])).
% 86.46/86.53 cnf(1924,plain,
% 86.46/86.53 (E(f3(a6),f2(f3(f3(a6)),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1918,1895,27,20])).
% 86.46/86.53 cnf(1926,plain,
% 86.46/86.53 (~E(f2(f2(a5,f3(a4)),f2(a4,a6)),f2(f2(a5,a4),a7))),
% 86.46/86.53 inference(scs_inference,[],[1918,1895,1732,1720,27,20,3])).
% 86.46/86.53 cnf(1930,plain,
% 86.46/86.53 (~E(f2(f1(a4),a6),f2(f3(a7),a7))),
% 86.46/86.53 inference(scs_inference,[],[1918,1818,1895,1732,1887,1720,27,20,3,9,21])).
% 86.46/86.53 cnf(1934,plain,
% 86.46/86.53 (~E(f2(f3(a7),a7),f2(f1(a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[1918,1818,1895,1749,1732,1887,1720,27,20,3,9,21,25,2])).
% 86.46/86.53 cnf(1942,plain,
% 86.46/86.53 (~E(a7,f2(f1(a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[12,1572,1934,1926,1000,888,27,2,21,3])).
% 86.46/86.53 cnf(1943,plain,
% 86.46/86.53 (E(f2(f3(x19431),x19431),x19431)),
% 86.46/86.53 inference(rename_variables,[],[12])).
% 86.46/86.53 cnf(1944,plain,
% 86.46/86.53 (~P2(f2(f3(a6),a6),a7)),
% 86.46/86.53 inference(scs_inference,[],[12,1943,1572,1934,1926,1000,28,888,27,2,21,3,9])).
% 86.46/86.53 cnf(1946,plain,
% 86.46/86.53 (P1(f2(f3(a6),f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[12,1943,1572,1934,1926,1000,28,888,877,1558,27,2,21,3,9,25])).
% 86.46/86.53 cnf(1948,plain,
% 86.46/86.53 (P1(f2(f2(a4,f3(a6)),f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[12,1943,1572,1934,1926,1691,1000,1487,28,888,877,1558,27,2,21,3,9,25,8])).
% 86.46/86.53 cnf(1962,plain,
% 86.46/86.53 (~P2(x19621,f1(f1(a4)))+P2(x19621,f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1946,1942,1802,1930,1924,1948,1803,1853,1763,24,27,2,3,9,20,25,10])).
% 86.46/86.53 cnf(2015,plain,
% 86.46/86.53 (~P2(f2(a7,f1(a7)),f2(f1(a4),a6))),
% 86.46/86.53 inference(scs_inference,[],[938,1818,1487,27,10])).
% 86.46/86.53 cnf(2160,plain,
% 86.46/86.53 (P2(f1(f1(a4)),f1(f1(a4)))),
% 86.46/86.53 inference(scs_inference,[],[1115,27])).
% 86.46/86.53 cnf(2163,plain,
% 86.46/86.53 (E(f2(x21631,f2(x21632,f1(x21632))),f2(x21631,x21632))),
% 86.46/86.53 inference(rename_variables,[],[1612])).
% 86.46/86.53 cnf(2164,plain,
% 86.46/86.53 (~P2(a6,f2(f3(a7),f2(a7,f1(a7))))),
% 86.46/86.53 inference(scs_inference,[],[1612,2163,1944,118,1115,27,9,10])).
% 86.46/86.53 cnf(2166,plain,
% 86.46/86.53 (~E(f2(f1(a4),f2(a7,f1(a7))),a6)),
% 86.46/86.53 inference(scs_inference,[],[1821,1612,2163,1834,1944,118,1115,27,9,10,3])).
% 86.46/86.53 cnf(2170,plain,
% 86.46/86.53 (P2(f1(f1(a4)),f1(f3(a6)))),
% 86.46/86.53 inference(scs_inference,[],[1716,1821,1612,2163,1834,1944,118,1115,27,9,10,3,25,1962])).
% 86.46/86.53 cnf(2178,plain,
% 86.46/86.53 (~E(f2(f2(a5,f3(a4)),f2(a4,a7)),f2(f2(a5,a4),a7))),
% 86.46/86.53 inference(scs_inference,[],[2160,2170,1338,1369,2164,2166,1002,1926,423,2,9,21,10,3])).
% 86.46/86.53 cnf(2182,plain,
% 86.46/86.53 (E(f3(f3(a7)),f1(f2(a5,a4)))),
% 86.46/86.53 inference(scs_inference,[],[14,2160,2170,1338,1369,1745,2164,2166,1002,1926,423,2,9,21,10,3,8,146])).
% 86.46/86.53 cnf(2189,plain,
% 86.46/86.53 (E(f2(f2(f3(x21891),x21891),x21892),f2(x21891,x21892))),
% 86.46/86.53 inference(rename_variables,[],[1835])).
% 86.46/86.53 cnf(2194,plain,
% 86.46/86.53 ($false),
% 86.46/86.53 inference(scs_inference,[],[2182,2178,1871,1639,2015,590,1835,2189,125,2,9,21,10,3]),
% 86.46/86.53 ['proof']).
% 86.46/86.53 % SZS output end Proof
% 86.46/86.53 % Total time :85.880000s
%------------------------------------------------------------------------------