%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC343+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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:03 PM UTC 2026
% Result : Theorem 23.03s 8.72s
% Output : Proof 23.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 1
% Syntax : Number of formulae : 97 ( 18 unt; 0 def)
% Number of atoms : 407 ( 189 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 520 ( 210 ~; 234 |; 58 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 84 ( 0 sgn 28 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil = V
| nil != U )
& ? [X4] :
( strictorderedP(U)
& ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssList(X6)
=> ( ! [X7] :
( ssItem(X7)
=> ! [X8] :
( ssList(X8)
=> ( ~ lt(X7,X5)
| app(X8,cons(X7,nil)) != U ) ) )
| app(cons(X5,nil),X6) != X4 ) ) )
& app(U,X4) = V
& ssList(X4) ) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( lt(X2,Z)
& app(X3,cons(X2,nil)) = W
& ssList(X3) )
& ssItem(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ strictorderedP(W)
| app(W,Y) != X ) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f95_neg,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil = V
| nil != U )
& ? [X4] :
( strictorderedP(U)
& ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssList(X6)
=> ( ! [X7] :
( ssItem(X7)
=> ! [X8] :
( ssList(X8)
=> ( ~ lt(X7,X5)
| app(X8,cons(X7,nil)) != U ) ) )
| app(cons(X5,nil),X6) != X4 ) ) )
& app(U,X4) = V
& ssList(X4) ) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( lt(X2,Z)
& app(X3,cons(X2,nil)) = W
& ssList(X3) )
& ssItem(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ strictorderedP(W)
| app(W,Y) != X ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f95_nnf,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( nil != V
& nil = U )
| ! [X4] :
( ~ strictorderedP(U)
| ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( lt(X7,X5)
& app(X8,cons(X7,nil)) = U
& ssList(X8) )
& ssItem(X7) )
& app(cons(X5,nil),X6) = X4
& ssList(X6) )
& ssItem(X5) )
| app(U,X4) != V
| ~ ssList(X4) ) )
& ( nil != W
| nil = X )
& ? [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ~ lt(X2,Z)
| app(X3,cons(X2,nil)) != W
| ~ ssList(X3) )
| ~ ssItem(X2) )
| app(cons(Z,nil),X1) != Y
| ~ ssList(X1) )
| ~ ssItem(Z) )
& strictorderedP(W)
& app(W,Y) = X
& ssList(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(nnf_transformation,[status(thm)],[f95_neg]) ).
fof(f95_sk,plain,
! [Z,X1,X2,X3,X4] :
( ( ( nil != sk48
& nil = sk47 )
| ~ strictorderedP(sk47)
| ( lt(sk54(X4),sk52(X4))
& app(sk55(X4),cons(sk54(X4),nil)) = sk47
& ssList(sk55(X4))
& ssItem(sk54(X4))
& app(cons(sk52(X4),nil),sk53(X4)) = X4
& ssList(sk53(X4))
& ssItem(sk52(X4)) )
| app(sk47,X4) != sk48
| ~ ssList(X4) )
& ( nil != sk49
| nil = sk50 )
& ( ~ lt(X2,Z)
| app(X3,cons(X2,nil)) != sk49
| ~ ssList(X3)
| ~ ssItem(X2)
| app(cons(Z,nil),X1) != sk51
| ~ ssList(X1)
| ~ ssItem(Z) )
& strictorderedP(sk49)
& app(sk49,sk51) = sk50
& ssList(sk51)
& 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,sk54,sk55])],[f95_nnf]) ).
cnf(c211,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk55(X9),cons(sk54(X9),nil)) = sk47
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c196,plain,
ssList(sk51),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p341,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk55(sk51),cons(sk54(sk51),nil)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c211,c196]) ).
cnf(p344,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk55(sk51),cons(sk54(sk51),nil)) = sk47 ),
inference(equality_resolution,[status(thm)],[p341]) ).
cnf(c195,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c198,plain,
strictorderedP(sk49),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p215,plain,
strictorderedP(sk47),
inference(superposition,[status(thm)],[c195,c198]) ).
cnf(p345,plain,
( nil = sk47
| app(sk55(sk51),cons(sk54(sk51),nil)) = sk47 ),
inference(resolution,[status(thm)],[p344,p215]) ).
cnf(c199,plain,
( ~ lt(X7,X5)
| app(X8,cons(X7,nil)) != sk49
| ~ ssList(X8)
| ~ ssItem(X7)
| app(cons(X5,nil),X6) != sk51
| ~ ssList(X6)
| ~ ssItem(X5) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c201,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk52(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p225,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk52(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c201,c196]) ).
cnf(p226,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk52(sk51)) ),
inference(equality_resolution,[status(thm)],[p225]) ).
cnf(p227,plain,
( nil = sk47
| ssItem(sk52(sk51)) ),
inference(resolution,[status(thm)],[p226,p215]) ).
cnf(p363,plain,
( nil = sk47
| ~ lt(X1,sk52(sk51))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk52(sk51),nil),X0) != sk51
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c199,p227]) ).
cnf(c203,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk53(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p239,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk53(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c203,c196]) ).
cnf(p240,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk53(sk51)) ),
inference(equality_resolution,[status(thm)],[p239]) ).
cnf(p241,plain,
( nil = sk47
| ssList(sk53(sk51)) ),
inference(resolution,[status(thm)],[p240,p215]) ).
cnf(p385,plain,
( nil = sk47
| nil = sk47
| ~ lt(X0,sk52(sk51))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk52(sk51),nil),sk53(sk51)) != sk51 ),
inference(resolution,[status(thm)],[p363,p241]) ).
cnf(p405,plain,
( nil = sk47
| ~ lt(X0,sk52(sk51))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk52(sk51),nil),sk53(sk51)) != sk51 ),
inference(factoring,[status(thm)],[p385]) ).
cnf(c205,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk52(X9),nil),sk53(X9)) = X9
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p323,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk52(sk51),nil),sk53(sk51)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c205,c196]) ).
cnf(p326,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk52(sk51),nil),sk53(sk51)) = sk51 ),
inference(equality_resolution,[status(thm)],[p323]) ).
cnf(p327,plain,
( nil = sk47
| app(cons(sk52(sk51),nil),sk53(sk51)) = sk51 ),
inference(resolution,[status(thm)],[p326,p215]) ).
cnf(p406,plain,
( nil = sk47
| nil = sk47
| ~ lt(X0,sk52(sk51))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p405,p327]) ).
cnf(p407,plain,
( nil = sk47
| ~ lt(X0,sk52(sk51))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p406]) ).
cnf(c207,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk54(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p257,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk54(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c207,c196]) ).
cnf(p259,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk54(sk51)) ),
inference(equality_resolution,[status(thm)],[p257]) ).
cnf(p260,plain,
( nil = sk47
| ssItem(sk54(sk51)) ),
inference(resolution,[status(thm)],[p259,p215]) ).
cnf(p409,plain,
( nil = sk47
| nil = sk47
| ~ lt(sk54(sk51),sk52(sk51))
| app(X0,cons(sk54(sk51),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p407,p260]) ).
cnf(p422,plain,
( nil = sk47
| ~ lt(sk54(sk51),sk52(sk51))
| app(X0,cons(sk54(sk51),nil)) != sk49
| ~ ssList(X0) ),
inference(factoring,[status(thm)],[p409]) ).
cnf(c209,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk55(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p273,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk55(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c209,c196]) ).
cnf(p275,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk55(sk51)) ),
inference(equality_resolution,[status(thm)],[p273]) ).
cnf(p276,plain,
( nil = sk47
| ssList(sk55(sk51)) ),
inference(resolution,[status(thm)],[p275,p215]) ).
cnf(p427,plain,
( nil = sk47
| nil = sk47
| ~ lt(sk54(sk51),sk52(sk51))
| app(sk55(sk51),cons(sk54(sk51),nil)) != sk49 ),
inference(resolution,[status(thm)],[p422,p276]) ).
cnf(p432,plain,
( nil = sk47
| ~ lt(sk54(sk51),sk52(sk51))
| app(sk55(sk51),cons(sk54(sk51),nil)) != sk49 ),
inference(factoring,[status(thm)],[p427]) ).
cnf(p434,plain,
( nil = sk47
| ~ lt(sk54(sk51),sk52(sk51))
| sk47 != sk49
| nil = sk47 ),
inference(superposition,[status(thm)],[p345,p432]) ).
cnf(p435,plain,
( ~ lt(sk54(sk51),sk52(sk51))
| sk47 != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p434]) ).
cnf(p436,plain,
( ~ lt(sk54(sk51),sk52(sk51))
| nil = sk47 ),
inference(resolution,[status(thm)],[p435,c195]) ).
cnf(c213,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk54(X9),sk52(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p297,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk54(sk51),sk52(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c213,c196]) ).
cnf(p300,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk54(sk51),sk52(sk51)) ),
inference(equality_resolution,[status(thm)],[p297]) ).
cnf(p301,plain,
( nil = sk47
| lt(sk54(sk51),sk52(sk51)) ),
inference(resolution,[status(thm)],[p300,p215]) ).
cnf(p437,plain,
( nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p436,p301]) ).
cnf(p438,plain,
nil = sk47,
inference(factoring,[status(thm)],[p437]) ).
cnf(c194,plain,
sk48 = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c197,plain,
app(sk49,sk51) = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p217,plain,
sk50 = sk48,
inference(superposition,[status(thm)],[c194,c197]) ).
cnf(c200,plain,
( nil != sk49
| nil = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p216,plain,
( nil != sk47
| nil = sk50 ),
inference(superposition,[status(thm)],[c195,c200]) ).
cnf(p220,plain,
( nil != sk47
| nil = sk48 ),
inference(demodulation,[status(thm)],[p217,p216]) ).
cnf(p441,plain,
nil = sk48,
inference(resolution,[status(thm)],[p438,p220]) ).
cnf(p521,plain,
sk48 = nil,
inference(superposition,[status(thm)],[p441,p217]) ).
cnf(c202,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk52(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p232,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk52(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c202,c196]) ).
cnf(p233,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk52(sk51)) ),
inference(equality_resolution,[status(thm)],[p232]) ).
cnf(p234,plain,
( nil != sk48
| ssItem(sk52(sk51)) ),
inference(resolution,[status(thm)],[p233,p215]) ).
cnf(p524,plain,
( nil != nil
| ssItem(sk52(sk51)) ),
inference(demodulation,[status(thm)],[p521,p234]) ).
cnf(p560,plain,
ssItem(sk52(sk51)),
inference(equality_resolution,[status(thm)],[p524]) ).
cnf(p561,plain,
( ~ lt(X1,sk52(sk51))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk52(sk51),nil),X0) != sk51
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p560,c199]) ).
cnf(c204,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk53(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p249,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk53(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c204,c196]) ).
cnf(p251,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk53(sk51)) ),
inference(equality_resolution,[status(thm)],[p249]) ).
cnf(p252,plain,
( nil != sk48
| ssList(sk53(sk51)) ),
inference(resolution,[status(thm)],[p251,p215]) ).
cnf(p525,plain,
( nil != nil
| ssList(sk53(sk51)) ),
inference(demodulation,[status(thm)],[p521,p252]) ).
cnf(p563,plain,
ssList(sk53(sk51)),
inference(equality_resolution,[status(thm)],[p525]) ).
cnf(p630,plain,
( ~ lt(X0,sk52(sk51))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| sk51 != sk51 ),
inference(resolution,[status(thm)],[p561,p563]) ).
cnf(p632,plain,
( ~ lt(X0,sk52(sk51))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(equality_resolution,[status(thm)],[p630]) ).
cnf(c208,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk54(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p265,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk54(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c208,c196]) ).
cnf(p267,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk54(sk51)) ),
inference(equality_resolution,[status(thm)],[p265]) ).
cnf(p268,plain,
( nil != sk48
| ssItem(sk54(sk51)) ),
inference(resolution,[status(thm)],[p267,p215]) ).
cnf(p526,plain,
( nil != nil
| ssItem(sk54(sk51)) ),
inference(demodulation,[status(thm)],[p521,p268]) ).
cnf(p564,plain,
ssItem(sk54(sk51)),
inference(equality_resolution,[status(thm)],[p526]) ).
cnf(p634,plain,
( ~ lt(sk54(sk51),sk52(sk51))
| app(X0,cons(sk54(sk51),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p632,p564]) ).
cnf(c210,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk55(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p288,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk55(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c210,c196]) ).
cnf(p291,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk55(sk51)) ),
inference(equality_resolution,[status(thm)],[p288]) ).
cnf(p292,plain,
( nil != sk48
| ssList(sk55(sk51)) ),
inference(resolution,[status(thm)],[p291,p215]) ).
cnf(p527,plain,
( nil != nil
| ssList(sk55(sk51)) ),
inference(demodulation,[status(thm)],[p521,p292]) ).
cnf(p567,plain,
ssList(sk55(sk51)),
inference(equality_resolution,[status(thm)],[p527]) ).
cnf(p645,plain,
( ~ lt(sk54(sk51),sk52(sk51))
| nil != sk49 ),
inference(resolution,[status(thm)],[p634,p567]) ).
cnf(p439,plain,
nil = sk49,
inference(superposition,[status(thm)],[p438,c195]) ).
cnf(p646,plain,
~ lt(sk54(sk51),sk52(sk51)),
inference(resolution,[status(thm)],[p645,p439]) ).
cnf(c214,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk54(X9),sk52(X9))
| app(sk47,X9) != sk48
| ~ ssList(X9) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p306,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk54(sk51),sk52(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c214,c196]) ).
cnf(p309,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk54(sk51),sk52(sk51)) ),
inference(equality_resolution,[status(thm)],[p306]) ).
cnf(p310,plain,
( nil != sk48
| lt(sk54(sk51),sk52(sk51)) ),
inference(resolution,[status(thm)],[p309,p215]) ).
cnf(p528,plain,
( nil != nil
| lt(sk54(sk51),sk52(sk51)) ),
inference(demodulation,[status(thm)],[p521,p310]) ).
cnf(p568,plain,
lt(sk54(sk51),sk52(sk51)),
inference(equality_resolution,[status(thm)],[p528]) ).
cnf(p647,plain,
$false,
inference(resolution,[status(thm)],[p646,p568]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC343+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.37 % Computer : n011.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Thu Sep 24 17:44:35 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 23.03/8.72 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.03/8.72 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------