%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT003-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 04:40:08 EDT 2024
% Result : Unsatisfiable 59.62s 59.88s
% Output : CNFRefutation 59.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CAT003-3 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n026.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jun 18 12:05:24 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 59.62/59.86 %-------------------------------------------
% 59.62/59.86 % File :CSE---1.7
% 59.62/59.86 % Problem :theBenchmark
% 59.62/59.86 % Transform :cnf
% 59.62/59.86 % Format :tptp:raw
% 59.62/59.86 % Command :java -jar mcs_scs.jar %d %s
% 59.62/59.86
% 59.62/59.86 % Result :Theorem 59.150000s
% 59.62/59.86 % Output :CNFRefutation 59.150000s
% 59.62/59.86 %-------------------------------------------
% 59.62/59.88 %--------------------------------------------------------------------------
% 59.62/59.88 % File : CAT003-3 : TPTP v8.2.0. Released v1.0.0.
% 59.62/59.88 % Domain : Category Theory
% 59.62/59.88 % Problem : XY epimorphism => X epimorphism
% 59.62/59.88 % Version : [Sco79] axioms : Reduced > Complete.
% 59.62/59.88 % English : If xy is an epimorphism, then x is an epimorphism.
% 59.62/59.88
% 59.62/59.88 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 59.62/59.88 % Source : [ANL]
% 59.62/59.88 % Names : p3.ver3.in [ANL]
% 59.62/59.88
% 59.62/59.88 % Status : Unsatisfiable
% 59.62/59.88 % Rating : 0.10 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.30 v6.1.0, 0.36 v6.0.0, 0.20 v5.5.0, 0.30 v5.3.0, 0.28 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.07 v4.1.0, 0.23 v4.0.1, 0.27 v4.0.0, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.42 v2.4.0, 0.11 v2.2.1, 0.22 v2.2.0, 0.11 v2.1.0, 0.56 v2.0.0
% 59.62/59.88 % Syntax : Number of clauses : 22 ( 7 unt; 2 nHn; 17 RR)
% 59.62/59.88 % Number of literals : 44 ( 20 equ; 20 neg)
% 59.62/59.88 % Maximal clause size : 4 ( 2 avg)
% 59.62/59.88 % Maximal term depth : 3 ( 1 avg)
% 59.62/59.88 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 59.62/59.88 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 59.62/59.88 % Number of variables : 34 ( 4 sgn)
% 59.62/59.88 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.62/59.88
% 59.62/59.88 % Comments : Axioms simplified by Art Quaife.
% 59.62/59.88 %--------------------------------------------------------------------------
% 59.62/59.88 %----Include Scott's axioms for category theory
% 59.62/59.88 include('Axioms/CAT003-0.ax').
% 59.62/59.88 %--------------------------------------------------------------------------
% 59.62/59.88 cnf(assume_ab_exists,hypothesis,
% 59.62/59.88 there_exists(compose(a,b)) ).
% 59.62/59.88
% 59.62/59.88 cnf(epimorphism,hypothesis,
% 59.62/59.88 ( compose(X,compose(a,b)) != Y
% 59.62/59.88 | compose(Z,compose(a,b)) != Y
% 59.62/59.88 | X = Z ) ).
% 59.62/59.88
% 59.62/59.88 cnf(assume_h_exists,hypothesis,
% 59.62/59.88 there_exists(h) ).
% 59.62/59.88
% 59.62/59.88 cnf(ha_equals_ga,hypothesis,
% 59.62/59.88 compose(h,a) = compose(g,a) ).
% 59.62/59.88
% 59.62/59.88 cnf(prove_g_equals_h,negated_conjecture,
% 59.62/59.88 g != h ).
% 59.62/59.88
% 59.62/59.88 %--------------------------------------------------------------------------
% 59.62/59.88 %-------------------------------------------
% 59.62/59.88 % Proof found
% 59.62/59.88 % SZS status Theorem for theBenchmark
% 59.62/59.88 % SZS output start Proof
% 59.73/59.89 %ClaNum:33(EqnAxiom:12)
% 59.73/59.89 %VarNum:64(SingletonVarNum:30)
% 59.73/59.89 %MaxLitNum:3
% 59.73/59.89 %MaxfuncDepth:2
% 59.73/59.89 %SharedTerms:11
% 59.73/59.89 %goalClause: 19
% 59.73/59.89 %singleGoalClaCount:1
% 59.73/59.89 [13]P1(a1)
% 59.73/59.89 [19]~E(a1,a7)
% 59.73/59.89 [16]E(f3(a1,a5),f3(a7,a5))
% 59.73/59.89 [17]P1(f3(a5,a6))
% 59.73/59.89 [14]E(f3(x141,f2(x141)),x141)
% 59.73/59.89 [15]E(f3(f4(x151),x151),x151)
% 59.73/59.89 [18]E(f3(f3(x181,x182),x183),f3(x181,f3(x182,x183)))
% 59.73/59.89 [20]P1(x201)+~P1(f2(x201))
% 59.73/59.89 [21]P1(x211)+~P1(f4(x211))
% 59.73/59.89 [22]~P2(x221,x222)+E(x221,x222)
% 59.73/59.89 [24]P1(x241)+~P2(x242,x241)
% 59.73/59.89 [25]P1(x251)+~P2(x251,x252)
% 59.73/59.89 [27]E(x271,x272)+P1(f8(x271,x272))
% 59.73/59.89 [29]E(f4(x291),f2(x292))+~P1(f3(x292,x291))
% 59.73/59.89 [30]P1(f2(x301))+~P1(f3(x301,x302))
% 59.73/59.89 [31]P1(f4(x311))+~P1(f3(x311,x312))
% 59.73/59.89 [23]~E(x231,x232)+~P1(x231)+P2(x231,x232)
% 59.73/59.89 [28]E(x281,x282)+E(f8(x281,x282),x282)+E(f8(x281,x282),x281)
% 59.73/59.89 [32]~E(f4(x322),f2(x321))+~P1(f2(x321))+P1(f3(x321,x322))
% 59.73/59.89 [33]E(x331,x332)+~E(f3(x331,f3(a5,a6)),x333)+~E(f3(x332,f3(a5,a6)),x333)
% 59.73/59.89 %EqnAxiom
% 59.73/59.89 [1]E(x11,x11)
% 59.73/59.89 [2]E(x22,x21)+~E(x21,x22)
% 59.73/59.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.73/59.89 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 59.73/59.89 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 59.73/59.89 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 59.73/59.89 [7]~E(x71,x72)+E(f4(x71),f4(x72))
% 59.73/59.89 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83))
% 59.73/59.89 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92))
% 59.73/59.89 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 59.73/59.89 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 59.73/59.89 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 59.73/59.89
% 59.73/59.89 %-------------------------------------------
% 59.73/59.91 cnf(34,plain,
% 59.73/59.91 (~P1(x341)+P2(x341,x341)),
% 59.73/59.91 inference(equality_inference,[],[23])).
% 59.73/59.91 cnf(35,plain,
% 59.73/59.91 (~P2(a1,a7)),
% 59.73/59.91 inference(scs_inference,[],[19,22])).
% 59.73/59.91 cnf(37,plain,
% 59.73/59.91 (E(f3(a7,a5),f3(a1,a5))),
% 59.73/59.91 inference(scs_inference,[],[19,16,22,2])).
% 59.73/59.91 cnf(38,plain,
% 59.73/59.91 (E(f4(a6),f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[19,16,17,22,2,29])).
% 59.73/59.91 cnf(40,plain,
% 59.73/59.91 (E(f3(f3(a1,a5),f2(f3(a1,a5))),f3(a7,a5))),
% 59.73/59.91 inference(scs_inference,[],[19,16,14,17,22,2,29,3])).
% 59.73/59.91 cnf(42,plain,
% 59.73/59.91 (P2(f3(a5,a6),x421)+~E(f3(a5,a6),x421)),
% 59.73/59.91 inference(scs_inference,[],[19,16,14,17,22,2,29,3,23])).
% 59.73/59.91 cnf(46,plain,
% 59.73/59.91 (P2(f3(a5,a6),f3(a5,a6))),
% 59.73/59.91 inference(equality_inference,[],[42])).
% 59.73/59.91 cnf(48,plain,
% 59.73/59.91 (E(f3(f4(f4(a6)),f4(a6)),f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[40,38,15,2,3])).
% 59.73/59.91 cnf(50,plain,
% 59.73/59.91 (P2(x501,f3(a5,a6))+~E(f3(a5,a6),x501)),
% 59.73/59.91 inference(scs_inference,[],[40,46,38,15,2,3,11])).
% 59.73/59.91 cnf(53,plain,
% 59.73/59.91 (E(f2(a5),f3(f4(f4(a6)),f4(a6)))),
% 59.73/59.91 inference(scs_inference,[],[48,2])).
% 59.73/59.91 cnf(54,plain,
% 59.73/59.91 (E(f3(f4(a6),f2(f4(a6))),f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[48,38,14,2,3])).
% 59.73/59.91 cnf(56,plain,
% 59.73/59.91 (~P1(f3(f4(f4(a6)),f4(a6)))+P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[48,38,14,2,3,10])).
% 59.73/59.91 cnf(61,plain,
% 59.73/59.91 (~E(f3(a5,a6),f3(f4(f4(a6)),f4(a6)))+P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[48,17,38,14,2,3,10,24,25,32,23])).
% 59.73/59.91 cnf(63,plain,
% 59.73/59.91 (E(f2(a5),f3(f4(a6),f2(f4(a6))))),
% 59.73/59.91 inference(scs_inference,[],[54,2])).
% 59.73/59.91 cnf(64,plain,
% 59.73/59.91 (~E(a1,f3(f4(a7),a7))),
% 59.73/59.91 inference(scs_inference,[],[19,54,15,2,3])).
% 59.73/59.91 cnf(68,plain,
% 59.73/59.91 (~P1(f3(f4(a6),f2(f4(a6))))+P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[19,54,15,2,3,22,10])).
% 59.73/59.91 cnf(69,plain,
% 59.73/59.91 (~P2(x691,f3(f4(a6),f2(f4(a6))))+P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[19,54,15,2,3,22,10,24])).
% 59.73/59.91 cnf(74,plain,
% 59.73/59.91 (E(f3(x741,f3(x742,x743)),f3(f3(x741,x742),x743))),
% 59.73/59.91 inference(scs_inference,[],[18,2])).
% 59.73/59.91 cnf(75,plain,
% 59.73/59.91 (~E(a1,f3(a7,f2(a7)))),
% 59.73/59.91 inference(scs_inference,[],[19,18,14,2,3])).
% 59.73/59.91 cnf(77,plain,
% 59.73/59.91 (~P2(a1,f3(a7,f2(a7)))),
% 59.73/59.91 inference(scs_inference,[],[19,18,14,2,3,22])).
% 59.73/59.91 cnf(79,plain,
% 59.73/59.91 (~P1(f2(a5))+P1(f3(f4(f4(a6)),f4(a6)))),
% 59.73/59.91 inference(scs_inference,[],[19,53,18,14,2,3,22,10])).
% 59.73/59.91 cnf(83,plain,
% 59.73/59.91 (P1(f3(f4(f4(a6)),f4(a6)))+~P1(f3(f4(a6),f2(f4(a6))))),
% 59.73/59.91 inference(scs_inference,[],[19,53,17,18,14,2,3,22,10,61,30,56,68])).
% 59.73/59.91 cnf(92,plain,
% 59.73/59.91 (E(f2(a5),f4(a6))),
% 59.73/59.91 inference(scs_inference,[],[38,2])).
% 59.73/59.91 cnf(93,plain,
% 59.73/59.91 (~P1(f3(x931,f3(x932,x933)))+P1(f3(f3(x931,x932),x933))),
% 59.73/59.91 inference(scs_inference,[],[74,38,2,10])).
% 59.73/59.91 cnf(98,plain,
% 59.73/59.91 (~E(f3(a5,a6),f3(x981,f3(x982,x983)))+P1(f3(f3(x981,x982),x983))),
% 59.73/59.91 inference(scs_inference,[],[74,17,38,2,10,25,24,32,23])).
% 59.73/59.91 cnf(100,plain,
% 59.73/59.91 (~E(f3(a5,a6),f3(f3(x1001,x1002),x1003))+P1(f3(f3(x1001,x1002),x1003))),
% 59.73/59.91 inference(scs_inference,[],[74,17,18,38,2,10,25,24,32,23,3])).
% 59.73/59.91 cnf(102,plain,
% 59.73/59.91 (E(x1021,f3(f4(x1021),x1021))),
% 59.73/59.91 inference(scs_inference,[],[15,2])).
% 59.73/59.91 cnf(107,plain,
% 59.73/59.91 (E(x1071,f3(x1071,f2(x1071)))),
% 59.73/59.91 inference(scs_inference,[],[14,2])).
% 59.73/59.91 cnf(119,plain,
% 59.73/59.91 (~P1(f2(a5))+P1(f4(a6))),
% 59.73/59.91 inference(scs_inference,[],[92,10])).
% 59.73/59.91 cnf(146,plain,
% 59.73/59.91 (~P1(f2(a5))+P1(f3(f4(a6),f2(f4(a6))))),
% 59.73/59.91 inference(scs_inference,[],[63,10])).
% 59.73/59.91 cnf(161,plain,
% 59.73/59.91 (~P1(f4(a6))+P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[38,10])).
% 59.73/59.91 cnf(166,plain,
% 59.73/59.91 (~P2(f4(a6),x1661)+P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[38,10,31,24,25])).
% 59.73/59.91 cnf(188,plain,
% 59.73/59.91 (P1(f3(a1,f2(a1)))),
% 59.73/59.91 inference(scs_inference,[],[13,107,10])).
% 59.73/59.91 cnf(192,plain,
% 59.73/59.91 (E(f2(a1),f4(f2(a1)))),
% 59.73/59.91 inference(scs_inference,[],[13,107,10,29,2])).
% 59.73/59.91 cnf(193,plain,
% 59.73/59.91 (E(f3(f4(f2(a1)),f2(a1)),f4(f2(a1)))),
% 59.73/59.91 inference(scs_inference,[],[13,107,15,10,29,2,3])).
% 59.73/59.91 cnf(199,plain,
% 59.73/59.91 (E(f4(a1),f2(f4(a1)))),
% 59.73/59.91 inference(scs_inference,[],[13,102,193,2,10,29])).
% 59.73/59.91 cnf(201,plain,
% 59.73/59.91 (E(f3(f4(f4(a1)),f4(a1)),f2(f4(a1)))),
% 59.73/59.91 inference(scs_inference,[],[13,102,193,15,2,10,29,3])).
% 59.73/59.91 cnf(203,plain,
% 59.73/59.91 (P1(f4(a6))),
% 59.73/59.91 inference(scs_inference,[],[17,119,30])).
% 59.73/59.91 cnf(204,plain,
% 59.73/59.91 (P1(f2(a5))),
% 59.73/59.91 inference(scs_inference,[],[203,161])).
% 59.73/59.91 cnf(205,plain,
% 59.73/59.91 (P1(a6)),
% 59.73/59.91 inference(scs_inference,[],[203,21])).
% 59.73/59.91 cnf(208,plain,
% 59.73/59.91 (P2(f4(a6),f3(f4(a6),f2(f4(a6))))),
% 59.73/59.91 inference(scs_inference,[],[107,201,203,21,2,23])).
% 59.73/59.91 cnf(211,plain,
% 59.78/59.91 (~P1(f2(a1))+P1(f4(f2(a1)))),
% 59.78/59.91 inference(scs_inference,[],[107,192,201,203,21,2,23,10])).
% 59.78/59.91 cnf(221,plain,
% 59.78/59.91 (P1(f2(a5))),
% 59.78/59.91 inference(scs_inference,[],[208,69])).
% 59.78/59.91 cnf(222,plain,
% 59.78/59.91 (P1(f3(f4(f4(a6)),f4(a6)))),
% 59.78/59.91 inference(scs_inference,[],[204,79])).
% 59.78/59.91 cnf(224,plain,
% 59.78/59.91 (P1(f3(f4(a6),f2(f4(a6))))),
% 59.78/59.91 inference(scs_inference,[],[204,146])).
% 59.78/59.91 cnf(225,plain,
% 59.78/59.91 (P1(f2(a5))),
% 59.78/59.91 inference(scs_inference,[],[208,166])).
% 59.78/59.91 cnf(230,plain,
% 59.78/59.91 (P1(f3(f4(f4(a6)),f4(a6)))),
% 59.78/59.91 inference(scs_inference,[],[224,83])).
% 59.78/59.91 cnf(233,plain,
% 59.78/59.91 (P1(a5)),
% 59.78/59.91 inference(scs_inference,[],[204,20])).
% 59.78/59.91 cnf(236,plain,
% 59.78/59.91 (P2(f2(a5),f3(f4(f2(a5)),f2(a5)))),
% 59.78/59.91 inference(scs_inference,[],[102,199,204,20,2,23])).
% 59.78/59.91 cnf(256,plain,
% 59.78/59.91 (P1(f8(a7,a1))),
% 59.78/59.91 inference(scs_inference,[],[19,27,2])).
% 59.78/59.91 cnf(257,plain,
% 59.78/59.91 (P2(f8(a7,a1),f3(f8(a7,a1),f2(f8(a7,a1))))),
% 59.78/59.91 inference(scs_inference,[],[107,256,23])).
% 59.78/59.91 cnf(285,plain,
% 59.78/59.91 (P2(f2(a5),f3(f2(a5),f2(f2(a5))))),
% 59.78/59.91 inference(scs_inference,[],[107,221,23])).
% 59.78/59.91 cnf(317,plain,
% 59.78/59.91 (P2(a6,f3(a6,f2(a6)))),
% 59.78/59.91 inference(scs_inference,[],[107,205,23])).
% 59.78/59.91 cnf(323,plain,
% 59.78/59.91 (P2(a5,f3(a5,f2(a5)))),
% 59.78/59.91 inference(scs_inference,[],[107,233,23])).
% 59.78/59.91 cnf(324,plain,
% 59.78/59.91 (E(x3241,f3(x3241,f2(x3241)))),
% 59.78/59.91 inference(rename_variables,[],[107])).
% 59.78/59.91 cnf(326,plain,
% 59.78/59.91 (P2(f3(a5,f2(a5)),f3(a5,f2(a5)))),
% 59.78/59.91 inference(scs_inference,[],[107,324,233,23,11])).
% 59.78/59.91 cnf(328,plain,
% 59.78/59.91 (P2(a6,f3(f4(a6),a6))),
% 59.78/59.91 inference(scs_inference,[],[102,205,23])).
% 59.78/59.91 cnf(329,plain,
% 59.78/59.91 (E(x3291,f3(f4(x3291),x3291))),
% 59.78/59.91 inference(rename_variables,[],[102])).
% 59.78/59.91 cnf(331,plain,
% 59.78/59.91 (P2(f3(f4(a6),a6),f3(a6,f2(a6)))),
% 59.78/59.91 inference(scs_inference,[],[102,329,317,205,23,11])).
% 59.78/59.91 cnf(333,plain,
% 59.78/59.91 (P2(f3(a6,f2(a6)),f3(f4(a6),a6))),
% 59.78/59.91 inference(scs_inference,[],[107,328,11])).
% 59.78/59.91 cnf(336,plain,
% 59.78/59.91 (E(x3361,f3(f4(x3361),x3361))),
% 59.78/59.91 inference(rename_variables,[],[102])).
% 59.78/59.91 cnf(338,plain,
% 59.78/59.91 (P2(f3(f4(a5),a5),f3(a5,f2(a5)))),
% 59.78/59.91 inference(scs_inference,[],[102,336,323,233,23,11])).
% 59.78/59.91 cnf(345,plain,
% 59.78/59.91 (P2(f2(a5),f2(a5))),
% 59.78/59.91 inference(scs_inference,[],[14,285,12])).
% 59.78/59.91 cnf(346,plain,
% 59.78/59.91 (E(f3(x3461,f2(x3461)),x3461)),
% 59.78/59.91 inference(rename_variables,[],[14])).
% 59.78/59.91 cnf(347,plain,
% 59.78/59.91 (P2(f3(a1,f2(a1)),a1)),
% 59.78/59.91 inference(scs_inference,[],[14,346,285,188,12,23])).
% 59.78/59.91 cnf(360,plain,
% 59.78/59.91 (P2(f3(a1,f2(a1)),f3(f4(a1),a1))),
% 59.78/59.91 inference(scs_inference,[],[102,347,12])).
% 59.78/59.91 cnf(374,plain,
% 59.78/59.91 (E(f3(x3741,f2(x3741)),x3741)),
% 59.78/59.91 inference(rename_variables,[],[14])).
% 59.78/59.91 cnf(377,plain,
% 59.78/59.91 (E(f3(x3771,f2(x3771)),x3771)),
% 59.78/59.91 inference(rename_variables,[],[14])).
% 59.78/59.91 cnf(378,plain,
% 59.78/59.91 (P2(a1,f3(f4(a1),a1))),
% 59.78/59.91 inference(scs_inference,[],[14,374,377,257,360,224,23,12,11])).
% 59.78/59.91 cnf(400,plain,
% 59.78/59.91 (P2(f3(a6,f2(a6)),a6)),
% 59.78/59.91 inference(scs_inference,[],[14,107,317,12,11])).
% 59.78/59.91 cnf(420,plain,
% 59.78/59.91 (P2(f3(f4(f2(a5)),f2(a5)),f2(a5))),
% 59.78/59.91 inference(scs_inference,[],[14,102,326,345,12,11])).
% 59.78/59.91 cnf(428,plain,
% 59.78/59.91 (P2(f3(a1,f2(a1)),f3(a1,f2(a1)))),
% 59.78/59.91 inference(scs_inference,[],[107,347,12])).
% 59.78/59.91 cnf(430,plain,
% 59.78/59.91 (P2(a1,f3(a1,f2(a1)))),
% 59.78/59.91 inference(scs_inference,[],[14,107,347,12,11])).
% 59.78/59.91 cnf(440,plain,
% 59.78/59.91 (~E(f3(f4(a1),a1),a7)),
% 59.78/59.91 inference(scs_inference,[],[35,378,12])).
% 59.78/59.91 cnf(443,plain,
% 59.78/59.91 (~E(f3(a1,f2(a1)),f3(a7,f2(a7)))),
% 59.78/59.91 inference(scs_inference,[],[77,430,12])).
% 59.78/59.91 cnf(444,plain,
% 59.78/59.91 (~P2(f3(a1,f2(a1)),f3(a7,f2(a7)))),
% 59.78/59.91 inference(scs_inference,[],[77,430,12,22])).
% 59.78/59.91 cnf(446,plain,
% 59.78/59.91 (~E(f3(f4(a1),a1),f3(a7,f2(a7)))),
% 59.78/59.91 inference(scs_inference,[],[444,360,12])).
% 59.78/59.91 cnf(480,plain,
% 59.78/59.91 (E(f4(a6),f3(f4(f2(a5)),f2(a5)))),
% 59.78/59.91 inference(scs_inference,[],[15,92,3,2])).
% 59.78/59.91 cnf(503,plain,
% 59.78/59.91 (P1(f3(f4(f2(a5)),f2(a5)))),
% 59.78/59.91 inference(scs_inference,[],[15,480,16,203,3,10])).
% 59.78/59.91 cnf(595,plain,
% 59.78/59.91 (P2(f3(f4(a1),a1),f3(f4(a1),a1))),
% 59.78/59.91 inference(scs_inference,[],[102,378,11])).
% 59.78/59.91 cnf(618,plain,
% 59.78/59.91 (P1(f3(a6,f2(a6)))),
% 59.78/59.91 inference(scs_inference,[],[205,107,10])).
% 59.78/59.91 cnf(622,plain,
% 59.78/59.91 (E(f2(a6),f4(f2(a6)))),
% 59.78/59.91 inference(scs_inference,[],[205,107,10,29,2])).
% 59.78/59.91 cnf(623,plain,
% 59.78/59.91 (E(f3(f4(f2(a6)),f2(a6)),f4(f2(a6)))),
% 59.78/59.91 inference(scs_inference,[],[205,107,15,10,29,2,3])).
% 59.78/59.91 cnf(627,plain,
% 59.78/59.91 (E(f4(f2(a6)),f3(f4(f2(a6)),f2(a6)))),
% 59.78/59.91 inference(scs_inference,[],[623,2])).
% 59.78/59.91 cnf(630,plain,
% 59.78/59.91 (E(f4(a6),f2(f4(a6)))),
% 59.78/59.91 inference(scs_inference,[],[205,102,623,2,10,29])).
% 59.78/59.91 cnf(632,plain,
% 59.78/59.91 (E(f2(a5),f2(f4(a6)))),
% 59.78/59.91 inference(scs_inference,[],[205,102,92,623,2,10,29,3])).
% 59.78/59.91 cnf(634,plain,
% 59.78/59.91 (E(f2(f4(a6)),f2(a5))),
% 59.78/59.91 inference(scs_inference,[],[632,2])).
% 59.78/59.91 cnf(635,plain,
% 59.78/59.91 (E(f3(f4(f4(a6)),f4(a6)),f2(f4(a6)))),
% 59.78/59.91 inference(scs_inference,[],[48,632,2,3])).
% 59.78/59.91 cnf(636,plain,
% 59.78/59.91 (P1(f2(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[48,632,225,2,3,10])).
% 59.78/59.92 cnf(653,plain,
% 59.78/59.92 (~P1(f4(f2(a6)))+P1(f3(f4(f2(a6)),f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[627,630,2,10])).
% 59.78/59.92 cnf(694,plain,
% 59.78/59.92 (P1(f3(a5,f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[233,107,10])).
% 59.78/59.92 cnf(698,plain,
% 59.78/59.92 (E(f2(a5),f4(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[233,107,10,29,2])).
% 59.78/59.92 cnf(699,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f4(a6)),f4(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[233,107,48,10,29,2,3])).
% 59.78/59.92 cnf(702,plain,
% 59.78/59.92 (E(f4(a6),f4(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[102,699,2,3])).
% 59.78/59.92 cnf(703,plain,
% 59.78/59.92 (E(x7031,f3(f4(x7031),x7031))),
% 59.78/59.92 inference(rename_variables,[],[102])).
% 59.78/59.92 cnf(706,plain,
% 59.78/59.92 (E(f4(a5),f2(f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[233,102,703,699,2,3,10,29])).
% 59.78/59.92 cnf(710,plain,
% 59.78/59.92 (E(f3(f4(f4(a5)),f4(a5)),f2(f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[702,15,706,2,3])).
% 59.78/59.92 cnf(714,plain,
% 59.78/59.92 (E(f2(f4(a5)),f3(f4(f4(a5)),f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[710,2])).
% 59.78/59.92 cnf(728,plain,
% 59.78/59.92 (~P1(f2(f4(a5)))+P1(f3(f4(f4(a5)),f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[714,706,2,10])).
% 59.78/59.92 cnf(744,plain,
% 59.78/59.92 (~P1(f4(a5))+P1(f2(f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[706,10])).
% 59.78/59.92 cnf(873,plain,
% 59.78/59.92 (E(f4(f2(a5)),f2(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[634,698,3,2])).
% 59.78/59.92 cnf(1247,plain,
% 59.78/59.92 (P1(f4(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[230,21,31])).
% 59.78/59.92 cnf(1292,plain,
% 59.78/59.92 (P1(f4(a5))),
% 59.78/59.92 inference(scs_inference,[],[46,24,31])).
% 59.78/59.92 cnf(1293,plain,
% 59.78/59.92 (P1(f2(f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[1292,744])).
% 59.78/59.92 cnf(1299,plain,
% 59.78/59.92 (P1(f3(f4(f4(a5)),f4(a5)))),
% 59.78/59.92 inference(scs_inference,[],[1293,728])).
% 59.78/59.92 cnf(1328,plain,
% 59.78/59.92 (P1(f2(f4(a1)))),
% 59.78/59.92 inference(scs_inference,[],[595,25,30])).
% 59.78/59.92 cnf(1336,plain,
% 59.78/59.92 (P1(f4(a1))),
% 59.78/59.92 inference(scs_inference,[],[1328,20])).
% 59.78/59.92 cnf(1383,plain,
% 59.78/59.92 (P2(f8(a1,a7),f8(a1,a7))),
% 59.78/59.92 inference(scs_inference,[],[19,34,27])).
% 59.78/59.92 cnf(1391,plain,
% 59.78/59.92 (E(x13911,f3(f4(x13911),x13911))),
% 59.78/59.92 inference(rename_variables,[],[102])).
% 59.78/59.92 cnf(1393,plain,
% 59.78/59.92 (P2(f8(a1,a7),f3(f4(f8(a1,a7)),f8(a1,a7)))),
% 59.78/59.92 inference(scs_inference,[],[102,1391,1383,1336,23,12])).
% 59.78/59.92 cnf(1401,plain,
% 59.78/59.92 (P2(f3(f4(f8(a1,a7)),f8(a1,a7)),f8(a1,a7))),
% 59.78/59.92 inference(scs_inference,[],[102,1383,11])).
% 59.78/59.92 cnf(1407,plain,
% 59.78/59.92 (E(f3(f3(x14071,f2(x14071)),x14072),f3(x14071,x14072))),
% 59.78/59.92 inference(scs_inference,[],[107,2,5])).
% 59.78/59.92 cnf(1408,plain,
% 59.78/59.92 (E(f3(x14081,x14082),f3(f3(x14081,f2(x14081)),x14082))),
% 59.78/59.92 inference(scs_inference,[],[1407,2])).
% 59.78/59.92 cnf(1410,plain,
% 59.78/59.92 (E(f3(f3(x14101,f2(x14101)),x14102),f3(x14101,x14102))),
% 59.78/59.92 inference(rename_variables,[],[1407])).
% 59.78/59.92 cnf(1411,plain,
% 59.78/59.92 (~P2(a1,f3(f3(a7,f2(a7)),f2(a7)))),
% 59.78/59.92 inference(scs_inference,[],[75,1407,2,3,22])).
% 59.78/59.92 cnf(1413,plain,
% 59.78/59.92 (~P1(f3(f3(x14131,f2(x14131)),x14132))+P1(f3(x14131,x14132))),
% 59.78/59.92 inference(scs_inference,[],[75,1407,1410,2,3,22,10])).
% 59.78/59.92 cnf(1434,plain,
% 59.78/59.92 (~P1(f3(f3(x14341,f2(x14341)),x14342))+E(f4(x14342),f2(x14341))),
% 59.78/59.92 inference(scs_inference,[],[1413,29])).
% 59.78/59.92 cnf(1435,plain,
% 59.78/59.92 (P1(f3(f3(a5,f2(a5)),a6))),
% 59.78/59.92 inference(scs_inference,[],[1408,100])).
% 59.78/59.92 cnf(1458,plain,
% 59.78/59.92 (E(f3(x14581,f4(a6)),f3(x14581,f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[1435,1434,6])).
% 59.78/59.92 cnf(1459,plain,
% 59.78/59.92 (E(f3(x14591,f2(a5)),f3(x14591,f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1458,2])).
% 59.78/59.92 cnf(1460,plain,
% 59.78/59.92 (E(f4(a6),f3(f4(f4(a6)),f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[102,1458,2,3])).
% 59.78/59.92 cnf(1461,plain,
% 59.78/59.92 (E(f3(x14611,f4(a6)),f3(x14611,f2(a5)))),
% 59.78/59.92 inference(rename_variables,[],[1458])).
% 59.78/59.92 cnf(1463,plain,
% 59.78/59.92 (P1(f3(f4(f4(a6)),f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[102,1458,1461,222,2,3,10])).
% 59.78/59.92 cnf(1466,plain,
% 59.78/59.92 (E(a5,f3(a5,f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[107,1459,1460,2,3])).
% 59.78/59.92 cnf(1467,plain,
% 59.78/59.92 (E(f3(x14671,f2(a5)),f3(x14671,f4(a6)))),
% 59.78/59.92 inference(rename_variables,[],[1459])).
% 59.78/59.92 cnf(1469,plain,
% 59.78/59.92 (P1(f3(a5,f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[107,1459,1467,1460,694,2,3,10])).
% 59.78/59.92 cnf(1471,plain,
% 59.78/59.92 (E(f4(f4(a6)),f2(a5))),
% 59.78/59.92 inference(scs_inference,[],[107,1459,1467,1460,694,2,3,10,29])).
% 59.78/59.92 cnf(1474,plain,
% 59.78/59.92 (E(f3(a5,f4(a6)),a5)),
% 59.78/59.92 inference(scs_inference,[],[1466,2])).
% 59.78/59.92 cnf(1475,plain,
% 59.78/59.92 (E(f3(f4(a5),a5),f3(a5,f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1466,15,2,3])).
% 59.78/59.92 cnf(1478,plain,
% 59.78/59.92 (E(f3(a5,f4(a6)),f3(f4(a5),a5))),
% 59.78/59.92 inference(scs_inference,[],[1475,2])).
% 59.78/59.92 cnf(1484,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f4(a6)),f4(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[48,1471,2,3])).
% 59.78/59.92 cnf(1508,plain,
% 59.78/59.92 (E(f3(x15081,f3(x15082,f2(x15082))),f3(x15081,x15082))),
% 59.78/59.92 inference(scs_inference,[],[107,2,6])).
% 59.78/59.92 cnf(1509,plain,
% 59.78/59.92 (E(f3(x15091,x15092),f3(x15091,f3(x15092,f2(x15092))))),
% 59.78/59.92 inference(scs_inference,[],[1508,2])).
% 59.78/59.92 cnf(1510,plain,
% 59.78/59.92 (P1(f3(a5,f3(a6,f2(a6))))),
% 59.78/59.92 inference(scs_inference,[],[17,1508,2,10])).
% 59.78/59.92 cnf(1511,plain,
% 59.78/59.92 (P1(f3(f3(a5,a6),f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[17,1508,2,10,98])).
% 59.78/59.92 cnf(1516,plain,
% 59.78/59.92 (E(f4(f3(a6,f2(a6))),f2(a5))),
% 59.78/59.92 inference(scs_inference,[],[17,1508,2,10,98,42,50,29])).
% 59.78/59.92 cnf(1518,plain,
% 59.78/59.92 (E(f4(f3(x15181,f2(x15181))),f4(x15181))),
% 59.78/59.92 inference(scs_inference,[],[107,2,7])).
% 59.78/59.92 cnf(1522,plain,
% 59.78/59.92 (E(f2(a6),f2(f3(a5,a6)))),
% 59.78/59.92 inference(scs_inference,[],[622,1518,1511,29,2,3])).
% 59.78/59.92 cnf(1524,plain,
% 59.78/59.92 (E(f8(x15241,f3(x15242,f2(x15242))),f8(x15241,x15242))),
% 59.78/59.92 inference(scs_inference,[],[107,2,9])).
% 59.78/59.92 cnf(1525,plain,
% 59.78/59.92 (E(f2(f3(a5,a6)),f2(a6))),
% 59.78/59.92 inference(scs_inference,[],[1522,2])).
% 59.78/59.92 cnf(1569,plain,
% 59.78/59.92 (E(f2(f3(a5,a6)),f4(f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[622,1525,1524,2,3])).
% 59.78/59.92 cnf(1573,plain,
% 59.78/59.92 (~P1(f2(f3(a5,a6)))+P1(f4(f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1569,1516,2,10])).
% 59.78/59.92 cnf(1591,plain,
% 59.78/59.92 (E(f2(a5),f4(f3(f2(a5),a6)))),
% 59.78/59.92 inference(scs_inference,[],[18,1435,10,29,2])).
% 59.78/59.92 cnf(1599,plain,
% 59.78/59.92 (E(f2(a5),f2(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[92,1591,221,10,21,29,2,3])).
% 59.78/59.92 cnf(1600,plain,
% 59.78/59.92 (P1(f4(f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1511,1573,30])).
% 59.78/59.92 cnf(1601,plain,
% 59.78/59.92 (P1(f3(f4(f2(a6)),f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1600,653])).
% 59.78/59.92 cnf(1603,plain,
% 59.78/59.92 (P1(f2(a6))),
% 59.78/59.92 inference(scs_inference,[],[1600,21])).
% 59.78/59.92 cnf(1606,plain,
% 59.78/59.92 (P2(f2(a6),f3(f2(a6),f2(f2(a6))))),
% 59.78/59.92 inference(scs_inference,[],[107,1599,1600,21,2,23])).
% 59.78/59.92 cnf(1609,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f4(a6)),f2(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[107,48,1599,1600,21,2,23,3])).
% 59.78/59.92 cnf(1610,plain,
% 59.78/59.92 (P1(f2(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[107,48,1599,225,1600,21,2,23,3,10])).
% 59.78/59.92 cnf(1627,plain,
% 59.78/59.92 (~E(a7,f3(f4(a1),a1))),
% 59.78/59.92 inference(scs_inference,[],[19,15,2,3])).
% 59.78/59.92 cnf(1636,plain,
% 59.78/59.92 (E(x16361,f3(f4(x16361),x16361))),
% 59.78/59.92 inference(rename_variables,[],[102])).
% 59.78/59.92 cnf(1638,plain,
% 59.78/59.92 (E(x16381,f3(f4(x16381),f3(x16381,f2(x16381))))),
% 59.78/59.92 inference(scs_inference,[],[102,1636,1509,1603,23,3])).
% 59.78/59.92 cnf(1684,plain,
% 59.78/59.92 (P1(f4(f2(a1)))),
% 59.78/59.92 inference(scs_inference,[],[188,30,211])).
% 59.78/59.92 cnf(1689,plain,
% 59.78/59.92 (P2(f2(a1),f3(f2(a1),f2(f2(a1))))),
% 59.78/59.92 inference(scs_inference,[],[107,1684,21,23])).
% 59.78/59.92 cnf(1696,plain,
% 59.78/59.92 (P1(f2(f8(a7,a1)))),
% 59.78/59.92 inference(scs_inference,[],[107,256,30,10])).
% 59.78/59.92 cnf(1699,plain,
% 59.78/59.92 (P1(f2(f4(f8(a1,a7))))),
% 59.78/59.92 inference(scs_inference,[],[1393,30,24])).
% 59.78/59.92 cnf(1700,plain,
% 59.78/59.92 (P1(f4(f8(a1,a7)))),
% 59.78/59.92 inference(scs_inference,[],[1699,20])).
% 59.78/59.92 cnf(1704,plain,
% 59.78/59.92 (P1(f4(f3(a5,a6)))),
% 59.78/59.92 inference(scs_inference,[],[1510,31,93])).
% 59.78/59.92 cnf(1743,plain,
% 59.78/59.92 (E(f3(f3(a5,f2(a5)),f4(a6)),a5)),
% 59.78/59.92 inference(scs_inference,[],[1407,1474,3])).
% 59.78/59.92 cnf(1747,plain,
% 59.78/59.92 (E(f3(f3(a5,f2(a5)),f4(a6)),f3(f4(a5),a5))),
% 59.78/59.92 inference(scs_inference,[],[1407,1478,1743,2,3])).
% 59.78/59.92 cnf(1862,plain,
% 59.78/59.92 (E(f3(x18621,x18622),f3(f3(x18621,f2(x18621)),x18622))),
% 59.78/59.92 inference(rename_variables,[],[1408])).
% 59.78/59.92 cnf(1864,plain,
% 59.78/59.92 (P2(a6,f3(f3(a6,f2(a6)),f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1408,1862,317,618,23,12])).
% 59.78/59.92 cnf(1865,plain,
% 59.78/59.92 (E(f3(x18651,x18652),f3(f3(x18651,f2(x18651)),x18652))),
% 59.78/59.92 inference(rename_variables,[],[1408])).
% 59.78/59.92 cnf(1866,plain,
% 59.78/59.92 (P2(f3(f3(a6,f2(a6)),f2(a6)),a6)),
% 59.78/59.92 inference(scs_inference,[],[1408,1862,1865,317,618,400,23,12,11])).
% 59.78/59.92 cnf(1878,plain,
% 59.78/59.92 (E(f3(x18781,x18782),f3(f3(x18781,f2(x18781)),x18782))),
% 59.78/59.92 inference(rename_variables,[],[1408])).
% 59.78/59.92 cnf(1882,plain,
% 59.78/59.92 (P2(f3(f3(a1,f2(a1)),f2(a1)),f3(a1,f2(a1)))),
% 59.78/59.92 inference(scs_inference,[],[1408,1878,107,428,1469,1866,23,12,11])).
% 59.78/59.92 cnf(1885,plain,
% 59.78/59.92 (P2(f3(f4(a6),a6),f3(f3(a6,f2(a6)),f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1408,331,12])).
% 59.78/59.92 cnf(1886,plain,
% 59.78/59.92 (E(f3(x18861,x18862),f3(f3(x18861,f2(x18861)),x18862))),
% 59.78/59.92 inference(rename_variables,[],[1408])).
% 59.78/59.92 cnf(1887,plain,
% 59.78/59.92 (P2(f3(f3(a6,f2(a6)),f2(a6)),f3(f4(a6),a6))),
% 59.78/59.92 inference(scs_inference,[],[1408,1886,333,331,12,11])).
% 59.78/59.92 cnf(1897,plain,
% 59.78/59.92 (~E(f3(a1,f2(a1)),f3(f3(a7,f2(a7)),f2(a7)))),
% 59.78/59.92 inference(scs_inference,[],[1411,430,12])).
% 59.78/59.92 cnf(1958,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f2(a5)),f2(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1459,635,3])).
% 59.78/59.92 cnf(1959,plain,
% 59.78/59.92 (E(f3(x19591,f2(a5)),f3(x19591,f4(a6)))),
% 59.78/59.92 inference(rename_variables,[],[1459])).
% 59.78/59.92 cnf(1960,plain,
% 59.78/59.92 (P2(a5,f3(a5,f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1459,1959,635,323,3,12])).
% 59.78/59.92 cnf(1966,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f2(a5)),f4(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[1459,699,1958,2,3])).
% 59.78/59.92 cnf(1967,plain,
% 59.78/59.92 (E(f3(x19671,f2(a5)),f3(x19671,f4(a6)))),
% 59.78/59.92 inference(rename_variables,[],[1459])).
% 59.78/59.92 cnf(1968,plain,
% 59.78/59.92 (P2(f2(a5),f3(f4(f2(a5)),f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1459,1967,699,1958,236,2,3,12])).
% 59.78/59.92 cnf(1974,plain,
% 59.78/59.92 (E(f3(a5,f2(a5)),f3(f4(a5),a5))),
% 59.78/59.92 inference(scs_inference,[],[1459,1478,1966,2,3])).
% 59.78/59.92 cnf(1982,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f2(a5)),f2(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[1459,1609,1974,2,3])).
% 59.78/59.92 cnf(1990,plain,
% 59.78/59.92 (E(f3(f4(f4(a6)),f2(a5)),f4(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1459,1484,1982,2,3])).
% 59.78/59.92 cnf(1998,plain,
% 59.78/59.92 (E(f3(f3(a5,f2(a5)),f2(a5)),f3(f4(a5),a5))),
% 59.78/59.92 inference(scs_inference,[],[1459,1990,1747,2,3])).
% 59.78/59.92 cnf(2006,plain,
% 59.78/59.92 (E(f3(f3(a5,f2(a5)),f2(a5)),a5)),
% 59.78/59.92 inference(scs_inference,[],[1459,1998,1743,2,3])).
% 59.78/59.92 cnf(2015,plain,
% 59.78/59.92 (E(f3(x20151,f2(a5)),f3(x20151,f4(a6)))),
% 59.78/59.92 inference(rename_variables,[],[1459])).
% 59.78/59.92 cnf(2016,plain,
% 59.78/59.92 (P2(f3(f4(f2(a5)),f4(a6)),f2(a5))),
% 59.78/59.92 inference(scs_inference,[],[1459,2015,2006,338,420,2,12,11])).
% 59.78/59.92 cnf(2027,plain,
% 59.78/59.92 (E(f4(f4(a6)),f2(f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[1471,632,1247,23,3])).
% 59.78/59.92 cnf(2033,plain,
% 59.78/59.92 (E(f4(f4(a6)),f2(f2(a5)))),
% 59.78/59.92 inference(scs_inference,[],[1471,1599,3])).
% 59.78/59.92 cnf(2059,plain,
% 59.78/59.92 (E(f4(f3(a5,f4(a6))),f4(a5))),
% 59.78/59.92 inference(scs_inference,[],[1704,440,1474,34,27,4,7])).
% 59.78/59.92 cnf(2070,plain,
% 59.78/59.92 (P1(f3(f4(f8(a1,a7)),f8(a1,a7)))),
% 59.78/59.92 inference(scs_inference,[],[2016,1401,503,1704,440,1474,34,27,4,7,5,6,8,9,31,30,22,25])).
% 59.78/59.92 cnf(2072,plain,
% 59.78/59.92 (P1(f3(f3(a6,f2(a6)),f2(a6)))),
% 59.78/59.92 inference(scs_inference,[],[2016,1401,503,1864,1704,440,1474,34,27,4,7,5,6,8,9,31,30,22,25,24])).
% 59.78/59.92 cnf(2074,plain,
% 59.78/59.92 (~E(a7,a1)),
% 59.78/59.92 inference(scs_inference,[],[19,2016,1401,503,1864,1704,440,1474,34,27,4,7,5,6,8,9,31,30,22,25,24,2])).
% 59.78/59.92 cnf(2075,plain,
% 59.78/59.92 (~E(f3(a1,f3(a5,a6)),f3(f3(a7,a5),a6))),
% 59.78/59.92 inference(scs_inference,[],[19,2016,1401,503,1864,1704,440,1474,74,34,27,4,7,5,6,8,9,31,30,22,25,24,2,33])).
% 59.78/59.92 cnf(2078,plain,
% 59.78/59.92 (P1(f3(f4(a6),f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[19,2016,1401,503,2027,1864,1704,440,1474,636,74,34,27,4,7,5,6,8,9,31,30,22,25,24,2,33,32])).
% 59.78/59.92 cnf(2099,plain,
% 59.78/59.92 (E(f3(a5,x20991),f3(f3(a5,f4(a6)),x20991))),
% 59.78/59.92 inference(scs_inference,[],[2078,1627,1466,6,9,34,27,8,7,4,5])).
% 59.78/59.92 cnf(2106,plain,
% 59.78/59.92 (P1(f3(f3(a1,f2(a1)),f2(a1)))),
% 59.78/59.92 inference(scs_inference,[],[2078,2072,2070,1968,1882,1627,1466,6,9,34,27,8,7,4,5,31,30,22,25])).
% 59.78/59.92 cnf(2110,plain,
% 59.78/59.92 (~E(f3(f3(a7,a5),a6),f3(a1,f3(a5,a6)))),
% 59.78/59.92 inference(scs_inference,[],[2078,2072,2070,1968,2075,1882,1606,1627,1466,6,9,34,27,8,7,4,5,31,30,22,25,24,2])).
% 59.78/59.92 cnf(2111,plain,
% 59.78/59.92 (~E(f3(f3(a1,f2(a1)),f3(a5,a6)),f3(a7,f3(a5,a6)))),
% 59.78/59.92 inference(scs_inference,[],[2078,2072,2070,1968,2075,1882,1606,443,1627,1466,1407,6,9,34,27,8,7,4,5,31,30,22,25,24,2,33])).
% 59.78/59.92 cnf(2145,plain,
% 59.78/59.92 (P1(f3(f2(a5),f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[2106,1601,1897,1887,1689,1700,446,2033,1610,64,16,1407,27,34,7,6,4,9,5,8,31,30,22,24,2,33,32])).
% 59.78/59.92 cnf(2149,plain,
% 59.78/59.92 (P2(a5,f3(f3(a5,f4(a6)),f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[2074,1960,2106,1601,1897,1887,1689,2099,1700,446,2033,1610,1638,64,16,1407,27,34,7,6,4,9,5,8,31,30,22,24,2,33,32,3,12])).
% 59.78/59.92 cnf(2163,plain,
% 59.78/59.92 (E(f3(f3(a7,a5),x21631),f3(f3(a1,a5),x21631))),
% 59.78/59.92 inference(scs_inference,[],[2145,75,37,27,34,9,7,6,5])).
% 59.78/59.92 cnf(2172,plain,
% 59.78/59.92 (P1(f3(f3(a5,f4(a6)),f4(a6)))),
% 59.78/59.92 inference(scs_inference,[],[2145,1299,1463,2149,75,37,27,34,9,7,6,5,8,4,30,31,22,24])).
% 59.78/59.92 cnf(2211,plain,
% 59.78/59.92 ($false),
% 59.78/59.92 inference(scs_inference,[],[2163,2172,2110,2059,2111,1885,1696,873,18,636,92,15,34,9,7,6,5,8,4,30,31,22,2,32,23,3]),
% 59.78/59.92 ['proof']).
% 59.78/59.92 % SZS output end Proof
% 59.78/59.92 % Total time :59.150000s
%------------------------------------------------------------------------------