%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT005-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 04:40:10 EDT 2024
% Result : Unsatisfiable 2.02s 2.21s
% Output : CNFRefutation 2.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : CAT005-3 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.32 % Computer : n020.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Tue Jun 18 12:31:54 EDT 2024
% 0.10/0.32 % CPUTime :
% 0.17/0.53 start to proof:theBenchmark
% 2.02/2.21 %-------------------------------------------
% 2.02/2.21 % File :CSE---1.7
% 2.02/2.21 % Problem :theBenchmark
% 2.02/2.21 % Transform :cnf
% 2.02/2.21 % Format :tptp:raw
% 2.02/2.21 % Command :java -jar mcs_scs.jar %d %s
% 2.02/2.21
% 2.02/2.21 % Result :Theorem 1.650000s
% 2.02/2.21 % Output :CNFRefutation 1.650000s
% 2.02/2.21 %-------------------------------------------
% 2.02/2.21 %--------------------------------------------------------------------------
% 2.02/2.21 % File : CAT005-3 : TPTP v8.2.0. Released v1.0.0.
% 2.02/2.21 % Domain : Category Theory
% 2.02/2.21 % Problem : Domain is the unique right identity
% 2.02/2.21 % Version : [Sco79] axioms : Reduced > Complete.
% 2.02/2.21 % English : domain(x) is the unique identity i such that xi is defined.
% 2.02/2.21
% 2.02/2.21 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 2.02/2.21 % Source : [ANL]
% 2.02/2.21 % Names : p5.ver3.in [ANL]
% 2.02/2.21
% 2.02/2.21 % Status : Unsatisfiable
% 2.02/2.21 % Rating : 0.10 v8.2.0, 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.21 v6.0.0, 0.10 v5.5.0, 0.25 v5.4.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.19 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.23 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.30 v2.5.0, 0.25 v2.4.0, 0.22 v2.3.0, 0.33 v2.2.0, 0.44 v2.1.0, 0.56 v2.0.0
% 2.02/2.21 % Syntax : Number of clauses : 21 ( 5 unt; 2 nHn; 16 RR)
% 2.02/2.21 % Number of literals : 43 ( 18 equ; 20 neg)
% 2.02/2.21 % Maximal clause size : 4 ( 2 avg)
% 2.02/2.21 % Maximal term depth : 3 ( 1 avg)
% 2.02/2.21 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 2.02/2.21 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 2.02/2.21 % Number of variables : 33 ( 4 sgn)
% 2.02/2.21 % SPC : CNF_UNS_RFO_SEQ_NHN
% 2.02/2.21
% 2.02/2.21 % Comments : Axioms simplified by Art Quaife.
% 2.02/2.21 %--------------------------------------------------------------------------
% 2.02/2.21 %----Include Scott's axioms for category theory
% 2.02/2.21 include('Axioms/CAT003-0.ax').
% 2.02/2.21 %--------------------------------------------------------------------------
% 2.02/2.21 %----Denial of the theorem: d is an identity not equal to dom(a),
% 2.02/2.21 cnf(ad_exists,hypothesis,
% 2.02/2.21 there_exists(compose(a,d)) ).
% 2.02/2.21
% 2.02/2.21 cnf(xd_equals_x,hypothesis,
% 2.02/2.21 ( ~ there_exists(compose(X,d))
% 2.02/2.21 | compose(X,d) = X ) ).
% 2.02/2.21
% 2.02/2.21 cnf(dy_equals_y,hypothesis,
% 2.02/2.21 ( ~ there_exists(compose(d,Y))
% 2.02/2.21 | compose(d,Y) = Y ) ).
% 2.02/2.21
% 2.02/2.21 cnf(prove_domain_of_a_is_d,negated_conjecture,
% 2.02/2.21 domain(a) != d ).
% 2.02/2.21
% 2.02/2.21 %--------------------------------------------------------------------------
% 2.02/2.21 %-------------------------------------------
% 2.02/2.21 % Proof found
% 2.02/2.21 % SZS status Theorem for theBenchmark
% 2.02/2.21 % SZS output start Proof
% 2.02/2.22 %ClaNum:32(EqnAxiom:12)
% 2.02/2.22 %VarNum:64(SingletonVarNum:29)
% 2.02/2.22 %MaxLitNum:3
% 2.02/2.22 %MaxfuncDepth:2
% 2.02/2.22 %SharedTerms:6
% 2.02/2.22 %goalClause: 17
% 2.02/2.22 %singleGoalClaCount:1
% 2.02/2.22 [15]P1(f2(a4,a5))
% 2.02/2.22 [17]~E(f1(a4),a5)
% 2.02/2.22 [13]E(f2(x131,f1(x131)),x131)
% 2.02/2.22 [14]E(f2(f3(x141),x141),x141)
% 2.02/2.22 [16]E(f2(f2(x161,x162),x163),f2(x161,f2(x162,x163)))
% 2.02/2.22 [18]P1(x181)+~P1(f1(x181))
% 2.02/2.22 [19]P1(x191)+~P1(f3(x191))
% 2.02/2.22 [28]E(f2(x281,a5),x281)+~P1(f2(x281,a5))
% 2.02/2.22 [29]E(f2(a5,x291),x291)+~P1(f2(a5,x291))
% 2.02/2.22 [20]~P2(x201,x202)+E(x201,x202)
% 2.02/2.22 [22]P1(x221)+~P2(x222,x221)
% 2.02/2.22 [23]P1(x231)+~P2(x231,x232)
% 2.02/2.22 [25]E(x251,x252)+P1(f6(x251,x252))
% 2.02/2.22 [27]E(f3(x271),f1(x272))+~P1(f2(x272,x271))
% 2.13/2.22 [30]P1(f1(x301))+~P1(f2(x301,x302))
% 2.13/2.22 [31]P1(f3(x311))+~P1(f2(x311,x312))
% 2.13/2.22 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 2.13/2.22 [26]E(x261,x262)+E(f6(x261,x262),x262)+E(f6(x261,x262),x261)
% 2.13/2.22 [32]~E(f3(x322),f1(x321))+~P1(f1(x321))+P1(f2(x321,x322))
% 2.13/2.22 %EqnAxiom
% 2.13/2.22 [1]E(x11,x11)
% 2.13/2.22 [2]E(x22,x21)+~E(x21,x22)
% 2.13/2.22 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.13/2.22 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 2.13/2.22 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 2.13/2.22 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 2.13/2.22 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 2.13/2.22 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 2.13/2.22 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 2.13/2.22 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 2.13/2.22 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 2.13/2.22 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 2.13/2.22
% 2.13/2.22 %-------------------------------------------
% 2.13/2.22 cnf(33,plain,
% 2.13/2.22 (~P1(x331)+P2(x331,x331)),
% 2.13/2.22 inference(equality_inference,[],[21])).
% 2.13/2.22 cnf(34,plain,
% 2.13/2.22 (~P2(f1(a4),a5)),
% 2.13/2.22 inference(scs_inference,[],[17,20])).
% 2.13/2.22 cnf(36,plain,
% 2.13/2.22 (E(x361,f2(x361,f1(x361)))),
% 2.13/2.22 inference(scs_inference,[],[17,13,20,2])).
% 2.13/2.22 cnf(37,plain,
% 2.13/2.22 (E(f3(a5),f1(a4))),
% 2.13/2.22 inference(scs_inference,[],[17,13,15,20,2,27])).
% 2.13/2.22 cnf(39,plain,
% 2.13/2.22 (E(f2(a4,a5),a4)),
% 2.13/2.22 inference(scs_inference,[],[17,13,15,20,2,27,28])).
% 2.13/2.22 cnf(41,plain,
% 2.13/2.22 (P2(f2(a4,a5),f2(f2(a4,a5),f1(f2(a4,a5))))),
% 2.13/2.22 inference(scs_inference,[],[17,13,15,20,2,27,28,21])).
% 2.13/2.22 cnf(43,plain,
% 2.13/2.22 (~E(f1(a4),f2(f3(a5),a5))),
% 2.13/2.22 inference(scs_inference,[],[17,13,14,15,20,2,27,28,21,3])).
% 2.13/2.22 cnf(45,plain,
% 2.13/2.22 (P1(f2(f2(a4,a5),f1(f2(a4,a5))))),
% 2.13/2.22 inference(scs_inference,[],[17,13,14,15,20,2,27,28,21,3,10])).
% 2.13/2.22 cnf(48,plain,
% 2.13/2.22 (P2(f2(f2(a4,a5),f1(f2(a4,a5))),f2(a4,a5))),
% 2.13/2.22 inference(scs_inference,[],[17,13,14,15,20,2,27,28,21,3,10,12,11])).
% 2.13/2.22 cnf(49,plain,
% 2.13/2.22 (~P2(f1(a4),f2(f3(a5),a5))),
% 2.13/2.22 inference(scs_inference,[],[43,20])).
% 2.13/2.22 cnf(51,plain,
% 2.13/2.22 (E(f1(a4),f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[43,37,20,2])).
% 2.13/2.22 cnf(52,plain,
% 2.13/2.22 (P1(a4)),
% 2.13/2.22 inference(scs_inference,[],[43,37,39,15,20,2,10])).
% 2.13/2.22 cnf(53,plain,
% 2.13/2.22 (E(f3(a5),f2(f1(a4),f1(f1(a4))))),
% 2.13/2.22 inference(scs_inference,[],[36,43,37,39,15,20,2,10,3])).
% 2.13/2.22 cnf(54,plain,
% 2.13/2.22 (E(x541,f2(x541,f1(x541)))),
% 2.13/2.22 inference(rename_variables,[],[36])).
% 2.13/2.22 cnf(55,plain,
% 2.13/2.22 (P2(a4,f2(a4,f1(a4)))),
% 2.13/2.22 inference(scs_inference,[],[36,54,43,37,39,15,20,2,10,3,21])).
% 2.13/2.22 cnf(60,plain,
% 2.13/2.22 (E(f2(f1(a4),f1(f1(a4))),f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[53,2])).
% 2.13/2.22 cnf(61,plain,
% 2.13/2.22 (E(f2(f3(f1(a4)),f1(a4)),f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[53,51,14,2,3])).
% 2.13/2.22 cnf(63,plain,
% 2.13/2.22 (~P1(f3(a5))+P1(f2(f1(a4),f1(f1(a4))))),
% 2.13/2.22 inference(scs_inference,[],[53,51,14,2,3,10])).
% 2.13/2.22 cnf(72,plain,
% 2.13/2.22 (~E(f2(a4,a5),f3(a5))+P1(f2(f1(a4),f1(f1(a4))))),
% 2.13/2.22 inference(scs_inference,[],[53,51,45,48,14,2,3,10,22,23,31,32,21,12])).
% 2.13/2.22 cnf(74,plain,
% 2.13/2.22 (E(f3(a5),f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.22 inference(scs_inference,[],[61,2])).
% 2.13/2.22 cnf(75,plain,
% 2.13/2.22 (E(f2(f2(a4,a5),f1(f2(a4,a5))),a4)),
% 2.13/2.22 inference(scs_inference,[],[61,39,13,2,3])).
% 2.13/2.22 cnf(77,plain,
% 2.13/2.22 (~P1(f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[60,61,39,13,2,3,10])).
% 2.13/2.22 cnf(78,plain,
% 2.13/2.22 (P1(f3(a5))+~E(f2(a4,a5),f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[60,61,39,13,2,3,10,72])).
% 2.13/2.22 cnf(79,plain,
% 2.13/2.22 (~P2(f2(f1(a4),f1(f1(a4))),x791)+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[60,61,39,13,2,3,10,72,23])).
% 2.13/2.22 cnf(81,plain,
% 2.13/2.22 (~P2(x811,f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[60,61,39,13,2,3,10,72,23,22])).
% 2.13/2.22 cnf(83,plain,
% 2.13/2.22 (~E(f2(a4,a5),f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[60,61,15,39,13,2,3,10,72,23,22,32,21])).
% 2.13/2.22 cnf(85,plain,
% 2.13/2.22 (~E(a4,f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[60,61,55,15,39,13,2,3,10,72,23,22,32,21,11])).
% 2.13/2.22 cnf(89,plain,
% 2.13/2.22 (P2(f2(a4,a5),a4)),
% 2.13/2.22 inference(scs_inference,[],[75,41,45,2,21,12])).
% 2.13/2.22 cnf(90,plain,
% 2.13/2.22 (P2(a4,f2(a4,a5))),
% 2.13/2.22 inference(scs_inference,[],[75,41,48,45,2,21,12,11])).
% 2.13/2.22 cnf(91,plain,
% 2.13/2.22 (E(f1(a4),f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.22 inference(scs_inference,[],[74,75,51,41,48,45,2,21,12,11,3])).
% 2.13/2.22 cnf(111,plain,
% 2.13/2.22 (E(f2(f3(f2(a4,a5)),f2(a4,a5)),a4)),
% 2.13/2.22 inference(scs_inference,[],[36,90,16,39,14,2,12,3])).
% 2.13/2.22 cnf(119,plain,
% 2.13/2.22 (~E(f2(a4,a5),f1(a4))+P1(f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.22 inference(scs_inference,[],[91,36,15,90,16,39,14,2,12,3,10,30,23,22,21])).
% 2.13/2.22 cnf(122,plain,
% 2.13/2.22 (E(a4,f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 2.13/2.22 inference(scs_inference,[],[111,2])).
% 2.13/2.22 cnf(123,plain,
% 2.13/2.22 (P1(f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 2.13/2.22 inference(scs_inference,[],[111,52,2,10])).
% 2.13/2.22 cnf(124,plain,
% 2.13/2.22 (~E(f1(a4),f2(a5,f1(a5)))),
% 2.13/2.22 inference(scs_inference,[],[17,111,52,13,2,10,3])).
% 2.13/2.22 cnf(126,plain,
% 2.13/2.22 (~P2(f1(a4),f2(a5,f1(a5)))),
% 2.13/2.22 inference(scs_inference,[],[17,111,52,13,2,10,3,20])).
% 2.13/2.22 cnf(128,plain,
% 2.13/2.22 (E(a4,f2(a4,a5))),
% 2.13/2.22 inference(scs_inference,[],[39,2])).
% 2.13/2.22 cnf(129,plain,
% 2.13/2.22 (~P1(f2(f3(f1(a4)),f1(a4)))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[61,39,2,10])).
% 2.13/2.22 cnf(130,plain,
% 2.13/2.22 (P1(f3(a5))+~E(f2(a4,a5),f1(a4))),
% 2.13/2.22 inference(scs_inference,[],[61,39,2,10,119])).
% 2.13/2.22 cnf(133,plain,
% 2.13/2.22 (~P2(f2(f3(f1(a4)),f1(a4)),x1331)+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[61,39,2,10,119,20,23])).
% 2.13/2.22 cnf(135,plain,
% 2.13/2.22 (~P2(x1351,f2(f3(f1(a4)),f1(a4)))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[61,39,2,10,119,20,23,22])).
% 2.13/2.22 cnf(139,plain,
% 2.13/2.22 (~E(f2(f2(a4,a5),f1(f2(a4,a5))),f1(a4))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[61,41,52,39,2,10,119,20,23,22,32,21,12])).
% 2.13/2.22 cnf(140,plain,
% 2.13/2.22 (~E(a4,f1(a4))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[61,91,41,52,39,2,10,119,20,23,22,32,21,12,3])).
% 2.13/2.22 cnf(141,plain,
% 2.13/2.22 (~E(f2(a4,a5),f2(f3(f1(a4)),f1(a4)))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[61,91,41,52,39,2,10,119,20,23,22,32,21,12,3,11])).
% 2.13/2.22 cnf(142,plain,
% 2.13/2.22 (E(x1421,f2(f3(x1421),x1421))),
% 2.13/2.22 inference(scs_inference,[],[14,2])).
% 2.13/2.22 cnf(144,plain,
% 2.13/2.22 (E(x1441,f2(x1441,f1(x1441)))),
% 2.13/2.22 inference(rename_variables,[],[36])).
% 2.13/2.22 cnf(147,plain,
% 2.13/2.22 (~P1(f1(a4))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[36,144,51,89,90,14,2,12,11,10])).
% 2.13/2.22 cnf(153,plain,
% 2.13/2.22 (~E(f2(f3(f2(a4,a5)),f2(a4,a5)),f1(a4))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[36,144,51,15,89,90,14,123,2,12,11,10,30,23,22,21])).
% 2.13/2.22 cnf(155,plain,
% 2.13/2.22 (~E(f2(f3(f2(a4,a5)),f2(a4,a5)),f3(a5))+P1(f3(a5))),
% 2.13/2.22 inference(scs_inference,[],[36,144,51,15,89,90,37,14,123,2,12,11,10,30,23,22,21,3])).
% 2.13/2.22 cnf(156,plain,
% 2.13/2.22 (~P1(f3(a5))+P1(f1(a4))),
% 2.13/2.22 inference(scs_inference,[],[37,10])).
% 2.13/2.22 cnf(157,plain,
% 2.13/2.22 (P1(f1(a4))+~E(f2(a4,a5),f1(a4))),
% 2.13/2.22 inference(scs_inference,[],[37,10,130])).
% 2.13/2.22 cnf(158,plain,
% 2.13/2.22 (P1(f1(a4))+~E(a4,f1(a4))),
% 2.13/2.22 inference(scs_inference,[],[37,10,130,140])).
% 2.13/2.22 cnf(159,plain,
% 2.13/2.22 (P1(f1(a4))+~E(f2(f3(f2(a4,a5)),f2(a4,a5)),f1(a4))),
% 2.13/2.22 inference(scs_inference,[],[37,10,130,140,153])).
% 2.13/2.22 cnf(160,plain,
% 2.13/2.22 (P1(f1(a4))+~E(f2(f3(f2(a4,a5)),f2(a4,a5)),f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155])).
% 2.13/2.23 cnf(161,plain,
% 2.13/2.23 (P1(f1(a4))+~P1(f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129])).
% 2.13/2.23 cnf(162,plain,
% 2.13/2.23 (P1(f1(a4))+~P2(f2(f3(f1(a4)),f1(a4)),x1621)),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133])).
% 2.13/2.23 cnf(163,plain,
% 2.13/2.23 (P1(f1(a4))+~P2(x1631,f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135])).
% 2.13/2.23 cnf(164,plain,
% 2.13/2.23 (P1(f1(a4))+~E(f2(f2(a4,a5),f1(f2(a4,a5))),f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135,139])).
% 2.13/2.23 cnf(165,plain,
% 2.13/2.23 (P1(f1(a4))+~E(f2(a4,a5),f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135,139,141])).
% 2.13/2.23 cnf(166,plain,
% 2.13/2.23 (P1(f1(a4))+~P2(f2(f1(a4),f1(f1(a4))),x1661)),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135,139,141,79])).
% 2.13/2.23 cnf(167,plain,
% 2.13/2.23 (P1(f1(a4))+~P2(x1671,f2(f1(a4),f1(f1(a4))))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135,139,141,79,81])).
% 2.13/2.23 cnf(168,plain,
% 2.13/2.23 (P1(f1(a4))+~E(f2(a4,a5),f2(f1(a4),f1(f1(a4))))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135,139,141,79,81,83])).
% 2.13/2.23 cnf(169,plain,
% 2.13/2.23 (P1(f1(a4))+~P1(f2(a5,x1691))),
% 2.13/2.23 inference(scs_inference,[],[37,10,130,140,153,155,129,133,135,139,141,79,81,83,31])).
% 2.13/2.23 cnf(180,plain,
% 2.13/2.23 (~E(a4,f2(f3(f1(a4)),f1(a4)))+P1(f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[37,52,10,130,140,153,155,129,133,135,139,141,79,81,83,31,85,78,77,20,23,22,32,21])).
% 2.13/2.23 cnf(185,plain,
% 2.13/2.23 (E(f2(x1851,f1(x1851)),x1851)),
% 2.13/2.23 inference(rename_variables,[],[13])).
% 2.13/2.23 cnf(190,plain,
% 2.13/2.23 (E(f3(f1(a4)),f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[13,185,128,55,15,12,3,2,10,27])).
% 2.13/2.23 cnf(197,plain,
% 2.13/2.23 (E(f2(a4,f1(a4)),f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 2.13/2.23 inference(scs_inference,[],[13,122,190,2,3])).
% 2.13/2.23 cnf(213,plain,
% 2.13/2.23 (P1(f3(f1(a4)))+~P1(f2(a5,x2131))),
% 2.13/2.23 inference(scs_inference,[],[13,122,190,2,3,10,157,158,159,160,168,180,161,162,163,164,165,166,167,169])).
% 2.13/2.23 cnf(228,plain,
% 2.13/2.23 (P1(f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[15,147,30])).
% 2.13/2.23 cnf(229,plain,
% 2.13/2.23 (P1(f2(f1(a4),f1(f1(a4))))),
% 2.13/2.23 inference(scs_inference,[],[228,63])).
% 2.13/2.23 cnf(231,plain,
% 2.13/2.23 (P1(f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[228,156])).
% 2.13/2.23 cnf(232,plain,
% 2.13/2.23 (P1(a5)),
% 2.13/2.23 inference(scs_inference,[],[228,19])).
% 2.13/2.23 cnf(237,plain,
% 2.13/2.23 (P2(f3(a5),f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[61,74,197,228,19,2,21,12])).
% 2.13/2.23 cnf(239,plain,
% 2.13/2.23 (E(f2(f3(a5),f1(f3(a5))),f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[13,61,74,197,37,228,19,2,21,12,11,3])).
% 2.13/2.23 cnf(260,plain,
% 2.13/2.23 (P2(f2(f1(a4),f1(f1(a4))),f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[13,239,229,2,21])).
% 2.13/2.23 cnf(264,plain,
% 2.13/2.23 (P2(f2(f1(a4),f1(f1(a4))),f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[13,53,239,229,237,2,21,12,11])).
% 2.13/2.23 cnf(265,plain,
% 2.13/2.23 (P1(f2(f3(a5),f1(f3(a5))))),
% 2.13/2.23 inference(scs_inference,[],[13,53,239,229,231,237,2,21,12,11,10])).
% 2.13/2.23 cnf(274,plain,
% 2.13/2.23 (P2(f2(f3(a5),f1(f3(a5))),f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[13,265,21])).
% 2.13/2.23 cnf(283,plain,
% 2.13/2.23 (P2(a5,f2(a5,f1(a5)))),
% 2.13/2.23 inference(scs_inference,[],[36,232,21])).
% 2.13/2.23 cnf(287,plain,
% 2.13/2.23 (E(f2(x2871,f1(x2871)),x2871)),
% 2.13/2.23 inference(rename_variables,[],[13])).
% 2.13/2.23 cnf(288,plain,
% 2.13/2.23 (P2(f1(a4),f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[13,287,36,264,232,21,12,11])).
% 2.13/2.23 cnf(290,plain,
% 2.13/2.23 (~E(a5,f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[126,283,11])).
% 2.13/2.23 cnf(292,plain,
% 2.13/2.23 (~E(a5,f2(f3(a5),f1(f3(a5))))),
% 2.13/2.23 inference(scs_inference,[],[34,126,239,283,288,11,12,3])).
% 2.13/2.23 cnf(293,plain,
% 2.13/2.23 (~P2(a5,f1(a4))),
% 2.13/2.23 inference(scs_inference,[],[34,126,239,283,288,11,12,3,20])).
% 2.13/2.23 cnf(299,plain,
% 2.13/2.23 (~E(a5,f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[293,292,260,283,37,290,20,11,12,3])).
% 2.13/2.23 cnf(303,plain,
% 2.13/2.23 (~E(f3(a5),f2(f3(a5),a5))),
% 2.13/2.23 inference(scs_inference,[],[49,299,274,288,20,11,12])).
% 2.13/2.23 cnf(384,plain,
% 2.13/2.23 (P2(f3(f1(a4)),f3(f1(a4)))+~P1(f2(a5,x3841))),
% 2.13/2.23 inference(scs_inference,[],[213,33])).
% 2.13/2.23 cnf(485,plain,
% 2.13/2.23 (E(x4851,f2(x4851,f1(x4851)))),
% 2.13/2.23 inference(rename_variables,[],[36])).
% 2.13/2.23 cnf(490,plain,
% 2.13/2.23 (E(f3(f1(a5)),f1(a5))),
% 2.13/2.23 inference(scs_inference,[],[232,36,10,384,29,27])).
% 2.13/2.23 cnf(492,plain,
% 2.13/2.23 (E(f1(a5),f2(a5,f1(a5)))),
% 2.13/2.23 inference(scs_inference,[],[232,36,10,384,29,27,2])).
% 2.13/2.23 cnf(493,plain,
% 2.13/2.23 (E(a5,f1(a5))),
% 2.13/2.23 inference(scs_inference,[],[232,36,485,10,384,29,27,2,3])).
% 2.13/2.23 cnf(505,plain,
% 2.13/2.23 (~E(f1(a4),f1(a5))),
% 2.13/2.23 inference(scs_inference,[],[232,124,142,492,493,2,10,3])).
% 2.13/2.23 cnf(506,plain,
% 2.13/2.23 (~E(a4,a5)),
% 2.13/2.23 inference(scs_inference,[],[232,124,142,492,493,2,10,3,4])).
% 2.13/2.23 cnf(507,plain,
% 2.13/2.23 (E(f2(f3(a5),a5),f3(a5))),
% 2.13/2.23 inference(scs_inference,[],[232,124,142,492,493,2,10,3,4,28])).
% 2.13/2.23 cnf(517,plain,
% 2.13/2.23 (~E(f1(a4),f3(f1(a5)))),
% 2.13/2.23 inference(scs_inference,[],[232,505,493,490,506,20,2,10,3])).
% 2.13/2.23 cnf(525,plain,
% 2.13/2.23 ($false),
% 2.13/2.23 inference(scs_inference,[],[517,303,507,20,2]),
% 2.13/2.23 ['proof']).
% 2.13/2.23 % SZS output end Proof
% 2.13/2.23 % Total time :1.650000s
%------------------------------------------------------------------------------