%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT004-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 : n011.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:10 EDT 2024
% Result : Unsatisfiable 59.33s 59.35s
% Output : CNFRefutation 59.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : CAT004-4 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jun 18 12:36:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 59.23/59.34 %-------------------------------------------
% 59.23/59.34 % File :CSE---1.7
% 59.23/59.34 % Problem :theBenchmark
% 59.23/59.34 % Transform :cnf
% 59.23/59.34 % Format :tptp:raw
% 59.23/59.34 % Command :java -jar mcs_scs.jar %d %s
% 59.23/59.34
% 59.23/59.34 % Result :Theorem 58.730000s
% 59.23/59.34 % Output :CNFRefutation 58.730000s
% 59.23/59.34 %-------------------------------------------
% 59.33/59.35 %--------------------------------------------------------------------------
% 59.33/59.35 % File : CAT004-4 : TPTP v8.2.0. Released v1.0.0.
% 59.33/59.35 % Domain : Category Theory
% 59.33/59.35 % Problem : X and Y epimorphisms, XY well-defined => XY epimorphism
% 59.33/59.35 % Version : [Sco79] axioms : Reduced > Complete.
% 59.33/59.35 % English : If x and y are epimorphisms and xy is well-defined, then
% 59.33/59.35 % xy is an epimorphism.
% 59.33/59.35
% 59.33/59.35 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 59.33/59.35 % Source : [TPTP]
% 59.33/59.35 % Names :
% 59.33/59.35
% 59.33/59.35 % Status : Unsatisfiable
% 59.33/59.35 % Rating : 0.12 v8.2.0, 0.08 v8.1.0, 0.00 v7.5.0, 0.10 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v7.0.0, 0.00 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.31 v5.4.0, 0.27 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.20 v2.4.0, 0.17 v2.2.1, 0.33 v2.2.0, 0.14 v2.1.0, 0.40 v2.0.0
% 59.33/59.35 % Syntax : Number of clauses : 17 ( 7 unt; 0 nHn; 14 RR)
% 59.33/59.35 % Number of literals : 31 ( 15 equ; 15 neg)
% 59.33/59.35 % Maximal clause size : 3 ( 1 avg)
% 59.33/59.35 % Maximal term depth : 3 ( 1 avg)
% 59.33/59.35 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 59.33/59.35 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 59.33/59.35 % Number of variables : 25 ( 2 sgn)
% 59.33/59.35 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.33/59.35
% 59.33/59.35 % Comments : The dependent axioms have been removed.
% 59.33/59.35 %--------------------------------------------------------------------------
% 59.33/59.35 %----Include Scott's axioms for category theory
% 59.33/59.35 include('Axioms/CAT004-0.ax').
% 59.33/59.35 %--------------------------------------------------------------------------
% 59.33/59.35 cnf(assume_ab_exists,hypothesis,
% 59.33/59.35 there_exists(compose(a,b)) ).
% 59.33/59.35
% 59.33/59.35 cnf(cancellation_for_product1,hypothesis,
% 59.33/59.35 ( compose(X,a) != Y
% 59.33/59.35 | compose(Z,a) != Y
% 59.33/59.35 | X = Z ) ).
% 59.33/59.35
% 59.33/59.35 cnf(cancellation_for_product2,hypothesis,
% 59.33/59.35 ( compose(X,b) != Y
% 59.33/59.35 | compose(Z,b) != Y
% 59.33/59.35 | X = Z ) ).
% 59.33/59.35
% 59.33/59.35 cnf(assume_h_exists,hypothesis,
% 59.33/59.35 there_exists(h) ).
% 59.33/59.35
% 59.33/59.35 cnf(h_ab_equals_g_ab,hypothesis,
% 59.33/59.35 compose(h,compose(a,b)) = compose(g,compose(a,b)) ).
% 59.33/59.35
% 59.33/59.35 cnf(prove_h_equals_g,negated_conjecture,
% 59.33/59.35 h != g ).
% 59.33/59.35
% 59.33/59.35 %--------------------------------------------------------------------------
% 59.33/59.35 %-------------------------------------------
% 59.33/59.35 % Proof found
% 59.33/59.35 % SZS status Theorem for theBenchmark
% 59.33/59.35 % SZS output start Proof
% 59.33/59.36 %ClaNum:27(EqnAxiom:10)
% 59.33/59.36 %VarNum:52(SingletonVarNum:25)
% 59.33/59.36 %MaxLitNum:3
% 59.33/59.36 %MaxfuncDepth:2
% 59.33/59.36 %SharedTerms:11
% 59.33/59.36 %goalClause: 17
% 59.33/59.36 %singleGoalClaCount:1
% 59.33/59.36 [11]P1(a1)
% 59.33/59.36 [17]~E(a1,a7)
% 59.33/59.36 [14]P1(f3(a5,a6))
% 59.33/59.36 [15]E(f3(a1,f3(a5,a6)),f3(a7,f3(a5,a6)))
% 59.33/59.36 [12]E(f3(x121,f2(x121)),x121)
% 59.33/59.36 [13]E(f3(f4(x131),x131),x131)
% 59.33/59.36 [16]E(f3(f3(x161,x162),x163),f3(x161,f3(x162,x163)))
% 59.33/59.36 [18]P1(x181)+~P1(f2(x181))
% 59.33/59.36 [19]P1(x191)+~P1(f4(x191))
% 59.33/59.36 [20]~P2(x201,x202)+E(x201,x202)
% 59.33/59.36 [22]P1(x221)+~P2(x221,x222)
% 59.33/59.36 [25]E(f4(x251),f2(x252))+~P1(f3(x252,x251))
% 59.33/59.36 [26]P1(f2(x261))+~P1(f3(x261,x262))
% 59.33/59.36 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 59.33/59.36 [27]~E(f4(x272),f2(x271))+~P1(f2(x271))+P1(f3(x271,x272))
% 59.33/59.36 [23]E(x231,x232)+~E(f3(x231,a5),x233)+~E(f3(x232,a5),x233)
% 59.33/59.36 [24]E(x241,x242)+~E(f3(x241,a6),x243)+~E(f3(x242,a6),x243)
% 59.33/59.36 %EqnAxiom
% 59.33/59.36 [1]E(x11,x11)
% 59.33/59.36 [2]E(x22,x21)+~E(x21,x22)
% 59.33/59.36 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.33/59.36 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 59.33/59.36 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 59.33/59.36 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 59.33/59.36 [7]~E(x71,x72)+E(f4(x71),f4(x72))
% 59.33/59.36 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 59.33/59.36 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93)
% 59.33/59.36 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101)
% 59.33/59.36
% 59.33/59.36 %-------------------------------------------
% 59.33/59.37 cnf(28,plain,
% 59.33/59.37 (~P1(x281)+P2(x281,x281)),
% 59.33/59.37 inference(equality_inference,[],[21])).
% 59.33/59.37 cnf(29,plain,
% 59.33/59.37 (~P2(a1,a7)),
% 59.33/59.37 inference(scs_inference,[],[17,20])).
% 59.33/59.37 cnf(31,plain,
% 59.33/59.37 (E(x311,f3(x311,f2(x311)))),
% 59.33/59.37 inference(scs_inference,[],[17,12,20,2])).
% 59.33/59.37 cnf(32,plain,
% 59.33/59.37 (E(f4(a6),f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[17,12,14,20,2,25])).
% 59.33/59.37 cnf(36,plain,
% 59.33/59.37 (~E(a1,f3(f4(a7),a7))),
% 59.33/59.37 inference(scs_inference,[],[17,12,13,14,20,2,25,21,3])).
% 59.33/59.37 cnf(38,plain,
% 59.33/59.37 (P1(f3(f3(a5,a6),f2(f3(a5,a6))))),
% 59.33/59.37 inference(scs_inference,[],[17,12,13,14,20,2,25,21,3,8])).
% 59.33/59.37 cnf(42,plain,
% 59.33/59.37 (E(f2(a5),f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[32,2])).
% 59.33/59.37 cnf(43,plain,
% 59.33/59.37 (~P2(a1,f3(f4(a7),a7))),
% 59.33/59.37 inference(scs_inference,[],[36,32,2,20])).
% 59.33/59.37 cnf(45,plain,
% 59.33/59.37 (E(f4(a6),f3(f2(a5),f2(f2(a5))))),
% 59.33/59.37 inference(scs_inference,[],[31,36,32,2,20,3])).
% 59.33/59.37 cnf(47,plain,
% 59.33/59.37 (~P1(f4(a6))+P1(f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[31,36,32,2,20,3,8])).
% 59.33/59.37 cnf(48,plain,
% 59.33/59.37 (~P2(f4(a6),x481)+P1(f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[31,36,32,2,20,3,8,22])).
% 59.33/59.37 cnf(51,plain,
% 59.33/59.37 (E(f3(f2(a5),f2(f2(a5))),f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[45,2])).
% 59.33/59.37 cnf(52,plain,
% 59.33/59.37 (E(f3(f4(f2(a5)),f2(a5)),f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[45,42,13,2,3])).
% 59.33/59.37 cnf(54,plain,
% 59.33/59.37 (~P1(f4(a6))+P1(f3(f2(a5),f2(f2(a5))))),
% 59.33/59.37 inference(scs_inference,[],[45,42,13,2,3,8])).
% 59.33/59.37 cnf(55,plain,
% 59.33/59.37 (~P2(f4(a6),x551)+P1(f3(f2(a5),f2(f2(a5))))),
% 59.33/59.37 inference(scs_inference,[],[45,42,13,2,3,8,22])).
% 59.33/59.37 cnf(58,plain,
% 59.33/59.37 (E(f4(a6),f3(f4(f2(a5)),f2(a5)))),
% 59.33/59.37 inference(scs_inference,[],[52,2])).
% 59.33/59.37 cnf(59,plain,
% 59.33/59.37 (E(f3(f3(a1,a5),a6),f3(a7,f3(a5,a6)))),
% 59.33/59.37 inference(scs_inference,[],[52,16,15,2,3])).
% 59.33/59.37 cnf(61,plain,
% 59.33/59.37 (~P1(f3(f2(a5),f2(f2(a5))))+P1(f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[51,52,16,15,2,3,8])).
% 59.33/59.37 cnf(69,plain,
% 59.33/59.37 (E(f3(a7,f3(a5,a6)),f3(f3(a1,a5),a6))),
% 59.33/59.37 inference(scs_inference,[],[59,2])).
% 59.33/59.37 cnf(78,plain,
% 59.33/59.37 (E(f3(x781,f3(x782,x783)),f3(f3(x781,x782),x783))),
% 59.33/59.37 inference(scs_inference,[],[16,2])).
% 59.33/59.37 cnf(79,plain,
% 59.33/59.37 (E(f3(a7,f3(a5,a6)),f3(a1,f3(a5,a6)))),
% 59.33/59.37 inference(scs_inference,[],[69,16,2,3])).
% 59.33/59.37 cnf(90,plain,
% 59.33/59.37 (E(x901,f3(f4(x901),x901))),
% 59.33/59.37 inference(scs_inference,[],[13,2])).
% 59.33/59.37 cnf(91,plain,
% 59.33/59.37 (E(f3(f4(f3(x911,a5)),x911),x911)),
% 59.33/59.37 inference(scs_inference,[],[13,16,2,23])).
% 59.33/59.37 cnf(97,plain,
% 59.33/59.37 (~P1(f3(x971,f3(x972,x973)))+P1(f3(f3(x971,x972),x973))),
% 59.33/59.37 inference(scs_inference,[],[17,78,13,16,2,23,3,20,8])).
% 59.33/59.37 cnf(98,plain,
% 59.33/59.37 (~P1(f3(x981,f3(x982,x983)))+E(f4(x983),f2(f3(x981,x982)))),
% 59.33/59.37 inference(scs_inference,[],[17,78,13,16,2,23,3,20,8,25])).
% 59.33/59.37 cnf(100,plain,
% 59.33/59.37 (E(x1001,f3(f4(f3(x1001,a5)),x1001))),
% 59.33/59.37 inference(scs_inference,[],[91,2])).
% 59.33/59.37 cnf(108,plain,
% 59.33/59.37 (~P1(f4(a6))+P1(f3(f4(f2(a5)),f2(a5)))),
% 59.33/59.37 inference(scs_inference,[],[58,8])).
% 59.33/59.37 cnf(140,plain,
% 59.33/59.37 (~P1(f2(a5))+P1(f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[42,8])).
% 59.33/59.37 cnf(154,plain,
% 59.33/59.37 (P1(x1541)+~P1(f2(f4(x1541)))),
% 59.33/59.37 inference(scs_inference,[],[18,19])).
% 59.33/59.37 cnf(155,plain,
% 59.33/59.37 (P1(f3(f4(f3(a1,a5)),a1))),
% 59.33/59.37 inference(scs_inference,[],[11,100,8])).
% 59.33/59.37 cnf(157,plain,
% 59.33/59.37 (E(f4(a1),f2(f4(f3(a1,a5))))),
% 59.33/59.37 inference(scs_inference,[],[11,100,8,25])).
% 59.33/59.37 cnf(159,plain,
% 59.33/59.37 (E(f2(f4(f3(a1,a5))),f4(a1))),
% 59.33/59.37 inference(scs_inference,[],[11,100,8,25,2])).
% 59.33/59.37 cnf(161,plain,
% 59.33/59.37 (E(f3(f4(f3(x1611,a5)),x1611),x1611)),
% 59.33/59.37 inference(rename_variables,[],[91])).
% 59.33/59.37 cnf(163,plain,
% 59.33/59.37 (P2(a1,a1)),
% 59.33/59.37 inference(scs_inference,[],[11,91,161,100,8,25,2,21,9])).
% 59.33/59.37 cnf(165,plain,
% 59.33/59.37 (P2(f3(a1,f2(a1)),a1)),
% 59.33/59.37 inference(scs_inference,[],[11,31,28,9])).
% 59.33/59.37 cnf(166,plain,
% 59.33/59.37 (P2(f3(a1,f2(a1)),f3(f4(a1),a1))),
% 59.33/59.37 inference(scs_inference,[],[90,165,10])).
% 59.33/59.37 cnf(167,plain,
% 59.33/59.37 (E(x1671,f3(f4(x1671),x1671))),
% 59.33/59.37 inference(rename_variables,[],[90])).
% 59.33/59.37 cnf(168,plain,
% 59.33/59.37 (P2(f3(f4(a1),a1),a1)),
% 59.33/59.37 inference(scs_inference,[],[90,167,163,165,10,9])).
% 59.33/59.37 cnf(169,plain,
% 59.33/59.37 (E(x1691,f3(f4(x1691),x1691))),
% 59.33/59.37 inference(rename_variables,[],[90])).
% 59.33/59.37 cnf(170,plain,
% 59.33/59.37 (P1(f3(f4(a1),a1))),
% 59.33/59.37 inference(scs_inference,[],[11,90,167,169,163,165,10,9,8])).
% 59.33/59.37 cnf(172,plain,
% 59.33/59.37 (E(f4(a1),f2(f4(a1)))),
% 59.33/59.37 inference(scs_inference,[],[11,90,167,169,163,165,10,9,8,25])).
% 59.33/59.37 cnf(174,plain,
% 59.33/59.37 (E(f2(f4(a1)),f4(a1))),
% 59.33/59.37 inference(scs_inference,[],[11,90,167,169,163,165,10,9,8,25,2])).
% 59.33/59.37 cnf(175,plain,
% 59.33/59.37 (~P1(f3(f2(a5),f2(f2(a5))))+P1(f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[47,61])).
% 59.33/59.37 cnf(176,plain,
% 59.33/59.37 (P1(f3(a1,f2(a1)))),
% 59.33/59.37 inference(scs_inference,[],[11,31,8])).
% 59.33/59.37 cnf(178,plain,
% 59.33/59.37 (E(f4(f2(a1)),f2(a1))),
% 59.33/59.37 inference(scs_inference,[],[11,31,8,25])).
% 59.33/59.37 cnf(180,plain,
% 59.33/59.37 (E(f2(a1),f4(f2(a1)))),
% 59.33/59.37 inference(scs_inference,[],[11,31,8,25,2])).
% 59.33/59.37 cnf(181,plain,
% 59.33/59.37 (P1(f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[14,140,26])).
% 59.33/59.37 cnf(182,plain,
% 59.33/59.37 (P1(f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[181,47])).
% 59.33/59.37 cnf(183,plain,
% 59.33/59.37 (P1(f3(f2(a5),f2(f2(a5))))),
% 59.33/59.37 inference(scs_inference,[],[181,54])).
% 59.33/59.37 cnf(184,plain,
% 59.33/59.37 (P1(f3(f4(f2(a5)),f2(a5)))),
% 59.33/59.37 inference(scs_inference,[],[181,108])).
% 59.33/59.37 cnf(185,plain,
% 59.33/59.37 (P1(a6)),
% 59.33/59.37 inference(scs_inference,[],[181,19])).
% 59.33/59.37 cnf(187,plain,
% 59.33/59.37 (P2(f4(a6),f3(f4(f2(a5)),f2(a5)))),
% 59.33/59.37 inference(scs_inference,[],[58,181,19,21])).
% 59.33/59.37 cnf(189,plain,
% 59.33/59.37 (P2(f4(a6),f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[58,52,181,19,21,10])).
% 59.33/59.37 cnf(191,plain,
% 59.33/59.37 (~P1(f2(f4(f3(a1,a5))))+P1(f4(a1))),
% 59.33/59.37 inference(scs_inference,[],[58,52,159,181,19,21,10,9,8])).
% 59.33/59.37 cnf(193,plain,
% 59.33/59.37 (~P2(f2(f4(f3(a1,a5))),x1931)+P1(f4(a1))),
% 59.33/59.37 inference(scs_inference,[],[58,52,159,155,181,19,21,10,9,8,26,22])).
% 59.33/59.37 cnf(195,plain,
% 59.33/59.37 (P1(f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[187,48])).
% 59.33/59.37 cnf(196,plain,
% 59.33/59.37 (P1(f3(f2(a5),f2(f2(a5))))),
% 59.33/59.37 inference(scs_inference,[],[187,55])).
% 59.33/59.37 cnf(199,plain,
% 59.33/59.37 (P1(f2(a5))),
% 59.33/59.37 inference(scs_inference,[],[183,175])).
% 59.33/59.37 cnf(200,plain,
% 59.33/59.37 (P1(f3(a1,a5))),
% 59.33/59.37 inference(scs_inference,[],[155,154,26])).
% 59.33/59.37 cnf(201,plain,
% 59.33/59.37 (P1(a5)),
% 59.33/59.37 inference(scs_inference,[],[182,18])).
% 59.33/59.37 cnf(203,plain,
% 59.33/59.37 (E(f4(a5),f2(a1))),
% 59.33/59.37 inference(scs_inference,[],[200,182,18,25])).
% 59.33/59.37 cnf(205,plain,
% 59.33/59.37 (E(f2(a1),f4(a5))),
% 59.33/59.37 inference(scs_inference,[],[200,182,18,25,2])).
% 59.33/59.37 cnf(208,plain,
% 59.33/59.37 (~P1(f2(a1))+P1(f4(f2(a1)))),
% 59.33/59.37 inference(scs_inference,[],[51,180,200,183,182,18,25,2,21,8])).
% 59.33/59.37 cnf(216,plain,
% 59.33/59.37 (E(x2161,f3(f4(f3(x2161,a5)),x2161))),
% 59.33/59.37 inference(rename_variables,[],[100])).
% 59.33/59.37 cnf(218,plain,
% 59.33/59.37 (P2(a6,a6)),
% 59.33/59.37 inference(scs_inference,[],[91,100,185,21,10])).
% 59.33/59.37 cnf(222,plain,
% 59.33/59.37 (~P1(f2(a1))+P1(f4(a5))),
% 59.33/59.37 inference(scs_inference,[],[91,100,216,205,185,21,10,9,8])).
% 59.33/59.37 cnf(227,plain,
% 59.33/59.37 (E(x2271,f3(f4(x2271),x2271))),
% 59.33/59.37 inference(rename_variables,[],[90])).
% 59.33/59.37 cnf(230,plain,
% 59.33/59.37 (E(x2301,f3(f4(x2301),x2301))),
% 59.33/59.37 inference(rename_variables,[],[90])).
% 59.33/59.37 cnf(231,plain,
% 59.33/59.37 (P2(f3(f4(a6),a6),a6)),
% 59.33/59.37 inference(scs_inference,[],[90,227,230,195,168,218,21,10,9])).
% 59.33/59.37 cnf(238,plain,
% 59.33/59.37 (P1(f4(a5))),
% 59.33/59.37 inference(scs_inference,[],[176,222,26])).
% 59.33/59.37 cnf(239,plain,
% 59.33/59.37 (P2(f2(a5),f3(f2(a5),f2(f2(a5))))),
% 59.33/59.37 inference(scs_inference,[],[31,199,21])).
% 59.33/59.37 cnf(240,plain,
% 59.33/59.37 (E(x2401,f3(x2401,f2(x2401)))),
% 59.33/59.37 inference(rename_variables,[],[31])).
% 59.33/59.37 cnf(242,plain,
% 59.33/59.37 (P2(f3(f4(a6),a6),f3(a6,f2(a6)))),
% 59.33/59.37 inference(scs_inference,[],[31,240,199,231,21,10])).
% 59.33/59.37 cnf(243,plain,
% 59.33/59.37 (E(x2431,f3(x2431,f2(x2431)))),
% 59.33/59.37 inference(rename_variables,[],[31])).
% 59.33/59.37 cnf(244,plain,
% 59.33/59.37 (P2(f3(a6,f2(a6)),a6)),
% 59.33/59.37 inference(scs_inference,[],[31,240,243,199,231,218,21,10,9])).
% 59.33/59.37 cnf(246,plain,
% 59.33/59.37 (P1(f2(a1))),
% 59.33/59.37 inference(scs_inference,[],[31,240,243,203,199,238,231,218,21,10,9,8])).
% 59.33/59.37 cnf(247,plain,
% 59.33/59.37 (P1(f4(f2(a1)))),
% 59.33/59.37 inference(scs_inference,[],[31,240,243,203,199,238,231,218,21,10,9,8,208])).
% 59.33/59.37 cnf(249,plain,
% 59.33/59.37 (P2(f3(a1,a5),f3(f3(a1,a5),f2(f3(a1,a5))))),
% 59.33/59.37 inference(scs_inference,[],[31,200,21])).
% 59.33/59.37 cnf(252,plain,
% 59.33/59.37 (P2(f2(a5),f4(a6))),
% 59.33/59.37 inference(scs_inference,[],[51,31,239,200,21,10])).
% 59.33/59.37 cnf(255,plain,
% 59.33/59.37 (P1(f2(f4(a1)))+~P1(f2(f4(f3(a1,a5))))),
% 59.33/59.37 inference(scs_inference,[],[51,31,239,172,200,21,10,8,193,191])).
% 59.33/59.37 cnf(264,plain,
% 59.33/59.37 (P2(a5,a5)),
% 59.33/59.37 inference(scs_inference,[],[91,100,201,21,10])).
% 59.33/59.37 cnf(268,plain,
% 59.33/59.37 (P2(f3(a1,a5),f3(f4(f3(a1,a5)),f3(a1,a5)))),
% 59.33/59.37 inference(scs_inference,[],[90,200,21])).
% 59.33/59.37 cnf(269,plain,
% 59.33/59.37 (E(x2691,f3(f4(x2691),x2691))),
% 59.33/59.37 inference(rename_variables,[],[90])).
% 59.33/59.37 cnf(271,plain,
% 59.33/59.37 (P2(f3(a6,f2(a6)),f3(f4(a6),a6))),
% 59.33/59.37 inference(scs_inference,[],[90,269,200,244,21,10])).
% 59.33/59.37 cnf(278,plain,
% 59.33/59.37 (E(f3(x2781,f2(x2781)),x2781)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(280,plain,
% 59.33/59.38 (E(f3(f2(a1),f2(f2(a1))),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[12,278,205,196,21,3])).
% 59.33/59.38 cnf(281,plain,
% 59.33/59.38 (E(f3(x2811,f2(x2811)),x2811)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(283,plain,
% 59.33/59.38 (E(f3(x2831,f2(x2831)),x2831)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(287,plain,
% 59.33/59.38 (P1(f3(f2(a1),f2(f2(a1))))),
% 59.33/59.38 inference(scs_inference,[],[12,278,281,283,205,249,238,271,196,21,3,10,9,2,8])).
% 59.33/59.38 cnf(289,plain,
% 59.33/59.38 (P2(f3(f2(a1),f2(f2(a1))),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[12,287,21])).
% 59.33/59.38 cnf(290,plain,
% 59.33/59.38 (E(f3(x2901,f2(x2901)),x2901)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(293,plain,
% 59.33/59.38 (E(f3(x2931,f2(x2931)),x2931)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(295,plain,
% 59.33/59.38 (E(f3(x2951,f2(x2951)),x2951)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(296,plain,
% 59.33/59.38 (P2(a1,f3(f4(a1),a1))),
% 59.33/59.38 inference(scs_inference,[],[12,290,293,295,239,32,287,166,21,3,10,9])).
% 59.33/59.38 cnf(299,plain,
% 59.33/59.38 (P1(f3(f4(a6),f2(f4(a6))))),
% 59.33/59.38 inference(scs_inference,[],[12,290,293,295,239,32,182,287,166,21,3,10,9,2,8])).
% 59.33/59.38 cnf(300,plain,
% 59.33/59.38 (P2(f3(f4(a6),f2(f4(a6))),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[12,299,21])).
% 59.33/59.38 cnf(301,plain,
% 59.33/59.38 (E(f3(x3011,f2(x3011)),x3011)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(303,plain,
% 59.33/59.38 (E(f3(f4(a5),f2(f4(a5))),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[12,301,203,299,21,3])).
% 59.33/59.38 cnf(304,plain,
% 59.33/59.38 (E(f3(x3041,f2(x3041)),x3041)),
% 59.33/59.38 inference(rename_variables,[],[12])).
% 59.33/59.38 cnf(311,plain,
% 59.33/59.38 (P1(f3(f4(a5),f2(f4(a5))))),
% 59.33/59.38 inference(scs_inference,[],[12,301,304,29,289,203,246,299,296,21,3,10,9,20,2,8])).
% 59.33/59.38 cnf(316,plain,
% 59.33/59.38 (~E(f3(f4(a1),a1),f3(f4(a7),a7))),
% 59.33/59.38 inference(scs_inference,[],[12,43,311,296,21,10])).
% 59.33/59.38 cnf(325,plain,
% 59.33/59.38 (E(f3(x3251,x3252),f3(x3251,f3(x3252,f2(x3252))))),
% 59.33/59.38 inference(scs_inference,[],[12,6,2])).
% 59.33/59.38 cnf(327,plain,
% 59.33/59.38 (~E(a1,f3(f4(a7),f3(a7,f2(a7))))),
% 59.33/59.38 inference(scs_inference,[],[36,325,2,3])).
% 59.33/59.38 cnf(338,plain,
% 59.33/59.38 (P1(f3(a5,f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[327,14,16,325,3,8])).
% 59.33/59.38 cnf(340,plain,
% 59.33/59.38 (E(f4(f3(a6,f2(a6))),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[327,14,16,325,3,8,25])).
% 59.33/59.38 cnf(342,plain,
% 59.33/59.38 (~P2(a1,f3(f3(f4(a7),a7),f2(a7)))),
% 59.33/59.38 inference(scs_inference,[],[327,14,16,325,3,8,25,20])).
% 59.33/59.38 cnf(344,plain,
% 59.33/59.38 (E(f2(a5),f4(f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[327,14,16,325,3,8,25,20,2])).
% 59.33/59.38 cnf(346,plain,
% 59.33/59.38 (P1(f4(f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[344,195,8])).
% 59.33/59.38 cnf(347,plain,
% 59.33/59.38 (P1(f3(a6,f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[344,195,8,19])).
% 59.33/59.38 cnf(349,plain,
% 59.33/59.38 (E(f4(f2(a6)),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[344,195,8,19,25])).
% 59.33/59.38 cnf(351,plain,
% 59.33/59.38 (E(f2(a6),f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[344,195,8,19,25,2])).
% 59.33/59.38 cnf(352,plain,
% 59.33/59.38 (P1(f2(f4(a1)))),
% 59.33/59.38 inference(scs_inference,[],[155,255,26])).
% 59.33/59.38 cnf(353,plain,
% 59.33/59.38 (P1(f4(a1))),
% 59.33/59.38 inference(scs_inference,[],[352,18])).
% 59.33/59.38 cnf(358,plain,
% 59.33/59.38 (P1(f2(f4(f3(a1,a5))))),
% 59.33/59.38 inference(scs_inference,[],[174,157,352,18,21,9,8])).
% 59.33/59.38 cnf(364,plain,
% 59.33/59.38 (~P1(f2(a6))+P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[159,351,358,21,8])).
% 59.33/59.38 cnf(366,plain,
% 59.33/59.38 (~P2(f2(a6),x3661)+P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[159,351,347,358,21,8,26,22])).
% 59.33/59.38 cnf(372,plain,
% 59.33/59.38 (E(f4(f2(a6)),f2(f3(a5,a6)))),
% 59.33/59.38 inference(scs_inference,[],[78,338,8,25])).
% 59.33/59.38 cnf(374,plain,
% 59.33/59.38 (E(f2(f3(a5,a6)),f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[78,338,8,25,2])).
% 59.33/59.38 cnf(375,plain,
% 59.33/59.38 (~P1(f2(f3(a5,a6)))+P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[374,8])).
% 59.33/59.38 cnf(377,plain,
% 59.33/59.38 (~P2(f2(f3(a5,a6)),x3771)+P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[374,38,8,26,22])).
% 59.33/59.38 cnf(380,plain,
% 59.33/59.38 (P2(f4(f2(a6)),f4(f2(a6)))+~P2(f2(a6),x3801)),
% 59.33/59.38 inference(scs_inference,[],[366,28])).
% 59.33/59.38 cnf(381,plain,
% 59.33/59.38 (~P1(f4(f2(a6)))+P1(f2(f3(a5,a6)))),
% 59.33/59.38 inference(scs_inference,[],[372,8])).
% 59.33/59.38 cnf(393,plain,
% 59.33/59.38 (~P1(f4(f2(a6)))+P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[381,375])).
% 59.33/59.38 cnf(395,plain,
% 59.33/59.38 (E(f3(f4(x3951),x3951),x3951)),
% 59.33/59.38 inference(rename_variables,[],[13])).
% 59.33/59.38 cnf(398,plain,
% 59.33/59.38 (E(f3(f4(x3981),x3981),x3981)),
% 59.33/59.38 inference(rename_variables,[],[13])).
% 59.33/59.38 cnf(399,plain,
% 59.33/59.38 (P2(f4(a6),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[13,395,398,205,187,184,21,3,10])).
% 59.33/59.38 cnf(400,plain,
% 59.33/59.38 (E(f3(f4(x4001),x4001),x4001)),
% 59.33/59.38 inference(rename_variables,[],[13])).
% 59.33/59.38 cnf(404,plain,
% 59.33/59.38 (P1(f3(f4(f2(a1)),f2(a1)))),
% 59.33/59.38 inference(scs_inference,[],[13,395,398,400,205,187,238,242,184,21,3,10,9,2,8])).
% 59.33/59.38 cnf(405,plain,
% 59.33/59.38 (P1(f2(a6))+~P2(f2(f3(a5,a6)),x4051)),
% 59.33/59.38 inference(scs_inference,[],[377,19])).
% 59.33/59.38 cnf(406,plain,
% 59.33/59.38 (P2(f3(f4(f2(a1)),f2(a1)),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[13,404,21])).
% 59.33/59.38 cnf(412,plain,
% 59.33/59.38 (~P1(f2(f3(a5,a6)))+P1(f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[405,28])).
% 59.33/59.38 cnf(415,plain,
% 59.33/59.38 (E(f4(f2(a6)),f3(f4(f2(a6)),f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[13,351,3,2])).
% 59.33/59.38 cnf(420,plain,
% 59.33/59.38 (P1(f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[38,412,26])).
% 59.33/59.38 cnf(421,plain,
% 59.33/59.38 (P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[420,364])).
% 59.33/59.38 cnf(424,plain,
% 59.33/59.38 (E(f2(a5),f3(f4(f4(a6)),f4(a6)))),
% 59.33/59.38 inference(scs_inference,[],[13,32,3,2])).
% 59.33/59.38 cnf(425,plain,
% 59.33/59.38 (~P1(f4(f2(a6)))+P1(f3(f4(f2(a6)),f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[13,415,32,3,2,8])).
% 59.33/59.38 cnf(438,plain,
% 59.33/59.38 (P1(f2(f3(a5,a6)))),
% 59.33/59.38 inference(scs_inference,[],[421,381])).
% 59.33/59.38 cnf(439,plain,
% 59.33/59.38 (P1(f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[421,393])).
% 59.33/59.38 cnf(442,plain,
% 59.33/59.38 (P1(f3(f4(f2(a6)),f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[421,425])).
% 59.33/59.38 cnf(445,plain,
% 59.33/59.38 (E(f3(f4(x4451),x4451),x4451)),
% 59.33/59.38 inference(rename_variables,[],[13])).
% 59.33/59.38 cnf(447,plain,
% 59.33/59.38 (E(f2(f4(a1)),f3(f4(f4(a1)),f4(a1)))),
% 59.33/59.38 inference(scs_inference,[],[13,424,172,199,3,8,2])).
% 59.33/59.38 cnf(448,plain,
% 59.33/59.38 (P2(f3(f4(f4(a6)),f4(a6)),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[13,445,424,172,199,3,8,2,21])).
% 59.33/59.38 cnf(455,plain,
% 59.33/59.38 (E(f3(f4(x4551),x4551),x4551)),
% 59.33/59.38 inference(rename_variables,[],[13])).
% 59.33/59.38 cnf(458,plain,
% 59.33/59.38 (E(f3(f4(x4581),x4581),x4581)),
% 59.33/59.38 inference(rename_variables,[],[13])).
% 59.33/59.38 cnf(459,plain,
% 59.33/59.38 (P2(f2(a6),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[13,455,458,203,442,21,3,9])).
% 59.33/59.38 cnf(461,plain,
% 59.33/59.38 (P1(f3(f4(f4(a1)),f4(a1)))),
% 59.33/59.38 inference(scs_inference,[],[13,455,458,447,352,203,442,21,3,9,8])).
% 59.33/59.38 cnf(462,plain,
% 59.33/59.38 (E(f2(a1),f3(f4(f4(a5)),f4(a5)))),
% 59.33/59.38 inference(scs_inference,[],[13,455,458,447,352,203,442,21,3,9,8,2])).
% 59.33/59.38 cnf(464,plain,
% 59.33/59.38 (P2(f4(f2(a6)),f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[459,380])).
% 59.33/59.38 cnf(473,plain,
% 59.33/59.38 (P1(f3(f4(f4(a5)),f4(a5)))),
% 59.33/59.38 inference(scs_inference,[],[13,462,246,461,21,8])).
% 59.33/59.38 cnf(477,plain,
% 59.33/59.38 (P2(f3(f4(f4(a5)),f4(a5)),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[13,473,21])).
% 59.33/59.38 cnf(481,plain,
% 59.33/59.38 (P2(f4(a6),f3(f4(f4(a6)),f4(a6)))),
% 59.33/59.38 inference(scs_inference,[],[90,181,21])).
% 59.33/59.38 cnf(489,plain,
% 59.33/59.38 (P2(f4(a6),f3(f4(a6),f2(f4(a6))))),
% 59.33/59.38 inference(scs_inference,[],[31,181,21])).
% 59.33/59.38 cnf(490,plain,
% 59.33/59.38 (E(x4901,f3(x4901,f2(x4901)))),
% 59.33/59.38 inference(rename_variables,[],[31])).
% 59.33/59.38 cnf(493,plain,
% 59.33/59.38 (E(x4931,f3(x4931,f2(x4931)))),
% 59.33/59.38 inference(rename_variables,[],[31])).
% 59.33/59.38 cnf(494,plain,
% 59.33/59.38 (P2(f3(a5,f2(a5)),a5)),
% 59.33/59.38 inference(scs_inference,[],[31,490,493,181,264,21,10,9])).
% 59.33/59.38 cnf(497,plain,
% 59.33/59.38 (P2(f2(a1),f3(f4(f2(a1)),f2(a1)))),
% 59.33/59.38 inference(scs_inference,[],[90,246,21])).
% 59.33/59.38 cnf(498,plain,
% 59.33/59.38 (E(x4981,f3(f4(x4981),x4981))),
% 59.33/59.38 inference(rename_variables,[],[90])).
% 59.33/59.38 cnf(500,plain,
% 59.33/59.38 (P2(a5,f3(f4(a5),a5))),
% 59.33/59.38 inference(scs_inference,[],[90,498,246,264,21,10])).
% 59.33/59.38 cnf(511,plain,
% 59.33/59.38 (E(f3(f3(x5111,x5112),x5113),f3(x5111,f3(x5112,x5113)))),
% 59.33/59.38 inference(rename_variables,[],[16])).
% 59.33/59.38 cnf(513,plain,
% 59.33/59.38 (E(f3(f3(a7,a5),a6),f3(a1,f3(a5,a6)))),
% 59.33/59.38 inference(scs_inference,[],[16,511,79,90,24,3])).
% 59.33/59.38 cnf(515,plain,
% 59.33/59.38 (E(x5151,f3(f4(f3(x5151,a6)),x5151))),
% 59.33/59.38 inference(scs_inference,[],[16,511,79,90,24,3,2])).
% 59.33/59.38 cnf(519,plain,
% 59.33/59.38 (E(f3(f3(a7,a5),a6),f3(f3(a1,a5),a6))),
% 59.33/59.38 inference(scs_inference,[],[16,69,513,2,3])).
% 59.33/59.38 cnf(525,plain,
% 59.33/59.38 (E(f3(f3(a1,a5),a6),f3(f3(a7,a5),a6))),
% 59.33/59.38 inference(scs_inference,[],[519,2])).
% 59.33/59.38 cnf(565,plain,
% 59.33/59.38 (P2(f2(a1),f3(f2(a1),f2(f2(a1))))),
% 59.33/59.38 inference(scs_inference,[],[31,246,21])).
% 59.33/59.38 cnf(582,plain,
% 59.33/59.38 (E(x5821,f3(x5821,f2(x5821)))),
% 59.33/59.38 inference(rename_variables,[],[31])).
% 59.33/59.38 cnf(585,plain,
% 59.33/59.38 (E(x5851,f3(x5851,f2(x5851)))),
% 59.33/59.38 inference(rename_variables,[],[31])).
% 59.33/59.38 cnf(586,plain,
% 59.33/59.38 (P2(f3(a5,f2(a5)),f3(f4(a5),a5))),
% 59.33/59.38 inference(scs_inference,[],[31,582,585,353,500,494,21,10,9])).
% 59.33/59.38 cnf(595,plain,
% 59.33/59.38 (E(x5951,f3(x5951,f2(x5951)))),
% 59.33/59.38 inference(rename_variables,[],[31])).
% 59.33/59.38 cnf(596,plain,
% 59.33/59.38 (P2(f3(f2(a6),f2(f2(a6))),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[31,595,165,459,10,9])).
% 59.33/59.38 cnf(603,plain,
% 59.33/59.38 (E(f4(a6),f4(f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[32,344,3])).
% 59.33/59.38 cnf(618,plain,
% 59.33/59.38 (~E(f3(f4(a1),a1),f3(f3(f4(a7),a7),f2(a7)))),
% 59.33/59.38 inference(scs_inference,[],[342,296,10])).
% 59.33/59.38 cnf(645,plain,
% 59.33/59.38 (P1(f3(f4(a1),f3(a1,f2(a1))))),
% 59.33/59.38 inference(scs_inference,[],[170,325,8])).
% 59.33/59.38 cnf(655,plain,
% 59.33/59.38 (P2(f4(f2(a1)),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[178,247,21])).
% 59.33/59.38 cnf(675,plain,
% 59.33/59.38 (E(f4(a6),f2(f4(f3(a6,a5))))),
% 59.33/59.38 inference(scs_inference,[],[185,100,8,25])).
% 59.33/59.38 cnf(679,plain,
% 59.33/59.38 (P1(f3(f4(a6),a6))),
% 59.33/59.38 inference(scs_inference,[],[185,90,8])).
% 59.33/59.38 cnf(681,plain,
% 59.33/59.38 (E(f4(a6),f2(f4(a6)))),
% 59.33/59.38 inference(scs_inference,[],[185,90,8,25])).
% 59.33/59.38 cnf(687,plain,
% 59.33/59.38 (E(f4(a6),f2(f4(f3(a6,a6))))),
% 59.33/59.38 inference(scs_inference,[],[185,515,8,25])).
% 59.33/59.38 cnf(695,plain,
% 59.33/59.38 (P1(f3(a6,a5))),
% 59.33/59.38 inference(scs_inference,[],[181,675,8,154])).
% 59.33/59.38 cnf(699,plain,
% 59.33/59.38 (E(f4(a5),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[181,675,8,154,18,25])).
% 59.33/59.38 cnf(701,plain,
% 59.33/59.38 (E(f2(a6),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[181,675,8,154,18,25,2])).
% 59.33/59.38 cnf(706,plain,
% 59.33/59.38 (P1(f2(f4(a6)))),
% 59.33/59.38 inference(scs_inference,[],[90,181,695,681,21,8])).
% 59.33/59.38 cnf(709,plain,
% 59.33/59.38 (P1(f3(a6,a6))),
% 59.33/59.38 inference(scs_inference,[],[181,687,8,154])).
% 59.33/59.38 cnf(713,plain,
% 59.33/59.38 (E(f4(a6),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[181,687,8,154,18,25])).
% 59.33/59.38 cnf(715,plain,
% 59.33/59.38 (E(f2(a6),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[181,687,8,154,18,25,2])).
% 59.33/59.38 cnf(728,plain,
% 59.33/59.38 (P1(f3(a1,f3(a5,f2(a5))))),
% 59.33/59.38 inference(scs_inference,[],[200,325,8])).
% 59.33/59.38 cnf(732,plain,
% 59.33/59.38 (E(f2(a1),f4(f3(a5,f2(a5))))),
% 59.33/59.38 inference(scs_inference,[],[200,325,8,25,2])).
% 59.33/59.38 cnf(737,plain,
% 59.33/59.38 (E(f4(f2(a5)),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[732,246,8,19,25])).
% 59.33/59.38 cnf(739,plain,
% 59.33/59.38 (E(f2(a5),f4(f2(a5)))),
% 59.33/59.38 inference(scs_inference,[],[732,246,8,19,25,2])).
% 59.33/59.38 cnf(741,plain,
% 59.33/59.38 (P1(f4(f2(a5)))),
% 59.33/59.38 inference(scs_inference,[],[739,182,8])).
% 59.33/59.38 cnf(746,plain,
% 59.33/59.38 (E(f4(a5),f2(f4(f3(a5,a5))))),
% 59.33/59.38 inference(scs_inference,[],[201,100,8,25])).
% 59.33/59.38 cnf(750,plain,
% 59.33/59.38 (P1(f3(f4(a5),a5))),
% 59.33/59.38 inference(scs_inference,[],[201,90,8])).
% 59.33/59.38 cnf(752,plain,
% 59.33/59.38 (E(f4(a5),f2(f4(a5)))),
% 59.33/59.38 inference(scs_inference,[],[201,90,8,25])).
% 59.33/59.38 cnf(754,plain,
% 59.33/59.38 (E(f2(f4(a5)),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[201,90,8,25,2])).
% 59.33/59.38 cnf(757,plain,
% 59.33/59.38 (E(f4(a5),f2(f4(f3(a5,a6))))),
% 59.33/59.38 inference(scs_inference,[],[201,515,8,25])).
% 59.33/59.38 cnf(765,plain,
% 59.33/59.38 (P1(f3(a5,a5))),
% 59.33/59.38 inference(scs_inference,[],[238,746,8,154])).
% 59.33/59.38 cnf(769,plain,
% 59.33/59.38 (E(f4(a5),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[238,746,8,154,18,25])).
% 59.33/59.38 cnf(771,plain,
% 59.33/59.38 (E(f2(a5),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[238,746,8,154,18,25,2])).
% 59.33/59.38 cnf(773,plain,
% 59.33/59.38 (P1(f2(f4(a5)))),
% 59.33/59.38 inference(scs_inference,[],[238,752,8])).
% 59.33/59.38 cnf(775,plain,
% 59.33/59.38 (P1(f2(f4(f3(a5,a6))))),
% 59.33/59.38 inference(scs_inference,[],[238,757,8])).
% 59.33/59.38 cnf(776,plain,
% 59.33/59.38 (P1(f4(f3(a5,a6)))),
% 59.33/59.38 inference(scs_inference,[],[238,757,8,18])).
% 59.33/59.38 cnf(793,plain,
% 59.33/59.38 (E(f2(a1),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[205,699,3])).
% 59.33/59.38 cnf(796,plain,
% 59.33/59.38 (E(f2(a6),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[205,497,655,699,3,10,9,2])).
% 59.33/59.38 cnf(798,plain,
% 59.33/59.38 (E(f2(a1),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[205,769,3])).
% 59.33/59.38 cnf(801,plain,
% 59.33/59.38 (E(f2(a5),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[205,565,406,769,3,10,9,2])).
% 59.33/59.38 cnf(848,plain,
% 59.33/59.38 (E(f2(a6),f3(f2(a1),f2(f2(a1))))),
% 59.33/59.38 inference(scs_inference,[],[280,699,3,2])).
% 59.33/59.38 cnf(877,plain,
% 59.33/59.38 (E(f2(a6),f3(f4(a5),f2(f4(a5))))),
% 59.33/59.38 inference(scs_inference,[],[303,793,3,2])).
% 59.33/59.38 cnf(895,plain,
% 59.33/59.38 (E(f3(x8951,x8952),f3(x8951,f3(x8952,f2(x8952))))),
% 59.33/59.38 inference(rename_variables,[],[325])).
% 59.33/59.38 cnf(898,plain,
% 59.33/59.38 (E(f3(x8981,x8982),f3(x8981,f3(x8982,f2(x8982))))),
% 59.33/59.38 inference(rename_variables,[],[325])).
% 59.33/59.38 cnf(899,plain,
% 59.33/59.38 (P2(f3(f4(a1),f3(a1,f2(a1))),a1)),
% 59.33/59.38 inference(scs_inference,[],[325,895,898,200,168,500,21,10,9])).
% 59.33/59.38 cnf(932,plain,
% 59.33/59.38 (E(f4(f3(a6,f2(a6))),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[340,771,346,21,3])).
% 59.33/59.38 cnf(935,plain,
% 59.33/59.38 (E(f4(f3(a6,f2(a6))),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[340,801,3])).
% 59.33/59.38 cnf(947,plain,
% 59.33/59.38 (P2(f4(f2(a6)),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[349,421,21])).
% 59.33/59.38 cnf(950,plain,
% 59.33/59.38 (P2(f2(a6),f4(f2(a6)))),
% 59.33/59.38 inference(scs_inference,[],[349,701,464,421,21,3,9])).
% 59.33/59.38 cnf(956,plain,
% 59.33/59.38 (E(f4(f2(a6)),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[349,796,3])).
% 59.33/59.38 cnf(971,plain,
% 59.33/59.38 (P2(f2(f3(a5,a6)),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[372,947,439,950,21,10,9])).
% 59.33/59.38 cnf(981,plain,
% 59.33/59.38 (E(f2(f3(a5,a6)),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[374,956,3])).
% 59.33/59.38 cnf(1022,plain,
% 59.33/59.38 (~P1(f2(f2(a1)))+P1(f3(a1,f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[935,18,27])).
% 59.33/59.38 cnf(1025,plain,
% 59.33/59.38 (P1(f3(a1,f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[287,1022,26])).
% 59.33/59.38 cnf(1107,plain,
% 59.33/59.38 (E(x11071,f3(f4(f3(x11071,a6)),x11071))),
% 59.33/59.38 inference(rename_variables,[],[515])).
% 59.33/59.38 cnf(1110,plain,
% 59.33/59.38 (E(x11101,f3(f4(f3(x11101,a6)),x11101))),
% 59.33/59.38 inference(rename_variables,[],[515])).
% 59.33/59.38 cnf(1111,plain,
% 59.33/59.38 (P2(f3(f4(f3(a1,a6)),a1),a1)),
% 59.33/59.38 inference(scs_inference,[],[515,1107,1110,163,264,185,21,10,9])).
% 59.33/59.38 cnf(1126,plain,
% 59.33/59.38 (~P2(a7,a1)),
% 59.33/59.38 inference(scs_inference,[],[17,2,20])).
% 59.33/59.38 cnf(1131,plain,
% 59.33/59.38 (~E(f3(f4(a1),f3(a1,f2(a1))),a7)),
% 59.33/59.38 inference(scs_inference,[],[1126,899,9])).
% 59.33/59.38 cnf(1135,plain,
% 59.33/59.38 (~E(f3(f4(f3(a1,a6)),a1),a7)),
% 59.33/59.38 inference(scs_inference,[],[1126,1111,9])).
% 59.33/59.38 cnf(1155,plain,
% 59.33/59.38 (E(f4(a6),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[603,932,3])).
% 59.33/59.38 cnf(1156,plain,
% 59.33/59.38 (E(f4(a5),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[603,932,3,2])).
% 59.33/59.38 cnf(1158,plain,
% 59.33/59.38 (E(f4(a6),f2(a1))),
% 59.33/59.38 inference(scs_inference,[],[603,935,3])).
% 59.33/59.38 cnf(1159,plain,
% 59.33/59.38 (E(f2(a1),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[603,935,3,2])).
% 59.33/59.38 cnf(1165,plain,
% 59.33/59.38 (~P2(f3(f3(f4(a7),a7),f2(a7)),f3(f4(a1),a1))),
% 59.33/59.38 inference(scs_inference,[],[618,2,20])).
% 59.33/59.38 cnf(1166,plain,
% 59.33/59.38 (~E(f3(a1,f2(a1)),f3(f3(f4(a7),a7),f2(a7)))),
% 59.33/59.38 inference(scs_inference,[],[1165,166,9])).
% 59.33/59.38 cnf(1172,plain,
% 59.33/59.38 (P1(f3(f3(f4(a1),a1),f2(a1)))),
% 59.33/59.38 inference(scs_inference,[],[645,78,8])).
% 59.33/59.38 cnf(1182,plain,
% 59.33/59.38 (~E(f3(a7,a5),f3(f4(f3(a1,a5)),f3(a1,a5)))),
% 59.33/59.38 inference(scs_inference,[],[17,90,2,23])).
% 59.33/59.38 cnf(1185,plain,
% 59.33/59.38 (~E(f3(a1,a5),f3(a7,a5))),
% 59.33/59.38 inference(scs_inference,[],[1182,268,20,9])).
% 59.33/59.38 cnf(1211,plain,
% 59.33/59.38 (P2(f4(a6),f2(f4(f3(a6,a5))))),
% 59.33/59.38 inference(scs_inference,[],[675,181,21])).
% 59.33/59.38 cnf(1214,plain,
% 59.33/59.38 (P2(f2(f4(f3(a6,a5))),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[675,181,189,252,21,10,9])).
% 59.33/59.38 cnf(1234,plain,
% 59.33/59.38 (~E(f3(a7,a6),f3(f4(f3(a1,a6)),f3(a1,a6)))),
% 59.33/59.38 inference(scs_inference,[],[17,90,2,24])).
% 59.33/59.38 cnf(1237,plain,
% 59.33/59.38 (P1(f3(f4(a6),f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[679,1234,325,20,8])).
% 59.33/59.38 cnf(1241,plain,
% 59.33/59.38 (P2(f4(a6),f2(f4(a6)))),
% 59.33/59.38 inference(scs_inference,[],[681,181,21])).
% 59.33/59.38 cnf(1251,plain,
% 59.33/59.38 (P2(f2(f4(a6)),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[681,189,9])).
% 59.33/59.38 cnf(1286,plain,
% 59.33/59.38 (P2(f4(a6),f2(f4(f3(a6,a6))))),
% 59.33/59.38 inference(scs_inference,[],[687,181,21])).
% 59.33/59.38 cnf(1314,plain,
% 59.33/59.38 (P1(f3(a6,f3(a5,f2(a5))))),
% 59.33/59.38 inference(scs_inference,[],[695,325,8])).
% 59.33/59.38 cnf(1318,plain,
% 59.33/59.38 (E(f2(a6),f4(f3(a5,f2(a5))))),
% 59.33/59.38 inference(scs_inference,[],[695,325,8,25,2])).
% 59.33/59.38 cnf(1349,plain,
% 59.33/59.38 (P2(f4(f2(a6)),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[701,947,10])).
% 59.33/59.38 cnf(1353,plain,
% 59.33/59.38 (P2(f3(f2(a6),f2(f2(a6))),f4(a5))),
% 59.33/59.38 inference(scs_inference,[],[701,596,10])).
% 59.33/59.38 cnf(1359,plain,
% 59.33/59.38 (E(f2(a6),f2(f4(f3(a5,a5))))),
% 59.33/59.38 inference(scs_inference,[],[701,971,746,10,3])).
% 59.33/59.38 cnf(1361,plain,
% 59.33/59.38 (E(f2(a6),f2(f4(f3(a5,a6))))),
% 59.33/59.38 inference(scs_inference,[],[701,757,3])).
% 59.33/59.38 cnf(1364,plain,
% 59.33/59.38 (E(f2(a6),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[701,769,3])).
% 59.33/59.38 cnf(1365,plain,
% 59.33/59.38 (E(f2(a5),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[701,769,3,2])).
% 59.33/59.38 cnf(1376,plain,
% 59.33/59.38 (P1(f3(a6,f3(a6,f2(a6))))),
% 59.33/59.38 inference(scs_inference,[],[709,325,8])).
% 59.33/59.38 cnf(1385,plain,
% 59.33/59.38 (E(f2(f2(a6)),f2(f4(a6)))),
% 59.33/59.38 inference(scs_inference,[],[713,4,2])).
% 59.33/59.38 cnf(1390,plain,
% 59.33/59.38 (E(f4(a6),f3(f2(a1),f2(f2(a1))))),
% 59.33/59.38 inference(scs_inference,[],[713,848,1385,489,300,706,2,10,8,9,3])).
% 59.33/59.38 cnf(1395,plain,
% 59.33/59.38 (E(f4(a6),f3(f4(a5),f2(f4(a5))))),
% 59.33/59.38 inference(scs_inference,[],[713,877,1390,1211,448,2,10,9,3])).
% 59.33/59.38 cnf(1398,plain,
% 59.33/59.38 (P2(f2(a5),f2(a6))),
% 59.33/59.38 inference(scs_inference,[],[713,1395,252,2,10])).
% 59.33/59.38 cnf(1400,plain,
% 59.33/59.38 (E(f4(a6),f4(f3(a5,f2(a5))))),
% 59.33/59.38 inference(scs_inference,[],[713,1318,1395,1286,252,2,10,9,3])).
% 59.33/59.38 cnf(1405,plain,
% 59.33/59.38 (E(f4(a6),f2(f4(f3(a5,a5))))),
% 59.33/59.38 inference(scs_inference,[],[713,1359,1400,481,1251,2,10,9,3])).
% 59.33/59.38 cnf(1410,plain,
% 59.33/59.38 (E(f4(a6),f2(f4(f3(a5,a6))))),
% 59.33/59.38 inference(scs_inference,[],[713,1361,1405,1241,1214,2,10,9,3])).
% 59.33/59.38 cnf(1426,plain,
% 59.33/59.38 (P2(f2(a6),f2(a5))),
% 59.33/59.38 inference(scs_inference,[],[713,399,9])).
% 59.33/59.38 cnf(1457,plain,
% 59.33/59.38 (P2(a1,f3(a1,f2(a1)))),
% 59.33/59.38 inference(scs_inference,[],[31,11,21])).
% 59.33/59.38 cnf(1472,plain,
% 59.33/59.38 (E(x14721,f3(f4(x14721),x14721))),
% 59.33/59.38 inference(rename_variables,[],[90])).
% 59.33/59.38 cnf(1473,plain,
% 59.33/59.38 (P2(f3(f4(a1),a1),f3(a1,f2(a1)))),
% 59.33/59.38 inference(scs_inference,[],[90,1472,1457,1349,10,9])).
% 59.33/59.38 cnf(1475,plain,
% 59.33/59.38 (P2(f3(f2(a6),f2(f2(a6))),f4(a6))),
% 59.33/59.38 inference(scs_inference,[],[715,596,10])).
% 59.33/59.38 cnf(1486,plain,
% 59.33/59.38 (P1(f3(f3(a1,a5),f2(a5)))),
% 59.33/59.38 inference(scs_inference,[],[728,78,8])).
% 59.33/59.38 cnf(1488,plain,
% 59.33/59.38 (E(f4(f2(a5)),f2(f3(a1,a5)))),
% 59.33/59.38 inference(scs_inference,[],[728,78,8,25])).
% 59.33/59.39 cnf(1492,plain,
% 59.33/59.39 (P1(f2(f3(a1,a5)))),
% 59.33/59.39 inference(scs_inference,[],[1488,741,8])).
% 59.33/59.39 cnf(1516,plain,
% 59.33/59.39 (E(x15161,f3(x15161,f2(x15161)))),
% 59.33/59.39 inference(rename_variables,[],[31])).
% 59.33/59.39 cnf(1517,plain,
% 59.33/59.39 (P2(f3(f2(a6),f2(f2(a6))),f2(a5))),
% 59.33/59.39 inference(scs_inference,[],[31,1516,1398,1426,10,9])).
% 59.33/59.39 cnf(1526,plain,
% 59.33/59.39 (P2(f4(f2(a5)),f2(a5))),
% 59.33/59.39 inference(scs_inference,[],[737,741,21])).
% 59.33/59.39 cnf(1546,plain,
% 59.33/59.39 (E(f4(f2(a5)),f4(a5))),
% 59.33/59.39 inference(scs_inference,[],[737,771,3])).
% 59.33/59.39 cnf(1547,plain,
% 59.33/59.39 (E(f4(a5),f4(f2(a5)))),
% 59.33/59.39 inference(scs_inference,[],[737,771,3,2])).
% 59.33/59.39 cnf(1564,plain,
% 59.33/59.39 (E(f2(a5),f2(f3(a1,a5)))),
% 59.33/59.39 inference(scs_inference,[],[739,1526,1488,10,3])).
% 59.33/59.39 cnf(1600,plain,
% 59.33/59.39 (P1(f3(f4(a5),f3(a5,f2(a5))))),
% 59.33/59.39 inference(scs_inference,[],[750,325,8])).
% 59.33/59.39 cnf(1653,plain,
% 59.33/59.39 (E(f4(f2(a5)),f2(f4(a5)))),
% 59.33/59.39 inference(scs_inference,[],[754,1547,3,2])).
% 59.33/59.39 cnf(1654,plain,
% 59.33/59.39 (E(f3(x16541,f4(a6)),f3(x16541,f2(a5)))),
% 59.33/59.39 inference(scs_inference,[],[14,25,6])).
% 59.33/59.39 cnf(1655,plain,
% 59.33/59.39 (E(f3(x16551,f2(a5)),f3(x16551,f4(a6)))),
% 59.33/59.39 inference(scs_inference,[],[1654,2])).
% 59.33/59.39 cnf(1715,plain,
% 59.33/59.39 (P1(f3(a5,f3(a5,f2(a5))))),
% 59.33/59.39 inference(scs_inference,[],[765,325,8])).
% 59.33/59.39 cnf(1728,plain,
% 59.33/59.39 (E(f4(a5),f2(f3(a1,a5)))),
% 59.33/59.39 inference(scs_inference,[],[769,1564,477,10,3])).
% 59.33/59.39 cnf(1754,plain,
% 59.33/59.39 (P1(f3(f3(f4(a6),a6),f2(a6)))),
% 59.33/59.39 inference(scs_inference,[],[1159,1492,1237,28,4,7,6,98,97])).
% 59.33/59.39 cnf(1797,plain,
% 59.33/59.39 (P1(f3(f3(a1,a5),f4(a6)))),
% 59.33/59.39 inference(scs_inference,[],[981,776,1486,773,586,1653,1172,1166,1600,1314,438,796,1156,1655,1111,525,1185,28,98,7,4,6,97,5,26,22,20,2,24,27,21,8])).
% 59.33/59.39 cnf(1811,plain,
% 59.33/59.39 (P1(f3(f3(a5,a5),f2(a5)))),
% 59.33/59.39 inference(scs_inference,[],[1797,1715,1364,28,98,7,4,6,97])).
% 59.33/59.39 cnf(1815,plain,
% 59.33/59.39 (E(f3(f4(a1),a1),f3(a1,f2(a1)))),
% 59.33/59.39 inference(scs_inference,[],[1797,1473,1754,1715,1364,28,98,7,4,6,97,26,5,20])).
% 59.33/59.39 cnf(1835,plain,
% 59.33/59.39 (P1(f2(f3(a5,a5)))),
% 59.33/59.39 inference(scs_inference,[],[1811,1376,1365,28,98,7,6,4,26])).
% 59.33/59.39 cnf(1837,plain,
% 59.33/59.39 (P1(f3(f3(a6,a6),f2(a6)))),
% 59.33/59.39 inference(scs_inference,[],[1811,1376,1365,28,98,7,6,4,26,97])).
% 59.33/59.39 cnf(1852,plain,
% 59.33/59.39 (~E(f3(a1,f2(a1)),f3(f4(a7),a7))),
% 59.33/59.39 inference(scs_inference,[],[17,1546,1811,1815,1353,1131,1376,775,316,1365,1410,741,1126,525,1185,91,325,28,98,7,6,4,26,97,5,20,2,23,24,27,21,10,3])).
% 59.33/59.39 cnf(1865,plain,
% 59.33/59.39 (P1(f3(f3(a1,a6),f2(a6)))),
% 59.33/59.39 inference(scs_inference,[],[1835,1837,1025,793,1155,28,98,7,26,4,6,97])).
% 59.33/59.39 cnf(1870,plain,
% 59.33/59.39 (~E(f3(a7,a5),f3(f4(f3(a1,a6)),f3(a1,a5)))),
% 59.33/59.39 inference(scs_inference,[],[1835,1837,1852,1475,1135,1025,793,1155,16,28,98,7,26,4,6,97,5,20,2,23])).
% 59.33/59.39 cnf(1876,plain,
% 59.33/59.39 (P1(f3(f3(a1,a5),a5))),
% 59.33/59.39 inference(scs_inference,[],[17,1835,1728,1837,1852,1475,1135,1025,1492,793,1155,16,325,28,98,7,26,4,6,97,5,20,2,23,24,27])).
% 59.33/59.39 cnf(1896,plain,
% 59.33/59.39 ($false),
% 59.33/59.39 inference(scs_inference,[],[1876,1865,1870,1517,1314,1156,798,1158,59,1185,16,28,7,26,5,97,4,6,20,2,24]),
% 59.33/59.39 ['proof']).
% 59.33/59.39 % SZS output end Proof
% 59.33/59.39 % Total time :58.730000s
%------------------------------------------------------------------------------