%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC104+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 : n014.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:22 PM UTC 2026
% Result : Theorem 84.51s 17.28s
% Output : Proof 84.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 24
% Syntax : Number of formulae : 192 ( 129 unt; 0 def)
% Number of atoms : 518 ( 207 equ)
% Maximal formula atoms : 21 ( 2 avg)
% Number of connectives : 558 ( 232 ~; 184 |; 91 &)
% ( 6 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 10 con; 0-4 aty)
% Number of variables : 218 ( 2 sgn 113 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
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(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]) ).
cnf(t166,plain,
or(not(ssList(X1)),or(not(ssList(X2)),or(not(neq(X1,X2)),not(eq(X1,X2))))) = true,
inference(equality_encoding,[status(esa)],[c80]) ).
cnf(t498,plain,
or(not(ssList(X1)),or(not(ssList(X2)),or(not(neq(X1,X2)),not(eq(X1,X2))))) = true,
inference(orient,[status(thm)],[t166]) ).
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( frontsegP(V,U)
& neq(U,nil) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( leq(X2,Z)
& app(X3,cons(X2,nil)) = W
& ssList(X3) )
& ssItem(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ totalorderedP(W)
| app(W,Y) != X ) )
| ~ neq(V,nil)
| 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)
=> ( ( frontsegP(V,U)
& neq(U,nil) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( leq(X2,Z)
& app(X3,cons(X2,nil)) = W
& ssList(X3) )
& ssItem(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ totalorderedP(W)
| app(W,Y) != X ) )
| ~ neq(V,nil)
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f95_nnf,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ~ frontsegP(V,U)
| ~ neq(U,nil) )
& ( nil != W
| nil = X )
& ? [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ~ leq(X2,Z)
| app(X3,cons(X2,nil)) != W
| ~ ssList(X3) )
| ~ ssItem(X2) )
| app(cons(Z,nil),X1) != Y
| ~ ssList(X1) )
| ~ ssItem(Z) )
& totalorderedP(W)
& app(W,Y) = X
& ssList(Y) )
& neq(V,nil)
& 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] :
( ( ~ frontsegP(sk48,sk47)
| ~ neq(sk47,nil) )
& ( nil != sk49
| nil = sk50 )
& ( ~ leq(X2,Z)
| app(X3,cons(X2,nil)) != sk49
| ~ ssList(X3)
| ~ ssItem(X2)
| app(cons(Z,nil),X1) != sk51
| ~ ssList(X1)
| ~ ssItem(Z) )
& totalorderedP(sk49)
& app(sk49,sk51) = sk50
& ssList(sk51)
& neq(sk48,nil)
& sk47 = sk49
& sk48 = sk50
& ssList(sk50)
& ssList(sk49)
& ssList(sk48)
& ssList(sk47) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47,sk48,sk49,sk50,sk51])],[f95_nnf]) ).
cnf(c196,plain,
neq(sk48,nil),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t32,plain,
neq(sk48,nil) = true,
inference(equality_encoding,[status(esa)],[c196]) ).
cnf(t937,plain,
neq(sk48,nil) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(c194,plain,
sk48 = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t1,plain,
sk50 = sk48,
inference(equality_encoding,[status(esa)],[c194]) ).
cnf(t951,plain,
sk48 = sk50,
inference(orient,[status(thm)],[t1]) ).
cnf(t141807,plain,
neq(sk50,nil) = true,
inference(step,[status(thm)],[t937,t951]) ).
cnf(t952,plain,
neq(sk50,nil) = true,
inference(rw,[status(thm)],[t141807]) ).
cnf(t2660,plain,
neq(sk50,nil) = true,
inference(orient,[status(thm)],[t952]) ).
cnf(t2664,plain,
true = or(not(ssList(sk50)),or(not(ssList(nil)),or(not(true),not(eq(sk50,nil))))),
inference(cp,[status(thm)],[t498,t2660]) ).
cnf(c191,plain,
ssList(sk48),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t12,plain,
ssList(sk48) = true,
inference(equality_encoding,[status(esa)],[c191]) ).
cnf(t141809,plain,
ssList(sk50) = true,
inference(step,[status(thm)],[t12,t951]) ).
cnf(t1680,plain,
ssList(sk50) = true,
inference(orient,[status(thm)],[t141809]) ).
cnf(t141867,plain,
true = or(not(true),or(not(ssList(nil)),or(not(true),not(eq(sk50,nil))))),
inference(step,[status(thm)],[t2664,t1680]) ).
cnf(t6,plain,
not(true) = false,
introduced(definition) ).
cnf(t642,plain,
not(true) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t141868,plain,
true = or(false,or(not(ssList(nil)),or(not(true),not(eq(sk50,nil))))),
inference(step,[status(thm)],[t141867,t642]) ).
cnf(t35,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t289,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t35]) ).
cnf(t141869,plain,
true = or(not(ssList(nil)),or(not(true),not(eq(sk50,nil)))),
inference(step,[status(thm)],[t141868,t289]) ).
fof(f16,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f16_nnf,plain,
ssList(nil),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c83,plain,
ssList(nil),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t10,plain,
ssList(nil) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(t1266,plain,
ssList(nil) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t141870,plain,
true = or(not(true),or(not(true),not(eq(sk50,nil)))),
inference(step,[status(thm)],[t141869,t1266]) ).
cnf(t141871,plain,
true = or(false,or(not(true),not(eq(sk50,nil)))),
inference(step,[status(thm)],[t141870,t642]) ).
cnf(t141872,plain,
true = or(not(true),not(eq(sk50,nil))),
inference(step,[status(thm)],[t141871,t289]) ).
cnf(t141873,plain,
true = or(false,not(eq(sk50,nil))),
inference(step,[status(thm)],[t141872,t642]) ).
cnf(t141874,plain,
true = not(eq(sk50,nil)),
inference(step,[status(thm)],[t141873,t289]) ).
cnf(t4022,plain,
not(eq(sk50,nil)) = true,
inference(orient,[status(thm)],[t141874]) ).
cnf(t4023,plain,
false = ifeq(true,true,eq(sk50,nil),false),
inference(cp,[status(thm)],[t291,t4022]) ).
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(t141875,plain,
false = eq(sk50,nil),
inference(step,[status(thm)],[t4023,t256]) ).
cnf(t4024,plain,
eq(sk50,nil) = false,
inference(orient,[status(thm)],[t141875]) ).
cnf(t63,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)],[t63]) ).
cnf(c81,plain,
( X0 = X1
| neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t161,plain,
ifeq(ssList(X1),true,ifeq(ssList(X2),true,or(neq(X1,X2),eq(X1,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c81]) ).
cnf(t415,plain,
ifeq(ssList(X1),true,ifeq(ssList(X2),true,or(neq(X1,X2),eq(X1,X2)),true),true) = true,
inference(orient,[status(thm)],[t161]) ).
cnf(c202,plain,
( ~ frontsegP(sk48,sk47)
| ~ neq(sk47,nil) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t84,plain,
or(not(neq(sk47,nil)),not(frontsegP(sk48,sk47))) = true,
inference(equality_encoding,[status(esa)],[c202]) ).
cnf(t486,plain,
or(not(neq(sk47,nil)),not(frontsegP(sk48,sk47))) = true,
inference(orient,[status(thm)],[t84]) ).
cnf(c195,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t0,plain,
sk49 = sk47,
inference(equality_encoding,[status(esa)],[c195]) ).
cnf(t944,plain,
sk47 = sk49,
inference(orient,[status(thm)],[t0]) ).
cnf(t141803,plain,
or(not(neq(sk49,nil)),not(frontsegP(sk48,sk47))) = true,
inference(step,[status(thm)],[t486,t944]) ).
cnf(t141804,plain,
or(not(neq(sk49,nil)),not(frontsegP(sk48,sk49))) = true,
inference(step,[status(thm)],[t141803,t944]) ).
cnf(t949,plain,
or(not(neq(sk49,nil)),not(frontsegP(sk48,sk49))) = true,
inference(rw,[status(thm)],[t141804]) ).
cnf(t145622,plain,
or(not(neq(sk49,nil)),not(frontsegP(sk50,sk49))) = true,
inference(step,[status(thm)],[t949,t951]) ).
fof(f4,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( frontsegP(U,V)
<=> ? [W] :
( app(V,W) = U
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( app(V,W) != U
| ~ ssList(W) )
| frontsegP(U,V) )
& ( ? [W] :
( app(V,W) = U
& ssList(W) )
| ~ frontsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [U,V,W] :
( ( ( app(V,W) != U
| ~ ssList(W)
| frontsegP(U,V) )
& ( ( app(V,sk5(U,V)) = U
& ssList(sk5(U,V)) )
| ~ frontsegP(U,V) ) )
| ~ ssList(V)
| ~ ssList(U) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f4_nnf]) ).
cnf(c14,plain,
( app(X1,X2) != X0
| ~ ssList(X2)
| frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t201,plain,
ifeq(ssList(X1),true,ifeq(ssList(X2),true,ifeq(ssList(X3),true,ifeq(app(X2,X3),X1,frontsegP(X1,X2),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t402,plain,
ifeq(ssList(X1),true,ifeq(ssList(X2),true,ifeq(ssList(X3),true,ifeq(app(X2,X3),X1,frontsegP(X1,X2),true),true),true),true) = true,
inference(orient,[status(thm)],[t201]) ).
cnf(t403,plain,
true = ifeq(ssList(app(X1,X2)),true,ifeq(ssList(X1),true,ifeq(ssList(X2),true,frontsegP(app(X1,X2),X1),true),true),true),
inference(cp,[status(thm)],[t402,t256]) ).
cnf(t104523,plain,
ifeq(ssList(app(X1,X2)),true,ifeq(ssList(X1),true,ifeq(ssList(X2),true,frontsegP(app(X1,X2),X1),true),true),true) = true,
inference(orient,[status(thm)],[t403]) ).
cnf(c198,plain,
app(sk49,sk51) = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t23,plain,
app(sk49,sk51) = sk50,
inference(equality_encoding,[status(esa)],[c198]) ).
cnf(t613,plain,
app(sk49,sk51) = sk50,
inference(orient,[status(thm)],[t23]) ).
cnf(t104545,plain,
true = ifeq(ssList(sk50),true,ifeq(ssList(sk49),true,ifeq(ssList(sk51),true,frontsegP(app(sk49,sk51),sk49),true),true),true),
inference(cp,[status(thm)],[t104523,t613]) ).
cnf(t144890,plain,
true = ifeq(true,true,ifeq(ssList(sk49),true,ifeq(ssList(sk51),true,frontsegP(app(sk49,sk51),sk49),true),true),true),
inference(step,[status(thm)],[t104545,t1680]) ).
cnf(t144891,plain,
true = ifeq(ssList(sk49),true,ifeq(ssList(sk51),true,frontsegP(app(sk49,sk51),sk49),true),true),
inference(step,[status(thm)],[t144890,t256]) ).
cnf(c190,plain,
ssList(sk47),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t11,plain,
ssList(sk47) = true,
inference(equality_encoding,[status(esa)],[c190]) ).
cnf(t141808,plain,
ssList(sk49) = true,
inference(step,[status(thm)],[t11,t944]) ).
cnf(t1441,plain,
ssList(sk49) = true,
inference(orient,[status(thm)],[t141808]) ).
cnf(t144892,plain,
true = ifeq(true,true,ifeq(ssList(sk51),true,frontsegP(app(sk49,sk51),sk49),true),true),
inference(step,[status(thm)],[t144891,t1441]) ).
cnf(t144893,plain,
true = ifeq(ssList(sk51),true,frontsegP(app(sk49,sk51),sk49),true),
inference(step,[status(thm)],[t144892,t256]) ).
cnf(c197,plain,
ssList(sk51),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t15,plain,
ssList(sk51) = true,
inference(equality_encoding,[status(esa)],[c197]) ).
cnf(t1919,plain,
ssList(sk51) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t144894,plain,
true = ifeq(true,true,frontsegP(app(sk49,sk51),sk49),true),
inference(step,[status(thm)],[t144893,t1919]) ).
cnf(t144895,plain,
true = frontsegP(app(sk49,sk51),sk49),
inference(step,[status(thm)],[t144894,t256]) ).
cnf(t144896,plain,
true = frontsegP(sk50,sk49),
inference(step,[status(thm)],[t144895,t613]) ).
cnf(t105170,plain,
frontsegP(sk50,sk49) = true,
inference(orient,[status(thm)],[t144896]) ).
cnf(t145623,plain,
or(not(neq(sk49,nil)),not(true)) = true,
inference(step,[status(thm)],[t145622,t105170]) ).
cnf(t145624,plain,
or(not(neq(sk49,nil)),false) = true,
inference(step,[status(thm)],[t145623,t642]) ).
cnf(t33,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t288,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t33]) ).
cnf(t145625,plain,
not(neq(sk49,nil)) = true,
inference(step,[status(thm)],[t145624,t288]) ).
cnf(t140751,plain,
not(neq(sk49,nil)) = true,
inference(orient,[status(thm)],[t145625]) ).
cnf(t140752,plain,
false = ifeq(true,true,neq(sk49,nil),false),
inference(cp,[status(thm)],[t291,t140751]) ).
cnf(t145626,plain,
false = neq(sk49,nil),
inference(step,[status(thm)],[t140752,t256]) ).
cnf(t140753,plain,
neq(sk49,nil) = false,
inference(orient,[status(thm)],[t145626]) ).
cnf(t140754,plain,
true = ifeq(ssList(sk49),true,ifeq(ssList(nil),true,or(false,eq(sk49,nil)),true),true),
inference(cp,[status(thm)],[t415,t140753]) ).
cnf(t145627,plain,
true = ifeq(true,true,ifeq(ssList(nil),true,or(false,eq(sk49,nil)),true),true),
inference(step,[status(thm)],[t140754,t1441]) ).
cnf(t145628,plain,
true = ifeq(ssList(nil),true,or(false,eq(sk49,nil)),true),
inference(step,[status(thm)],[t145627,t256]) ).
cnf(t145629,plain,
true = ifeq(true,true,or(false,eq(sk49,nil)),true),
inference(step,[status(thm)],[t145628,t1266]) ).
cnf(t145630,plain,
true = or(false,eq(sk49,nil)),
inference(step,[status(thm)],[t145629,t256]) ).
cnf(t145631,plain,
true = eq(sk49,nil),
inference(step,[status(thm)],[t145630,t289]) ).
cnf(t140758,plain,
eq(sk49,nil) = true,
inference(orient,[status(thm)],[t145631]) ).
cnf(t140759,plain,
nil = ifeq(true,true,sk49,nil),
inference(cp,[status(thm)],[t257,t140758]) ).
cnf(t145632,plain,
nil = sk49,
inference(step,[status(thm)],[t140759,t256]) ).
cnf(t140766,plain,
nil = sk49,
inference(orient,[status(thm)],[t145632]) ).
cnf(t145659,plain,
eq(sk50,sk49) = false,
inference(step,[status(thm)],[t4024,t140766]) ).
cnf(t140782,plain,
eq(sk50,sk49) = false,
inference(rw,[status(thm)],[t145659]) ).
fof(f27,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f27_nnf,plain,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c97,plain,
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(t68,plain,
ifeq(ssList(X1),true,app(nil,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c97]) ).
cnf(t287,plain,
ifeq(ssList(X1),true,app(nil,X1),X1) = X1,
inference(orient,[status(thm)],[t68]) ).
cnf(t1926,plain,
sk51 = ifeq(true,true,app(nil,sk51),sk51),
inference(cp,[status(thm)],[t287,t1919]) ).
cnf(t141828,plain,
sk51 = app(nil,sk51),
inference(step,[status(thm)],[t1926,t256]) ).
cnf(t2889,plain,
app(nil,sk51) = sk51,
inference(orient,[status(thm)],[t141828]) ).
cnf(t145663,plain,
app(sk49,sk51) = sk51,
inference(step,[status(thm)],[t2889,t140766]) ).
cnf(t145664,plain,
sk50 = sk51,
inference(step,[status(thm)],[t145663,t613]) ).
cnf(t140786,plain,
sk50 = sk51,
inference(rw,[status(thm)],[t145664]) ).
cnf(t141694,plain,
sk50 = sk51,
inference(orient,[status(thm)],[t140786]) ).
cnf(t147623,plain,
eq(sk51,sk49) = false,
inference(step,[status(thm)],[t140782,t141694]) ).
cnf(c201,plain,
( nil != sk49
| nil = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t57,plain,
ifeq(nil,sk49,nil,sk50) = sk50,
inference(equality_encoding,[status(esa)],[c201]) ).
cnf(t290,plain,
ifeq(nil,sk49,nil,sk50) = sk50,
inference(orient,[status(thm)],[t57]) ).
cnf(t145685,plain,
ifeq(sk49,sk49,nil,sk50) = sk50,
inference(step,[status(thm)],[t290,t140766]) ).
cnf(t145686,plain,
nil = sk50,
inference(step,[status(thm)],[t145685,t256]) ).
cnf(t145687,plain,
sk49 = sk50,
inference(step,[status(thm)],[t145686,t140766]) ).
cnf(t140805,plain,
sk49 = sk50,
inference(rw,[status(thm)],[t145687]) ).
cnf(t147601,plain,
sk49 = sk51,
inference(step,[status(thm)],[t140805,t141694]) ).
cnf(t141713,plain,
sk49 = sk51,
inference(orient,[status(thm)],[t147601]) ).
cnf(t147624,plain,
eq(sk51,sk51) = false,
inference(step,[status(thm)],[t147623,t141713]) ).
cnf(t24,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t644,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t147625,plain,
true = false,
inference(step,[status(thm)],[t147624,t644]) ).
cnf(t141757,plain,
false = true,
inference(orient,[status(thm)],[t147625]) ).
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(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(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]) ).
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(c200,plain,
( ~ leq(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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c4,c22,c65,c80,c84,c90,c103,c113,c114,c182,c185,c188,c200,c202]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t141757]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC104+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/5.35 % Computer : n014.cluster.edu
% 0.08/5.35 % Model : x86_64 x86_64
% 0.08/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.35 % Memory : 8046.5625MB
% 0.08/5.35 % OS : Linux 6.8.0-71-generic
% 0.08/5.35 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Thu Sep 24 16:24:24 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 84.51/17.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 84.51/17.28 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------