%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT001-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 04:40:07 EDT 2024
% Result : Unsatisfiable 60.96s 61.11s
% Output : CNFRefutation 60.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : CAT001-3 : TPTP v8.2.0. Released v1.0.0.
% 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n004.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:02:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.19/0.59 start to proof:theBenchmark
% 60.87/61.10 %-------------------------------------------
% 60.87/61.10 % File :CSE---1.7
% 60.87/61.10 % Problem :theBenchmark
% 60.87/61.10 % Transform :cnf
% 60.87/61.10 % Format :tptp:raw
% 60.87/61.10 % Command :java -jar mcs_scs.jar %d %s
% 60.87/61.10
% 60.87/61.10 % Result :Theorem 60.360000s
% 60.87/61.10 % Output :CNFRefutation 60.360000s
% 60.87/61.10 %-------------------------------------------
% 60.96/61.11 %--------------------------------------------------------------------------
% 60.96/61.11 % File : CAT001-3 : TPTP v8.2.0. Released v1.0.0.
% 60.96/61.11 % Domain : Category Theory
% 60.96/61.11 % Problem : XY monomorphism => Y monomorphism
% 60.96/61.11 % Version : [Sco79] axioms : Reduced > Complete.
% 60.96/61.11 % English : If xy is a monomorphism, then y is a monomorphism.
% 60.96/61.11
% 60.96/61.11 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 60.96/61.11 % Source : [ANL]
% 60.96/61.11 % Names : p1.ver3.in [ANL]
% 60.96/61.11
% 60.96/61.11 % Status : Unsatisfiable
% 60.96/61.11 % Rating : 0.15 v8.2.0, 0.14 v8.1.0, 0.05 v7.5.0, 0.16 v7.4.0, 0.18 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.27 v6.4.0, 0.20 v6.3.0, 0.09 v6.2.0, 0.30 v6.1.0, 0.36 v6.0.0, 0.30 v5.5.0, 0.35 v5.4.0, 0.30 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0, 0.23 v4.0.1, 0.36 v4.0.0, 0.18 v3.7.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.25 v2.4.0, 0.11 v2.2.1, 0.22 v2.2.0, 0.11 v2.1.0, 0.33 v2.0.0
% 60.96/61.11 % Syntax : Number of clauses : 22 ( 7 unt; 2 nHn; 17 RR)
% 60.96/61.11 % Number of literals : 44 ( 20 equ; 20 neg)
% 60.96/61.11 % Maximal clause size : 4 ( 2 avg)
% 60.96/61.11 % Maximal term depth : 3 ( 1 avg)
% 60.96/61.11 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 60.96/61.11 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 60.96/61.11 % Number of variables : 34 ( 4 sgn)
% 60.96/61.11 % SPC : CNF_UNS_RFO_SEQ_NHN
% 60.96/61.11
% 60.96/61.11 % Comments : Axioms simplified by Art Quaife.
% 60.96/61.11 %--------------------------------------------------------------------------
% 60.96/61.11 %----Include Scott's axioms for category theory
% 60.96/61.11 include('Axioms/CAT003-0.ax').
% 60.96/61.11 %--------------------------------------------------------------------------
% 60.96/61.11 cnf(assume_ab_exists,hypothesis,
% 60.96/61.11 there_exists(compose(a,b)) ).
% 60.96/61.11
% 60.96/61.11 cnf(monomorphism,hypothesis,
% 60.96/61.11 ( compose(compose(a,b),X) != Y
% 60.96/61.11 | compose(compose(a,b),Z) != Y
% 60.96/61.11 | X = Z ) ).
% 60.96/61.11
% 60.96/61.11 cnf(assume_bh_exists,hypothesis,
% 60.96/61.11 there_exists(compose(b,h)) ).
% 60.96/61.11
% 60.96/61.11 cnf(bh_equals_bg,hypothesis,
% 60.96/61.11 compose(b,h) = compose(b,g) ).
% 60.96/61.11
% 60.96/61.11 cnf(prove_h_equals_g,negated_conjecture,
% 60.96/61.11 h != g ).
% 60.96/61.11
% 60.96/61.11 %--------------------------------------------------------------------------
% 60.96/61.11 %-------------------------------------------
% 60.96/61.11 % Proof found
% 60.96/61.11 % SZS status Theorem for theBenchmark
% 60.96/61.11 % SZS output start Proof
% 60.96/61.11 %ClaNum:33(EqnAxiom:12)
% 60.96/61.11 %VarNum:64(SingletonVarNum:30)
% 60.96/61.11 %MaxLitNum:3
% 60.96/61.11 %MaxfuncDepth:2
% 60.96/61.12 %SharedTerms:11
% 60.96/61.12 %goalClause: 19
% 60.96/61.12 %singleGoalClaCount:1
% 60.96/61.12 [19]~E(a6,a8)
% 60.96/61.12 [15]E(f2(a4,a6),f2(a4,a8))
% 60.96/61.12 [16]P1(f2(a5,a4))
% 60.96/61.12 [17]P1(f2(a4,a8))
% 60.96/61.12 [13]E(f2(x131,f1(x131)),x131)
% 60.96/61.12 [14]E(f2(f3(x141),x141),x141)
% 60.96/61.12 [18]E(f2(f2(x181,x182),x183),f2(x181,f2(x182,x183)))
% 60.96/61.12 [20]P1(x201)+~P1(f1(x201))
% 60.96/61.12 [21]P1(x211)+~P1(f3(x211))
% 60.96/61.12 [22]~P2(x221,x222)+E(x221,x222)
% 60.96/61.12 [24]P1(x241)+~P2(x242,x241)
% 60.96/61.12 [25]P1(x251)+~P2(x251,x252)
% 60.96/61.12 [27]E(x271,x272)+P1(f7(x271,x272))
% 60.96/61.12 [29]E(f3(x291),f1(x292))+~P1(f2(x292,x291))
% 60.96/61.12 [30]P1(f1(x301))+~P1(f2(x301,x302))
% 60.96/61.12 [31]P1(f3(x311))+~P1(f2(x311,x312))
% 60.96/61.12 [23]~E(x231,x232)+~P1(x231)+P2(x231,x232)
% 60.96/61.12 [28]E(x281,x282)+E(f7(x281,x282),x282)+E(f7(x281,x282),x281)
% 60.96/61.12 [32]~E(f3(x322),f1(x321))+~P1(f1(x321))+P1(f2(x321,x322))
% 60.96/61.12 [33]E(x331,x332)+~E(f2(f2(a5,a4),x331),x333)+~E(f2(f2(a5,a4),x332),x333)
% 60.96/61.12 %EqnAxiom
% 60.96/61.12 [1]E(x11,x11)
% 60.96/61.12 [2]E(x22,x21)+~E(x21,x22)
% 60.96/61.12 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.96/61.12 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 60.96/61.12 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 60.96/61.12 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 60.96/61.12 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 60.96/61.12 [8]~E(x81,x82)+E(f7(x81,x83),f7(x82,x83))
% 60.96/61.12 [9]~E(x91,x92)+E(f7(x93,x91),f7(x93,x92))
% 60.96/61.12 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 60.96/61.12 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 60.96/61.12 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 60.96/61.12
% 60.96/61.12 %-------------------------------------------
% 60.96/61.13 cnf(34,plain,
% 60.96/61.13 (~P1(x341)+P2(x341,x341)),
% 60.96/61.13 inference(equality_inference,[],[23])).
% 60.96/61.13 cnf(35,plain,
% 60.96/61.13 (~P2(a6,a8)),
% 60.96/61.13 inference(scs_inference,[],[19,22])).
% 60.96/61.13 cnf(37,plain,
% 60.96/61.13 (E(f2(a4,a8),f2(a4,a6))),
% 60.96/61.13 inference(scs_inference,[],[19,15,22,2])).
% 60.96/61.13 cnf(38,plain,
% 60.96/61.13 (E(f3(a8),f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[19,15,17,22,2,29])).
% 60.96/61.13 cnf(40,plain,
% 60.96/61.13 (P2(f2(a4,a8),f2(a4,a6))),
% 60.96/61.13 inference(scs_inference,[],[19,15,17,22,2,29,23])).
% 60.96/61.13 cnf(42,plain,
% 60.96/61.13 (E(f2(f2(a4,a6),f1(f2(a4,a6))),f2(a4,a8))),
% 60.96/61.13 inference(scs_inference,[],[19,15,13,17,22,2,29,23,3])).
% 60.96/61.13 cnf(44,plain,
% 60.96/61.13 (P1(f2(a4,a6))),
% 60.96/61.13 inference(scs_inference,[],[19,15,13,17,22,2,29,23,3,10])).
% 60.96/61.13 cnf(45,plain,
% 60.96/61.13 (P2(f2(a4,a6),f2(a4,a6))),
% 60.96/61.13 inference(scs_inference,[],[19,15,13,17,22,2,29,23,3,10,11])).
% 60.96/61.13 cnf(46,plain,
% 60.96/61.13 (P2(f2(a4,a8),f2(a4,a8))),
% 60.96/61.13 inference(scs_inference,[],[19,15,13,17,22,2,29,23,3,10,11,12])).
% 60.96/61.13 cnf(47,plain,
% 60.96/61.13 (E(f3(a6),f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[44,29])).
% 60.96/61.13 cnf(49,plain,
% 60.96/61.13 (E(f2(a4,a8),f2(f2(a4,a6),f1(f2(a4,a6))))),
% 60.96/61.13 inference(scs_inference,[],[42,44,29,2])).
% 60.96/61.13 cnf(50,plain,
% 60.96/61.13 (P2(f2(a4,a6),f2(a4,a8))),
% 60.96/61.13 inference(scs_inference,[],[42,44,15,29,2,23])).
% 60.96/61.13 cnf(52,plain,
% 60.96/61.13 (P1(f2(f2(a4,a6),f1(f2(a4,a6))))),
% 60.96/61.13 inference(scs_inference,[],[42,44,15,17,29,2,23,10])).
% 60.96/61.13 cnf(53,plain,
% 60.96/61.13 (E(f2(f3(f3(a8)),f3(a8)),f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[42,38,44,14,15,17,29,2,23,10,3])).
% 60.96/61.13 cnf(55,plain,
% 60.96/61.13 (E(f3(a4),f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[16,29])).
% 60.96/61.13 cnf(57,plain,
% 60.96/61.13 (E(f1(a4),f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.13 inference(scs_inference,[],[53,16,29,2])).
% 60.96/61.13 cnf(60,plain,
% 60.96/61.13 (P2(f2(a4,a6),f2(f2(a4,a6),f1(f2(a4,a6))))),
% 60.96/61.13 inference(scs_inference,[],[53,49,42,50,52,16,29,2,23,12])).
% 60.96/61.13 cnf(62,plain,
% 60.96/61.13 (E(f2(f3(a6),f1(f3(a6))),f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[53,49,42,40,50,52,47,16,13,29,2,23,12,11,3])).
% 60.96/61.13 cnf(64,plain,
% 60.96/61.13 (~P1(f2(f3(f3(a8)),f3(a8)))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[53,49,42,40,50,52,47,16,13,29,2,23,12,11,3,10])).
% 60.96/61.13 cnf(65,plain,
% 60.96/61.13 (~P2(x651,f2(f3(f3(a8)),f3(a8)))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[53,49,42,40,50,52,47,16,13,29,2,23,12,11,3,10,24])).
% 60.96/61.13 cnf(67,plain,
% 60.96/61.13 (~P2(f2(f3(f3(a8)),f3(a8)),x671)+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[53,49,42,40,50,52,47,16,13,29,2,23,12,11,3,10,24,25])).
% 60.96/61.13 cnf(70,plain,
% 60.96/61.13 (E(f1(a4),f2(f3(a6),f1(f3(a6))))),
% 60.96/61.13 inference(scs_inference,[],[62,2])).
% 60.96/61.13 cnf(72,plain,
% 60.96/61.13 (E(f2(f3(f3(a4)),f3(a4)),f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[62,60,55,14,15,2,11,3])).
% 60.96/61.13 cnf(74,plain,
% 60.96/61.13 (P2(f2(a5,a4),x741)+~E(f2(a5,a4),x741)),
% 60.96/61.13 inference(scs_inference,[],[62,60,55,14,16,15,2,11,3,23])).
% 60.96/61.13 cnf(78,plain,
% 60.96/61.13 (P2(f2(a5,a4),f2(a5,a4))),
% 60.96/61.13 inference(equality_inference,[],[74])).
% 60.96/61.13 cnf(79,plain,
% 60.96/61.13 (E(f1(a5),f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.13 inference(scs_inference,[],[72,2])).
% 60.96/61.13 cnf(80,plain,
% 60.96/61.13 (~E(a6,f2(a8,f1(a8)))),
% 60.96/61.13 inference(scs_inference,[],[19,72,13,2,3])).
% 60.96/61.13 cnf(82,plain,
% 60.96/61.13 (~P2(a6,f2(a8,f1(a8)))),
% 60.96/61.13 inference(scs_inference,[],[19,72,13,2,3,22])).
% 60.96/61.13 cnf(84,plain,
% 60.96/61.13 (~P1(f2(f3(f3(a4)),f3(a4)))+P1(f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[19,72,13,2,3,22,10])).
% 60.96/61.13 cnf(89,plain,
% 60.96/61.13 (~E(f2(a4,a6),f2(f3(f3(a4)),f3(a4)))+P1(f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[19,72,44,13,2,3,22,10,24,25,32,23])).
% 60.96/61.13 cnf(91,plain,
% 60.96/61.13 (~E(f2(a4,a8),f2(f3(f3(a4)),f3(a4)))+P1(f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[19,72,50,44,13,2,3,22,10,24,25,32,23,12])).
% 60.96/61.13 cnf(92,plain,
% 60.96/61.13 (~E(f2(a5,a4),f2(f3(f3(a4)),f3(a4)))+P1(f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[19,72,50,78,44,13,2,3,22,10,24,25,32,23,12,11])).
% 60.96/61.13 cnf(93,plain,
% 60.96/61.13 (E(x931,f2(x931,f1(x931)))),
% 60.96/61.13 inference(scs_inference,[],[13,2])).
% 60.96/61.13 cnf(94,plain,
% 60.96/61.13 (P2(f2(a5,a4),f2(f2(a5,a4),f1(f2(a5,a4))))),
% 60.96/61.13 inference(scs_inference,[],[16,13,2,23])).
% 60.96/61.13 cnf(96,plain,
% 60.96/61.13 (P1(f2(f2(a5,a4),f1(f2(a5,a4))))),
% 60.96/61.13 inference(scs_inference,[],[16,13,2,23,10])).
% 60.96/61.13 cnf(98,plain,
% 60.96/61.13 (E(f2(f3(f3(a6)),f3(a6)),f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[78,16,13,47,14,2,23,10,11,3])).
% 60.96/61.13 cnf(100,plain,
% 60.96/61.13 (E(f1(a4),f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.13 inference(scs_inference,[],[98,2])).
% 60.96/61.13 cnf(101,plain,
% 60.96/61.13 (E(f2(f3(a8),f1(f3(a8))),f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[98,13,38,2,3])).
% 60.96/61.13 cnf(103,plain,
% 60.96/61.13 (~P1(f2(f3(f3(a6)),f3(a6)))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[98,13,38,2,3,10])).
% 60.96/61.13 cnf(104,plain,
% 60.96/61.13 (~P2(f2(f3(f3(a6)),f3(a6)),x1041)+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[98,13,38,2,3,10,25])).
% 60.96/61.13 cnf(106,plain,
% 60.96/61.13 (~P2(x1061,f2(f3(f3(a6)),f3(a6)))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[98,13,38,2,3,10,25,24])).
% 60.96/61.13 cnf(108,plain,
% 60.96/61.13 (~E(f2(a5,a4),f2(f3(f3(a6)),f3(a6)))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[98,16,13,38,2,3,10,25,24,32,23])).
% 60.96/61.13 cnf(110,plain,
% 60.96/61.13 (~E(f2(a4,a8),f2(f3(f3(a6)),f3(a6)))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[98,40,16,13,38,2,3,10,25,24,32,23,11])).
% 60.96/61.13 cnf(111,plain,
% 60.96/61.13 (E(f1(a4),f2(f3(a8),f1(f3(a8))))),
% 60.96/61.13 inference(scs_inference,[],[101,2])).
% 60.96/61.13 cnf(113,plain,
% 60.96/61.13 (E(x1131,f2(x1131,f1(x1131)))),
% 60.96/61.13 inference(rename_variables,[],[93])).
% 60.96/61.13 cnf(116,plain,
% 60.96/61.13 (E(x1161,f2(x1161,f1(x1161)))),
% 60.96/61.13 inference(rename_variables,[],[93])).
% 60.96/61.13 cnf(119,plain,
% 60.96/61.13 (E(f2(f3(a4),f1(f3(a4))),f1(a5))),
% 60.96/61.13 inference(scs_inference,[],[93,113,116,101,50,40,17,13,55,2,23,12,11,3])).
% 60.96/61.13 cnf(121,plain,
% 60.96/61.13 (~P1(f1(a5))+P1(f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.13 inference(scs_inference,[],[93,113,116,79,101,50,40,17,13,55,2,23,12,11,3,10])).
% 60.96/61.13 cnf(124,plain,
% 60.96/61.13 (P1(f2(f3(f3(a4)),f3(a4)))+~P1(f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.13 inference(scs_inference,[],[93,113,116,79,101,50,40,16,17,13,55,2,23,12,11,3,10,89,30,84])).
% 60.96/61.13 cnf(127,plain,
% 60.96/61.13 (~P2(f1(a5),x1271)+P1(f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.13 inference(scs_inference,[],[93,113,116,79,101,50,40,16,17,13,55,2,23,12,11,3,10,89,30,84,91,92,25])).
% 60.96/61.13 cnf(132,plain,
% 60.96/61.13 (E(f1(a5),f2(f3(a4),f1(f3(a4))))),
% 60.96/61.13 inference(scs_inference,[],[119,2])).
% 60.96/61.13 cnf(133,plain,
% 60.96/61.13 (~E(a6,f2(f3(a8),a8))),
% 60.96/61.13 inference(scs_inference,[],[19,119,14,2,3])).
% 60.96/61.13 cnf(135,plain,
% 60.96/61.13 (~P2(a6,f2(f3(a8),a8))),
% 60.96/61.13 inference(scs_inference,[],[19,119,14,2,3,22])).
% 60.96/61.13 cnf(151,plain,
% 60.96/61.13 (~E(f2(a5,a4),f2(f3(f3(a8)),f3(a8)))+P1(f2(f3(a6),f1(f3(a6))))),
% 60.96/61.13 inference(scs_inference,[],[19,70,119,16,44,14,2,3,22,10,108,64,65,67,103,104,106,110,30,25,24,32,23])).
% 60.96/61.13 cnf(155,plain,
% 60.96/61.13 (E(f2(x1551,f2(x1552,x1553)),f2(f2(x1551,x1552),x1553))),
% 60.96/61.13 inference(scs_inference,[],[18,2])).
% 60.96/61.13 cnf(158,plain,
% 60.96/61.13 (~P1(f1(a4))+P1(f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.13 inference(scs_inference,[],[93,100,46,18,2,11,10])).
% 60.96/61.13 cnf(161,plain,
% 60.96/61.13 (P1(f2(f3(f3(a6)),f3(a6)))+~P1(f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.13 inference(scs_inference,[],[93,100,46,18,2,11,10,67,65,64])).
% 60.96/61.13 cnf(165,plain,
% 60.96/61.13 (P1(f2(f3(f3(a6)),f3(a6)))+~P1(f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.13 inference(scs_inference,[],[93,100,46,44,18,2,11,10,67,65,64,110,108,30,103])).
% 60.96/61.13 cnf(174,plain,
% 60.96/61.13 (E(f1(a4),f3(a6))),
% 60.96/61.13 inference(scs_inference,[],[47,2])).
% 60.96/61.13 cnf(175,plain,
% 60.96/61.13 (E(f2(f3(a8),f1(f3(a8))),f3(a6))),
% 60.96/61.13 inference(scs_inference,[],[101,47,2,3])).
% 60.96/61.13 cnf(176,plain,
% 60.96/61.13 (~P1(f2(f3(a8),f1(f3(a8))))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[101,47,2,3,10])).
% 60.96/61.13 cnf(177,plain,
% 60.96/61.13 (~P2(f2(f3(a8),f1(f3(a8))),x1771)+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[101,47,2,3,10,25])).
% 60.96/61.13 cnf(179,plain,
% 60.96/61.13 (~P2(x1791,f2(f3(a8),f1(f3(a8))))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[101,47,2,3,10,25,24])).
% 60.96/61.13 cnf(181,plain,
% 60.96/61.13 (~E(f2(a5,a4),f2(f3(a8),f1(f3(a8))))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[101,16,47,2,3,10,25,24,32,23])).
% 60.96/61.13 cnf(183,plain,
% 60.96/61.13 (~E(f2(a4,a6),f2(f3(a8),f1(f3(a8))))+P1(f1(a4))),
% 60.96/61.13 inference(scs_inference,[],[101,50,16,47,2,3,10,25,24,32,23,11])).
% 60.96/61.13 cnf(185,plain,
% 60.96/61.13 (E(f3(a8),f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[93,175,2,3])).
% 60.96/61.14 cnf(187,plain,
% 60.96/61.14 (~P1(f2(f3(a4),f1(f3(a4))))+P1(f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[93,119,175,2,3,10])).
% 60.96/61.14 cnf(195,plain,
% 60.96/61.14 (E(f3(a6),f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[185,2])).
% 60.96/61.14 cnf(196,plain,
% 60.96/61.14 (E(f1(a4),f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[174,185,2,3])).
% 60.96/61.14 cnf(197,plain,
% 60.96/61.14 (~P1(f2(f3(a6),f1(f3(a6))))+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[62,174,185,2,3,10])).
% 60.96/61.14 cnf(198,plain,
% 60.96/61.14 (P1(f1(a4))+~E(f2(a5,a4),f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.14 inference(scs_inference,[],[62,174,185,2,3,10,151])).
% 60.96/61.14 cnf(199,plain,
% 60.96/61.14 (~P2(f2(f3(a6),f1(f3(a6))),x1991)+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[62,174,185,2,3,10,151,25])).
% 60.96/61.14 cnf(201,plain,
% 60.96/61.14 (~P2(x2011,f2(f3(a6),f1(f3(a6))))+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[62,174,185,2,3,10,151,25,24])).
% 60.96/61.14 cnf(203,plain,
% 60.96/61.14 (~E(f2(a5,a4),f2(f3(a6),f1(f3(a6))))+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[62,174,185,16,2,3,10,151,25,24,32,23])).
% 60.96/61.14 cnf(205,plain,
% 60.96/61.14 (~E(f2(a4,a6),f2(f3(a6),f1(f3(a6))))+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[62,174,185,50,16,2,3,10,151,25,24,32,23,11])).
% 60.96/61.14 cnf(206,plain,
% 60.96/61.14 (E(f1(a5),f3(a4))),
% 60.96/61.14 inference(scs_inference,[],[55,2])).
% 60.96/61.14 cnf(207,plain,
% 60.96/61.14 (E(f2(f3(a6),f1(f3(a6))),f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[62,196,55,2,3])).
% 60.96/61.14 cnf(211,plain,
% 60.96/61.14 (E(f3(a8),f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[207,2])).
% 60.96/61.14 cnf(212,plain,
% 60.96/61.14 (~P1(f1(a4))+P1(f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[111,207,2,10])).
% 60.96/61.14 cnf(241,plain,
% 60.96/61.14 (E(x2411,f2(f3(x2411),x2411))),
% 60.96/61.14 inference(scs_inference,[],[14,2])).
% 60.96/61.14 cnf(242,plain,
% 60.96/61.14 (P1(f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 60.96/61.14 inference(scs_inference,[],[16,14,2,10])).
% 60.96/61.14 cnf(258,plain,
% 60.96/61.14 (~P1(f1(a5))+P1(f3(a4))),
% 60.96/61.14 inference(scs_inference,[],[206,10])).
% 60.96/61.14 cnf(276,plain,
% 60.96/61.14 (~P1(f1(a4))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[196,10])).
% 60.96/61.14 cnf(277,plain,
% 60.96/61.14 (P1(f3(a8))+~P2(f2(f3(a8),f1(f3(a8))),x2771)),
% 60.96/61.14 inference(scs_inference,[],[196,10,177])).
% 60.96/61.14 cnf(278,plain,
% 60.96/61.14 (P1(f3(a8))+~P2(x2781,f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179])).
% 60.96/61.14 cnf(280,plain,
% 60.96/61.14 (P1(f3(a8))+~E(f2(a5,a4),f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179,198,181])).
% 60.96/61.14 cnf(282,plain,
% 60.96/61.14 (P1(f3(a8))+~E(f2(a4,a6),f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179,198,181,106,205])).
% 60.96/61.14 cnf(283,plain,
% 60.96/61.14 (P1(f3(a8))+~P1(f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179,198,181,106,205,176])).
% 60.96/61.14 cnf(285,plain,
% 60.96/61.14 (P1(f3(a8))+~P1(f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179,198,181,106,205,176,201,197])).
% 60.96/61.14 cnf(286,plain,
% 60.96/61.14 (P1(f3(a8))+~E(f2(a5,a4),f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179,198,181,106,205,176,201,197,203])).
% 60.96/61.14 cnf(289,plain,
% 60.96/61.14 (P1(f3(a8))+~E(f2(a4,a6),f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[196,10,177,179,198,181,106,205,176,201,197,203,199,67,183])).
% 60.96/61.14 cnf(303,plain,
% 60.96/61.14 (~E(f2(a4,a8),f2(f3(a8),f1(f3(a8))))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[196,44,17,10,177,179,198,181,106,205,176,201,197,203,199,67,183,108,104,22,65,64,30,110,103,25,24,32,23])).
% 60.96/61.14 cnf(306,plain,
% 60.96/61.14 (~E(f2(a5,a4),f1(a4))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[100,196,45,44,17,10,177,179,198,181,106,205,176,201,197,203,199,67,183,108,104,22,65,64,30,110,103,25,24,32,23,12,3])).
% 60.96/61.14 cnf(307,plain,
% 60.96/61.14 (~P1(f1(a4))+P1(f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[174,10])).
% 60.96/61.14 cnf(330,plain,
% 60.96/61.14 (~P2(f1(a4),x3301)+P1(f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[174,44,10,198,179,106,177,203,181,199,176,104,201,205,67,197,108,22,65,183,64,30,110,103,25])).
% 60.96/61.14 cnf(339,plain,
% 60.96/61.14 (P1(f3(a8))+~P1(f2(a6,x3391))),
% 60.96/61.14 inference(scs_inference,[],[195,10,31])).
% 60.96/61.14 cnf(341,plain,
% 60.96/61.14 (~P2(f3(a6),x3411)+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[195,10,31,25])).
% 60.96/61.14 cnf(343,plain,
% 60.96/61.14 (~P2(x3431,f3(a6))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[195,10,31,25,24])).
% 60.96/61.14 cnf(345,plain,
% 60.96/61.14 (~E(f2(a5,a4),f3(a6))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[195,16,10,31,25,24,32,23])).
% 60.96/61.14 cnf(347,plain,
% 60.96/61.14 (~E(f2(f2(a5,a4),f1(f2(a5,a4))),f3(a6))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[195,94,16,10,31,25,24,32,23,12])).
% 60.96/61.14 cnf(348,plain,
% 60.96/61.14 (~E(f2(a4,a6),f3(a6))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[195,50,94,16,10,31,25,24,32,23,12,11])).
% 60.96/61.14 cnf(349,plain,
% 60.96/61.14 (~E(f2(a5,a4),f3(a8))+P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[195,185,50,94,16,10,31,25,24,32,23,12,11,3])).
% 60.96/61.14 cnf(350,plain,
% 60.96/61.14 (~P1(f3(a8))+P1(f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[185,10])).
% 60.96/61.14 cnf(367,plain,
% 60.96/61.14 (~P1(f3(a8))+P1(f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[211,10])).
% 60.96/61.14 cnf(378,plain,
% 60.96/61.14 (P1(f2(f3(a6),f1(f3(a6))))+~P1(f2(a6,x3781))),
% 60.96/61.14 inference(scs_inference,[],[211,10,280,286,303,306,277,278,282,283,285,289,339])).
% 60.96/61.14 cnf(385,plain,
% 60.96/61.14 (P1(f2(f3(a6),f1(f3(a6))))+~P1(f2(a8,x3851))),
% 60.96/61.14 inference(scs_inference,[],[211,10,280,286,303,306,277,278,282,283,285,289,339,341,343,347,349,345,348,31])).
% 60.96/61.14 cnf(394,plain,
% 60.96/61.14 (~P1(f1(a5))+P1(f2(f3(a4),f1(f3(a4))))),
% 60.96/61.14 inference(scs_inference,[],[132,10])).
% 60.96/61.14 cnf(410,plain,
% 60.96/61.14 (~P1(f1(a4))+P1(f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.14 inference(scs_inference,[],[57,10])).
% 60.96/61.14 cnf(421,plain,
% 60.96/61.14 (P1(f2(f3(f3(a8)),f3(a8)))+~P1(f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[57,10,179,106,198,203,199,201,177,181,104,205,176])).
% 60.96/61.14 cnf(424,plain,
% 60.96/61.14 (P1(f2(f3(f3(a8)),f3(a8)))+~P1(f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[57,10,179,106,198,203,199,201,177,181,104,205,176,108,183,197])).
% 60.96/61.14 cnf(438,plain,
% 60.96/61.14 (~P1(f3(a8))+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[38,10])).
% 60.96/61.14 cnf(462,plain,
% 60.96/61.14 (~P1(f3(a6))+P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[47,10])).
% 60.96/61.14 cnf(465,plain,
% 60.96/61.14 (~P1(f3(a4))+P1(f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[55,10])).
% 60.96/61.14 cnf(476,plain,
% 60.96/61.14 (P2(f7(a6,a8),f7(a6,a8))),
% 60.96/61.14 inference(scs_inference,[],[19,34,27])).
% 60.96/61.14 cnf(478,plain,
% 60.96/61.14 (E(x4781,f2(x4781,f1(x4781)))),
% 60.96/61.14 inference(rename_variables,[],[93])).
% 60.96/61.14 cnf(479,plain,
% 60.96/61.14 (P2(f2(f7(a6,a8),f1(f7(a6,a8))),f7(a6,a8))),
% 60.96/61.14 inference(scs_inference,[],[93,478,476,12,11])).
% 60.96/61.14 cnf(483,plain,
% 60.96/61.14 (E(f3(a4),f2(f1(a5),f1(f1(a5))))),
% 60.96/61.14 inference(scs_inference,[],[13,93,478,206,476,12,11,3,2])).
% 60.96/61.14 cnf(496,plain,
% 60.96/61.14 (~P1(f3(a4))+P1(f2(f1(a5),f1(f1(a5))))),
% 60.96/61.14 inference(scs_inference,[],[13,196,483,3,2,10])).
% 60.96/61.14 cnf(598,plain,
% 60.96/61.14 (P1(f3(a4))),
% 60.96/61.14 inference(scs_inference,[],[16,258,30])).
% 60.96/61.14 cnf(599,plain,
% 60.96/61.14 (P1(f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[598,465])).
% 60.96/61.14 cnf(600,plain,
% 60.96/61.14 (P1(f2(f1(a5),f1(f1(a5))))),
% 60.96/61.14 inference(scs_inference,[],[598,496])).
% 60.96/61.14 cnf(601,plain,
% 60.96/61.14 (P1(a4)),
% 60.96/61.14 inference(scs_inference,[],[598,21])).
% 60.96/61.14 cnf(604,plain,
% 60.96/61.14 (E(f2(f3(x6041),x6041),x6041)),
% 60.96/61.14 inference(rename_variables,[],[14])).
% 60.96/61.14 cnf(609,plain,
% 60.96/61.14 (P1(f2(f3(f1(a5)),f1(a5)))),
% 60.96/61.14 inference(scs_inference,[],[14,604,206,242,598,21,23,3,2,10])).
% 60.96/61.14 cnf(610,plain,
% 60.96/61.14 (P1(f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.14 inference(scs_inference,[],[599,121])).
% 60.96/61.14 cnf(611,plain,
% 60.96/61.14 (P1(f2(f3(a4),f1(f3(a4))))),
% 60.96/61.14 inference(scs_inference,[],[599,394])).
% 60.96/61.14 cnf(613,plain,
% 60.96/61.14 (P1(f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[44,276,30])).
% 60.96/61.14 cnf(614,plain,
% 60.96/61.14 (P1(f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[610,84])).
% 60.96/61.14 cnf(615,plain,
% 60.96/61.14 (P1(f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.14 inference(scs_inference,[],[610,124])).
% 60.96/61.14 cnf(616,plain,
% 60.96/61.14 (P1(f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[611,187])).
% 60.96/61.14 cnf(617,plain,
% 60.96/61.14 (P1(f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[613,350])).
% 60.96/61.14 cnf(618,plain,
% 60.96/61.14 (P1(f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[613,367])).
% 60.96/61.14 cnf(621,plain,
% 60.96/61.14 (P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[613,438])).
% 60.96/61.14 cnf(625,plain,
% 60.96/61.14 (P1(a5)),
% 60.96/61.14 inference(scs_inference,[],[599,20])).
% 60.96/61.14 cnf(627,plain,
% 60.96/61.14 (P1(a8)),
% 60.96/61.14 inference(scs_inference,[],[599,613,20,21])).
% 60.96/61.14 cnf(629,plain,
% 60.96/61.14 (P2(f2(f3(a4),f1(f3(a4))),f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[119,611,599,613,20,21,23])).
% 60.96/61.14 cnf(631,plain,
% 60.96/61.14 (P2(f1(a5),f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[119,611,599,613,20,21,23,11])).
% 60.96/61.14 cnf(632,plain,
% 60.96/61.14 (E(f2(f3(f1(a4)),f1(a4)),f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[14,119,196,611,599,613,20,21,23,11,3])).
% 60.96/61.14 cnf(635,plain,
% 60.96/61.14 (P2(f1(a5),f2(f1(a5),f1(f1(a5))))),
% 60.96/61.14 inference(scs_inference,[],[14,119,93,196,611,599,613,20,21,23,11,3,2,12])).
% 60.96/61.14 cnf(637,plain,
% 60.96/61.14 (P1(f2(f3(f1(a4)),f1(a4)))),
% 60.96/61.14 inference(scs_inference,[],[14,119,93,196,611,599,613,20,21,23,11,3,2,12,10])).
% 60.96/61.14 cnf(638,plain,
% 60.96/61.14 (P1(f2(f3(f3(a4)),f3(a4)))),
% 60.96/61.14 inference(scs_inference,[],[635,127])).
% 60.96/61.14 cnf(641,plain,
% 60.96/61.14 (P1(f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.14 inference(scs_inference,[],[621,158])).
% 60.96/61.14 cnf(643,plain,
% 60.96/61.14 (P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[618,197])).
% 60.96/61.14 cnf(644,plain,
% 60.96/61.14 (P1(f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[621,212])).
% 60.96/61.14 cnf(647,plain,
% 60.96/61.14 (P1(f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[621,307])).
% 60.96/61.14 cnf(652,plain,
% 60.96/61.14 (P1(f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.14 inference(scs_inference,[],[621,410])).
% 60.96/61.14 cnf(653,plain,
% 60.96/61.14 (P1(f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.14 inference(scs_inference,[],[618,424])).
% 60.96/61.14 cnf(654,plain,
% 60.96/61.14 (P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[617,462])).
% 60.96/61.14 cnf(662,plain,
% 60.96/61.14 (P2(f3(a6),f3(a6))+~P2(f1(a4),x6621)),
% 60.96/61.14 inference(scs_inference,[],[330,34])).
% 60.96/61.14 cnf(667,plain,
% 60.96/61.14 (P1(f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.14 inference(scs_inference,[],[652,161])).
% 60.96/61.14 cnf(668,plain,
% 60.96/61.14 (P1(f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.14 inference(scs_inference,[],[641,165])).
% 60.96/61.14 cnf(677,plain,
% 60.96/61.14 (P1(f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.14 inference(scs_inference,[],[644,421])).
% 60.96/61.14 cnf(683,plain,
% 60.96/61.14 (P1(a6)),
% 60.96/61.14 inference(scs_inference,[],[617,21])).
% 60.96/61.14 cnf(685,plain,
% 60.96/61.14 (P2(f2(f3(a8),f1(f3(a8))),f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[101,644,617,21,23])).
% 60.96/61.14 cnf(691,plain,
% 60.96/61.14 (E(f3(a6),f2(f3(f1(a4)),f1(a4)))),
% 60.96/61.14 inference(scs_inference,[],[14,101,93,174,644,617,631,21,23,11,3,2])).
% 60.96/61.14 cnf(694,plain,
% 60.96/61.14 (P1(f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[685,177])).
% 60.96/61.14 cnf(704,plain,
% 60.96/61.14 (P2(f2(f3(f1(a5)),f1(a5)),f1(a5))),
% 60.96/61.14 inference(scs_inference,[],[14,609,23])).
% 60.96/61.14 cnf(705,plain,
% 60.96/61.14 (E(f2(f3(x7051),x7051),x7051)),
% 60.96/61.14 inference(rename_variables,[],[14])).
% 60.96/61.14 cnf(707,plain,
% 60.96/61.14 (P2(f1(a4),f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[14,101,685,609,23,11])).
% 60.96/61.14 cnf(711,plain,
% 60.96/61.14 (P2(f1(a4),f2(f1(a4),f1(f1(a4))))),
% 60.96/61.14 inference(scs_inference,[],[14,705,101,93,195,685,609,23,11,3,2,12])).
% 60.96/61.14 cnf(720,plain,
% 60.96/61.14 (P2(f3(a6),f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[711,662])).
% 60.96/61.14 cnf(730,plain,
% 60.96/61.14 (P2(f2(f3(f1(a4)),f1(a4)),f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[14,637,23])).
% 60.96/61.14 cnf(731,plain,
% 60.96/61.14 (E(f2(f3(x7311),x7311),x7311)),
% 60.96/61.14 inference(rename_variables,[],[14])).
% 60.96/61.14 cnf(733,plain,
% 60.96/61.14 (P2(f3(a6),f2(f3(a6),f1(f3(a6))))),
% 60.96/61.14 inference(scs_inference,[],[14,93,720,637,23,12])).
% 60.96/61.14 cnf(734,plain,
% 60.96/61.14 (E(x7341,f2(x7341,f1(x7341)))),
% 60.96/61.14 inference(rename_variables,[],[93])).
% 60.96/61.14 cnf(735,plain,
% 60.96/61.14 (P2(f2(f3(a6),f1(f3(a6))),f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[14,93,734,720,637,23,12,11])).
% 60.96/61.14 cnf(737,plain,
% 60.96/61.14 (E(f2(f3(f3(a8)),f3(a8)),f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[14,731,93,734,185,720,637,23,12,11,3])).
% 60.96/61.14 cnf(751,plain,
% 60.96/61.14 (E(f2(f3(x7511),x7511),x7511)),
% 60.96/61.14 inference(rename_variables,[],[14])).
% 60.96/61.14 cnf(753,plain,
% 60.96/61.14 (P2(f3(a6),f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[14,62,733,641,23,12])).
% 60.96/61.14 cnf(754,plain,
% 60.96/61.14 (P2(f1(a4),f3(a6))),
% 60.96/61.14 inference(scs_inference,[],[14,62,733,641,735,23,12,11])).
% 60.96/61.14 cnf(758,plain,
% 60.96/61.14 (P1(f2(f3(f2(a4,a8)),f2(a4,a8)))),
% 60.96/61.14 inference(scs_inference,[],[14,751,62,37,44,733,641,735,23,12,11,3,2,10])).
% 60.96/61.14 cnf(766,plain,
% 60.96/61.14 (E(f2(f3(x7661),x7661),x7661)),
% 60.96/61.14 inference(rename_variables,[],[14])).
% 60.96/61.14 cnf(769,plain,
% 60.96/61.14 (E(x7691,f2(x7691,f1(x7691)))),
% 60.96/61.14 inference(rename_variables,[],[93])).
% 60.96/61.14 cnf(775,plain,
% 60.96/61.14 (P1(f2(f3(f2(a4,a6)),f2(a4,a6)))),
% 60.96/61.14 inference(scs_inference,[],[14,766,93,769,17,15,758,707,753,23,12,11,3,2,10])).
% 60.96/61.14 cnf(777,plain,
% 60.96/61.14 (P2(f2(f3(f2(a4,a6)),f2(a4,a6)),f2(a4,a6))),
% 60.96/61.14 inference(scs_inference,[],[14,775,23])).
% 60.96/61.14 cnf(784,plain,
% 60.96/61.14 (P2(f2(f3(f3(a8)),f3(a8)),f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[14,652,23])).
% 60.96/61.14 cnf(799,plain,
% 60.96/61.14 (P2(f2(f3(f3(a4)),f3(a4)),f3(a4))),
% 60.96/61.14 inference(scs_inference,[],[14,610,23])).
% 60.96/61.14 cnf(800,plain,
% 60.96/61.14 (E(f2(f3(x8001),x8001),x8001)),
% 60.96/61.14 inference(rename_variables,[],[14])).
% 60.96/61.14 cnf(804,plain,
% 60.96/61.14 (P2(f3(a8),f2(f3(a8),f1(f3(a8))))),
% 60.96/61.14 inference(scs_inference,[],[14,800,93,784,610,23,11,12])).
% 60.96/61.14 cnf(821,plain,
% 60.96/61.14 (P2(a4,f2(a4,f1(a4)))),
% 60.96/61.14 inference(scs_inference,[],[93,601,23])).
% 60.96/61.14 cnf(824,plain,
% 60.96/61.14 (P2(f3(a8),f1(a4))),
% 60.96/61.14 inference(scs_inference,[],[101,93,804,601,23,12])).
% 60.96/61.14 cnf(825,plain,
% 60.96/61.14 (P2(f3(a4),f3(a4))),
% 60.96/61.14 inference(scs_inference,[],[14,101,93,799,804,601,23,12,11])).
% 60.96/61.14 cnf(829,plain,
% 60.96/61.14 (E(f1(x8291),f1(f2(f3(x8291),x8291)))),
% 60.96/61.14 inference(scs_inference,[],[14,4,2])).
% 60.96/61.14 cnf(831,plain,
% 60.96/61.14 (P2(a5,f2(a5,f1(a5)))),
% 60.96/61.14 inference(scs_inference,[],[93,829,625,2,23])).
% 60.96/61.14 cnf(832,plain,
% 60.96/61.14 (E(x8321,f2(x8321,f1(x8321)))),
% 60.96/61.14 inference(rename_variables,[],[93])).
% 60.96/61.14 cnf(834,plain,
% 60.96/61.14 (P2(f3(a4),f2(f3(a4),f1(f3(a4))))),
% 60.96/61.14 inference(scs_inference,[],[93,832,829,825,625,2,23,12])).
% 60.96/61.14 cnf(835,plain,
% 60.96/61.14 (E(x8351,f2(x8351,f1(x8351)))),
% 60.96/61.14 inference(rename_variables,[],[93])).
% 60.96/61.14 cnf(836,plain,
% 60.96/61.14 (P1(f1(f2(f3(a5),a5)))),
% 60.96/61.14 inference(scs_inference,[],[93,832,829,825,614,625,2,23,12,10])).
% 60.96/61.14 cnf(840,plain,
% 60.96/61.14 (P1(f2(f3(a5),a5))),
% 60.96/61.14 inference(scs_inference,[],[93,832,835,821,829,825,614,625,2,23,12,10,11,20])).
% 60.96/61.14 cnf(842,plain,
% 60.96/61.14 (E(f3(a5),f1(f3(a5)))),
% 60.96/61.14 inference(scs_inference,[],[93,832,835,821,829,825,614,625,2,23,12,10,11,20,29])).
% 60.96/61.14 cnf(844,plain,
% 60.96/61.14 (E(f2(f3(f3(a5)),f3(a5)),f1(f3(a5)))),
% 60.96/61.14 inference(scs_inference,[],[14,93,832,835,821,829,825,614,625,2,23,12,10,11,20,29,3])).
% 60.96/61.14 cnf(849,plain,
% 60.96/61.14 (E(f1(f3(a5)),f2(f3(f3(a5)),f3(a5)))),
% 60.96/61.14 inference(scs_inference,[],[844,2])).
% 60.96/61.14 cnf(850,plain,
% 60.96/61.14 (P2(f2(f3(a5),a5),a5)),
% 60.96/61.14 inference(scs_inference,[],[14,844,840,2,23])).
% 60.96/61.14 cnf(856,plain,
% 60.96/61.14 (~P1(f2(f3(f3(a5)),f3(a5)))+P1(f1(f3(a5)))),
% 60.96/61.14 inference(scs_inference,[],[14,119,93,844,831,840,834,2,23,12,11,10])).
% 60.96/61.14 cnf(862,plain,
% 60.96/61.14 (E(f1(f3(a5)),f3(a5))),
% 60.96/61.14 inference(scs_inference,[],[842,2])).
% 60.96/61.14 cnf(863,plain,
% 60.96/61.14 (P2(f1(a4),f3(a8))),
% 60.96/61.14 inference(scs_inference,[],[196,842,621,2,23])).
% 60.96/61.14 cnf(868,plain,
% 60.96/61.14 (~P1(f1(f3(a5)))+P1(f2(f3(f3(a5)),f3(a5)))),
% 60.96/61.14 inference(scs_inference,[],[14,196,849,730,850,842,621,2,23,12,11,10])).
% 60.96/61.14 cnf(869,plain,
% 60.96/61.14 (P1(f2(f3(f3(a5)),f3(a5)))+~P1(f2(f3(f3(a5)),f3(a5)))),
% 60.96/61.14 inference(scs_inference,[],[14,196,849,730,850,842,621,2,23,12,11,10,856])).
% 60.96/61.14 cnf(876,plain,
% 60.96/61.14 (P2(a8,f2(a8,f1(a8)))),
% 60.96/61.14 inference(scs_inference,[],[93,627,23])).
% 60.96/61.14 cnf(903,plain,
% 60.96/61.14 (P2(f1(a5),f3(a4))),
% 60.96/61.14 inference(scs_inference,[],[206,616,23])).
% 60.96/61.14 cnf(906,plain,
% 60.96/61.14 (E(x9061,f2(f3(x9061),x9061))),
% 60.96/61.14 inference(rename_variables,[],[241])).
% 60.96/61.14 cnf(907,plain,
% 60.96/61.14 (P2(f2(f3(f7(a6,a8)),f7(a6,a8)),f7(a6,a8))),
% 60.96/61.14 inference(scs_inference,[],[206,241,906,476,616,23,12,11])).
% 60.96/61.14 cnf(909,plain,
% 60.96/61.14 (P2(f3(a6),f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.14 inference(scs_inference,[],[241,647,23])).
% 60.96/61.14 cnf(913,plain,
% 60.96/61.14 (~E(a8,a6)),
% 60.96/61.14 inference(scs_inference,[],[82,206,241,629,876,647,23,12,11])).
% 60.96/61.14 cnf(914,plain,
% 60.96/61.14 (~P2(a8,a6)),
% 60.96/61.14 inference(scs_inference,[],[82,206,241,629,876,647,23,12,11,22])).
% 60.96/61.14 cnf(923,plain,
% 60.96/61.14 (E(x9231,f2(f3(x9231),x9231))),
% 60.96/61.14 inference(rename_variables,[],[241])).
% 60.96/61.14 cnf(926,plain,
% 60.96/61.14 (E(x9261,f2(f3(x9261),x9261))),
% 60.96/61.14 inference(rename_variables,[],[241])).
% 60.96/61.14 cnf(927,plain,
% 60.96/61.14 (P2(f2(f3(a4),a4),f2(a4,f1(a4)))),
% 60.96/61.14 inference(scs_inference,[],[241,923,926,903,821,598,23,12,11])).
% 60.96/61.14 cnf(933,plain,
% 60.96/61.14 (E(x9331,f2(f3(x9331),x9331))),
% 60.96/61.14 inference(rename_variables,[],[241])).
% 60.96/61.14 cnf(936,plain,
% 60.96/61.14 (P2(f2(f3(a5),a5),f2(a5,f1(a5)))),
% 60.96/61.14 inference(scs_inference,[],[206,241,933,704,831,613,23,12,11])).
% 60.96/61.14 cnf(944,plain,
% 60.96/61.14 (P2(a4,f2(f3(a4),a4))),
% 60.96/61.14 inference(scs_inference,[],[241,601,23])).
% 60.96/61.14 cnf(949,plain,
% 60.96/61.14 (P2(a5,f2(f3(a5),a5))),
% 60.96/61.14 inference(scs_inference,[],[241,625,23])).
% 60.96/61.14 cnf(950,plain,
% 60.96/61.14 (E(x9501,f2(f3(x9501),x9501))),
% 60.96/61.14 inference(rename_variables,[],[241])).
% 60.96/61.14 cnf(954,plain,
% 60.96/61.14 (P2(f2(f3(a4),a4),f2(f3(a4),a4))),
% 60.96/61.14 inference(scs_inference,[],[14,241,950,944,625,23,12,11])).
% 60.96/61.14 cnf(959,plain,
% 60.96/61.14 (~E(f2(a8,f1(a8)),a6)),
% 60.96/61.15 inference(scs_inference,[],[914,876,12])).
% 60.96/61.15 cnf(963,plain,
% 60.96/61.15 (P2(f1(a4),f2(f3(f3(a8)),f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[241,863,12])).
% 60.96/61.15 cnf(972,plain,
% 60.96/61.15 (P2(f2(f3(f3(a6)),f3(a6)),f1(a4))),
% 60.96/61.15 inference(scs_inference,[],[14,241,954,753,12,11])).
% 60.96/61.15 cnf(990,plain,
% 60.96/61.15 (E(f3(a8),f1(f2(f3(a4),a4)))),
% 60.96/61.15 inference(scs_inference,[],[38,829,3])).
% 60.96/61.15 cnf(993,plain,
% 60.96/61.15 (P1(f1(f2(f3(a4),a4)))),
% 60.96/61.15 inference(scs_inference,[],[38,613,829,3,2,10])).
% 60.96/61.15 cnf(996,plain,
% 60.96/61.15 (E(f3(a4),f1(f3(a4)))),
% 60.96/61.15 inference(scs_inference,[],[38,613,829,3,2,10,20,29])).
% 60.96/61.15 cnf(999,plain,
% 60.96/61.15 (P1(f1(f3(a4)))),
% 60.96/61.15 inference(scs_inference,[],[598,996,2,10])).
% 60.96/61.15 cnf(1000,plain,
% 60.96/61.15 (E(f1(a5),f1(f3(a4)))),
% 60.96/61.15 inference(scs_inference,[],[206,598,996,2,10,3])).
% 60.96/61.15 cnf(1001,plain,
% 60.96/61.15 (E(f1(f3(a4)),f1(a5))),
% 60.96/61.15 inference(scs_inference,[],[1000,2])).
% 60.96/61.15 cnf(1002,plain,
% 60.96/61.15 (E(f3(a6),f1(f2(f3(a4),a4)))),
% 60.96/61.15 inference(scs_inference,[],[47,829,3])).
% 60.96/61.15 cnf(1007,plain,
% 60.96/61.15 (E(f3(a4),f1(f2(f3(a5),a5)))),
% 60.96/61.15 inference(scs_inference,[],[55,829,3])).
% 60.96/61.15 cnf(1016,plain,
% 60.96/61.15 (~P1(f2(a6,x10161))+P1(f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[378,30])).
% 60.96/61.15 cnf(1017,plain,
% 60.96/61.15 (P1(f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[93,683,1016,10])).
% 60.96/61.15 cnf(1018,plain,
% 60.96/61.15 (~P1(f2(a8,x10181))+P1(f3(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[385,31])).
% 60.96/61.15 cnf(1019,plain,
% 60.96/61.15 (P1(f3(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[876,1018,24])).
% 60.96/61.15 cnf(1028,plain,
% 60.96/61.15 (P2(f2(a5,f1(a5)),f2(f3(a5),a5))),
% 60.96/61.15 inference(scs_inference,[],[93,949,11])).
% 60.96/61.15 cnf(1033,plain,
% 60.96/61.15 (P2(f2(a4,f1(a4)),f2(f3(a4),a4))),
% 60.96/61.15 inference(scs_inference,[],[93,944,11])).
% 60.96/61.15 cnf(1094,plain,
% 60.96/61.15 (E(f3(f1(a4)),f1(a4))),
% 60.96/61.15 inference(scs_inference,[],[601,93,10,29])).
% 60.96/61.15 cnf(1096,plain,
% 60.96/61.15 (E(f1(a4),f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[601,93,10,29,2])).
% 60.96/61.15 cnf(1098,plain,
% 60.96/61.15 (P1(f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1096,643,10])).
% 60.96/61.15 cnf(1119,plain,
% 60.96/61.15 (E(f1(a5),f3(f1(a5)))),
% 60.96/61.15 inference(scs_inference,[],[625,93,10,29,2])).
% 60.96/61.15 cnf(1124,plain,
% 60.96/61.15 (E(f3(a8),f1(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[627,241,10,29])).
% 60.96/61.15 cnf(1127,plain,
% 60.96/61.15 (E(f1(a4),f1(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[627,196,241,10,29,2,3])).
% 60.96/61.15 cnf(1131,plain,
% 60.96/61.15 (E(f3(f1(a8)),f1(a8))),
% 60.96/61.15 inference(scs_inference,[],[627,93,1127,2,10,29])).
% 60.96/61.15 cnf(1139,plain,
% 60.96/61.15 (P1(f1(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1127,654,1131,2,10])).
% 60.96/61.15 cnf(1149,plain,
% 60.96/61.15 (E(f2(f3(f1(a4)),f1(a4)),f1(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[632,1124,3])).
% 60.96/61.15 cnf(1186,plain,
% 60.96/61.15 (P1(f2(a6,f1(a6)))),
% 60.96/61.15 inference(scs_inference,[],[683,93,10])).
% 60.96/61.15 cnf(1198,plain,
% 60.96/61.15 (P1(f2(f3(a6),a6))),
% 60.96/61.15 inference(scs_inference,[],[683,241,10])).
% 60.96/61.15 cnf(1200,plain,
% 60.96/61.15 (E(f3(a6),f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[683,241,10,29])).
% 60.96/61.15 cnf(1203,plain,
% 60.96/61.15 (E(f1(a4),f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[683,174,241,10,29,2,3])).
% 60.96/61.15 cnf(1205,plain,
% 60.96/61.15 (E(f1(f3(a6)),f1(a4))),
% 60.96/61.15 inference(scs_inference,[],[1203,2])).
% 60.96/61.15 cnf(1225,plain,
% 60.96/61.15 (E(f3(a6),f1(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[691,1149,3])).
% 60.96/61.15 cnf(1267,plain,
% 60.96/61.15 (E(f2(f3(f3(a8)),f3(a8)),f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[737,1200,3])).
% 60.96/61.15 cnf(1270,plain,
% 60.96/61.15 (E(f3(a8),f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[241,1267,3])).
% 60.96/61.15 cnf(1391,plain,
% 60.96/61.15 (~E(a8,f2(a6,f1(a6)))),
% 60.96/61.15 inference(scs_inference,[],[913,13,3])).
% 60.96/61.15 cnf(1393,plain,
% 60.96/61.15 (~P2(a8,f2(a6,f1(a6)))),
% 60.96/61.15 inference(scs_inference,[],[913,13,3,22])).
% 60.96/61.15 cnf(1396,plain,
% 60.96/61.15 (~E(a8,f2(f3(a6),a6))),
% 60.96/61.15 inference(scs_inference,[],[913,14,3])).
% 60.96/61.15 cnf(1398,plain,
% 60.96/61.15 (~E(f2(a8,f1(a8)),f2(a6,f1(a6)))),
% 60.96/61.15 inference(scs_inference,[],[913,1393,876,14,3,12])).
% 60.96/61.15 cnf(1399,plain,
% 60.96/61.15 (~P2(a8,f2(f3(a6),a6))),
% 60.96/61.15 inference(scs_inference,[],[913,1393,876,14,3,12,22])).
% 60.96/61.15 cnf(1404,plain,
% 60.96/61.15 (~E(f2(a8,f1(a8)),f2(f3(a6),a6))),
% 60.96/61.15 inference(scs_inference,[],[1399,876,1398,22,12])).
% 60.96/61.15 cnf(1406,plain,
% 60.96/61.15 (~P2(f2(a8,f1(a8)),f2(f3(a6),a6))),
% 60.96/61.15 inference(scs_inference,[],[1404,22])).
% 60.96/61.15 cnf(1430,plain,
% 60.96/61.15 (E(f3(f1(a5)),f1(f3(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1001,1119,3,2])).
% 60.96/61.15 cnf(1442,plain,
% 60.96/61.15 (P1(f1(f3(a5)))),
% 60.96/61.15 inference(scs_inference,[],[836,20,30])).
% 60.96/61.15 cnf(1443,plain,
% 60.96/61.15 (P1(f2(f3(f3(a5)),f3(a5)))),
% 60.96/61.15 inference(scs_inference,[],[1442,868])).
% 60.96/61.15 cnf(1453,plain,
% 60.96/61.15 (P2(f3(a5),f2(f3(a5),f1(f3(a5))))),
% 60.96/61.15 inference(scs_inference,[],[862,93,1442,20,23,11,12])).
% 60.96/61.15 cnf(1455,plain,
% 60.96/61.15 (P1(f2(f3(f3(a5)),f3(a5)))),
% 60.96/61.15 inference(scs_inference,[],[1443,869])).
% 60.96/61.15 cnf(1477,plain,
% 60.96/61.15 (P2(f3(f1(a4)),f3(a8))),
% 60.96/61.15 inference(scs_inference,[],[1094,196,1098,23,3,12])).
% 60.96/61.15 cnf(1482,plain,
% 60.96/61.15 (E(f3(f1(a4)),f2(f3(f3(a6)),f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[1094,100,3])).
% 60.96/61.15 cnf(1487,plain,
% 60.96/61.15 (E(f3(f1(a4)),f1(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1094,1127,3])).
% 60.96/61.15 cnf(1490,plain,
% 60.96/61.15 (E(f3(f1(a4)),f1(f3(a6)))),
% 60.96/61.15 inference(scs_inference,[],[1094,1203,3])).
% 60.96/61.15 cnf(1491,plain,
% 60.96/61.15 (E(f1(f3(a6)),f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1094,1203,3,2])).
% 60.96/61.15 cnf(1497,plain,
% 60.96/61.15 (P2(f2(f3(f1(a4)),f1(a4)),f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1096,730,694,754,23,11,12])).
% 60.96/61.15 cnf(1499,plain,
% 60.96/61.15 (P2(f3(a8),f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1096,824,963,11,12])).
% 60.96/61.15 cnf(1507,plain,
% 60.96/61.15 (P2(f2(f3(f3(a6)),f3(a6)),f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1096,972,12])).
% 60.96/61.15 cnf(1513,plain,
% 60.96/61.15 (P1(f7(a8,a6))),
% 60.96/61.15 inference(scs_inference,[],[19,2,27])).
% 60.96/61.15 cnf(1515,plain,
% 60.96/61.15 (E(x15151,f2(x15151,f1(x15151)))),
% 60.96/61.15 inference(rename_variables,[],[93])).
% 60.96/61.15 cnf(1517,plain,
% 60.96/61.15 (P1(f2(f7(a8,a6),f1(f7(a8,a6))))),
% 60.96/61.15 inference(scs_inference,[],[93,1515,1513,23,10])).
% 60.96/61.15 cnf(1520,plain,
% 60.96/61.15 (P1(f2(f3(f7(a8,a6)),f7(a8,a6)))),
% 60.96/61.15 inference(scs_inference,[],[241,1513,10])).
% 60.96/61.15 cnf(1571,plain,
% 60.96/61.15 (E(f7(f2(a4,a8),x15711),f7(f2(a4,a6),x15711))),
% 60.96/61.15 inference(scs_inference,[],[19,1198,37,34,27,4,7,5,6,8])).
% 60.96/61.15 cnf(1572,plain,
% 60.96/61.15 (E(f7(x15721,f2(a4,a8)),f7(x15721,f2(a4,a6)))),
% 60.96/61.15 inference(scs_inference,[],[19,1198,37,34,27,4,7,5,6,8,9])).
% 60.96/61.15 cnf(1579,plain,
% 60.96/61.15 (P1(f2(f3(f7(a6,a8)),f7(a6,a8)))),
% 60.96/61.15 inference(scs_inference,[],[19,907,927,1455,1520,1198,37,34,27,4,7,5,6,8,9,31,30,22,25])).
% 60.96/61.15 cnf(1583,plain,
% 60.96/61.15 (~E(f2(a6,f1(a6)),a8)),
% 60.96/61.15 inference(scs_inference,[],[19,1391,907,927,1455,1520,1453,1198,37,34,27,4,7,5,6,8,9,31,30,22,25,24,2])).
% 60.96/61.15 cnf(1584,plain,
% 60.96/61.15 (~E(f2(f2(a5,a4),a8),f2(f2(f2(a5,a4),a6),f1(a6)))),
% 60.96/61.15 inference(scs_inference,[],[19,1391,907,927,1455,1520,1453,1198,155,37,34,27,4,7,5,6,8,9,31,30,22,25,24,2,33])).
% 60.96/61.15 cnf(1587,plain,
% 60.96/61.15 (P1(f2(f2(f3(a4),a4),a8))),
% 60.96/61.15 inference(scs_inference,[],[19,1391,907,927,1455,1520,1453,1198,993,990,155,37,34,27,4,7,5,6,8,9,31,30,22,25,24,2,33,32])).
% 60.96/61.15 cnf(1591,plain,
% 60.96/61.15 (~E(f2(f3(a6),a6),a8)),
% 60.96/61.15 inference(scs_inference,[],[19,1205,1391,907,927,1455,1520,1453,1198,993,1017,990,155,37,241,34,27,4,7,5,6,8,9,31,30,22,25,24,2,33,32,23,3])).
% 60.96/61.15 cnf(1597,plain,
% 60.96/61.15 (P1(f2(f3(a4),f2(a4,a8)))),
% 60.96/61.15 inference(scs_inference,[],[19,1205,1477,1270,1499,1391,907,927,1455,1520,1453,1198,993,1017,990,155,18,37,241,34,27,4,7,5,6,8,9,31,30,22,25,24,2,33,32,23,3,11,12,28,10])).
% 60.96/61.15 cnf(1602,plain,
% 60.96/61.15 (E(f3(f3(a6)),f3(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1597,195,34,7])).
% 60.96/61.15 cnf(1603,plain,
% 60.96/61.15 (E(f2(f3(a6),x16031),f2(f3(a8),x16031))),
% 60.96/61.15 inference(scs_inference,[],[1597,195,34,7,5])).
% 60.96/61.15 cnf(1606,plain,
% 60.96/61.15 (E(f2(x16061,f3(a6)),f2(x16061,f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1396,1597,195,34,7,5,27,6])).
% 60.96/61.15 cnf(1610,plain,
% 60.96/61.15 (P1(f3(f3(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1396,1597,195,34,7,5,27,6,8,4,9,31])).
% 60.96/61.15 cnf(1616,plain,
% 60.96/61.15 (P1(f2(f7(a6,a8),f1(f7(a6,a8))))),
% 60.96/61.15 inference(scs_inference,[],[1396,1597,936,1579,479,195,34,7,5,27,6,8,4,9,31,30,22,25])).
% 60.96/61.15 cnf(1619,plain,
% 60.96/61.15 (~E(f2(f2(a5,a4),a6),f2(a5,f2(a4,a8)))),
% 60.96/61.15 inference(scs_inference,[],[19,1396,1597,936,1579,1584,479,18,195,34,7,5,27,6,8,4,9,31,30,22,25,2,33])).
% 60.96/61.15 cnf(1622,plain,
% 60.96/61.15 (P1(f2(f3(a4),f1(a5)))),
% 60.96/61.15 inference(scs_inference,[],[19,1396,1597,936,1430,1579,1584,479,999,18,195,34,7,5,27,6,8,4,9,31,30,22,25,2,33,32])).
% 60.96/61.15 cnf(1637,plain,
% 60.96/61.15 (E(f2(f3(a8),x16371),f2(f1(a4),x16371))),
% 60.96/61.15 inference(scs_inference,[],[1591,1610,38,34,27,6,8,7,5])).
% 60.96/61.15 cnf(1640,plain,
% 60.96/61.15 (P1(f3(f7(a6,a8)))),
% 60.96/61.15 inference(scs_inference,[],[1591,1610,1616,38,34,27,6,8,7,5,4,9,31])).
% 60.96/61.15 cnf(1642,plain,
% 60.96/61.15 (P1(f1(f7(a6,a8)))),
% 60.96/61.15 inference(scs_inference,[],[1591,1610,1616,38,34,27,6,8,7,5,4,9,31,30])).
% 60.96/61.15 cnf(1647,plain,
% 60.96/61.15 (P1(f2(f3(a8),a6))),
% 60.96/61.15 inference(scs_inference,[],[1591,1610,1028,1619,1616,1139,1225,38,34,27,6,8,7,5,4,9,31,30,22,2,32])).
% 60.96/61.15 cnf(1649,plain,
% 60.96/61.15 (~E(f2(f3(a8),a6),a8)),
% 60.96/61.15 inference(scs_inference,[],[1591,1610,1028,1619,1603,1616,1139,1225,38,34,27,6,8,7,5,4,9,31,30,22,2,32,3])).
% 60.96/61.15 cnf(1650,plain,
% 60.96/61.15 (E(f2(f3(a6),x16501),f2(f3(a8),x16501))),
% 60.96/61.15 inference(rename_variables,[],[1603])).
% 60.96/61.15 cnf(1651,plain,
% 60.96/61.15 (~P2(f2(a6,f1(a6)),a8)),
% 60.96/61.15 inference(scs_inference,[],[35,1591,1610,1028,1619,1603,1616,1139,1225,38,13,34,27,6,8,7,5,4,9,31,30,22,2,32,3,11])).
% 60.96/61.15 cnf(1653,plain,
% 60.96/61.15 (~P2(a6,f2(f3(a6),a8))),
% 60.96/61.15 inference(scs_inference,[],[35,135,1591,1610,1028,1619,1603,1650,1616,1139,1225,38,13,34,27,6,8,7,5,4,9,31,30,22,2,32,3,11,12])).
% 60.96/61.15 cnf(1658,plain,
% 60.96/61.15 (~E(a6,f2(f3(a6),a8))),
% 60.96/61.15 inference(scs_inference,[],[35,135,1591,1610,1028,1619,1603,1650,1616,1139,80,1225,155,683,38,13,34,27,6,8,7,5,4,9,31,30,22,2,32,3,11,12,33,23])).
% 60.96/61.15 cnf(1668,plain,
% 60.96/61.15 (E(f2(f3(a6),x16681),f2(f1(a4),x16681))),
% 60.96/61.15 inference(scs_inference,[],[1640,1583,47,34,27,7,6,8,4,5])).
% 60.96/61.15 cnf(1670,plain,
% 60.96/61.15 (P1(f3(f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1640,1583,1647,47,34,27,7,6,8,4,5,9,31])).
% 60.96/61.15 cnf(1676,plain,
% 60.96/61.15 (~E(f2(f3(a6),a8),a6)),
% 60.96/61.15 inference(scs_inference,[],[1640,1583,1658,1647,1033,653,47,34,27,7,6,8,4,5,9,31,30,22,2])).
% 60.96/61.15 cnf(1677,plain,
% 60.96/61.15 (P1(f2(f3(a6),f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1640,1583,1658,1647,1033,1490,653,1017,47,34,27,7,6,8,4,5,9,31,30,22,2,32])).
% 60.96/61.15 cnf(1693,plain,
% 60.96/61.15 (E(f2(f3(a8),x16931),f2(f3(a6),x16931))),
% 60.96/61.15 inference(scs_inference,[],[1642,1676,185,34,27,7,8,6,9,5])).
% 60.96/61.15 cnf(1701,plain,
% 60.96/61.15 (~E(a8,f2(f3(a8),a6))),
% 60.96/61.15 inference(scs_inference,[],[1642,1676,1649,1497,1587,667,185,34,27,7,8,6,9,5,4,22,31,30,2])).
% 60.96/61.15 cnf(1704,plain,
% 60.96/61.15 (~E(f2(f1(a4),a8),a6)),
% 60.96/61.15 inference(scs_inference,[],[1642,1676,1649,1668,1497,1587,667,1002,993,185,34,27,7,8,6,9,5,4,22,31,30,2,32,3])).
% 60.96/61.15 cnf(1705,plain,
% 60.96/61.15 (E(f2(f3(a6),x17051),f2(f1(a4),x17051))),
% 60.96/61.15 inference(rename_variables,[],[1668])).
% 60.96/61.15 cnf(1707,plain,
% 60.96/61.15 (E(f2(x17071,f1(x17071)),x17071)),
% 60.96/61.15 inference(rename_variables,[],[13])).
% 60.96/61.15 cnf(1708,plain,
% 60.96/61.15 (~P2(f2(a6,f1(a6)),f2(a8,f1(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1642,1651,1676,1649,1653,1668,1497,1587,667,1002,993,185,13,1707,34,27,7,8,6,9,5,4,22,31,30,2,32,3,11,12])).
% 60.96/61.15 cnf(1710,plain,
% 60.96/61.15 (~E(f2(a6,f1(a6)),f2(f3(a6),a8))),
% 60.96/61.15 inference(scs_inference,[],[1642,1651,1676,1649,1653,1668,1497,1587,667,1002,1186,993,185,13,1707,34,27,7,8,6,9,5,4,22,31,30,2,32,3,11,12,23])).
% 60.96/61.15 cnf(1712,plain,
% 60.96/61.15 (P1(f2(f1(a4),f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1642,1677,1651,1676,1649,1653,1668,1705,1497,1587,667,1002,1186,993,185,13,1707,34,27,7,8,6,9,5,4,22,31,30,2,32,3,11,12,23,10])).
% 60.96/61.15 cnf(1719,plain,
% 60.96/61.15 (E(f2(x17191,f2(a4,a6)),f2(x17191,f2(a4,a8)))),
% 60.96/61.15 inference(scs_inference,[],[1622,1701,15,34,27,6])).
% 60.96/61.15 cnf(1729,plain,
% 60.96/61.15 (~E(a6,f2(f1(a4),a8))),
% 60.96/61.15 inference(scs_inference,[],[1622,1701,1704,668,615,15,34,27,6,7,8,4,5,9,30,31,2])).
% 60.96/61.15 cnf(1730,plain,
% 60.96/61.15 (P1(f2(f2(f3(a5),a5),a4))),
% 60.96/61.15 inference(scs_inference,[],[1622,1701,1704,668,615,1007,836,15,34,27,6,7,8,4,5,9,30,31,2,32])).
% 60.96/61.15 cnf(1737,plain,
% 60.96/61.15 (P2(f2(f3(f3(a6)),f3(a8)),f3(f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1622,1701,1704,1571,1572,1606,1602,1507,668,615,1019,1007,836,15,34,27,6,7,8,4,5,9,30,31,2,32,23,3,11])).
% 60.96/61.15 cnf(1738,plain,
% 60.96/61.15 (E(f2(x17381,f3(a6)),f2(x17381,f3(a8)))),
% 60.96/61.15 inference(rename_variables,[],[1606])).
% 60.96/61.15 cnf(1739,plain,
% 60.96/61.15 (P2(f3(a6),f2(f3(f3(a6)),f3(a8)))),
% 60.96/61.15 inference(scs_inference,[],[1622,1701,1704,909,1571,1572,1606,1738,1602,1507,668,615,1019,1007,836,15,34,27,6,7,8,4,5,9,30,31,2,32,23,3,11,12])).
% 60.96/61.15 cnf(1761,plain,
% 60.96/61.15 (P1(f2(f3(a8),f1(a4)))),
% 60.96/61.15 inference(scs_inference,[],[1670,1729,1710,1739,1737,1730,600,1487,1139,55,34,27,8,6,5,9,7,4,22,31,30,25,2,32])).
% 60.96/61.15 cnf(1765,plain,
% 60.96/61.15 (~E(f2(f3(a6),a6),f2(f1(a4),a8))),
% 60.96/61.15 inference(scs_inference,[],[1670,1729,1708,1710,1739,1737,1730,600,1487,1139,1186,55,241,34,27,8,6,5,9,7,4,22,31,30,25,2,32,23,3])).
% 60.96/61.15 cnf(1767,plain,
% 60.96/61.15 (~P2(f2(a6,f1(a6)),f2(f3(a8),a8))),
% 60.96/61.15 inference(scs_inference,[],[1670,1729,1708,1710,1739,1737,1730,600,135,1487,1139,1186,55,13,241,34,27,8,6,5,9,7,4,22,31,30,25,2,32,23,3,11])).
% 60.96/61.15 cnf(1771,plain,
% 60.96/61.15 (~E(f2(f2(a5,a4),a8),f2(a5,f2(a4,a6)))),
% 60.96/61.15 inference(scs_inference,[],[1670,1729,1406,1708,1710,1693,1739,1737,1730,600,135,1487,1139,1186,913,18,55,13,241,34,27,8,6,5,9,7,4,22,31,30,25,2,32,23,3,11,12,33])).
% 60.96/61.15 cnf(1791,plain,
% 60.96/61.15 (~E(f2(a5,f2(a4,a6)),f2(f2(a5,a4),a8))),
% 60.96/61.15 inference(scs_inference,[],[1712,1771,677,96,959,1737,174,34,27,5,9,8,6,7,4,31,22,30,2])).
% 60.96/61.15 cnf(1792,plain,
% 60.96/61.15 (P1(f2(f3(a6),a8))),
% 60.96/61.15 inference(scs_inference,[],[1712,1771,677,96,959,1737,1270,1017,174,34,27,5,9,8,6,7,4,31,22,30,2,32])).
% 60.96/61.15 cnf(1798,plain,
% 60.96/61.15 (P2(f2(f3(f2(a4,a6)),f2(a4,a8)),f2(a4,a6))),
% 60.96/61.15 inference(scs_inference,[],[1712,1761,777,1491,1771,1719,1637,1482,677,96,959,1737,1270,1017,174,34,27,5,9,8,6,7,4,31,22,30,2,32,23,3,11])).
% 60.96/61.15 cnf(1824,plain,
% 60.96/61.15 ($false),
% 60.96/61.15 inference(scs_inference,[],[1792,1798,1767,1791,1765,638,1517,133,1719,1186,155,206,34,27,8,5,6,9,22,31,4,7,30,25,2,23,3]),
% 60.96/61.15 ['proof']).
% 60.96/61.15 % SZS output end Proof
% 60.96/61.15 % Total time :60.360000s
%------------------------------------------------------------------------------