%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT009-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 04:40:12 EDT 2024
% Result : Unsatisfiable 62.97s 63.07s
% Output : CNFRefutation 63.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : CAT009-3 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Jun 18 12:28:54 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.48/0.63 start to proof:theBenchmark
% 62.97/63.06 %-------------------------------------------
% 62.97/63.06 % File :CSE---1.7
% 62.97/63.06 % Problem :theBenchmark
% 62.97/63.06 % Transform :cnf
% 62.97/63.06 % Format :tptp:raw
% 62.97/63.06 % Command :java -jar mcs_scs.jar %d %s
% 62.97/63.06
% 62.97/63.06 % Result :Theorem 62.330000s
% 62.97/63.06 % Output :CNFRefutation 62.330000s
% 62.97/63.06 %-------------------------------------------
% 62.97/63.06 %--------------------------------------------------------------------------
% 62.97/63.06 % File : CAT009-3 : TPTP v8.2.0. Released v1.0.0.
% 62.97/63.06 % Domain : Category Theory
% 62.97/63.06 % Problem : If xy is defined, then domain(xy) = domain(y)
% 62.97/63.06 % Version : [Sco79] axioms : Reduced > Complete.
% 62.97/63.06 % English :
% 62.97/63.06
% 62.97/63.06 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 62.97/63.06 % Source : [ANL]
% 62.97/63.06 % Names : p9.ver3.in [ANL]
% 62.97/63.06
% 62.97/63.06 % Status : Unsatisfiable
% 62.97/63.06 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.29 v6.0.0, 0.30 v5.5.0, 0.45 v5.3.0, 0.44 v5.2.0, 0.31 v5.1.0, 0.35 v5.0.0, 0.21 v4.1.0, 0.23 v4.0.1, 0.27 v3.7.0, 0.10 v3.5.0, 0.18 v3.4.0, 0.25 v3.3.0, 0.36 v3.2.0, 0.38 v3.1.0, 0.36 v2.7.0, 0.42 v2.6.0, 0.40 v2.5.0, 0.42 v2.4.0, 0.22 v2.3.0, 0.33 v2.2.1, 0.44 v2.2.0, 0.67 v2.1.0, 0.78 v2.0.0
% 62.97/63.06 % Syntax : Number of clauses : 19 ( 5 unt; 2 nHn; 14 RR)
% 62.97/63.06 % Number of literals : 39 ( 16 equ; 18 neg)
% 62.97/63.06 % Maximal clause size : 4 ( 2 avg)
% 62.97/63.06 % Maximal term depth : 3 ( 1 avg)
% 62.97/63.06 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 62.97/63.06 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 62.97/63.06 % Number of variables : 31 ( 4 sgn)
% 62.97/63.06 % SPC : CNF_UNS_RFO_SEQ_NHN
% 62.97/63.06
% 62.97/63.06 % Comments : Axioms simplified by Art Quaife. The ANL version has been
% 62.97/63.06 % extended to use all axioms.
% 62.97/63.06 %--------------------------------------------------------------------------
% 62.97/63.06 %----Include Scott's axioms for category theory
% 62.97/63.06 include('Axioms/CAT003-0.ax').
% 62.97/63.07 %--------------------------------------------------------------------------
% 62.97/63.07 cnf(ab_exists,hypothesis,
% 62.97/63.07 there_exists(compose(a,b)) ).
% 62.97/63.07
% 62.97/63.07 cnf(prove_domain_of_ab_equals_domain_of_b,negated_conjecture,
% 62.97/63.07 domain(compose(a,b)) != domain(b) ).
% 62.97/63.07
% 62.97/63.07 %--------------------------------------------------------------------------
% 62.97/63.07 %-------------------------------------------
% 62.97/63.07 % Proof found
% 62.97/63.07 % SZS status Theorem for theBenchmark
% 62.97/63.07 % SZS output start Proof
% 62.97/63.07 %ClaNum:30(EqnAxiom:12)
% 62.97/63.07 %VarNum:58(SingletonVarNum:27)
% 62.97/63.07 %MaxLitNum:3
% 62.97/63.07 %MaxfuncDepth:2
% 62.97/63.07 %SharedTerms:7
% 62.97/63.07 %goalClause: 17
% 62.97/63.07 %singleGoalClaCount:1
% 62.97/63.07 [15]P1(f2(a4,a5))
% 62.97/63.07 [17]~E(f1(f2(a4,a5)),f1(a5))
% 62.97/63.07 [13]E(f2(x131,f1(x131)),x131)
% 62.97/63.07 [14]E(f2(f3(x141),x141),x141)
% 62.97/63.07 [16]E(f2(f2(x161,x162),x163),f2(x161,f2(x162,x163)))
% 62.97/63.07 [18]P1(x181)+~P1(f1(x181))
% 62.97/63.07 [19]P1(x191)+~P1(f3(x191))
% 62.97/63.07 [20]~P2(x201,x202)+E(x201,x202)
% 62.97/63.07 [22]P1(x221)+~P2(x222,x221)
% 62.97/63.07 [23]P1(x231)+~P2(x231,x232)
% 62.97/63.07 [25]E(x251,x252)+P1(f6(x251,x252))
% 62.97/63.07 [27]E(f3(x271),f1(x272))+~P1(f2(x272,x271))
% 62.97/63.07 [28]P1(f1(x281))+~P1(f2(x281,x282))
% 62.97/63.07 [29]P1(f3(x291))+~P1(f2(x291,x292))
% 62.97/63.07 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 62.97/63.07 [26]E(x261,x262)+E(f6(x261,x262),x262)+E(f6(x261,x262),x261)
% 62.97/63.07 [30]~E(f3(x302),f1(x301))+~P1(f1(x301))+P1(f2(x301,x302))
% 62.97/63.07 %EqnAxiom
% 62.97/63.07 [1]E(x11,x11)
% 62.97/63.07 [2]E(x22,x21)+~E(x21,x22)
% 62.97/63.07 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 62.97/63.07 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 62.97/63.07 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 62.97/63.07 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 62.97/63.07 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 62.97/63.07 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 62.97/63.07 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 62.97/63.07 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 62.97/63.07 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 62.97/63.07 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 62.97/63.07
% 62.97/63.07 %-------------------------------------------
% 62.97/63.08 cnf(31,plain,
% 62.97/63.08 (~P1(x311)+P2(x311,x311)),
% 62.97/63.08 inference(equality_inference,[],[21])).
% 62.97/63.08 cnf(32,plain,
% 62.97/63.08 (~P2(f1(f2(a4,a5)),f1(a5))),
% 62.97/63.08 inference(scs_inference,[],[17,20])).
% 62.97/63.08 cnf(34,plain,
% 62.97/63.08 (E(x341,f2(x341,f1(x341)))),
% 62.97/63.08 inference(scs_inference,[],[17,13,20,2])).
% 62.97/63.08 cnf(35,plain,
% 62.97/63.08 (~E(f2(a4,a5),a5)),
% 62.97/63.08 inference(scs_inference,[],[17,13,20,2,4])).
% 62.97/63.08 cnf(36,plain,
% 62.97/63.08 (E(f3(a5),f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[17,13,15,20,2,4,27])).
% 62.97/63.08 cnf(38,plain,
% 62.97/63.08 (P2(f2(a4,a5),f2(f2(a4,a5),f1(f2(a4,a5))))),
% 62.97/63.08 inference(scs_inference,[],[17,13,15,20,2,4,27,21])).
% 62.97/63.08 cnf(40,plain,
% 62.97/63.08 (~E(f1(f2(a4,a5)),f2(f3(f1(a5)),f1(a5)))),
% 62.97/63.08 inference(scs_inference,[],[17,13,14,15,20,2,4,27,21,3])).
% 62.97/63.08 cnf(42,plain,
% 62.97/63.08 (P1(f2(f2(a4,a5),f1(f2(a4,a5))))),
% 62.97/63.08 inference(scs_inference,[],[17,13,14,15,20,2,4,27,21,3,10])).
% 62.97/63.08 cnf(43,plain,
% 62.97/63.08 (P2(f2(a4,a5),f2(a4,a5))),
% 62.97/63.08 inference(scs_inference,[],[17,13,14,15,20,2,4,27,21,3,10,12])).
% 62.97/63.08 cnf(48,plain,
% 62.97/63.08 (E(f1(a4),f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[40,36,20,2])).
% 62.97/63.08 cnf(49,plain,
% 62.97/63.08 (E(f3(a5),f2(f1(a4),f1(f1(a4))))),
% 62.97/63.08 inference(scs_inference,[],[34,40,36,20,2,3])).
% 62.97/63.08 cnf(51,plain,
% 62.97/63.08 (~P1(f3(a5))+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[34,40,36,20,2,3,10])).
% 62.97/63.08 cnf(52,plain,
% 62.97/63.08 (~P2(x521,f3(a5))+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[34,40,36,20,2,3,10,22])).
% 62.97/63.08 cnf(54,plain,
% 62.97/63.08 (~P2(f3(a5),x541)+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[34,40,36,20,2,3,10,22,23])).
% 62.97/63.08 cnf(56,plain,
% 62.97/63.08 (P1(f1(a4))+~P1(f2(a5,x561))),
% 62.97/63.08 inference(scs_inference,[],[34,40,36,20,2,3,10,22,23,29])).
% 62.97/63.08 cnf(58,plain,
% 62.97/63.08 (~E(f2(f2(a4,a5),f1(f2(a4,a5))),f3(a5))+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[34,40,42,36,20,2,3,10,22,23,29,30,21])).
% 62.97/63.08 cnf(61,plain,
% 62.97/63.08 (~P2(f2(a4,a5),a5)),
% 62.97/63.08 inference(scs_inference,[],[35,20])).
% 62.97/63.08 cnf(63,plain,
% 62.97/63.08 (E(f2(f1(a4),f1(f1(a4))),f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[35,49,20,2])).
% 62.97/63.08 cnf(64,plain,
% 62.97/63.08 (~E(f2(f2(a4,a5),f1(f2(a4,a5))),a5)),
% 62.97/63.08 inference(scs_inference,[],[35,49,38,20,2,12])).
% 62.97/63.08 cnf(65,plain,
% 62.97/63.08 (E(f2(f3(f1(a4)),f1(a4)),f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[35,49,48,38,14,20,2,12,3])).
% 62.97/63.08 cnf(67,plain,
% 62.97/63.08 (~P1(f3(a5))+P1(f2(f1(a4),f1(f1(a4))))),
% 62.97/63.08 inference(scs_inference,[],[35,49,48,38,14,20,2,12,3,10])).
% 62.97/63.08 cnf(74,plain,
% 62.97/63.08 (~E(f2(f2(a4,a5),f1(f2(a4,a5))),f3(a5))+P1(f2(f1(a4),f1(f1(a4))))),
% 62.97/63.08 inference(scs_inference,[],[35,49,48,38,42,14,20,2,12,3,10,22,23,29,30,21])).
% 62.97/63.08 cnf(76,plain,
% 62.97/63.08 (~E(f2(a4,a5),f3(a5))+P1(f2(f1(a4),f1(f1(a4))))),
% 62.97/63.08 inference(scs_inference,[],[35,49,48,38,42,14,20,2,12,3,10,22,23,29,30,21,11])).
% 62.97/63.08 cnf(79,plain,
% 62.97/63.08 (E(f3(a5),f2(f3(f1(a4)),f1(a4)))),
% 62.97/63.08 inference(scs_inference,[],[65,64,20,2])).
% 62.97/63.08 cnf(80,plain,
% 62.97/63.08 (~P1(f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,64,20,2,10])).
% 62.97/63.08 cnf(81,plain,
% 62.97/63.08 (P1(f3(a5))+~E(f2(f2(a4,a5),f1(f2(a4,a5))),f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,64,20,2,10,74])).
% 62.97/63.08 cnf(82,plain,
% 62.97/63.08 (P1(f3(a5))+~E(f2(a4,a5),f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,64,20,2,10,74,76])).
% 62.97/63.08 cnf(83,plain,
% 62.97/63.08 (~P2(x831,f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,64,20,2,10,74,76,22])).
% 62.97/63.08 cnf(85,plain,
% 62.97/63.08 (~P2(f2(f1(a4),f1(f1(a4))),x851)+P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,64,20,2,10,74,76,22,23])).
% 62.97/63.08 cnf(87,plain,
% 62.97/63.08 (~E(f2(f2(a4,a5),f1(f2(a4,a5))),f1(a4))+P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,48,64,20,2,10,74,76,22,23,30,3])).
% 62.97/63.08 cnf(88,plain,
% 62.97/63.08 (~E(f2(a4,a5),f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[63,65,48,38,64,20,2,10,74,76,22,23,30,3,11])).
% 62.97/63.08 cnf(89,plain,
% 62.97/63.08 (E(f2(x891,f2(x892,x893)),f2(f2(x891,x892),x893))),
% 62.97/63.08 inference(scs_inference,[],[16,2])).
% 62.97/63.08 cnf(102,plain,
% 62.97/63.08 (P1(f2(f3(f1(a4)),f1(a4)))+~P1(f2(a5,x1021))),
% 62.97/63.08 inference(scs_inference,[],[79,16,2,10,81,87,80,82,83,85,88,22,20,29])).
% 62.97/63.08 cnf(108,plain,
% 62.97/63.08 (E(x1081,f2(f3(x1081),x1081))),
% 62.97/63.08 inference(scs_inference,[],[14,2])).
% 62.97/63.08 cnf(109,plain,
% 62.97/63.08 (P1(f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 62.97/63.08 inference(scs_inference,[],[15,14,2,10])).
% 62.97/63.08 cnf(110,plain,
% 62.97/63.08 (P2(f2(f3(f2(a4,a5)),f2(a4,a5)),f2(a4,a5))),
% 62.97/63.08 inference(scs_inference,[],[108,43,11])).
% 62.97/63.08 cnf(112,plain,
% 62.97/63.08 (~P1(f1(a4))+P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[48,108,43,11,10])).
% 62.97/63.08 cnf(129,plain,
% 62.97/63.08 (E(f2(f3(a5),f1(f3(a5))),f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[13,36,3])).
% 62.97/63.08 cnf(131,plain,
% 62.97/63.08 (E(f1(a4),f2(f3(a5),f1(f3(a5))))),
% 62.97/63.08 inference(scs_inference,[],[13,36,3,2])).
% 62.97/63.08 cnf(132,plain,
% 62.97/63.08 (~P1(f2(f3(a5),f1(f3(a5))))+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[13,36,3,2,10])).
% 62.97/63.08 cnf(133,plain,
% 62.97/63.08 (~P2(x1331,f2(f3(a5),f1(f3(a5))))+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[13,36,3,2,10,22])).
% 62.97/63.08 cnf(135,plain,
% 62.97/63.08 (~P2(f2(f3(a5),f1(f3(a5))),x1351)+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[13,36,3,2,10,22,23])).
% 62.97/63.08 cnf(142,plain,
% 62.97/63.08 (P1(f2(f3(a5),f1(f3(a5))))+~P2(f3(a5),x1421)),
% 62.97/63.08 inference(scs_inference,[],[131,10,58,52,54])).
% 62.97/63.08 cnf(155,plain,
% 62.97/63.08 (~P1(f2(f1(a4),f1(f1(a4))))+P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[51,80])).
% 62.97/63.08 cnf(156,plain,
% 62.97/63.08 (P1(f3(a5))),
% 62.97/63.08 inference(scs_inference,[],[15,112,28])).
% 62.97/63.08 cnf(157,plain,
% 62.97/63.08 (P1(f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[156,51])).
% 62.97/63.08 cnf(158,plain,
% 62.97/63.08 (P1(f2(f1(a4),f1(f1(a4))))),
% 62.97/63.08 inference(scs_inference,[],[156,67])).
% 62.97/63.08 cnf(160,plain,
% 62.97/63.08 (P1(a5)),
% 62.97/63.08 inference(scs_inference,[],[156,19])).
% 62.97/63.08 cnf(162,plain,
% 62.97/63.08 (P2(f3(a5),f2(f3(f1(a4)),f1(a4)))),
% 62.97/63.08 inference(scs_inference,[],[79,156,19,21])).
% 62.97/63.08 cnf(164,plain,
% 62.97/63.08 (P2(f3(a5),f1(a4))),
% 62.97/63.08 inference(scs_inference,[],[14,79,156,19,21,12])).
% 62.97/63.09 cnf(165,plain,
% 62.97/63.09 (E(f2(f3(x1651),x1651),x1651)),
% 62.97/63.09 inference(rename_variables,[],[14])).
% 62.97/63.09 cnf(166,plain,
% 62.97/63.09 (E(f2(f3(x1661),x1661),f2(x1661,f1(x1661)))),
% 62.97/63.09 inference(scs_inference,[],[14,165,79,34,156,19,21,12,3])).
% 62.97/63.09 cnf(168,plain,
% 62.97/63.09 (P1(f2(f3(a5),f1(f3(a5))))),
% 62.97/63.09 inference(scs_inference,[],[14,165,79,34,156,19,21,12,3,142])).
% 62.97/63.09 cnf(170,plain,
% 62.97/63.09 (E(f2(x1701,f1(x1701)),f2(f3(x1701),x1701))),
% 62.97/63.09 inference(scs_inference,[],[14,165,79,34,156,19,21,12,3,142,2])).
% 62.97/63.09 cnf(171,plain,
% 62.97/63.09 (P2(f2(f3(f1(a4)),f1(a4)),f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[14,165,79,34,156,19,21,12,3,142,2,11])).
% 62.97/63.09 cnf(176,plain,
% 62.97/63.09 (P1(f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[168,132])).
% 62.97/63.09 cnf(177,plain,
% 62.97/63.09 (P1(f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[158,155])).
% 62.97/63.09 cnf(179,plain,
% 62.97/63.09 (P1(a4)),
% 62.97/63.09 inference(scs_inference,[],[157,18])).
% 62.97/63.09 cnf(181,plain,
% 62.97/63.09 (P2(f2(f1(a4),f1(f1(a4))),f3(a5))),
% 62.97/63.09 inference(scs_inference,[],[63,158,157,18,21])).
% 62.97/63.09 cnf(183,plain,
% 62.97/63.09 (P2(f1(a4),f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[14,63,171,158,157,18,21,11])).
% 62.97/63.09 cnf(184,plain,
% 62.97/63.09 (E(f2(f3(x1841),x1841),x1841)),
% 62.97/63.09 inference(rename_variables,[],[14])).
% 62.97/63.09 cnf(186,plain,
% 62.97/63.09 (E(f2(f3(f3(a5)),f3(a5)),f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[14,184,63,48,36,171,158,157,18,21,11,12,3])).
% 62.97/63.09 cnf(189,plain,
% 62.97/63.09 (P1(f2(f3(f3(a5)),f3(a5)))),
% 62.97/63.09 inference(scs_inference,[],[14,184,63,48,36,171,158,157,18,21,11,12,3,2,10])).
% 62.97/63.09 cnf(190,plain,
% 62.97/63.09 (P1(f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[181,52])).
% 62.97/63.09 cnf(195,plain,
% 62.97/63.09 (P2(f2(f3(f3(a5)),f3(a5)),f3(a5))),
% 62.97/63.09 inference(scs_inference,[],[14,189,21])).
% 62.97/63.09 cnf(201,plain,
% 62.97/63.09 (P2(a5,f2(f3(a5),a5))),
% 62.97/63.09 inference(scs_inference,[],[108,160,21])).
% 62.97/63.09 cnf(202,plain,
% 62.97/63.09 (E(x2021,f2(f3(x2021),x2021))),
% 62.97/63.09 inference(rename_variables,[],[108])).
% 62.97/63.09 cnf(204,plain,
% 62.97/63.09 (P2(f2(f3(a5),a5),f2(f3(a5),a5))),
% 62.97/63.09 inference(scs_inference,[],[108,202,160,21,11])).
% 62.97/63.09 cnf(208,plain,
% 62.97/63.09 (P2(a4,f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[108,179,21])).
% 62.97/63.09 cnf(209,plain,
% 62.97/63.09 (E(x2091,f2(f3(x2091),x2091))),
% 62.97/63.09 inference(rename_variables,[],[108])).
% 62.97/63.09 cnf(211,plain,
% 62.97/63.09 (P2(f2(f3(a4),a4),f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[108,209,179,21,11])).
% 62.97/63.09 cnf(213,plain,
% 62.97/63.09 (P2(a5,a5)),
% 62.97/63.09 inference(scs_inference,[],[14,108,209,201,179,21,11,12])).
% 62.97/63.09 cnf(217,plain,
% 62.97/63.09 (P2(a4,a4)),
% 62.97/63.09 inference(scs_inference,[],[14,61,208,213,11,12])).
% 62.97/63.09 cnf(219,plain,
% 62.97/63.09 (~P2(a5,f2(a4,a5))),
% 62.97/63.09 inference(scs_inference,[],[14,61,208,213,11,12,20])).
% 62.97/63.09 cnf(223,plain,
% 62.97/63.09 (~E(f2(f3(a5),a5),f2(a4,a5))),
% 62.97/63.09 inference(scs_inference,[],[219,201,110,11,12])).
% 62.97/63.09 cnf(224,plain,
% 62.97/63.09 (~E(f3(a5),a4)),
% 62.97/63.09 inference(scs_inference,[],[219,201,110,11,12,5])).
% 62.97/63.09 cnf(227,plain,
% 62.97/63.09 (~P1(f2(a5,x2271))+P1(f3(f3(f1(a4))))),
% 62.97/63.09 inference(scs_inference,[],[102,29])).
% 62.97/63.09 cnf(228,plain,
% 62.97/63.09 (~P2(f2(f3(a5),a5),f2(a4,a5))),
% 62.97/63.09 inference(scs_inference,[],[223,20])).
% 62.97/63.09 cnf(230,plain,
% 62.97/63.09 (P2(f2(f3(a4),a4),a4)),
% 62.97/63.09 inference(scs_inference,[],[108,223,217,20,11])).
% 62.97/63.09 cnf(232,plain,
% 62.97/63.09 (P1(f3(f1(a4)))+~P1(f2(a5,x2321))),
% 62.97/63.09 inference(scs_inference,[],[227,19])).
% 62.97/63.09 cnf(233,plain,
% 62.97/63.09 (~P2(f3(a5),a4)),
% 62.97/63.09 inference(scs_inference,[],[224,20])).
% 62.97/63.09 cnf(235,plain,
% 62.97/63.09 (~E(f2(a4,a5),f2(f3(a5),a5))),
% 62.97/63.09 inference(scs_inference,[],[228,43,224,20,11])).
% 62.97/63.09 cnf(236,plain,
% 62.97/63.09 (~E(f2(f3(f1(a4)),f1(a4)),a4)),
% 62.97/63.09 inference(scs_inference,[],[228,162,43,224,20,11,12])).
% 62.97/63.09 cnf(237,plain,
% 62.97/63.09 (~E(a4,f3(a5))),
% 62.97/63.09 inference(scs_inference,[],[228,162,43,224,20,11,12,5])).
% 62.97/63.09 cnf(238,plain,
% 62.97/63.09 (~E(a4,f2(f1(a4),f1(f1(a4))))),
% 62.97/63.09 inference(scs_inference,[],[228,63,162,43,224,20,11,12,5,3])).
% 62.97/63.09 cnf(239,plain,
% 62.97/63.09 (P2(f3(f1(a4)),f3(f1(a4)))+~P1(f2(a5,x2391))),
% 62.97/63.09 inference(scs_inference,[],[232,31])).
% 62.97/63.09 cnf(240,plain,
% 62.97/63.09 (~P2(a4,f2(f1(a4),f1(f1(a4))))),
% 62.97/63.09 inference(scs_inference,[],[238,20])).
% 62.97/63.09 cnf(242,plain,
% 62.97/63.09 (~E(a4,f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[48,238,237,20,3])).
% 62.97/63.09 cnf(243,plain,
% 62.97/63.09 (~E(f2(f3(f2(a4,a5)),f2(a4,a5)),f2(f3(a5),a5))),
% 62.97/63.09 inference(scs_inference,[],[228,48,238,110,237,20,3,11])).
% 62.97/63.09 cnf(244,plain,
% 62.97/63.09 (~E(f1(a4),a4)),
% 62.97/63.09 inference(scs_inference,[],[233,228,48,238,110,164,237,20,3,11,12])).
% 62.97/63.09 cnf(245,plain,
% 62.97/63.09 (~P2(a4,f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[242,20])).
% 62.97/63.09 cnf(247,plain,
% 62.97/63.09 (~E(a4,f2(f3(f1(a4)),f1(a4)))),
% 62.97/63.09 inference(scs_inference,[],[65,242,237,20,3])).
% 62.97/63.09 cnf(248,plain,
% 62.97/63.09 (~E(f2(f3(a4),a4),f3(a5))),
% 62.97/63.09 inference(scs_inference,[],[233,65,242,230,237,20,3,11])).
% 62.97/63.09 cnf(249,plain,
% 62.97/63.09 (~P2(a4,f2(f3(f1(a4)),f1(a4)))),
% 62.97/63.09 inference(scs_inference,[],[247,20])).
% 62.97/63.09 cnf(251,plain,
% 62.97/63.09 (~E(f2(f3(a4),a4),f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[48,247,248,20,3])).
% 62.97/63.09 cnf(253,plain,
% 62.97/63.09 (~P2(f2(f3(a4),a4),f1(a4))),
% 62.97/63.09 inference(scs_inference,[],[251,20])).
% 62.97/63.09 cnf(255,plain,
% 62.97/63.09 (~E(f2(f3(a4),a4),f2(f3(f1(a4)),f1(a4)))),
% 62.97/63.09 inference(scs_inference,[],[65,251,248,20,3])).
% 62.97/63.09 cnf(258,plain,
% 62.97/63.09 (~P2(f2(f3(a4),a4),f2(f3(f1(a4)),f1(a4)))),
% 62.97/63.09 inference(scs_inference,[],[255,20])).
% 62.97/63.09 cnf(260,plain,
% 62.97/63.09 (~E(f2(f3(a4),a4),f2(f3(f3(a5)),f3(a5)))),
% 62.97/63.09 inference(scs_inference,[],[186,255,251,20,3])).
% 62.97/63.09 cnf(261,plain,
% 62.97/63.09 (~E(f1(a4),f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[253,186,255,251,183,20,3,11])).
% 62.97/63.09 cnf(262,plain,
% 62.97/63.09 (~P2(f2(f3(a4),a4),f2(f3(f3(a5)),f3(a5)))),
% 62.97/63.09 inference(scs_inference,[],[260,20])).
% 62.97/63.09 cnf(264,plain,
% 62.97/63.09 (~E(a4,f2(f3(a5),f1(f3(a5))))),
% 62.97/63.09 inference(scs_inference,[],[129,260,242,20,3])).
% 62.97/63.09 cnf(265,plain,
% 62.97/63.09 (~E(f3(a5),f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[258,129,260,242,162,20,3,11])).
% 62.97/63.09 cnf(267,plain,
% 62.97/63.09 (~P2(a4,f2(f3(a5),f1(f3(a5))))),
% 62.97/63.09 inference(scs_inference,[],[264,20])).
% 62.97/63.09 cnf(269,plain,
% 62.97/63.09 (~E(a4,f2(f3(f3(a5)),f3(a5)))),
% 62.97/63.09 inference(scs_inference,[],[262,264,230,20,12])).
% 62.97/63.09 cnf(271,plain,
% 62.97/63.09 (~P2(f1(a4),a4)),
% 62.97/63.09 inference(scs_inference,[],[244,20])).
% 62.97/63.09 cnf(274,plain,
% 62.97/63.09 (~P2(f2(f3(f1(a4)),f1(a4)),a4)),
% 62.97/63.09 inference(scs_inference,[],[236,20])).
% 62.97/63.09 cnf(277,plain,
% 62.97/63.09 (~P2(a4,f2(f3(f3(a5)),f3(a5)))),
% 62.97/63.09 inference(scs_inference,[],[269,20])).
% 62.97/63.09 cnf(282,plain,
% 62.97/63.09 (~E(f2(f3(a5),a5),f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 62.97/63.09 inference(scs_inference,[],[204,243,20,11])).
% 62.97/63.09 cnf(284,plain,
% 62.97/63.09 (~P2(f2(f3(a5),a5),f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 62.97/63.09 inference(scs_inference,[],[282,20])).
% 62.97/63.09 cnf(287,plain,
% 62.97/63.09 (~P2(f2(a4,a5),f2(f3(a5),a5))),
% 62.97/63.09 inference(scs_inference,[],[235,20])).
% 62.97/63.09 cnf(292,plain,
% 62.97/63.09 (~P2(f1(a4),f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[261,20])).
% 62.97/63.09 cnf(294,plain,
% 62.97/63.09 (~P2(f3(a5),f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[265,20])).
% 62.97/63.09 cnf(305,plain,
% 62.97/63.09 (~E(f2(f3(f3(a5)),f3(a5)),a4)),
% 62.97/63.09 inference(scs_inference,[],[195,237,20,11])).
% 62.97/63.09 cnf(307,plain,
% 62.97/63.09 (~P2(f2(f3(f3(a5)),f3(a5)),a4)),
% 62.97/63.09 inference(scs_inference,[],[305,20])).
% 62.97/63.09 cnf(323,plain,
% 62.97/63.09 (~E(f2(a4,a5),f2(a5,f1(a5)))),
% 62.97/63.09 inference(scs_inference,[],[35,13,3])).
% 62.97/63.09 cnf(325,plain,
% 62.97/63.09 (~P2(f2(a4,a5),f2(a5,f1(a5)))),
% 62.97/63.09 inference(scs_inference,[],[35,13,3,20])).
% 62.97/63.09 cnf(329,plain,
% 62.97/63.09 (P1(f2(f3(a4),a4))),
% 62.97/63.09 inference(scs_inference,[],[176,108,18,10])).
% 62.97/63.09 cnf(330,plain,
% 62.97/63.09 (E(f3(a4),f1(f3(a4)))),
% 62.97/63.09 inference(scs_inference,[],[329,27])).
% 62.97/63.09 cnf(333,plain,
% 62.97/63.09 (P1(f2(a4,f1(a4)))),
% 62.97/63.09 inference(scs_inference,[],[166,329,27,2,10])).
% 62.97/63.09 cnf(335,plain,
% 62.97/63.09 (E(f2(f3(f3(a4)),f3(a4)),f1(f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[166,14,329,27,2,10,3])).
% 63.08/63.09 cnf(337,plain,
% 63.08/63.09 (E(f3(f1(a4)),f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[333,27])).
% 63.08/63.09 cnf(339,plain,
% 63.08/63.09 (E(f1(f3(a4)),f2(f3(f3(a4)),f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[335,333,27,2])).
% 63.08/63.09 cnf(340,plain,
% 63.08/63.09 (~E(a4,f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[335,242,333,27,2,3])).
% 63.08/63.09 cnf(341,plain,
% 63.08/63.09 (~P2(a4,f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[335,242,333,27,2,3,20])).
% 63.08/63.09 cnf(352,plain,
% 63.08/63.09 (E(f1(a4),f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[337,2])).
% 63.08/63.09 cnf(353,plain,
% 63.08/63.09 (P1(f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[177,337,2,10])).
% 63.08/63.09 cnf(355,plain,
% 63.08/63.09 (~P2(f2(f3(a4),a4),f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[251,177,337,2,10,3,20])).
% 63.08/63.09 cnf(357,plain,
% 63.08/63.09 (~P1(f1(f3(a4)))+P1(f2(f3(f3(a4)),f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[339,10])).
% 63.08/63.09 cnf(368,plain,
% 63.08/63.09 (~P1(f3(a4))+P1(f1(f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[330,10])).
% 63.08/63.09 cnf(376,plain,
% 63.08/63.09 (P2(f1(f3(a4)),f1(f3(a4)))+~P1(f3(a4))),
% 63.08/63.09 inference(scs_inference,[],[368,31])).
% 63.08/63.09 cnf(389,plain,
% 63.08/63.09 (P2(f2(f3(a5),f1(f3(a5))),f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[129,168,21])).
% 63.08/63.09 cnf(392,plain,
% 63.08/63.09 (~E(f2(f3(a5),f1(f3(a5))),a4)),
% 63.08/63.09 inference(scs_inference,[],[129,245,48,168,21,12,11])).
% 63.08/63.09 cnf(393,plain,
% 63.08/63.09 (~P2(f2(f3(a5),f1(f3(a5))),a4)),
% 63.08/63.09 inference(scs_inference,[],[129,245,48,168,21,12,11,20])).
% 63.08/63.09 cnf(395,plain,
% 63.08/63.09 (P1(f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[389,135])).
% 63.08/63.09 cnf(403,plain,
% 63.08/63.09 (E(f3(a5),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[160,108,10,27])).
% 63.08/63.09 cnf(405,plain,
% 63.08/63.09 (E(f1(f3(a5)),f3(a5))),
% 63.08/63.09 inference(scs_inference,[],[160,108,10,27,2])).
% 63.08/63.09 cnf(410,plain,
% 63.08/63.09 (P1(f2(a5,f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[160,34,10])).
% 63.08/63.09 cnf(412,plain,
% 63.08/63.09 (~E(f2(f3(a4),a4),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[160,34,405,248,10,3])).
% 63.08/63.09 cnf(413,plain,
% 63.08/63.09 (P2(f3(f1(a4)),f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[160,34,405,248,10,3,239])).
% 63.08/63.09 cnf(419,plain,
% 63.08/63.09 (E(f1(a5),f3(f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[160,34,405,248,10,3,239,227,27,2])).
% 63.08/63.09 cnf(422,plain,
% 63.08/63.09 (~E(f3(f1(a4)),f2(f3(a4),a4))),
% 63.08/63.09 inference(scs_inference,[],[160,355,34,405,248,10,3,239,227,27,2,20,11])).
% 63.08/63.09 cnf(423,plain,
% 63.08/63.09 (P1(f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[410,56])).
% 63.08/63.09 cnf(425,plain,
% 63.08/63.09 (P1(f2(f3(f1(a4)),f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[410,102])).
% 63.08/63.09 cnf(431,plain,
% 63.08/63.09 (P1(f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[156,403,422,20,10])).
% 63.08/63.09 cnf(434,plain,
% 63.08/63.09 (~E(f3(f1(a4)),a4)),
% 63.08/63.09 inference(scs_inference,[],[341,419,413,14,156,403,422,20,10,3,11])).
% 63.08/63.09 cnf(435,plain,
% 63.08/63.09 (E(f3(f1(a5)),f2(f3(f1(a5)),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[341,419,413,14,156,403,422,20,10,3,11,2])).
% 63.08/63.09 cnf(439,plain,
% 63.08/63.09 (~E(f1(f2(a4,a5)),f3(f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[40,435,434,20,3])).
% 63.08/63.09 cnf(440,plain,
% 63.08/63.09 (~P1(f3(f1(a5)))+P1(f2(f3(f1(a5)),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[40,435,434,20,3,10])).
% 63.08/63.09 cnf(441,plain,
% 63.08/63.09 (P1(f2(f3(f1(a5)),f1(a5)))+~P1(f2(f1(a5),x4411))),
% 63.08/63.09 inference(scs_inference,[],[40,435,434,20,3,10,29])).
% 63.08/63.09 cnf(450,plain,
% 63.08/63.09 (~P1(f3(f1(a5)))+P1(f1(f3(f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[440,28])).
% 63.08/63.09 cnf(461,plain,
% 63.08/63.09 (~P1(f1(a5))+P1(f3(f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[419,10])).
% 63.08/63.09 cnf(473,plain,
% 63.08/63.09 (P2(f2(a4,f1(a4)),f2(f3(a4),a4))),
% 63.08/63.09 inference(scs_inference,[],[170,333,21])).
% 63.08/63.09 cnf(479,plain,
% 63.08/63.09 (P2(f2(a5,f1(a5)),f2(f3(a5),a5))),
% 63.08/63.09 inference(scs_inference,[],[170,410,21])).
% 63.08/63.09 cnf(490,plain,
% 63.08/63.09 (~E(f2(a5,f1(a5)),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[287,479,11])).
% 63.08/63.09 cnf(491,plain,
% 63.08/63.09 (~P2(f2(a5,f1(a5)),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[287,479,11,20])).
% 63.08/63.09 cnf(494,plain,
% 63.08/63.09 (~E(f2(a4,f1(a4)),f3(a5))),
% 63.08/63.09 inference(scs_inference,[],[294,473,11])).
% 63.08/63.09 cnf(495,plain,
% 63.08/63.09 (~P2(f2(a4,f1(a4)),f3(a5))),
% 63.08/63.09 inference(scs_inference,[],[294,473,11,20])).
% 63.08/63.09 cnf(498,plain,
% 63.08/63.09 (~E(f2(f3(f3(a5)),f3(a5)),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[495,195,11])).
% 63.08/63.09 cnf(499,plain,
% 63.08/63.09 (~P2(f2(f3(f3(a5)),f3(a5)),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[495,195,11,20])).
% 63.08/63.09 cnf(505,plain,
% 63.08/63.09 (~P1(f2(f1(a5),x5051))+E(f3(f1(a5)),f1(f3(f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[441,27])).
% 63.08/63.09 cnf(510,plain,
% 63.08/63.09 (~E(f2(a4,f1(a4)),f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[292,473,11])).
% 63.08/63.09 cnf(511,plain,
% 63.08/63.09 (~P2(f2(a4,f1(a4)),f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[292,473,11,20])).
% 63.08/63.09 cnf(518,plain,
% 63.08/63.09 (~E(f3(a5),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[511,164,11])).
% 63.08/63.09 cnf(519,plain,
% 63.08/63.09 (~P2(f3(a5),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[511,164,11,20])).
% 63.08/63.09 cnf(549,plain,
% 63.08/63.09 (~E(f1(a4),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[244,13,3])).
% 63.08/63.09 cnf(551,plain,
% 63.08/63.09 (~P2(f1(a4),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[244,13,3,20])).
% 63.08/63.09 cnf(568,plain,
% 63.08/63.09 (P1(f1(f2(a4,a5)))),
% 63.08/63.09 inference(scs_inference,[],[38,22,28])).
% 63.08/63.09 cnf(570,plain,
% 63.08/63.09 (P1(f3(f2(a4,a5)))),
% 63.08/63.09 inference(scs_inference,[],[38,22,29])).
% 63.08/63.09 cnf(571,plain,
% 63.08/63.09 (P1(f3(a4))),
% 63.08/63.09 inference(scs_inference,[],[38,23,29])).
% 63.08/63.09 cnf(572,plain,
% 63.08/63.09 (P1(f1(f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[571,368])).
% 63.08/63.09 cnf(573,plain,
% 63.08/63.09 (P2(f1(f3(a4)),f1(f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[571,376])).
% 63.08/63.09 cnf(577,plain,
% 63.08/63.09 (E(x5771,f2(f3(x5771),x5771))),
% 63.08/63.09 inference(rename_variables,[],[108])).
% 63.08/63.09 cnf(580,plain,
% 63.08/63.09 (P2(f2(f3(f3(a4)),f3(a4)),f1(f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[335,108,577,571,21,12,11])).
% 63.08/63.09 cnf(585,plain,
% 63.08/63.09 (P1(f2(f3(f3(a4)),f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[572,357])).
% 63.08/63.09 cnf(625,plain,
% 63.08/63.09 (~P1(f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[439,2,27])).
% 63.08/63.09 cnf(626,plain,
% 63.08/63.09 (~P2(x6261,f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[625,22])).
% 63.08/63.09 cnf(628,plain,
% 63.08/63.09 (~P2(f2(f2(a4,a5),f1(a5)),x6281)),
% 63.08/63.09 inference(scs_inference,[],[625,22,23])).
% 63.08/63.09 cnf(634,plain,
% 63.08/63.09 (~E(f1(f3(a4)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[573,431,568,625,22,23,30,21,11])).
% 63.08/63.09 cnf(644,plain,
% 63.08/63.09 (~E(f3(f2(a4,a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[570,626,21])).
% 63.08/63.09 cnf(657,plain,
% 63.08/63.09 (E(f2(x6571,f3(f1(a5))),f2(x6571,f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[419,2,6])).
% 63.08/63.09 cnf(658,plain,
% 63.08/63.09 (~P2(f1(f3(a5)),f2(f3(a4),a4))),
% 63.08/63.09 inference(scs_inference,[],[412,2,20])).
% 63.08/63.09 cnf(662,plain,
% 63.08/63.09 (~P2(f2(a4,f1(a4)),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[658,473,431,21,11,20])).
% 63.08/63.09 cnf(668,plain,
% 63.08/63.09 (~P1(f3(f1(a5)))+P2(f3(f1(a5)),f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[419,2,21])).
% 63.08/63.09 cnf(669,plain,
% 63.08/63.09 (P2(f3(f1(a5)),f1(a5))+~P1(f1(f3(f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[668,18])).
% 63.08/63.09 cnf(693,plain,
% 63.08/63.09 (P1(f6(f2(a4,a5),a5))),
% 63.08/63.09 inference(scs_inference,[],[17,25,4])).
% 63.08/63.09 cnf(698,plain,
% 63.08/63.09 (P1(f6(a4,f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[235,25,5])).
% 63.08/63.09 cnf(699,plain,
% 63.08/63.09 (~E(f6(a4,f3(a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[698,626,21])).
% 63.08/63.09 cnf(702,plain,
% 63.08/63.09 (P1(f6(f3(a5),a4))),
% 63.08/63.09 inference(scs_inference,[],[223,25,5])).
% 63.08/63.09 cnf(707,plain,
% 63.08/63.09 (P2(f6(f2(a4,f1(a4)),f1(a4)),f6(f2(a4,f1(a4)),f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[510,25,31])).
% 63.08/63.09 cnf(731,plain,
% 63.08/63.09 (P1(f3(f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[410,28,461])).
% 63.08/63.09 cnf(732,plain,
% 63.08/63.09 (P1(f2(f3(f1(a5)),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[731,440])).
% 63.08/63.09 cnf(733,plain,
% 63.08/63.09 (P1(f1(f3(f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[731,450])).
% 63.08/63.09 cnf(736,plain,
% 63.08/63.09 (P2(f3(f1(a5)),f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[731,668])).
% 63.08/63.09 cnf(737,plain,
% 63.08/63.09 (P1(f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[731,19])).
% 63.08/63.09 cnf(739,plain,
% 63.08/63.09 (P2(f3(f1(a5)),f2(f3(f1(a5)),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[435,731,19,21])).
% 63.08/63.09 cnf(746,plain,
% 63.08/63.09 (P2(f3(f1(a5)),f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[733,669])).
% 63.08/63.09 cnf(747,plain,
% 63.08/63.09 (P1(f1(f3(f3(a4))))),
% 63.08/63.09 inference(scs_inference,[],[580,28,23])).
% 63.08/63.09 cnf(749,plain,
% 63.08/63.09 (P1(f3(f3(a4)))),
% 63.08/63.09 inference(scs_inference,[],[747,18])).
% 63.08/63.09 cnf(764,plain,
% 63.08/63.09 (E(f1(f3(a5)),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[15,4,27])).
% 63.08/63.09 cnf(765,plain,
% 63.08/63.09 (E(f1(f1(a4)),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[764,2])).
% 63.08/63.09 cnf(766,plain,
% 63.08/63.09 (P1(f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[764,431,2,10])).
% 63.08/63.09 cnf(768,plain,
% 63.08/63.09 (E(f1(f1(a4)),f3(a5))),
% 63.08/63.09 inference(scs_inference,[],[405,765,3])).
% 63.08/63.09 cnf(769,plain,
% 63.08/63.09 (E(f3(a5),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[405,765,3,2])).
% 63.08/63.09 cnf(786,plain,
% 63.08/63.09 (E(f3(f3(a5)),f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[15,7,27])).
% 63.08/63.09 cnf(788,plain,
% 63.08/63.09 (P1(f3(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[353,786,2,10])).
% 63.08/63.09 cnf(789,plain,
% 63.08/63.09 (E(f1(a4),f3(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[352,353,786,2,10,3])).
% 63.08/63.09 cnf(790,plain,
% 63.08/63.09 (~E(f3(a5),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[626,352,195,353,786,2,10,3,12])).
% 63.08/63.09 cnf(793,plain,
% 63.08/63.09 (E(f3(f3(a5)),f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[789,2])).
% 63.08/63.09 cnf(797,plain,
% 63.08/63.09 (~E(f1(a4),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[626,389,12])).
% 63.08/63.09 cnf(808,plain,
% 63.08/63.09 (~E(f3(f1(a5)),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[626,739,12,5])).
% 63.08/63.09 cnf(809,plain,
% 63.08/63.09 (~P2(f3(f1(a5)),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[626,739,12,5,20])).
% 63.08/63.09 cnf(812,plain,
% 63.08/63.09 (~E(f1(a5),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[626,746,12])).
% 63.08/63.09 cnf(817,plain,
% 63.08/63.09 (~E(f2(a4,a5),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[626,43,12])).
% 63.08/63.09 cnf(820,plain,
% 63.08/63.09 (~E(a4,f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[626,230,12])).
% 63.08/63.09 cnf(822,plain,
% 63.08/63.09 (~E(a5,f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[626,213,12])).
% 63.08/63.09 cnf(832,plain,
% 63.08/63.09 (~E(f2(a5,f1(a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[628,479,11])).
% 63.08/63.09 cnf(834,plain,
% 63.08/63.09 (~E(f2(f3(f1(a5)),f1(a5)),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[628,809,739,479,11,12])).
% 63.08/63.09 cnf(838,plain,
% 63.08/63.09 (~E(f2(a4,f1(a4)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.09 inference(scs_inference,[],[628,473,11])).
% 63.08/63.09 cnf(856,plain,
% 63.08/63.09 (P1(f2(f1(a5),f1(f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[732,166,10])).
% 63.08/63.09 cnf(859,plain,
% 63.08/63.09 (E(f3(f1(a5)),f1(f3(f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[856,505])).
% 63.08/63.09 cnf(873,plain,
% 63.08/63.09 (~E(f1(a5),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[809,736,12])).
% 63.08/63.09 cnf(874,plain,
% 63.08/63.09 (~P2(f1(a5),f2(a4,a5))),
% 63.08/63.09 inference(scs_inference,[],[809,736,12,20])).
% 63.08/63.09 cnf(877,plain,
% 63.08/63.09 (~E(f2(a4,a5),f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[874,43,11])).
% 63.08/63.09 cnf(878,plain,
% 63.08/63.09 (~P2(f2(a4,a5),f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[874,43,11,20])).
% 63.08/63.09 cnf(883,plain,
% 63.08/63.09 (P2(f1(f3(a5)),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[764,431,21])).
% 63.08/63.09 cnf(886,plain,
% 63.08/63.09 (~P2(f1(f1(a4)),f2(f3(a4),a4))),
% 63.08/63.09 inference(scs_inference,[],[764,658,431,21,12,20])).
% 63.08/63.09 cnf(890,plain,
% 63.08/63.09 (~P2(a4,f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[886,208,11,20])).
% 63.08/63.09 cnf(892,plain,
% 63.08/63.09 (~E(f1(f3(a5)),a4)),
% 63.08/63.09 inference(scs_inference,[],[890,883,11])).
% 63.08/63.09 cnf(916,plain,
% 63.08/63.09 (E(f1(a4),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[768,36,3,2])).
% 63.08/63.09 cnf(927,plain,
% 63.08/63.09 (E(f1(a4),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[916,765,3])).
% 63.08/63.09 cnf(931,plain,
% 63.08/63.09 (P2(f3(f3(a5)),f3(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[786,788,21])).
% 63.08/63.09 cnf(933,plain,
% 63.08/63.09 (~E(f3(f3(a5)),a4)),
% 63.08/63.09 inference(scs_inference,[],[786,341,788,21,11])).
% 63.08/63.09 cnf(938,plain,
% 63.08/63.09 (~P2(f3(f3(a5)),f2(f3(a4),a4))),
% 63.08/63.09 inference(scs_inference,[],[355,931,11,20])).
% 63.08/63.09 cnf(970,plain,
% 63.08/63.09 (E(f3(f3(a5)),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[793,927,3])).
% 63.08/63.09 cnf(971,plain,
% 63.08/63.09 (E(f1(f3(a5)),f3(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[793,927,3,2])).
% 63.08/63.09 cnf(973,plain,
% 63.08/63.09 (E(f3(f3(a5)),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[793,916,3])).
% 63.08/63.09 cnf(974,plain,
% 63.08/63.09 (E(f1(f1(a4)),f3(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[793,916,3,2])).
% 63.08/63.09 cnf(986,plain,
% 63.08/63.09 (E(f3(f1(a4)),f1(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[971,786,3,2])).
% 63.08/63.09 cnf(989,plain,
% 63.08/63.09 (E(f3(f1(a4)),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[974,786,3,2])).
% 63.08/63.09 cnf(1016,plain,
% 63.08/63.09 (~E(f2(f3(f2(a4,a5)),f2(a4,a5)),f1(a5))),
% 63.08/63.09 inference(scs_inference,[],[874,110,11])).
% 63.08/63.09 cnf(1023,plain,
% 63.08/63.09 (~E(f2(a4,f1(a4)),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[886,473,11])).
% 63.08/63.09 cnf(1024,plain,
% 63.08/63.09 (~P2(f2(a4,f1(a4)),f1(f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[886,473,11,20])).
% 63.08/63.09 cnf(1027,plain,
% 63.08/63.09 (~P2(f1(f3(a5)),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[1024,883,11,20])).
% 63.08/63.09 cnf(1032,plain,
% 63.08/63.09 (~P2(f1(f1(a4)),f2(a4,f1(a4)))),
% 63.08/63.09 inference(scs_inference,[],[886,1027,883,211,12,11,20])).
% 63.08/63.09 cnf(1097,plain,
% 63.08/63.09 (~E(f2(a4,f1(a4)),f3(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[938,473,11])).
% 63.08/63.09 cnf(1098,plain,
% 63.08/63.09 (~P2(f2(a4,f1(a4)),f3(f3(a5)))),
% 63.08/63.09 inference(scs_inference,[],[938,473,11,20])).
% 63.08/63.09 cnf(1229,plain,
% 63.08/63.09 (E(f3(x12291),f3(f2(x12291,f1(x12291))))),
% 63.08/63.09 inference(scs_inference,[],[13,7,2])).
% 63.08/63.09 cnf(1230,plain,
% 63.08/63.09 (E(f3(f2(x12301,f1(x12301))),f3(x12301))),
% 63.08/63.09 inference(scs_inference,[],[1229,2])).
% 63.08/63.09 cnf(1253,plain,
% 63.08/63.09 (E(f3(x12531),f3(f2(f3(x12531),x12531)))),
% 63.08/63.09 inference(scs_inference,[],[14,7,2])).
% 63.08/63.09 cnf(1255,plain,
% 63.08/63.09 (P1(f3(f2(f3(a5),a5)))),
% 63.08/63.09 inference(scs_inference,[],[1253,156,2,10])).
% 63.08/63.09 cnf(1275,plain,
% 63.08/63.09 (P2(f3(a5),f2(f3(a5),f1(f3(a5))))),
% 63.08/63.09 inference(scs_inference,[],[34,156,21])).
% 63.08/63.09 cnf(1278,plain,
% 63.08/63.09 (P1(f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[1275,133])).
% 63.08/63.09 cnf(1331,plain,
% 63.08/63.09 (E(f1(a4),f3(f2(a5,f1(a5))))),
% 63.08/63.09 inference(scs_inference,[],[48,1229,3])).
% 63.08/63.09 cnf(1333,plain,
% 63.08/63.09 (E(f3(f2(a5,f1(a5))),f1(a4))),
% 63.08/63.09 inference(scs_inference,[],[48,1229,3,2])).
% 63.08/63.09 cnf(1335,plain,
% 63.08/63.09 (E(f1(a4),f3(f2(f3(a5),a5)))),
% 63.08/63.09 inference(scs_inference,[],[48,1253,3])).
% 63.08/63.10 cnf(1337,plain,
% 63.08/63.10 (E(f3(f2(f3(a5),a5)),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[48,1253,3,2])).
% 63.08/63.10 cnf(1403,plain,
% 63.08/63.10 (P1(f6(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[877,25])).
% 63.08/63.10 cnf(1411,plain,
% 63.08/63.10 (~P1(f3(f2(f2(a4,a5),f1(a5))))),
% 63.08/63.10 inference(scs_inference,[],[877,749,352,330,625,25,7,6,8,9,31,19])).
% 63.08/63.10 cnf(1413,plain,
% 63.08/63.10 (~P1(f1(f2(f2(a4,a5),f1(a5))))),
% 63.08/63.10 inference(scs_inference,[],[877,749,352,330,625,25,7,6,8,9,31,19,18])).
% 63.08/63.10 cnf(1421,plain,
% 63.08/63.10 (P1(f6(f2(a4,f1(a4)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[877,749,585,425,707,352,330,625,25,7,6,8,9,31,19,18,4,28,5,29,22])).
% 63.08/63.10 cnf(1423,plain,
% 63.08/63.10 (~E(f2(f2(a4,a5),f1(a5)),f1(a5))),
% 63.08/63.10 inference(scs_inference,[],[877,812,749,585,425,707,352,330,625,25,7,6,8,9,31,19,18,4,28,5,29,22,2])).
% 63.08/63.10 cnf(1427,plain,
% 63.08/63.10 (~E(f1(f3(f1(a5))),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[877,1278,808,812,749,585,425,1333,707,859,352,330,625,25,7,6,8,9,31,19,18,4,28,5,29,22,2,30,10,3])).
% 63.08/63.10 cnf(1428,plain,
% 63.08/63.10 (~P1(f2(f2(a4,a5),f3(f1(a5))))),
% 63.08/63.10 inference(scs_inference,[],[877,1278,808,812,749,585,425,1333,657,707,859,352,330,626,625,25,7,6,8,9,31,19,18,4,28,5,29,22,2,30,10,3,21])).
% 63.08/63.10 cnf(1438,plain,
% 63.08/63.10 (P1(f6(f1(a5),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[873,25])).
% 63.08/63.10 cnf(1440,plain,
% 63.08/63.10 (E(f6(x14401,f3(a5)),f6(x14401,f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[873,36,25,9])).
% 63.08/63.10 cnf(1441,plain,
% 63.08/63.10 (E(f6(f3(a5),x14411),f6(f1(a4),x14411))),
% 63.08/63.10 inference(scs_inference,[],[873,36,25,9,8])).
% 63.08/63.10 cnf(1444,plain,
% 63.08/63.10 (E(f2(x14441,f3(a5)),f2(x14441,f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[873,1403,36,25,9,8,31,6])).
% 63.08/63.10 cnf(1446,plain,
% 63.08/63.10 (E(f2(f3(a5),x14461),f2(f1(a4),x14461))),
% 63.08/63.10 inference(scs_inference,[],[873,1403,36,13,25,9,8,31,6,4,5])).
% 63.08/63.10 cnf(1447,plain,
% 63.08/63.10 (P1(f1(f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[873,1403,856,36,13,25,9,8,31,6,4,5,28])).
% 63.08/63.10 cnf(1451,plain,
% 63.08/63.10 (~E(f2(f2(a4,a5),f1(a5)),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[873,797,1403,856,109,36,13,25,9,8,31,6,4,5,28,29,2])).
% 63.08/63.10 cnf(1455,plain,
% 63.08/63.10 (~E(f3(f3(a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[873,797,1403,1337,1411,395,856,737,789,109,36,13,25,9,8,31,6,4,5,28,29,2,30,10,3])).
% 63.08/63.10 cnf(1459,plain,
% 63.08/63.10 (~P2(f1(a4),f2(a4,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[873,551,797,1403,1337,1255,1411,395,271,856,737,789,109,36,13,25,9,8,31,6,4,5,28,29,2,30,10,3,21,11,12])).
% 63.08/63.10 cnf(1462,plain,
% 63.08/63.10 (P1(f6(f2(a4,f1(a4)),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[494,25])).
% 63.08/63.10 cnf(1466,plain,
% 63.08/63.10 (E(f6(x14661,f1(a4)),f6(x14661,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[494,1438,48,25,31,9])).
% 63.08/63.10 cnf(1467,plain,
% 63.08/63.10 (E(f2(x14671,f1(a4)),f2(x14671,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[494,1438,48,25,31,9,6])).
% 63.08/63.10 cnf(1468,plain,
% 63.08/63.10 (E(f6(f1(a4),x14681),f6(f3(a5),x14681))),
% 63.08/63.10 inference(scs_inference,[],[494,1438,48,25,31,9,6,8])).
% 63.08/63.10 cnf(1474,plain,
% 63.08/63.10 (E(f2(f1(a4),x14741),f2(f3(a5),x14741))),
% 63.08/63.10 inference(scs_inference,[],[494,1438,109,189,48,14,25,31,9,6,8,4,29,28,5])).
% 63.08/63.10 cnf(1475,plain,
% 63.08/63.10 (~E(f2(f2(a4,a5),f1(a5)),a4)),
% 63.08/63.10 inference(scs_inference,[],[494,820,1438,109,189,48,14,25,31,9,6,8,4,29,28,5,2])).
% 63.08/63.10 cnf(1476,plain,
% 63.08/63.10 (P1(f2(f1(a4),a5))),
% 63.08/63.10 inference(scs_inference,[],[494,820,1438,769,109,189,766,48,14,25,31,9,6,8,4,29,28,5,2,30])).
% 63.08/63.10 cnf(1478,plain,
% 63.08/63.10 (~E(f6(f1(a5),f2(a4,a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[494,820,1438,769,109,189,766,48,14,625,25,31,9,6,8,4,29,28,5,2,30,10])).
% 63.08/63.10 cnf(1479,plain,
% 63.08/63.10 (~E(f1(a4),f2(a4,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[494,820,1438,1459,423,769,109,189,766,48,14,625,25,31,9,6,8,4,29,28,5,2,30,10,21])).
% 63.08/63.10 cnf(1481,plain,
% 63.08/63.10 (~E(f2(a4,f2(a5,f1(a5))),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[494,1451,820,1438,1459,423,16,769,109,189,766,48,14,625,25,31,9,6,8,4,29,28,5,2,30,10,21,3])).
% 63.08/63.10 cnf(1483,plain,
% 63.08/63.10 (~P2(f2(f3(f1(a4)),f3(a5)),a4)),
% 63.08/63.10 inference(scs_inference,[],[494,1451,820,1438,1459,274,1444,423,16,769,109,189,766,48,14,625,25,31,9,6,8,4,29,28,5,2,30,10,21,3,11])).
% 63.08/63.10 cnf(1484,plain,
% 63.08/63.10 (E(f2(x14841,f3(a5)),f2(x14841,f1(a4)))),
% 63.08/63.10 inference(rename_variables,[],[1444])).
% 63.08/63.10 cnf(1485,plain,
% 63.08/63.10 (~P2(a4,f2(f3(f1(a4)),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[494,1451,820,1438,1459,249,274,1444,1484,423,16,769,109,189,766,48,14,625,25,31,9,6,8,4,29,28,5,2,30,10,21,3,11,12])).
% 63.08/63.10 cnf(1487,plain,
% 63.08/63.10 (P1(f6(f2(a5,f1(a5)),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[490,25])).
% 63.08/63.10 cnf(1491,plain,
% 63.08/63.10 (E(f2(x14911,f2(x14912,f1(x14912))),f2(x14911,x14912))),
% 63.08/63.10 inference(scs_inference,[],[490,1447,13,25,31,6])).
% 63.08/63.10 cnf(1492,plain,
% 63.08/63.10 (E(f6(f2(x14921,f1(x14921)),x14922),f6(x14921,x14922))),
% 63.08/63.10 inference(scs_inference,[],[490,1447,13,25,31,6,8])).
% 63.08/63.10 cnf(1494,plain,
% 63.08/63.10 (E(f1(x14941),f1(f2(x14941,f1(x14941))))),
% 63.08/63.10 inference(scs_inference,[],[490,1447,13,34,25,31,6,8,9,4])).
% 63.08/63.10 cnf(1495,plain,
% 63.08/63.10 (E(f2(f2(x14951,f1(x14951)),x14952),f2(x14951,x14952))),
% 63.08/63.10 inference(scs_inference,[],[490,1447,13,34,25,31,6,8,9,4,5])).
% 63.08/63.10 cnf(1498,plain,
% 63.08/63.10 (~E(f2(f2(a4,a5),f1(a5)),a5)),
% 63.08/63.10 inference(scs_inference,[],[490,822,1447,189,13,34,25,31,6,8,9,4,5,28,2])).
% 63.08/63.10 cnf(1499,plain,
% 63.08/63.10 (P1(f2(f3(a5),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[490,822,1447,970,189,431,13,34,25,31,6,8,9,4,5,28,2,30])).
% 63.08/63.10 cnf(1505,plain,
% 63.08/63.10 (~E(f6(a4,f1(a4)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[490,822,1447,1440,1441,1413,702,699,395,970,189,431,13,34,25,31,6,8,9,4,5,28,2,30,10,21,3])).
% 63.08/63.10 cnf(1511,plain,
% 63.08/63.10 (P1(f6(f1(a4),a4))),
% 63.08/63.10 inference(scs_inference,[],[490,822,1447,307,1440,1441,1446,1467,240,1413,702,699,395,970,189,431,13,34,25,31,6,8,9,4,5,28,2,30,10,21,3,11,12,22])).
% 63.08/63.10 cnf(1515,plain,
% 63.08/63.10 (P1(f6(f2(f2(a4,a5),f1(a5)),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1423,25])).
% 63.08/63.10 cnf(1521,plain,
% 63.08/63.10 (E(f2(x15211,f2(f3(x15212),x15212)),f2(x15211,x15212))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,14,25,31,9,8,6])).
% 63.08/63.10 cnf(1523,plain,
% 63.08/63.10 (E(f2(f2(f3(x15231),x15231),x15232),f2(x15231,x15232))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,14,108,25,31,9,8,6,4,5])).
% 63.08/63.10 cnf(1524,plain,
% 63.08/63.10 (~E(f2(a4,f3(a5)),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,1479,14,108,25,31,9,8,6,4,5,2])).
% 63.08/63.10 cnf(1525,plain,
% 63.08/63.10 (P1(f2(f1(a4),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,1479,973,766,14,108,25,31,9,8,6,4,5,2,30])).
% 63.08/63.10 cnf(1528,plain,
% 63.08/63.10 (~E(a4,f2(f3(f1(a4)),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,1479,1485,179,973,766,14,625,108,25,31,9,8,6,4,5,2,30,10,21])).
% 63.08/63.10 cnf(1530,plain,
% 63.08/63.10 (~E(f2(a4,f2(a5,f1(a5))),f1(a5))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,1479,1485,179,973,16,766,14,625,108,25,31,9,8,6,4,5,2,30,10,21,3])).
% 63.08/63.10 cnf(1532,plain,
% 63.08/63.10 (~P2(f2(f1(a4),a5),f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,1479,1474,1485,284,179,973,16,766,14,625,108,25,31,9,8,6,4,5,2,30,10,21,3,11])).
% 63.08/63.10 cnf(1536,plain,
% 63.08/63.10 (E(f6(f2(f2(a4,a5),f1(a5)),f1(a5)),f2(f2(a4,a5),f1(a5)))+E(f6(f2(f2(a4,a5),f1(a5)),f1(a5)),f1(a5))),
% 63.08/63.10 inference(scs_inference,[],[1423,1511,1479,1474,1485,1483,284,179,973,16,766,13,14,625,108,25,31,9,8,6,4,5,2,30,10,21,3,11,12,26])).
% 63.08/63.10 cnf(1540,plain,
% 63.08/63.10 (P1(f6(f2(a4,f3(a5)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1524,25])).
% 63.08/63.10 cnf(1544,plain,
% 63.08/63.10 (E(f2(x15441,x15442),f2(x15441,f2(x15442,f1(x15442))))),
% 63.08/63.10 inference(scs_inference,[],[1524,1525,34,25,31,6])).
% 63.08/63.10 cnf(1547,plain,
% 63.08/63.10 (E(f2(x15471,x15472),f2(f2(x15471,f1(x15471)),x15472))),
% 63.08/63.10 inference(scs_inference,[],[1524,1525,34,25,31,6,9,8,5])).
% 63.08/63.10 cnf(1549,plain,
% 63.08/63.10 (P1(f2(f3(a5),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1524,1525,634,986,431,34,25,31,6,9,8,5,2,30])).
% 63.08/63.10 cnf(1555,plain,
% 63.08/63.10 (~E(f2(a4,a5),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[1524,1525,634,1468,1491,1481,1411,1511,986,179,431,34,25,31,6,9,8,5,2,30,10,21,3])).
% 63.08/63.10 cnf(1556,plain,
% 63.08/63.10 (E(f2(x15561,f2(x15562,f1(x15562))),f2(x15561,x15562))),
% 63.08/63.10 inference(rename_variables,[],[1491])).
% 63.08/63.10 cnf(1559,plain,
% 63.08/63.10 (~P2(f1(f1(a4)),f2(a4,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1524,1525,634,1032,1468,1491,1556,1481,878,1444,1411,1511,986,179,431,34,25,31,6,9,8,5,2,30,10,21,3,11,12])).
% 63.08/63.10 cnf(1561,plain,
% 63.08/63.10 (P1(f6(f2(a4,a5),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1555,25])).
% 63.08/63.10 cnf(1565,plain,
% 63.08/63.10 (E(f6(x15651,x15652),f6(f2(f3(x15651),x15651),x15652))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,108,25,31,8])).
% 63.08/63.10 cnf(1567,plain,
% 63.08/63.10 (E(f2(x15671,x15672),f2(x15671,f2(f3(x15672),x15672)))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,108,25,31,8,9,6])).
% 63.08/63.10 cnf(1568,plain,
% 63.08/63.10 (E(f2(x15681,x15682),f2(f2(f3(x15681),x15681),x15682))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,108,25,31,8,9,6,5])).
% 63.08/63.10 cnf(1569,plain,
% 63.08/63.10 (~E(f1(a4),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,108,25,31,8,9,6,5,2])).
% 63.08/63.10 cnf(1570,plain,
% 63.08/63.10 (P1(f2(f1(a4),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,989,766,108,25,31,8,9,6,5,2,30])).
% 63.08/63.10 cnf(1572,plain,
% 63.08/63.10 (~E(f1(f1(a4)),f2(a4,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,1559,989,766,108,25,31,8,9,6,5,2,30,21])).
% 63.08/63.10 cnf(1578,plain,
% 63.08/63.10 (~P2(f1(f1(a4)),f2(f2(a4,f1(a4)),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1555,1549,1559,1528,1495,499,1467,989,766,108,25,31,8,9,6,5,2,30,21,3,11,12])).
% 63.08/63.10 cnf(1580,plain,
% 63.08/63.10 (P1(f6(f1(a4),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[1569,25])).
% 63.08/63.10 cnf(1585,plain,
% 63.08/63.10 (P1(f2(a4,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1569,1561,644,423,793,25,31,2,30])).
% 63.08/63.10 cnf(1589,plain,
% 63.08/63.10 (E(f6(x15891,f1(a4)),f6(x15891,f3(a5)))),
% 63.08/63.10 inference(rename_variables,[],[1466])).
% 63.08/63.10 cnf(1591,plain,
% 63.08/63.10 (E(f6(f2(x15911,f1(x15911)),f1(a4)),f6(x15911,f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1569,1561,644,1466,1589,1492,1413,423,737,793,25,31,2,30,10,21,3])).
% 63.08/63.10 cnf(1597,plain,
% 63.08/63.10 (P1(f6(f2(a4,a5),f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1569,1561,644,1466,1589,1492,1521,267,253,1474,1413,423,737,793,25,31,2,30,10,21,3,11,12,22])).
% 63.08/63.10 cnf(1604,plain,
% 63.08/63.10 (~E(f2(a4,f3(a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[933,1585,832,625,25,31,2,10])).
% 63.08/63.10 cnf(1607,plain,
% 63.08/63.10 (~E(f1(f2(a5,f1(a5))),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[933,1585,832,1532,1494,1476,873,625,25,31,2,10,21,3])).
% 63.08/63.10 cnf(1609,plain,
% 63.08/63.10 (~P2(f2(a4,f3(a5)),f1(f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[933,1585,662,832,1532,1494,1476,873,1444,625,25,31,2,10,21,3,11])).
% 63.08/63.10 cnf(1622,plain,
% 63.08/63.10 (~P1(f2(f2(f3(f2(a4,a5)),f2(a4,a5)),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1580,1498,838,1523,1428,190,626,25,31,2,10,21])).
% 63.08/63.10 cnf(1623,plain,
% 63.08/63.10 (E(f2(f2(f3(x16231),x16231),x16232),f2(x16231,x16232))),
% 63.08/63.10 inference(rename_variables,[],[1523])).
% 63.08/63.10 cnf(1630,plain,
% 63.08/63.10 (~P2(a4,f2(f3(f3(a5)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1580,1498,277,1098,838,1523,1623,1568,1428,190,1467,626,25,31,2,10,21,3,11,12])).
% 63.08/63.10 cnf(1639,plain,
% 63.08/63.10 (~E(f6(f2(a4,a5),f3(a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1597,1475,1604,625,25,31,2,10])).
% 63.08/63.10 cnf(1640,plain,
% 63.08/63.10 (~E(f2(a4,f3(a5)),f1(f3(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1597,1475,1604,1609,1585,625,25,31,2,10,21])).
% 63.08/63.10 cnf(1642,plain,
% 63.08/63.10 (~E(f3(f2(a5,f1(a5))),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1597,1475,1604,1609,1331,1569,1585,625,25,31,2,10,21,3])).
% 63.08/63.10 cnf(1656,plain,
% 63.08/63.10 (~E(f6(f2(a4,a5),f1(a4)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[834,1639,1421,1591,1622,1570,1440,1278,25,31,2,10,21,3])).
% 63.08/63.10 cnf(1658,plain,
% 63.08/63.10 (~P2(f2(a4,f1(a4)),f2(f3(f3(a5)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[834,1639,1421,1630,1591,1622,1570,1440,1278,13,25,31,2,10,21,3,11])).
% 63.08/63.10 cnf(1666,plain,
% 63.08/63.10 (~E(f6(f2(a5,f1(a5)),f2(a4,a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1016,1487,1656,1499,625,25,31,2,10])).
% 63.08/63.10 cnf(1669,plain,
% 63.08/63.10 (~E(f3(a5),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1016,1487,1656,1642,1658,1499,1230,333,625,25,31,2,10,21,3])).
% 63.08/63.10 cnf(1673,plain,
% 63.08/63.10 (~P2(f2(a4,a5),f2(f2(a5,f1(a5)),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1016,1487,1656,1642,1658,393,1499,325,1495,1474,1230,333,625,25,31,2,10,21,3,11,12])).
% 63.08/63.10 cnf(1680,plain,
% 63.08/63.10 (P1(f6(f3(a5),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[1669,698,31,25])).
% 63.08/63.10 cnf(1686,plain,
% 63.08/63.10 (~E(f6(a5,f2(a4,a5)),f2(f2(a4,a5),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1669,1666,1335,698,1492,1622,395,571,31,25,2,10,21,3])).
% 63.08/63.10 cnf(1690,plain,
% 63.08/63.10 (~P2(f2(a4,a5),f2(a5,f2(f1(a5),f1(a5))))),
% 63.08/63.10 inference(scs_inference,[],[1669,1673,1666,1335,89,698,1485,1492,1622,395,571,13,31,25,2,10,21,3,11,12])).
% 63.08/63.10 cnf(1718,plain,
% 63.08/63.10 (~P2(f2(f2(f3(a5),a5),f1(a5)),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1686,1565,323,491,1441,1523,1476,1680,1622,737,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1730,plain,
% 63.08/63.10 (~P2(f2(f3(a5),f2(a5,f1(a5))),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1718,1023,1478,1462,1578,1547,340,89,570,766,625,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1739,plain,
% 63.08/63.10 (P1(f6(f3(f1(a5)),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[808,693,31,25])).
% 63.08/63.10 cnf(1756,plain,
% 63.08/63.10 (P1(f6(f2(f2(a4,a5),f1(a5)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1451,702,31,25])).
% 63.08/63.10 cnf(1764,plain,
% 63.08/63.10 (~P2(f2(f1(a4),f2(a5,f1(a5))),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1739,1455,1730,1690,1567,1451,877,702,1474,15,625,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1777,plain,
% 63.08/63.10 (~P2(f2(f1(a4),a5),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1640,1505,1764,518,1580,1468,1544,1565,1428,568,179,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1779,plain,
% 63.08/63.10 (~P2(f3(a5),f2(f2(a4,f1(a4)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1640,1505,1764,518,519,1580,1468,1544,1565,1495,1428,568,179,31,25,2,10,21,3,11,12])).
% 63.08/63.10 cnf(1786,plain,
% 63.08/63.10 (~E(f2(a4,f3(a5)),f1(f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1572,549,737,31,25,2])).
% 63.08/63.10 cnf(1788,plain,
% 63.08/63.10 (~E(f2(f1(a4),a5),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1777,1515,1572,549,1476,737,625,31,25,2,10,21])).
% 63.08/63.10 cnf(1792,plain,
% 63.08/63.10 (~P2(f2(f1(a4),f2(f3(a5),a5)),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1777,1097,1515,1572,549,1547,1521,1476,737,625,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1798,plain,
% 63.08/63.10 (E(f6(f2(f2(a4,a5),f1(a5)),f1(a5)),f1(a5))),
% 63.08/63.10 inference(scs_inference,[],[1777,1097,1515,1779,1572,510,549,1547,1521,89,1476,737,625,31,25,2,10,21,3,11,12,26,1536])).
% 63.08/63.10 cnf(1801,plain,
% 63.08/63.10 (P1(f6(f2(f1(a4),a5),f2(a4,a5)))),
% 63.08/63.10 inference(scs_inference,[],[1788,788,31,25])).
% 63.08/63.10 cnf(1803,plain,
% 63.08/63.10 (~E(f2(a4,a5),f2(f1(a4),a5))),
% 63.08/63.10 inference(scs_inference,[],[1788,788,31,25,2])).
% 63.08/63.10 cnf(1807,plain,
% 63.08/63.10 (~E(f2(f1(a4),f2(f3(a5),a5)),f2(a4,a5))),
% 63.08/63.10 inference(scs_inference,[],[1788,1798,1756,1515,1567,788,625,31,25,2,10,21,3])).
% 63.08/63.10 cnf(1809,plain,
% 63.08/63.10 (~P2(f2(f2(f3(a4),a4),f1(a4)),f3(a5))),
% 63.08/63.10 inference(scs_inference,[],[1788,1798,1756,495,1515,1567,1523,788,625,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1811,plain,
% 63.08/63.10 (~P2(f1(f2(a4,a5)),f6(f2(f2(a4,a5),f1(a5)),f1(a5)))),
% 63.08/63.10 inference(scs_inference,[],[1788,1798,1756,32,495,1515,1567,1523,788,625,31,25,2,10,21,3,11,12])).
% 63.08/63.10 cnf(1812,plain,
% 63.08/63.10 (E(f6(f2(f2(a4,a5),f1(a5)),f1(a4)),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[1788,1798,1756,32,495,1515,1567,1451,1523,788,625,31,25,2,10,21,3,11,12,26])).
% 63.08/63.10 cnf(1828,plain,
% 63.08/63.10 (~P2(f2(a4,f1(a4)),f6(f2(f2(a4,a5),f1(a5)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1803,1812,1786,1607,1792,1811,511,1568,1446,1411,568,571,431,31,25,2,10,21,3,11,12])).
% 63.08/63.10 cnf(1844,plain,
% 63.08/63.10 (~P2(f2(f3(a4),a4),f6(f2(f2(a4,a5),f1(a5)),f1(a4)))),
% 63.08/63.10 inference(scs_inference,[],[1801,1530,498,1828,790,1812,1756,166,1444,766,625,31,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1854,plain,
% 63.08/63.10 (~E(f2(f2(a4,f1(a4)),f3(a5)),f1(a4))),
% 63.08/63.10 inference(scs_inference,[],[1807,1844,1524,812,1547,1413,329,179,25,2,10,21,3])).
% 63.08/63.10 cnf(1856,plain,
% 63.08/63.10 (~P2(f2(f2(f3(a4),a4),f3(a5)),f3(a5))),
% 63.08/63.10 inference(scs_inference,[],[1809,1807,1844,1524,812,1547,1413,329,1444,179,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1867,plain,
% 63.08/63.10 (~P2(f2(a4,f3(a5)),f3(a5))),
% 63.08/63.10 inference(scs_inference,[],[1854,1856,1540,392,1331,1568,423,1446,625,25,2,10,21,3,11])).
% 63.08/63.10 cnf(1882,plain,
% 63.08/63.10 ($false),
% 63.08/63.10 inference(scs_inference,[],[1867,1427,892,817,1544,1428,89,1585,160,25,2,10,21,3]),
% 63.08/63.10 ['proof']).
% 63.08/63.10 % SZS output end Proof
% 63.08/63.10 % Total time :62.330000s
%------------------------------------------------------------------------------