%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN008-1 : 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 07:26:50 EDT 2024
% Result : Unsatisfiable 63.24s 63.42s
% Output : CNFRefutation 63.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : HEN008-1 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n021.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Sat Jun 22 05:39:08 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 63.24/63.41 %-------------------------------------------
% 63.24/63.41 % File :CSE---1.7
% 63.24/63.41 % Problem :theBenchmark
% 63.24/63.41 % Transform :cnf
% 63.24/63.41 % Format :tptp:raw
% 63.24/63.41 % Command :java -jar mcs_scs.jar %d %s
% 63.24/63.41
% 63.24/63.41 % Result :Theorem 62.680000s
% 63.24/63.41 % Output :CNFRefutation 62.680000s
% 63.24/63.41 %-------------------------------------------
% 63.24/63.42 %--------------------------------------------------------------------------
% 63.24/63.42 % File : HEN008-1 : TPTP v8.2.0. Released v1.0.0.
% 63.24/63.42 % Domain : Henkin Models
% 63.24/63.42 % Problem : X <= Y => X/Z <= Y/Z
% 63.24/63.42 % Version : [MOW76] axioms.
% 63.24/63.42 % English :
% 63.24/63.42
% 63.24/63.42 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 63.24/63.42 % Source : [ANL]
% 63.24/63.42 % Names : hp8.ver1.in [ANL]
% 63.24/63.42
% 63.24/63.42 % Status : Unsatisfiable
% 63.24/63.42 % Rating : 0.12 v8.2.0, 0.00 v7.4.0, 0.11 v7.3.0, 0.22 v7.2.0, 0.25 v7.1.0, 0.29 v7.0.0, 0.00 v6.4.0, 0.14 v6.3.0, 0.00 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.00 v4.1.0, 0.11 v4.0.1, 0.00 v4.0.0, 0.17 v3.5.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.3.0, 0.17 v2.2.1, 0.33 v2.2.0, 0.29 v2.1.0, 0.20 v2.0.0
% 63.24/63.42 % Syntax : Number of clauses : 13 ( 7 unt; 0 nHn; 10 RR)
% 63.24/63.42 % Number of literals : 25 ( 2 equ; 13 neg)
% 63.24/63.42 % Maximal clause size : 6 ( 1 avg)
% 63.24/63.42 % Maximal term depth : 2 ( 1 avg)
% 63.24/63.42 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 63.24/63.42 % Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% 63.24/63.42 % Number of variables : 25 ( 3 sgn)
% 63.24/63.42 % SPC : CNF_UNS_RFO_SEQ_HRN
% 63.24/63.42
% 63.24/63.42 % Comments :
% 63.24/63.42 %--------------------------------------------------------------------------
% 63.24/63.42 %----Include Henkin model axioms
% 63.24/63.42 include('Axioms/HEN001-0.ax').
% 63.24/63.42 %--------------------------------------------------------------------------
% 63.24/63.42 cnf(aLEb,hypothesis,
% 63.24/63.42 less_equal(a,b) ).
% 63.24/63.42
% 63.24/63.42 cnf(aQc,hypothesis,
% 63.24/63.42 quotient(a,c,aQc) ).
% 63.24/63.42
% 63.24/63.42 cnf(bQc,hypothesis,
% 63.24/63.42 quotient(b,c,bQc) ).
% 63.24/63.42
% 63.24/63.42 cnf(prove_aQcLEbQc,negated_conjecture,
% 63.24/63.42 ~ less_equal(aQc,bQc) ).
% 63.24/63.42
% 63.24/63.42 %--------------------------------------------------------------------------
% 63.24/63.42 %-------------------------------------------
% 63.24/63.42 % Proof found
% 63.24/63.42 % SZS status Theorem for theBenchmark
% 63.24/63.42 % SZS output start Proof
% 63.24/63.43 %ClaNum:23(EqnAxiom:10)
% 63.24/63.43 %VarNum:50(SingletonVarNum:25)
% 63.24/63.43 %MaxLitNum:6
% 63.24/63.43 %MaxfuncDepth:1
% 63.24/63.43 %SharedTerms:11
% 63.24/63.43 %goalClause: 17
% 63.24/63.43 %singleGoalClaCount:1
% 63.24/63.43 [11]P1(a1,a2)
% 63.24/63.43 [14]P2(a1,a5,a3)
% 63.24/63.43 [15]P2(a2,a5,a6)
% 63.24/63.43 [17]~P1(a3,a6)
% 63.24/63.43 [12]P1(x121,a4)
% 63.24/63.43 [13]P1(a8,x131)
% 63.24/63.43 [16]P2(x161,x162,f7(x161,x162))
% 63.24/63.43 [19]~P1(x191,x192)+P2(x191,x192,a8)
% 63.24/63.43 [20]P1(x201,x202)+~P2(x201,x202,a8)
% 63.24/63.43 [21]P1(x211,x212)+~P2(x212,x213,x211)
% 63.24/63.43 [18]~P1(x182,x181)+~P1(x181,x182)+E(x181,x182)
% 63.24/63.43 [22]~P2(x223,x224,x221)+E(x221,x222)+~P2(x223,x224,x222)
% 63.24/63.43 [23]~P2(x238,x237,x235)+P1(x231,x232)+~P2(x233,x234,x231)+~P2(x235,x236,x232)+~P2(x237,x236,x234)+~P2(x238,x236,x233)
% 63.24/63.43 %EqnAxiom
% 63.24/63.43 [1]E(x11,x11)
% 63.24/63.43 [2]E(x22,x21)+~E(x21,x22)
% 63.24/63.43 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.24/63.43 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 63.24/63.43 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 63.24/63.43 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 63.24/63.43 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 63.24/63.43 [8]P2(x82,x83,x84)+~E(x81,x82)+~P2(x81,x83,x84)
% 63.24/63.43 [9]P2(x93,x92,x94)+~E(x91,x92)+~P2(x93,x91,x94)
% 63.24/63.43 [10]P2(x103,x104,x102)+~E(x101,x102)+~P2(x103,x104,x101)
% 63.24/63.43
% 63.24/63.43 %-------------------------------------------
% 63.27/63.44 cnf(24,plain,
% 63.27/63.44 (~P2(a6,x241,a3)),
% 63.27/63.44 inference(scs_inference,[],[17,21])).
% 63.27/63.44 cnf(26,plain,
% 63.27/63.44 (~E(a8,a3)),
% 63.27/63.44 inference(scs_inference,[],[17,13,21,6])).
% 63.27/63.44 cnf(27,plain,
% 63.27/63.44 (P1(a8,x271)),
% 63.27/63.44 inference(rename_variables,[],[13])).
% 63.27/63.44 cnf(28,plain,
% 63.27/63.44 (~E(a4,a6)),
% 63.27/63.44 inference(scs_inference,[],[17,12,13,21,6,7])).
% 63.27/63.44 cnf(30,plain,
% 63.27/63.44 (~P1(a3,a8)),
% 63.27/63.44 inference(scs_inference,[],[17,12,13,27,21,6,7,18])).
% 63.27/63.44 cnf(33,plain,
% 63.27/63.44 (~E(a1,a6)),
% 63.27/63.44 inference(scs_inference,[],[17,12,13,27,14,21,6,7,18,8])).
% 63.27/63.44 cnf(35,plain,
% 63.27/63.44 (P2(x351,x352,f7(x351,x352))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(36,plain,
% 63.27/63.44 (P2(x361,x362,f7(x361,x363))+~E(x363,x362)),
% 63.27/63.44 inference(scs_inference,[],[17,16,35,12,13,27,14,21,6,7,18,8,10,9])).
% 63.27/63.44 cnf(43,plain,
% 63.27/63.44 (~P2(a8,x431,a3)),
% 63.27/63.44 inference(scs_inference,[],[30,21])).
% 63.27/63.44 cnf(45,plain,
% 63.27/63.44 (E(a6,f7(a2,a5))),
% 63.27/63.44 inference(scs_inference,[],[15,30,16,21,22])).
% 63.27/63.44 cnf(46,plain,
% 63.27/63.44 (P2(x461,x462,f7(x461,x462))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(48,plain,
% 63.27/63.44 (P2(f7(a2,a5),x481,f7(a6,x481))),
% 63.27/63.44 inference(scs_inference,[],[15,30,16,46,21,22,8])).
% 63.27/63.44 cnf(49,plain,
% 63.27/63.44 (P2(x491,x492,f7(x491,x492))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(50,plain,
% 63.27/63.44 (P2(x501,f7(a2,a5),f7(x501,a6))),
% 63.27/63.44 inference(scs_inference,[],[15,30,16,46,49,21,22,8,9])).
% 63.27/63.44 cnf(51,plain,
% 63.27/63.44 (P2(x511,x512,f7(x511,x512))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(52,plain,
% 63.27/63.44 (~E(f7(a6,x521),a3)),
% 63.27/63.44 inference(scs_inference,[],[24,15,30,16,46,49,51,21,22,8,9,10])).
% 63.27/63.44 cnf(54,plain,
% 63.27/63.44 (E(f7(a2,a5),a6)),
% 63.27/63.44 inference(scs_inference,[],[24,15,30,16,46,49,51,21,22,8,9,10,2])).
% 63.27/63.44 cnf(55,plain,
% 63.27/63.44 (~E(a4,f7(a2,a5))),
% 63.27/63.44 inference(scs_inference,[],[24,15,28,30,16,46,49,51,21,22,8,9,10,2,3])).
% 63.27/63.44 cnf(63,plain,
% 63.27/63.44 (P2(x631,a6,f7(x631,f7(a2,a5)))),
% 63.27/63.44 inference(scs_inference,[],[54,36])).
% 63.27/63.44 cnf(64,plain,
% 63.27/63.44 (E(f7(x641,a6),f7(x641,f7(a2,a5)))),
% 63.27/63.44 inference(scs_inference,[],[50,54,16,36,22])).
% 63.27/63.44 cnf(67,plain,
% 63.27/63.44 (~E(a1,f7(a2,a5))),
% 63.27/63.44 inference(scs_inference,[],[50,54,33,16,36,22,3])).
% 63.27/63.44 cnf(70,plain,
% 63.27/63.44 (P2(a6,f7(a2,a5),f7(f7(a2,a5),a6))),
% 63.27/63.44 inference(scs_inference,[],[50,48,54,33,16,36,22,3,9,8])).
% 63.27/63.44 cnf(85,plain,
% 63.27/63.44 (E(f7(x851,f7(a2,a5)),f7(x851,a6))),
% 63.27/63.44 inference(scs_inference,[],[64,2])).
% 63.27/63.44 cnf(93,plain,
% 63.27/63.44 (P2(f7(a2,a5),f7(a2,a5),f7(a6,a6))),
% 63.27/63.44 inference(scs_inference,[],[45,54,64,63,70,48,50,2,22,3,9,8])).
% 63.27/63.44 cnf(141,plain,
% 63.27/63.44 (~E(f7(a8,x1411),a3)),
% 63.27/63.44 inference(scs_inference,[],[43,16,10])).
% 63.27/63.44 cnf(149,plain,
% 63.27/63.44 (P2(a1,a5,x1491)+~E(a3,x1491)),
% 63.27/63.44 inference(scs_inference,[],[14,10])).
% 63.27/63.44 cnf(171,plain,
% 63.27/63.44 (E(a3,f7(a1,a5))),
% 63.27/63.44 inference(scs_inference,[],[14,16,22])).
% 63.27/63.44 cnf(174,plain,
% 63.27/63.44 (P2(x1741,f7(a1,a5),f7(x1741,a3))),
% 63.27/63.44 inference(scs_inference,[],[14,16,22,36])).
% 63.27/63.44 cnf(175,plain,
% 63.27/63.44 (E(f7(a1,a5),a3)),
% 63.27/63.44 inference(scs_inference,[],[14,16,22,36,2])).
% 63.27/63.44 cnf(176,plain,
% 63.27/63.44 (~E(a8,f7(a1,a5))),
% 63.27/63.44 inference(scs_inference,[],[14,26,16,22,36,2,3])).
% 63.27/63.44 cnf(177,plain,
% 63.27/63.44 (P2(f7(a2,a5),f7(a1,a5),f7(a6,a3))),
% 63.27/63.44 inference(scs_inference,[],[14,26,45,16,22,36,2,3,8])).
% 63.27/63.44 cnf(227,plain,
% 63.27/63.44 (~P2(a2,a5,a4)),
% 63.27/63.44 inference(scs_inference,[],[16,55,22])).
% 63.27/63.44 cnf(228,plain,
% 63.27/63.44 (P2(x2281,x2282,f7(x2281,x2282))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(231,plain,
% 63.27/63.44 (~P1(a4,a6)),
% 63.27/63.44 inference(scs_inference,[],[16,15,12,55,22,10,18])).
% 63.27/63.44 cnf(239,plain,
% 63.27/63.44 (~P2(a6,x2391,a4)),
% 63.27/63.44 inference(scs_inference,[],[16,228,17,15,12,63,55,22,10,18,23,21])).
% 63.27/63.44 cnf(243,plain,
% 63.27/63.44 (P2(x2431,x2432,f7(x2431,x2432))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(245,plain,
% 63.27/63.44 (~E(f7(a6,x2451),a4)),
% 63.27/63.44 inference(scs_inference,[],[16,243,239,176,22,10])).
% 63.27/63.44 cnf(247,plain,
% 63.27/63.44 (~P1(a1,a5)),
% 63.27/63.44 inference(scs_inference,[],[16,243,239,176,22,10,19])).
% 63.27/63.44 cnf(250,plain,
% 63.27/63.44 (~P2(a5,x2501,a1)),
% 63.27/63.44 inference(scs_inference,[],[16,243,239,176,22,10,19,149,21])).
% 63.27/63.44 cnf(262,plain,
% 63.27/63.44 (P2(x2621,x2622,f7(x2621,x2622))),
% 63.27/63.44 inference(rename_variables,[],[16])).
% 63.27/63.44 cnf(264,plain,
% 63.27/63.44 (~E(f7(a5,x2641),a1)),
% 63.27/63.44 inference(scs_inference,[],[16,262,250,12,67,245,18,22,10])).
% 63.27/63.44 cnf(343,plain,
% 63.27/63.44 (~P2(a1,a5,f7(a6,x3431))),
% 63.27/63.44 inference(scs_inference,[],[52,14,175,3,22])).
% 63.27/63.44 cnf(427,plain,
% 63.27/63.44 (~P2(a1,a5,f7(a8,x4271))),
% 63.27/63.44 inference(scs_inference,[],[141,14,22])).
% 63.27/63.44 cnf(433,plain,
% 63.27/63.44 (~E(a8,a1)),
% 63.27/63.44 inference(scs_inference,[],[141,14,48,175,343,22,3,8,4])).
% 63.27/63.44 cnf(436,plain,
% 63.27/63.44 (~E(a3,f7(a8,x4361))),
% 63.27/63.44 inference(scs_inference,[],[427,149])).
% 63.27/63.44 cnf(441,plain,
% 63.27/63.44 (P2(f7(a1,a5),a6,f7(a3,a6))),
% 63.27/63.44 inference(scs_inference,[],[171,63,85,8,10])).
% 63.27/63.44 cnf(448,plain,
% 63.27/63.44 (P2(f7(a1,a5),f7(a2,a5),f7(a3,a6))),
% 63.27/63.44 inference(scs_inference,[],[45,441,9])).
% 63.27/63.44 cnf(493,plain,
% 63.27/63.44 (~P1(f7(a1,a5),a8)),
% 63.27/63.44 inference(scs_inference,[],[176,13,18])).
% 63.27/63.44 cnf(536,plain,
% 63.27/63.44 (~E(f7(a2,a5),a4)),
% 63.27/63.44 inference(scs_inference,[],[227,16,10])).
% 63.27/63.44 cnf(541,plain,
% 63.27/63.44 (~E(a8,a4)),
% 63.27/63.44 inference(scs_inference,[],[231,13,6])).
% 63.27/63.44 cnf(547,plain,
% 63.27/63.44 (~P1(a4,a8)),
% 63.27/63.44 inference(scs_inference,[],[541,13,18])).
% 63.27/63.44 cnf(550,plain,
% 63.27/63.44 (~P2(a8,x5501,a4)),
% 63.27/63.44 inference(scs_inference,[],[541,13,18,21])).
% 63.27/63.44 cnf(564,plain,
% 63.27/63.44 (~E(a4,a5)),
% 63.27/63.44 inference(scs_inference,[],[247,12,7])).
% 63.27/63.44 cnf(663,plain,
% 63.27/63.44 (~P1(a1,a8)),
% 63.27/63.44 inference(scs_inference,[],[433,13,18])).
% 63.27/63.44 cnf(666,plain,
% 63.27/63.44 (~P2(a8,x6661,a1)),
% 63.27/63.44 inference(scs_inference,[],[433,13,18,21])).
% 63.27/63.44 cnf(797,plain,
% 63.27/63.44 (~P1(a4,f7(a2,a5))),
% 63.27/63.44 inference(scs_inference,[],[536,12,18])).
% 63.27/63.44 cnf(815,plain,
% 63.27/63.44 (~E(f7(a8,x8151),a4)),
% 63.27/63.44 inference(scs_inference,[],[550,16,10])).
% 63.27/63.44 cnf(834,plain,
% 63.27/63.44 (~E(a2,a8)),
% 63.27/63.44 inference(scs_inference,[],[663,11,7])).
% 63.27/63.44 cnf(853,plain,
% 63.27/63.44 (~E(f7(a8,x8531),a1)),
% 63.27/63.44 inference(scs_inference,[],[666,16,10])).
% 63.27/63.44 cnf(870,plain,
% 63.27/63.44 (~P1(a4,f7(a8,x8701))),
% 63.27/63.44 inference(scs_inference,[],[815,12,18])).
% 63.27/63.44 cnf(2472,plain,
% 63.27/63.44 (P1(f7(a1,a5),a6)+~E(f7(a3,a6),a8)),
% 63.27/63.44 inference(scs_inference,[],[441,10,20])).
% 63.27/63.44 cnf(2487,plain,
% 63.27/63.44 (P2(a8,x24871,a8)),
% 63.27/63.44 inference(scs_inference,[],[13,19])).
% 63.27/63.44 cnf(2489,plain,
% 63.27/63.44 (~P2(a3,a6,a8)),
% 63.27/63.44 inference(scs_inference,[],[17,13,19,20])).
% 63.27/63.44 cnf(2491,plain,
% 63.27/63.44 (P1(f7(a6,a3),f7(a2,a5))),
% 63.27/63.44 inference(scs_inference,[],[17,177,13,19,20,21])).
% 63.27/63.44 cnf(2494,plain,
% 63.27/63.44 (~P1(a4,a5)),
% 63.27/63.44 inference(scs_inference,[],[17,564,177,13,12,19,20,21,2,18])).
% 63.27/63.44 cnf(2497,plain,
% 63.27/63.44 (~P1(f7(a1,a5),a6)),
% 63.27/63.44 inference(scs_inference,[],[17,564,177,13,12,175,19,20,21,2,18,6])).
% 63.27/63.44 cnf(2504,plain,
% 63.27/63.44 (~E(f7(a3,a6),a8)),
% 63.27/63.44 inference(scs_inference,[],[2497,2472])).
% 63.27/63.44 cnf(2505,plain,
% 63.27/63.44 (P2(f7(a6,a3),f7(a2,a5),a8)),
% 63.27/63.44 inference(scs_inference,[],[2491,19])).
% 63.27/63.44 cnf(2507,plain,
% 63.27/63.44 (~P2(a4,a5,a8)),
% 63.27/63.44 inference(scs_inference,[],[2494,2491,19,20])).
% 63.27/63.44 cnf(2509,plain,
% 63.27/63.44 (P1(f7(a6,a6),f7(a2,a5))),
% 63.27/63.44 inference(scs_inference,[],[2494,2491,93,19,20,21])).
% 63.27/63.44 cnf(2512,plain,
% 63.27/63.44 (~P2(f7(a6,a3),f7(a2,a5),a3)),
% 63.27/63.44 inference(scs_inference,[],[2494,2491,264,26,93,19,20,21,2,22])).
% 63.27/63.44 cnf(2514,plain,
% 63.27/63.44 (~P2(a3,f7(a2,a5),a8)),
% 63.27/63.44 inference(scs_inference,[],[2489,2494,2491,264,26,93,54,19,20,21,2,22,9])).
% 63.27/63.44 cnf(2527,plain,
% 63.27/63.44 (P2(f7(a6,a6),f7(a2,a5),a8)),
% 63.27/63.44 inference(scs_inference,[],[2509,797,20,19])).
% 63.27/63.44 cnf(2529,plain,
% 63.27/63.44 (P1(f7(x25291,a3),x25291)),
% 63.27/63.44 inference(scs_inference,[],[2509,797,174,20,19,21])).
% 63.27/63.44 cnf(2531,plain,
% 63.27/63.44 (~E(a8,f7(a3,a6))),
% 63.27/63.44 inference(scs_inference,[],[2509,2504,797,174,20,19,21,2])).
% 63.27/63.44 cnf(2534,plain,
% 63.27/63.44 (~P1(f7(a3,a6),a8)),
% 63.27/63.44 inference(scs_inference,[],[2509,2504,2505,433,797,174,13,20,19,21,2,22,18])).
% 63.27/63.44 cnf(2538,plain,
% 63.27/63.44 (~P2(f7(a6,a3),f7(a2,a5),f7(a1,a5))),
% 63.27/63.44 inference(scs_inference,[],[2509,2504,2505,2512,2514,433,797,174,13,175,20,19,21,2,22,18,8,10])).
% 63.27/63.44 cnf(2542,plain,
% 63.27/63.44 (P2(f7(x25421,a3),x25421,a8)),
% 63.27/63.44 inference(scs_inference,[],[2529,19])).
% 63.27/63.44 cnf(2546,plain,
% 63.27/63.44 (P1(f7(x25461,a6),x25461)),
% 63.27/63.45 inference(scs_inference,[],[2529,2534,50,19,20,21])).
% 63.27/63.45 cnf(2548,plain,
% 63.27/63.45 (~E(a1,f7(a8,x25481))),
% 63.27/63.45 inference(scs_inference,[],[2529,2534,853,50,19,20,21,2])).
% 63.27/63.45 cnf(2549,plain,
% 63.27/63.45 (~P2(f7(a6,a6),f7(a2,a5),f7(a3,a6))),
% 63.27/63.45 inference(scs_inference,[],[2529,2527,2531,2534,853,50,19,20,21,2,22])).
% 63.27/63.45 cnf(2551,plain,
% 63.27/63.45 (~P1(a2,a8)),
% 63.27/63.45 inference(scs_inference,[],[2529,2527,2531,2534,853,834,50,13,19,20,21,2,22,18])).
% 63.27/63.45 cnf(2555,plain,
% 63.27/63.45 (P1(f7(a3,a3),f7(a1,a5))),
% 63.27/63.45 inference(scs_inference,[],[2538,2529,2527,2531,2534,853,834,50,13,45,171,19,20,21,2,22,18,9,7])).
% 63.27/63.45 cnf(2559,plain,
% 63.27/63.45 (~P2(a2,a8,a8)),
% 63.27/63.45 inference(scs_inference,[],[2551,20])).
% 63.27/63.45 cnf(2561,plain,
% 63.27/63.45 (P2(f7(a3,a3),f7(a1,a5),a8)),
% 63.27/63.45 inference(scs_inference,[],[2551,2555,20,19])).
% 63.27/63.45 cnf(2563,plain,
% 63.27/63.45 (P1(f7(a3,a6),f7(a1,a5))),
% 63.27/63.45 inference(scs_inference,[],[2551,2555,448,20,19,21])).
% 63.27/63.45 cnf(2565,plain,
% 63.27/63.45 (~E(a8,a2)),
% 63.27/63.45 inference(scs_inference,[],[2551,2555,834,448,20,19,21,2])).
% 63.27/63.45 cnf(2568,plain,
% 63.27/63.45 (E(a8,f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2551,2555,2546,2542,541,834,13,448,20,19,21,2,22,18])).
% 63.27/63.45 cnf(2569,plain,
% 63.27/63.45 (P1(f7(x25691,a6),x25691)),
% 63.27/63.45 inference(rename_variables,[],[2546])).
% 63.27/63.45 cnf(2573,plain,
% 63.27/63.45 (~E(f7(a8,a6),a2)),
% 63.27/63.45 inference(scs_inference,[],[2551,2555,2549,2546,2569,2542,541,834,13,448,45,20,19,21,2,22,18,9,6])).
% 63.27/63.45 cnf(2579,plain,
% 63.27/63.45 (P2(f7(a3,a6),f7(a1,a5),a8)),
% 63.27/63.45 inference(scs_inference,[],[2563,19])).
% 63.27/63.45 cnf(2583,plain,
% 63.27/63.45 (P1(f7(a6,x25831),f7(a2,a5))),
% 63.27/63.45 inference(scs_inference,[],[2563,547,48,19,20,21])).
% 63.27/63.45 cnf(2585,plain,
% 63.27/63.45 (~E(a2,f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2563,2573,547,48,19,20,21,2])).
% 63.27/63.45 cnf(2588,plain,
% 63.27/63.45 (P1(f7(a8,a6),x25881)),
% 63.27/63.45 inference(scs_inference,[],[2565,2563,2561,2573,2568,547,13,48,19,20,21,2,22,6])).
% 63.27/63.45 cnf(2599,plain,
% 63.27/63.45 (P2(f7(a8,a6),x25991,a8)),
% 63.27/63.45 inference(scs_inference,[],[2588,493,20,19])).
% 63.27/63.45 cnf(2601,plain,
% 63.27/63.45 (P1(a3,a1)),
% 63.27/63.45 inference(scs_inference,[],[2588,493,14,20,19,21])).
% 63.27/63.45 cnf(2605,plain,
% 63.27/63.45 (~P1(a2,f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2588,2579,2585,2565,493,14,20,19,21,22,18])).
% 63.27/63.45 cnf(2606,plain,
% 63.27/63.45 (P1(f7(a8,a6),x26061)),
% 63.27/63.45 inference(rename_variables,[],[2588])).
% 63.27/63.45 cnf(2608,plain,
% 63.27/63.45 (~E(f7(a8,a6),f7(a3,a6))),
% 63.27/63.45 inference(scs_inference,[],[2588,2606,2579,2585,2565,2534,493,14,20,19,21,22,18,6])).
% 63.27/63.45 cnf(2617,plain,
% 63.27/63.45 (P2(a3,a1,a8)),
% 63.27/63.45 inference(scs_inference,[],[2601,19])).
% 63.27/63.45 cnf(2621,plain,
% 63.27/63.45 (P1(a6,a2)),
% 63.27/63.45 inference(scs_inference,[],[2601,2605,15,19,20,21])).
% 63.27/63.45 cnf(2625,plain,
% 63.27/63.45 (~P1(f7(a3,a6),f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2601,2608,2599,2605,2531,2588,15,19,20,21,22,18])).
% 63.27/63.45 cnf(2634,plain,
% 63.27/63.45 (P2(a6,a2,a8)),
% 63.27/63.45 inference(scs_inference,[],[2621,2625,20,19])).
% 63.27/63.45 cnf(2636,plain,
% 63.27/63.45 (P1(f7(x26361,x26362),x26361)),
% 63.27/63.45 inference(scs_inference,[],[2621,2625,16,20,19,21])).
% 63.27/63.45 cnf(2638,plain,
% 63.27/63.45 (~P2(a3,a1,a3)),
% 63.27/63.45 inference(scs_inference,[],[2617,2621,2625,26,16,20,19,21,22])).
% 63.27/63.45 cnf(2669,plain,
% 63.27/63.45 (P2(f7(x26691,x26692),x26691,a8)),
% 63.27/63.45 inference(scs_inference,[],[2636,19])).
% 63.27/63.45 cnf(2675,plain,
% 63.27/63.45 (~P1(a3,f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2634,2636,436,433,2588,870,19,20,22,18])).
% 63.27/63.45 cnf(2682,plain,
% 63.27/63.45 (~E(a4,f7(a5,x26821))),
% 63.27/63.45 inference(scs_inference,[],[2634,2638,2636,436,433,2494,2588,870,175,19,20,22,18,6,10,2])).
% 63.27/63.45 cnf(2687,plain,
% 63.27/63.45 (P2(f7(a6,x26871),f7(a2,a5),a8)),
% 63.27/63.45 inference(scs_inference,[],[2583,2675,20,19])).
% 63.27/63.45 cnf(2689,plain,
% 63.27/63.45 (~P2(f7(x26891,x26892),x26891,a4)),
% 63.27/63.45 inference(scs_inference,[],[2583,2669,2675,541,20,19,22])).
% 63.27/63.45 cnf(2691,plain,
% 63.27/63.45 (~P1(a4,f7(a5,x26911))),
% 63.27/63.45 inference(scs_inference,[],[2583,2669,2675,2682,541,12,20,19,22,18])).
% 63.27/63.45 cnf(2705,plain,
% 63.27/63.45 (~P1(a1,f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2687,2691,2548,2565,2588,12,19,20,22,18])).
% 63.27/63.45 cnf(2710,plain,
% 63.27/63.45 (~P2(f7(x27101,x27102),x27101,a4)),
% 63.27/63.45 inference(rename_variables,[],[2689])).
% 63.27/63.45 cnf(2716,plain,
% 63.27/63.45 (~P1(f7(a1,a5),f7(a8,a6))),
% 63.27/63.45 inference(scs_inference,[],[2689,2710,2687,2691,2548,2675,2605,2565,2588,93,50,12,175,171,19,20,22,18,9,8,23,6])).
% 63.27/63.45 cnf(2717,plain,
% 63.27/63.45 (P1(f7(a3,x27171),f7(a1,a5))),
% 63.27/63.45 inference(scs_inference,[],[2689,2710,2687,2691,2548,2675,2605,2636,2565,2588,93,50,12,175,171,19,20,22,18,9,8,23,6,7])).
% 63.27/63.45 cnf(2721,plain,
% 63.27/63.45 (P2(f7(a3,x27211),f7(a1,a5),a8)),
% 63.27/63.45 inference(scs_inference,[],[2716,2717,20,19])).
% 63.27/63.45 cnf(2739,plain,
% 63.27/63.45 (P2(a1,a2,a8)),
% 63.27/63.45 inference(scs_inference,[],[2705,11,20,19])).
% 63.27/63.45 cnf(3092,plain,
% 63.27/63.45 (~E(a8,f7(a4,a5))),
% 63.27/63.45 inference(scs_inference,[],[2507,16,10,2])).
% 63.27/63.45 cnf(3160,plain,
% 63.27/63.45 (~E(f7(a2,a8),a8)),
% 63.27/63.45 inference(scs_inference,[],[2559,3092,2599,16,22,10])).
% 63.27/63.45 cnf(3162,plain,
% 63.27/63.45 (~E(a8,f7(a2,a8))),
% 63.27/63.45 inference(scs_inference,[],[2559,3092,2599,16,22,10,2])).
% 63.27/63.45 cnf(3171,plain,
% 63.27/63.45 (~E(f7(a8,a6),f7(a2,a8))),
% 63.27/63.45 inference(scs_inference,[],[3160,3162,2568,2721,13,22,18,3])).
% 63.27/63.45 cnf(3175,plain,
% 63.27/63.45 (~E(f7(a8,x31751),f7(a3,a6))),
% 63.27/63.45 inference(scs_inference,[],[3160,3162,2568,2636,2721,2534,13,22,18,3,20,2,6])).
% 63.27/63.45 cnf(3191,plain,
% 63.27/63.45 (~P2(a2,a5,f7(a2,a5))),
% 63.27/63.45 inference(scs_inference,[],[3171,3175,3162,2588,2669,2739,2487,2534,448,16,2,22,18,20,3,23])).
% 63.27/63.45 cnf(3196,plain,
% 63.27/63.45 ($false),
% 63.27/63.45 inference(scs_inference,[],[3191,16]),
% 63.27/63.45 ['proof']).
% 63.27/63.45 % SZS output end Proof
% 63.27/63.45 % Total time :62.680000s
%------------------------------------------------------------------------------