%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT006-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 : n021.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:11 EDT 2024
% Result : Unsatisfiable 0.81s 0.88s
% Output : CNFRefutation 0.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : CAT006-3 : TPTP v8.2.0. Released v1.0.0.
% 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n021.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jun 18 12:15:39 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.18/0.59 start to proof:theBenchmark
% 0.81/0.88 %-------------------------------------------
% 0.81/0.88 % File :CSE---1.7
% 0.81/0.88 % Problem :theBenchmark
% 0.81/0.88 % Transform :cnf
% 0.81/0.88 % Format :tptp:raw
% 0.81/0.88 % Command :java -jar mcs_scs.jar %d %s
% 0.81/0.88
% 0.81/0.88 % Result :Theorem 0.250000s
% 0.81/0.88 % Output :CNFRefutation 0.250000s
% 0.81/0.88 %-------------------------------------------
% 0.81/0.88 %--------------------------------------------------------------------------
% 0.81/0.88 % File : CAT006-3 : TPTP v8.2.0. Released v1.0.0.
% 0.81/0.88 % Domain : Category Theory
% 0.81/0.88 % Problem : Codomain is the unique left identity
% 0.81/0.88 % Version : [Sco79] axioms : Reduced > Complete.
% 0.81/0.88 % English : codomain(x) is the unique identity j such that jx is defined.
% 0.81/0.88
% 0.81/0.88 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 0.81/0.88 % Source : [ANL]
% 0.81/0.88 % Names : p6.ver3.in [ANL]
% 0.81/0.88
% 0.81/0.88 % Status : Unsatisfiable
% 0.81/0.88 % Rating : 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.07 v6.4.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.12 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.15 v3.1.0, 0.27 v2.7.0, 0.17 v2.6.0, 0.30 v2.5.0, 0.17 v2.4.0, 0.22 v2.3.0, 0.33 v2.2.1, 0.44 v2.2.0, 0.56 v2.1.0, 0.56 v2.0.0
% 0.81/0.88 % Syntax : Number of clauses : 21 ( 5 unt; 2 nHn; 16 RR)
% 0.81/0.88 % Number of literals : 43 ( 18 equ; 20 neg)
% 0.81/0.88 % Maximal clause size : 4 ( 2 avg)
% 0.81/0.88 % Maximal term depth : 3 ( 1 avg)
% 0.81/0.88 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 0.81/0.88 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 0.81/0.88 % Number of variables : 33 ( 4 sgn)
% 0.81/0.88 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.81/0.88
% 0.81/0.88 % Comments : Axioms simplified by Art Quaife.
% 0.81/0.88 %--------------------------------------------------------------------------
% 0.81/0.88 %----Include Scott's axioms for category theory
% 0.81/0.88 include('Axioms/CAT003-0.ax').
% 0.81/0.88 %--------------------------------------------------------------------------
% 0.81/0.88 %----Denial of theorem: d is an identity which is not cod(a),
% 0.81/0.88 cnf(da_exists,hypothesis,
% 0.81/0.88 there_exists(compose(d,a)) ).
% 0.81/0.88
% 0.81/0.88 cnf(xd_equals_x,hypothesis,
% 0.81/0.88 ( ~ there_exists(compose(X,d))
% 0.81/0.88 | compose(X,d) = X ) ).
% 0.81/0.88
% 0.81/0.88 cnf(dx_equals_x,hypothesis,
% 0.81/0.88 ( ~ there_exists(compose(d,X))
% 0.81/0.88 | compose(d,X) = X ) ).
% 0.81/0.88
% 0.81/0.88 cnf(prove_codomain_of_a_is_d,negated_conjecture,
% 0.81/0.88 codomain(a) != d ).
% 0.81/0.88
% 0.81/0.88 %--------------------------------------------------------------------------
% 0.81/0.88 %-------------------------------------------
% 0.81/0.88 % Proof found
% 0.81/0.88 % SZS status Theorem for theBenchmark
% 0.81/0.88 % SZS output start Proof
% 0.81/0.89 %ClaNum:32(EqnAxiom:12)
% 0.81/0.89 %VarNum:64(SingletonVarNum:29)
% 0.81/0.89 %MaxLitNum:3
% 0.81/0.89 %MaxfuncDepth:2
% 0.81/0.89 %SharedTerms:6
% 0.81/0.89 %goalClause: 17
% 0.81/0.89 %singleGoalClaCount:1
% 0.81/0.89 [15]P1(f2(a5,a4))
% 0.81/0.89 [17]~E(f3(a4),a5)
% 0.81/0.89 [13]E(f2(x131,f1(x131)),x131)
% 0.81/0.89 [14]E(f2(f3(x141),x141),x141)
% 0.81/0.89 [16]E(f2(f2(x161,x162),x163),f2(x161,f2(x162,x163)))
% 0.81/0.89 [18]P1(x181)+~P1(f1(x181))
% 0.81/0.89 [19]P1(x191)+~P1(f3(x191))
% 0.81/0.89 [28]E(f2(x281,a5),x281)+~P1(f2(x281,a5))
% 0.81/0.89 [29]E(f2(a5,x291),x291)+~P1(f2(a5,x291))
% 0.81/0.89 [20]~P2(x201,x202)+E(x201,x202)
% 0.81/0.89 [22]P1(x221)+~P2(x222,x221)
% 0.81/0.89 [23]P1(x231)+~P2(x231,x232)
% 0.81/0.89 [25]E(x251,x252)+P1(f6(x251,x252))
% 0.81/0.89 [27]E(f3(x271),f1(x272))+~P1(f2(x272,x271))
% 0.84/0.89 [30]P1(f1(x301))+~P1(f2(x301,x302))
% 0.84/0.89 [31]P1(f3(x311))+~P1(f2(x311,x312))
% 0.84/0.89 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 0.84/0.89 [26]E(x261,x262)+E(f6(x261,x262),x262)+E(f6(x261,x262),x261)
% 0.84/0.89 [32]~E(f3(x322),f1(x321))+~P1(f1(x321))+P1(f2(x321,x322))
% 0.84/0.89 %EqnAxiom
% 0.84/0.89 [1]E(x11,x11)
% 0.84/0.89 [2]E(x22,x21)+~E(x21,x22)
% 0.84/0.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.84/0.89 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 0.84/0.89 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 0.84/0.89 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 0.84/0.89 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 0.84/0.89 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.84/0.89 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.84/0.89 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 0.84/0.89 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 0.84/0.89 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 0.84/0.89
% 0.84/0.89 %-------------------------------------------
% 0.84/0.89 cnf(34,plain,
% 0.84/0.89 (~P2(f3(a4),a5)),
% 0.84/0.89 inference(scs_inference,[],[17,20])).
% 0.84/0.89 cnf(36,plain,
% 0.84/0.89 (E(x361,f2(x361,f1(x361)))),
% 0.84/0.89 inference(scs_inference,[],[17,13,20,2])).
% 0.84/0.89 cnf(37,plain,
% 0.84/0.89 (E(f3(a4),f1(a5))),
% 0.84/0.89 inference(scs_inference,[],[17,13,15,20,2,27])).
% 0.84/0.89 cnf(39,plain,
% 0.84/0.89 (E(f2(a5,a4),a4)),
% 0.84/0.89 inference(scs_inference,[],[17,13,15,20,2,27,29])).
% 0.84/0.89 cnf(41,plain,
% 0.84/0.89 (P2(f2(a5,a4),f2(f2(a5,a4),f1(f2(a5,a4))))),
% 0.84/0.89 inference(scs_inference,[],[17,13,15,20,2,27,29,21])).
% 0.84/0.89 cnf(43,plain,
% 0.84/0.89 (~E(f3(a4),f2(f3(a5),a5))),
% 0.84/0.89 inference(scs_inference,[],[17,13,14,15,20,2,27,29,21,3])).
% 0.84/0.89 cnf(45,plain,
% 0.84/0.89 (P1(f2(f2(a5,a4),f1(f2(a5,a4))))),
% 0.84/0.89 inference(scs_inference,[],[17,13,14,15,20,2,27,29,21,3,10])).
% 0.84/0.89 cnf(46,plain,
% 0.84/0.89 (P2(f2(a5,a4),f2(a5,a4))),
% 0.84/0.89 inference(scs_inference,[],[17,13,14,15,20,2,27,29,21,3,10,12])).
% 0.84/0.89 cnf(48,plain,
% 0.84/0.89 (P2(f2(f2(a5,a4),f1(f2(a5,a4))),f2(a5,a4))),
% 0.84/0.89 inference(scs_inference,[],[17,13,14,15,20,2,27,29,21,3,10,12,11])).
% 0.84/0.89 cnf(51,plain,
% 0.84/0.89 (E(f1(a5),f3(a4))),
% 0.84/0.89 inference(scs_inference,[],[43,37,20,2])).
% 0.84/0.89 cnf(52,plain,
% 0.84/0.89 (P1(a4)),
% 0.84/0.89 inference(scs_inference,[],[43,37,39,15,20,2,10])).
% 0.84/0.89 cnf(53,plain,
% 0.84/0.89 (E(f3(a4),f2(f1(a5),f1(f1(a5))))),
% 0.84/0.89 inference(scs_inference,[],[36,43,37,39,15,20,2,10,3])).
% 0.84/0.89 cnf(54,plain,
% 0.84/0.89 (E(x541,f2(x541,f1(x541)))),
% 0.84/0.89 inference(rename_variables,[],[36])).
% 0.84/0.89 cnf(55,plain,
% 0.84/0.89 (P2(a4,f2(a4,f1(a4)))),
% 0.84/0.89 inference(scs_inference,[],[36,54,43,37,39,15,20,2,10,3,21])).
% 0.84/0.89 cnf(60,plain,
% 0.84/0.89 (E(f2(f1(a5),f1(f1(a5))),f3(a4))),
% 0.84/0.89 inference(scs_inference,[],[53,2])).
% 0.84/0.89 cnf(61,plain,
% 0.84/0.89 (E(f2(f3(f1(a5)),f1(a5)),f3(a4))),
% 0.84/0.89 inference(scs_inference,[],[53,51,14,2,3])).
% 0.84/0.89 cnf(68,plain,
% 0.84/0.89 (P1(f2(f1(a5),f1(f1(a5))))+~P1(f2(a4,x681))),
% 0.84/0.89 inference(scs_inference,[],[53,51,14,2,3,10,22,23,31])).
% 0.84/0.89 cnf(71,plain,
% 0.84/0.89 (~E(f2(a5,a4),f3(a4))+P1(f2(f1(a5),f1(f1(a5))))),
% 0.84/0.89 inference(scs_inference,[],[53,51,41,14,15,2,3,10,22,23,31,32,12,21])).
% 0.84/0.89 cnf(74,plain,
% 0.84/0.89 (E(f3(a4),f2(f3(f1(a5)),f1(a5)))),
% 0.84/0.89 inference(scs_inference,[],[61,2])).
% 0.84/0.89 cnf(75,plain,
% 0.84/0.89 (E(f2(f2(a5,a4),f1(f2(a5,a4))),a4)),
% 0.84/0.89 inference(scs_inference,[],[61,39,13,2,3])).
% 0.84/0.89 cnf(77,plain,
% 0.84/0.89 (~P1(f2(f1(a5),f1(f1(a5))))+P1(f3(a4))),
% 0.84/0.89 inference(scs_inference,[],[60,61,39,13,2,3,10])).
% 0.84/0.89 cnf(78,plain,
% 0.84/0.89 (P1(f3(a4))+~E(f2(a5,a4),f3(a4))),
% 0.84/0.89 inference(scs_inference,[],[60,61,39,13,2,3,10,71])).
% 0.84/0.89 cnf(79,plain,
% 0.84/0.89 (~P2(f2(f1(a5),f1(f1(a5))),x791)+P1(f3(a4))),
% 0.84/0.89 inference(scs_inference,[],[60,61,39,13,2,3,10,71,23])).
% 0.84/0.89 cnf(81,plain,
% 0.84/0.89 (~P2(x811,f2(f1(a5),f1(f1(a5))))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[60,61,39,13,2,3,10,71,23,22])).
% 0.84/0.90 cnf(83,plain,
% 0.84/0.90 (~E(f2(a5,a4),f2(f1(a5),f1(f1(a5))))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[60,61,46,39,13,2,3,10,71,23,22,32,12])).
% 0.84/0.90 cnf(84,plain,
% 0.84/0.90 (~E(a4,f2(f1(a5),f1(f1(a5))))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[60,61,55,46,39,13,2,3,10,71,23,22,32,12,11])).
% 0.84/0.90 cnf(85,plain,
% 0.84/0.90 (E(a4,f2(f2(a5,a4),f1(f2(a5,a4))))),
% 0.84/0.90 inference(scs_inference,[],[75,2])).
% 0.84/0.90 cnf(88,plain,
% 0.84/0.90 (P2(f2(a5,a4),a4)),
% 0.84/0.90 inference(scs_inference,[],[75,41,45,2,21,12])).
% 0.84/0.90 cnf(89,plain,
% 0.84/0.90 (E(f1(a5),f2(f3(f1(a5)),f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[74,75,51,41,45,2,21,12,3])).
% 0.84/0.90 cnf(90,plain,
% 0.84/0.90 (P2(a4,f2(a5,a4))),
% 0.84/0.90 inference(scs_inference,[],[74,75,51,41,48,45,2,21,12,3,11])).
% 0.84/0.90 cnf(98,plain,
% 0.84/0.90 (P1(f2(f3(f1(a5)),f1(a5)))+~P1(f2(a4,x981))),
% 0.84/0.90 inference(scs_inference,[],[74,75,51,41,48,45,2,21,12,3,11,10,78,77,79,81,83,84,31])).
% 0.84/0.90 cnf(110,plain,
% 0.84/0.90 (E(f2(f3(f2(a5,a4)),f2(a5,a4)),a4)),
% 0.84/0.90 inference(scs_inference,[],[85,52,16,39,14,2,21,3])).
% 0.84/0.90 cnf(119,plain,
% 0.84/0.90 (~E(f2(a5,a4),f1(a5))+P1(f2(f3(f1(a5)),f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[89,85,41,15,52,16,39,14,2,21,3,10,30,23,22,12,11])).
% 0.84/0.90 cnf(120,plain,
% 0.84/0.90 (E(a4,f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 0.84/0.90 inference(scs_inference,[],[110,2])).
% 0.84/0.90 cnf(122,plain,
% 0.84/0.90 (E(x1221,f2(x1221,f1(x1221)))),
% 0.84/0.90 inference(rename_variables,[],[36])).
% 0.84/0.90 cnf(128,plain,
% 0.84/0.90 (~P2(f3(a4),f2(a5,f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[17,110,36,122,52,88,90,13,2,12,10,3,11,20])).
% 0.84/0.90 cnf(130,plain,
% 0.84/0.90 (E(a4,f2(a5,a4))),
% 0.84/0.90 inference(scs_inference,[],[39,2])).
% 0.84/0.90 cnf(131,plain,
% 0.84/0.90 (P2(a4,f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 0.84/0.90 inference(scs_inference,[],[120,52,39,2,21])).
% 0.84/0.90 cnf(134,plain,
% 0.84/0.90 (P2(f2(f3(f2(a5,a4)),f2(a5,a4)),f2(a4,f1(a4)))),
% 0.84/0.90 inference(scs_inference,[],[120,55,52,88,39,2,21,12,11])).
% 0.84/0.90 cnf(135,plain,
% 0.84/0.90 (~P1(f2(f3(f1(a5)),f1(a5)))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[120,61,55,52,88,39,2,21,12,11,10])).
% 0.84/0.90 cnf(136,plain,
% 0.84/0.90 (P1(f3(a4))+~E(f2(a5,a4),f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[120,61,55,52,88,39,2,21,12,11,10,119])).
% 0.84/0.90 cnf(139,plain,
% 0.84/0.90 (~P2(f2(f3(f1(a5)),f1(a5)),x1391)+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[120,61,55,52,88,39,2,21,12,11,10,119,20,23])).
% 0.84/0.90 cnf(141,plain,
% 0.84/0.90 (~P2(x1411,f2(f3(f1(a5)),f1(a5)))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[120,61,55,52,88,39,2,21,12,11,10,119,20,23,22])).
% 0.84/0.90 cnf(155,plain,
% 0.84/0.90 (~E(f2(a4,f1(a4)),f1(a5))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[36,51,55,131,15,52,14,2,11,10,30,23,22,21,12])).
% 0.84/0.90 cnf(156,plain,
% 0.84/0.90 (~E(a4,f3(a4))+P1(f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[36,51,55,131,15,37,52,14,2,11,10,30,23,22,21,12,3])).
% 0.84/0.90 cnf(159,plain,
% 0.84/0.90 (P1(f1(a5))+~P1(f2(f3(f1(a5)),f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[37,10,156,135])).
% 0.84/0.90 cnf(167,plain,
% 0.84/0.90 (P1(f1(a5))+~P1(f2(f1(a5),f1(f1(a5))))),
% 0.84/0.90 inference(scs_inference,[],[37,10,156,135,136,139,141,155,81,78,83,77])).
% 0.84/0.90 cnf(168,plain,
% 0.84/0.90 (P1(f1(a5))+~P2(f2(f1(a5),f1(f1(a5))),x1681)),
% 0.84/0.90 inference(scs_inference,[],[37,10,156,135,136,139,141,155,81,78,83,77,79])).
% 0.84/0.90 cnf(170,plain,
% 0.84/0.90 (P1(f1(a5))+~P1(f2(a4,x1701))),
% 0.84/0.90 inference(scs_inference,[],[37,10,156,135,136,139,141,155,81,78,83,77,79,84,31])).
% 0.84/0.90 cnf(185,plain,
% 0.84/0.90 (E(f2(x1851,f1(x1851)),x1851)),
% 0.84/0.90 inference(rename_variables,[],[13])).
% 0.84/0.90 cnf(187,plain,
% 0.84/0.90 (E(f2(x1871,f1(x1871)),x1871)),
% 0.84/0.90 inference(rename_variables,[],[13])).
% 0.84/0.90 cnf(191,plain,
% 0.84/0.90 (P1(f2(a4,f1(a4)))),
% 0.84/0.90 inference(scs_inference,[],[13,185,36,130,55,15,12,3,11,2,10])).
% 0.84/0.90 cnf(192,plain,
% 0.84/0.90 (P1(f2(f1(a5),f1(f1(a5))))),
% 0.84/0.90 inference(scs_inference,[],[13,185,36,130,55,15,12,3,11,2,10,68])).
% 0.84/0.90 cnf(194,plain,
% 0.84/0.90 (P1(f2(f3(f1(a5)),f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[13,185,36,130,55,15,12,3,11,2,10,68,98])).
% 0.84/0.90 cnf(196,plain,
% 0.84/0.90 (E(f3(f1(a4)),f1(a4))),
% 0.84/0.90 inference(scs_inference,[],[13,185,36,130,55,15,12,3,11,2,10,68,98,27])).
% 0.84/0.90 cnf(198,plain,
% 0.84/0.90 (P2(f2(f1(a5),f1(f1(a5))),f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[13,185,187,36,130,55,15,12,3,11,2,10,68,98,27,21])).
% 0.84/0.90 cnf(205,plain,
% 0.84/0.90 (P1(f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[194,159])).
% 0.84/0.90 cnf(206,plain,
% 0.84/0.90 (P1(f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[192,167])).
% 0.84/0.90 cnf(207,plain,
% 0.84/0.90 (P1(f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[198,168])).
% 0.84/0.90 cnf(208,plain,
% 0.84/0.90 (P1(f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[191,170])).
% 0.84/0.90 cnf(212,plain,
% 0.84/0.90 (P1(a5)),
% 0.84/0.90 inference(scs_inference,[],[205,18])).
% 0.84/0.90 cnf(218,plain,
% 0.84/0.90 (E(f2(a4,f1(a4)),f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 0.84/0.90 inference(scs_inference,[],[13,61,51,120,198,194,196,205,18,2,21,12,3])).
% 0.84/0.90 cnf(219,plain,
% 0.84/0.90 (E(f2(x2191,f1(x2191)),x2191)),
% 0.84/0.90 inference(rename_variables,[],[13])).
% 0.84/0.90 cnf(220,plain,
% 0.84/0.90 (P2(f1(a5),f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[13,219,61,51,120,198,194,196,205,18,2,21,12,3,11])).
% 0.84/0.90 cnf(234,plain,
% 0.84/0.90 (P2(f1(a5),f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[51,218,206,2,21])).
% 0.84/0.90 cnf(237,plain,
% 0.84/0.90 (E(f2(x2371,f1(x2371)),x2371)),
% 0.84/0.90 inference(rename_variables,[],[13])).
% 0.84/0.90 cnf(238,plain,
% 0.84/0.90 (E(f2(f3(a4),f1(f3(a4))),f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[13,237,51,218,37,134,206,2,21,12,3])).
% 0.84/0.90 cnf(243,plain,
% 0.84/0.90 (P2(a5,f2(a5,f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[36,238,212,2,21])).
% 0.84/0.90 cnf(247,plain,
% 0.84/0.90 (P1(f2(f3(a4),f1(f3(a4))))),
% 0.84/0.90 inference(scs_inference,[],[74,36,238,234,207,212,2,21,12,10])).
% 0.84/0.90 cnf(248,plain,
% 0.84/0.90 (P2(f3(a4),f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[74,51,36,238,234,207,220,212,2,21,12,10,11])).
% 0.84/0.90 cnf(252,plain,
% 0.84/0.90 (E(f2(x2521,f1(x2521)),x2521)),
% 0.84/0.90 inference(rename_variables,[],[13])).
% 0.84/0.90 cnf(256,plain,
% 0.84/0.90 (~E(a5,f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[13,252,128,243,247,21,12,11])).
% 0.84/0.90 cnf(259,plain,
% 0.84/0.90 (~E(a5,f2(f1(a5),f1(f1(a5))))),
% 0.84/0.90 inference(scs_inference,[],[13,252,128,60,243,247,21,12,11,20,3])).
% 0.84/0.90 cnf(263,plain,
% 0.84/0.90 (~E(a5,f2(f3(f1(a5)),f1(a5)))),
% 0.84/0.90 inference(scs_inference,[],[61,53,259,234,256,20,12,3])).
% 0.84/0.90 cnf(270,plain,
% 0.84/0.90 (~E(f1(a5),a5)),
% 0.84/0.90 inference(scs_inference,[],[34,263,248,20,12])).
% 0.84/0.90 cnf(271,plain,
% 0.84/0.90 (~E(a5,f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[34,51,263,248,256,20,12,3])).
% 0.84/0.90 cnf(281,plain,
% 0.84/0.90 (E(f1(x2811),f1(f2(x2811,f1(x2811))))),
% 0.84/0.90 inference(scs_inference,[],[13,4,2])).
% 0.84/0.90 cnf(282,plain,
% 0.84/0.90 (~P2(f1(a5),a5)),
% 0.84/0.90 inference(scs_inference,[],[270,20])).
% 0.84/0.90 cnf(287,plain,
% 0.84/0.90 (~E(a5,f1(f2(a5,f1(a5))))),
% 0.84/0.90 inference(scs_inference,[],[271,281,270,208,20,2,10,3])).
% 0.84/0.90 cnf(292,plain,
% 0.84/0.90 (E(f2(a5,f1(a5)),f1(a5))),
% 0.84/0.90 inference(scs_inference,[],[271,281,270,208,20,2,10,3,18,27,29])).
% 0.84/0.90 cnf(294,plain,
% 0.84/0.90 (P2(f2(a5,f1(a5)),a5)),
% 0.84/0.90 inference(scs_inference,[],[13,271,281,270,208,20,2,10,3,18,27,29,21])).
% 0.84/0.90 cnf(299,plain,
% 0.84/0.90 (~E(f2(a5,f1(a5)),f3(a4))),
% 0.84/0.90 inference(scs_inference,[],[13,34,36,271,281,270,208,20,2,10,3,18,27,29,21,12,11])).
% 0.84/0.90 cnf(305,plain,
% 0.84/0.90 ($false),
% 0.84/0.90 inference(scs_inference,[],[282,61,287,294,299,292,20,2,3,11]),
% 0.84/0.90 ['proof']).
% 0.84/0.90 % SZS output end Proof
% 0.84/0.90 % Total time :0.250000s
%------------------------------------------------------------------------------