%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT006-4 : 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 : n025.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.66s 0.78s
% Output : CNFRefutation 0.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CAT006-4 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 12:14:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 0.66/0.77 %-------------------------------------------
% 0.66/0.77 % File :CSE---1.7
% 0.66/0.77 % Problem :theBenchmark
% 0.66/0.77 % Transform :cnf
% 0.66/0.77 % Format :tptp:raw
% 0.66/0.77 % Command :java -jar mcs_scs.jar %d %s
% 0.66/0.77
% 0.66/0.77 % Result :Theorem 0.150000s
% 0.66/0.77 % Output :CNFRefutation 0.150000s
% 0.66/0.77 %-------------------------------------------
% 0.66/0.77 %--------------------------------------------------------------------------
% 0.66/0.77 % File : CAT006-4 : TPTP v8.2.0. Released v1.0.0.
% 0.66/0.78 % Domain : Category Theory
% 0.66/0.78 % Problem : Codomain is the unique left identity
% 0.66/0.78 % Version : [Sco79] axioms : Reduced > Complete.
% 0.66/0.78 % English : codomain(x) is the unique identity j such that jx is defined.
% 0.66/0.78
% 0.66/0.78 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 0.66/0.78 % Source : [TPTP]
% 0.66/0.78 % Names :
% 0.66/0.78
% 0.66/0.78 % Status : Unsatisfiable
% 0.66/0.78 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.43 v2.5.0, 0.20 v2.4.0, 0.17 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 0.66/0.78 % Syntax : Number of clauses : 15 ( 5 unt; 0 nHn; 12 RR)
% 0.66/0.78 % Number of literals : 27 ( 10 equ; 13 neg)
% 0.66/0.78 % Maximal clause size : 3 ( 1 avg)
% 0.66/0.78 % Maximal term depth : 3 ( 1 avg)
% 0.66/0.78 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 0.66/0.78 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 0.66/0.78 % Number of variables : 21 ( 2 sgn)
% 0.66/0.78 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.66/0.78
% 0.66/0.78 % Comments : The dependent axioms have been removed.
% 0.66/0.78 %--------------------------------------------------------------------------
% 0.66/0.78 %----Include Scott's axioms for category theory
% 0.66/0.78 include('Axioms/CAT004-0.ax').
% 0.66/0.78 %--------------------------------------------------------------------------
% 0.66/0.78 %----Denial of theorem: d is an identity which is not cod(a),
% 0.66/0.78 cnf(da_exists,hypothesis,
% 0.66/0.78 there_exists(compose(d,a)) ).
% 0.66/0.78
% 0.66/0.78 cnf(xd_equals_x,hypothesis,
% 0.66/0.78 ( ~ there_exists(compose(X,d))
% 0.66/0.78 | compose(X,d) = X ) ).
% 0.66/0.78
% 0.66/0.78 cnf(dx_equals_x,hypothesis,
% 0.66/0.78 ( ~ there_exists(compose(d,X))
% 0.66/0.78 | compose(d,X) = X ) ).
% 0.66/0.78
% 0.66/0.78 cnf(prove_codomain_of_a_is_d,negated_conjecture,
% 0.66/0.78 codomain(a) != d ).
% 0.66/0.78
% 0.66/0.78 %--------------------------------------------------------------------------
% 0.66/0.78 %-------------------------------------------
% 0.66/0.78 % Proof found
% 0.66/0.78 % SZS status Theorem for theBenchmark
% 0.66/0.78 % SZS output start Proof
% 0.66/0.78 %ClaNum:25(EqnAxiom:10)
% 0.66/0.78 %VarNum:46(SingletonVarNum:21)
% 0.66/0.78 %MaxLitNum:3
% 0.66/0.78 %MaxfuncDepth:2
% 0.66/0.78 %SharedTerms:6
% 0.66/0.78 %goalClause: 15
% 0.66/0.78 %singleGoalClaCount:1
% 0.66/0.78 [13]P1(f2(a5,a4))
% 0.66/0.78 [15]~E(f3(a4),a5)
% 0.66/0.78 [11]E(f2(x111,f1(x111)),x111)
% 0.66/0.78 [12]E(f2(f3(x121),x121),x121)
% 0.66/0.78 [14]E(f2(f2(x141,x142),x143),f2(x141,f2(x142,x143)))
% 0.66/0.78 [16]P1(x161)+~P1(f1(x161))
% 0.66/0.78 [17]P1(x171)+~P1(f3(x171))
% 0.66/0.78 [22]E(f2(x221,a5),x221)+~P1(f2(x221,a5))
% 0.66/0.78 [23]E(f2(a5,x231),x231)+~P1(f2(a5,x231))
% 0.66/0.78 [18]~P2(x181,x182)+E(x181,x182)
% 0.66/0.78 [20]P1(x201)+~P2(x201,x202)
% 0.66/0.78 [21]E(f3(x211),f1(x212))+~P1(f2(x212,x211))
% 0.66/0.78 [24]P1(f1(x241))+~P1(f2(x241,x242))
% 0.66/0.78 [19]~E(x191,x192)+~P1(x191)+P2(x191,x192)
% 0.66/0.78 [25]~E(f3(x252),f1(x251))+~P1(f1(x251))+P1(f2(x251,x252))
% 0.66/0.78 %EqnAxiom
% 0.66/0.78 [1]E(x11,x11)
% 0.66/0.78 [2]E(x22,x21)+~E(x21,x22)
% 0.66/0.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.66/0.78 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 0.66/0.78 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 0.66/0.78 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 0.66/0.78 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 0.66/0.78 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 0.66/0.78 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93)
% 0.66/0.78 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101)
% 0.66/0.78
% 0.66/0.78 %-------------------------------------------
% 0.66/0.78 cnf(26,plain,
% 0.66/0.78 (~P1(x261)+P2(x261,x261)),
% 0.66/0.78 inference(equality_inference,[],[19])).
% 0.66/0.78 cnf(29,plain,
% 0.66/0.78 (E(x291,f2(x291,f1(x291)))),
% 0.66/0.78 inference(scs_inference,[],[15,11,18,2])).
% 0.66/0.78 cnf(30,plain,
% 0.66/0.78 (E(f3(a4),f1(a5))),
% 0.66/0.78 inference(scs_inference,[],[15,11,13,18,2,21])).
% 0.66/0.78 cnf(32,plain,
% 0.66/0.78 (E(f2(a5,a4),a4)),
% 0.66/0.78 inference(scs_inference,[],[15,11,13,18,2,21,23])).
% 0.66/0.78 cnf(34,plain,
% 0.66/0.78 (P2(f2(a5,a4),f2(f2(a5,a4),f1(f2(a5,a4))))),
% 0.66/0.78 inference(scs_inference,[],[15,11,13,18,2,21,23,19])).
% 0.66/0.78 cnf(36,plain,
% 0.66/0.78 (~E(f3(a4),f2(f3(a5),a5))),
% 0.66/0.78 inference(scs_inference,[],[15,11,12,13,18,2,21,23,19,3])).
% 0.66/0.78 cnf(38,plain,
% 0.66/0.78 (P1(f2(f2(a5,a4),f1(f2(a5,a4))))),
% 0.66/0.78 inference(scs_inference,[],[15,11,12,13,18,2,21,23,19,3,8])).
% 0.66/0.78 cnf(41,plain,
% 0.66/0.78 (P2(f2(f2(a5,a4),f1(f2(a5,a4))),f2(a5,a4))),
% 0.66/0.78 inference(scs_inference,[],[15,11,12,13,18,2,21,23,19,3,8,10,9])).
% 0.66/0.78 cnf(44,plain,
% 0.66/0.78 (E(f1(a5),f3(a4))),
% 0.66/0.78 inference(scs_inference,[],[36,30,18,2])).
% 0.66/0.78 cnf(45,plain,
% 0.66/0.78 (E(f3(a4),f2(f1(a5),f1(f1(a5))))),
% 0.66/0.78 inference(scs_inference,[],[29,36,30,18,2,3])).
% 0.66/0.78 cnf(46,plain,
% 0.66/0.78 (E(x461,f2(x461,f1(x461)))),
% 0.66/0.78 inference(rename_variables,[],[29])).
% 0.66/0.78 cnf(47,plain,
% 0.66/0.78 (P1(a4)),
% 0.66/0.78 inference(scs_inference,[],[29,36,30,32,13,18,2,3,8])).
% 0.66/0.78 cnf(48,plain,
% 0.66/0.78 (P2(a4,f2(a4,f1(a4)))),
% 0.66/0.78 inference(scs_inference,[],[29,46,36,30,32,13,18,2,3,8,19])).
% 0.66/0.78 cnf(53,plain,
% 0.66/0.78 (E(f2(f1(a5),f1(f1(a5))),f3(a4))),
% 0.66/0.78 inference(scs_inference,[],[45,2])).
% 0.66/0.78 cnf(54,plain,
% 0.66/0.78 (E(f2(f3(f1(a5)),f1(a5)),f3(a4))),
% 0.66/0.78 inference(scs_inference,[],[45,44,12,2,3])).
% 0.66/0.78 cnf(57,plain,
% 0.66/0.78 (~P2(f3(a4),x571)+P1(f2(f1(a5),f1(f1(a5))))),
% 0.66/0.78 inference(scs_inference,[],[45,44,12,2,3,8,20])).
% 0.66/0.78 cnf(59,plain,
% 0.66/0.78 (~E(f2(a5,a4),f3(a4))+P1(f2(f1(a5),f1(f1(a5))))),
% 0.66/0.78 inference(scs_inference,[],[45,44,34,12,2,3,8,20,9])).
% 0.66/0.78 cnf(60,plain,
% 0.66/0.78 (E(f3(a4),f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.78 inference(scs_inference,[],[54,2])).
% 0.66/0.78 cnf(61,plain,
% 0.66/0.78 (E(f2(f2(a5,a4),f1(f2(a5,a4))),a4)),
% 0.66/0.78 inference(scs_inference,[],[54,32,11,2,3])).
% 0.66/0.78 cnf(65,plain,
% 0.66/0.78 (~P2(f2(f1(a5),f1(f1(a5))),x651)+P1(f3(a4))),
% 0.66/0.78 inference(scs_inference,[],[53,54,32,11,2,3,8,59,20])).
% 0.66/0.78 cnf(71,plain,
% 0.66/0.79 (E(a4,f2(f2(a5,a4),f1(f2(a5,a4))))),
% 0.66/0.79 inference(scs_inference,[],[61,2])).
% 0.66/0.79 cnf(72,plain,
% 0.66/0.79 (P2(f2(f2(a5,a4),f1(f2(a5,a4))),a4)),
% 0.66/0.79 inference(scs_inference,[],[61,38,2,19])).
% 0.66/0.79 cnf(74,plain,
% 0.66/0.79 (P2(f2(a5,a4),a4)),
% 0.66/0.79 inference(scs_inference,[],[61,34,38,2,19,10])).
% 0.66/0.79 cnf(75,plain,
% 0.66/0.79 (E(f1(a5),f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[60,61,44,34,38,2,19,10,3])).
% 0.66/0.79 cnf(76,plain,
% 0.66/0.79 (P2(a4,f2(a5,a4))),
% 0.66/0.79 inference(scs_inference,[],[60,61,44,34,41,38,2,19,10,3,9])).
% 0.66/0.79 cnf(92,plain,
% 0.66/0.79 (E(f2(f3(f2(a5,a4)),f2(a5,a4)),a4)),
% 0.66/0.79 inference(scs_inference,[],[71,47,14,32,12,2,19,3])).
% 0.66/0.79 cnf(96,plain,
% 0.66/0.79 (~P2(f1(a5),x961)+P1(f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[75,71,13,47,14,32,12,2,19,3,8,24,20])).
% 0.66/0.79 cnf(98,plain,
% 0.66/0.79 (~E(f2(f2(a5,a4),f1(f2(a5,a4))),f1(a5))+P1(f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[75,71,72,13,47,14,32,12,2,19,3,8,24,20,9])).
% 0.66/0.79 cnf(99,plain,
% 0.66/0.79 (E(a4,f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 0.66/0.79 inference(scs_inference,[],[92,2])).
% 0.66/0.79 cnf(101,plain,
% 0.66/0.79 (E(x1011,f2(x1011,f1(x1011)))),
% 0.66/0.79 inference(rename_variables,[],[29])).
% 0.66/0.79 cnf(107,plain,
% 0.66/0.79 (~P2(f3(a4),f2(a5,f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[15,92,29,101,47,74,76,11,2,10,3,9,8,18])).
% 0.66/0.79 cnf(109,plain,
% 0.66/0.79 (E(a4,f2(a5,a4))),
% 0.66/0.79 inference(scs_inference,[],[32,2])).
% 0.66/0.79 cnf(110,plain,
% 0.66/0.79 (P2(a4,f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 0.66/0.79 inference(scs_inference,[],[99,47,32,2,19])).
% 0.66/0.79 cnf(113,plain,
% 0.66/0.79 (P2(f2(f3(f2(a5,a4)),f2(a5,a4)),f2(a4,f1(a4)))),
% 0.66/0.79 inference(scs_inference,[],[99,48,47,74,32,2,19,10,9])).
% 0.66/0.79 cnf(114,plain,
% 0.66/0.79 (~P1(f2(f3(f1(a5)),f1(a5)))+P1(f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[99,54,48,47,74,32,2,19,10,9,8])).
% 0.66/0.79 cnf(115,plain,
% 0.66/0.79 (P1(f3(a4))+~E(f2(f2(a5,a4),f1(f2(a5,a4))),f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[99,54,48,47,74,32,2,19,10,9,8,98])).
% 0.66/0.79 cnf(116,plain,
% 0.66/0.79 (~P2(f2(f2(a5,a4),f1(f2(a5,a4))),f1(a5))+P1(f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[99,54,48,47,74,32,2,19,10,9,8,98,18])).
% 0.66/0.79 cnf(118,plain,
% 0.66/0.79 (~P2(f2(f3(f1(a5)),f1(a5)),x1181)+P1(f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[99,54,48,47,74,32,2,19,10,9,8,98,18,20])).
% 0.66/0.79 cnf(126,plain,
% 0.66/0.79 (~P2(f1(a5),x1261)+P1(f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[29,44,110,13,12,2,9,8,24,20])).
% 0.66/0.79 cnf(128,plain,
% 0.66/0.79 (~P1(f3(a4))+P1(f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[30,8])).
% 0.66/0.79 cnf(130,plain,
% 0.66/0.79 (P1(f1(a5))+~P1(f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[30,8,116,114])).
% 0.66/0.79 cnf(133,plain,
% 0.66/0.79 (P1(f1(a5))+~P2(f2(f1(a5),f1(f1(a5))),x1331)),
% 0.66/0.79 inference(scs_inference,[],[30,8,116,114,115,118,65])).
% 0.66/0.79 cnf(148,plain,
% 0.66/0.79 (E(f2(x1481,f1(x1481)),x1481)),
% 0.66/0.79 inference(rename_variables,[],[11])).
% 0.66/0.79 cnf(153,plain,
% 0.66/0.79 (E(f3(f1(a4)),f1(a4))),
% 0.66/0.79 inference(scs_inference,[],[11,148,109,48,13,10,3,2,8,21])).
% 0.66/0.79 cnf(158,plain,
% 0.66/0.79 (P2(f1(a5),f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[13,26,24])).
% 0.66/0.79 cnf(159,plain,
% 0.66/0.79 (P1(f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[158,96])).
% 0.66/0.79 cnf(160,plain,
% 0.66/0.79 (P1(f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[158,126])).
% 0.66/0.79 cnf(162,plain,
% 0.66/0.79 (P2(f1(a5),f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[44,158,153,2,10])).
% 0.66/0.79 cnf(163,plain,
% 0.66/0.79 (E(f2(a4,f1(a4)),f2(f3(f2(a5,a4)),f2(a5,a4)))),
% 0.66/0.79 inference(scs_inference,[],[11,44,99,158,153,2,10,3])).
% 0.66/0.79 cnf(164,plain,
% 0.66/0.79 (E(f2(x1641,f1(x1641)),x1641)),
% 0.66/0.79 inference(rename_variables,[],[11])).
% 0.66/0.79 cnf(165,plain,
% 0.66/0.79 (P2(f3(a4),f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[11,44,99,158,153,2,10,3,9])).
% 0.66/0.79 cnf(168,plain,
% 0.66/0.79 (P2(f2(f1(a5),f1(f1(a5))),f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[11,164,44,99,158,153,2,10,3,9,57,19])).
% 0.66/0.79 cnf(182,plain,
% 0.66/0.79 (P1(f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[160,128])).
% 0.66/0.79 cnf(183,plain,
% 0.66/0.79 (P1(f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[159,130])).
% 0.66/0.79 cnf(184,plain,
% 0.66/0.79 (P1(f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[168,133])).
% 0.66/0.79 cnf(190,plain,
% 0.66/0.79 (P1(a5)),
% 0.66/0.79 inference(scs_inference,[],[182,16])).
% 0.66/0.79 cnf(195,plain,
% 0.66/0.79 (P2(f2(f1(a5),f1(f1(a5))),f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[54,44,163,168,159,182,16,2,19,10])).
% 0.66/0.79 cnf(196,plain,
% 0.66/0.79 (E(f2(f3(a4),f1(f3(a4))),f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[11,54,44,163,168,30,159,182,16,2,19,10,3])).
% 0.66/0.79 cnf(203,plain,
% 0.66/0.79 (P2(a5,f2(a5,f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[29,196,190,2,19])).
% 0.66/0.79 cnf(206,plain,
% 0.66/0.79 (P2(f2(f3(f2(a5,a4)),f2(a5,a4)),a4)),
% 0.66/0.79 inference(scs_inference,[],[11,29,196,113,190,2,19,10])).
% 0.66/0.79 cnf(209,plain,
% 0.66/0.79 (P1(f2(f3(a4),f1(f3(a4))))),
% 0.66/0.79 inference(scs_inference,[],[11,60,29,196,113,165,183,190,2,19,10,9,8])).
% 0.66/0.79 cnf(211,plain,
% 0.66/0.79 (E(f2(x2111,f1(x2111)),x2111)),
% 0.66/0.79 inference(rename_variables,[],[11])).
% 0.66/0.79 cnf(215,plain,
% 0.66/0.79 (~E(a5,f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[11,211,107,203,209,19,10,9])).
% 0.66/0.79 cnf(216,plain,
% 0.66/0.79 (~P2(a5,f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[11,211,107,203,209,19,10,9,18])).
% 0.66/0.79 cnf(218,plain,
% 0.66/0.79 (~E(a5,f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[11,211,107,54,203,209,19,10,9,18,3])).
% 0.66/0.79 cnf(219,plain,
% 0.66/0.79 (~P2(a5,f2(f3(f1(a5)),f1(a5)))),
% 0.66/0.79 inference(scs_inference,[],[218,18])).
% 0.66/0.79 cnf(221,plain,
% 0.66/0.79 (~E(f2(a5,f1(a5)),f3(a4))),
% 0.66/0.79 inference(scs_inference,[],[216,218,203,18,10])).
% 0.66/0.79 cnf(222,plain,
% 0.66/0.79 (~E(a5,f2(f1(a5),f1(f1(a5))))),
% 0.66/0.79 inference(scs_inference,[],[216,53,218,203,215,18,10,3])).
% 0.66/0.79 cnf(228,plain,
% 0.66/0.79 (~E(f2(a5,f1(a5)),f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[219,44,222,203,221,18,10,3])).
% 0.66/0.79 cnf(234,plain,
% 0.66/0.79 (~E(a5,f1(a5))),
% 0.66/0.79 inference(scs_inference,[],[44,109,228,206,215,18,10,3])).
% 0.66/0.79 cnf(236,plain,
% 0.66/0.79 (E(f1(x2361),f1(f2(x2361,f1(x2361))))),
% 0.66/0.79 inference(scs_inference,[],[11,4,2])).
% 0.66/0.79 cnf(247,plain,
% 0.66/0.79 ($false),
% 0.66/0.79 inference(scs_inference,[],[216,60,234,196,228,236,195,184,162,18,2,10,8,3,9,16,23]),
% 0.66/0.79 ['proof']).
% 0.66/0.79 % SZS output end Proof
% 0.66/0.79 % Total time :0.150000s
%------------------------------------------------------------------------------