%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT004-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 : n028.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.87s 59.90s
% Output : CNFRefutation 59.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.12 % Problem : CAT004-3 : TPTP v8.2.0. Released v1.0.0.
% 0.09/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Tue Jun 18 12:18:23 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.18/0.55 start to proof:theBenchmark
% 59.77/59.89 %-------------------------------------------
% 59.77/59.89 % File :CSE---1.7
% 59.77/59.89 % Problem :theBenchmark
% 59.77/59.89 % Transform :cnf
% 59.77/59.89 % Format :tptp:raw
% 59.77/59.89 % Command :java -jar mcs_scs.jar %d %s
% 59.77/59.89
% 59.77/59.89 % Result :Theorem 59.300000s
% 59.77/59.89 % Output :CNFRefutation 59.300000s
% 59.77/59.89 %-------------------------------------------
% 59.87/59.90 %--------------------------------------------------------------------------
% 59.87/59.90 % File : CAT004-3 : TPTP v8.2.0. Released v1.0.0.
% 59.87/59.90 % Domain : Category Theory
% 59.87/59.90 % Problem : X and Y epimorphisms, XY well-defined => XY epimorphism
% 59.87/59.90 % Version : [Sco79] axioms : Reduced > Complete.
% 59.87/59.90 % English : If x and y are epimorphisms and xy is well-defined, then
% 59.87/59.90 % xy is an epimorphism.
% 59.87/59.90
% 59.87/59.90 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 59.87/59.90 % Source : [ANL]
% 59.87/59.90 % Names : p4.ver3.in [ANL]
% 59.87/59.90
% 59.87/59.90 % Status : Unsatisfiable
% 59.87/59.90 % Rating : 0.20 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.12 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.43 v6.0.0, 0.20 v5.5.0, 0.40 v5.3.0, 0.39 v5.2.0, 0.31 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0, 0.15 v4.0.1, 0.27 v4.0.0, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0, 0.38 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.30 v2.5.0, 0.50 v2.4.0, 0.44 v2.2.1, 0.44 v2.2.0, 0.22 v2.1.0, 0.56 v2.0.0
% 59.87/59.90 % Syntax : Number of clauses : 23 ( 7 unt; 2 nHn; 18 RR)
% 59.87/59.90 % Number of literals : 47 ( 23 equ; 22 neg)
% 59.87/59.90 % Maximal clause size : 4 ( 2 avg)
% 59.87/59.90 % Maximal term depth : 3 ( 1 avg)
% 59.87/59.90 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 59.87/59.90 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 59.87/59.90 % Number of variables : 37 ( 4 sgn)
% 59.87/59.90 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.87/59.90
% 59.87/59.90 % Comments : Axioms simplified by Art Quaife.
% 59.87/59.90 %--------------------------------------------------------------------------
% 59.87/59.90 %----Include Scott's axioms for category theory
% 59.87/59.90 include('Axioms/CAT003-0.ax').
% 59.87/59.90 %--------------------------------------------------------------------------
% 59.87/59.90 cnf(assume_ab_exists,hypothesis,
% 59.87/59.90 there_exists(compose(a,b)) ).
% 59.87/59.90
% 59.87/59.90 cnf(cancellation_for_product1,hypothesis,
% 59.87/59.90 ( compose(X,a) != Y
% 59.87/59.90 | compose(Z,a) != Y
% 59.87/59.90 | X = Z ) ).
% 59.87/59.90
% 59.87/59.90 cnf(cancellation_for_product2,hypothesis,
% 59.87/59.90 ( compose(X,b) != Y
% 59.87/59.90 | compose(Z,b) != Y
% 59.87/59.90 | X = Z ) ).
% 59.87/59.90
% 59.87/59.90 cnf(assume_h_exists,hypothesis,
% 59.87/59.90 there_exists(h) ).
% 59.87/59.90
% 59.87/59.90 cnf(h_ab_equals_g_ab,hypothesis,
% 59.87/59.90 compose(h,compose(a,b)) = compose(g,compose(a,b)) ).
% 59.87/59.90
% 59.87/59.90 cnf(prove_h_equals_g,negated_conjecture,
% 59.87/59.90 h != g ).
% 59.87/59.90
% 59.87/59.90 %--------------------------------------------------------------------------
% 59.87/59.90 %-------------------------------------------
% 59.87/59.90 % Proof found
% 59.87/59.90 % SZS status Theorem for theBenchmark
% 59.87/59.90 % SZS output start Proof
% 59.87/59.90 %ClaNum:34(EqnAxiom:12)
% 59.87/59.90 %VarNum:70(SingletonVarNum:33)
% 59.87/59.90 %MaxLitNum:3
% 59.87/59.90 %MaxfuncDepth:2
% 59.87/59.90 %SharedTerms:11
% 59.87/59.90 %goalClause: 19
% 59.87/59.90 %singleGoalClaCount:1
% 59.87/59.90 [13]P1(a1)
% 59.87/59.90 [19]~E(a1,a7)
% 59.87/59.90 [16]P1(f3(a5,a6))
% 59.87/59.90 [17]E(f3(a1,f3(a5,a6)),f3(a7,f3(a5,a6)))
% 59.87/59.90 [14]E(f3(x141,f2(x141)),x141)
% 59.87/59.90 [15]E(f3(f4(x151),x151),x151)
% 59.87/59.90 [18]E(f3(f3(x181,x182),x183),f3(x181,f3(x182,x183)))
% 59.87/59.90 [20]P1(x201)+~P1(f2(x201))
% 59.87/59.90 [21]P1(x211)+~P1(f4(x211))
% 59.87/59.90 [22]~P2(x221,x222)+E(x221,x222)
% 59.87/59.90 [24]P1(x241)+~P2(x242,x241)
% 59.87/59.90 [25]P1(x251)+~P2(x251,x252)
% 59.87/59.90 [27]E(x271,x272)+P1(f8(x271,x272))
% 59.87/59.90 [31]E(f4(x311),f2(x312))+~P1(f3(x312,x311))
% 59.87/59.90 [32]P1(f2(x321))+~P1(f3(x321,x322))
% 59.87/59.90 [33]P1(f4(x331))+~P1(f3(x331,x332))
% 59.87/59.90 [23]~E(x231,x232)+~P1(x231)+P2(x231,x232)
% 59.87/59.90 [28]E(x281,x282)+E(f8(x281,x282),x282)+E(f8(x281,x282),x281)
% 59.87/59.90 [34]~E(f4(x342),f2(x341))+~P1(f2(x341))+P1(f3(x341,x342))
% 59.87/59.90 [29]E(x291,x292)+~E(f3(x291,a5),x293)+~E(f3(x292,a5),x293)
% 59.87/59.90 [30]E(x301,x302)+~E(f3(x301,a6),x303)+~E(f3(x302,a6),x303)
% 59.87/59.90 %EqnAxiom
% 59.87/59.90 [1]E(x11,x11)
% 59.87/59.90 [2]E(x22,x21)+~E(x21,x22)
% 59.87/59.90 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.87/59.90 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 59.87/59.90 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 59.87/59.90 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 59.87/59.90 [7]~E(x71,x72)+E(f4(x71),f4(x72))
% 59.87/59.90 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83))
% 59.87/59.90 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92))
% 59.87/59.90 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 59.87/59.90 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 59.87/59.90 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 59.87/59.90
% 59.87/59.90 %-------------------------------------------
% 59.87/59.91 cnf(35,plain,
% 59.87/59.91 (~P1(x351)+P2(x351,x351)),
% 59.87/59.91 inference(equality_inference,[],[23])).
% 59.87/59.91 cnf(36,plain,
% 59.87/59.91 (~P2(a1,a7)),
% 59.87/59.91 inference(scs_inference,[],[19,22])).
% 59.87/59.91 cnf(38,plain,
% 59.87/59.91 (E(x381,f3(x381,f2(x381)))),
% 59.87/59.91 inference(scs_inference,[],[19,14,22,2])).
% 59.87/59.91 cnf(39,plain,
% 59.87/59.91 (E(f4(a6),f2(a5))),
% 59.87/59.91 inference(scs_inference,[],[19,14,16,22,2,31])).
% 59.87/59.91 cnf(41,plain,
% 59.87/59.91 (P2(f3(a5,a6),f3(f3(a5,a6),f2(f3(a5,a6))))),
% 59.87/59.91 inference(scs_inference,[],[19,14,16,22,2,31,23])).
% 59.87/59.91 cnf(43,plain,
% 59.87/59.91 (~E(a1,f3(f4(a7),a7))),
% 59.87/59.91 inference(scs_inference,[],[19,14,15,16,22,2,31,23,3])).
% 59.87/59.91 cnf(45,plain,
% 59.87/59.91 (P1(f3(f3(a5,a6),f2(f3(a5,a6))))),
% 59.87/59.91 inference(scs_inference,[],[19,14,15,16,22,2,31,23,3,10])).
% 59.87/59.91 cnf(46,plain,
% 59.87/59.91 (P2(f3(a5,a6),f3(a5,a6))),
% 59.87/59.91 inference(scs_inference,[],[19,14,15,16,22,2,31,23,3,10,12])).
% 59.87/59.91 cnf(49,plain,
% 59.87/59.91 (~P2(a1,f3(f4(a7),a7))),
% 59.87/59.91 inference(scs_inference,[],[43,22])).
% 59.87/59.91 cnf(51,plain,
% 59.87/59.91 (E(f2(a5),f4(a6))),
% 59.87/59.91 inference(scs_inference,[],[43,39,22,2])).
% 59.87/59.91 cnf(52,plain,
% 59.87/59.91 (E(f4(a6),f3(f2(a5),f2(f2(a5))))),
% 59.87/59.91 inference(scs_inference,[],[38,43,39,22,2,3])).
% 59.87/59.91 cnf(54,plain,
% 59.87/59.91 (~P1(f4(a6))+P1(f2(a5))),
% 59.87/59.91 inference(scs_inference,[],[38,43,39,22,2,3,10])).
% 59.87/59.91 cnf(55,plain,
% 59.87/59.91 (~P2(x551,f4(a6))+P1(f2(a5))),
% 59.87/59.91 inference(scs_inference,[],[38,43,39,22,2,3,10,24])).
% 59.87/59.91 cnf(59,plain,
% 59.87/59.91 (P1(f2(a5))+~P1(f3(a6,x591))),
% 59.87/59.91 inference(scs_inference,[],[38,43,39,22,2,3,10,24,25,33])).
% 59.87/59.91 cnf(64,plain,
% 59.87/59.91 (E(f3(f2(a5),f2(f2(a5))),f4(a6))),
% 59.87/59.91 inference(scs_inference,[],[52,2])).
% 59.87/59.91 cnf(65,plain,
% 59.87/59.91 (E(f3(f4(f2(a5)),f2(a5)),f4(a6))),
% 59.87/59.91 inference(scs_inference,[],[52,51,15,2,3])).
% 59.87/59.91 cnf(67,plain,
% 59.87/59.91 (P1(f3(a1,f2(a1)))),
% 59.87/59.91 inference(scs_inference,[],[52,51,38,13,15,2,3,10])).
% 59.87/59.91 cnf(69,plain,
% 59.87/59.91 (E(f4(f2(a1)),f2(a1))),
% 59.87/59.91 inference(scs_inference,[],[52,51,38,13,15,2,3,10,31])).
% 59.87/59.91 cnf(71,plain,
% 59.87/59.91 (E(f4(a6),f3(f4(f2(a5)),f2(a5)))),
% 59.87/59.91 inference(scs_inference,[],[65,2])).
% 59.87/59.91 cnf(72,plain,
% 59.87/59.91 (E(f3(f3(a1,a5),a6),f3(a7,f3(a5,a6)))),
% 59.87/59.91 inference(scs_inference,[],[65,18,17,2,3])).
% 59.87/59.91 cnf(74,plain,
% 59.87/59.91 (~P1(f3(f2(a5),f2(f2(a5))))+P1(f4(a6))),
% 59.87/59.91 inference(scs_inference,[],[64,65,18,17,2,3,10])).
% 59.87/59.91 cnf(80,plain,
% 59.87/59.91 (E(f3(a7,f3(a5,a6)),f3(f3(a1,a5),a6))),
% 59.87/59.91 inference(scs_inference,[],[72,2])).
% 59.87/59.91 cnf(81,plain,
% 59.87/59.91 (~E(a1,f3(a7,f2(a7)))),
% 59.87/59.91 inference(scs_inference,[],[19,72,14,2,3])).
% 59.87/59.91 cnf(83,plain,
% 59.87/59.91 (~P2(a1,f3(a7,f2(a7)))),
% 59.87/59.91 inference(scs_inference,[],[19,72,14,2,3,22])).
% 59.87/59.91 cnf(92,plain,
% 59.87/59.91 (E(f2(a1),f4(f2(a1)))),
% 59.87/59.91 inference(scs_inference,[],[69,2])).
% 59.87/59.91 cnf(93,plain,
% 59.87/59.91 (E(f3(a7,f3(a5,a6)),f3(a1,f3(a5,a6)))),
% 59.87/59.91 inference(scs_inference,[],[80,69,18,2,3])).
% 59.87/59.91 cnf(108,plain,
% 59.87/59.91 (E(x1081,f3(f4(x1081),x1081))),
% 59.87/59.91 inference(scs_inference,[],[15,2])).
% 59.87/59.91 cnf(109,plain,
% 59.87/59.91 (E(f3(f4(f3(x1091,a5)),x1091),x1091)),
% 59.87/59.91 inference(scs_inference,[],[15,18,2,29])).
% 59.87/59.91 cnf(115,plain,
% 59.87/59.91 (~P1(f4(a6))+P1(f3(f4(f2(a5)),f2(a5)))),
% 59.87/59.91 inference(scs_inference,[],[19,71,15,18,2,29,3,22,10])).
% 59.87/59.91 cnf(116,plain,
% 59.87/59.91 (P1(f3(f4(f2(a5)),f2(a5)))+~P1(f3(f2(a5),f2(f2(a5))))),
% 59.87/59.91 inference(scs_inference,[],[19,71,15,18,2,29,3,22,10,74])).
% 59.87/59.91 cnf(127,plain,
% 59.87/59.91 (E(x1271,f3(f4(f3(x1271,a5)),x1271))),
% 59.87/59.91 inference(scs_inference,[],[109,2])).
% 59.87/59.91 cnf(129,plain,
% 59.87/59.91 (E(x1291,f3(f4(x1291),x1291))),
% 59.87/59.91 inference(rename_variables,[],[108])).
% 59.87/59.91 cnf(131,plain,
% 59.87/59.91 (E(x1311,f3(f4(x1311),x1311))),
% 59.87/59.91 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(132,plain,
% 59.87/59.92 (P1(f3(f4(f3(a5,a6)),f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[108,129,131,109,16,46,2,12,11,10])).
% 59.87/59.92 cnf(134,plain,
% 59.87/59.92 (E(f3(x1341,f3(x1342,x1343)),f3(f3(x1341,x1342),x1343))),
% 59.87/59.92 inference(scs_inference,[],[18,2])).
% 59.87/59.92 cnf(162,plain,
% 59.87/59.92 (~P1(f2(a1))+P1(f4(f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[92,10])).
% 59.87/59.92 cnf(172,plain,
% 59.87/59.92 (~P1(f2(a5))+P1(f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[51,10])).
% 59.87/59.92 cnf(183,plain,
% 59.87/59.92 (~P1(f4(a6))+P1(f3(f2(a5),f2(f2(a5))))),
% 59.87/59.92 inference(scs_inference,[],[52,10])).
% 59.87/59.92 cnf(220,plain,
% 59.87/59.92 (P1(x2201)+~P1(f2(f4(x2201)))),
% 59.87/59.92 inference(scs_inference,[],[20,21])).
% 59.87/59.92 cnf(221,plain,
% 59.87/59.92 (P1(f3(f4(f3(a1,a5)),a1))),
% 59.87/59.92 inference(scs_inference,[],[13,127,10])).
% 59.87/59.92 cnf(223,plain,
% 59.87/59.92 (E(f4(a1),f2(f4(f3(a1,a5))))),
% 59.87/59.92 inference(scs_inference,[],[13,127,10,31])).
% 59.87/59.92 cnf(225,plain,
% 59.87/59.92 (E(f2(f4(f3(a1,a5))),f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[13,127,10,31,2])).
% 59.87/59.92 cnf(226,plain,
% 59.87/59.92 (P2(f3(f4(f3(a1,a5)),a1),a1)),
% 59.87/59.92 inference(scs_inference,[],[13,109,127,10,31,2,23])).
% 59.87/59.92 cnf(227,plain,
% 59.87/59.92 (E(f3(f4(f3(x2271,a5)),x2271),x2271)),
% 59.87/59.92 inference(rename_variables,[],[109])).
% 59.87/59.92 cnf(229,plain,
% 59.87/59.92 (P2(a1,a1)),
% 59.87/59.92 inference(scs_inference,[],[13,109,227,127,10,31,2,23,11])).
% 59.87/59.92 cnf(231,plain,
% 59.87/59.92 (P2(f3(f4(a1),a1),a1)),
% 59.87/59.92 inference(scs_inference,[],[13,108,35,11])).
% 59.87/59.92 cnf(232,plain,
% 59.87/59.92 (P1(f3(f4(a1),a1))),
% 59.87/59.92 inference(scs_inference,[],[13,108,10])).
% 59.87/59.92 cnf(234,plain,
% 59.87/59.92 (E(f4(a1),f2(f4(a1)))),
% 59.87/59.92 inference(scs_inference,[],[13,108,10,31])).
% 59.87/59.92 cnf(236,plain,
% 59.87/59.92 (E(f2(f4(a1)),f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[13,108,10,31,2])).
% 59.87/59.92 cnf(237,plain,
% 59.87/59.92 (~P1(f3(f2(a5),f2(f2(a5))))+P1(f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[54,74])).
% 59.87/59.92 cnf(238,plain,
% 59.87/59.92 (~P1(f2(f4(f3(a1,a5))))+P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[225,10])).
% 59.87/59.92 cnf(240,plain,
% 59.87/59.92 (~P2(f2(f4(f3(a1,a5))),x2401)+P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[225,221,10,32,25])).
% 59.87/59.92 cnf(242,plain,
% 59.87/59.92 (~P2(x2421,f2(f4(f3(a1,a5))))+P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[225,221,10,32,25,24])).
% 59.87/59.92 cnf(244,plain,
% 59.87/59.92 (~E(f3(a5,a6),f2(f4(f3(a1,a5))))+P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[225,16,221,10,32,25,24,23])).
% 59.87/59.92 cnf(247,plain,
% 59.87/59.92 (~E(f3(a5,a6),f4(a1))+P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[225,16,223,229,221,10,32,25,24,23,11,3])).
% 59.87/59.92 cnf(248,plain,
% 59.87/59.92 (P1(f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[16,172,32])).
% 59.87/59.92 cnf(249,plain,
% 59.87/59.92 (P1(f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[248,54])).
% 59.87/59.92 cnf(250,plain,
% 59.87/59.92 (P1(f3(f4(f2(a5)),f2(a5)))),
% 59.87/59.92 inference(scs_inference,[],[248,115])).
% 59.87/59.92 cnf(251,plain,
% 59.87/59.92 (P1(f3(f2(a5),f2(f2(a5))))),
% 59.87/59.92 inference(scs_inference,[],[248,183])).
% 59.87/59.92 cnf(252,plain,
% 59.87/59.92 (P1(a6)),
% 59.87/59.92 inference(scs_inference,[],[248,21])).
% 59.87/59.92 cnf(255,plain,
% 59.87/59.92 (E(x2551,f3(f4(f3(x2551,a5)),x2551))),
% 59.87/59.92 inference(rename_variables,[],[127])).
% 59.87/59.92 cnf(257,plain,
% 59.87/59.92 (P2(a6,a6)),
% 59.87/59.92 inference(scs_inference,[],[109,127,248,21,23,12])).
% 59.87/59.92 cnf(264,plain,
% 59.87/59.92 (P1(f2(f4(a1)))+~P1(f2(f4(f3(a1,a5))))),
% 59.87/59.92 inference(scs_inference,[],[109,127,255,234,248,21,23,12,11,10,244,247,238])).
% 59.87/59.92 cnf(270,plain,
% 59.87/59.92 (~P2(f4(a1),x2701)+P1(f2(f4(a1)))),
% 59.87/59.92 inference(scs_inference,[],[109,127,255,67,221,234,248,21,23,12,11,10,244,247,238,240,242,32,33,22,25])).
% 59.87/59.92 cnf(275,plain,
% 59.87/59.92 (P1(f3(f4(f2(a5)),f2(a5)))),
% 59.87/59.92 inference(scs_inference,[],[251,116])).
% 59.87/59.92 cnf(278,plain,
% 59.87/59.92 (P1(f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[251,237])).
% 59.87/59.92 cnf(279,plain,
% 59.87/59.92 (P1(f3(a1,a5))),
% 59.87/59.92 inference(scs_inference,[],[221,220,32])).
% 59.87/59.92 cnf(280,plain,
% 59.87/59.92 (P1(a5)),
% 59.87/59.92 inference(scs_inference,[],[249,20])).
% 59.87/59.92 cnf(282,plain,
% 59.87/59.92 (E(f4(a5),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[279,249,20,31])).
% 59.87/59.92 cnf(284,plain,
% 59.87/59.92 (E(f2(a1),f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[279,249,20,31,2])).
% 59.87/59.92 cnf(285,plain,
% 59.87/59.92 (P2(f3(a1,a5),f3(f3(a1,a5),f2(f3(a1,a5))))),
% 59.87/59.92 inference(scs_inference,[],[38,279,249,20,31,2,23])).
% 59.87/59.92 cnf(286,plain,
% 59.87/59.92 (E(x2861,f3(x2861,f2(x2861)))),
% 59.87/59.92 inference(rename_variables,[],[38])).
% 59.87/59.92 cnf(288,plain,
% 59.87/59.92 (P2(f3(f4(a1),a1),f3(a1,f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[38,286,279,249,231,20,31,2,23,12])).
% 59.87/59.92 cnf(289,plain,
% 59.87/59.92 (E(x2891,f3(x2891,f2(x2891)))),
% 59.87/59.92 inference(rename_variables,[],[38])).
% 59.87/59.92 cnf(290,plain,
% 59.87/59.92 (P2(f3(a1,f2(a1)),a1)),
% 59.87/59.92 inference(scs_inference,[],[38,286,289,229,279,249,231,20,31,2,23,12,11])).
% 59.87/59.92 cnf(292,plain,
% 59.87/59.92 (~P1(f4(a1))+P1(f2(f4(f3(a1,a5))))),
% 59.87/59.92 inference(scs_inference,[],[38,286,289,223,229,279,249,231,20,31,2,23,12,11,10])).
% 59.87/59.92 cnf(304,plain,
% 59.87/59.92 (P1(f8(a7,a1))),
% 59.87/59.92 inference(scs_inference,[],[19,27,2])).
% 59.87/59.92 cnf(305,plain,
% 59.87/59.92 (P2(f8(a7,a1),f3(f4(f8(a7,a1)),f8(a7,a1)))),
% 59.87/59.92 inference(scs_inference,[],[108,304,23])).
% 59.87/59.92 cnf(306,plain,
% 59.87/59.92 (E(x3061,f3(f4(x3061),x3061))),
% 59.87/59.92 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(308,plain,
% 59.87/59.92 (P2(a6,f3(f4(a6),a6))),
% 59.87/59.92 inference(scs_inference,[],[108,306,304,257,23,12])).
% 59.87/59.92 cnf(309,plain,
% 59.87/59.92 (E(x3091,f3(f4(x3091),x3091))),
% 59.87/59.92 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(312,plain,
% 59.87/59.92 (~P1(f2(a1))+P1(f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[108,306,309,284,304,257,23,12,11,10])).
% 59.87/59.92 cnf(318,plain,
% 59.87/59.92 (P1(f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[67,312,32])).
% 59.87/59.92 cnf(319,plain,
% 59.87/59.92 (P2(f8(a7,a1),f3(f8(a7,a1),f2(f8(a7,a1))))),
% 59.87/59.92 inference(scs_inference,[],[38,304,23])).
% 59.87/59.92 cnf(320,plain,
% 59.87/59.92 (E(x3201,f3(x3201,f2(x3201)))),
% 59.87/59.92 inference(rename_variables,[],[38])).
% 59.87/59.92 cnf(322,plain,
% 59.87/59.92 (P2(f3(a1,f2(a1)),f3(a1,f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[38,320,304,290,23,12])).
% 59.87/59.92 cnf(323,plain,
% 59.87/59.92 (E(x3231,f3(x3231,f2(x3231)))),
% 59.87/59.92 inference(rename_variables,[],[38])).
% 59.87/59.92 cnf(324,plain,
% 59.87/59.92 (P2(f3(a6,f2(a6)),f3(f4(a6),a6))),
% 59.87/59.92 inference(scs_inference,[],[38,320,323,304,290,308,23,12,11])).
% 59.87/59.92 cnf(326,plain,
% 59.87/59.92 (P1(f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[38,320,323,304,282,318,290,308,23,12,11,10])).
% 59.87/59.92 cnf(327,plain,
% 59.87/59.92 (P1(f4(f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[38,320,323,304,282,318,290,308,23,12,11,10,162])).
% 59.87/59.92 cnf(328,plain,
% 59.87/59.92 (P2(f2(a5),f2(a5))+~P2(x3281,f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[55,35])).
% 59.87/59.92 cnf(339,plain,
% 59.87/59.92 (P2(f2(a5),f2(a5))+~P1(f3(a6,x3391))),
% 59.87/59.92 inference(scs_inference,[],[59,35])).
% 59.87/59.92 cnf(340,plain,
% 59.87/59.92 (P2(f2(a5),f3(f2(a5),f2(f2(a5))))),
% 59.87/59.92 inference(scs_inference,[],[38,278,23])).
% 59.87/59.92 cnf(348,plain,
% 59.87/59.92 (P2(f3(f2(a5),f2(f2(a5))),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[64,251,23])).
% 59.87/59.92 cnf(350,plain,
% 59.87/59.92 (P2(f2(a5),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[64,340,251,23,12])).
% 59.87/59.92 cnf(351,plain,
% 59.87/59.92 (P2(f4(a6),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[64,340,251,23,12,11])).
% 59.87/59.92 cnf(356,plain,
% 59.87/59.92 (P2(f2(a5),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[348,328])).
% 59.87/59.92 cnf(361,plain,
% 59.87/59.92 (E(x3611,f3(x3611,f2(x3611)))),
% 59.87/59.92 inference(rename_variables,[],[38])).
% 59.87/59.92 cnf(362,plain,
% 59.87/59.92 (P2(f3(f2(a5),f2(f2(a5))),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[65,38,361,356,250,350,23,12,11])).
% 59.87/59.92 cnf(366,plain,
% 59.87/59.92 (P2(f2(a1),f3(f2(a1),f2(f2(a1))))),
% 59.87/59.92 inference(scs_inference,[],[38,326,23])).
% 59.87/59.92 cnf(367,plain,
% 59.87/59.92 (E(x3671,f3(x3671,f2(x3671)))),
% 59.87/59.92 inference(rename_variables,[],[38])).
% 59.87/59.92 cnf(371,plain,
% 59.87/59.92 (P2(f4(a6),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[64,38,367,362,326,257,23,12,11])).
% 59.87/59.92 cnf(373,plain,
% 59.87/59.92 (P2(a5,f3(a5,f2(a5)))),
% 59.87/59.92 inference(scs_inference,[],[38,280,23])).
% 59.87/59.92 cnf(380,plain,
% 59.87/59.92 (P2(f2(f4(a1)),f2(f4(a1)))+~P2(f4(a1),x3801)),
% 59.87/59.92 inference(scs_inference,[],[270,35])).
% 59.87/59.92 cnf(381,plain,
% 59.87/59.92 (P2(f4(a5),f3(f4(a5),f2(f4(a5))))),
% 59.87/59.92 inference(scs_inference,[],[38,318,23])).
% 59.87/59.92 cnf(390,plain,
% 59.87/59.92 (E(f3(x3901,f2(x3901)),x3901)),
% 59.87/59.92 inference(rename_variables,[],[14])).
% 59.87/59.92 cnf(391,plain,
% 59.87/59.92 (P2(f3(a1,a5),f3(a1,a5))),
% 59.87/59.92 inference(scs_inference,[],[14,390,284,285,3,12])).
% 59.87/59.92 cnf(392,plain,
% 59.87/59.92 (E(f3(x3921,f2(x3921)),x3921)),
% 59.87/59.92 inference(rename_variables,[],[14])).
% 59.87/59.92 cnf(393,plain,
% 59.87/59.92 (P2(a1,f3(a1,f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[14,390,392,284,285,322,3,12,11])).
% 59.87/59.92 cnf(401,plain,
% 59.87/59.92 (P1(f4(f3(a1,a5)))+~P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[292,20])).
% 59.87/59.92 cnf(403,plain,
% 59.87/59.92 (E(f3(x4031,f2(x4031)),x4031)),
% 59.87/59.92 inference(rename_variables,[],[14])).
% 59.87/59.92 cnf(410,plain,
% 59.87/59.92 (E(f2(a5),f3(f4(a6),f2(f4(a6))))),
% 59.87/59.92 inference(scs_inference,[],[14,403,38,108,304,319,39,391,3,12,11,10,2])).
% 59.87/59.92 cnf(411,plain,
% 59.87/59.92 (P2(f4(f3(a1,a5)),f4(f3(a1,a5)))+~P1(f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[401,35])).
% 59.87/59.92 cnf(413,plain,
% 59.87/59.92 (E(f3(x4131,f2(x4131)),x4131)),
% 59.87/59.92 inference(rename_variables,[],[14])).
% 59.87/59.92 cnf(414,plain,
% 59.87/59.92 (P2(f2(a1),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[14,413,366,282,3,12])).
% 59.87/59.92 cnf(424,plain,
% 59.87/59.92 (P1(f3(f4(a6),f2(f4(a6))))),
% 59.87/59.92 inference(scs_inference,[],[14,38,410,381,249,12,11,10])).
% 59.87/59.92 cnf(425,plain,
% 59.87/59.92 (E(f3(x4251,x4252),f3(x4251,f3(x4252,f2(x4252))))),
% 59.87/59.92 inference(scs_inference,[],[14,6,2])).
% 59.87/59.92 cnf(426,plain,
% 59.87/59.92 (E(f3(x4261,f3(x4262,f2(x4262))),f3(x4261,x4262))),
% 59.87/59.92 inference(scs_inference,[],[425,2])).
% 59.87/59.92 cnf(427,plain,
% 59.87/59.92 (~E(a1,f3(f4(a7),f3(a7,f2(a7))))),
% 59.87/59.92 inference(scs_inference,[],[43,425,2,3])).
% 59.87/59.92 cnf(428,plain,
% 59.87/59.92 (P2(a5,a5)),
% 59.87/59.92 inference(scs_inference,[],[14,43,373,425,2,3,12])).
% 59.87/59.92 cnf(430,plain,
% 59.87/59.92 (P2(f3(a5,f2(a5)),a5)),
% 59.87/59.92 inference(scs_inference,[],[14,38,43,373,425,2,3,12,11])).
% 59.87/59.92 cnf(436,plain,
% 59.87/59.92 (~E(a1,f3(f3(f4(a7),a7),f2(a7)))),
% 59.87/59.92 inference(scs_inference,[],[427,18,3])).
% 59.87/59.92 cnf(438,plain,
% 59.87/59.92 (~E(f3(a1,f2(a1)),a7)),
% 59.87/59.92 inference(scs_inference,[],[36,427,18,393,3,12])).
% 59.87/59.92 cnf(439,plain,
% 59.87/59.92 (P1(f3(a5,f3(a6,f2(a6))))),
% 59.87/59.92 inference(scs_inference,[],[36,427,16,18,393,425,3,12,10])).
% 59.87/59.92 cnf(441,plain,
% 59.87/59.92 (E(f4(f3(a6,f2(a6))),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[36,427,16,18,393,425,3,12,10,31])).
% 59.87/59.92 cnf(443,plain,
% 59.87/59.92 (~P2(a1,f3(f3(f4(a7),a7),f2(a7)))),
% 59.87/59.92 inference(scs_inference,[],[36,427,16,18,393,425,3,12,10,31,22])).
% 59.87/59.92 cnf(445,plain,
% 59.87/59.92 (E(f2(a5),f4(f3(a6,f2(a6))))),
% 59.87/59.92 inference(scs_inference,[],[36,427,16,18,393,425,3,12,10,31,22,2])).
% 59.87/59.92 cnf(449,plain,
% 59.87/59.92 (~E(f3(a1,f2(a1)),f3(f4(a7),a7))),
% 59.87/59.92 inference(scs_inference,[],[49,438,393,22,12])).
% 59.87/59.92 cnf(450,plain,
% 59.87/59.92 (P1(f4(f3(a6,f2(a6))))),
% 59.87/59.92 inference(scs_inference,[],[49,445,278,438,393,22,12,10])).
% 59.87/59.92 cnf(451,plain,
% 59.87/59.92 (P1(f3(a6,f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[49,445,278,438,393,22,12,10,21])).
% 59.87/59.92 cnf(453,plain,
% 59.87/59.92 (E(f4(f2(a6)),f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[49,445,278,438,393,22,12,10,21,31])).
% 59.87/59.92 cnf(455,plain,
% 59.87/59.92 (E(f2(a6),f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[49,445,278,438,393,22,12,10,21,31,2])).
% 59.87/59.92 cnf(459,plain,
% 59.87/59.92 (P2(f2(a5),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[451,339])).
% 59.87/59.92 cnf(461,plain,
% 59.87/59.92 (~P2(f3(a1,f2(a1)),f3(f4(a7),a7))),
% 59.87/59.92 inference(scs_inference,[],[449,22])).
% 59.87/59.92 cnf(463,plain,
% 59.87/59.92 (~E(f3(a1,f2(a1)),f3(a7,f2(a7)))),
% 59.87/59.92 inference(scs_inference,[],[83,449,393,22,12])).
% 59.87/59.92 cnf(464,plain,
% 59.87/59.92 (~P1(f2(a6))+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[83,455,449,393,22,12,10])).
% 59.87/59.92 cnf(466,plain,
% 59.87/59.92 (~P2(f2(a6),x4661)+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[83,455,451,449,393,22,12,10,32,25])).
% 59.87/59.92 cnf(472,plain,
% 59.87/59.92 (~E(f8(a7,a1),f4(f2(a6)))+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[83,455,304,451,449,453,393,22,12,10,32,25,24,23,3])).
% 59.87/59.92 cnf(473,plain,
% 59.87/59.92 (~E(f3(a5,a6),f2(a6))+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[83,455,304,41,451,449,453,393,22,12,10,32,25,24,23,3,11])).
% 59.87/59.92 cnf(477,plain,
% 59.87/59.92 (P1(f3(f3(a5,a6),f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[134,439,463,22,10])).
% 59.87/59.92 cnf(479,plain,
% 59.87/59.92 (E(f4(f2(a6)),f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[134,439,463,22,10,31])).
% 59.87/59.92 cnf(481,plain,
% 59.87/59.92 (E(f2(f3(a5,a6)),f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[134,439,463,22,10,31,2])).
% 59.87/59.92 cnf(482,plain,
% 59.87/59.92 (~P1(f2(f3(a5,a6)))+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[481,10])).
% 59.87/59.92 cnf(490,plain,
% 59.87/59.92 (~E(f3(f4(f8(a7,a1)),f8(a7,a1)),f2(f3(a5,a6)))+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[481,304,305,45,10,32,25,24,23,12])).
% 59.87/59.92 cnf(491,plain,
% 59.87/59.92 (~E(f3(a5,a6),f2(f3(a5,a6)))+P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[481,304,41,305,45,10,32,25,24,23,12,11])).
% 59.87/59.92 cnf(492,plain,
% 59.87/59.92 (P2(f4(f2(a6)),f4(f2(a6)))+~P2(f2(a6),x4921)),
% 59.87/59.92 inference(scs_inference,[],[466,35])).
% 59.87/59.92 cnf(493,plain,
% 59.87/59.92 (~P1(f4(f2(a6)))+P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[479,10])).
% 59.87/59.92 cnf(496,plain,
% 59.87/59.92 (P1(f2(f3(a5,a6)))+~P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[479,10,472,473,482])).
% 59.87/59.92 cnf(502,plain,
% 59.87/59.92 (~P2(f4(f2(a6)),x5021)+P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[479,477,10,472,473,482,490,491,32,33,25])).
% 59.87/59.92 cnf(515,plain,
% 59.87/59.92 (P2(f3(f4(f2(a5)),f2(a5)),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[15,275,23])).
% 59.87/59.92 cnf(516,plain,
% 59.87/59.92 (E(f3(f4(x5161),x5161),x5161)),
% 59.87/59.92 inference(rename_variables,[],[15])).
% 59.87/59.92 cnf(521,plain,
% 59.87/59.92 (P1(f3(f4(f2(a1)),f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[15,516,92,327,275,23,3,2,10])).
% 59.87/59.92 cnf(522,plain,
% 59.87/59.92 (P2(f3(f4(f2(a1)),f2(a1)),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[15,521,23])).
% 59.87/59.92 cnf(563,plain,
% 59.87/59.92 (P1(f2(f4(a1)))),
% 59.87/59.92 inference(scs_inference,[],[221,264,32])).
% 59.87/59.92 cnf(570,plain,
% 59.87/59.92 (P2(f4(a1),f4(a1))),
% 59.87/59.92 inference(scs_inference,[],[15,236,234,563,20,23,3,11])).
% 59.87/59.92 cnf(571,plain,
% 59.87/59.92 (P1(f2(f4(f3(a1,a5))))),
% 59.87/59.92 inference(scs_inference,[],[15,236,234,223,563,20,23,3,11,10])).
% 59.87/59.92 cnf(574,plain,
% 59.87/59.92 (E(f2(f4(a1)),f3(f4(f4(a1)),f4(a1)))),
% 59.87/59.92 inference(scs_inference,[],[15,236,234,223,563,20,23,3,11,10,411,401,2])).
% 59.87/59.92 cnf(575,plain,
% 59.87/59.92 (P2(f4(a1),f3(f4(a1),f2(f4(a1))))),
% 59.87/59.92 inference(scs_inference,[],[15,236,38,234,223,563,20,23,3,11,10,411,401,2,12])).
% 59.87/59.92 cnf(577,plain,
% 59.87/59.92 (P2(f2(f4(a1)),f2(f4(a1)))),
% 59.87/59.92 inference(scs_inference,[],[575,380])).
% 59.87/59.92 cnf(581,plain,
% 59.87/59.92 (E(f3(f4(f4(a6)),f4(a6)),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[15,225,39,571,23,3])).
% 59.87/59.92 cnf(584,plain,
% 59.87/59.92 (P1(f3(f4(f4(a1)),f4(a1)))),
% 59.87/59.92 inference(scs_inference,[],[15,225,236,574,577,39,571,563,23,3,11,10])).
% 59.87/59.92 cnf(585,plain,
% 59.87/59.92 (E(f2(a5),f3(f4(f4(a6)),f4(a6)))),
% 59.87/59.92 inference(scs_inference,[],[15,225,236,574,577,39,571,563,23,3,11,10,2])).
% 59.87/59.92 cnf(587,plain,
% 59.87/59.92 (E(f3(f4(x5871),x5871),x5871)),
% 59.87/59.92 inference(rename_variables,[],[15])).
% 59.87/59.92 cnf(593,plain,
% 59.87/59.92 (P1(f3(f4(f4(a6)),f4(a6)))),
% 59.87/59.92 inference(scs_inference,[],[15,587,38,585,282,249,584,570,23,3,11,10])).
% 59.87/59.92 cnf(596,plain,
% 59.87/59.92 (P2(f3(f4(f4(a6)),f4(a6)),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[15,593,23])).
% 59.87/59.92 cnf(600,plain,
% 59.87/59.92 (P2(f2(f3(a5,a6)),f2(f3(a5,a6)))+~P2(f4(f2(a6)),x6001)),
% 59.87/59.92 inference(scs_inference,[],[502,35])).
% 59.87/59.92 cnf(608,plain,
% 59.87/59.92 (E(f3(f4(f3(x6081,a6)),x6081),x6081)),
% 59.87/59.92 inference(scs_inference,[],[18,108,30])).
% 59.87/59.92 cnf(610,plain,
% 59.87/59.92 (E(f3(f3(x6101,x6102),x6103),f3(x6101,f3(x6102,x6103)))),
% 59.87/59.92 inference(rename_variables,[],[18])).
% 59.87/59.92 cnf(612,plain,
% 59.87/59.92 (E(f3(f3(a7,a5),a6),f3(a1,f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[18,610,93,108,30,3])).
% 59.87/59.92 cnf(614,plain,
% 59.87/59.92 (E(x6141,f3(f4(f3(x6141,a6)),x6141))),
% 59.87/59.92 inference(scs_inference,[],[18,610,93,108,30,3,2])).
% 59.87/59.92 cnf(618,plain,
% 59.87/59.92 (E(f3(f3(a7,a5),a6),f3(f3(a1,a5),a6))),
% 59.87/59.92 inference(scs_inference,[],[18,80,612,2,3])).
% 59.87/59.92 cnf(630,plain,
% 59.87/59.92 (E(f3(f3(a1,a5),a6),f3(f3(a7,a5),a6))),
% 59.87/59.92 inference(scs_inference,[],[618,2])).
% 59.87/59.92 cnf(632,plain,
% 59.87/59.92 (E(x6321,f3(f4(x6321),x6321))),
% 59.87/59.92 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(637,plain,
% 59.87/59.92 (E(x6371,f3(f4(x6371),x6371))),
% 59.87/59.92 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(638,plain,
% 59.87/59.92 (P2(f3(f4(a5),a5),f3(a5,f2(a5)))),
% 59.87/59.92 inference(scs_inference,[],[19,108,632,637,608,618,459,373,248,2,23,3,12,11])).
% 59.87/59.92 cnf(673,plain,
% 59.87/59.92 (E(x6731,f3(f4(x6731),x6731))),
% 59.87/59.92 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(675,plain,
% 59.87/59.92 (P2(f2(a1),f3(f4(f2(a1)),f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[108,673,318,414,23,12])).
% 59.87/59.92 cnf(698,plain,
% 59.87/59.92 (E(f2(f3(a5,a6)),f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[455,479,3,2])).
% 59.87/59.92 cnf(699,plain,
% 59.87/59.92 (~P1(f2(a6))+P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[455,479,3,2,10])).
% 59.87/59.92 cnf(701,plain,
% 59.87/59.92 (~P2(f2(a6),x7011)+P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[455,479,451,3,2,10,32,25])).
% 59.87/59.92 cnf(710,plain,
% 59.87/59.92 (~P1(f2(f3(a5,a6)))+P1(f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[698,10])).
% 59.87/59.92 cnf(725,plain,
% 59.87/59.92 (P1(f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[477,710,32])).
% 59.87/59.92 cnf(726,plain,
% 59.87/59.92 (P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[725,464])).
% 59.87/59.92 cnf(727,plain,
% 59.87/59.92 (P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[725,699])).
% 59.87/59.92 cnf(729,plain,
% 59.87/59.92 (P2(f2(a6),f3(f2(a6),f2(f2(a6))))),
% 59.87/59.92 inference(scs_inference,[],[38,725,23])).
% 59.87/59.92 cnf(732,plain,
% 59.87/59.92 (P1(f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[729,466])).
% 59.87/59.92 cnf(734,plain,
% 59.87/59.92 (P2(f4(f2(a6)),f4(f2(a6)))),
% 59.87/59.92 inference(scs_inference,[],[729,492])).
% 59.87/59.92 cnf(735,plain,
% 59.87/59.92 (P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[726,493])).
% 59.87/59.92 cnf(736,plain,
% 59.87/59.92 (P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[727,496])).
% 59.87/59.92 cnf(743,plain,
% 59.87/59.92 (P1(f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[729,701])).
% 59.87/59.92 cnf(749,plain,
% 59.87/59.92 (P2(f2(f3(a5,a6)),f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[734,600])).
% 59.87/59.92 cnf(762,plain,
% 59.87/59.92 (E(f4(a6),f4(f3(a6,f2(a6))))),
% 59.87/59.92 inference(scs_inference,[],[39,481,445,596,727,23,12,3])).
% 59.87/59.92 cnf(763,plain,
% 59.87/59.92 (P2(f4(f2(a6)),f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[39,481,445,749,596,727,23,12,3,11])).
% 59.87/59.92 cnf(790,plain,
% 59.87/59.92 (P2(f4(f2(a1)),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[69,327,23])).
% 59.87/59.92 cnf(792,plain,
% 59.87/59.92 (E(f4(f2(a1)),f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[69,284,327,23,3])).
% 59.87/59.92 cnf(793,plain,
% 59.87/59.92 (E(f4(a5),f4(f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[69,284,327,23,3,2])).
% 59.87/59.92 cnf(797,plain,
% 59.87/59.92 (~E(f3(a1,f2(a1)),f3(f3(f4(a7),a7),f2(a7)))),
% 59.87/59.92 inference(scs_inference,[],[443,393,12])).
% 59.87/59.92 cnf(805,plain,
% 59.87/59.92 (P2(f2(a1),f4(f2(a1)))),
% 59.87/59.92 inference(scs_inference,[],[92,326,23])).
% 59.87/59.92 cnf(814,plain,
% 59.87/59.92 (E(x8141,f3(f4(x8141),x8141))),
% 59.87/59.92 inference(rename_variables,[],[108])).
% 59.87/59.92 cnf(816,plain,
% 59.87/59.92 (P2(f3(a5,f2(a5)),f3(f4(a5),a5))),
% 59.87/59.92 inference(scs_inference,[],[108,814,430,280,23,12])).
% 59.87/59.92 cnf(852,plain,
% 59.87/59.92 (P1(f3(f4(a1),f3(a1,f2(a1))))),
% 59.87/59.92 inference(scs_inference,[],[232,425,10])).
% 59.87/59.92 cnf(864,plain,
% 59.87/59.92 (E(f4(a6),f2(f4(f3(a6,a5))))),
% 59.87/59.92 inference(scs_inference,[],[252,127,10,31])).
% 59.87/59.92 cnf(870,plain,
% 59.87/59.92 (E(f4(a6),f2(f4(a6)))),
% 59.87/59.92 inference(scs_inference,[],[252,108,10,31])).
% 59.87/59.92 cnf(872,plain,
% 59.87/59.92 (E(f2(f4(a6)),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[252,108,10,31,2])).
% 59.87/59.92 cnf(876,plain,
% 59.87/59.92 (E(f4(a6),f2(f4(f3(a6,a6))))),
% 59.87/59.92 inference(scs_inference,[],[252,614,10,31])).
% 59.87/59.92 cnf(884,plain,
% 59.87/59.92 (P1(f3(a6,a5))),
% 59.87/59.92 inference(scs_inference,[],[248,864,10,220])).
% 59.87/59.92 cnf(888,plain,
% 59.87/59.92 (E(f4(a5),f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[248,864,10,220,20,31])).
% 59.87/59.92 cnf(890,plain,
% 59.87/59.92 (E(f2(a6),f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[248,864,10,220,20,31,2])).
% 59.87/59.92 cnf(898,plain,
% 59.87/59.92 (P1(f3(a6,a6))),
% 59.87/59.92 inference(scs_inference,[],[248,876,10,220])).
% 59.87/59.92 cnf(902,plain,
% 59.87/59.92 (E(f4(a6),f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[248,876,10,220,20,31])).
% 59.87/59.92 cnf(904,plain,
% 59.87/59.92 (E(f2(a6),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[248,876,10,220,20,31,2])).
% 59.87/59.92 cnf(922,plain,
% 59.87/59.92 (P1(f3(a1,f3(a5,f2(a5))))),
% 59.87/59.92 inference(scs_inference,[],[279,425,10])).
% 59.87/59.92 cnf(926,plain,
% 59.87/59.92 (E(f2(a1),f4(f3(a5,f2(a5))))),
% 59.87/59.92 inference(scs_inference,[],[279,425,10,31,2])).
% 59.87/59.92 cnf(930,plain,
% 59.87/59.92 (E(f4(f2(a5)),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[926,326,10,21,31])).
% 59.87/59.92 cnf(932,plain,
% 59.87/59.92 (E(f2(a5),f4(f2(a5)))),
% 59.87/59.92 inference(scs_inference,[],[926,326,10,21,31,2])).
% 59.87/59.92 cnf(934,plain,
% 59.87/59.92 (P1(f4(f2(a5)))),
% 59.87/59.92 inference(scs_inference,[],[932,278,10])).
% 59.87/59.92 cnf(939,plain,
% 59.87/59.92 (E(f4(a5),f2(f4(f3(a5,a5))))),
% 59.87/59.92 inference(scs_inference,[],[280,127,10,31])).
% 59.87/59.92 cnf(943,plain,
% 59.87/59.92 (P1(f3(f4(a5),a5))),
% 59.87/59.92 inference(scs_inference,[],[280,108,10])).
% 59.87/59.92 cnf(945,plain,
% 59.87/59.92 (E(f4(a5),f2(f4(a5)))),
% 59.87/59.92 inference(scs_inference,[],[280,108,10,31])).
% 59.87/59.92 cnf(963,plain,
% 59.87/59.92 (E(f4(a5),f2(a5))),
% 59.87/59.92 inference(scs_inference,[],[318,939,10,220,20,31])).
% 59.87/59.92 cnf(965,plain,
% 59.87/59.92 (E(f2(a5),f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[318,939,10,220,20,31,2])).
% 59.87/59.92 cnf(970,plain,
% 59.87/59.92 (P1(f2(f4(a5)))),
% 59.87/59.92 inference(scs_inference,[],[318,945,10])).
% 59.87/59.92 cnf(995,plain,
% 59.87/59.92 (E(f2(a1),f2(a6))),
% 59.87/59.92 inference(scs_inference,[],[284,888,3])).
% 59.87/59.92 cnf(998,plain,
% 59.87/59.92 (E(f2(a6),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[284,805,790,888,3,12,11,2])).
% 59.87/59.92 cnf(1003,plain,
% 59.87/59.92 (E(f2(a5),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[284,522,963,675,3,12,11,2])).
% 59.87/59.92 cnf(1137,plain,
% 59.87/59.92 (E(f4(f3(a6,f2(a6))),f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[441,965,450,23,3])).
% 59.87/59.92 cnf(1140,plain,
% 59.87/59.92 (E(f4(f3(a6,f2(a6))),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[441,1003,3])).
% 59.87/59.92 cnf(1153,plain,
% 59.87/59.92 (E(f4(f2(a6)),f4(a5))),
% 59.87/59.92 inference(scs_inference,[],[453,890,732,23,3])).
% 59.87/59.92 cnf(1161,plain,
% 59.87/59.92 (E(f4(f2(a6)),f4(a6))),
% 59.87/59.92 inference(scs_inference,[],[453,904,3])).
% 59.87/59.92 cnf(1166,plain,
% 59.87/59.92 (E(f4(f2(a6)),f2(a1))),
% 59.87/59.92 inference(scs_inference,[],[453,998,3])).
% 59.87/59.92 cnf(1180,plain,
% 59.87/59.92 (E(f4(a5),f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[481,1153,3,2])).
% 59.87/59.92 cnf(1182,plain,
% 59.87/59.92 (E(f4(a6),f2(f3(a5,a6)))),
% 59.87/59.92 inference(scs_inference,[],[481,1161,3,2])).
% 59.87/59.92 cnf(1185,plain,
% 59.87/59.93 (E(f2(f3(a5,a6)),f2(a1))),
% 59.87/59.93 inference(scs_inference,[],[481,1166,3])).
% 59.87/59.93 cnf(1225,plain,
% 59.87/59.93 (E(f3(f4(f4(a6)),f4(a6)),f2(a1))),
% 59.87/59.93 inference(scs_inference,[],[581,1003,3])).
% 59.87/59.93 cnf(1250,plain,
% 59.87/59.93 (E(x12501,f3(f4(f3(x12501,a6)),x12501))),
% 59.87/59.93 inference(rename_variables,[],[614])).
% 59.87/59.93 cnf(1253,plain,
% 59.87/59.93 (E(x12531,f3(f4(f3(x12531,a6)),x12531))),
% 59.87/59.93 inference(rename_variables,[],[614])).
% 59.87/59.93 cnf(1254,plain,
% 59.87/59.93 (P2(f3(f4(f3(a1,a6)),a1),a1)),
% 59.87/59.93 inference(scs_inference,[],[614,1250,1253,229,428,252,23,12,11])).
% 59.87/59.93 cnf(1266,plain,
% 59.87/59.93 (P1(f3(f2(a6),f2(f2(a6))))),
% 59.87/59.93 inference(scs_inference,[],[725,38,10])).
% 59.87/59.93 cnf(1295,plain,
% 59.87/59.93 (E(f4(a6),f4(a5))),
% 59.87/59.93 inference(scs_inference,[],[762,1137,3])).
% 59.87/59.93 cnf(1296,plain,
% 59.87/59.93 (E(f4(a5),f4(a6))),
% 59.87/59.93 inference(scs_inference,[],[762,1137,3,2])).
% 59.87/59.93 cnf(1297,plain,
% 59.87/59.93 (E(f4(a6),f2(a1))),
% 59.87/59.93 inference(scs_inference,[],[762,1140,3])).
% 59.87/59.93 cnf(1298,plain,
% 59.87/59.93 (E(f2(a1),f4(a6))),
% 59.87/59.93 inference(scs_inference,[],[762,1140,3,2])).
% 59.87/59.93 cnf(1300,plain,
% 59.87/59.93 (P1(f3(f3(a5,a6),a5))),
% 59.87/59.93 inference(scs_inference,[],[763,1180,24,34])).
% 59.87/59.93 cnf(1331,plain,
% 59.87/59.93 (E(f4(f2(a1)),f2(f3(a5,a6)))),
% 59.87/59.93 inference(scs_inference,[],[792,1180,3])).
% 59.87/59.93 cnf(1339,plain,
% 59.87/59.93 (~P2(a7,a1)),
% 59.87/59.93 inference(scs_inference,[],[19,2,22])).
% 59.87/59.93 cnf(1340,plain,
% 59.87/59.93 (~E(f3(f4(f3(a1,a5)),a1),a7)),
% 59.87/59.93 inference(scs_inference,[],[1339,226,11])).
% 59.87/59.93 cnf(1346,plain,
% 59.87/59.93 (~E(f3(f4(a1),a1),a7)),
% 59.87/59.93 inference(scs_inference,[],[1339,231,11])).
% 59.87/59.93 cnf(1353,plain,
% 59.87/59.93 (~E(f3(a7,a5),f3(f3(a1,a5),f2(f3(a1,a5))))),
% 59.87/59.93 inference(scs_inference,[],[19,38,2,29])).
% 59.87/59.93 cnf(1356,plain,
% 59.87/59.93 (~E(f3(a1,a5),f3(a7,a5))),
% 59.87/59.93 inference(scs_inference,[],[1353,285,22,11])).
% 59.87/59.93 cnf(1357,plain,
% 59.87/59.93 (~E(a7,a1)),
% 59.87/59.93 inference(scs_inference,[],[1356,2,5])).
% 59.87/59.93 cnf(1367,plain,
% 59.87/59.93 (~P2(f3(a1,a5),f3(a7,a5))),
% 59.87/59.93 inference(scs_inference,[],[1356,22])).
% 59.87/59.93 cnf(1398,plain,
% 59.87/59.93 (P1(f3(f3(f4(a1),a1),f2(a1)))),
% 59.87/59.93 inference(scs_inference,[],[852,134,10])).
% 59.87/59.93 cnf(1422,plain,
% 59.87/59.93 (P2(f4(a6),f2(f4(a6)))),
% 59.87/59.93 inference(scs_inference,[],[870,248,23])).
% 59.87/59.93 cnf(1427,plain,
% 59.87/59.93 (P2(f2(f4(a6)),f2(f4(a6)))),
% 59.87/59.93 inference(scs_inference,[],[870,1422,596,12,11])).
% 59.87/59.93 cnf(1430,plain,
% 59.87/59.93 (P2(f2(f4(a6)),f4(a6))),
% 59.87/59.93 inference(scs_inference,[],[870,351,350,12,11])).
% 59.87/59.93 cnf(1451,plain,
% 59.87/59.93 (E(f2(f4(a6)),f4(a5))),
% 59.87/59.93 inference(scs_inference,[],[872,1295,3])).
% 59.87/59.93 cnf(1458,plain,
% 59.87/59.93 (E(f2(a1),f2(f4(a6)))),
% 59.87/59.93 inference(scs_inference,[],[872,1297,3,2])).
% 59.87/59.93 cnf(1459,plain,
% 59.87/59.93 (E(f2(f4(a6)),f2(a5))),
% 59.87/59.93 inference(scs_inference,[],[872,39,3])).
% 59.87/59.93 cnf(1488,plain,
% 59.87/59.93 (P1(f3(f3(a6,a5),f2(f3(a6,a5))))),
% 59.87/59.93 inference(scs_inference,[],[884,38,10])).
% 59.87/59.93 cnf(1490,plain,
% 59.87/59.93 (P1(f3(f4(f3(a6,a5)),f3(a6,a5)))),
% 59.87/59.93 inference(scs_inference,[],[884,108,10])).
% 59.87/59.93 cnf(1559,plain,
% 59.87/59.93 (E(f2(a6),f2(a5))),
% 59.87/59.93 inference(scs_inference,[],[890,963,3])).
% 59.87/59.93 cnf(1560,plain,
% 59.87/59.93 (E(f2(a5),f2(a6))),
% 59.87/59.93 inference(scs_inference,[],[890,963,3,2])).
% 59.87/59.93 cnf(1562,plain,
% 59.87/59.93 (E(f2(a6),f2(f4(a5)))),
% 59.87/59.93 inference(scs_inference,[],[890,945,3])).
% 59.87/59.93 cnf(1568,plain,
% 59.87/59.93 (P1(f3(f3(a6,a6),f2(f3(a6,a6))))),
% 59.87/59.93 inference(scs_inference,[],[898,38,10])).
% 59.87/59.93 cnf(1606,plain,
% 59.87/59.93 (E(f4(a6),f2(f4(a5)))),
% 59.87/59.93 inference(scs_inference,[],[902,1562,371,1430,12,11,3])).
% 59.87/59.93 cnf(1682,plain,
% 59.87/59.93 (P1(f3(f3(a1,a5),f2(a5)))),
% 59.87/59.93 inference(scs_inference,[],[922,134,10])).
% 59.87/59.93 cnf(1684,plain,
% 59.87/59.93 (E(f4(f2(a5)),f2(f3(a1,a5)))),
% 59.87/59.93 inference(scs_inference,[],[922,134,10,31])).
% 59.87/59.93 cnf(1688,plain,
% 59.87/59.93 (P1(f2(f3(a1,a5)))),
% 59.87/59.93 inference(scs_inference,[],[1684,934,10])).
% 59.87/59.93 cnf(1713,plain,
% 59.87/59.93 (E(f4(f2(a5)),f2(a6))),
% 59.87/59.93 inference(scs_inference,[],[930,1560,3])).
% 59.87/59.93 cnf(1728,plain,
% 59.87/59.93 (E(f4(f2(a5)),f4(a5))),
% 59.87/59.93 inference(scs_inference,[],[930,965,3])).
% 59.87/59.93 cnf(1737,plain,
% 59.87/59.93 (E(f2(a5),f2(f3(a1,a5)))),
% 59.87/59.93 inference(scs_inference,[],[932,515,278,1684,23,12,3])).
% 59.87/59.93 cnf(1744,plain,
% 59.87/59.93 (P2(f4(a6),f4(f2(a5)))),
% 59.87/59.93 inference(scs_inference,[],[932,371,12])).
% 59.87/59.93 cnf(1778,plain,
% 59.87/59.93 (P1(f3(f4(a5),f3(a5,f2(a5))))),
% 59.87/59.93 inference(scs_inference,[],[943,425,10])).
% 59.87/59.93 cnf(1868,plain,
% 59.87/59.93 (E(f3(x18681,f2(a1)),f3(x18681,f4(a6)))),
% 59.87/59.93 inference(scs_inference,[],[1298,1300,1346,35,27,4,7,6])).
% 59.87/59.93 cnf(1878,plain,
% 59.87/59.93 (E(f3(f4(a1),a1),f3(a1,f2(a1)))),
% 59.87/59.93 inference(scs_inference,[],[1298,1300,1346,288,132,1398,1254,35,27,4,7,6,8,9,32,33,5,25,22])).
% 59.87/59.93 cnf(1880,plain,
% 59.87/59.93 (~E(a7,f3(f4(a1),a1))),
% 59.87/59.93 inference(scs_inference,[],[1298,1300,1346,288,132,1398,1254,35,27,4,7,6,8,9,32,33,5,25,22,2])).
% 59.87/59.93 cnf(1881,plain,
% 59.87/59.93 (~E(f3(a7,a5),f3(f4(a1),f3(a1,a5)))),
% 59.87/59.93 inference(scs_inference,[],[1298,1300,1346,288,132,1398,1254,18,35,27,4,7,6,8,9,32,33,5,25,22,2,29])).
% 59.87/59.93 cnf(1889,plain,
% 59.87/59.93 (P2(f2(f4(a6)),f4(a5))),
% 59.87/59.93 inference(scs_inference,[],[1298,1185,1451,1713,1300,1346,735,288,1427,132,1398,1254,630,725,1356,18,35,27,4,7,6,8,9,32,33,5,25,22,2,29,30,34,23,12])).
% 59.87/59.93 cnf(1891,plain,
% 59.87/59.93 (P2(f4(a5),f2(f4(a6)))),
% 59.87/59.93 inference(scs_inference,[],[1298,1559,1185,1451,1713,1300,1346,1737,735,288,1427,132,1398,1254,630,725,1356,18,35,27,4,7,6,8,9,32,33,5,25,22,2,29,30,34,23,12,3,11])).
% 59.87/59.93 cnf(1912,plain,
% 59.87/59.93 (~E(f3(f4(a1),f3(a1,a5)),f3(a7,a5))),
% 59.87/59.93 inference(scs_inference,[],[1688,1881,1490,1266,324,998,1296,35,27,4,7,6,8,9,33,32,5,22,2])).
% 59.87/59.93 cnf(1920,plain,
% 59.87/59.93 (P2(f2(a5),f4(a5))),
% 59.87/59.93 inference(scs_inference,[],[1459,1889,1688,736,1881,1891,1490,1868,797,1266,324,998,1296,1331,630,1356,35,27,4,7,6,8,9,33,32,5,22,2,30,34,12,3,11])).
% 59.87/59.93 cnf(1954,plain,
% 59.87/59.93 (P1(f2(f3(a6,a5)))),
% 59.87/59.93 inference(scs_inference,[],[1682,1880,1488,1560,35,27,4,7,6,8,9,32])).
% 59.87/59.93 cnf(1969,plain,
% 59.87/59.93 (~P2(f3(f4(a1),a1),f3(f4(a7),a7))),
% 59.87/59.93 inference(scs_inference,[],[1920,1728,793,743,1682,1880,461,1878,1340,1488,424,1357,638,1560,1182,934,614,35,27,4,7,6,8,9,32,33,5,22,2,34,23,12,3,11])).
% 59.87/59.93 cnf(1999,plain,
% 59.87/59.93 ($false),
% 59.87/59.93 inference(scs_inference,[],[1458,1606,1954,970,1225,1969,1568,1778,1744,816,436,81,1912,232,995,1367,1295,426,630,1356,35,27,4,7,6,8,9,33,32,5,22,2,34,23,12,3,11,30]),
% 59.87/59.93 ['proof']).
% 59.87/59.93 % SZS output end Proof
% 59.87/59.93 % Total time :59.300000s
%------------------------------------------------------------------------------