%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC046+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 : n007.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:05:11 PM UTC 2026
% Result : Theorem 262.27s 38.53s
% Output : Proof 262.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 25
% Syntax : Number of formulae : 259 ( 179 unt; 0 def)
% Number of atoms : 617 ( 273 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 602 ( 244 ~; 207 |; 91 &)
% ( 6 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 9 con; 0-4 aty)
% Number of variables : 277 ( 2 sgn 128 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ? [Y] :
( ( ( ( ? [Z] :
( segmentP(X,app(app(cons(Y,nil),Z),cons(Y,nil)))
& ssList(Z) )
| ~ memberP(X,Y) )
& memberP(W,Y) )
| ( memberP(X,Y)
& ! [Z] :
( ssList(Z)
=> ~ segmentP(X,app(app(cons(Y,nil),Z),cons(Y,nil))) )
& ~ memberP(W,Y) ) )
& ssItem(Y) )
| nil = U
| U != W
| V != X
| nil != V ) ) ) ) ),
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)
=> ( ? [Y] :
( ( ( ( ? [Z] :
( segmentP(X,app(app(cons(Y,nil),Z),cons(Y,nil)))
& ssList(Z) )
| ~ memberP(X,Y) )
& memberP(W,Y) )
| ( memberP(X,Y)
& ! [Z] :
( ssList(Z)
=> ~ segmentP(X,app(app(cons(Y,nil),Z),cons(Y,nil))) )
& ~ memberP(W,Y) ) )
& ssItem(Y) )
| nil = U
| U != W
| V != X
| nil != V ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f95_nnf,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ! [Y] :
( ( ( ( ! [Z] :
( ~ segmentP(X,app(app(cons(Y,nil),Z),cons(Y,nil)))
| ~ ssList(Z) )
& memberP(X,Y) )
| ~ memberP(W,Y) )
& ( ~ memberP(X,Y)
| ? [Z] :
( segmentP(X,app(app(cons(Y,nil),Z),cons(Y,nil)))
& ssList(Z) )
| memberP(W,Y) ) )
| ~ ssItem(Y) )
& nil != U
& U = W
& V = X
& nil = V
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(nnf_transformation,[status(thm)],[f95_neg]) ).
fof(f95_sk,plain,
! [Y,Z] :
( ( ( ( ( ( ~ segmentP(sk50,app(app(cons(Y,nil),Z),cons(Y,nil)))
| ~ ssList(Z) )
& memberP(sk50,Y) )
| ~ memberP(sk49,Y) )
& ( ~ memberP(sk50,Y)
| ( segmentP(sk50,app(app(cons(Y,nil),sk51(Y)),cons(Y,nil)))
& ssList(sk51(Y)) )
| memberP(sk49,Y) ) )
| ~ ssItem(Y) )
& nil != sk47
& sk47 = sk49
& sk48 = sk50
& nil = sk48
& ssList(sk50)
& ssList(sk49)
& ssList(sk48)
& ssList(sk47) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47,sk48,sk49,sk50,sk51])],[f95_nnf]) ).
cnf(c200,plain,
( memberP(sk50,X4)
| ~ memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t93,plain,
ifeq(ssItem(X1),true,ifeq(memberP(sk49,X1),true,memberP(sk50,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c200]) ).
cnf(t297,plain,
ifeq(ssItem(X1),true,ifeq(memberP(sk49,X1),true,memberP(sk50,X1),true),true) = true,
inference(orient,[status(thm)],[t93]) ).
fof(f36,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssList(W)
=> ( memberP(cons(V,W),U)
<=> ( memberP(W,U)
| U = V ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax37) ).
fof(f36_nnf,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( ( ~ memberP(W,U)
& U != V )
| memberP(cons(V,W),U) )
& ( memberP(W,U)
| U = V
| ~ memberP(cons(V,W),U) ) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [U,V,W] :
( ( ( ( ~ memberP(W,U)
& U != V )
| memberP(cons(V,W),U) )
& ( memberP(W,U)
| U = V
| ~ memberP(cons(V,W),U) ) )
| ~ ssList(W)
| ~ ssItem(V)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c111,plain,
( X0 != X1
| memberP(cons(X1,X2),X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t195,plain,
ifeq(ssItem(X1),true,ifeq(ssItem(X2),true,ifeq(ssList(X3),true,ifeq(X1,X2,memberP(cons(X2,X3),X1),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(t326,plain,
ifeq(ssItem(X1),true,ifeq(ssItem(X2),true,ifeq(ssList(X3),true,ifeq(X1,X2,memberP(cons(X2,X3),X1),true),true),true),true) = true,
inference(orient,[status(thm)],[t195]) ).
cnf(t56,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t56]) ).
cnf(t327,plain,
true = ifeq(ssItem(X1),true,ifeq(ssItem(X1),true,ifeq(ssList(X2),true,memberP(cons(X1,X2),X1),true),true),true),
inference(cp,[status(thm)],[t326,t256]) ).
cnf(t24416,plain,
ifeq(ssItem(X1),true,ifeq(ssItem(X1),true,ifeq(ssList(X2),true,memberP(cons(X1,X2),X1),true),true),true) = true,
inference(orient,[status(thm)],[t327]) ).
cnf(t62,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t257,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t62]) ).
fof(f19,axiom,
! [U] :
( ssList(U)
=> ( ? [V] :
( ? [W] :
( cons(W,V) = U
& ssItem(W) )
& ssList(V) )
| nil = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f19_nnf,plain,
! [U] :
( ? [V] :
( ? [W] :
( cons(W,V) = U
& ssItem(W) )
& ssList(V) )
| nil = U
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [U] :
( ( cons(sk44(U),sk43(U)) = U
& ssItem(sk44(U))
& ssList(sk43(U)) )
| nil = U
| ~ ssList(U) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk43,sk44])],[f19_nnf]) ).
cnf(c89,plain,
( cons(sk44(X0),sk43(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t151,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(cons(sk44(X1),sk43(X1)),X1)),true) = true,
inference(equality_encoding,[status(esa)],[c89]) ).
cnf(t432,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(cons(sk44(X1),sk43(X1)),X1)),true) = true,
inference(orient,[status(thm)],[t151]) ).
cnf(c194,plain,
nil = sk48,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t0,plain,
sk48 = nil,
inference(equality_encoding,[status(esa)],[c194]) ).
cnf(t641,plain,
nil = sk48,
inference(orient,[status(thm)],[t0]) ).
cnf(t390273,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(cons(sk44(X1),sk43(X1)),X1)),true) = true,
inference(step,[status(thm)],[t432,t641]) ).
cnf(t680,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(cons(sk44(X1),sk43(X1)),X1)),true) = true,
inference(rw,[status(thm)],[t390273]) ).
cnf(c195,plain,
sk48 = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t2,plain,
sk50 = sk48,
inference(equality_encoding,[status(esa)],[c195]) ).
cnf(t981,plain,
sk48 = sk50,
inference(orient,[status(thm)],[t2]) ).
cnf(t397651,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(cons(sk44(X1),sk43(X1)),X1)),true) = true,
inference(step,[status(thm)],[t680,t981]) ).
cnf(t362963,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(cons(sk44(X1),sk43(X1)),X1)),true) = true,
inference(orient,[status(thm)],[t397651]) ).
cnf(c190,plain,
ssList(sk47),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t12,plain,
ssList(sk47) = true,
inference(equality_encoding,[status(esa)],[c190]) ).
cnf(c196,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t1,plain,
sk49 = sk47,
inference(equality_encoding,[status(esa)],[c196]) ).
cnf(t1009,plain,
sk47 = sk49,
inference(orient,[status(thm)],[t1]) ).
cnf(t390370,plain,
ssList(sk49) = true,
inference(step,[status(thm)],[t12,t1009]) ).
cnf(t1634,plain,
ssList(sk49) = true,
inference(orient,[status(thm)],[t390370]) ).
cnf(t363960,plain,
true = ifeq(true,true,or(eq(sk50,sk49),eq(cons(sk44(sk49),sk43(sk49)),sk49)),true),
inference(cp,[status(thm)],[t362963,t1634]) ).
cnf(t397917,plain,
true = or(eq(sk50,sk49),eq(cons(sk44(sk49),sk43(sk49)),sk49)),
inference(step,[status(thm)],[t363960,t256]) ).
cnf(c197,plain,
nil != sk47,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t24,plain,
eq(nil,sk47) = false,
inference(equality_encoding,[status(esa)],[c197]) ).
cnf(t518,plain,
eq(nil,sk47) = false,
inference(orient,[status(thm)],[t24]) ).
cnf(t390227,plain,
eq(sk48,sk47) = false,
inference(step,[status(thm)],[t518,t641]) ).
cnf(t644,plain,
eq(sk48,sk47) = false,
inference(rw,[status(thm)],[t390227]) ).
cnf(t390375,plain,
eq(sk50,sk47) = false,
inference(step,[status(thm)],[t644,t981]) ).
cnf(t390376,plain,
eq(sk50,sk49) = false,
inference(step,[status(thm)],[t390375,t1009]) ).
cnf(t2179,plain,
eq(sk50,sk49) = false,
inference(orient,[status(thm)],[t390376]) ).
cnf(t397918,plain,
true = or(false,eq(cons(sk44(sk49),sk43(sk49)),sk49)),
inference(step,[status(thm)],[t397917,t2179]) ).
cnf(t34,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t289,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t34]) ).
cnf(t397919,plain,
true = eq(cons(sk44(sk49),sk43(sk49)),sk49),
inference(step,[status(thm)],[t397918,t289]) ).
cnf(t387023,plain,
eq(cons(sk44(sk49),sk43(sk49)),sk49) = true,
inference(orient,[status(thm)],[t397919]) ).
cnf(t387024,plain,
sk49 = ifeq(true,true,cons(sk44(sk49),sk43(sk49)),sk49),
inference(cp,[status(thm)],[t257,t387023]) ).
cnf(t397920,plain,
sk49 = cons(sk44(sk49),sk43(sk49)),
inference(step,[status(thm)],[t387024,t256]) ).
cnf(t387033,plain,
cons(sk44(sk49),sk43(sk49)) = sk49,
inference(orient,[status(thm)],[t397920]) ).
fof(f22,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> hd(cons(V,U)) = V ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f22_nnf,plain,
! [U] :
( ! [V] :
( hd(cons(V,U)) = V
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [U,V] :
( hd(cons(V,U)) = V
| ~ ssItem(V)
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c92,plain,
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t95,plain,
ifeq(ssList(X1),true,ifeq(ssItem(X2),true,hd(cons(X2,X1)),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t263,plain,
ifeq(ssList(X1),true,ifeq(ssItem(X2),true,hd(cons(X2,X1)),X2),X2) = X2,
inference(orient,[status(thm)],[t95]) ).
cnf(t387034,plain,
sk44(sk49) = ifeq(ssList(sk43(sk49)),true,ifeq(ssItem(sk44(sk49)),true,hd(sk49),sk44(sk49)),sk44(sk49)),
inference(cp,[status(thm)],[t263,t387033]) ).
cnf(c87,plain,
( ssList(sk43(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t103,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssList(sk43(X1)),true)),true) = true,
inference(equality_encoding,[status(esa)],[c87]) ).
cnf(t437,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssList(sk43(X1)),true)),true) = true,
inference(orient,[status(thm)],[t103]) ).
cnf(t390269,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssList(sk43(X1)),true)),true) = true,
inference(step,[status(thm)],[t437,t641]) ).
cnf(t676,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssList(sk43(X1)),true)),true) = true,
inference(rw,[status(thm)],[t390269]) ).
cnf(t397270,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssList(sk43(X1)),true)),true) = true,
inference(step,[status(thm)],[t676,t981]) ).
cnf(t335033,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssList(sk43(X1)),true)),true) = true,
inference(orient,[status(thm)],[t397270]) ).
cnf(t335954,plain,
true = ifeq(true,true,or(eq(sk50,sk49),eq(ssList(sk43(sk49)),true)),true),
inference(cp,[status(thm)],[t335033,t1634]) ).
cnf(t397271,plain,
true = or(eq(sk50,sk49),eq(ssList(sk43(sk49)),true)),
inference(step,[status(thm)],[t335954,t256]) ).
cnf(t397272,plain,
true = or(false,eq(ssList(sk43(sk49)),true)),
inference(step,[status(thm)],[t397271,t2179]) ).
cnf(t397273,plain,
true = eq(ssList(sk43(sk49)),true),
inference(step,[status(thm)],[t397272,t289]) ).
cnf(t335957,plain,
eq(ssList(sk43(sk49)),true) = true,
inference(orient,[status(thm)],[t397273]) ).
cnf(t335958,plain,
true = ifeq(true,true,ssList(sk43(sk49)),true),
inference(cp,[status(thm)],[t257,t335957]) ).
cnf(t397274,plain,
true = ssList(sk43(sk49)),
inference(step,[status(thm)],[t335958,t256]) ).
cnf(t335967,plain,
ssList(sk43(sk49)) = true,
inference(orient,[status(thm)],[t397274]) ).
cnf(t397921,plain,
sk44(sk49) = ifeq(true,true,ifeq(ssItem(sk44(sk49)),true,hd(sk49),sk44(sk49)),sk44(sk49)),
inference(step,[status(thm)],[t387034,t335967]) ).
cnf(t397922,plain,
sk44(sk49) = ifeq(ssItem(sk44(sk49)),true,hd(sk49),sk44(sk49)),
inference(step,[status(thm)],[t397921,t256]) ).
cnf(c88,plain,
( ssItem(sk44(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t101,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssItem(sk44(X1)),true)),true) = true,
inference(equality_encoding,[status(esa)],[c88]) ).
cnf(t435,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssItem(sk44(X1)),true)),true) = true,
inference(orient,[status(thm)],[t101]) ).
cnf(t390271,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssItem(sk44(X1)),true)),true) = true,
inference(step,[status(thm)],[t435,t641]) ).
cnf(t678,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssItem(sk44(X1)),true)),true) = true,
inference(rw,[status(thm)],[t390271]) ).
cnf(t397432,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssItem(sk44(X1)),true)),true) = true,
inference(step,[status(thm)],[t678,t981]) ).
cnf(t343976,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssItem(sk44(X1)),true)),true) = true,
inference(orient,[status(thm)],[t397432]) ).
cnf(t344916,plain,
true = ifeq(true,true,or(eq(sk50,sk49),eq(ssItem(sk44(sk49)),true)),true),
inference(cp,[status(thm)],[t343976,t1634]) ).
cnf(t397433,plain,
true = or(eq(sk50,sk49),eq(ssItem(sk44(sk49)),true)),
inference(step,[status(thm)],[t344916,t256]) ).
cnf(t397434,plain,
true = or(false,eq(ssItem(sk44(sk49)),true)),
inference(step,[status(thm)],[t397433,t2179]) ).
cnf(t397435,plain,
true = eq(ssItem(sk44(sk49)),true),
inference(step,[status(thm)],[t397434,t289]) ).
cnf(t344919,plain,
eq(ssItem(sk44(sk49)),true) = true,
inference(orient,[status(thm)],[t397435]) ).
cnf(t344920,plain,
true = ifeq(true,true,ssItem(sk44(sk49)),true),
inference(cp,[status(thm)],[t257,t344919]) ).
cnf(t397436,plain,
true = ssItem(sk44(sk49)),
inference(step,[status(thm)],[t344920,t256]) ).
cnf(t344929,plain,
ssItem(sk44(sk49)) = true,
inference(orient,[status(thm)],[t397436]) ).
cnf(t397923,plain,
sk44(sk49) = ifeq(true,true,hd(sk49),sk44(sk49)),
inference(step,[status(thm)],[t397922,t344929]) ).
cnf(t397924,plain,
sk44(sk49) = hd(sk49),
inference(step,[status(thm)],[t397923,t256]) ).
fof(f74,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ? [V] :
( hd(U) = V
& ssItem(V) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax75) ).
fof(f74_nnf,plain,
! [U] :
( ? [V] :
( hd(U) = V
& ssItem(V) )
| nil = U
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [U] :
( ( hd(U) = sk45(U)
& ssItem(sk45(U)) )
| nil = U
| ~ ssList(U) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk45])],[f74_nnf]) ).
cnf(c164,plain,
( hd(X0) = sk45(X0)
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(t99,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(hd(X1),sk45(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c164]) ).
cnf(t433,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(hd(X1),sk45(X1))),true) = true,
inference(orient,[status(thm)],[t99]) ).
cnf(t390256,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(hd(X1),sk45(X1))),true) = true,
inference(step,[status(thm)],[t433,t641]) ).
cnf(t667,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(hd(X1),sk45(X1))),true) = true,
inference(rw,[status(thm)],[t390256]) ).
cnf(t396685,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(hd(X1),sk45(X1))),true) = true,
inference(step,[status(thm)],[t667,t981]) ).
cnf(t307569,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(hd(X1),sk45(X1))),true) = true,
inference(orient,[status(thm)],[t396685]) ).
cnf(t308449,plain,
true = ifeq(true,true,or(eq(sk50,sk49),eq(hd(sk49),sk45(sk49))),true),
inference(cp,[status(thm)],[t307569,t1634]) ).
cnf(t396686,plain,
true = or(eq(sk50,sk49),eq(hd(sk49),sk45(sk49))),
inference(step,[status(thm)],[t308449,t256]) ).
cnf(t396687,plain,
true = or(false,eq(hd(sk49),sk45(sk49))),
inference(step,[status(thm)],[t396686,t2179]) ).
cnf(t396688,plain,
true = eq(hd(sk49),sk45(sk49)),
inference(step,[status(thm)],[t396687,t289]) ).
cnf(t308640,plain,
eq(hd(sk49),sk45(sk49)) = true,
inference(orient,[status(thm)],[t396688]) ).
cnf(t308641,plain,
sk45(sk49) = ifeq(true,true,hd(sk49),sk45(sk49)),
inference(cp,[status(thm)],[t257,t308640]) ).
cnf(t396689,plain,
sk45(sk49) = hd(sk49),
inference(step,[status(thm)],[t308641,t256]) ).
cnf(t308650,plain,
hd(sk49) = sk45(sk49),
inference(orient,[status(thm)],[t396689]) ).
cnf(t397925,plain,
sk44(sk49) = sk45(sk49),
inference(step,[status(thm)],[t397924,t308650]) ).
cnf(t387107,plain,
sk44(sk49) = sk45(sk49),
inference(orient,[status(thm)],[t397925]) ).
cnf(t397926,plain,
cons(sk45(sk49),sk43(sk49)) = sk49,
inference(step,[status(thm)],[t387033,t387107]) ).
cnf(t387109,plain,
cons(sk45(sk49),sk43(sk49)) = sk49,
inference(rw,[status(thm)],[t397926]) ).
cnf(t387110,plain,
cons(sk45(sk49),sk43(sk49)) = sk49,
inference(orient,[status(thm)],[t387109]) ).
fof(f24,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> tl(cons(V,U)) = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f24_nnf,plain,
! [U] :
( ! [V] :
( tl(cons(V,U)) = U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [U,V] :
( tl(cons(V,U)) = U
| ~ ssItem(V)
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c94,plain,
( tl(cons(X1,X0)) = X0
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t97,plain,
ifeq(ssList(X1),true,ifeq(ssItem(X2),true,tl(cons(X2,X1)),X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(t275,plain,
ifeq(ssList(X1),true,ifeq(ssItem(X2),true,tl(cons(X2,X1)),X1),X1) = X1,
inference(orient,[status(thm)],[t97]) ).
cnf(t387113,plain,
sk43(sk49) = ifeq(ssList(sk43(sk49)),true,ifeq(ssItem(sk45(sk49)),true,tl(sk49),sk43(sk49)),sk43(sk49)),
inference(cp,[status(thm)],[t275,t387110]) ).
cnf(t397930,plain,
sk43(sk49) = ifeq(true,true,ifeq(ssItem(sk45(sk49)),true,tl(sk49),sk43(sk49)),sk43(sk49)),
inference(step,[status(thm)],[t387113,t335967]) ).
cnf(t397931,plain,
sk43(sk49) = ifeq(ssItem(sk45(sk49)),true,tl(sk49),sk43(sk49)),
inference(step,[status(thm)],[t397930,t256]) ).
cnf(c163,plain,
( ssItem(sk45(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(t102,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssItem(sk45(X1)),true)),true) = true,
inference(equality_encoding,[status(esa)],[c163]) ).
cnf(t436,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssItem(sk45(X1)),true)),true) = true,
inference(orient,[status(thm)],[t102]) ).
cnf(t390270,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssItem(sk45(X1)),true)),true) = true,
inference(step,[status(thm)],[t436,t641]) ).
cnf(t677,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssItem(sk45(X1)),true)),true) = true,
inference(rw,[status(thm)],[t390270]) ).
cnf(t397367,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssItem(sk45(X1)),true)),true) = true,
inference(step,[status(thm)],[t677,t981]) ).
cnf(t340169,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssItem(sk45(X1)),true)),true) = true,
inference(orient,[status(thm)],[t397367]) ).
cnf(t341103,plain,
true = ifeq(true,true,or(eq(sk50,sk49),eq(ssItem(sk45(sk49)),true)),true),
inference(cp,[status(thm)],[t340169,t1634]) ).
cnf(t397368,plain,
true = or(eq(sk50,sk49),eq(ssItem(sk45(sk49)),true)),
inference(step,[status(thm)],[t341103,t256]) ).
cnf(t397369,plain,
true = or(false,eq(ssItem(sk45(sk49)),true)),
inference(step,[status(thm)],[t397368,t2179]) ).
cnf(t397370,plain,
true = eq(ssItem(sk45(sk49)),true),
inference(step,[status(thm)],[t397369,t289]) ).
cnf(t341106,plain,
eq(ssItem(sk45(sk49)),true) = true,
inference(orient,[status(thm)],[t397370]) ).
cnf(t341107,plain,
true = ifeq(true,true,ssItem(sk45(sk49)),true),
inference(cp,[status(thm)],[t257,t341106]) ).
cnf(t397371,plain,
true = ssItem(sk45(sk49)),
inference(step,[status(thm)],[t341107,t256]) ).
cnf(t341116,plain,
ssItem(sk45(sk49)) = true,
inference(orient,[status(thm)],[t397371]) ).
cnf(t397932,plain,
sk43(sk49) = ifeq(true,true,tl(sk49),sk43(sk49)),
inference(step,[status(thm)],[t397931,t341116]) ).
cnf(t397933,plain,
sk43(sk49) = tl(sk49),
inference(step,[status(thm)],[t397932,t256]) ).
cnf(t390078,plain,
sk43(sk49) = tl(sk49),
inference(orient,[status(thm)],[t397933]) ).
cnf(t397934,plain,
cons(sk45(sk49),tl(sk49)) = sk49,
inference(step,[status(thm)],[t387110,t390078]) ).
cnf(t390080,plain,
cons(sk45(sk49),tl(sk49)) = sk49,
inference(rw,[status(thm)],[t397934]) ).
cnf(t390081,plain,
cons(sk45(sk49),tl(sk49)) = sk49,
inference(orient,[status(thm)],[t390080]) ).
cnf(t390084,plain,
true = ifeq(ssItem(sk45(sk49)),true,ifeq(ssItem(sk45(sk49)),true,ifeq(ssList(tl(sk49)),true,memberP(sk49,sk45(sk49)),true),true),true),
inference(cp,[status(thm)],[t24416,t390081]) ).
cnf(t397935,plain,
true = ifeq(true,true,ifeq(ssItem(sk45(sk49)),true,ifeq(ssList(tl(sk49)),true,memberP(sk49,sk45(sk49)),true),true),true),
inference(step,[status(thm)],[t390084,t341116]) ).
cnf(t397936,plain,
true = ifeq(ssItem(sk45(sk49)),true,ifeq(ssList(tl(sk49)),true,memberP(sk49,sk45(sk49)),true),true),
inference(step,[status(thm)],[t397935,t256]) ).
cnf(t397937,plain,
true = ifeq(true,true,ifeq(ssList(tl(sk49)),true,memberP(sk49,sk45(sk49)),true),true),
inference(step,[status(thm)],[t397936,t341116]) ).
cnf(t397938,plain,
true = ifeq(ssList(tl(sk49)),true,memberP(sk49,sk45(sk49)),true),
inference(step,[status(thm)],[t397937,t256]) ).
fof(f23,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssList(tl(U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f23_nnf,plain,
! [U] :
( ssList(tl(U))
| nil = U
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [U] :
( ssList(tl(U))
| nil = U
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c93,plain,
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t105,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssList(tl(X1)),true)),true) = true,
inference(equality_encoding,[status(esa)],[c93]) ).
cnf(t439,plain,
ifeq(ssList(X1),true,or(eq(nil,X1),eq(ssList(tl(X1)),true)),true) = true,
inference(orient,[status(thm)],[t105]) ).
cnf(t390267,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssList(tl(X1)),true)),true) = true,
inference(step,[status(thm)],[t439,t641]) ).
cnf(t674,plain,
ifeq(ssList(X1),true,or(eq(sk48,X1),eq(ssList(tl(X1)),true)),true) = true,
inference(rw,[status(thm)],[t390267]) ).
cnf(t397103,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssList(tl(X1)),true)),true) = true,
inference(step,[status(thm)],[t674,t981]) ).
cnf(t320170,plain,
ifeq(ssList(X1),true,or(eq(sk50,X1),eq(ssList(tl(X1)),true)),true) = true,
inference(orient,[status(thm)],[t397103]) ).
cnf(t321024,plain,
true = ifeq(true,true,or(eq(sk50,sk49),eq(ssList(tl(sk49)),true)),true),
inference(cp,[status(thm)],[t320170,t1634]) ).
cnf(t397104,plain,
true = or(eq(sk50,sk49),eq(ssList(tl(sk49)),true)),
inference(step,[status(thm)],[t321024,t256]) ).
cnf(t397105,plain,
true = or(false,eq(ssList(tl(sk49)),true)),
inference(step,[status(thm)],[t397104,t2179]) ).
cnf(t397106,plain,
true = eq(ssList(tl(sk49)),true),
inference(step,[status(thm)],[t397105,t289]) ).
cnf(t321027,plain,
eq(ssList(tl(sk49)),true) = true,
inference(orient,[status(thm)],[t397106]) ).
cnf(t321028,plain,
true = ifeq(true,true,ssList(tl(sk49)),true),
inference(cp,[status(thm)],[t257,t321027]) ).
cnf(t397107,plain,
true = ssList(tl(sk49)),
inference(step,[status(thm)],[t321028,t256]) ).
cnf(t321037,plain,
ssList(tl(sk49)) = true,
inference(orient,[status(thm)],[t397107]) ).
cnf(t397939,plain,
true = ifeq(true,true,memberP(sk49,sk45(sk49)),true),
inference(step,[status(thm)],[t397938,t321037]) ).
cnf(t397940,plain,
true = memberP(sk49,sk45(sk49)),
inference(step,[status(thm)],[t397939,t256]) ).
cnf(t390153,plain,
memberP(sk49,sk45(sk49)) = true,
inference(orient,[status(thm)],[t397940]) ).
cnf(t390154,plain,
true = ifeq(ssItem(sk45(sk49)),true,ifeq(true,true,memberP(sk50,sk45(sk49)),true),true),
inference(cp,[status(thm)],[t297,t390153]) ).
cnf(t397941,plain,
true = ifeq(true,true,ifeq(true,true,memberP(sk50,sk45(sk49)),true),true),
inference(step,[status(thm)],[t390154,t341116]) ).
cnf(t397942,plain,
true = ifeq(true,true,memberP(sk50,sk45(sk49)),true),
inference(step,[status(thm)],[t397941,t256]) ).
cnf(t397943,plain,
true = memberP(sk50,sk45(sk49)),
inference(step,[status(thm)],[t397942,t256]) ).
cnf(t59,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t291,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t59]) ).
fof(f37,axiom,
! [U] :
( ssItem(U)
=> ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax38) ).
fof(f37_nnf,plain,
! [U] :
( ~ memberP(nil,U)
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [U] :
( ~ memberP(nil,U)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c113,plain,
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(t74,plain,
or(not(ssItem(X1)),not(memberP(nil,X1))) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(t390300,plain,
or(not(ssItem(X1)),not(memberP(sk48,X1))) = true,
inference(step,[status(thm)],[t74,t641]) ).
cnf(t711,plain,
or(not(ssItem(X1)),not(memberP(sk48,X1))) = true,
inference(orient,[status(thm)],[t390300]) ).
cnf(t390359,plain,
or(not(ssItem(X1)),not(memberP(sk50,X1))) = true,
inference(step,[status(thm)],[t711,t981]) ).
cnf(t1006,plain,
or(not(ssItem(X1)),not(memberP(sk50,X1))) = true,
inference(rw,[status(thm)],[t390359]) ).
cnf(t17871,plain,
or(not(ssItem(X1)),not(memberP(sk50,X1))) = true,
inference(orient,[status(thm)],[t1006]) ).
cnf(t341135,plain,
true = or(not(true),not(memberP(sk50,sk45(sk49)))),
inference(cp,[status(thm)],[t17871,t341116]) ).
cnf(t7,plain,
not(true) = false,
introduced(definition) ).
cnf(t769,plain,
not(true) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t397385,plain,
true = or(false,not(memberP(sk50,sk45(sk49)))),
inference(step,[status(thm)],[t341135,t769]) ).
cnf(t397386,plain,
true = not(memberP(sk50,sk45(sk49))),
inference(step,[status(thm)],[t397385,t289]) ).
cnf(t341912,plain,
not(memberP(sk50,sk45(sk49))) = true,
inference(orient,[status(thm)],[t397386]) ).
cnf(t341913,plain,
false = ifeq(true,true,memberP(sk50,sk45(sk49)),false),
inference(cp,[status(thm)],[t291,t341912]) ).
cnf(t397387,plain,
false = memberP(sk50,sk45(sk49)),
inference(step,[status(thm)],[t341913,t256]) ).
cnf(t341914,plain,
memberP(sk50,sk45(sk49)) = false,
inference(orient,[status(thm)],[t397387]) ).
cnf(t397944,plain,
true = false,
inference(step,[status(thm)],[t397943,t341914]) ).
cnf(t390165,plain,
false = true,
inference(orient,[status(thm)],[t397944]) ).
fof(f0,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f0_nnf,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [U,V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssItem(V)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( X0 != X1
| ~ neq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f1,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f1_nnf,plain,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( sk0 != sk1
& ssItem(sk1)
& ssItem(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f1_nnf]) ).
cnf(c4,plain,
sk0 != sk1,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f7,axiom,
! [U] :
( ssList(U)
=> ( cyclefreeP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ~ ( leq(W,V)
& leq(V,W) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f7_nnf,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( leq(W,V)
& leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| cyclefreeP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( ~ leq(W,V)
| ~ leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ cyclefreeP(U) ) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [U,V,W,X,Y,Z] :
( ( ( ( leq(sk10(U),sk9(U))
& leq(sk9(U),sk10(U))
& app(app(sk11(U),cons(sk9(U),sk12(U))),cons(sk10(U),sk13(U))) = U
& ssList(sk13(U))
& ssList(sk12(U))
& ssList(sk11(U))
& ssItem(sk10(U))
& ssItem(sk9(U)) )
| cyclefreeP(U) )
& ( ~ leq(W,V)
| ~ leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z)
| ~ ssList(Y)
| ~ ssList(X)
| ~ ssItem(W)
| ~ ssItem(V)
| ~ cyclefreeP(U) ) )
| ~ ssList(U) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10,sk11,sk12,sk13])],[f7_nnf]) ).
cnf(c22,plain,
( ~ leq(X2,X1)
| ~ leq(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ cyclefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f12,axiom,
! [U] :
( ssList(U)
=> ( duplicatefreeP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> V != W ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f12_nnf,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( V = W
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| duplicatefreeP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( V != W
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ duplicatefreeP(U) ) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [U,V,W,X,Y,Z] :
( ( ( ( sk34(U) = sk35(U)
& app(app(sk36(U),cons(sk34(U),sk37(U))),cons(sk35(U),sk38(U))) = U
& ssList(sk38(U))
& ssList(sk37(U))
& ssList(sk36(U))
& ssItem(sk35(U))
& ssItem(sk34(U)) )
| duplicatefreeP(U) )
& ( V != W
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z)
| ~ ssList(Y)
| ~ ssList(X)
| ~ ssItem(W)
| ~ ssItem(V)
| ~ duplicatefreeP(U) ) )
| ~ ssList(U) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk34,sk35,sk36,sk37,sk38])],[f12_nnf]) ).
cnf(c65,plain,
( X1 != X2
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ duplicatefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f14,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f14_nnf,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [U,V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V)
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c80,plain,
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f17,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) != U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
fof(f17_nnf,plain,
! [U] :
( ! [V] :
( cons(V,U) != U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [U,V] :
( cons(V,U) != U
| ~ ssItem(V)
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c84,plain,
( cons(X1,X0) != X0
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f20,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> nil != cons(V,U) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
fof(f20_nnf,plain,
! [U] :
( ! [V] :
( nil != cons(V,U)
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [U,V] :
( nil != cons(V,U)
| ~ ssItem(V)
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c90,plain,
( nil != cons(X1,X0)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
fof(f32,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( lt(U,V)
=> ~ lt(V,U) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax33) ).
fof(f32_nnf,plain,
! [U] :
( ! [V] :
( ~ lt(V,U)
| ~ lt(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [U,V] :
( ~ lt(V,U)
| ~ lt(U,V)
| ~ ssItem(V)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c103,plain,
( ~ lt(X1,X0)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
fof(f38,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax39) ).
fof(f38_nnf,plain,
~ singletonP(nil),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
~ singletonP(nil),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c114,plain,
~ singletonP(nil),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f89,axiom,
! [U] :
( ssItem(U)
=> ~ lt(U,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax90) ).
fof(f89_nnf,plain,
! [U] :
( ~ lt(U,U)
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [U] :
( ~ lt(U,U)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f89_nnf]) ).
cnf(c182,plain,
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
fof(f92,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( lt(U,V)
<=> ( leq(U,V)
& U != V ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax93) ).
fof(f92_nnf,plain,
! [U] :
( ! [V] :
( ( ( ~ leq(U,V)
| U = V
| lt(U,V) )
& ( ( leq(U,V)
& U != V )
| ~ lt(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
! [U,V] :
( ( ( ~ leq(U,V)
| U = V
| lt(U,V) )
& ( ( leq(U,V)
& U != V )
| ~ lt(U,V) ) )
| ~ ssItem(V)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c185,plain,
( X0 != X1
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
fof(f93,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( gt(U,V)
=> ~ gt(V,U) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax94) ).
fof(f93_nnf,plain,
! [U] :
( ! [V] :
( ~ gt(V,U)
| ~ gt(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
! [U,V] :
( ~ gt(V,U)
| ~ gt(U,V)
| ~ ssItem(V)
| ~ ssItem(U) ),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c188,plain,
( ~ gt(X1,X0)
| ~ gt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(c201,plain,
( ~ segmentP(sk50,app(app(cons(X4,nil),X5),cons(X4,nil)))
| ~ ssList(X5)
| ~ memberP(sk49,X4)
| ~ ssItem(X4) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c4,c22,c65,c80,c84,c90,c103,c113,c114,c182,c185,c188,c197,c201]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t390165]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC046+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.41 % Computer : n007.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Thu Sep 24 16:03:23 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 262.27/38.53 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 262.27/38.53 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------