%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT003-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 : n032.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:09 EDT 2024
% Result : Unsatisfiable 59.22s 59.30s
% Output : CNFRefutation 59.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : CAT003-4 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.28 % Computer : n032.cluster.edu
% 0.07/0.28 % Model : x86_64 x86_64
% 0.07/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.28 % Memory : 8042.1875MB
% 0.07/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.28 % CPULimit : 300
% 0.07/0.28 % WCLimit : 300
% 0.07/0.28 % DateTime : Tue Jun 18 12:47:23 EDT 2024
% 0.07/0.28 % CPUTime :
% 0.14/0.47 start to proof:theBenchmark
% 59.22/59.28 %-------------------------------------------
% 59.22/59.28 % File :CSE---1.7
% 59.22/59.28 % Problem :theBenchmark
% 59.22/59.28 % Transform :cnf
% 59.22/59.28 % Format :tptp:raw
% 59.22/59.28 % Command :java -jar mcs_scs.jar %d %s
% 59.22/59.28
% 59.22/59.28 % Result :Theorem 58.780000s
% 59.22/59.28 % Output :CNFRefutation 58.780000s
% 59.22/59.28 %-------------------------------------------
% 59.22/59.29 %--------------------------------------------------------------------------
% 59.22/59.29 % File : CAT003-4 : TPTP v8.2.0. Released v1.0.0.
% 59.22/59.29 % Domain : Category Theory
% 59.22/59.29 % Problem : XY epimorphism => X epimorphism
% 59.22/59.29 % Version : [Sco79] axioms : Reduced > Complete.
% 59.22/59.29 % English : If xy is an epimorphism, then x is an epimorphism.
% 59.22/59.29
% 59.22/59.29 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 59.22/59.29 % Source : [TPTP]
% 59.22/59.29 % Names :
% 59.22/59.29
% 59.22/59.29 % Status : Unsatisfiable
% 59.22/59.29 % 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.27 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.40 v2.0.0
% 59.22/59.29 % Syntax : Number of clauses : 16 ( 7 unt; 0 nHn; 13 RR)
% 59.22/59.29 % Number of literals : 28 ( 12 equ; 13 neg)
% 59.22/59.29 % Maximal clause size : 3 ( 1 avg)
% 59.22/59.29 % Maximal term depth : 3 ( 1 avg)
% 59.22/59.29 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 59.22/59.29 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 59.22/59.29 % Number of variables : 22 ( 2 sgn)
% 59.22/59.29 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.22/59.29
% 59.22/59.29 % Comments : The dependent axioms have been removed.
% 59.22/59.29 %--------------------------------------------------------------------------
% 59.22/59.29 %----Include Scott's axioms for category theory
% 59.22/59.29 include('Axioms/CAT004-0.ax').
% 59.22/59.29 %--------------------------------------------------------------------------
% 59.22/59.29 cnf(assume_ab_exists,hypothesis,
% 59.22/59.29 there_exists(compose(a,b)) ).
% 59.22/59.29
% 59.22/59.29 cnf(epimorphism,hypothesis,
% 59.22/59.29 ( compose(X,compose(a,b)) != Y
% 59.22/59.29 | compose(Z,compose(a,b)) != Y
% 59.22/59.29 | X = Z ) ).
% 59.22/59.29
% 59.22/59.29 cnf(assume_h_exists,hypothesis,
% 59.22/59.30 there_exists(h) ).
% 59.22/59.30
% 59.22/59.30 cnf(ha_equals_ga,hypothesis,
% 59.22/59.30 compose(h,a) = compose(g,a) ).
% 59.22/59.30
% 59.22/59.30 cnf(prove_g_equals_h,negated_conjecture,
% 59.22/59.30 g != h ).
% 59.22/59.30
% 59.22/59.30 %--------------------------------------------------------------------------
% 59.22/59.30 %-------------------------------------------
% 59.22/59.30 % Proof found
% 59.22/59.30 % SZS status Theorem for theBenchmark
% 59.22/59.30 % SZS output start Proof
% 59.22/59.30 %ClaNum:26(EqnAxiom:10)
% 59.22/59.30 %VarNum:46(SingletonVarNum:22)
% 59.22/59.30 %MaxLitNum:3
% 59.22/59.30 %MaxfuncDepth:2
% 59.22/59.30 %SharedTerms:11
% 59.22/59.30 %goalClause: 17
% 59.22/59.30 %singleGoalClaCount:1
% 59.22/59.30 [11]P1(a1)
% 59.22/59.30 [17]~E(a1,a7)
% 59.22/59.30 [14]E(f3(a1,a5),f3(a7,a5))
% 59.22/59.30 [15]P1(f3(a5,a6))
% 59.22/59.30 [12]E(f3(x121,f2(x121)),x121)
% 59.22/59.30 [13]E(f3(f4(x131),x131),x131)
% 59.22/59.30 [16]E(f3(f3(x161,x162),x163),f3(x161,f3(x162,x163)))
% 59.22/59.30 [18]P1(x181)+~P1(f2(x181))
% 59.22/59.30 [19]P1(x191)+~P1(f4(x191))
% 59.22/59.30 [20]~P2(x201,x202)+E(x201,x202)
% 59.22/59.30 [22]P1(x221)+~P2(x221,x222)
% 59.22/59.30 [23]E(f4(x231),f2(x232))+~P1(f3(x232,x231))
% 59.22/59.30 [24]P1(f2(x241))+~P1(f3(x241,x242))
% 59.22/59.30 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 59.22/59.30 [25]~E(f4(x252),f2(x251))+~P1(f2(x251))+P1(f3(x251,x252))
% 59.22/59.30 [26]E(x261,x262)+~E(f3(x261,f3(a5,a6)),x263)+~E(f3(x262,f3(a5,a6)),x263)
% 59.22/59.30 %EqnAxiom
% 59.22/59.30 [1]E(x11,x11)
% 59.22/59.30 [2]E(x22,x21)+~E(x21,x22)
% 59.22/59.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.22/59.30 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 59.22/59.30 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 59.22/59.30 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 59.22/59.30 [7]~E(x71,x72)+E(f4(x71),f4(x72))
% 59.22/59.30 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 59.22/59.30 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93)
% 59.22/59.30 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101)
% 59.22/59.30
% 59.22/59.30 %-------------------------------------------
% 59.22/59.31 cnf(27,plain,
% 59.22/59.31 (~P1(x271)+P2(x271,x271)),
% 59.22/59.31 inference(equality_inference,[],[21])).
% 59.22/59.31 cnf(30,plain,
% 59.22/59.31 (E(f3(a7,a5),f3(a1,a5))),
% 59.22/59.31 inference(scs_inference,[],[17,14,20,2])).
% 59.22/59.31 cnf(31,plain,
% 59.22/59.31 (E(f4(a6),f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[17,14,15,20,2,23])).
% 59.22/59.31 cnf(33,plain,
% 59.22/59.31 (E(f3(f3(a1,a5),f2(f3(a1,a5))),f3(a7,a5))),
% 59.22/59.31 inference(scs_inference,[],[17,14,12,15,20,2,23,3])).
% 59.22/59.31 cnf(35,plain,
% 59.22/59.31 (P2(f3(a5,a6),x351)+~E(f3(a5,a6),x351)),
% 59.22/59.31 inference(scs_inference,[],[17,14,12,15,20,2,23,3,21])).
% 59.22/59.31 cnf(39,plain,
% 59.22/59.31 (P2(f3(a5,a6),f3(a5,a6))),
% 59.22/59.31 inference(equality_inference,[],[35])).
% 59.22/59.31 cnf(41,plain,
% 59.22/59.31 (E(f3(f4(f4(a6)),f4(a6)),f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[33,31,13,2,3])).
% 59.22/59.31 cnf(47,plain,
% 59.22/59.31 (E(f2(a5),f3(f4(f4(a6)),f4(a6)))),
% 59.22/59.31 inference(scs_inference,[],[41,2])).
% 59.22/59.31 cnf(48,plain,
% 59.22/59.31 (E(f3(f4(a6),f2(f4(a6))),f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[41,31,12,2,3])).
% 59.22/59.31 cnf(50,plain,
% 59.22/59.31 (P2(x501,f3(a5,a6))+~E(f3(a5,a6),x501)),
% 59.22/59.31 inference(scs_inference,[],[41,39,31,12,2,3,9])).
% 59.22/59.31 cnf(51,plain,
% 59.22/59.31 (~P1(f3(f4(f4(a6)),f4(a6)))+P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[41,39,31,12,2,3,9,8])).
% 59.22/59.31 cnf(53,plain,
% 59.22/59.31 (E(f2(a5),f3(f4(a6),f2(f4(a6))))),
% 59.22/59.31 inference(scs_inference,[],[48,2])).
% 59.22/59.31 cnf(54,plain,
% 59.22/59.31 (~E(a1,f3(f4(a7),a7))),
% 59.22/59.31 inference(scs_inference,[],[17,48,13,2,3])).
% 59.22/59.31 cnf(56,plain,
% 59.22/59.31 (~P2(a1,f3(f4(a7),a7))),
% 59.22/59.31 inference(scs_inference,[],[17,48,13,2,3,20])).
% 59.22/59.31 cnf(58,plain,
% 59.22/59.31 (~P1(f3(f4(a6),f2(f4(a6))))+P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[17,48,13,2,3,20,8])).
% 59.22/59.31 cnf(59,plain,
% 59.22/59.31 (~P2(f3(f4(a6),f2(f4(a6))),x591)+P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[17,48,13,2,3,20,8,22])).
% 59.22/59.31 cnf(61,plain,
% 59.22/59.31 (~E(f3(a5,a6),f3(f4(a6),f2(f4(a6))))+P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[17,48,39,15,13,2,3,20,8,22,25,21,10,9])).
% 59.22/59.31 cnf(62,plain,
% 59.22/59.31 (E(f3(x621,f3(x622,x623)),f3(f3(x621,x622),x623))),
% 59.22/59.31 inference(scs_inference,[],[16,2])).
% 59.22/59.31 cnf(63,plain,
% 59.22/59.31 (~E(a1,f3(a7,f2(a7)))),
% 59.22/59.31 inference(scs_inference,[],[17,16,12,2,3])).
% 59.22/59.31 cnf(65,plain,
% 59.22/59.31 (~P2(a1,f3(a7,f2(a7)))),
% 59.22/59.31 inference(scs_inference,[],[17,16,12,2,3,20])).
% 59.22/59.31 cnf(67,plain,
% 59.22/59.31 (~P1(f2(a5))+P1(f3(f4(f4(a6)),f4(a6)))),
% 59.22/59.31 inference(scs_inference,[],[17,47,16,12,2,3,20,8])).
% 59.22/59.31 cnf(76,plain,
% 59.22/59.31 (E(f2(a5),f4(a6))),
% 59.22/59.31 inference(scs_inference,[],[31,2])).
% 59.22/59.31 cnf(80,plain,
% 59.22/59.31 (~E(f3(a5,a6),f3(x801,f3(x802,x803)))+P1(f3(f3(x801,x802),x803))),
% 59.22/59.31 inference(scs_inference,[],[62,39,15,31,2,8,22,25,21,10,9])).
% 59.22/59.31 cnf(83,plain,
% 59.22/59.31 (E(x831,f3(f4(x831),x831))),
% 59.22/59.31 inference(scs_inference,[],[13,2])).
% 59.22/59.31 cnf(86,plain,
% 59.22/59.31 (P1(f3(f4(f3(a5,a6)),f3(a5,a6)))),
% 59.22/59.31 inference(scs_inference,[],[15,13,2,21,8])).
% 59.22/59.31 cnf(88,plain,
% 59.22/59.31 (E(x881,f3(x881,f2(x881)))),
% 59.22/59.31 inference(scs_inference,[],[12,2])).
% 59.22/59.31 cnf(100,plain,
% 59.22/59.31 (~P1(f2(a5))+P1(f4(a6))),
% 59.22/59.31 inference(scs_inference,[],[76,8])).
% 59.22/59.31 cnf(108,plain,
% 59.22/59.31 (~P2(f3(a5,a6),f3(f4(a6),f2(f4(a6))))+P1(f4(a6))),
% 59.22/59.31 inference(scs_inference,[],[76,15,8,59,24,58,61,22,51,20])).
% 59.22/59.31 cnf(120,plain,
% 59.22/59.31 (~P1(f2(a5))+P1(f3(f4(a6),f2(f4(a6))))),
% 59.22/59.31 inference(scs_inference,[],[53,8])).
% 59.22/59.31 cnf(132,plain,
% 59.22/59.31 (~P1(f4(a6))+P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[31,8])).
% 59.22/59.31 cnf(134,plain,
% 59.22/59.31 (~P2(f4(a6),x1341)+P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[31,8,108,22])).
% 59.22/59.31 cnf(146,plain,
% 59.22/59.31 (P1(x1461)+~P1(f2(f4(x1461)))),
% 59.22/59.31 inference(scs_inference,[],[18,19])).
% 59.22/59.31 cnf(147,plain,
% 59.22/59.31 (P1(f3(f4(a1),a1))),
% 59.22/59.31 inference(scs_inference,[],[11,83,8])).
% 59.22/59.31 cnf(149,plain,
% 59.22/59.31 (E(f4(a1),f2(f4(a1)))),
% 59.22/59.31 inference(scs_inference,[],[11,83,8,23])).
% 59.22/59.31 cnf(152,plain,
% 59.22/59.31 (E(f3(f4(f4(a1)),f4(a1)),f2(f4(a1)))),
% 59.22/59.31 inference(scs_inference,[],[11,83,13,8,23,2,3])).
% 59.22/59.31 cnf(155,plain,
% 59.22/59.31 (E(f2(f4(a1)),f3(f4(f4(a1)),f4(a1)))),
% 59.22/59.31 inference(scs_inference,[],[152,2])).
% 59.22/59.31 cnf(156,plain,
% 59.22/59.31 (P1(f3(a1,f2(a1)))),
% 59.22/59.31 inference(scs_inference,[],[11,88,152,2,8])).
% 59.22/59.31 cnf(158,plain,
% 59.22/59.31 (E(f4(f2(a1)),f2(a1))),
% 59.22/59.31 inference(scs_inference,[],[11,88,152,2,8,23])).
% 59.22/59.31 cnf(160,plain,
% 59.22/59.31 (P1(f4(a6))),
% 59.22/59.31 inference(scs_inference,[],[15,100,24])).
% 59.22/59.31 cnf(161,plain,
% 59.22/59.31 (P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[160,132])).
% 59.22/59.31 cnf(162,plain,
% 59.22/59.31 (P1(a6)),
% 59.22/59.31 inference(scs_inference,[],[160,19])).
% 59.22/59.31 cnf(164,plain,
% 59.22/59.31 (E(f2(a1),f4(f2(a1)))),
% 59.22/59.31 inference(scs_inference,[],[158,160,19,2])).
% 59.22/59.31 cnf(165,plain,
% 59.22/59.31 (P2(f4(a6),f3(f4(f4(a6)),f4(a6)))),
% 59.22/59.31 inference(scs_inference,[],[83,158,160,19,2,21])).
% 59.22/59.31 cnf(168,plain,
% 59.22/59.31 (E(f3(f4(f2(a1)),f2(a1)),f4(f2(a1)))),
% 59.22/59.31 inference(scs_inference,[],[83,13,158,160,19,2,21,3])).
% 59.22/59.31 cnf(170,plain,
% 59.22/59.31 (~P1(f2(f4(a1)))+P1(f3(f4(f4(a1)),f4(a1)))),
% 59.22/59.31 inference(scs_inference,[],[83,155,13,158,160,19,2,21,3,8])).
% 59.22/59.31 cnf(177,plain,
% 59.22/59.31 (P1(f3(f4(f4(a6)),f4(a6)))),
% 59.22/59.31 inference(scs_inference,[],[161,67])).
% 59.22/59.31 cnf(178,plain,
% 59.22/59.31 (P1(f3(f4(a6),f2(f4(a6))))),
% 59.22/59.31 inference(scs_inference,[],[161,120])).
% 59.22/59.31 cnf(179,plain,
% 59.22/59.31 (P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[165,134])).
% 59.22/59.31 cnf(180,plain,
% 59.22/59.31 (~P1(f2(f4(f3(x1801,x1802))))+E(f4(x1802),f2(x1801))),
% 59.22/59.31 inference(scs_inference,[],[146,23])).
% 59.22/59.31 cnf(181,plain,
% 59.22/59.31 (P1(f2(a5))),
% 59.22/59.31 inference(scs_inference,[],[177,51])).
% 59.22/59.31 cnf(187,plain,
% 59.22/59.31 (P1(a5)),
% 59.22/59.31 inference(scs_inference,[],[161,18])).
% 59.22/59.31 cnf(189,plain,
% 59.22/59.31 (E(f4(f2(a1)),f3(f4(f2(a1)),f2(a1)))),
% 59.22/59.31 inference(scs_inference,[],[168,161,18,2])).
% 59.22/59.31 cnf(190,plain,
% 59.22/59.31 (P2(f2(a5),f3(f2(a5),f2(f2(a5))))),
% 59.22/59.31 inference(scs_inference,[],[88,168,161,18,2,21])).
% 59.22/59.31 cnf(202,plain,
% 59.22/59.31 (P2(f4(a6),f3(f4(a6),f2(f4(a6))))),
% 59.22/59.31 inference(scs_inference,[],[88,160,21])).
% 59.22/59.31 cnf(205,plain,
% 59.22/59.31 (~P1(f2(a1))+P1(f4(f2(a1)))),
% 59.22/59.31 inference(scs_inference,[],[88,164,160,21,8])).
% 59.22/59.31 cnf(216,plain,
% 59.22/59.31 (~P1(f4(f2(a1)))+P1(f3(f4(f2(a1)),f2(a1)))),
% 59.22/59.31 inference(scs_inference,[],[83,189,179,21,8])).
% 59.22/59.31 cnf(224,plain,
% 59.22/59.31 (P2(a6,f3(a6,f2(a6)))),
% 59.22/59.31 inference(scs_inference,[],[88,162,21])).
% 59.22/59.31 cnf(225,plain,
% 59.22/59.31 (E(x2251,f3(x2251,f2(x2251)))),
% 59.22/59.31 inference(rename_variables,[],[88])).
% 59.22/59.31 cnf(229,plain,
% 59.22/59.31 (~P1(f3(f4(f4(a1)),f4(a1)))+P1(f2(f4(a1)))),
% 59.22/59.31 inference(scs_inference,[],[88,225,152,162,21,9,8])).
% 59.22/59.31 cnf(236,plain,
% 59.22/59.31 (P2(a5,f3(f4(a5),a5))),
% 59.22/59.31 inference(scs_inference,[],[83,187,21])).
% 59.22/59.31 cnf(237,plain,
% 59.22/59.31 (E(x2371,f3(f4(x2371),x2371))),
% 59.22/59.31 inference(rename_variables,[],[83])).
% 59.22/59.31 cnf(239,plain,
% 59.22/59.31 (P2(f3(f4(a6),a6),f3(a6,f2(a6)))),
% 59.22/59.31 inference(scs_inference,[],[83,237,224,187,21,9])).
% 59.22/59.31 cnf(241,plain,
% 59.22/59.31 (~P1(f4(a1))+P1(f2(f4(a1)))),
% 59.22/59.31 inference(scs_inference,[],[83,237,224,149,187,21,9,8])).
% 59.22/59.31 cnf(248,plain,
% 59.22/59.31 (P2(a5,f3(a5,f2(a5)))),
% 59.22/59.31 inference(scs_inference,[],[88,187,21])).
% 59.22/59.31 cnf(253,plain,
% 59.22/59.31 (P2(f3(a5,f2(a5)),f3(a5,f2(a5)))),
% 59.22/59.31 inference(scs_inference,[],[88,248,9])).
% 59.22/59.31 cnf(255,plain,
% 59.22/59.31 (P2(a6,f3(f4(a6),a6))),
% 59.22/59.31 inference(scs_inference,[],[83,162,21])).
% 59.22/59.31 cnf(256,plain,
% 59.22/59.31 (E(x2561,f3(f4(x2561),x2561))),
% 59.22/59.32 inference(rename_variables,[],[83])).
% 59.22/59.32 cnf(258,plain,
% 59.22/59.32 (P2(f3(f4(a5),a5),f3(a5,f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[83,256,248,162,21,9])).
% 59.22/59.32 cnf(265,plain,
% 59.22/59.32 (P2(f3(a1,f2(a1)),a1)),
% 59.22/59.32 inference(scs_inference,[],[12,156,21])).
% 59.22/59.32 cnf(266,plain,
% 59.22/59.32 (E(f3(x2661,f2(x2661)),x2661)),
% 59.22/59.32 inference(rename_variables,[],[12])).
% 59.22/59.32 cnf(268,plain,
% 59.22/59.32 (P2(f2(a5),f2(a5))),
% 59.22/59.32 inference(scs_inference,[],[12,266,190,156,21,10])).
% 59.22/59.32 cnf(269,plain,
% 59.22/59.32 (E(f3(x2691,f2(x2691)),x2691)),
% 59.22/59.32 inference(rename_variables,[],[12])).
% 59.22/59.32 cnf(271,plain,
% 59.22/59.32 (E(f3(x2711,f2(x2711)),x2711)),
% 59.22/59.32 inference(rename_variables,[],[12])).
% 59.22/59.32 cnf(272,plain,
% 59.22/59.32 (P2(a1,a1)),
% 59.22/59.32 inference(scs_inference,[],[12,266,269,271,30,190,156,21,10,3,9])).
% 59.22/59.32 cnf(282,plain,
% 59.22/59.32 (E(f3(x2821,f2(x2821)),x2821)),
% 59.22/59.32 inference(rename_variables,[],[12])).
% 59.22/59.32 cnf(284,plain,
% 59.22/59.32 (P2(f4(a6),f4(a6))),
% 59.22/59.32 inference(scs_inference,[],[12,282,202,178,21,10])).
% 59.22/59.32 cnf(285,plain,
% 59.22/59.32 (E(f3(x2851,f2(x2851)),x2851)),
% 59.22/59.32 inference(rename_variables,[],[12])).
% 59.22/59.32 cnf(288,plain,
% 59.22/59.32 (P2(f3(f2(a5),f2(f2(a5))),f2(a5))),
% 59.22/59.32 inference(scs_inference,[],[12,282,285,88,76,202,178,268,21,10,3,9])).
% 59.22/59.32 cnf(299,plain,
% 59.22/59.32 (P2(f3(a1,f2(a1)),f3(f4(a1),a1))),
% 59.22/59.32 inference(scs_inference,[],[83,265,10])).
% 59.22/59.32 cnf(308,plain,
% 59.22/59.32 (P2(f3(a1,f2(a1)),f3(a1,f2(a1)))),
% 59.22/59.32 inference(scs_inference,[],[88,265,10])).
% 59.22/59.32 cnf(313,plain,
% 59.22/59.32 (E(f3(x3131,f2(x3131)),x3131)),
% 59.22/59.32 inference(rename_variables,[],[12])).
% 59.22/59.32 cnf(314,plain,
% 59.22/59.32 (P2(a1,f3(a1,f2(a1)))),
% 59.22/59.32 inference(scs_inference,[],[12,313,248,308,10,9])).
% 59.22/59.32 cnf(318,plain,
% 59.22/59.32 (P2(f3(f4(f4(a6)),f4(a6)),f4(a6))),
% 59.22/59.32 inference(scs_inference,[],[12,83,253,284,10,9])).
% 59.22/59.32 cnf(320,plain,
% 59.22/59.32 (P2(f3(f4(a5),a5),a5)),
% 59.22/59.32 inference(scs_inference,[],[12,258,10])).
% 59.22/59.32 cnf(322,plain,
% 59.22/59.32 (P2(f3(f4(a6),a6),a6)),
% 59.22/59.32 inference(scs_inference,[],[12,239,10])).
% 59.22/59.32 cnf(327,plain,
% 59.22/59.32 (~E(f3(a1,f2(a1)),f3(a7,f2(a7)))),
% 59.22/59.32 inference(scs_inference,[],[65,314,10])).
% 59.22/59.32 cnf(328,plain,
% 59.22/59.32 (~P2(f3(a1,f2(a1)),f3(a7,f2(a7)))),
% 59.22/59.32 inference(scs_inference,[],[65,314,10,20])).
% 59.22/59.32 cnf(330,plain,
% 59.22/59.32 (~E(f3(f4(a1),a1),f3(a7,f2(a7)))),
% 59.22/59.32 inference(scs_inference,[],[328,299,10])).
% 59.22/59.32 cnf(336,plain,
% 59.22/59.32 (E(f2(x3361),f2(f3(x3361,f2(x3361))))),
% 59.22/59.32 inference(scs_inference,[],[12,4,2])).
% 59.22/59.32 cnf(343,plain,
% 59.22/59.32 (E(f4(f2(a5)),f2(a5))),
% 59.22/59.32 inference(scs_inference,[],[56,181,336,314,2,10,8,18,23])).
% 59.22/59.32 cnf(347,plain,
% 59.22/59.32 (E(f2(a5),f4(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[343,2])).
% 59.22/59.32 cnf(360,plain,
% 59.22/59.32 (E(f3(f4(f2(a5)),f2(a5)),f4(a6))),
% 59.22/59.32 inference(scs_inference,[],[13,76,3])).
% 59.22/59.32 cnf(362,plain,
% 59.22/59.32 (E(f4(a6),f3(f4(f2(a5)),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[13,76,3,2])).
% 59.22/59.32 cnf(373,plain,
% 59.22/59.32 (P1(f3(f4(f2(a5)),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[13,347,362,160,3,8])).
% 59.22/59.32 cnf(374,plain,
% 59.22/59.32 (E(f4(f2(a5)),f3(f4(f2(a5)),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[13,347,362,160,3,8,2])).
% 59.22/59.32 cnf(406,plain,
% 59.22/59.32 (E(f3(f4(f4(a6)),f4(a6)),f4(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[41,347,3])).
% 59.22/59.32 cnf(407,plain,
% 59.22/59.32 (E(f4(f2(a5)),f3(f4(f4(a6)),f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[41,347,3,2])).
% 59.22/59.32 cnf(412,plain,
% 59.22/59.32 (E(f3(x4121,f3(x4122,f2(x4122))),f3(x4121,x4122))),
% 59.22/59.32 inference(scs_inference,[],[88,6,2])).
% 59.22/59.32 cnf(413,plain,
% 59.22/59.32 (E(f3(x4131,x4132),f3(x4131,f3(x4132,f2(x4132))))),
% 59.22/59.32 inference(scs_inference,[],[412,2])).
% 59.22/59.32 cnf(415,plain,
% 59.22/59.32 (P1(f3(f3(a5,a6),f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[15,412,2,8,80])).
% 59.22/59.32 cnf(419,plain,
% 59.22/59.32 (E(f4(f3(a6,f2(a6))),f2(a5))),
% 59.22/59.32 inference(scs_inference,[],[15,412,2,8,80,50,35,23])).
% 59.22/59.32 cnf(422,plain,
% 59.22/59.32 (E(f4(f2(a6)),f2(f3(a5,a6)))),
% 59.22/59.32 inference(scs_inference,[],[415,23])).
% 59.22/59.32 cnf(426,plain,
% 59.22/59.32 (P1(f3(a6,f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[179,415,419,23,2,8,19])).
% 59.22/59.32 cnf(429,plain,
% 59.22/59.32 (E(f4(f2(a6)),f2(a6))),
% 59.22/59.32 inference(scs_inference,[],[426,23])).
% 59.22/59.32 cnf(431,plain,
% 59.22/59.32 (E(f2(f3(a5,a6)),f4(f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[426,422,23,2])).
% 59.22/59.32 cnf(441,plain,
% 59.22/59.32 (~P1(f2(f3(a5,a6)))+P1(f4(f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[431,429,2,3,8])).
% 59.22/59.32 cnf(494,plain,
% 59.22/59.32 (P1(f4(f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[415,441,24])).
% 59.22/59.32 cnf(497,plain,
% 59.22/59.32 (P1(f2(a6))),
% 59.22/59.32 inference(scs_inference,[],[494,19])).
% 59.22/59.32 cnf(521,plain,
% 59.22/59.32 (P2(f4(a6),f2(a5))),
% 59.22/59.32 inference(scs_inference,[],[31,160,21])).
% 59.22/59.32 cnf(536,plain,
% 59.22/59.32 (E(x5361,f3(f4(x5361),x5361))),
% 59.22/59.32 inference(rename_variables,[],[83])).
% 59.22/59.32 cnf(538,plain,
% 59.22/59.32 (E(x5381,f3(f4(x5381),f3(x5381,f2(x5381))))),
% 59.22/59.32 inference(scs_inference,[],[83,536,413,497,21,3])).
% 59.22/59.32 cnf(541,plain,
% 59.22/59.32 (E(x5411,f3(f4(x5411),x5411))),
% 59.22/59.32 inference(rename_variables,[],[83])).
% 59.22/59.32 cnf(542,plain,
% 59.22/59.32 (P2(f3(f4(a1),a1),a1)),
% 59.22/59.32 inference(scs_inference,[],[83,536,541,413,521,272,497,21,3,10,9])).
% 59.22/59.32 cnf(546,plain,
% 59.22/59.32 (~E(a1,f3(f4(a7),f3(a7,f2(a7))))),
% 59.22/59.32 inference(scs_inference,[],[17,538,2,3])).
% 59.22/59.32 cnf(548,plain,
% 59.22/59.32 (P2(f2(a5),f4(a6))),
% 59.22/59.32 inference(scs_inference,[],[31,17,538,284,318,2,3,10,9])).
% 59.22/59.32 cnf(560,plain,
% 59.22/59.32 (~P2(a1,f3(f3(f4(a7),a7),f2(a7)))),
% 59.22/59.32 inference(scs_inference,[],[88,546,16,548,3,9,20])).
% 59.22/59.32 cnf(571,plain,
% 59.22/59.32 (~P1(f2(f4(f3(x5711,x5712))))+E(f2(f4(x5712)),f2(f2(x5711)))),
% 59.22/59.32 inference(scs_inference,[],[180,4])).
% 59.22/59.32 cnf(602,plain,
% 59.22/59.32 (P1(f3(f4(a1),f3(a1,f2(a1))))),
% 59.22/59.32 inference(scs_inference,[],[147,413,8])).
% 59.22/59.32 cnf(614,plain,
% 59.22/59.32 (E(f4(a6),f2(f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[162,83,8,23])).
% 59.22/59.32 cnf(618,plain,
% 59.22/59.32 (P1(f3(f4(a6),f3(a6,f2(a6))))),
% 59.22/59.32 inference(scs_inference,[],[162,538,8])).
% 59.22/59.32 cnf(621,plain,
% 59.22/59.32 (P1(f2(f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[160,614,8])).
% 59.22/59.32 cnf(637,plain,
% 59.22/59.32 (P1(f3(f4(a5),a5))),
% 59.22/59.32 inference(scs_inference,[],[187,83,8])).
% 59.22/59.32 cnf(639,plain,
% 59.22/59.32 (E(f4(a5),f2(f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[187,83,8,23])).
% 59.22/59.32 cnf(641,plain,
% 59.22/59.32 (E(f2(f4(a5)),f4(a5))),
% 59.22/59.32 inference(scs_inference,[],[187,83,8,23,2])).
% 59.22/59.32 cnf(643,plain,
% 59.22/59.32 (P1(f3(f4(a5),f3(a5,f2(a5))))),
% 59.22/59.32 inference(scs_inference,[],[187,538,8])).
% 59.22/59.32 cnf(646,plain,
% 59.22/59.32 (~P1(f4(a5))+P1(f2(f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[639,8])).
% 59.22/59.32 cnf(726,plain,
% 59.22/59.32 (E(f3(f4(f2(a5)),f2(a5)),f2(f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[360,614,3])).
% 59.22/59.32 cnf(737,plain,
% 59.22/59.32 (E(f4(f2(a5)),f2(f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[374,726,3])).
% 59.22/59.32 cnf(741,plain,
% 59.22/59.32 (E(f3(f4(f4(a6)),f4(a6)),f2(f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[406,737,3])).
% 59.22/59.32 cnf(774,plain,
% 59.22/59.32 (P2(a6,f3(f4(a6),f3(a6,f2(a6))))),
% 59.22/59.32 inference(scs_inference,[],[413,255,10])).
% 59.22/59.32 cnf(775,plain,
% 59.22/59.32 (E(f3(x7751,x7752),f3(x7751,f3(x7752,f2(x7752))))),
% 59.22/59.32 inference(rename_variables,[],[413])).
% 59.22/59.32 cnf(776,plain,
% 59.22/59.32 (P2(f3(f4(a5),f3(a5,f2(a5))),a5)),
% 59.22/59.32 inference(scs_inference,[],[413,775,255,320,10,9])).
% 59.22/59.32 cnf(779,plain,
% 59.22/59.32 (P2(a5,f3(f4(a5),f3(a5,f2(a5))))),
% 59.22/59.32 inference(scs_inference,[],[413,236,10])).
% 59.22/59.32 cnf(780,plain,
% 59.22/59.32 (E(f3(x7801,x7802),f3(x7801,f3(x7802,f2(x7802))))),
% 59.22/59.32 inference(rename_variables,[],[413])).
% 59.22/59.32 cnf(781,plain,
% 59.22/59.32 (P2(f3(f4(a6),f3(a6,f2(a6))),a6)),
% 59.22/59.32 inference(scs_inference,[],[413,780,236,322,10,9])).
% 59.22/59.32 cnf(784,plain,
% 59.22/59.32 (P2(f3(f4(a1),f3(a1,f2(a1))),a1)),
% 59.22/59.32 inference(scs_inference,[],[413,542,9])).
% 59.22/59.32 cnf(834,plain,
% 59.22/59.32 (P1(f3(f2(a6),f2(f2(a6))))),
% 59.22/59.32 inference(scs_inference,[],[497,88,8])).
% 59.22/59.32 cnf(837,plain,
% 59.22/59.32 (P1(f3(f4(f2(a6)),f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[497,83,8])).
% 59.22/59.32 cnf(860,plain,
% 59.22/59.32 (~E(f3(a1,f2(a1)),f3(f3(f4(a7),a7),f2(a7)))),
% 59.22/59.32 inference(scs_inference,[],[560,314,10])).
% 59.22/59.32 cnf(870,plain,
% 59.22/59.32 (P1(f3(f3(f4(a1),a1),f2(a1)))),
% 59.22/59.32 inference(scs_inference,[],[602,62,8])).
% 59.22/59.32 cnf(885,plain,
% 59.22/59.32 (P1(f3(f3(f4(a6),a6),f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[618,62,8])).
% 59.22/59.32 cnf(887,plain,
% 59.22/59.32 (P1(f3(f3(f4(a5),a5),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[643,62,8])).
% 59.22/59.32 cnf(894,plain,
% 59.22/59.32 (~P1(f2(f2(f4(a6))))+P1(f3(f4(a6),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[737,18,25])).
% 59.22/59.32 cnf(898,plain,
% 59.22/59.32 (P1(f4(a1))+~P1(f3(f4(f4(a1)),f4(a1)))),
% 59.22/59.32 inference(scs_inference,[],[18,229])).
% 59.22/59.32 cnf(905,plain,
% 59.22/59.32 (P1(f4(a1))+~P1(f4(a1))),
% 59.22/59.32 inference(scs_inference,[],[18,241])).
% 59.22/59.32 cnf(939,plain,
% 59.22/59.32 (E(f2(f4(a5)),f3(f4(f4(a5)),f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[13,639,3,2])).
% 59.22/59.32 cnf(940,plain,
% 59.22/59.32 (~P1(f3(f4(f4(a5)),f4(a5)))+P1(f2(f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[13,639,3,2,8])).
% 59.22/59.32 cnf(947,plain,
% 59.22/59.32 (~P1(f2(f4(a5)))+P1(f3(f4(f4(a5)),f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[939,8])).
% 59.22/59.32 cnf(1112,plain,
% 59.22/59.32 (P2(a5,f3(f3(f4(a5),a5),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[62,779,10])).
% 59.22/59.32 cnf(1113,plain,
% 59.22/59.32 (E(f3(x11131,f3(x11132,x11133)),f3(f3(x11131,x11132),x11133))),
% 59.22/59.32 inference(rename_variables,[],[62])).
% 59.22/59.32 cnf(1114,plain,
% 59.22/59.32 (P2(f3(f3(f4(a5),a5),f2(a5)),a5)),
% 59.22/59.32 inference(scs_inference,[],[62,1113,779,776,10,9])).
% 59.22/59.32 cnf(1117,plain,
% 59.22/59.32 (P2(a6,f3(f3(f4(a6),a6),f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[62,774,10])).
% 59.22/59.32 cnf(1118,plain,
% 59.22/59.32 (E(f3(x11181,f3(x11182,x11183)),f3(f3(x11181,x11182),x11183))),
% 59.22/59.32 inference(rename_variables,[],[62])).
% 59.22/59.32 cnf(1119,plain,
% 59.22/59.32 (P2(f3(f3(f4(a6),a6),f2(a6)),a6)),
% 59.22/59.32 inference(scs_inference,[],[62,1118,774,781,10,9])).
% 59.22/59.32 cnf(1122,plain,
% 59.22/59.32 (P2(f3(f3(f4(a6),a6),f2(a6)),f3(a6,f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[88,1119,10])).
% 59.22/59.32 cnf(1124,plain,
% 59.22/59.32 (P2(f3(f3(f4(a1),a1),f2(a1)),a1)),
% 59.22/59.32 inference(scs_inference,[],[62,88,784,1119,10,9])).
% 59.22/59.32 cnf(1127,plain,
% 59.22/59.32 (P2(f3(f3(f4(a1),a1),f2(a1)),f3(a1,f2(a1)))),
% 59.22/59.32 inference(scs_inference,[],[88,1124,10])).
% 59.22/59.32 cnf(1128,plain,
% 59.22/59.32 (E(x11281,f3(x11281,f2(x11281)))),
% 59.22/59.32 inference(rename_variables,[],[88])).
% 59.22/59.32 cnf(1129,plain,
% 59.22/59.32 (P2(f3(a6,f2(a6)),f3(f3(f4(a6),a6),f2(a6)))),
% 59.22/59.32 inference(scs_inference,[],[88,1128,1124,1117,10,9])).
% 59.22/59.32 cnf(1131,plain,
% 59.22/59.32 (P2(f3(f3(f4(a5),a5),f2(a5)),f3(a5,f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[88,1114,10])).
% 59.22/59.32 cnf(1132,plain,
% 59.22/59.32 (E(x11321,f3(x11321,f2(x11321)))),
% 59.22/59.32 inference(rename_variables,[],[88])).
% 59.22/59.32 cnf(1133,plain,
% 59.22/59.32 (P2(f3(a5,f2(a5)),f3(f3(f4(a5),a5),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[88,1132,1114,1112,10,9])).
% 59.22/59.32 cnf(1145,plain,
% 59.22/59.32 (P2(f3(f3(f4(a6),a6),f2(a6)),f3(f4(a6),a6))),
% 59.22/59.32 inference(scs_inference,[],[83,1119,10])).
% 59.22/59.32 cnf(1150,plain,
% 59.22/59.32 (P2(f3(f3(f4(a5),a5),f2(a5)),f3(f4(a5),a5))),
% 59.22/59.32 inference(scs_inference,[],[83,1114,10])).
% 59.22/59.32 cnf(1488,plain,
% 59.22/59.32 (E(f3(f3(x14881,f2(x14881)),x14882),f3(x14881,x14882))),
% 59.22/59.32 inference(scs_inference,[],[88,2,5])).
% 59.22/59.32 cnf(1489,plain,
% 59.22/59.32 (E(f3(x14891,x14892),f3(f3(x14891,f2(x14891)),x14892))),
% 59.22/59.32 inference(scs_inference,[],[1488,2])).
% 59.22/59.32 cnf(1490,plain,
% 59.22/59.32 (~E(a1,f3(f3(a7,f2(a7)),f2(a7)))),
% 59.22/59.32 inference(scs_inference,[],[63,1488,2,3])).
% 59.22/59.32 cnf(1589,plain,
% 59.22/59.32 (~P2(a7,a1)),
% 59.22/59.32 inference(scs_inference,[],[17,2,20])).
% 59.22/59.32 cnf(1590,plain,
% 59.22/59.32 (~E(f3(f3(f4(a1),a1),f2(a1)),a7)),
% 59.22/59.32 inference(scs_inference,[],[1589,1124,9])).
% 59.22/59.32 cnf(1591,plain,
% 59.22/59.32 (~P2(f3(f3(f4(a1),a1),f2(a1)),a7)),
% 59.22/59.32 inference(scs_inference,[],[1589,1124,9,20])).
% 59.22/59.32 cnf(1627,plain,
% 59.22/59.32 (P1(f3(f4(f4(a1)),f4(a1)))),
% 59.22/59.32 inference(scs_inference,[],[147,24,170])).
% 59.22/59.32 cnf(1629,plain,
% 59.22/59.32 (P1(f4(a1))),
% 59.22/59.32 inference(scs_inference,[],[1627,898])).
% 59.22/59.32 cnf(1630,plain,
% 59.22/59.32 (P1(f2(f4(a1)))),
% 59.22/59.32 inference(scs_inference,[],[1629,241])).
% 59.22/59.32 cnf(1636,plain,
% 59.22/59.32 (P1(f4(a1))),
% 59.22/59.32 inference(scs_inference,[],[1629,905])).
% 59.22/59.32 cnf(1642,plain,
% 59.22/59.32 (P1(f4(f2(a1)))),
% 59.22/59.32 inference(scs_inference,[],[156,24,205])).
% 59.22/59.32 cnf(1643,plain,
% 59.22/59.32 (P1(f3(f4(f2(a1)),f2(a1)))),
% 59.22/59.32 inference(scs_inference,[],[1642,216])).
% 59.22/59.32 cnf(1644,plain,
% 59.22/59.32 (P1(f2(a1))),
% 59.22/59.32 inference(scs_inference,[],[1642,19])).
% 59.22/59.32 cnf(1652,plain,
% 59.22/59.32 (P1(f2(f2(f4(a6))))),
% 59.22/59.32 inference(scs_inference,[],[88,621,24,8])).
% 59.22/59.32 cnf(1653,plain,
% 59.22/59.32 (P1(f3(f4(a6),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[1652,894])).
% 59.22/59.32 cnf(1654,plain,
% 59.22/59.32 (E(f2(f4(a6)),f2(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[86,24,571])).
% 59.22/59.32 cnf(1656,plain,
% 59.22/59.32 (P1(f2(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[621,1654,2,8])).
% 59.22/59.32 cnf(1657,plain,
% 59.22/59.32 (P1(f3(f4(f4(a5)),f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[637,24,947])).
% 59.22/59.32 cnf(1658,plain,
% 59.22/59.32 (P1(f2(f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[1657,940])).
% 59.22/59.32 cnf(1660,plain,
% 59.22/59.32 (P1(f4(a5))),
% 59.22/59.32 inference(scs_inference,[],[1658,18])).
% 59.22/59.32 cnf(1665,plain,
% 59.22/59.32 (P1(f2(f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[1660,646])).
% 59.22/59.32 cnf(1669,plain,
% 59.22/59.32 (P2(f4(a5),f2(f4(a5)))),
% 59.22/59.32 inference(scs_inference,[],[639,1660,21])).
% 59.22/59.32 cnf(1677,plain,
% 59.22/59.32 (P2(f3(f4(a5),f2(f4(a5))),f4(a5))),
% 59.22/59.32 inference(scs_inference,[],[641,88,1669,1665,21,10,9])).
% 59.22/59.32 cnf(1689,plain,
% 59.22/59.32 (E(f3(f4(f2(a5)),f2(a5)),f2(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[726,1654,3])).
% 59.22/59.32 cnf(1693,plain,
% 59.22/59.32 (E(f2(f2(a5)),f2(a5))),
% 59.22/59.32 inference(scs_inference,[],[83,1689,3,2])).
% 59.22/59.32 cnf(1697,plain,
% 59.22/59.32 (E(f4(f2(a5)),f2(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[737,1654,3])).
% 59.22/59.32 cnf(1698,plain,
% 59.22/59.32 (E(f2(f2(a5)),f4(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[737,1654,3,2])).
% 59.22/59.32 cnf(1700,plain,
% 59.22/59.32 (E(f3(f4(f4(a6)),f4(a6)),f2(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[741,1654,3])).
% 59.22/59.32 cnf(1703,plain,
% 59.22/59.32 (E(f4(a6),f2(f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[83,1700,3])).
% 59.22/59.32 cnf(1705,plain,
% 59.22/59.32 (E(f2(f2(a5)),f4(a6))),
% 59.22/59.32 inference(scs_inference,[],[83,1700,3,2])).
% 59.22/59.32 cnf(1728,plain,
% 59.22/59.32 (~E(a7,a1)),
% 59.22/59.32 inference(scs_inference,[],[17,1636,1693,1643,1677,1122,27,4,7,5,6,24,22,20,2])).
% 59.22/59.32 cnf(1729,plain,
% 59.22/59.32 (~E(f3(a1,f3(a5,a6)),f3(f3(a7,f2(a7)),f3(a5,a6)))),
% 59.22/59.32 inference(scs_inference,[],[17,1636,1693,1643,1677,1122,1489,27,4,7,5,6,24,22,20,2,26])).
% 59.22/59.32 cnf(1732,plain,
% 59.22/59.32 (P1(f3(f2(a5),a6))),
% 59.22/59.32 inference(scs_inference,[],[17,1636,1693,1703,1656,1643,1677,1122,1489,27,4,7,5,6,24,22,20,2,26,25])).
% 59.22/59.32 cnf(1743,plain,
% 59.22/59.32 (E(f3(f2(a5),x17431),f3(f4(a6),x17431))),
% 59.22/59.32 inference(scs_inference,[],[1644,76,27,5])).
% 59.22/59.32 cnf(1745,plain,
% 59.22/59.32 (E(f3(x17451,f2(a5)),f3(x17451,f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[1644,76,14,27,5,4,6])).
% 59.22/59.32 cnf(1746,plain,
% 59.22/59.32 (E(f4(f2(a5)),f4(f4(a6)))),
% 59.22/59.32 inference(scs_inference,[],[1644,76,14,27,5,4,6,7])).
% 59.22/59.32 cnf(1753,plain,
% 59.22/59.32 (E(f3(f3(x17531,f2(x17531)),x17532),f3(x17531,x17532))),
% 59.22/59.32 inference(rename_variables,[],[1488])).
% 59.22/59.32 cnf(1755,plain,
% 59.22/59.32 (P1(f3(f2(a5),f2(a5)))),
% 59.22/59.32 inference(scs_inference,[],[1644,1490,1697,1657,1127,327,1656,1488,76,14,27,5,4,6,7,24,20,2,26,25])).
% 59.22/59.32 cnf(1757,plain,
% 59.22/59.33 (~E(f3(a7,f2(a7)),a1)),
% 59.22/59.33 inference(scs_inference,[],[1644,1490,1697,1657,1127,327,1656,1488,1753,76,14,27,5,4,6,7,24,20,2,26,25,3])).
% 59.22/59.33 cnf(1767,plain,
% 59.22/59.33 (E(f3(f3(a1,a5),x17671),f3(f3(a7,a5),x17671))),
% 59.22/59.33 inference(scs_inference,[],[1630,14,27,5])).
% 59.22/59.33 cnf(1768,plain,
% 59.22/59.33 (E(f3(x17681,f3(a1,a5)),f3(x17681,f3(a7,a5)))),
% 59.22/59.33 inference(scs_inference,[],[1630,14,27,5,6])).
% 59.22/59.33 cnf(1776,plain,
% 59.22/59.33 (~E(f3(f3(f4(a1),a1),f3(a5,a6)),f3(a7,f3(a5,a6)))),
% 59.22/59.33 inference(scs_inference,[],[1630,1590,870,1129,330,1488,14,30,27,5,6,4,7,24,20,2,26])).
% 59.22/59.33 cnf(1779,plain,
% 59.22/59.33 (E(f2(f2(a5)),f4(f4(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1630,1590,1698,870,1746,1129,330,1488,14,30,27,5,6,4,7,24,20,2,26,3])).
% 59.22/59.33 cnf(1782,plain,
% 59.22/59.33 (P2(f3(f4(a6),f2(f2(a5))),f2(a5))),
% 59.22/59.33 inference(scs_inference,[],[1630,1590,1591,1698,870,1743,1746,288,1129,330,1488,14,30,12,27,5,6,4,7,24,20,2,26,3,10,9])).
% 59.22/59.33 cnf(1784,plain,
% 59.22/59.33 (~E(f3(f3(f4(a1),a1),f2(a1)),f3(a7,f2(a7)))),
% 59.22/59.33 inference(scs_inference,[],[1630,1590,1591,1698,870,1743,1746,288,1129,330,1488,14,30,12,27,5,6,4,7,24,20,2,26,3,10,9,21])).
% 59.22/59.33 cnf(1793,plain,
% 59.22/59.33 (E(f3(f3(a7,a5),x17931),f3(f3(a1,a5),x17931))),
% 59.22/59.33 inference(scs_inference,[],[1653,30,27,5])).
% 59.22/59.33 cnf(1795,plain,
% 59.22/59.33 (E(f3(x17951,f3(a7,a5)),f3(x17951,f3(a1,a5)))),
% 59.22/59.33 inference(scs_inference,[],[1653,30,13,27,5,4,6])).
% 59.22/59.33 cnf(1807,plain,
% 59.22/59.33 (P2(f2(f2(a5)),f4(a6))),
% 59.22/59.33 inference(scs_inference,[],[1728,1705,1653,885,1782,1784,1656,1489,30,13,27,5,4,6,7,24,22,20,2,26,21])).
% 59.22/59.33 cnf(1813,plain,
% 59.22/59.33 (E(f3(x18131,f2(a5)),f3(x18131,f4(a6)))),
% 59.22/59.33 inference(rename_variables,[],[1745])).
% 59.22/59.33 cnf(1814,plain,
% 59.22/59.33 (P2(f3(f3(f4(a5),a5),f4(a6)),f3(a5,f2(a5)))),
% 59.22/59.33 inference(scs_inference,[],[1728,1705,1653,1767,1768,885,1745,1813,1782,1131,1784,1656,1489,30,13,27,5,4,6,7,24,22,20,2,26,21,3,10,9])).
% 59.22/59.33 cnf(1815,plain,
% 59.22/59.33 (E(f3(x18151,f2(a5)),f3(x18151,f4(a6)))),
% 59.22/59.33 inference(rename_variables,[],[1745])).
% 59.22/59.33 cnf(1816,plain,
% 59.22/59.33 (P1(f3(f4(a6),f4(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1728,1705,1653,1767,1768,885,1745,1813,1815,1782,1131,1784,1656,1489,30,13,27,5,4,6,7,24,22,20,2,26,21,3,10,9,8])).
% 59.22/59.33 cnf(1821,plain,
% 59.22/59.33 (E(f3(f4(a6),x18211),f3(f2(a5),x18211))),
% 59.22/59.33 inference(scs_inference,[],[1755,31,27,5])).
% 59.22/59.33 cnf(1822,plain,
% 59.22/59.33 (E(f3(x18221,f4(a6)),f3(x18221,f2(a5)))),
% 59.22/59.33 inference(scs_inference,[],[1755,31,27,5,6])).
% 59.22/59.33 cnf(1823,plain,
% 59.22/59.33 (E(f4(f4(a6)),f4(f2(a5)))),
% 59.22/59.33 inference(scs_inference,[],[1755,31,27,5,6,7])).
% 59.22/59.33 cnf(1832,plain,
% 59.22/59.33 (~E(f3(a1,f3(a5,a6)),f3(f3(a7,a5),a6))),
% 59.22/59.33 inference(scs_inference,[],[17,1755,887,1133,1729,1814,62,31,83,27,5,6,7,4,24,22,20,2,26])).
% 59.22/59.33 cnf(1840,plain,
% 59.22/59.33 (P2(f4(f4(a6)),f4(a6))),
% 59.22/59.33 inference(scs_inference,[],[17,1807,1755,1793,1795,887,1779,1133,1729,1814,1589,62,31,12,83,27,5,6,7,4,24,22,20,2,26,3,10,9])).
% 59.22/59.33 cnf(1844,plain,
% 59.22/59.33 (P2(f3(f4(a6),f4(a6)),f3(f4(a6),f4(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1816,27])).
% 59.22/59.33 cnf(1846,plain,
% 59.22/59.33 (E(f3(f3(f4(x18461),x18461),x18462),f3(x18461,x18462))),
% 59.22/59.33 inference(scs_inference,[],[1816,13,27,5])).
% 59.22/59.33 cnf(1849,plain,
% 59.22/59.33 (P1(f2(f2(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1816,834,13,27,5,7,6,24])).
% 59.22/59.33 cnf(1851,plain,
% 59.22/59.33 (P1(f4(f4(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1840,1816,834,13,27,5,7,6,24,22])).
% 59.22/59.33 cnf(1855,plain,
% 59.22/59.33 (~E(f3(f3(a7,a5),a6),f3(a1,f3(a5,a6)))),
% 59.22/59.33 inference(scs_inference,[],[1840,1816,1832,834,13,27,5,7,6,24,22,20,2])).
% 59.22/59.33 cnf(1857,plain,
% 59.22/59.33 (E(f3(f4(a6),x18571),f3(f2(a5),x18571))),
% 59.22/59.33 inference(rename_variables,[],[1821])).
% 59.22/59.33 cnf(1859,plain,
% 59.22/59.33 (E(f3(f4(a6),f4(a6)),f3(f2(a5),f2(a5)))),
% 59.22/59.33 inference(scs_inference,[],[1840,1816,1821,1857,1822,1832,834,13,27,5,7,6,24,22,20,2,21,3])).
% 59.22/59.33 cnf(1868,plain,
% 59.22/59.33 (E(f3(x18681,x18682),f3(f3(f4(x18681),x18681),x18682))),
% 59.22/59.33 inference(scs_inference,[],[1849,83,27,5])).
% 59.22/59.33 cnf(1876,plain,
% 59.22/59.33 (~E(f3(a1,f3(a5,a6)),f3(a7,f3(a5,a6)))),
% 59.22/59.33 inference(scs_inference,[],[1849,1846,1145,1776,373,54,83,27,5,6,7,24,20,2,26])).
% 59.22/59.33 cnf(1879,plain,
% 59.22/59.33 (E(f4(f4(a6)),f3(f4(f4(a6)),f4(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1849,1823,1846,1145,1776,373,407,54,83,27,5,6,7,24,20,2,26,3])).
% 59.22/59.33 cnf(1902,plain,
% 59.22/59.33 (P2(f3(f2(a5),f2(a5)),f3(f4(a6),f4(a6)))),
% 59.22/59.33 inference(scs_inference,[],[1851,1757,1876,1859,1879,1868,1844,1150,177,1816,27,24,20,2,21,3,10,9])).
% 59.22/59.33 cnf(1912,plain,
% 59.22/59.33 ($false),
% 59.22/59.33 inference(scs_inference,[],[1732,1902,1855,860,1793,837,16,27,24,20,2,3]),
% 59.22/59.33 ['proof']).
% 59.22/59.33 % SZS output end Proof
% 59.22/59.33 % Total time :58.780000s
%------------------------------------------------------------------------------