%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT014-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:16 EDT 2024
% Result : Unsatisfiable 62.86s 62.92s
% Output : CNFRefutation 62.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : CAT014-3 : TPTP v8.2.0. Released v1.0.0.
% 0.09/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.33 % Computer : n020.cluster.edu
% 0.10/0.33 % Model : x86_64 x86_64
% 0.10/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.33 % Memory : 8042.1875MB
% 0.10/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.33 % CPULimit : 300
% 0.10/0.33 % WCLimit : 300
% 0.10/0.33 % DateTime : Tue Jun 18 12:30:09 EDT 2024
% 0.10/0.33 % CPUTime :
% 0.18/0.55 start to proof:theBenchmark
% 62.85/62.92 %-------------------------------------------
% 62.85/62.92 % File :CSE---1.7
% 62.85/62.92 % Problem :theBenchmark
% 62.85/62.92 % Transform :cnf
% 62.85/62.92 % Format :tptp:raw
% 62.85/62.92 % Command :java -jar mcs_scs.jar %d %s
% 62.85/62.92
% 62.85/62.92 % Result :Theorem 62.350000s
% 62.85/62.92 % Output :CNFRefutation 62.350000s
% 62.85/62.92 %-------------------------------------------
% 62.86/62.92 %--------------------------------------------------------------------------
% 62.86/62.92 % File : CAT014-3 : TPTP v8.2.0. Released v1.0.0.
% 62.86/62.92 % Domain : Category Theory
% 62.86/62.92 % Problem : codomain(codomain(x)) = codomain(x)
% 62.86/62.92 % Version : [Sco79] axioms : Reduced > Complete.
% 62.86/62.92 % English :
% 62.86/62.92
% 62.86/62.92 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 62.86/62.92 % Source : [ANL]
% 62.86/62.92 % Names : p14.ver3.in [ANL]
% 62.86/62.92
% 62.86/62.92 % Status : Unsatisfiable
% 62.86/62.92 % Rating : 0.10 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.3.0, 0.09 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.28 v5.2.0, 0.12 v5.1.0, 0.18 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v3.7.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.17 v3.3.0, 0.21 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
% 62.86/62.92 % Syntax : Number of clauses : 19 ( 5 unt; 2 nHn; 14 RR)
% 62.86/62.92 % Number of literals : 39 ( 16 equ; 18 neg)
% 62.86/62.92 % Maximal clause size : 4 ( 2 avg)
% 62.86/62.92 % Maximal term depth : 3 ( 1 avg)
% 62.86/62.92 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 62.86/62.92 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% 62.86/62.92 % Number of variables : 31 ( 4 sgn)
% 62.86/62.92 % SPC : CNF_UNS_RFO_SEQ_NHN
% 62.86/62.92
% 62.86/62.92 % Comments : Axioms simplified by Art Quaife.
% 62.86/62.92 %--------------------------------------------------------------------------
% 62.86/62.92 %----Include Scott's axioms for category theory
% 62.86/62.92 include('Axioms/CAT003-0.ax').
% 62.86/62.92 %--------------------------------------------------------------------------
% 62.86/62.92 cnf(assume_codomain_exists,hypothesis,
% 62.86/62.92 there_exists(codomain(a)) ).
% 62.86/62.92
% 62.86/62.92 cnf(prove_codomain_is_idempotent,negated_conjecture,
% 62.86/62.92 codomain(codomain(a)) != codomain(a) ).
% 62.86/62.92
% 62.86/62.92 %--------------------------------------------------------------------------
% 62.86/62.92 %-------------------------------------------
% 62.86/62.92 % Proof found
% 62.86/62.92 % SZS status Theorem for theBenchmark
% 62.86/62.92 % SZS output start Proof
% 62.86/62.93 %ClaNum:30(EqnAxiom:12)
% 62.86/62.93 %VarNum:58(SingletonVarNum:27)
% 62.86/62.93 %MaxLitNum:3
% 62.86/62.93 %MaxfuncDepth:2
% 62.86/62.93 %SharedTerms:5
% 62.86/62.93 %goalClause: 17
% 62.86/62.93 %singleGoalClaCount:1
% 62.86/62.93 [13]P1(f2(a1))
% 62.86/62.93 [17]~E(f2(f2(a1)),f2(a1))
% 62.86/62.93 [14]E(f4(x141,f3(x141)),x141)
% 62.86/62.93 [15]E(f4(f2(x151),x151),x151)
% 62.86/62.93 [16]E(f4(f4(x161,x162),x163),f4(x161,f4(x162,x163)))
% 62.86/62.93 [18]P1(x181)+~P1(f3(x181))
% 62.86/62.93 [19]P1(x191)+~P1(f2(x191))
% 62.86/62.93 [20]~P2(x201,x202)+E(x201,x202)
% 62.86/62.93 [22]P1(x221)+~P2(x222,x221)
% 62.86/62.93 [23]P1(x231)+~P2(x231,x232)
% 62.86/62.93 [25]E(x251,x252)+P1(f5(x251,x252))
% 62.86/62.93 [27]E(f2(x271),f3(x272))+~P1(f4(x272,x271))
% 62.86/62.93 [28]P1(f3(x281))+~P1(f4(x281,x282))
% 62.86/62.93 [29]P1(f2(x291))+~P1(f4(x291,x292))
% 62.86/62.93 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 62.86/62.93 [26]E(x261,x262)+E(f5(x261,x262),x262)+E(f5(x261,x262),x261)
% 62.86/62.93 [30]~E(f2(x302),f3(x301))+~P1(f3(x301))+P1(f4(x301,x302))
% 62.86/62.93 %EqnAxiom
% 62.86/62.93 [1]E(x11,x11)
% 62.86/62.93 [2]E(x22,x21)+~E(x21,x22)
% 62.86/62.93 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 62.86/62.93 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 62.86/62.93 [5]~E(x51,x52)+E(f3(x51),f3(x52))
% 62.86/62.93 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 62.86/62.93 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 62.86/62.93 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 62.86/62.93 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 62.86/62.93 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 62.86/62.93 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 62.86/62.93 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 62.86/62.93
% 62.86/62.93 %-------------------------------------------
% 62.86/62.94 cnf(31,plain,
% 62.86/62.94 (~P1(x311)+P2(x311,x311)),
% 62.86/62.94 inference(equality_inference,[],[21])).
% 62.86/62.94 cnf(34,plain,
% 62.86/62.94 (E(x341,f4(x341,f3(x341)))),
% 62.86/62.94 inference(scs_inference,[],[17,14,20,2])).
% 62.86/62.94 cnf(35,plain,
% 62.86/62.94 (~E(f2(a1),a1)),
% 62.86/62.94 inference(scs_inference,[],[17,14,20,2,4])).
% 62.86/62.94 cnf(36,plain,
% 62.86/62.94 (P1(a1)),
% 62.86/62.94 inference(scs_inference,[],[17,14,13,20,2,4,19])).
% 62.86/62.94 cnf(38,plain,
% 62.86/62.94 (P2(f2(a1),f4(f2(a1),f3(f2(a1))))),
% 62.86/62.94 inference(scs_inference,[],[17,14,13,20,2,4,19,21])).
% 62.86/62.94 cnf(40,plain,
% 62.86/62.94 (~E(f2(f2(a1)),f4(f2(f2(a1)),f2(a1)))),
% 62.86/62.94 inference(scs_inference,[],[17,14,15,13,20,2,4,19,21,3])).
% 62.86/62.94 cnf(42,plain,
% 62.86/62.94 (P1(f4(f2(a1),f3(f2(a1))))),
% 62.86/62.94 inference(scs_inference,[],[17,14,15,13,20,2,4,19,21,3,10])).
% 62.86/62.94 cnf(45,plain,
% 62.86/62.94 (~E(f2(a1),f2(f2(a1)))),
% 62.86/62.94 inference(scs_inference,[],[17,14,15,13,20,2,4,19,21,3,10,12,11])).
% 62.86/62.94 cnf(48,plain,
% 62.86/62.94 (~E(a1,f2(a1))),
% 62.86/62.94 inference(scs_inference,[],[40,45,20,4])).
% 62.86/62.94 cnf(49,plain,
% 62.86/62.94 (E(f4(x491,f4(x492,x493)),f4(f4(x491,x492),x493))),
% 62.86/62.94 inference(scs_inference,[],[40,45,16,20,4,2])).
% 62.86/62.94 cnf(50,plain,
% 62.86/62.94 (P2(a1,f4(a1,f3(a1)))),
% 62.86/62.94 inference(scs_inference,[],[34,40,45,36,16,20,4,2,21])).
% 62.86/62.94 cnf(51,plain,
% 62.86/62.94 (E(x511,f4(x511,f3(x511)))),
% 62.86/62.94 inference(rename_variables,[],[34])).
% 62.86/62.94 cnf(55,plain,
% 62.86/62.94 (~P1(f4(f4(x551,x552),x553))+P1(f4(x551,f4(x552,x553)))),
% 62.86/62.94 inference(scs_inference,[],[34,51,40,45,36,16,20,4,2,21,11,10])).
% 62.86/62.94 cnf(56,plain,
% 62.86/62.94 (~P2(x561,f4(f4(x562,x563),x564))+P1(f4(x562,f4(x563,x564)))),
% 62.86/62.94 inference(scs_inference,[],[34,51,40,45,36,16,20,4,2,21,11,10,22])).
% 62.86/62.94 cnf(58,plain,
% 62.86/62.94 (~P2(f4(f4(x581,x582),x583),x584)+P1(f4(x581,f4(x582,x583)))),
% 62.86/62.94 inference(scs_inference,[],[34,51,40,45,36,16,20,4,2,21,11,10,22,23])).
% 62.86/62.94 cnf(62,plain,
% 62.86/62.94 (~P2(f2(a1),a1)),
% 62.86/62.94 inference(scs_inference,[],[35,20])).
% 62.86/62.94 cnf(64,plain,
% 62.86/62.94 (E(x641,f4(f2(x641),x641))),
% 62.86/62.94 inference(scs_inference,[],[35,15,20,2])).
% 62.86/62.94 cnf(66,plain,
% 62.86/62.94 (P1(f4(f2(f2(a1)),f2(a1)))),
% 62.86/62.94 inference(scs_inference,[],[35,38,15,13,20,2,12,10])).
% 62.86/62.94 cnf(67,plain,
% 62.86/62.94 (~P2(a1,f2(a1))),
% 62.86/62.94 inference(scs_inference,[],[48,20])).
% 62.86/62.94 cnf(71,plain,
% 62.86/62.94 (~E(f4(a1,f3(a1)),f2(a1))),
% 62.86/62.94 inference(scs_inference,[],[64,48,50,20,11,12])).
% 62.86/62.94 cnf(72,plain,
% 62.86/62.94 (~P1(f4(x721,f4(x722,x723)))+P1(f4(f4(x721,x722),x723))),
% 62.86/62.94 inference(scs_inference,[],[64,49,48,50,20,11,12,10])).
% 62.86/62.94 cnf(74,plain,
% 62.86/62.94 (~P2(f4(x741,f4(x742,x743)),x744)+P1(f4(f4(x741,x742),x743))),
% 62.86/62.94 inference(scs_inference,[],[64,49,48,50,20,11,12,10,55,23])).
% 62.86/62.94 cnf(76,plain,
% 62.86/62.94 (~P2(x761,f4(x762,f4(x763,x764)))+P1(f4(f4(x762,x763),x764))),
% 62.86/62.94 inference(scs_inference,[],[64,49,48,50,20,11,12,10,55,23,22])).
% 62.86/62.94 cnf(82,plain,
% 62.86/62.94 (~P2(f4(a1,f3(a1)),f2(a1))),
% 62.86/62.94 inference(scs_inference,[],[71,20])).
% 62.86/62.94 cnf(87,plain,
% 62.86/62.94 (P2(a1,a1)),
% 62.86/62.94 inference(scs_inference,[],[50,31,23])).
% 62.86/62.94 cnf(99,plain,
% 62.86/62.94 (P2(f4(f2(f2(a1)),f2(a1)),f2(a1))),
% 62.86/62.94 inference(scs_inference,[],[15,66,21])).
% 62.86/62.94 cnf(111,plain,
% 62.86/62.94 (~P2(f4(f2(f2(a1)),f2(a1)),f4(a1,f3(a1)))),
% 62.86/62.94 inference(scs_inference,[],[82,99,11,20])).
% 62.86/62.94 cnf(114,plain,
% 62.86/62.94 (~E(f2(a1),f4(a1,f3(a1)))),
% 62.86/62.94 inference(scs_inference,[],[111,99,12])).
% 62.86/62.94 cnf(127,plain,
% 62.86/62.94 (~P2(x1271,f4(f4(x1272,x1273),x1274))+E(f2(f4(x1273,x1274)),f3(x1272))),
% 62.86/62.94 inference(scs_inference,[],[56,27])).
% 62.86/62.94 cnf(128,plain,
% 62.86/62.94 (~E(f2(a1),f4(f2(a1),a1))),
% 62.86/62.94 inference(scs_inference,[],[35,15,3])).
% 62.86/62.94 cnf(134,plain,
% 62.86/62.94 (P1(f4(a1,f3(a1)))),
% 62.86/62.94 inference(scs_inference,[],[36,34,10])).
% 62.86/62.94 cnf(138,plain,
% 62.86/62.94 (E(f3(a1),f2(f3(a1)))),
% 62.86/62.94 inference(scs_inference,[],[36,34,10,27,2])).
% 62.86/62.94 cnf(139,plain,
% 62.86/62.94 (E(f4(f2(f3(a1)),f3(a1)),f2(f3(a1)))),
% 62.86/62.94 inference(scs_inference,[],[36,34,15,10,27,2,3])).
% 62.86/62.94 cnf(143,plain,
% 62.86/62.94 (P1(f4(f2(a1),a1))),
% 62.86/62.94 inference(scs_inference,[],[36,139,64,2,10])).
% 62.86/62.94 cnf(147,plain,
% 62.86/62.94 (E(f4(f2(f2(a1)),f2(a1)),f3(f2(a1)))),
% 62.86/62.94 inference(scs_inference,[],[36,139,64,15,2,10,27,3])).
% 62.86/62.94 cnf(151,plain,
% 62.86/62.94 (~E(f2(f2(a1)),f3(f2(a1)))),
% 62.86/62.94 inference(scs_inference,[],[147,40,2,3])).
% 62.86/62.94 cnf(152,plain,
% 62.86/62.94 (P1(f3(f2(a1)))),
% 62.86/62.94 inference(scs_inference,[],[147,40,66,2,3,10])).
% 62.86/62.94 cnf(156,plain,
% 62.86/62.94 (P2(f4(f4(x1561,x1562),x1563),f4(f4(x1561,x1562),x1563))+~P2(f4(x1561,f4(x1562,x1563)),x1564)),
% 62.86/62.94 inference(scs_inference,[],[74,31])).
% 62.86/62.94 cnf(238,plain,
% 62.86/62.94 (~P2(x2381,f4(f4(x2382,x2383),x2384))+E(f3(x2382),f2(f4(x2383,x2384)))),
% 62.86/62.94 inference(scs_inference,[],[127,2])).
% 62.86/62.94 cnf(278,plain,
% 62.86/62.94 (~P1(f3(f4(f2(a1),f2(a1))))),
% 62.86/62.94 inference(scs_inference,[],[151,18,27])).
% 62.86/62.94 cnf(287,plain,
% 62.86/62.94 (~P2(f4(f2(a1),f4(f2(a1),x2871)),x2872)),
% 62.86/62.94 inference(scs_inference,[],[49,278,28,22,23,10,74])).
% 62.86/62.94 cnf(293,plain,
% 62.86/62.94 (~P2(x2931,f4(f4(f2(a1),f2(a1)),x2932))),
% 62.86/62.94 inference(scs_inference,[],[49,278,28,22,23,10,74,76,58,56])).
% 62.86/62.94 cnf(311,plain,
% 62.86/62.94 (~E(a1,f4(f2(a1),f4(f2(a1),x3111)))),
% 62.86/62.94 inference(scs_inference,[],[287,87,11])).
% 62.86/62.94 cnf(313,plain,
% 62.86/62.94 (~E(a1,f4(f4(f2(a1),f2(a1)),x3131))),
% 62.86/62.94 inference(scs_inference,[],[287,87,16,11,3])).
% 62.86/62.94 cnf(315,plain,
% 62.86/62.95 (~E(a1,f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[34,313,3])).
% 62.86/62.95 cnf(321,plain,
% 62.86/62.95 (~P2(a1,f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[315,20])).
% 62.86/62.95 cnf(331,plain,
% 62.86/62.95 (~P1(f2(f4(f2(a1),f2(a1))))),
% 62.86/62.95 inference(scs_inference,[],[151,19,27])).
% 62.86/62.95 cnf(334,plain,
% 62.86/62.95 (~P2(x3341,f2(f4(f2(a1),f2(a1))))),
% 62.86/62.95 inference(scs_inference,[],[331,23,22])).
% 62.86/62.95 cnf(340,plain,
% 62.86/62.95 (~E(f4(a1,f3(a1)),f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[321,50,12])).
% 62.86/62.95 cnf(365,plain,
% 62.86/62.95 (P1(f3(a1))),
% 62.86/62.95 inference(scs_inference,[],[50,22,28])).
% 62.86/62.95 cnf(377,plain,
% 62.86/62.95 (~P2(x3771,f4(a1,f4(f2(a1),f2(a1))))),
% 62.86/62.95 inference(scs_inference,[],[334,365,21,238,156,31,72,76])).
% 62.86/62.95 cnf(389,plain,
% 62.86/62.95 (~E(f3(a1),f4(f4(f2(a1),f2(a1)),x3891))),
% 62.86/62.95 inference(scs_inference,[],[293,365,21])).
% 62.86/62.95 cnf(393,plain,
% 62.86/62.95 (~E(f3(a1),f4(a1,f4(f2(a1),f2(a1))))),
% 62.86/62.95 inference(scs_inference,[],[377,365,21])).
% 62.86/62.95 cnf(399,plain,
% 62.86/62.95 (~E(f3(a1),f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[34,389,3])).
% 62.86/62.95 cnf(403,plain,
% 62.86/62.95 (~P2(f3(a1),f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[399,20])).
% 62.86/62.95 cnf(405,plain,
% 62.86/62.95 (~E(f3(a1),f4(f4(a1,f2(a1)),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[399,393,16,20,3])).
% 62.86/62.95 cnf(468,plain,
% 62.86/62.95 (P1(f5(f2(a1),a1))),
% 62.86/62.95 inference(scs_inference,[],[17,25,4])).
% 62.86/62.95 cnf(501,plain,
% 62.86/62.95 (~E(f2(f3(a1)),f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[403,138,365,21,12])).
% 62.86/62.95 cnf(544,plain,
% 62.86/62.95 (P1(f4(f3(a1),f3(f3(a1))))),
% 62.86/62.95 inference(scs_inference,[],[365,34,10])).
% 62.86/62.95 cnf(647,plain,
% 62.86/62.95 (E(f4(x6471,x6472),f4(x6471,f4(x6472,f3(x6472))))),
% 62.86/62.95 inference(scs_inference,[],[14,7,2])).
% 62.86/62.95 cnf(648,plain,
% 62.86/62.95 (E(f4(x6481,f4(x6482,f3(x6482))),f4(x6481,x6482))),
% 62.86/62.95 inference(scs_inference,[],[647,2])).
% 62.86/62.95 cnf(650,plain,
% 62.86/62.95 (E(f4(x6501,f3(x6501)),x6501)),
% 62.86/62.95 inference(rename_variables,[],[14])).
% 62.86/62.95 cnf(652,plain,
% 62.86/62.95 (E(f4(x6521,f3(x6521)),f4(f2(x6521),x6521))),
% 62.86/62.95 inference(scs_inference,[],[14,650,64,647,134,2,21,3])).
% 62.86/62.95 cnf(659,plain,
% 62.86/62.95 (P1(f4(f2(a1),f4(a1,f3(a1))))),
% 62.86/62.95 inference(scs_inference,[],[14,652,647,143,42,2,21,10])).
% 62.86/62.95 cnf(665,plain,
% 62.86/62.95 (P1(f4(f4(f2(a1),a1),f3(a1)))),
% 62.86/62.95 inference(scs_inference,[],[14,49,659,544,21,10])).
% 62.86/62.95 cnf(670,plain,
% 62.86/62.95 (E(f4(f4(x6701,x6702),f3(x6702)),f4(x6701,x6702))),
% 62.86/62.95 inference(scs_inference,[],[16,648,3])).
% 62.86/62.95 cnf(674,plain,
% 62.86/62.95 (E(f4(x6741,x6742),f4(f4(x6741,x6742),f3(x6742)))),
% 62.86/62.95 inference(scs_inference,[],[670,2])).
% 62.86/62.95 cnf(699,plain,
% 62.86/62.95 (E(x6991,f4(f2(x6991),x6991))),
% 62.86/62.95 inference(rename_variables,[],[64])).
% 62.86/62.95 cnf(703,plain,
% 62.86/62.95 (E(f4(f4(f2(x7031),x7031),f3(x7031)),x7031)),
% 62.86/62.95 inference(scs_inference,[],[64,699,674,13,21,3,2])).
% 62.86/62.95 cnf(851,plain,
% 62.86/62.95 (E(f4(x8511,f3(x8511)),f4(f2(x8511),x8511))),
% 62.86/62.95 inference(rename_variables,[],[652])).
% 62.86/62.95 cnf(853,plain,
% 62.86/62.95 (E(f4(x8531,f3(x8531)),f4(f4(f2(x8531),x8531),f3(x8531)))),
% 62.86/62.95 inference(scs_inference,[],[652,851,674,134,21,3])).
% 62.86/62.95 cnf(886,plain,
% 62.86/62.95 (~E(f4(f4(f2(a1),a1),f3(a1)),f2(a1))),
% 62.86/62.95 inference(scs_inference,[],[703,62,665,21,11])).
% 62.86/62.95 cnf(922,plain,
% 62.86/62.95 (P2(f4(a1,f3(a1)),f4(f4(f2(a1),a1),f3(a1)))),
% 62.86/62.95 inference(scs_inference,[],[853,134,21])).
% 62.86/62.95 cnf(1418,plain,
% 62.86/62.95 (P1(f2(f4(a1,f3(a1))))),
% 62.86/62.95 inference(scs_inference,[],[922,152,238,10])).
% 62.86/62.95 cnf(1519,plain,
% 62.86/62.95 (P1(f3(f3(a1)))),
% 62.86/62.95 inference(scs_inference,[],[886,544,64,468,25,8,9,6,7,5,31,28])).
% 62.86/62.95 cnf(1521,plain,
% 62.86/62.95 (E(f2(x15211),f2(f4(f2(x15211),x15211)))),
% 62.86/62.95 inference(scs_inference,[],[886,544,64,468,25,8,9,6,7,5,31,28,4])).
% 62.86/62.95 cnf(1522,plain,
% 62.86/62.95 (~E(f4(f4(a1,f2(a1)),f2(a1)),f3(a1))),
% 62.86/62.95 inference(scs_inference,[],[886,405,544,64,468,25,8,9,6,7,5,31,28,4,2])).
% 62.86/62.95 cnf(1532,plain,
% 62.86/62.95 (E(f4(x15321,f4(f2(x15322),x15322)),f4(x15321,x15322))),
% 62.86/62.95 inference(scs_inference,[],[1522,14,15,9,5,25,6,8,7])).
% 62.86/62.95 cnf(1535,plain,
% 62.86/62.95 (E(f2(f4(x15351,f3(x15351))),f2(x15351))),
% 62.86/62.95 inference(scs_inference,[],[1519,1522,14,15,9,5,25,6,8,7,31,4])).
% 62.86/62.95 cnf(1552,plain,
% 62.86/62.95 (E(f2(f4(x15521,f3(x15521))),f2(x15521))),
% 62.86/62.95 inference(rename_variables,[],[1535])).
% 62.86/62.95 cnf(1557,plain,
% 62.86/62.95 (~P2(f2(f4(a1,f3(a1))),a1)),
% 62.86/62.95 inference(scs_inference,[],[501,1535,1552,1521,114,67,62,35,36,15,25,5,6,9,8,4,2,12,21,3,11])).
% 62.86/62.95 cnf(1568,plain,
% 62.86/62.95 (E(f4(x15681,x15682),f4(f4(x15681,f3(x15681)),x15682))),
% 62.86/62.95 inference(scs_inference,[],[128,34,25,6])).
% 62.86/62.95 cnf(1589,plain,
% 62.86/62.95 (~E(f4(f4(a1,f3(a1)),f3(a1)),f4(f2(a1),f2(a1)))),
% 62.86/62.95 inference(scs_inference,[],[340,1568,1418,1557,399,25,2,21,3])).
% 62.86/62.95 cnf(1661,plain,
% 62.86/62.95 (E(f4(f2(x16611),f4(f2(x16611),x16611)),x16611)),
% 62.86/62.95 inference(scs_inference,[],[15,1532,1589,2,3])).
% 62.86/62.95 cnf(1735,plain,
% 62.86/62.95 ($false),
% 62.86/62.95 inference(scs_inference,[],[311,1661,2]),
% 62.86/62.95 ['proof']).
% 62.86/62.95 % SZS output end Proof
% 62.86/62.95 % Total time :62.350000s
%------------------------------------------------------------------------------