%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC327+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 : n003.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:00 PM UTC 2026
% Result : Theorem 21.46s 3.82s
% Output : Proof 21.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 1
% Syntax : Number of formulae : 71 ( 16 unt; 0 def)
% Number of atoms : 289 ( 154 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 354 ( 136 ~; 152 |; 50 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 61 ( 0 sgn 24 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil = V
| nil != U )
& ? [X3] :
( equalelemsP(U)
& ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ( ! [X6] :
( ssList(X6)
=> app(X6,cons(X4,nil)) != U )
| app(cons(X4,nil),X5) != X3 ) ) )
& app(U,X3) = V
& ssList(X3) ) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ( ? [Z] :
( ? [X1] :
( ? [X2] :
( app(X2,cons(Z,nil)) = W
& ssList(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ equalelemsP(W)
| app(W,Y) != X ) )
| 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)
=> ( ( ( nil = V
| nil != U )
& ? [X3] :
( equalelemsP(U)
& ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ( ! [X6] :
( ssList(X6)
=> app(X6,cons(X4,nil)) != U )
| app(cons(X4,nil),X5) != X3 ) ) )
& app(U,X3) = V
& ssList(X3) ) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ( ? [Z] :
( ? [X1] :
( ? [X2] :
( app(X2,cons(Z,nil)) = W
& ssList(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ equalelemsP(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 )
| ! [X3] :
( ~ equalelemsP(U)
| ? [X4] :
( ? [X5] :
( ? [X6] :
( app(X6,cons(X4,nil)) = U
& ssList(X6) )
& app(cons(X4,nil),X5) = X3
& ssList(X5) )
& ssItem(X4) )
| app(U,X3) != V
| ~ ssList(X3) ) )
& ( nil != W
| nil = X )
& ? [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( app(X2,cons(Z,nil)) != W
| ~ ssList(X2) )
| app(cons(Z,nil),X1) != Y
| ~ ssList(X1) )
| ~ ssItem(Z) )
& equalelemsP(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] :
( ( ( nil != sk48
& nil = sk47 )
| ~ equalelemsP(sk47)
| ( app(sk54(X3),cons(sk52(X3),nil)) = sk47
& ssList(sk54(X3))
& app(cons(sk52(X3),nil),sk53(X3)) = X3
& ssList(sk53(X3))
& ssItem(sk52(X3)) )
| app(sk47,X3) != sk48
| ~ ssList(X3) )
& ( nil != sk49
| nil = sk50 )
& ( app(X2,cons(Z,nil)) != sk49
| ~ ssList(X2)
| app(cons(Z,nil),X1) != sk51
| ~ ssList(X1)
| ~ ssItem(Z) )
& equalelemsP(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])],[f95_nnf]) ).
cnf(c209,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| app(sk54(X8),cons(sk52(X8),nil)) = sk47
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c196,plain,
ssList(sk51),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p309,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| app(sk54(sk51),cons(sk52(sk51),nil)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c209,c196]) ).
cnf(p312,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| app(sk54(sk51),cons(sk52(sk51),nil)) = sk47 ),
inference(equality_resolution,[status(thm)],[p309]) ).
cnf(c195,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c198,plain,
equalelemsP(sk49),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p211,plain,
equalelemsP(sk47),
inference(superposition,[status(thm)],[c195,c198]) ).
cnf(p313,plain,
( nil = sk47
| app(sk54(sk51),cons(sk52(sk51),nil)) = sk47 ),
inference(resolution,[status(thm)],[p312,p211]) ).
cnf(c199,plain,
( app(X7,cons(X5,nil)) != sk49
| ~ ssList(X7)
| app(cons(X5,nil),X6) != sk51
| ~ ssList(X6)
| ~ ssItem(X5) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c201,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssItem(sk52(X8))
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p221,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssItem(sk52(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c201,c196]) ).
cnf(p222,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssItem(sk52(sk51)) ),
inference(equality_resolution,[status(thm)],[p221]) ).
cnf(p223,plain,
( nil = sk47
| ssItem(sk52(sk51)) ),
inference(resolution,[status(thm)],[p222,p211]) ).
cnf(p279,plain,
( nil = sk47
| app(X1,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X1)
| app(cons(sk52(sk51),nil),X0) != sk51
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c199,p223]) ).
cnf(c203,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssList(sk53(X8))
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p232,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssList(sk53(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c203,c196]) ).
cnf(p235,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssList(sk53(sk51)) ),
inference(equality_resolution,[status(thm)],[p232]) ).
cnf(p236,plain,
( nil = sk47
| ssList(sk53(sk51)) ),
inference(resolution,[status(thm)],[p235,p211]) ).
cnf(p328,plain,
( nil = sk47
| nil = sk47
| app(X0,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X0)
| app(cons(sk52(sk51),nil),sk53(sk51)) != sk51 ),
inference(resolution,[status(thm)],[p279,p236]) ).
cnf(p337,plain,
( nil = sk47
| app(X0,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X0)
| app(cons(sk52(sk51),nil),sk53(sk51)) != sk51 ),
inference(factoring,[status(thm)],[p328]) ).
cnf(c205,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| app(cons(sk52(X8),nil),sk53(X8)) = X8
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p291,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| app(cons(sk52(sk51),nil),sk53(sk51)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c205,c196]) ).
cnf(p294,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| app(cons(sk52(sk51),nil),sk53(sk51)) = sk51 ),
inference(equality_resolution,[status(thm)],[p291]) ).
cnf(p295,plain,
( nil = sk47
| app(cons(sk52(sk51),nil),sk53(sk51)) = sk51 ),
inference(resolution,[status(thm)],[p294,p211]) ).
cnf(p338,plain,
( nil = sk47
| nil = sk47
| app(X0,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p337,p295]) ).
cnf(p339,plain,
( nil = sk47
| app(X0,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X0) ),
inference(factoring,[status(thm)],[p338]) ).
cnf(c207,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssList(sk54(X8))
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p253,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssList(sk54(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c207,c196]) ).
cnf(p255,plain,
( nil = sk47
| ~ equalelemsP(sk47)
| ssList(sk54(sk51)) ),
inference(equality_resolution,[status(thm)],[p253]) ).
cnf(p256,plain,
( nil = sk47
| ssList(sk54(sk51)) ),
inference(resolution,[status(thm)],[p255,p211]) ).
cnf(p344,plain,
( nil = sk47
| nil = sk47
| app(sk54(sk51),cons(sk52(sk51),nil)) != sk49 ),
inference(resolution,[status(thm)],[p339,p256]) ).
cnf(p349,plain,
( nil = sk47
| app(sk54(sk51),cons(sk52(sk51),nil)) != sk49 ),
inference(factoring,[status(thm)],[p344]) ).
cnf(p351,plain,
( nil = sk47
| sk47 != sk49
| nil = sk47 ),
inference(superposition,[status(thm)],[p313,p349]) ).
cnf(p352,plain,
( sk47 != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p351]) ).
cnf(p353,plain,
nil = sk47,
inference(resolution,[status(thm)],[p352,c195]) ).
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(p213,plain,
sk50 = sk48,
inference(superposition,[status(thm)],[c194,c197]) ).
cnf(c200,plain,
( nil != sk49
| nil = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p212,plain,
( nil != sk47
| nil = sk50 ),
inference(superposition,[status(thm)],[c195,c200]) ).
cnf(p216,plain,
( nil != sk47
| nil = sk48 ),
inference(demodulation,[status(thm)],[p213,p212]) ).
cnf(p356,plain,
nil = sk48,
inference(resolution,[status(thm)],[p353,p216]) ).
cnf(p414,plain,
sk48 = nil,
inference(superposition,[status(thm)],[p356,p213]) ).
cnf(c202,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssItem(sk52(X8))
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p228,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssItem(sk52(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c202,c196]) ).
cnf(p233,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssItem(sk52(sk51)) ),
inference(equality_resolution,[status(thm)],[p228]) ).
cnf(p234,plain,
( nil != sk48
| ssItem(sk52(sk51)) ),
inference(resolution,[status(thm)],[p233,p211]) ).
cnf(p417,plain,
( nil != nil
| ssItem(sk52(sk51)) ),
inference(demodulation,[status(thm)],[p414,p234]) ).
cnf(p443,plain,
ssItem(sk52(sk51)),
inference(equality_resolution,[status(thm)],[p417]) ).
cnf(p444,plain,
( app(X1,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X1)
| app(cons(sk52(sk51),nil),X0) != sk51
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p443,c199]) ).
cnf(c204,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssList(sk53(X8))
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p245,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssList(sk53(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c204,c196]) ).
cnf(p247,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssList(sk53(sk51)) ),
inference(equality_resolution,[status(thm)],[p245]) ).
cnf(p248,plain,
( nil != sk48
| ssList(sk53(sk51)) ),
inference(resolution,[status(thm)],[p247,p211]) ).
cnf(p418,plain,
( nil != nil
| ssList(sk53(sk51)) ),
inference(demodulation,[status(thm)],[p414,p248]) ).
cnf(p446,plain,
ssList(sk53(sk51)),
inference(equality_resolution,[status(thm)],[p418]) ).
cnf(p483,plain,
( app(X0,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X0)
| sk51 != sk51 ),
inference(resolution,[status(thm)],[p444,p446]) ).
cnf(p485,plain,
( app(X0,cons(sk52(sk51),nil)) != sk49
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[p483]) ).
cnf(c208,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssList(sk54(X8))
| app(sk47,X8) != sk48
| ~ ssList(X8) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p266,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssList(sk54(sk51))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[c208,c196]) ).
cnf(p269,plain,
( nil != sk48
| ~ equalelemsP(sk47)
| ssList(sk54(sk51)) ),
inference(equality_resolution,[status(thm)],[p266]) ).
cnf(p270,plain,
( nil != sk48
| ssList(sk54(sk51)) ),
inference(resolution,[status(thm)],[p269,p211]) ).
cnf(p419,plain,
( nil != nil
| ssList(sk54(sk51)) ),
inference(demodulation,[status(thm)],[p414,p270]) ).
cnf(p447,plain,
ssList(sk54(sk51)),
inference(equality_resolution,[status(thm)],[p419]) ).
cnf(p488,plain,
nil != sk49,
inference(resolution,[status(thm)],[p485,p447]) ).
cnf(p354,plain,
nil = sk49,
inference(superposition,[status(thm)],[p353,c195]) ).
cnf(p489,plain,
$false,
inference(resolution,[status(thm)],[p488,p354]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC327+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.57 % Computer : n003.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Thu Sep 24 17:40:37 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.57 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.46/3.82 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.46/3.82 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------