%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC379+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:06:11 PM UTC 2026
% Result : Theorem 21.74s 4.25s
% Output : Proof 21.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 1
% Syntax : Number of formulae : 125 ( 11 unt; 0 def)
% Number of atoms : 506 ( 92 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 531 ( 150 ~; 305 |; 62 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-1 aty)
% Number of variables : 45 ( 0 sgn 20 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X1] :
( ssItem(X1)
=> ( ( memberP(U,X1)
& memberP(V,X1)
& ! [X2] :
( ssItem(X2)
=> ( X1 = X2
| ~ leq(X2,X1)
| ~ memberP(V,X2) ) ) )
| ( ( ? [X2] :
( leq(X2,X1)
& memberP(V,X2)
& X1 != X2
& ssItem(X2) )
| ~ memberP(V,X1) )
& ~ memberP(U,X1) ) ) )
| ? [Y] :
( ( ( ( ? [Z] :
( leq(Z,Y)
& memberP(X,Z)
& Y != Z
& ssItem(Z) )
| ~ memberP(X,Y) )
& memberP(W,Y) )
| ( memberP(X,Y)
& ! [Z] :
( ssItem(Z)
=> ( Y = Z
| ~ leq(Z,Y)
| ~ memberP(X,Z) ) )
& ~ memberP(W,Y) ) )
& ssItem(Y) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f95_neg,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X1] :
( ssItem(X1)
=> ( ( memberP(U,X1)
& memberP(V,X1)
& ! [X2] :
( ssItem(X2)
=> ( X1 = X2
| ~ leq(X2,X1)
| ~ memberP(V,X2) ) ) )
| ( ( ? [X2] :
( leq(X2,X1)
& memberP(V,X2)
& X1 != X2
& ssItem(X2) )
| ~ memberP(V,X1) )
& ~ memberP(U,X1) ) ) )
| ? [Y] :
( ( ( ( ? [Z] :
( leq(Z,Y)
& memberP(X,Z)
& Y != Z
& ssItem(Z) )
| ~ memberP(X,Y) )
& memberP(W,Y) )
| ( memberP(X,Y)
& ! [Z] :
( ssItem(Z)
=> ( Y = Z
| ~ leq(Z,Y)
| ~ memberP(X,Z) ) )
& ~ memberP(W,Y) ) )
& ssItem(Y) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f95_nnf,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [X1] :
( ( ~ memberP(U,X1)
| ~ memberP(V,X1)
| ? [X2] :
( X1 != X2
& leq(X2,X1)
& memberP(V,X2)
& ssItem(X2) ) )
& ( ( ! [X2] :
( ~ leq(X2,X1)
| ~ memberP(V,X2)
| X1 = X2
| ~ ssItem(X2) )
& memberP(V,X1) )
| memberP(U,X1) )
& ssItem(X1) )
& ! [Y] :
( ( ( ( ! [Z] :
( ~ leq(Z,Y)
| ~ memberP(X,Z)
| Y = Z
| ~ ssItem(Z) )
& memberP(X,Y) )
| ~ memberP(W,Y) )
& ( ~ memberP(X,Y)
| ? [Z] :
( Y != Z
& leq(Z,Y)
& memberP(X,Z)
& ssItem(Z) )
| memberP(W,Y) ) )
| ~ ssItem(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(nnf_transformation,[status(thm)],[f95_neg]) ).
fof(f95_sk,plain,
! [Y,Z,X2] :
( ( ~ memberP(sk47,sk52)
| ~ memberP(sk48,sk52)
| ( sk52 != sk53
& leq(sk53,sk52)
& memberP(sk48,sk53)
& ssItem(sk53) ) )
& ( ( ( ~ leq(X2,sk52)
| ~ memberP(sk48,X2)
| sk52 = X2
| ~ ssItem(X2) )
& memberP(sk48,sk52) )
| memberP(sk47,sk52) )
& ssItem(sk52)
& ( ( ( ( ( ~ leq(Z,Y)
| ~ memberP(sk50,Z)
| Y = Z
| ~ ssItem(Z) )
& memberP(sk50,Y) )
| ~ memberP(sk49,Y) )
& ( ~ memberP(sk50,Y)
| ( Y != sk51(Y)
& leq(sk51(Y),Y)
& memberP(sk50,sk51(Y))
& ssItem(sk51(Y)) )
| memberP(sk49,Y) ) )
| ~ ssItem(Y) )
& sk47 = sk49
& sk48 = sk50
& ssList(sk50)
& ssList(sk49)
& ssList(sk48)
& ssList(sk47) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47,sk48,sk49,sk50,sk51,sk52,sk53])],[f95_nnf]) ).
cnf(c194,plain,
sk48 = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c195,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c204,plain,
( ~ leq(X7,sk52)
| ~ memberP(sk48,X7)
| sk52 = X7
| ~ ssItem(X7)
| memberP(sk47,sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c203,plain,
( memberP(sk48,sk52)
| memberP(sk47,sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c196,plain,
( ~ memberP(sk50,X4)
| ssItem(sk51(X4))
| memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c202,plain,
ssItem(sk52),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p211,plain,
( ~ memberP(sk50,sk52)
| ssItem(sk51(sk52))
| memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[c196,c202]) ).
cnf(p212,plain,
( ~ memberP(sk48,sk52)
| ssItem(sk51(sk52))
| memberP(sk49,sk52) ),
inference(superposition,[status(thm)],[c194,p211]) ).
cnf(p216,plain,
( ssItem(sk51(sk52))
| memberP(sk49,sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[c203,p212]) ).
cnf(p217,plain,
( ssItem(sk51(sk52))
| memberP(sk47,sk52)
| memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c195,p216]) ).
cnf(p219,plain,
( ssItem(sk51(sk52))
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p217]) ).
cnf(c200,plain,
( memberP(sk50,X4)
| ~ memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p209,plain,
( memberP(sk50,sk52)
| ~ memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[c200,c202]) ).
cnf(p210,plain,
( memberP(sk50,sk52)
| ~ memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c195,p209]) ).
cnf(p220,plain,
( memberP(sk50,sk52)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p219,p210]) ).
cnf(p221,plain,
( memberP(sk48,sk52)
| ssItem(sk51(sk52)) ),
inference(superposition,[status(thm)],[c194,p220]) ).
cnf(c205,plain,
( ~ memberP(sk47,sk52)
| ~ memberP(sk48,sk52)
| ssItem(sk53) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p224,plain,
( ~ memberP(sk47,sk52)
| ssItem(sk53)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p221,c205]) ).
cnf(p227,plain,
( ssItem(sk51(sk52))
| ssItem(sk53)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p224,p219]) ).
cnf(p228,plain,
( ssItem(sk53)
| ssItem(sk51(sk52)) ),
inference(factoring,[status(thm)],[p227]) ).
cnf(p247,plain,
( ssItem(sk53)
| ~ leq(sk51(sk52),sk52)
| ~ memberP(sk48,sk51(sk52))
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[c204,p228]) ).
cnf(c197,plain,
( ~ memberP(sk50,X4)
| memberP(sk50,sk51(X4))
| memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p213,plain,
( ~ memberP(sk50,sk52)
| memberP(sk50,sk51(sk52))
| memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[c197,c202]) ).
cnf(p214,plain,
( ~ memberP(sk48,sk52)
| memberP(sk50,sk51(sk52))
| memberP(sk49,sk52) ),
inference(superposition,[status(thm)],[c194,p213]) ).
cnf(p238,plain,
( memberP(sk47,sk52)
| memberP(sk50,sk51(sk52))
| memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[p214,c203]) ).
cnf(p241,plain,
( memberP(sk47,sk52)
| memberP(sk48,sk51(sk52))
| memberP(sk49,sk52) ),
inference(superposition,[status(thm)],[c194,p238]) ).
cnf(p257,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| ~ leq(sk51(sk52),sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p247,p241]) ).
cnf(p261,plain,
( memberP(sk49,sk52)
| ssItem(sk53)
| ~ leq(sk51(sk52),sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p257]) ).
cnf(c198,plain,
( ~ memberP(sk50,X4)
| leq(sk51(X4),X4)
| memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p215,plain,
( ~ memberP(sk50,sk52)
| leq(sk51(sk52),sk52)
| memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[c198,c202]) ).
cnf(p239,plain,
( ~ memberP(sk48,sk52)
| leq(sk51(sk52),sk52)
| memberP(sk49,sk52) ),
inference(superposition,[status(thm)],[c194,p215]) ).
cnf(p242,plain,
( memberP(sk47,sk52)
| leq(sk51(sk52),sk52)
| memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[p239,c203]) ).
cnf(p262,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p261,p242]) ).
cnf(p263,plain,
( memberP(sk49,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p262]) ).
cnf(p265,plain,
( memberP(sk49,sk52)
| ssItem(sk53)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p263]) ).
cnf(c199,plain,
( ~ memberP(sk50,X4)
| X4 != sk51(X4)
| memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p243,plain,
( ~ memberP(sk50,sk52)
| sk52 != sk51(sk52)
| memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[c199,c202]) ).
cnf(p268,plain,
( ~ memberP(sk50,sk52)
| memberP(sk49,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p265,p243]) ).
cnf(p275,plain,
( ~ memberP(sk50,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p268]) ).
cnf(p276,plain,
( ~ memberP(sk48,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c194,p275]) ).
cnf(p277,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| ssItem(sk53)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p276,c203]) ).
cnf(p278,plain,
( memberP(sk49,sk52)
| ssItem(sk53)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p277]) ).
cnf(p279,plain,
( memberP(sk47,sk52)
| ssItem(sk53)
| memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c195,p278]) ).
cnf(p282,plain,
( ssItem(sk53)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p283,plain,
( memberP(sk50,sk52)
| ssItem(sk53) ),
inference(resolution,[status(thm)],[p282,p210]) ).
cnf(p285,plain,
( memberP(sk48,sk52)
| ssItem(sk53) ),
inference(superposition,[status(thm)],[c194,p283]) ).
cnf(p288,plain,
( ~ memberP(sk47,sk52)
| ssItem(sk53)
| ssItem(sk53) ),
inference(resolution,[status(thm)],[p285,c205]) ).
cnf(p291,plain,
( ~ memberP(sk47,sk52)
| ssItem(sk53) ),
inference(factoring,[status(thm)],[p288]) ).
cnf(p292,plain,
( ssItem(sk53)
| ssItem(sk53) ),
inference(resolution,[status(thm)],[p291,p282]) ).
cnf(p293,plain,
ssItem(sk53),
inference(factoring,[status(thm)],[p292]) ).
cnf(c201,plain,
( ~ leq(X5,X4)
| ~ memberP(sk50,X5)
| X4 = X5
| ~ ssItem(X5)
| ~ memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p253,plain,
( ~ leq(X0,sk52)
| ~ memberP(sk50,X0)
| sk52 = X0
| ~ ssItem(X0)
| ~ memberP(sk49,sk52) ),
inference(resolution,[status(thm)],[c201,c202]) ).
cnf(p222,plain,
( ssItem(sk51(sk52))
| memberP(sk49,sk52)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p220,p211]) ).
cnf(p233,plain,
( memberP(sk49,sk52)
| ssItem(sk51(sk52)) ),
inference(factoring,[status(thm)],[p222]) ).
cnf(p256,plain,
( ssItem(sk51(sk52))
| ~ leq(X0,sk52)
| ~ memberP(sk50,X0)
| sk52 = X0
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p253,p233]) ).
cnf(p301,plain,
( ssItem(sk51(sk52))
| ~ leq(sk53,sk52)
| ~ memberP(sk50,sk53)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p293,p256]) ).
cnf(p312,plain,
( ssItem(sk51(sk52))
| ~ leq(sk53,sk52)
| ~ memberP(sk48,sk53)
| sk52 = sk53 ),
inference(superposition,[status(thm)],[c194,p301]) ).
cnf(c206,plain,
( ~ memberP(sk47,sk52)
| ~ memberP(sk48,sk52)
| memberP(sk48,sk53) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p225,plain,
( ~ memberP(sk47,sk52)
| memberP(sk48,sk53)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p221,c206]) ).
cnf(p234,plain,
( ssItem(sk51(sk52))
| memberP(sk48,sk53)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p225,p219]) ).
cnf(p236,plain,
( memberP(sk48,sk53)
| ssItem(sk51(sk52)) ),
inference(factoring,[status(thm)],[p234]) ).
cnf(p314,plain,
( ssItem(sk51(sk52))
| ssItem(sk51(sk52))
| ~ leq(sk53,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p312,p236]) ).
cnf(p315,plain,
( ssItem(sk51(sk52))
| ~ leq(sk53,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p314]) ).
cnf(c207,plain,
( ~ memberP(sk47,sk52)
| ~ memberP(sk48,sk52)
| leq(sk53,sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p226,plain,
( ~ memberP(sk47,sk52)
| leq(sk53,sk52)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p221,c207]) ).
cnf(p235,plain,
( ssItem(sk51(sk52))
| leq(sk53,sk52)
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p226,p219]) ).
cnf(p237,plain,
( leq(sk53,sk52)
| ssItem(sk51(sk52)) ),
inference(factoring,[status(thm)],[p235]) ).
cnf(p316,plain,
( ssItem(sk51(sk52))
| ssItem(sk51(sk52))
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p315,p237]) ).
cnf(p317,plain,
( ssItem(sk51(sk52))
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p316]) ).
cnf(p323,plain,
( ~ leq(sk51(sk52),sk52)
| ~ memberP(sk48,sk51(sk52))
| sk52 = sk51(sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p317,c204]) ).
cnf(p337,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| ~ leq(sk51(sk52),sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p323,p241]) ).
cnf(p347,plain,
( memberP(sk49,sk52)
| ~ leq(sk51(sk52),sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p337]) ).
cnf(p350,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| memberP(sk49,sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p347,p242]) ).
cnf(p353,plain,
( memberP(sk49,sk52)
| memberP(sk49,sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p350]) ).
cnf(p355,plain,
( memberP(sk49,sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p353]) ).
cnf(p360,plain,
( ~ memberP(sk50,sk52)
| memberP(sk49,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p355,p243]) ).
cnf(p368,plain,
( ~ memberP(sk50,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p360]) ).
cnf(p369,plain,
( ~ memberP(sk48,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(superposition,[status(thm)],[c194,p368]) ).
cnf(p370,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p369,c203]) ).
cnf(p371,plain,
( memberP(sk49,sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p370]) ).
cnf(p372,plain,
( memberP(sk47,sk52)
| memberP(sk47,sk52)
| sk52 = sk53 ),
inference(superposition,[status(thm)],[c195,p371]) ).
cnf(p375,plain,
( memberP(sk47,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p372]) ).
cnf(p255,plain,
( ~ leq(X0,sk52)
| ~ memberP(sk50,X0)
| sk52 = X0
| ~ ssItem(X0)
| ~ memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c195,p253]) ).
cnf(p377,plain,
( ~ leq(X0,sk52)
| ~ memberP(sk50,X0)
| sk52 = X0
| ~ ssItem(X0)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p375,p255]) ).
cnf(p398,plain,
( ~ leq(sk53,sk52)
| ~ memberP(sk50,sk53)
| ~ ssItem(sk53)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p377]) ).
cnf(p403,plain,
( ~ leq(sk53,sk52)
| ~ memberP(sk50,sk53)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p398,p293]) ).
cnf(p404,plain,
( ~ leq(sk53,sk52)
| ~ memberP(sk48,sk53)
| sk52 = sk53 ),
inference(superposition,[status(thm)],[c194,p403]) ).
cnf(p376,plain,
( memberP(sk50,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p375,p210]) ).
cnf(p378,plain,
( memberP(sk48,sk52)
| sk52 = sk53 ),
inference(superposition,[status(thm)],[c194,p376]) ).
cnf(p381,plain,
( ~ memberP(sk47,sk52)
| memberP(sk48,sk53)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p378,c206]) ).
cnf(p383,plain,
( sk52 = sk53
| memberP(sk48,sk53)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p381,p375]) ).
cnf(p385,plain,
( memberP(sk48,sk53)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p383]) ).
cnf(p406,plain,
( sk52 = sk53
| ~ leq(sk53,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p404,p385]) ).
cnf(p407,plain,
( ~ leq(sk53,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p406]) ).
cnf(p382,plain,
( ~ memberP(sk47,sk52)
| leq(sk53,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p378,c207]) ).
cnf(p384,plain,
( sk52 = sk53
| leq(sk53,sk52)
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p382,p375]) ).
cnf(p389,plain,
( leq(sk53,sk52)
| sk52 = sk53 ),
inference(factoring,[status(thm)],[p384]) ).
cnf(p408,plain,
( sk52 = sk53
| sk52 = sk53 ),
inference(resolution,[status(thm)],[p407,p389]) ).
cnf(p409,plain,
sk52 = sk53,
inference(factoring,[status(thm)],[p408]) ).
cnf(c208,plain,
( ~ memberP(sk47,sk52)
| ~ memberP(sk48,sk52)
| sk52 != sk53 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p410,plain,
( ~ memberP(sk47,sk52)
| ~ memberP(sk48,sk52) ),
inference(resolution,[status(thm)],[p409,c208]) ).
cnf(p430,plain,
( ssItem(sk51(sk52))
| ~ memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p410,p221]) ).
cnf(p432,plain,
( ssItem(sk51(sk52))
| ssItem(sk51(sk52)) ),
inference(resolution,[status(thm)],[p430,p219]) ).
cnf(p433,plain,
ssItem(sk51(sk52)),
inference(factoring,[status(thm)],[p432]) ).
cnf(p439,plain,
( ~ leq(sk51(sk52),sk52)
| ~ memberP(sk48,sk51(sk52))
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p433,c204]) ).
cnf(p525,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| ~ leq(sk51(sk52),sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p439,p241]) ).
cnf(p564,plain,
( memberP(sk49,sk52)
| ~ leq(sk51(sk52),sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p525]) ).
cnf(p565,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| memberP(sk49,sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p564,p242]) ).
cnf(p567,plain,
( memberP(sk49,sk52)
| memberP(sk49,sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p565]) ).
cnf(p569,plain,
( memberP(sk49,sk52)
| sk52 = sk51(sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p567]) ).
cnf(p572,plain,
( ~ memberP(sk50,sk52)
| memberP(sk49,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p569,p243]) ).
cnf(p604,plain,
( ~ memberP(sk50,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p572]) ).
cnf(p605,plain,
( ~ memberP(sk48,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c194,p604]) ).
cnf(p606,plain,
( memberP(sk47,sk52)
| memberP(sk49,sk52)
| memberP(sk47,sk52) ),
inference(resolution,[status(thm)],[p605,c203]) ).
cnf(p607,plain,
( memberP(sk49,sk52)
| memberP(sk47,sk52) ),
inference(factoring,[status(thm)],[p606]) ).
cnf(p608,plain,
( memberP(sk47,sk52)
| memberP(sk47,sk52) ),
inference(superposition,[status(thm)],[c195,p607]) ).
cnf(p613,plain,
memberP(sk47,sk52),
inference(factoring,[status(thm)],[p608]) ).
cnf(p614,plain,
memberP(sk50,sk52),
inference(resolution,[status(thm)],[p613,p210]) ).
cnf(p618,plain,
memberP(sk48,sk52),
inference(superposition,[status(thm)],[c194,p614]) ).
cnf(p624,plain,
~ memberP(sk47,sk52),
inference(resolution,[status(thm)],[p618,p410]) ).
cnf(p625,plain,
$false,
inference(resolution,[status(thm)],[p624,p613]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC379+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.43 % Computer : n017.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Thu Sep 24 17:51:32 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.74/4.25 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.74/4.25 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------