%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC413+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 : n004.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:17 PM UTC 2026
% Result : Theorem 28.12s 4.62s
% Output : Proof 28.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 1
% Syntax : Number of formulae : 148 ( 16 unt; 0 def)
% Number of atoms : 536 ( 188 equ)
% Maximal formula atoms : 28 ( 3 avg)
% Number of connectives : 645 ( 257 ~; 308 |; 54 &)
% ( 0 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 14 con; 0-2 aty)
% Number of variables : 168 ( 0 sgn 38 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssList(X4)
=> app(app(cons(X2,nil),cons(X3,nil)),X4) != V ) ) )
| ? [X8] :
( ? [X9] :
( ? [X10] :
( app(app(cons(X8,nil),cons(X9,nil)),X10) = X
& ssList(X10) )
& ssItem(X9) )
& ssItem(X8) ) )
& ( ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssItem(X6)
=> ! [X7] :
( ssList(X7)
=> ( app(app(cons(X6,nil),cons(X5,nil)),X7) != W
| app(app(cons(X5,nil),cons(X6,nil)),X7) != X ) ) ) )
| ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssList(X4)
=> app(app(cons(X2,nil),cons(X3,nil)),X4) != V ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( app(app(cons(Z,nil),cons(Y,nil)),X1) = U
& app(app(cons(Y,nil),cons(Z,nil)),X1) = V
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) ) ) )
| 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)
=> ( ( ( ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssList(X4)
=> app(app(cons(X2,nil),cons(X3,nil)),X4) != V ) ) )
| ? [X8] :
( ? [X9] :
( ? [X10] :
( app(app(cons(X8,nil),cons(X9,nil)),X10) = X
& ssList(X10) )
& ssItem(X9) )
& ssItem(X8) ) )
& ( ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssItem(X6)
=> ! [X7] :
( ssList(X7)
=> ( app(app(cons(X6,nil),cons(X5,nil)),X7) != W
| app(app(cons(X5,nil),cons(X6,nil)),X7) != X ) ) ) )
| ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssList(X4)
=> app(app(cons(X2,nil),cons(X3,nil)),X4) != V ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( app(app(cons(Z,nil),cons(Y,nil)),X1) = U
& app(app(cons(Y,nil),cons(Z,nil)),X1) = V
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) ) ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f95_nnf,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ? [X2] :
( ? [X3] :
( ? [X4] :
( app(app(cons(X2,nil),cons(X3,nil)),X4) = V
& ssList(X4) )
& ssItem(X3) )
& ssItem(X2) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( app(app(cons(X8,nil),cons(X9,nil)),X10) != X
| ~ ssList(X10) )
| ~ ssItem(X9) )
| ~ ssItem(X8) ) )
| ( ? [X5] :
( ? [X6] :
( ? [X7] :
( app(app(cons(X6,nil),cons(X5,nil)),X7) = W
& app(app(cons(X5,nil),cons(X6,nil)),X7) = X
& ssList(X7) )
& ssItem(X6) )
& ssItem(X5) )
& ? [X2] :
( ? [X3] :
( ? [X4] :
( app(app(cons(X2,nil),cons(X3,nil)),X4) = V
& ssList(X4) )
& ssItem(X3) )
& ssItem(X2) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( app(app(cons(Z,nil),cons(Y,nil)),X1) != U
| app(app(cons(Y,nil),cons(Z,nil)),X1) != V
| ~ ssList(X1) )
| ~ ssItem(Z) )
| ~ 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,X1,X8,X9,X10] :
( ( ( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
& ssList(sk59)
& ssItem(sk58)
& ssItem(sk57)
& ( app(app(cons(X8,nil),cons(X9,nil)),X10) != sk50
| ~ ssList(X10)
| ~ ssItem(X9)
| ~ ssItem(X8) ) )
| ( app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk49
& app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50
& ssList(sk56)
& ssItem(sk55)
& ssItem(sk54)
& app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48
& ssList(sk53)
& ssItem(sk52)
& ssItem(sk51)
& ( app(app(cons(Z,nil),cons(Y,nil)),X1) != sk47
| app(app(cons(Y,nil),cons(Z,nil)),X1) != sk48
| ~ ssList(X1)
| ~ ssItem(Z)
| ~ 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,sk54,sk55,sk56,sk57,sk58,sk59])],[f95_nnf]) ).
cnf(c194,plain,
sk48 = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c199,plain,
( ssList(sk59)
| app(app(cons(X5,nil),cons(X4,nil)),X6) != sk47
| app(app(cons(X4,nil),cons(X5,nil)),X6) != sk48
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c225,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| ssItem(sk54) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c221,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| ssItem(sk54) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c222,plain,
( ssItem(sk57)
| ssItem(sk54) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p418,plain,
( ssItem(sk54)
| app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk54) ),
inference(resolution,[status(thm)],[c221,c222]) ).
cnf(p1369,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk54) ),
inference(factoring,[status(thm)],[p418]) ).
cnf(c223,plain,
( ssItem(sk58)
| ssItem(sk54) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1371,plain,
( ssItem(sk54)
| app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk54) ),
inference(resolution,[status(thm)],[p1369,c223]) ).
cnf(p1416,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk54) ),
inference(factoring,[status(thm)],[p1371]) ).
cnf(c224,plain,
( ssList(sk59)
| ssItem(sk54) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1424,plain,
( ssItem(sk54)
| app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk54) ),
inference(resolution,[status(thm)],[p1416,c224]) ).
cnf(p1505,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk54) ),
inference(factoring,[status(thm)],[p1424]) ).
cnf(p1507,plain,
( sk48 != sk50
| ssItem(sk54)
| ssItem(sk54) ),
inference(superposition,[status(thm)],[c225,p1505]) ).
cnf(p1511,plain,
( sk48 != sk50
| ssItem(sk54) ),
inference(factoring,[status(thm)],[p1507]) ).
cnf(p1512,plain,
ssItem(sk54),
inference(resolution,[status(thm)],[p1511,c194]) ).
cnf(p4485,plain,
( ssList(sk59)
| app(app(cons(X0,nil),cons(sk54,nil)),X1) != sk47
| app(app(cons(sk54,nil),cons(X0,nil)),X1) != sk48
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[c199,p1512]) ).
cnf(c230,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| ssItem(sk55) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c227,plain,
( ssItem(sk57)
| ssItem(sk55) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c226,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| ssItem(sk55) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p610,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk55)
| ssItem(sk55) ),
inference(resolution,[status(thm)],[c227,c226]) ).
cnf(p1882,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk55) ),
inference(factoring,[status(thm)],[p610]) ).
cnf(c228,plain,
( ssItem(sk58)
| ssItem(sk55) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1883,plain,
( ssItem(sk55)
| app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk55) ),
inference(resolution,[status(thm)],[p1882,c228]) ).
cnf(p1923,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk55) ),
inference(factoring,[status(thm)],[p1883]) ).
cnf(c229,plain,
( ssList(sk59)
| ssItem(sk55) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1929,plain,
( ssItem(sk55)
| app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk55) ),
inference(resolution,[status(thm)],[p1923,c229]) ).
cnf(p1978,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk55) ),
inference(factoring,[status(thm)],[p1929]) ).
cnf(p1980,plain,
( sk48 != sk50
| ssItem(sk55)
| ssItem(sk55) ),
inference(superposition,[status(thm)],[c230,p1978]) ).
cnf(p1985,plain,
( sk48 != sk50
| ssItem(sk55) ),
inference(factoring,[status(thm)],[p1980]) ).
cnf(p1986,plain,
ssItem(sk55),
inference(resolution,[status(thm)],[p1985,c194]) ).
cnf(p4637,plain,
( ssList(sk59)
| app(app(cons(sk55,nil),cons(sk54,nil)),X0) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p4485,p1986]) ).
cnf(c235,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| ssList(sk56) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c198,plain,
( ssItem(sk58)
| app(app(cons(X5,nil),cons(X4,nil)),X6) != sk47
| app(app(cons(X4,nil),cons(X5,nil)),X6) != sk48
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3305,plain,
( ssItem(sk58)
| app(app(cons(X0,nil),cons(sk54,nil)),X1) != sk47
| app(app(cons(sk54,nil),cons(X0,nil)),X1) != sk48
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[c198,p1512]) ).
cnf(p3456,plain,
( ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),X0) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p3305,p1986]) ).
cnf(c233,plain,
( ssItem(sk58)
| ssList(sk56) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3479,plain,
( ssItem(sk58)
| ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) != sk48 ),
inference(resolution,[status(thm)],[p3456,c233]) ).
cnf(p3495,plain,
( ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) != sk48 ),
inference(factoring,[status(thm)],[p3479]) ).
cnf(c238,plain,
( ssItem(sk58)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p247,plain,
( ssItem(sk58)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk48 ),
inference(superposition,[status(thm)],[c194,c238]) ).
cnf(p3499,plain,
( ssItem(sk58)
| ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47 ),
inference(resolution,[status(thm)],[p3495,p247]) ).
cnf(p3522,plain,
( ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47 ),
inference(factoring,[status(thm)],[p3499]) ).
cnf(c195,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c243,plain,
( ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk49 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p250,plain,
( ssItem(sk58)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk47 ),
inference(superposition,[status(thm)],[c195,c243]) ).
cnf(p3524,plain,
( ssItem(sk58)
| ssItem(sk58) ),
inference(resolution,[status(thm)],[p3522,p250]) ).
cnf(p3525,plain,
ssItem(sk58),
inference(factoring,[status(thm)],[p3524]) ).
cnf(c197,plain,
( ssItem(sk57)
| app(app(cons(X5,nil),cons(X4,nil)),X6) != sk47
| app(app(cons(X4,nil),cons(X5,nil)),X6) != sk48
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2614,plain,
( ssItem(sk57)
| app(app(cons(X0,nil),cons(sk54,nil)),X1) != sk47
| app(app(cons(sk54,nil),cons(X0,nil)),X1) != sk48
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[c197,p1512]) ).
cnf(p2752,plain,
( ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),X0) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p2614,p1986]) ).
cnf(c232,plain,
( ssItem(sk57)
| ssList(sk56) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2779,plain,
( ssItem(sk57)
| ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) != sk48 ),
inference(resolution,[status(thm)],[p2752,c232]) ).
cnf(p2788,plain,
( ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) != sk48 ),
inference(factoring,[status(thm)],[p2779]) ).
cnf(c237,plain,
( ssItem(sk57)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p246,plain,
( ssItem(sk57)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk48 ),
inference(superposition,[status(thm)],[c194,c237]) ).
cnf(p2794,plain,
( ssItem(sk57)
| ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47 ),
inference(resolution,[status(thm)],[p2788,p246]) ).
cnf(p2825,plain,
( ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47 ),
inference(factoring,[status(thm)],[p2794]) ).
cnf(c242,plain,
( ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk49 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p249,plain,
( ssItem(sk57)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk47 ),
inference(superposition,[status(thm)],[c195,c242]) ).
cnf(p2827,plain,
( ssItem(sk57)
| ssItem(sk57) ),
inference(resolution,[status(thm)],[p2825,p249]) ).
cnf(p2828,plain,
ssItem(sk57),
inference(factoring,[status(thm)],[p2827]) ).
cnf(c231,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| ssList(sk56) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2831,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssList(sk56) ),
inference(resolution,[status(thm)],[p2828,c231]) ).
cnf(p3557,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssList(sk56) ),
inference(resolution,[status(thm)],[p3525,p2831]) ).
cnf(c234,plain,
( ssList(sk59)
| ssList(sk56) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3670,plain,
( ssList(sk56)
| app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssList(sk56) ),
inference(resolution,[status(thm)],[p3557,c234]) ).
cnf(p3841,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssList(sk56) ),
inference(factoring,[status(thm)],[p3670]) ).
cnf(p3843,plain,
( sk48 != sk50
| ssList(sk56)
| ssList(sk56) ),
inference(superposition,[status(thm)],[c235,p3841]) ).
cnf(p3847,plain,
( sk48 != sk50
| ssList(sk56) ),
inference(factoring,[status(thm)],[p3843]) ).
cnf(p3848,plain,
ssList(sk56),
inference(resolution,[status(thm)],[p3847,c194]) ).
cnf(p4661,plain,
( ssList(sk59)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) != sk48 ),
inference(resolution,[status(thm)],[p4637,p3848]) ).
cnf(c239,plain,
( ssList(sk59)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p248,plain,
( ssList(sk59)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk48 ),
inference(superposition,[status(thm)],[c194,c239]) ).
cnf(p4665,plain,
( ssList(sk59)
| ssList(sk59)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47 ),
inference(resolution,[status(thm)],[p4661,p248]) ).
cnf(p4666,plain,
( ssList(sk59)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) != sk47 ),
inference(factoring,[status(thm)],[p4665]) ).
cnf(c244,plain,
( ssList(sk59)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk49 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p251,plain,
( ssList(sk59)
| app(app(cons(sk55,nil),cons(sk54,nil)),sk56) = sk47 ),
inference(superposition,[status(thm)],[c195,c244]) ).
cnf(p4668,plain,
( ssList(sk59)
| ssList(sk59) ),
inference(resolution,[status(thm)],[p4666,p251]) ).
cnf(p4669,plain,
ssList(sk59),
inference(factoring,[status(thm)],[p4668]) ).
cnf(c216,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2841,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(resolution,[status(thm)],[p2828,c216]) ).
cnf(p3558,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(resolution,[status(thm)],[p3525,p2841]) ).
cnf(p4760,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(resolution,[status(thm)],[p4669,p3558]) ).
cnf(p4868,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk48
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(superposition,[status(thm)],[c194,p4760]) ).
cnf(c220,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4892,plain,
( app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48
| app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48 ),
inference(resolution,[status(thm)],[p4868,c220]) ).
cnf(p4898,plain,
app(app(cons(sk51,nil),cons(sk52,nil)),sk53) = sk48,
inference(factoring,[status(thm)],[p4892]) ).
cnf(c215,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| ssList(sk53) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c211,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| ssList(sk53) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2829,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssList(sk53) ),
inference(resolution,[status(thm)],[p2828,c211]) ).
cnf(p3556,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssList(sk53) ),
inference(resolution,[status(thm)],[p3525,p2829]) ).
cnf(c214,plain,
( ssList(sk59)
| ssList(sk53) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3660,plain,
( ssList(sk53)
| app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssList(sk53) ),
inference(resolution,[status(thm)],[p3556,c214]) ).
cnf(p3695,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssList(sk53) ),
inference(factoring,[status(thm)],[p3660]) ).
cnf(p3697,plain,
( sk48 != sk50
| ssList(sk53)
| ssList(sk53) ),
inference(superposition,[status(thm)],[c215,p3695]) ).
cnf(p3702,plain,
( sk48 != sk50
| ssList(sk53) ),
inference(factoring,[status(thm)],[p3697]) ).
cnf(p3703,plain,
ssList(sk53),
inference(resolution,[status(thm)],[p3702,c194]) ).
cnf(c236,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c205,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| ssItem(sk51) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c201,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| ssItem(sk51) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c202,plain,
( ssItem(sk57)
| ssItem(sk51) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p262,plain,
( ssItem(sk51)
| app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk51) ),
inference(resolution,[status(thm)],[c201,c202]) ).
cnf(p515,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk51) ),
inference(factoring,[status(thm)],[p262]) ).
cnf(c203,plain,
( ssItem(sk58)
| ssItem(sk51) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p518,plain,
( ssItem(sk51)
| app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk51) ),
inference(resolution,[status(thm)],[p515,c203]) ).
cnf(p547,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk51) ),
inference(factoring,[status(thm)],[p518]) ).
cnf(c204,plain,
( ssList(sk59)
| ssItem(sk51) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p549,plain,
( ssItem(sk51)
| app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk51) ),
inference(resolution,[status(thm)],[p547,c204]) ).
cnf(p626,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk51) ),
inference(factoring,[status(thm)],[p549]) ).
cnf(p628,plain,
( sk48 != sk50
| ssItem(sk51)
| ssItem(sk51) ),
inference(superposition,[status(thm)],[c205,p626]) ).
cnf(p634,plain,
( sk48 != sk50
| ssItem(sk51) ),
inference(factoring,[status(thm)],[p628]) ).
cnf(p635,plain,
ssItem(sk51),
inference(resolution,[status(thm)],[p634,c194]) ).
cnf(p2314,plain,
( app(app(cons(sk51,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(resolution,[status(thm)],[c236,p635]) ).
cnf(c210,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) = sk48
| ssItem(sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c206,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| ssItem(sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c207,plain,
( ssItem(sk57)
| ssItem(sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p341,plain,
( ssItem(sk52)
| app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk52) ),
inference(resolution,[status(thm)],[c206,c207]) ).
cnf(p921,plain,
( app(app(cons(sk57,nil),cons(X0,nil)),X1) != sk50
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk52) ),
inference(factoring,[status(thm)],[p341]) ).
cnf(c208,plain,
( ssItem(sk58)
| ssItem(sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p922,plain,
( ssItem(sk52)
| app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk52) ),
inference(resolution,[status(thm)],[p921,c208]) ).
cnf(p942,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),X0) != sk50
| ~ ssList(X0)
| ssItem(sk52) ),
inference(factoring,[status(thm)],[p922]) ).
cnf(c209,plain,
( ssList(sk59)
| ssItem(sk52) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p948,plain,
( ssItem(sk52)
| app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk52) ),
inference(resolution,[status(thm)],[p942,c209]) ).
cnf(p985,plain,
( app(app(cons(sk57,nil),cons(sk58,nil)),sk59) != sk50
| ssItem(sk52) ),
inference(factoring,[status(thm)],[p948]) ).
cnf(p987,plain,
( sk48 != sk50
| ssItem(sk52)
| ssItem(sk52) ),
inference(superposition,[status(thm)],[c210,p985]) ).
cnf(p994,plain,
( sk48 != sk50
| ssItem(sk52) ),
inference(factoring,[status(thm)],[p987]) ).
cnf(p995,plain,
ssItem(sk52),
inference(resolution,[status(thm)],[p994,c194]) ).
cnf(p2354,plain,
( app(app(cons(sk51,nil),cons(sk52,nil)),X0) != sk50
| ~ ssList(X0)
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(resolution,[status(thm)],[p2314,p995]) ).
cnf(p3740,plain,
( app(app(cons(sk51,nil),cons(sk52,nil)),sk53) != sk50
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(resolution,[status(thm)],[p3703,p2354]) ).
cnf(p4899,plain,
( sk48 != sk50
| app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50 ),
inference(demodulation,[status(thm)],[p4898,p3740]) ).
cnf(p4903,plain,
app(app(cons(sk54,nil),cons(sk55,nil)),sk56) = sk50,
inference(resolution,[status(thm)],[p4899,c194]) ).
cnf(p4906,plain,
sk50 = sk48,
inference(superposition,[status(thm)],[c194,p4903]) ).
cnf(c196,plain,
( app(app(cons(X13,nil),cons(X14,nil)),X15) != sk50
| ~ ssList(X15)
| ~ ssItem(X14)
| ~ ssItem(X13)
| app(app(cons(X5,nil),cons(X4,nil)),X6) != sk47
| app(app(cons(X4,nil),cons(X5,nil)),X6) != sk48
| ~ ssList(X6)
| ~ ssItem(X5)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4907,plain,
( app(app(cons(X3,nil),cons(X4,nil)),X5) != sk48
| ~ ssList(X5)
| ~ ssItem(X4)
| ~ ssItem(X3)
| app(app(cons(X1,nil),cons(X0,nil)),X2) != sk47
| app(app(cons(X0,nil),cons(X1,nil)),X2) != sk48
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(demodulation,[status(thm)],[p4906,c196]) ).
cnf(p5089,plain,
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| app(app(cons(X1,nil),cons(X0,nil)),X2) != sk47
| app(app(cons(X0,nil),cons(X1,nil)),X2) != sk48
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p4907]) ).
cnf(p5098,plain,
( ~ ssList(X2)
| ~ ssItem(X1)
| app(app(cons(X1,nil),cons(X0,nil)),X2) != sk47
| app(app(cons(X0,nil),cons(X1,nil)),X2) != sk48
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p5089]) ).
cnf(p5102,plain,
( ~ ssList(X2)
| app(app(cons(X1,nil),cons(X0,nil)),X2) != sk47
| app(app(cons(X0,nil),cons(X1,nil)),X2) != sk48
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p5098]) ).
cnf(p5105,plain,
( app(app(cons(X1,nil),cons(X0,nil)),X2) != sk47
| app(app(cons(X0,nil),cons(X1,nil)),X2) != sk48
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p5102]) ).
cnf(p5145,plain,
( app(app(cons(X0,nil),cons(sk54,nil)),X1) != sk47
| app(app(cons(sk54,nil),cons(X0,nil)),X1) != sk48
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p5105,p1512]) ).
cnf(p5212,plain,
( app(app(cons(sk55,nil),cons(sk54,nil)),X0) != sk47
| app(app(cons(sk54,nil),cons(sk55,nil)),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p5145,p1986]) ).
cnf(p5228,plain,
( sk47 != sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5212,p3848]) ).
cnf(p5230,plain,
sk47 != sk47,
inference(equality_resolution,[status(thm)],[p5228]) ).
cnf(p5232,plain,
$false,
inference(equality_resolution,[status(thm)],[p5230]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC413+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 18:07:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 28.12/4.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.12/4.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------